Quelle  UGraph.thy

section ‹UGraph - undirected graph with Uprod edges›

theory UGraph
  imports 
    "Automatic_Refinement.Misc"
    "Collections.Partial_Equivalence_Relation"
    "HOL-Library.Uprod"   
begin

subsection "Edge path"

fun epath :: "'a uprod set ==> 'a ==> ('a uprod) list ==> 'a ==> bool"  where
  "epath E u [] v = (u = v)"
| "epath E u (x#xs) v ⟷ (∃w. u≠w ∧ Upair u w = x ∧ epath E w xs v) ∧ x∈E"  

lemma [simp,intro!]: "epath E u [] u" by simp

lemma epath_subset_E: "epath E u p v ==> set p ⊆ E"
  apply(induct p arbitrary: u) by auto 

lemma path_append_conv[simp]: "epath E u (p@q) v ⟷ (∃w. epath E u p w ∧ epath E w q v)"
  apply(induct p arbitrary: u) by auto

lemma epath_rev[simp]: "epath E y (rev p) x = epath E x p y"
  apply(induct p arbitrary: x) by auto

lemma "epath E x p y ==> ∃p. epath E y p x"
  apply(rule exI[where x="rev p"]) by simp

lemma epath_mono: "E ⊆ E' ==> epath E u p v ==> epath E' u p v"
  apply(induct p arbitrary: u) by auto

lemma epath_restrict: "set p ⊆ I ==> epath E u p v ==> epath (E∩I) u p v"
  apply(induct p arbitrary: u)
  by auto

lemma assumes "A⊆A'" "~ epath A u p v" "epath A' u p v"
  shows epath_diff_edge: "(∃e. e∈set p - A)"
proof (rule ccontr)
  assume "¬(∃e. e ∈ set p - A)" 
  then have i: "set p ⊆ A"
    by auto
  have ii: "A = A' ∩ A" using assms(1) by auto
  have "epath A u p v" 
    apply(subst ii) 
    apply(rule epath_restrict  ) by fact+
  with assms(2) show "False" by auto    
qed


lemma epath_restrict': "epath (insert e E) u p v ==> e∉set p ==> epath E u p v"
proof -
  assume a: "epath (insert e E) u p v" and "e∉set p"
  then have b: "set p ⊆ E" by(auto dest: epath_subset_E)
  have e: "insert e E ∩ E = E " by auto   
  show ?thesis apply(rule epath_restrict[where I=E and E="insert e E", simplified e] )
    using a b by auto
qed

lemma epath_not_direct:
  assumes ep: "epath E u p v" and unv: "u ≠ v"
    and edge_notin: "Upair u v ∉ E" 
  shows "length p ≥ 2"
proof (rule ccontr)
  from ep have setp: "set p ⊆ E" using epath_subset_E by fast
  assume "¬length p ≥ 2"
  then have "length p <2" by auto
  moreover
  {
    assume "length p = 0"
    then have "p=[]" by auto
    with ep unv have "False" by auto
  } moreover {
    assume "length p = 1"
    then obtain e where p: "p = [e]"
      using list_decomp_1 by blast 
    with ep have i: "e=Upair u v" by auto
    from p i setp and edge_notin have "False" by auto
  }
  ultimately show "False" by linarith
qed


lemma epath_decompose:
  assumes e: "epath G v p v'"
    and elem :"Upair a b ∈ set p"
  shows  "∃ u u' p' p'' . u ∈ {a, b} ∧ u' ∈ {a, b} ∧ epath G v p' u ∧ epath G u' p'' v' ∧
          length p' < length p ∧ length p'' < length p"
proof -
  from elem obtain p' p'' where p: "p = p' @ (Upair a b) # p''" using in_set_conv_decomp
    by metis
  from p have "epath G v (p' @ (Upair a b) # p'') v'" using e by auto
  then obtain z z' where pr: "epath G v p' z"  "epath G z' p'' v'" and u: "Upair z z'=Upair a b"   by auto 
  from u have u': "z ∈ {a, b} ∧ z' ∈ {a, b}" by auto
  have len: "length p' < length p"  "length p'' < length p" using p by auto    
  from len pr u' show ?thesis by auto
qed

lemma epath_decompose':
  assumes e: "epath G v p v'"
    and elem :"Upair a b ∈ set p"
  shows  "∃ u u' p' p'' . Upair a b = Upair u u' ∧ epath G v p' u ∧ epath G u' p'' v' ∧
          length p' < length p ∧ length p'' < length p"
proof -
  from elem obtain p' p'' where p: "p = p' @ (Upair a b) # p''" using in_set_conv_decomp
    by metis
  from p have "epath G v (p' @ (Upair a b) # p'') v'" using e by auto
  then obtain z z' where pr: "epath G v p' z"  "epath G z' p'' v'" and u: "Upair z z'=Upair a b"   by auto 
  have len: "length p' < length p"  "length p'' < length p" using p by auto    
  from len pr u show ?thesis by auto
qed


(* adapted from Julian's is_path_undir_split_distinct *)
lemma epath_split_distinct:
  assumes "epath G v p v'"
  assumes "Upair a b ∈ set p"
  shows "(∃p' p'' u u'.
            epath G v p' u ∧ epath G u' p'' v' ∧
            length p' < length p ∧ length p'' < length p ∧
            (u ∈ {a, b} ∧ u' ∈ {a, b}) ∧
            Upair a b ∉ set p' ∧ Upair a b ∉ set p'')"
  using assms
proof (induction n == "length p" arbitrary: p v v' rule: nat_less_induct)
  case 1
  obtain u u' p' p'' where u: "u ∈ {a, b} ∧ u' ∈ {a, b}"
    and p': "epath G v p' u" and p'': "epath G u' p'' v'"
    and len_p': "length p' < length p" and len_p'': "length p'' < length p"
    using epath_decompose[OF 1(2,3)] by blast
  from 1 len_p' p' have "Upair a b ∈ set p' ⟶ (∃p'2 u2.
            epath G v p'2 u2 ∧
            length p'2 < length p' ∧
            u2 ∈ {a, b} ∧
            Upair a b ∉ set p'2)"
    by metis
  with len_p' p' u have p': "∃p' u. epath G v p' u ∧ length p' < length p ∧
      u ∈ {a,b} ∧ Upair a b ∉ set p' ∧ Upair a b ∉ set p'"
    by fastforce
  from 1 len_p'' p'' have "Upair a b ∈ set p'' ⟶ (∃p''2 u'2.
            epath G u'2 p''2 v' ∧
            length p''2 < length p'' ∧
            u'2 ∈ {a, b} ∧
            Upair a b ∉ set p''2 ∧ Upair a b ∉ set p''2)"
    by metis
  with len_p'' p'' u have "∃p'' u'. epath G u' p'' v'∧ length p'' < length p ∧
      u' ∈ {a,b} ∧ Upair a b ∉ set p'' ∧ Upair a b ∉ set p''"
    by fastforce
  with p' show ?case by auto
qed

 

subsection "Distinct edge path"


definition "depath E u dp v ≡ epath E u dp v ∧ distinct dp"      

lemma epath_to_depath: "set p ⊆ I ==> epath E u p v ==> ∃dp. depath E u dp v ∧ set dp ⊆ I"
proof (induction p rule: length_induct)
  case (1 p)
  hence IH: "∧p'. [length p' < length p; set p' ⊆ I; epath E u p' v]
    ==> ∃p'. depath E u p' v ∧ set p' ⊆ I"
    and PATH: "epath E u p v"
    and set: "set p ⊆ I"
    by auto

  show "∃p. depath E u p v ∧ set p ⊆ I"  
  proof cases
    assume "distinct p"
    thus ?thesis using PATH set by (auto simp: depath_def)
  next
    assume "¬(distinct p)"  
    then obtain pv1 pv2 pv3 w where p: "p = pv1@w#pv2@w#pv3" 
      by (auto dest: not_distinct_decomp) 
    with PATH obtain a where 1: "epath E u pv1 a" and 2:"epath E a (w#pv2@w#pv3) v" by auto
    then obtain b where ab: "w=Upair a b" "a≠b" by auto 
    with 2 have "epath E b (pv2@w#pv3) v" by auto
    then obtain c where 3: "epath E b pv2 c" and 4: "epath E c (w#pv3) v" by auto
    then have cw: "c∈set_uprod w" by auto
    { assume "c=a"
      then have "length (pv1@w#pv3) < length p" "set (pv1@w#pv3) ⊆ I" "epath E u (pv1@w#pv3) v"
        using 1 4 p set by auto
      hence "∃p'. depath E u p' v ∧ set p' ⊆ I" by (rule IH)
    }
    moreover
    { assume "c≠a"
      with ab cw have "c=b" by auto
      with 4 ab have "epath E a pv3 v" by auto
      then have "length (pv1@pv3) < length p" "set (pv1@pv3) ⊆ I" "epath E u (pv1@pv3) v" using p 1 set by auto
      hence "∃p'. depath E u p' v ∧ set p' ⊆ I" by (rule IH)
    }
    ultimately show ?case by auto
  qed
qed

lemma epath_to_depath': "epath E u p v ==> ∃dp. depath E u dp v"
  using epath_to_depath[where I="set p"] by blast

definition "decycle E u p == epath E u p u ∧ length p > 2 ∧ distinct p"

subsection "Connectivity in undirected Graphs"    

definition "uconnected E ≡ {(u,v). ∃p. epath E u p v}"  

lemma uconnectedempty: "uconnected {} = {(a,a)|a. True}"
  unfolding uconnected_def 
  using epath.elims(2) by fastforce    

lemma uconnected_refl: "refl (uconnected E)"
  by(auto simp: refl_on_def uconnected_def)  

lemma uconnected_sym: "sym (uconnected E)"
  apply(clarsimp simp: sym_def uconnected_def) 
  subgoal for x y p apply (rule exI[where x="rev p"]) by (auto) done
lemma uconnected_trans: "trans (uconnected E)"
  apply(clarsimp simp: trans_def uconnected_def) 
  subgoal for x y p z q by (rule exI[where x="p@q"], auto) done

lemma uconnected_symI: "(u,v) ∈ uconnected E ==> (v,u) ∈ uconnected E"    
  using uconnected_sym sym_def by fast

lemma "equiv UNIV (uconnected E)"
proof (rule equivI)
  show "uconnected E ⊆ UNIV × UNIV"
    by simp
next
  show "refl (uconnected E)"
    by (auto simp: refl_on_def uconnected_def)
next
  show "sym (uconnected E)"
    by (simp add: uconnected_sym)
next
  show "trans (uconnected E)"
    using uconnected_trans .
qed

lemma uconnected_refcl: "(uconnected E)^* = (uconnected E)⁼"
  apply(rule trans_rtrancl_eq_reflcl)
  by (fact uconnected_trans)

lemma uconnected_transcl: "(uconnected E)^* = uconnected E"
  apply (simp only: uconnected_refcl)
  by (auto simp: uconnected_def)

lemma uconnected_mono: "A⊆A' ==> uconnected A ⊆ uconnected A'"
  unfolding uconnected_def apply(auto)
    using epath_mono by metis



lemma findaugmenting_edge: assumes "epath E1 u p v"
  and "¬(∃p. epath E2 u p v)"
shows "∃a b. (a,b) ∉ uconnected E2 ∧ Upair a b ∉ E2 ∧ Upair a b ∈ E1"
  using assms
proof (induct p arbitrary: u)
  case Nil 
  then show ?case by auto
next
  case (Cons a p)
  then obtain w where axy: "a=Upair u w" "u≠w" and e': "epath E1 w p v"
      and uwE1: "Upair u w ∈ E1" by auto
  show ?case
  proof (cases "a∈E2")
    case True
    have e2': "¬(∃p. epath E2 w p v)"
    proof (rule ccontr, clarsimp)
      fix p2
      assume "epath E2 w p2 v"
      with True axy have "epath E2 u (a#p2) v" by auto
      with Cons(3) show False by blast
    qed
    from Cons(1)[OF e' e2'] show ?thesis .
  next
    case False
    {
      assume e2': "¬(∃p. epath E2 w p v)"
      from Cons(1)[OF e' e2'] have ?thesis .
    } moreover {
      assume e2': "∃p. epath E2 w p v"
      then obtain p1 where p1: "epath E2 w p1 v" by auto  

      from False axy have "Upair u w∉E2" by auto
      moreover
      have "(u,w) ∉ uconnected E2"
      proof(rule ccontr, auto simp add: uconnected_def)
        fix p2 
        assume "epath E2 u p2 w"
        with p1 have "epath E2 u (p2@p1) v" by auto
        then show "False" using Cons(3) by blast
      qed
      moreover
      note uwE1   
      ultimately have ?thesis by auto
    }
    ultimately show ?thesis by auto
  qed
qed


subsection "Forest"

definition "forest E ≡ ~(∃u p. decycle E u p)"

lemma forest_mono: "Y ⊆ X ==> forest X ==> forest Y"  
  unfolding forest_def decycle_def apply (auto) using epath_mono by metis

lemma forrest2_E: assumes "(u,v) ∈ uconnected E"
  and "Upair u v ∉ E"                    
  and "u ≠ v" 
shows "~ forest (insert (Upair u v) E)"
proof -
  from assms[unfolded uconnected_def] obtain p' where "epath E u p' v" by blast
  then obtain p where ep: "epath E u p v" and dep: "distinct p" using epath_to_depath' unfolding depath_def by fast
  from ep have setp: "set p ⊆ E" using epath_subset_E by fast

  have lengthp: "length p ≥ 2" apply(rule epath_not_direct) by fact+

  from epath_mono[OF _ ep] have ep': "epath (insert (Upair u v) E) u p v" by auto

  have "epath (insert (Upair u v) E) v ((Upair u v)#p) v" "length ((Upair u v)#p) > 2"  "distinct ((Upair u v)#p)"
    using ep' assms(3) lengthp dep setp assms(2) by auto
  then have "decycle (insert (Upair u v) E) v ((Upair u v)#p)" unfolding decycle_def by auto
  then show ?thesis unfolding forest_def by auto
qed

lemma insert_stays_forest_means_not_connected: assumes "forest (insert (Upair u v) E)"
  and "(Upair u v) ∉ E"
  and "u ≠ v"
shows "~ (u,v) ∈ uconnected E"
  using forrest2_E assms by metis 

lemma epath_singleton: "epath F a [e] b ==> e = Upair a b"
  by auto

lemma forest_alt1: 
  assumes " Upair a b ∈ F" "forest F" "∧e. e∈F ==> proper_uprod e"
  shows "(a,b) ∉ uconnected (F - {Upair a b})"
proof (rule ccontr)
  from assms(1,3) have anb: "a≠b" by force
  assume "¬ (a, b) ∉ uconnected (F - {Upair a b})"
  then obtain p where "epath (F - {Upair a b}) a p b" unfolding uconnected_def  by blast
  then obtain p' where dp: "depath (F - {Upair a b}) a p' b" using epath_to_depath' by force
  then have ab: "Upair a b ∉ set p'" by(auto simp: depath_def dest: epath_subset_E)
  from anb dp have n0: "length p' ≠ 0" by (auto simp: depath_def)
  from ab dp have n1: "length p' ≠ 1" by (auto simp: depath_def simp del: One_nat_def dest!: list_decomp_1)
  from n0 n1 have l: "length p' ≥ 2" by linarith
  from dp have "epath F a p' b" by (auto intro: epath_mono simp: depath_def)
  then have e: "epath F b (Upair a b#p') b" using assms(1) anb by auto
  from dp ab have d: "distinct (Upair a b#p')" by (auto simp: depath_def)
  from d e l have "decycle F b (Upair a b#p')" by (auto simp: decycle_def)
  with assms(2) show "False" by (simp add: forest_def)
qed


lemma forest_alt2: 
  assumes "∧e. e∈F ==> proper_uprod e"
    and "∧a b. Upair a b ∈ F ==> (a,b) ∉ uconnected (F - {Upair a b})"
  shows "forest F"
proof (rule ccontr)
  assume "¬ forest F"  
  then obtain a p where e: "epath F a p a" "length p > 2" "distinct p"
    unfolding decycle_def forest_def by auto
  then obtain b p' where p': "p = Upair a b # p'" 
    by (metis Suc_1 epath.simps(2) less_imp_not_less list.size(3) neq_NilE zero_less_Suc)
  then have u: "Upair a b∈F" using e(1) by auto
  then have F: "(insert (Upair a b) F) = F" by auto
  have "epath (F - {Upair a b}) b p' a"
    apply(rule epath_restrict'[where e="Upair a b"]) using e  p' by (auto simp: F)
  then have "epath (F - {Upair a b}) a (rev p') b" by auto
  with   assms(2)[OF u]
  show "False" unfolding uconnected_def by blast
qed


lemma forest_alt:
  assumes "∧e. e∈F ==> proper_uprod e"
  shows "forest F ⟷ (∀a b. Upair a b ∈ F ⟶ (a,b) ∉ uconnected (F - {Upair a b})) "
  using assms forest_alt1 forest_alt2
  by metis
  


lemma augment_forest_overedges: 
  assumes "F⊆E" "forest F" "(Upair u v) ∈ E" "(u,v) ∉ uconnected F"
    and notsame: "u≠v"
  shows "forest (insert (Upair u v) F)"
  unfolding forest_def 
proof (rule ccontr, clarsimp simp: decycle_def )
  fix w p 
  assume d: "distinct p" and v: "epath (insert (Upair u v) F) w p w" and p: "2 < length p"

  have setep: "set p ⊆ insert (Upair u v) F" using epath_subset_E v
    by metis

  have uvF: "(Upair u v)∉F"
  proof(rule ccontr, clarsimp)
    assume "(Upair u v) ∈ F"
    then have "epath F u [(Upair u v)] v" using notsame by auto
    then have "(u,v) ∈ uconnected F" unfolding  uconnected_def by blast
    then show "False" using assms(4) by auto
  qed
  have k: "insert (Upair u v) F ∩ F = F" by auto

  show False
  proof (cases)
    assume "(Upair u v) ∈ set p"
    then obtain as bs where ep: "p = as @ (Upair u v) # bs" using in_set_conv_decomp
      by metis
    then have "epath (insert (Upair u v) F) w (as @ (Upair u v) # bs) w" using v by auto
    then obtain z where pr: "epath (insert (Upair u v) F) w as z"   "epath (insert (Upair u v) F) z ((Upair u v) # bs) w"   by auto  
    from d ep have uvas: "(Upair u v) ∉ set (as@bs)" by auto
    then have setasbs: "set (bs@as) ⊆ F" using ep setep by auto
    { assume "z=u"
      with pr have "epath (insert (Upair u v) F) w as u"   "epath (insert(Upair u v) F) v bs w" by auto
      then have "epath (insert (Upair u v) F) v (bs@as) u" by auto
      from epath_restrict[where I=F, OF setasbs this] have "epath F v (bs@as) u" using uvF by auto
      then have "(v,u) ∈ uconnected F" using uconnected_def
        by blast
      then have "(u,v) ∈ uconnected F" by (rule uconnected_symI)
    } moreover
    { assume "z≠u"
      then have "z=v" using pr(2) by auto
      with pr have "epath (insert (Upair u v) F) w as v"   "epath (insert (Upair u v) F) u bs w" by auto
      then have "epath (insert (Upair u v) F) u (bs@as) v" by auto
      from epath_restrict[where I=F, OF setasbs this] have "epath F u (bs@as) v" using uvF by auto
      then have "(u,v) ∈ uconnected F" using uconnected_def
        by fast  
    }
    ultimately have "(u,v) ∈ uconnected F" by auto 
    then show "False" using assms by auto 
  next
    assume "(Upair u v) ∉ set p" 
    with setep have "set p ⊆ F" by auto
    then have "epath (insert (Upair u v) F ∩ F) w p w" using epath_restrict[OF _ v, where I="F"] by auto
    then have "epath F w p w" using k by auto 
    with ‹forest F› show "False" unfolding forest_def decycle_def using p d
      by auto
  qed
qed


subsection "uGraph locale"

locale uGraph =
  fixes E :: "'a uprod set"   
    and w :: "'a uprod ==> 'c::{linorder, ordered_comm_monoid_add}"
  assumes ecard2: "∧e. e∈E ==> proper_uprod e" 
    and finiteE[simp]: "finite E"
begin

abbreviation "uconnected_on E' V ≡ uconnected E' ∩ (V×V)"

abbreviation "verts ≡ ∪(set_uprod ` E)"

lemma set_uprod_nonemptyY[simp]: "set_uprod x ≠ {}" apply(cases x) by auto
 

abbreviation "uconnectedV E' ≡ Restr (uconnected E') verts"


lemma equiv_unconnected_on: "equiv V (uconnected_on E' V)"
proof (rule equivI)
  show "Restr (uconnected E') V ⊆ V × V"
    by simp
next
  show "refl_on V (Restr (uconnected E') V)"
    by (auto simp: refl_on_def uconnected_def) 
next
  show "sym (Restr (uconnected E') V)"
    by (metis mem_Sigma_iff symI sym_Int uconnected_sym)
next
  show "trans (Restr (uconnected E') V)"
    by (simp add: trans_Restr uconnected_trans)
qed

lemma uconnectedV_refl: "E'⊆E ==> refl_on verts (uconnectedV E')"
  by(auto simp: refl_on_def uconnected_def) 

lemma uconnectedV_trans: "trans (uconnectedV E')"
  apply(clarsimp simp: trans_def uconnected_def) subgoal for x y z p a b c q apply (rule exI[where x="p@q"]) by auto done
lemma uconnectedV_sym: "sym (uconnectedV E')"
  apply(clarsimp simp: sym_def uconnected_def) subgoal for x y p apply (rule exI[where x="rev p"]) by (auto) done

lemma equiv_vert_uconnected: "equiv verts (uconnectedV E')"
  using equiv_unconnected_on by auto



lemma uconnectedV_tracl: "(uconnectedV F)^* = (uconnectedV F)⁼"
  apply(rule trans_rtrancl_eq_reflcl)
  by (fact uconnectedV_trans) 

lemma uconnectedV_cl: "(uconnectedV F)⁺ = (uconnectedV F)"
  apply(rule trancl_id)
  by (fact uconnectedV_trans) 

lemma uconnectedV_Restrcl: "Restr ((uconnectedV F)^*) verts = (uconnectedV F)"
  apply(simp only: uconnectedV_tracl)
  apply auto unfolding uconnected_def by auto

lemma restr_ucon: "F ⊆ E ==> uconnected F = uconnectedV F ∪ Id"
  unfolding uconnected_def apply auto  
proof (goal_cases)
  case (1 a b p)
  then have "p≠[]" by auto
  then obtain e es where "p=e#es"
    using list.exhaust by blast 
  with 1(2) have "a∈ set_uprod e" "e∈F" by auto    
  then show ?case using 1(1)
    by blast
next
  case (2 a b p)
  then have "rev p≠[]" "epath F b (rev p) a" by auto
  then obtain e es where "rev p=e#es"
    using list.exhaust by metis
  with 2(2) have "b∈ set_uprod e" "e∈F" by auto    
  then show ?case using 2(1)
    by blast
qed

lemma relI:
  assumes "∧a b. (a,b) ∈ F ==> (a,b) ∈ G"
    and "∧a b. (a,b) ∈ G ==> (a,b) ∈ F" shows "F=G"
  using assms by auto

lemma in_per_union: "u ∈ {x, y} ==> u' ∈ {x, y} ==> x∈V ==> y∈V ==>
    refl_on V R ==> part_equiv R ==> (u, u') ∈ per_union R x y"
  by (auto simp: per_union_def dest: refl_onD) 

lemma uconnectedV_mono: " (a,b)∈uconnectedV F ==> F⊆F' ==> (a,b)∈uconnectedV F'"
  unfolding uconnected_def by (auto intro: epath_mono)

lemma per_union_subs: "x ∈ S ==> y∈S ==> R⊆S × S ==> per_union R x y ⊆ S × S"
  unfolding per_union_def by auto

(* adapted preserve_corresponding_union_find_add by Julian Biendarra *)
lemma insert_uconnectedV_per: 
  assumes  "x≠y" and inV: "x∈verts" "y∈verts" and subE: "F⊆E"
  shows "uconnectedV (insert (Upair x y) F) = per_union (uconnectedV F) x y"
    (is "uconnectedV ?F' = per_union ?uf x y")
proof -
  have PER: "part_equiv (uconnectedV F)" unfolding part_equiv_def 
    using uconnectedV_sym uconnectedV_trans by auto
  from PER have PER': "part_equiv (per_union (uconnectedV F) x y)"
    by (auto simp: union_part_equivp)
  have ref: "refl_on verts (uconnectedV F)" using uconnectedV_refl assms(4) by auto

  show ?thesis
  proof (rule relI)
    fix a b
    assume "(a,b) ∈ uconnectedV ?F'"
    then obtain p where p: "epath ?F' a p b" and ab: "a∈verts" "b∈verts"
      unfolding uconnected_def 
      by blast
    show "(a,b)∈per_union (uconnectedV F) x y"
    proof (cases "Upair x y∈set p")
      case True
      obtain p' p'' u u' where
        "epath ?F' a p' u" "epath ?F' u' p'' b"and
        u: "u∈{x,y} ∧ u'∈{x,y}" and
        "Upair x y ∉ set p'" "Upair x y ∉ set p''"
        using epath_split_distinct[OF p True] by blast
      then have "epath F a p' u" "epath F u' p'' b" by(auto intro: epath_restrict')
      then have a: "(a,u)∈(uconnectedV F)" and b: "(u',b)∈(uconnectedV F)"
        unfolding uconnected_def using u ab assms by auto

      from a 
      have "(a,u)∈per_union ?uf x y" by (auto simp: per_union_def)
      also 
      have "(u,u')∈per_union ?uf x y" apply (rule in_per_union) using u inV ref PER by auto
      also (part_equiv_trans[OF PER'])
      have "(u',b)∈per_union ?uf x y" using b by (auto simp: per_union_def) 
      finally (part_equiv_trans[OF PER'])
      show "(a,b)∈per_union ?uf x y" .
    next
      case False
      with p have "epath F a p b" by(auto intro: epath_restrict')
      then have "(a,b)∈uconnectedV F" using ab by (auto simp: uconnected_def)
      then show ?thesis unfolding per_union_def by auto 
    qed
  next
    fix a b
    assume asm: "(a,b)∈per_union ?uf x y" 
    have "per_union ?uf x y ⊆ verts × verts" apply(rule per_union_subs)
      using inV by auto 
    with asm have ab: "a∈verts" "b∈verts" by auto
    have "Upair x y ∈ ?F'" by simp
    show "(a,b) ∈ uconnectedV ?F'"
    proof (cases "(a, b) ∈ ?uf")
      case True
      then show ?thesis using uconnectedV_mono by blast
    next
      case False
      with asm part_equiv_sym[OF PER]
      have "(a,x) ∈ ?uf ∧ (y,b) ∈ ?uf ∨ (a,y) ∈ ?uf ∧ (x,b) ∈ ?uf"
        by (auto simp: per_union_def)
      with assms(1) ‹x∈verts› ‹y∈verts› inV  obtain p q p' q'
        where "epath F a p x ∧ epath F y q b ∨ epath F a p' y ∧ epath F x q' b"
        unfolding uconnected_def
        by fastforce
      then have "epath ?F' a p x ∧ epath ?F' y q b ∨ epath ?F' a p' y ∧ epath ?F' x q' b"
        by (auto intro: epath_mono)
      then have 2: "epath ?F' a (p @ Upair x y # q) b ∨ epath ?F' a (p' @ Upair x y # q') b"
        using assms(1) by auto 
      then show ?thesis unfolding uconnected_def
        using ab by blast
    qed
  qed
qed


lemma epath_filter_selfloop: "epath (insert (Upair x x) F) a p b ==> ∃p. epath F a p b"
proof (induction n == "length p" arbitrary: p  rule: nat_less_induct)
  case 1
  from 1(1) have indhyp:
      "∧xa. length xa < length p ==> epath (insert (Upair x x) F) a xa b ==> (∃p. epath F a p b)" by auto
  
  from 1(2) have k: "set p ⊆ (insert (Upair x x) F)" using epath_subset_E by fast
  { assume a: "set p ⊆ F"
    have F: "(insert (Upair x x) F ∩ F) = F" by auto
    from epath_restrict[OF a 1(2)] F have "epath F a p b" by simp
    then have "(∃p. epath F a p b)" by auto
  } moreover
  { assume "¬ set p ⊆ F"
    with k have "Upair x x ∈ set p" by auto
    then obtain xs ys where p: "p = xs @ Upair x x # ys"  
      by (meson split_list_last) 
    then have "epath (insert (Upair x x) F) a xs x"  "epath (insert (Upair x x) F) x ys b" 
      using "1.prems" by auto  
    then have "epath (insert (Upair x x) F) a (xs@ys) b" by auto
    from indhyp[OF _ this] p have "(∃p. epath F a p b)" by simp
  }
  ultimately show ?thesis by auto
qed


lemma uconnectedV_insert_selfloop: "x∈verts ==> uconnectedV (insert (Upair x x) F) = uconnectedV F"
  apply(rule)
   apply auto 
  subgoal unfolding uconnected_def apply auto using epath_filter_selfloop by metis
  subgoal by (meson subsetCE subset_insertI uconnected_mono) 
  done

lemma equiv_selfloop_per_union_id: "equiv S F ==> x∈S ==> per_union F x x = F"
  apply rule
  subgoal unfolding per_union_def     
    using equiv_class_eq_iff by fastforce 
  subgoal unfolding per_union_def by auto
  done
  

lemma insert_uconnectedV_per_eq: 
  assumes    inV: "x∈verts"   and subE: "F⊆E"
  shows "uconnectedV (insert (Upair x x) F) = per_union (uconnectedV F) x x"
  using assms
  by(simp add: uconnectedV_insert_selfloop equiv_selfloop_per_union_id[OF equiv_vert_uconnected])

lemma insert_uconnectedV_per': 
  assumes  inV: "x∈verts" "y∈verts" and subE: "F⊆E"
  shows "uconnectedV (insert (Upair x y) F) = per_union (uconnectedV F) x y"
  apply(cases "x=y")
  subgoal using assms insert_uconnectedV_per_eq by simp 
  subgoal using assms insert_uconnectedV_per by simp
  done


definition "subforest F ≡ forest F ∧ F ⊆ E"

definition spanningForest where "spanningForest X ⟷ subforest X ∧ (∀x ∈ E - X. ¬ subforest (insert x X))"

definition "minSpanningForest F ≡ spanningForest F ∧ (∀F'. spanningForest F' ⟶ sum w F ≤ sum w F')"

end

end