Quelle  Vwalk.thy

theory Vwalk
  imports Pair_Graph
begin

section ‹A Theory on Vertex Walks in a Digraph›

context fixes G :: "'v dgraph" begin
inductive vwalk where
  vwalk0: "vwalk []" |
  vwalk1: "v ∈ dVs G ==> vwalk [v]" |
  vwalk2: "(u,v) ∈ G ==> vwalk (v#vs) ==> vwalk (u#v#vs)"
end
declare vwalk0[simp]

inductive_simps vwalk_1[simp]: "vwalk E [v]"

inductive_simps vwalk_2[simp]: "vwalk E (u # v # vs)"

definition vwalk_bet::"('v × 'v) set ==> 'v ==> 'v list ==> 'v ==> bool" where 
  "vwalk_bet G u p v = ( vwalk G p ∧ p ≠ [] ∧ hd p = u ∧ last p = v)"

lemma vwalk_then_edge: "vwalk_bet dG u p v ==> u ≠ v ==> (∃v''. (u, v'') ∈ dG)"
  by(cases p; auto split: if_splits simp: neq_Nil_conv vwalk_bet_def)

lemma vwalk_then_in_dVs: "vwalk dG p ==> v ∈ set p ==> v ∈ dVs dG"
  by(induction rule: vwalk.induct) (auto simp: dVs_def)

lemma vwalk_cons: "vwalk dG (v1#v2#p) ==> (v1,v2) ∈ dG"
  by simp

lemma hd_of_vwalk_bet:
  "vwalk_bet dG v p v' ==> ∃p'. p = v # p'"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

lemma hd_of_vwalk_bet': 
  "vwalk_bet dG v p v' ==> v = hd p"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

― ‹TODO: intro›

lemma hd_of_vwalk_bet'': "vwalk_bet dG u p v ==> u ∈ set p"
  using hd_of_vwalk_bet
  by force 

lemma last_of_vwalk_bet: 
  "vwalk_bet dG v p v' ==> v' = last p"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

lemma last_of_vwalk_bet': 
  "vwalk_bet dG v p v' ==> ∃p'. p = p' @ [v']"
  by(auto simp: vwalk_bet_def dest: append_butlast_last_id[symmetric])

lemma append_vwalk_pref: "vwalk dG (p1 @ p2) ==> vwalk dG p1"
  by (induction p1) (fastforce intro: vwalk.intros elim: vwalk.cases simp: dVsI)+

lemma append_vwalk_suff: "vwalk dG (p1 @ p2) ==> vwalk dG p2"
  by (induction p1) (fastforce intro: vwalk.intros elim: vwalk.cases simp:)+

lemma append_vwalk: "vwalk dG p1 ==> vwalk dG p2 ==> (p1 ≠ [] ==> p2 ≠ [] ==> (last p1, hd p2) ∈ dG) ==> vwalk dG (p1 @ p2)"
  by (induction p1) (fastforce intro: vwalk.intros elim: vwalk.cases simp: dVsI)+

― ‹TODO: dest›
lemma split_vwalk:
  "vwalk_bet dG v1 (p1 @ v2 # p2) v3 ==> vwalk_bet dG v2 (v2 # p2) v3"
  unfolding vwalk_bet_def
proof (induction p1)
  case (Cons v p1)
  then show ?case 
    by (auto intro: append_vwalk_suff[where ?p1.0 = "v1 # p1"] simp add: vwalk_then_in_dVs vwalk_bet_def)
qed auto

lemma vwalk_bet_cons:
  "vwalk_bet dG v (v # p) u ==> p ≠ [] ==> vwalk_bet dG (hd p) p u"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

lemma vwalk_bet_cons_2: 
  "vwalk_bet dG v p v' ==> p ≠ [] ==> vwalk_bet dG v (v # tl p) v'"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

lemma vwalk_bet_snoc: 
  "vwalk_bet dG v' (p @ [v]) v'' ==> v = v''"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

lemma vwalk_bet_vwalk:
  "p ≠ [] ==> vwalk_bet dG (hd p) p (last p) ⟷ vwalk dG p"
  by(auto simp: neq_Nil_conv vwalk_bet_def)

lemma vwalk_snoc_edge': "vwalk dG (p @ [v]) ==> (v, v') ∈ dG ==> vwalk dG ((p @ [v]) @ [v'])"
  by (rule append_vwalk) (auto simp add: dVs_def)

lemma vwalk_snoc_edge: "vwalk dG (p @ [v]) ==> (v, v') ∈ dG ==> vwalk dG (p @ [v, v'])"
  using vwalk_snoc_edge'
  by simp

lemma vwalk_snoc_edge_2: "vwalk dG (p @ [v, v']) ==> (v, v') ∈ dG"
  using append_vwalk_suff[where ?p2.0 = "[v, v']"]
  by auto

lemma vwalk_append_edge: "vwalk dG (p1 @ p2) ==> p1 ≠ [] ==> p2 ≠ [] ==> (last p1, hd p2) ∈ dG"
  by (induction p1) (auto simp: vwalk_then_in_dVs neq_Nil_conv)

lemma vwalk_transitive_rel:
  assumes "(∧x y z. R x y ==> R y z ==> R x z)" "(∧v1 v2. (v1, v2) ∈ dG ==> R v1 v2)"
  shows "vwalk dG (v#vs) ==> v' ∈ set vs ==> R v v'"
proof(induction vs arbitrary: v v')
  case (Cons v'' vs)
  hence "R v v''"
    using assms(2)
    by simp
  thus ?case
  proof(cases "v' = v''")
    case False
    thus ?thesis
      apply(intro assms(1)[OF ‹R v v''›] Cons)
      using Cons.prems
      by auto
  qed simp
qed auto

lemma vwalk_transitive_rel': 
  assumes "(∧x y z. R x y ==> R y z ==> R x z)" "(∧v1 v2. (v1, v2) ∈ dG ==> R v1 v2)"
  shows "vwalk dG (vs @ [v]) ==> v' ∈ set vs ==> R v' v"
proof(induction vs arbitrary: v v' rule: rev_induct)
  case (snoc v'' vs)
  hence "R v'' v"
    by(auto intro: assms vwalk_snoc_edge_2)    
  thus ?case
  proof(cases "v' = v''")
    case True
    then show ?thesis 
      by (simp add: ‹R v'' v›)
  next
    case False
    thus ?thesis
      apply(intro assms(1)[OF _ ‹R v'' v›] snoc append_vwalk_pref[where ?p1.0 = "vs @ [v'']"])
      using snoc(2,3)
      by auto
  qed
qed auto


fun edges_of_vwalk where
  "edges_of_vwalk [] = []" |
  "edges_of_vwalk [v] = []" |
  "edges_of_vwalk (v#v'#l) = (v, v') # edges_of_vwalk (v'#l)"

lemma vwalk_ball_edges: "vwalk E p ==> b ∈ set (edges_of_vwalk p) ==> b ∈ E"
  by (induction p rule: edges_of_vwalk.induct, auto)

lemma edges_of_vwalk_index:
  "Suc i < length p ==> edges_of_vwalk p ! i = (p ! i, p ! Suc i)"
proof (induction i arbitrary: p)
  case (Suc i)
  then obtain u v ps where "p = u#v#ps" by (auto dest!: Suc_leI simp: Suc_le_length_iff)
  hence "edges_of_vwalk (v#ps) ! i = ((v#ps) ! i, (v#ps) ! Suc i)" using Suc.IH Suc.prems by simp
  then show ?case using ‹p = u#v#ps› by simp
qed (auto dest!: Suc_leI simp: Suc_le_length_iff)

lemma edges_of_vwalk_length: "length (edges_of_vwalk p) = length p - 1"
  by (induction p rule: edges_of_vwalk.induct, auto)

text ‹With the given assumptions we can only obtain an outgoing edge from term‹v›.›
lemma edges_of_vwalk_for_inner:
  assumes "p ! i = v" "Suc i < length p"
  obtains w where "edges_of_vwalk p ! i = (v, w)"
  by (simp add: assms edges_of_vwalk_index)

text ‹For an incoming edge we need an additional assumption (term‹i > 0›).›
lemma edges_of_vwalk_for_inner':
  assumes "p ! (Suc i) = v" "Suc i < length p"
  obtains u where "(u, v) = edges_of_vwalk p ! i"
  using assms by (simp add: edges_of_vwalk_index)

lemma hd_edges_neq_last:  
  "[(last p, hd p) ∉ set (edges_of_vwalk p); hd p ≠ last p; p ≠ []] ==>
   hd (edges_of_vwalk (last p # p)) ≠ last (edges_of_vwalk (last p # p))"
  by (induction p) (auto elim: edges_of_vwalk.elims)

lemma v_in_edge_in_vwalk: 
  assumes "(u, v) ∈ set (edges_of_vwalk p)"
  shows "u ∈ set p" "v ∈ set p"
  using assms
  by (induction p rule: edges_of_vwalk.induct) auto


lemma distinct_edges_of_vwalk:
  "distinct p ==> distinct (edges_of_vwalk p)"
  by (induction p rule: edges_of_vwalk.induct) (auto dest: v_in_edge_in_vwalk)

lemma distinct_edges_of_vwalk_cons:
  "distinct (edges_of_vwalk (v # p)) ==> distinct (edges_of_vwalk p)"
  by (cases p; simp)

lemma tl_vwalk_is_vwalk: "vwalk E p ==> vwalk E (tl p)"
  by (induction p rule: vwalk.induct; simp)

lemma vwalk_concat:
  assumes "vwalk E p" "vwalk E q" "q ≠ []" "p ≠ [] ==> last p = hd q"
  shows "vwalk E (p @ tl q)"
  using assms
  by (induction p) (simp_all add: tl_vwalk_is_vwalk)

lemma edges_of_vwalk_append_2:
  "p' ≠ [] ==> edges_of_vwalk (p @ p') = edges_of_vwalk (p @ [hd p']) @ edges_of_vwalk p'"
  by (induction p rule: induct_list012) (auto intro: list.exhaust[of p'])

lemma edges_of_vwalk_append: "∃ep. edges_of_vwalk (p @ p') = ep @ edges_of_vwalk p'"
  by (cases "p' = []") (auto dest: edges_of_vwalk_append_2)

lemma append_butlast_last_cancel: "p ≠ [] ==> butlast p @ last p # p' = p @ p'"
  by simp

lemma edges_of_vwalk_append_3:
  assumes "p ≠ []"
  shows "edges_of_vwalk (p @ p') = edges_of_vwalk p @ edges_of_vwalk (last p # p')"
  using assms
  by (auto simp flip: append_butlast_last_cancel simp: edges_of_vwalk_append_2)

lemma vwalk_vertex_has_edge:
  assumes "length p ≥ 2" "v ∈ set p"
  obtains e u where "e ∈ set (edges_of_vwalk p)" "e = (u, v) ∨ e = (v, u)"
proof -
  obtain i where idef: "p ! i = v" "i < length p" 
    using assms(2) by (auto simp: in_set_conv_nth)
  have eodplength': "Suc (length (edges_of_vwalk p)) = length p"
    using assms(1) by (auto simp: edges_of_vwalk_length)
  hence eodplength: "length (edges_of_vwalk p) ≥ 1" using assms(1) by simp

  from idef consider (nil) "i = 0" | (gt) "i > 0" "Suc i < length p" | (last) "Suc i = length p"
    by linarith
  thus ?thesis
  proof cases
    case nil
    hence "edges_of_vwalk p ! 0 = (p ! 0, p ! 1)" using edges_of_vwalk_index assms(1) by force
    then show ?thesis using that nil idef eodplength
      by (force simp: in_set_conv_nth)
  next
    case gt
    then obtain w where w: "(v, w) = edges_of_vwalk p ! i"
      by (auto elim: edges_of_vwalk_for_inner[OF idef(1)])
    have "i < length (edges_of_vwalk p)"
      using eodplength' gt(2) by auto
    then show ?thesis using that w[symmetric] nth_mem by blast
  next
    case last
    then obtain w where w: "(w, v) = edges_of_vwalk p ! (i - 1)"
      using edges_of_vwalk_for_inner'[of p "i - 1"] eodplength' eodplength
      by (auto simp: idef)
    have "i - 1 < length (edges_of_vwalk p)"
      using eodplength eodplength' last by linarith
    then show ?thesis using that w[symmetric] nth_mem by blast
  qed
qed

lemma v_in_edge_in_vwalk_inj:
  assumes "e ∈ set (edges_of_vwalk p)"
  obtains u v where "e = (u, v)"
  by fastforce

lemma v_in_edge_in_vwalk_gen:
  assumes "e ∈ set (edges_of_vwalk p)" "e = (u, v)"
  shows "u ∈ set p" "v ∈ set p"
  using assms v_in_edge_in_vwalk by simp_all

lemma edges_of_vwalk_dVs: "dVs (set (edges_of_vwalk p)) ⊆ set p"
  by (auto intro: v_in_edge_in_vwalk simp: dVs_def)

lemma last_v_snd_last_e:
  assumes "length p ≥ 2"
  shows "last p = snd (last (edges_of_vwalk p))" ― ‹is this the best formulation for this?›
  using assms
  by (induction p rule: induct_list012) 
     (auto split: if_splits elim: edges_of_vwalk.elims simp: Suc_leI)

lemma hd_v_fst_hd_e:
  assumes "length p ≥ 2"
  shows "hd p = fst (hd (edges_of_vwalk p))"
  using assms
  by (auto dest: Suc_leI simp: Suc_le_length_iff numeral_2_eq_2)

lemma last_in_edge:
   "p ≠ [] ==> ∃u. (u, last p) ∈ set (edges_of_vwalk (v # p)) ∧ u ∈ set (v # p)"
  by (induction p arbitrary: v) auto

lemma edges_of_vwalk_append_subset:
  shows "set (edges_of_vwalk p') ⊆ set (edges_of_vwalk (p @ p'))"
  by (fastforce intro: exE[OF edges_of_vwalk_append, of p p'])

lemma nonempty_vwalk_vwalk_bet[intro?]:
  assumes "vwalk E p" "p ≠ []" "hd p = u" "last p = v"
  shows "vwalk_bet E u p v"
  using assms
  unfolding vwalk_bet_def
  by blast

lemma vwalk_bet_nonempty:
  assumes "vwalk_bet E u p v"
  shows [simp]: "p ≠ []"
  using assms 
  unfolding vwalk_bet_def by blast

lemma vwalk_bet_nonempty_vwalk[elim]:
  assumes "vwalk_bet E u p v"
  shows "vwalk E p" "p ≠ []" "hd p = u" "last p = v"
  using assms 
  unfolding vwalk_bet_def by blast+

lemma vwalk_bet_reflexive[intro]:
  assumes "w ∈ dVs E"
  shows "vwalk_bet E w [w] w"
  using assms 
  unfolding vwalk_bet_def by simp

lemma singleton_hd_last: "q ≠ [] ==> tl q = [] ==> hd q = last q"
  by (cases q) simp_all

lemma singleton_hd_last': "q ≠ [] ==> butlast q = [] ==> hd q = last q"
  by (cases q) auto

lemma vwalk_bet_transitive:
  assumes "vwalk_bet E u p v" "vwalk_bet E v q w"
  shows "vwalk_bet E u (p @ tl q) w"
  using assms
  unfolding vwalk_bet_def
  by (auto intro: vwalk_concat simp: last_append singleton_hd_last last_tl)

lemma vwalk_bet_in_dVs:
  assumes "vwalk_bet E a p b"
  shows "set p ⊆ dVs E"
  using assms vwalk_then_in_dVs
  unfolding vwalk_bet_def by fast

lemma vwalk_bet_endpoints:
  assumes "vwalk_bet E u p v"
  shows [simp]: "u ∈ dVs E"
  and   [simp]: "v ∈ dVs E"
  using assms vwalk_then_in_dVs
  unfolding vwalk_bet_def by fastforce+

lemma vwalk_bet_pref:
  assumes "vwalk_bet E u (pr @ [x] @ su) v"
  shows "vwalk_bet E u (pr @ [x]) x"
  using assms
  unfolding vwalk_bet_def
  by (auto simp: append_vwalk_pref) (simp add: hd_append)

lemma vwalk_bet_suff:
  assumes "vwalk_bet E u (pr @ [x] @ su) v"
  shows "vwalk_bet E x (x # su) v"
  using append_vwalk_suff assms 
  unfolding vwalk_bet_def by auto

lemma edges_are_vwalk_bet:
  assumes "(v, w) ∈ E"
  shows "vwalk_bet E v [v, w] w"
  unfolding vwalk_bet_def
  using assms
  by (simp add: dVsI)

lemma induct_vwalk_bet[case_names path1 path2, consumes 1, induct set: vwalk_bet]:
  assumes "vwalk_bet E a p b"
  assumes Path1: "∧v. v ∈ dVs E ==> P E [v] v v"
  assumes Path2: "∧v v' vs b. (v, v') ∈ E ==> vwalk_bet E v' (v' # vs) b ==> P E (v' # vs) v' b ==> P E (v # v' # vs) v b"
  shows "P E p a b"
proof -
  have "vwalk E p" "p ≠ []" "hd p = a" "last p = b" using assms(1) by auto
  thus ?thesis
  proof (induction p arbitrary: a b)
    case vwalk0
    then show ?case by simp
  next
    case vwalk1
    then show ?case using Path1 by fastforce
  next
    case (vwalk2 v v' vs a b)
    then have "vwalk_bet E v' (v' # vs) b"
      by (simp add: vwalk2.hyps(1) vwalk_bet_def)
    then show ?case using vwalk2 Path2
      by auto
  qed
qed

lemma vwalk_append:
  assumes "vwalk E xs" "vwalk E ys" "last xs = hd ys"
  shows "vwalk E (xs @ tl ys)"
  using assms vwalk_concat by fastforce

lemma vwalk_append2:
  assumes "vwalk E (xs @ [x])" "vwalk E (x # ys)"
  shows "vwalk E (xs @ x # ys)"
  using assms by (auto dest: vwalk_append)

lemma vwalk_appendD_last:
  "vwalk E (xs @ [x, y]) ==> vwalk E (xs @ [x])"
  by (simp add: append_vwalk_pref)

lemma vwalk_ConsD:
  "vwalk E (x # xs) ==> vwalk E xs"
  by (auto dest: tl_vwalk_is_vwalk)

lemmas vwalkD = vwalk_ConsD append_vwalk_pref append_vwalk_suff

lemma vwalk_alt_induct[consumes 1, case_names Single Snoc]:
  assumes
    "vwalk E p"  "P []" "(∧x. P [x])"
    "∧y x xs. (y, x) ∈ E ==> vwalk E (xs @ [y]) ==> P (xs @ [y]) ==> P (xs @ [y, x])"
  shows "P p"
  using assms(1)
proof (induction rule: rev_induct)
  case Nil
  then show ?case by (simp add: assms)
next
  case (snoc x xs)
  then show ?case
    by (cases xs rule: rev_cases) (auto intro!: assms simp add: vwalk_snoc_edge_2 append_vwalk_pref)
qed

lemma vwalk_append_single:
  assumes "vwalk E p" "(last p, x) ∈ E"
  shows "vwalk E (p @ [x])"
  using assms
  by (auto intro!: append_vwalk dest: dVsI)

lemmas vwalk_decomp = append_vwalk_pref append_vwalk_suff vwalk_append_edge

lemma vwalk_rotate:
  assumes "vwalk E (x # xs @ y # ys @ [x])"
  shows "vwalk E (y # ys @ x # xs @ [y])"
proof -
  from vwalk_decomp[of E "x # xs" "y # ys @ [x]"] assms have
    "vwalk E (x # xs)" "vwalk E (y # ys @ [x])" "(last (x # xs), y) ∈ E"
    by auto
  then have "vwalk E (x # xs @ [y])"
    by (auto dest: vwalk_append_single)
  from vwalk_append[OF ‹vwalk E (y # ys @ [x])› this] show ?thesis by auto
qed

lemma vwalk_bet_nonempty'[simp]: "¬ vwalk_bet E u [] v" 
  unfolding vwalk_bet_def by simp

lemma vwalk_ConsE: 
  assumes "vwalk E (a # p)" "p ≠ []"
  obtains e where "e ∈ E" "e = (a, hd p)" "vwalk E p"
  using assms
  by (metis vwalk_2 hd_Cons_tl)

lemma vwalk_reachable:
  "p ≠ [] ==> vwalk E p ==> hd p →^* last p"
  by (induction p rule: list_nonempty_induct)
     (auto elim!: vwalk_ConsE simp: reachable_def converse_rtrancl_on_into_rtrancl_on dVsI)

lemma vwalk_reachable':
  "vwalk E p ==> p ≠ [] ==> hd p = u ==> last p = v ==> u →^* v"
  by (auto dest: vwalk_reachable)

lemma vwalkI: "(x, hd p) ∈ E ==> vwalk E p ==> vwalk E (x#p)" 
  by (induction p) (auto simp: dVsI)

lemma reachable_vwalk:
  assumes "u →^* v"
  shows "∃p. hd p = u ∧ last p = v ∧ vwalk E p ∧ p ≠ []"
  using assms
  apply induction
   apply force
  apply clarsimp
  subgoal for x p
    by (auto intro!: exI[where x="x#p"] vwalkI)
  done

lemma reachable_vwalk_iff:
  "u →^* v ⟷ (∃p. hd p = u ∧ last p = v ∧ vwalk E p ∧ p ≠ [])"
  by (auto simp: vwalk_reachable reachable_vwalk)

lemma reachable_vwalk_bet_iff:
  "u →^* v ⟷ (∃p. vwalk_bet E u p v)"
  by (auto simp: reachable_vwalk_iff vwalk_bet_def)

lemma reachable_vwalk_betD:
  "vwalk_bet E u p v ==> u →^* v"
  using iffD2[OF reachable_vwalk_bet_iff]
  by force

lemma vwalk_reachable1:
  "vwalk E (u # p @ [v]) ==> u →⁺ v"
  by (induction p arbitrary: u) (auto simp add: trancl_into_trancl2)

lemma reachable1_vwalk:
  assumes "u →⁺ v"
  shows "∃p. vwalk E (u # p @ [v])"
proof -
  from assms obtain w where "(u,w) ∈ E" "w →^* v"
    by (meson converse_tranclE reachable1_in_dVs(2) reachable1_reachable reachable_refl)
  from reachable_vwalk[OF this(2)] obtain p where *: "hd p = w" "last p = v" "vwalk E p" "p ≠ []"
    by auto
  then obtain p' where [simp]: "p = p' @ [v]"
    by (auto intro!: append_butlast_last_id[symmetric])
  with ‹(u,w) ∈ E› * show ?thesis
    by (auto intro: vwalkI)
qed

lemma reachable1_vwalk_iff:
  "u →⁺ v ⟷ (∃p. vwalk E (u # p @ [v]))"
  by (auto simp: vwalk_reachable1 reachable1_vwalk)

lemma reachable_vwalk_iff2:
  "u →^* v ⟷ (u = v ∧ u ∈ dVs E ∨ (∃p. vwalk E (u # p @ [v])))"
  by (auto dest: reachable1_vwalk simp: reachable_in_dVs vwalk_reachable1 reachable1_reachable)

lemma vwalk_remove_cycleE:
  assumes "vwalk E (u # p @ [v])"
  obtains p' where "vwalk E (u # p' @ [v])" 
    "distinct p'" "u ∉ set p'" "v ∉ set p'" "set p' ⊆ set p"
  using assms
proof (induction "length p" arbitrary: p rule: less_induct)
  case less
  note prems = less.prems(2) and intro = less.prems(1) and IH = less.hyps
  consider
    "distinct p" "u ∉ set p" "v ∉ set p" | "u ∈ set p" | "v ∈ set p" | "¬ distinct p" by auto
  then consider (goal) ?case
    | (a) as bs where "p = as @ u # bs" | (b) as bs where "p = as @ v # bs"
    | (between) x as bs cs where "p = as @ x # bs @ x # cs"
    using prems
    by (cases, auto dest: not_distinct_decomp split_list intro: intro)
  then show ?case
  proof cases
    case a
    with prems show ?thesis
      by - (rule IH[where p = "bs"], auto 4 3 intro: intro dest: vwalkD)
  next
    case b
    with prems have "vwalk E (u # as @ v # [] @ (bs @ [v]))" by simp
    then have "vwalk E (u # as @ [v])" by (auto simp: append_vwalk_pref)
    with b show ?thesis
      by - (rule IH[where p = "as"], auto 4 3 intro: intro)
  next
    case between
    with prems have expanded: "vwalk E ((u # as @ x # bs) @ x # cs @ [v])" by simp
    then have xv: "vwalk E (x # cs @ [v])" by (rule append_vwalk_suff)
    have ux: "vwalk E ((u # as) @ [x])" using append_vwalk_pref expanded by force
    with xv have "vwalk E ((u # as) @ x # cs @ [v])"
      using vwalk_append2[OF ux xv] by auto
    with between show ?thesis
      by - (rule IH[where p = "as @ x # cs"], auto 4 3 intro: intro)
  qed
qed

abbreviation closed_vwalk_bet :: "('v × 'v) set ==> 'v list ==> 'v ==> bool" where
  "closed_vwalk_bet E c v ≡ vwalk_bet E v c v ∧ Suc 0 < length c"

lemma edge_iff_vwalk_bet: "(u, v) ∈ E = vwalk_bet E u [u, v] v"
  by (auto simp: edges_are_vwalk_bet vwalk_bet_def dVsI)

lemma vwalk_bet_in_vertices: "vwalk_bet E u p v ==> w ∈ set p ==> w ∈ dVs E"
  by (auto intro: vwalk_then_in_dVs)

lemma vwalk_bet_hd_neq_last_implies_edges_nonempty:
  assumes "vwalk_bet E u p v"
  assumes "u ≠ v"
  shows "E ≠ {}"
  using assms
  by (induction p) (auto dest: vwalk_then_edge)

lemma vwalk_bet_edges_in_edges: "vwalk_bet E u p v ==> set (edges_of_vwalk p) ⊆ E"
  by (auto simp add: vwalk_bet_def intro: vwalk_ball_edges)

lemma vwalk_bet_prefix_is_vwalk_bet:
  assumes "p ≠ []"
  assumes "vwalk_bet E u (p @ q) v"
  shows "vwalk_bet E u p (last p)"
  using assms
  by (auto simp: vwalk_bet_def dest: append_vwalk_pref)

lemma vwalk_bet_suffix_is_vwalk_bet:
  assumes "q ≠ []"
  assumes "vwalk_bet E u (p @ q) v"
  shows "vwalk_bet E (hd q) q v"
  using assms
  by (auto simp: vwalk_bet_def dest: append_vwalk_suff)

lemma vwalk_bet_append_append_is_vwalk_bet:
  assumes "vwalk_bet E u p v"
  assumes "vwalk_bet E v q w"
  assumes "vwalk_bet E w r x"
  shows "vwalk_bet E u (p @ tl q @ tl r) x"
  using assms
  by (auto dest: vwalk_bet_transitive)

lemma 
  assumes "p ≠ []"
  shows "edges_of_vwalk (p @ q) = edges_of_vwalk p @ edges_of_vwalk ([last p] @ q)"
  using assms
  by (simp add: edges_of_vwalk_append_3)

fun is_vwalk_bet_vertex_decomp :: "('v × 'v) set ==> 'v list ==> 'v ==> 'v list × 'v list ==> bool" where
  "is_vwalk_bet_vertex_decomp E p v (q, r) ⟷ p = q @ tl r ∧ (∃u w. vwalk_bet E u q v ∧ vwalk_bet E v r w)"

definition vwalk_bet_vertex_decomp :: "('v × 'v) set ==> 'v list ==> 'v ==> 'v list × 'v list" where
  "vwalk_bet_vertex_decomp E p v = ( SOME qr. is_vwalk_bet_vertex_decomp E p v qr)"


lemma vwalk_bet_vertex_decompE:
  assumes p_vwalk: "vwalk_bet E u p v"
  assumes p_decomp: "p = xs @ y # ys"
  obtains q r where
    "p = q @ tl r"
    "q = xs @ [y]"
    "r = y # ys"
    "vwalk_bet E u q y"
    "vwalk_bet E y r v"
  using assms
  by (simp add: vwalk_bet_pref split_vwalk)

lemma vwalk_bet_vertex_decomp_is_vwalk_bet_vertex_decomp:
  assumes p_vwalk: "vwalk_bet E u p w"
  assumes v_in_p: "v ∈ set p"
  shows "is_vwalk_bet_vertex_decomp E p v (vwalk_bet_vertex_decomp E p v)"
proof -
  obtain xs ys where
    "p = xs @ v # ys"
    using v_in_p by (auto simp: in_set_conv_decomp)
  with p_vwalk
  obtain q r where
    "p = q @ tl r"
    "vwalk_bet E u q v"
    "vwalk_bet E v r w"
    by (blast elim: vwalk_bet_vertex_decompE)
  hence "is_vwalk_bet_vertex_decomp E p v (q, r)"
    by (simp add: vwalk_bet_def)
  hence "∃qr. is_vwalk_bet_vertex_decomp E p v qr"
    by blast
  thus ?thesis
    unfolding vwalk_bet_vertex_decomp_def
    ..
qed

lemma vwalk_bet_vertex_decompE_2:
  assumes p_vwalk: "vwalk_bet E u p w"
  assumes v_in_p: "v ∈ set p"
  assumes qr_def: "vwalk_bet_vertex_decomp E p v = (q, r)"
  obtains
    "p = q @ tl r"
    "vwalk_bet E u q v"
    "vwalk_bet E v r w"
proof
  have *: "is_vwalk_bet_vertex_decomp E p v (q, r)"
    using assms by (auto dest: vwalk_bet_vertex_decomp_is_vwalk_bet_vertex_decomp)
  then obtain u' w' where
    p_decomp: "p = q @ tl r" and
    q_vwalk: "vwalk_bet E u' q v" and
    r_vwalk: "vwalk_bet E v r w'"
    by auto
  hence "vwalk_bet E u' p w'" by (simp add: vwalk_bet_transitive)
  hence "u' = u" "w' = w" using p_vwalk by (simp_all add: vwalk_bet_def)
  thus
    "p = q @ tl r"
    "vwalk_bet E u q v"
    "vwalk_bet E v r w"
    using p_decomp q_vwalk r_vwalk by simp_all
qed


definition vtrail :: "('v × 'v) set ==> 'v ==> 'v list ==> 'v ==> bool" where
  "vtrail E u p v = ( vwalk_bet E u p v ∧ distinct (edges_of_vwalk p))"

abbreviation closed_vtrail :: "('v × 'v) set ==> 'v list ==> 'v ==> bool" where
  "closed_vtrail E c v ≡ vtrail E v c v ∧ Suc 0 < length c"

lemma closed_vtrail_implies_Cons:
  assumes "closed_vtrail E c v"
  shows "c = v # tl c"
  using assms
  by (auto simp add: vtrail_def vwalk_bet_def)

lemma tl_non_empty_conv:
  shows "tl l ≠ [] ⟷ Suc 0 < length l"
proof -
  have "tl l ≠ [] ⟷ 0 < length (tl l)"
    by blast
  also have "... ⟷ Suc 0 < length l"
    by simp
  finally show ?thesis
    .
qed

lemma closed_vtrail_implies_tl_nonempty:
  assumes "closed_vtrail E c v"
  shows "tl c ≠ []"
  using assms
  by (simp add: tl_non_empty_conv)

lemma vtrail_in_vertices:
  "vtrail E u p v ==> w ∈ set p ==> w ∈ dVs E"
  by (auto simp add: vtrail_def intro: vwalk_bet_in_vertices)

lemma
  assumes "vtrail E u p v"
  shows vtrail_hd_in_vertices: "u ∈ dVs E"
  and vtrail_last_in_vertices: "v ∈ dVs E"
  using assms
  by (auto intro: vwalk_bet_endpoints simp: vtrail_def)

lemma list_set_tl: "x ∈ set (tl xs) ==> x ∈ set xs"
  by (cases xs) auto

lemma closed_vtrail_hd_tl_in_vertices:
  assumes "closed_vtrail E c v"
  shows "hd (tl c) ∈ dVs E"
  using assms
  by (auto intro!: vtrail_in_vertices simp flip: tl_non_empty_conv simp add: list_set_tl)

lemma vtrail_prefix_is_vtrail:
  notes vtrail_def [simp]
  assumes "p ≠ []"
  assumes "vtrail E u (p @ q) v"
  shows "vtrail E u p (last p)"
  using assms 
  by (auto simp: vwalk_bet_prefix_is_vwalk_bet edges_of_vwalk_append_3)

lemma vtrail_suffix_is_vtrail:
  notes vtrail_def [simp]
  assumes "q ≠ []"
  assumes "vtrail E u (p @ q) v"
  shows "vtrail E (hd q) q v"
  using assms
  by (auto simp: vwalk_bet_suffix_is_vwalk_bet edges_of_vwalk_append_2[OF ‹q ≠ []›])

definition distinct_vwalk_bet :: "('v × 'v) set ==> 'v ==> 'v list ==> 'v ==> bool" where
  "distinct_vwalk_bet E u p v = ( vwalk_bet E u p v ∧ distinct p)"

lemma distinct_vwalk_bet_length_le_card_vertices:
  assumes "distinct_vwalk_bet E u p v"
  assumes "finite E"
  shows "length p ≤ card (dVs E)"
  using assms
  unfolding distinct_vwalk_bet_def
  by (auto dest!: distinct_card[symmetric] intro!: card_mono simp: vwalk_bet_in_vertices finite_vertices_iff)

lemma distinct_vwalk_bet_triples_finite:
  assumes "finite E"
  shows "finite {(p, u, v). distinct_vwalk_bet E u p v}"
proof (rule finite_subset)
  have "∧p u v. vwalk_bet E u p v ==> distinct p ==> length p ≤ card (dVs E)"
    by (auto intro!: distinct_vwalk_bet_length_le_card_vertices simp: distinct_vwalk_bet_def assms)
  thus "{(p, u, v). distinct_vwalk_bet E u p v} ⊆
    {p. set p ⊆ dVs E ∧ length p ≤ card (dVs E)} × dVs E × dVs E"
    by (auto simp: distinct_vwalk_bet_def vwalk_bet_in_vertices)
  show "finite …"
    by (auto intro!: finite_cartesian_product finite_lists_length_le 
             simp: assms finite_vertices_iff)
qed

lemma distinct_vwalk_bets_finite:
  "finite E ==> finite {p. distinct_vwalk_bet E u p v}"
  by (rule finite_surj[OF  distinct_vwalk_bet_triples_finite]) auto

section‹Vwalks to paths (as opposed to arc walks (term‹awalk_to_apath› before)›
fun is_closed_decomp :: "('v × 'v) set ==> 'v list ==> 'v list × 'v list × 'v list ==> bool" where
  "is_closed_decomp E p (q, r, s) ⟷
    p = q @ tl r @ tl s ∧
    (∃u v w. vwalk_bet E u q v ∧ closed_vwalk_bet E r v ∧ vwalk_bet E v s w) ∧
    distinct q"

definition closed_vwalk_bet_decomp :: "('v × 'v) set ==> 'v list ==> 'v list × 'v list × 'v list" where
  "closed_vwalk_bet_decomp E p = ( SOME qrs. is_closed_decomp E p qrs)"

lemma closed_vwalk_bet_decompE:
  assumes p_vwalk: "vwalk_bet E u p v"
  assumes p_decomp: "p = xs @ y # ys @ y # zs"
  obtains q r s where
    "p = q @ tl r @ tl s"
    "q = xs @ [y]"
    "r = y # ys @ [y]"
    "s = y # zs"
    "vwalk_bet E u q y"
    "vwalk_bet E y r y"
    "vwalk_bet E y s v"
  using assms
  by auto (metis Cons_eq_appendI vwalk_bet_vertex_decompE)

lemma closed_vwalk_bet_decomp_is_closed_decomp:
  assumes p_vwalk: "vwalk_bet E u p v"
  assumes p_not_distinct: "¬ distinct p"
  shows "is_closed_decomp E p (closed_vwalk_bet_decomp E p)"
proof -
  obtain xs y ys zs where
    "p = xs @ y # ys @ y # zs" and
    xs_distinct: "distinct xs" and
    y_not_in_xs: "y ∉ set xs"
    using p_not_distinct not_distinct_decomp    
    by (smt append.assoc append.simps(2) in_set_conv_decomp_first not_distinct_conv_prefix)
  from p_vwalk this(1)
  obtain q r s where
    "p = q @ tl r @ tl s"
    "q = xs @ [y]"
    "r = y # ys @ [y]"
    "s = y # zs"
    "vwalk_bet E u q y"
    "vwalk_bet E y r y"
    "vwalk_bet E y s v"
    by (erule closed_vwalk_bet_decompE)
  moreover hence
    "distinct q"
    "Suc 0 < length r"
    using xs_distinct y_not_in_xs
    by simp+
  ultimately have
    "∃q r s.
      p = q @ tl r @ tl s ∧
      (∃u v w. vwalk_bet E u q v ∧ closed_vwalk_bet E r v ∧ vwalk_bet E v s w) ∧
      distinct q"
    by blast
  hence "∃qrs. is_closed_decomp E p qrs" by simp
  thus ?thesis unfolding closed_vwalk_bet_decomp_def ..
qed

lemma closed_vwalk_bet_decompE_2:
  assumes p_vwalk: "vwalk_bet E u p v"
  assumes p_not_distinct: "¬ distinct p"
  assumes qrs_def: "closed_vwalk_bet_decomp E p = (q, r, s)"
  obtains
    "p = q @ tl r @ tl s"
    "∃w. vwalk_bet E u q w ∧ closed_vwalk_bet E r w ∧ vwalk_bet E w s v"
    "distinct q"
proof -
  have "is_closed_decomp E p (q, r, s)"
    unfolding qrs_def[symmetric]
    using p_vwalk p_not_distinct
    by (rule closed_vwalk_bet_decomp_is_closed_decomp)
  then obtain u' w' v' where
    p_decomp: "p = q @ tl r @ tl s" and
    q_distinct: "distinct q" and
    vwalks: "vwalk_bet E u' q w'"
    "closed_vwalk_bet E r w'"
    "vwalk_bet E w' s v'"
    by auto
  hence "vwalk_bet E u' p v'"
    by (auto intro: vwalk_bet_append_append_is_vwalk_bet)
  hence "u' = u" "v' = v"
    using p_vwalk
    by (simp_all add: vwalk_bet_def)
  hence "∃w. vwalk_bet E u q w ∧ closed_vwalk_bet E r w ∧ vwalk_bet E w s v"
    using vwalks by blast
  with p_decomp q_distinct that
  show ?thesis by blast
qed

function vwalk_bet_to_distinct :: "('v × 'v) set ==> 'v list ==> 'v list" where
  "vwalk_bet_to_distinct E p =
    (if (∃u v. vwalk_bet E u p v) ∧ ¬ distinct p
     then let (q, r, s) = closed_vwalk_bet_decomp E p in vwalk_bet_to_distinct E (q @ tl s)
     else p)"
  by auto

termination vwalk_bet_to_distinct
proof (relation "measure (length ∘ snd)")
  fix E p qrs rs q r s
  assume
    p_not_vwalk: "(∃u v. vwalk_bet E u p v) ∧ ¬ distinct p" and
    assms: "qrs = closed_vwalk_bet_decomp E p"
    "(q, rs) = qrs"
    "(r, s) = rs"
  then obtain u v where
    p_vwalk: "vwalk_bet E u p v"
    by blast
  hence "(q, r, s) = closed_vwalk_bet_decomp E p"
    using assms
    by simp
  then obtain
    "p = q @ tl r @ tl s"
    "Suc 0 < length r"
    using p_vwalk p_not_vwalk
    by (elim closed_vwalk_bet_decompE_2) auto
  thus "((E, (q @ tl s)), E, p) ∈ measure (length ∘ snd)"
    by auto
qed simp

lemma vwalk_bet_to_distinct_induct [consumes 1, case_names path decomp]:
  assumes "vwalk_bet E u p v"
  assumes distinct: "∧p. [ vwalk_bet E u p v; distinct p ] ==> P p"
  assumes
    decomp: "∧p q r s. [ vwalk_bet E u p v; ¬ distinct p;
      closed_vwalk_bet_decomp E p = (q, r, s); P (q @ tl s) ] ==> P p"
  shows "P p"
  using assms(1)
proof (induct "length p" arbitrary: p rule: less_induct)
  case less
  show ?case
  proof (cases "distinct p")
    case True
    with less.prems
    show ?thesis
      by (rule distinct)
  next
    case False
    obtain q r s where
      qrs_def: "closed_vwalk_bet_decomp E p = (q, r, s)"
      by (cases "closed_vwalk_bet_decomp E p")
    with less.prems False
    obtain
      "p = q @ tl r @ tl s"
      "∃w. vwalk_bet E u q w ∧ closed_vwalk_bet E r w ∧ vwalk_bet E w s v"
      by (elim closed_vwalk_bet_decompE_2)
    hence
      "length (q @ tl s) < length p"
      "vwalk_bet E u (q @ tl s) v"
      by (auto simp: tl_non_empty_conv intro: vwalk_bet_transitive)
    hence "P (q @ tl s)"
      by (rule less.hyps)
    with less.prems False qrs_def
    show ?thesis
      by (rule decomp)
  qed
qed

lemma vwalk_bet_to_distinct_is_distinct_vwalk_bet:
  assumes "vwalk_bet E u p v"
  shows "distinct_vwalk_bet E u (vwalk_bet_to_distinct E p) v"
  using assms
  by (induction rule: vwalk_bet_to_distinct_induct) (auto simp: distinct_vwalk_bet_def)

lemma vwalk_betE[elim?]:
  assumes "vwalk_bet E u p v"
  assumes singleton: "[ v∈ dVs E; u = v] ==> P"
  assumes
    step: "∧p' x. [ p = u#x#p'; (u,x)∈E; vwalk_bet E x (x#p') v] ==> P"
  shows "P"
  using assms
  by (induction rule: induct_vwalk_bet) auto

lemma vwalk_subset:
  "[vwalk G p; G ⊆ G'] ==> vwalk G' p"
  by (induction p rule: vwalk.induct) (auto simp: dVs_def)

lemma vwalk_bet_subset:
  "[vwalk_bet G u p v; G ⊆ G'] ==> vwalk_bet G' u p v"
  using vwalk_subset
  by (auto simp: vwalk_bet_def)

lemma reachable_subset[intro]:
  "[u →^* v; G ⊆ G'] ==> u →^*_' v"
  by(auto simp add: reachable_vwalk_bet_iff dest: vwalk_bet_subset)

lemma reachable_Union_1[intro]:
  "[u →^* v] ==> u →^* _{∪ G'} v"
  "[u →^* v] ==> u →^*_{' ∪ G} v"
  by auto

lemma reachableE[elim?]:
  assumes "reachable E u v"
  assumes singleton: "[ v∈ dVs E; u = v] ==> P"
  assumes
    step: "∧x. [ (u,x)∈E; reachable E x v] ==> P"
  shows "P"
  using assms
  by (metis converse_tranclE reachable1_reachable reachable_in_dVs(2) reachable_neq_reachable1 reachable_refl)


lemma vwalk_insertE[case_names nil sing1 sing2 in_e in_E]:
   "[vwalk (insert e E) p;
     (p = [] ==> P);
     (∧u v. p = [v] ==> e = (u,v) ==> P);
     (∧u v. p = [v] ==> e = (v,u) ==> P);
     (∧v. p = [v] ==> v ∈ dVs E ==> P);
     (∧p' v1 v2. [vwalk {e} [v1, v2]; vwalk (insert e E) (v2 # p'); p = v1 # v2 # p'] ==> P);
     (∧p' v1 v2. [vwalk E [v1,v2]; vwalk (insert e E) (v2 # p'); p = v1 # v2 # p'] ==> P )]
    ==> P"
proof(induction rule: vwalk.induct)
  case vwalk0
  then show ?case 
    by auto
next
  case (vwalk1 v)
  then show ?case
    by (auto simp: dVs_def)
next
  case (vwalk2 v v' vs)
  then show ?case
    apply (auto simp: dVs_def)
    by (metis insertCI)
qed

text ‹A lemma which allows for case splitting over paths when doing induction on graph edges.›

lemma vwalk_bet_insertE[case_names nil sing1 sing2 in_e in_E]:
   "[vwalk_bet (insert e E) v1 p v2;
     ([v1∈dVs (insert e E); v1 = v2; p = []] ==> P);
     (∧u v. p = [u] ==> e = (u,v) ==> P);
     (∧u v. p = [v] ==> e = (u,v) ==> P);
     (∧v. p = [v] ==> v = v1 ==> v = v2 ==> v ∈ dVs E ==> P);
     (∧p' v3. [vwalk_bet {e} v1 [v1,v3] v3; vwalk_bet (insert e E) v3 (v3 # p') v2; p = v1 # v3 # p'] ==> P);
     (∧p' v3. [vwalk_bet E v1 [v1,v3] v3; vwalk_bet (insert e E) v3 (v3 # p') v2; p = v1 # v3 # p'] ==> P)]
    ==> P"
  unfolding vwalk_bet_def
  apply safe
  apply(erule vwalk_insertE)
  by (simp | force)+

find_theorems name: induct vwalk_bet

lemma vwalk_bet2[simp]:
  "vwalk_bet G u (u # v # vs) b ⟷ ((u,v) ∈ G ∧ vwalk_bet G v (v # vs) b)"
  by(auto simp: vwalk_bet_def)

(*lemma assumes "vwalk_bet G' u p v""G \<subseteq> G'""u \<in> dVs G"
  shows "vwalk_bet G u p v \<or> 
       (\<exists>p1 w p2. vwalk_bet G' u p1 w \<and> w \<in> dVs G \<and> hd p2 \<notin> dVs G \<and> vwalk_bet G' w (w#p2) v)"
  using assms                              
proof(induction rule: induct_vwalk_bet)
  case (path1 v)
  then show ?case 
   by auto
next
  case (path2 u v vs b)
  then show ?case
  proof(cases "(u,v) \<notin> G")
    case T1: True
    then show ?thesis
    proof(cases "v \<notin> dVs G")
      case T2: True
      hence "vwalk_bet G u [u] u \<and> hd (v # vs) \<notin> dVs G \<and> vwalk_bet G' u (u # v # vs) b"
        using path2
        by auto
      then show ?thesis
        by metis
    next
      case F2: False
      hence "v \<in> dVs G"
        by auto
      hence "vwalk_bet G v (v # vs) b \<or> (\<exists>p1 w p2. vwalk_bet G v p1 w \<and> hd p2 \<notin> dVs G \<and> vwalk_bet G' w (w # p2) b)"
        using path2
        by auto
      with path2 show ?thesis
      proof(elim disjE, goal_cases)
        case 1
        then show ?case
          by auto
      next
        case 2
        then show ?case sorry
      qed

    qed
    
  next
    case False
    then show ?thesis sorry
  qed
qed

  
  find_theorems name: split vwalk_bet
*)

lemma butlast_vwalk_is_vwalk: "vwalk E p ==> vwalk E (butlast p)"
  by (induction p rule: vwalk.induct, auto)


lemma vwalk_concat_2:
  assumes "vwalk E p" "vwalk E q" "q ≠ []" "p ≠ [] ==> last p = hd q"
  shows "vwalk E (butlast p @ q)"
  using assms
  by (induction rule: vwalk.induct) (auto simp add: butlast_vwalk_is_vwalk neq_Nil_conv)

lemma vwalk_bet_transitive_2:
  assumes "vwalk_bet E u p v" "vwalk_bet E v q w"
  shows "vwalk_bet E u (butlast p @ q) w"
  using assms
  unfolding vwalk_bet_def
  by (auto intro!: vwalk_concat_2 simp: last_append singleton_hd_last' neq_Nil_conv)

 lemma vwalk_not_vwalk: 
   "[vwalk G p; ¬vwalk G' p] ==>
          (∃(u,v) ∈ set (edges_of_vwalk p). (u,v) ∈ (G - G')) ∨
          (∃v∈set p. v ∈ (dVs G - dVs G'))"
  by(induction rule: vwalk.induct) (auto simp: dVs_def)


 lemma vwalk_not_vwalk_2: 
   "[vwalk G p; ¬vwalk G' p; length p ≥ 2] ==>
          (∃(u,v) ∈ set (edges_of_vwalk p). (u,v) ∈ (G - G'))"
   apply (induction rule: vwalk.induct) 
   apply (auto simp: dVs_def)
   by (metis Suc_leI dVsI(2) length_greater_0_conv vwalk_1)

 lemma vwalk_not_vwalk_elim: 
   "[vwalk G p; ¬vwalk G' p] ==>
          [∧u v. [(u,v) ∈ set (edges_of_vwalk p); (u,v) ∈ (G - G')] ==> P;
          ∧v. [v∈set p; v ∈ (dVs G - dVs G')] ==> P] ==> P"
   using vwalk_not_vwalk
   by blast

 lemma vwalk_not_vwalk_elim_2: 
   "[vwalk G p; ¬vwalk G' p; length p ≥ 2] ==>
          [∧u v. [(u,v) ∈ set (edges_of_vwalk p); (u,v) ∈ (G - G')] ==> P
          ] ==> P"
   using vwalk_not_vwalk_2
   by blast


 lemma vwalk_bet_not_vwalk_bet: 
   "[vwalk_bet G u p v; ¬vwalk_bet G' u p v] ==>
          (∃(u,v) ∈ set (edges_of_vwalk p). (u,v) ∈ (G - G')) ∨
          (∃v∈set p. v ∈ (dVs G - dVs G'))"
   using vwalk_not_vwalk
   by (auto simp: vwalk_bet_def)

 lemma vwalk_bet_not_vwalk_bet_elim: 
   "[vwalk_bet G u p v; ¬vwalk_bet G' u p v] ==>
          [∧u v. [(u,v) ∈ set (edges_of_vwalk p); (u,v) ∈ (G - G')] ==> P;
          ∧v. [v∈set p; v ∈ (dVs G - dVs G')] ==> P] ==> P"
   using vwalk_not_vwalk_elim
   apply (auto simp: vwalk_bet_def)
   by blast

 lemma vwalk_bet_not_vwalk_bet_elim_2: 
   "[vwalk_bet G u p v; ¬vwalk_bet G' u p v; length p ≥ 2] ==>
          [∧u v. [(u,v) ∈ set (edges_of_vwalk p); (u,v) ∈ (G - G')] ==> P
          ] ==> P"
   using vwalk_not_vwalk_elim_2
   apply (auto simp: vwalk_bet_def)
   by blast


lemma vwalk_bet_props:
  "vwalk_bet G u p v ==> ([vwalk G p; p≠[]; hd p = u; last p = v] ==> P) ==> P"
  by (auto simp: vwalk_bet_def)

lemma no_outgoing_last:
  "[vwalk G p; ∧v. (u,v) ∉ G; u ∈ set p] ==> last p = u"
  by(induction rule: vwalk.induct) (auto simp: dVs_def)

lemma not_vwalk_bet_empty: "¬ Vwalk.vwalk_bet {} u p v"
  by (auto simp: vwalk_bet_def neq_Nil_conv split: if_splits)

lemma edges_in_vwalk_split:
     "(u, v) ∈ set (edges_of_vwalk p) ==> ∃ p1 p2. p = p1 @[u,v]@p2" 
proof(induction p rule: edges_of_vwalk.induct)
  case (3 a b p)
  show ?case 
  proof(cases "(a, b) = (u, v)")
    case True
    hence "a # b # p = [u, v] @ p" by auto
    then show ?thesis by auto
  next
    case False
    hence "(u, v) ∈ set (edges_of_vwalk (b # p))"
      using 3(2) by auto
    then obtain p1 p2 where "b # p = p1 @ [u, v] @ p2"
      using 3(1) by auto
    hence "a#b # p = (a#p1) @ [u, v] @ p2" by auto
    then show ?thesis by fast
  qed
qed simp+

end