Theory Undirected_Graph

section  ‹Undirected Graphs›
theory Undirected_Graph
imports
  Common
begin
subsection ‹Nodes and Edges›  

typedef 'v ugraph 
  = "{ (V::'v set , E). E ⊆ V×V ∧ finite V ∧ sym E ∧ irrefl E }"
  unfolding sym_def irrefl_def by blast

setup_lifting type_definition_ugraph

lift_definition nodes_internal :: "'v ugraph ⇒ 'v set" is fst .
lift_definition edges_internal :: "'v ugraph ⇒ ('v×'v) set" is snd .
lift_definition graph_internal :: "'v set ⇒ ('v×'v) set ⇒ 'v ugraph" 
  is "λV E. if finite V ∧ finite E then (V∪fst`E∪snd`E, (E∪E¯)-Id) else ({},{})"
  by (auto simp: sym_def irrefl_def; force)     

definition nodes :: "'v ugraph ⇒ 'v set" 
  where "nodes = nodes_internal" 
definition edges :: "'v ugraph ⇒ ('v×'v) set" 
  where "edges = edges_internal" 
definition graph :: "'v set ⇒ ('v×'v) set ⇒ 'v ugraph" 
  where "graph = graph_internal" 

lemma edges_subset: "edges g ⊆ nodes g × nodes g"
  unfolding edges_def nodes_def by transfer auto

lemma nodes_finite[simp, intro!]: "finite (nodes g)"
  unfolding edges_def nodes_def by transfer auto
  
lemma edges_sym: "sym (edges g)"    
  unfolding edges_def nodes_def by transfer auto

lemma edges_irrefl: "irrefl (edges g)"      
  unfolding edges_def nodes_def by transfer auto

lemma nodes_graph: "⟦finite V; finite E⟧ ⟹ nodes (graph V E) = V∪fst`E∪snd`E"    
  unfolding edges_def nodes_def graph_def by transfer auto
  
lemma edges_graph: "⟦finite V; finite E⟧ ⟹ edges (graph V E) = (E∪E¯)-Id"    
  unfolding edges_def nodes_def graph_def by transfer auto

lemmas graph_accs = nodes_graph edges_graph  
  
lemma nodes_edges_graph_presentation: "⟦finite V; finite E⟧ 
    ⟹ nodes (graph V E) = V ∪ fst`E ∪ snd`E ∧ edges (graph V E) = E∪E¯ - Id"
  by (simp add: graph_accs)
      
lemma graph_eq[simp]: "graph (nodes g) (edges g) = g"  
  unfolding edges_def nodes_def graph_def
  apply transfer
  unfolding sym_def irrefl_def
  apply (clarsimp split: prod.splits)
  by (fastforce simp: finite_subset)

lemma edges_finite[simp, intro!]: "finite (edges g)"
  using edges_subset finite_subset by fastforce
  
lemma graph_cases[cases type]: obtains V E 
  where "g = graph V E" "finite V" "finite E" "E⊆V×V" "sym E" "irrefl E"  
proof -
  show ?thesis
    apply (rule that[of "nodes g" "edges g"]) 
    using edges_subset edges_sym edges_irrefl[of g]
    by auto
qed     

lemma graph_eq_iff: "g=g' ⟷ nodes g = nodes g' ∧ edges g = edges g'"  
  unfolding edges_def nodes_def graph_def by transfer auto

  
  
lemma edges_sym': "(u,v)∈edges g ⟹ (v,u)∈edges g" using edges_sym 
  by (blast intro: symD)
  
lemma edges_irrefl'[simp,intro!]: "(u,u)∉edges g"
  by (meson edges_irrefl irrefl_def)
  
lemma edges_irreflI[simp, intro]: "(u,v)∈edges g ⟹ u≠v" by auto 
  
lemma edgesT_diff_sng_inv_eq[simp]: 
  "(edges T - {(x, y), (y, x)})¯ = edges T - {(x, y), (y, x)}"
  using edges_sym' by fast
  
lemma nodesI[simp,intro]: assumes "(u,v)∈edges g" shows "u∈nodes g" "v∈nodes g"
  using assms edges_subset by auto
  
lemma split_edges_sym: "∃E. E∩E¯ = {} ∧ edges g = E ∪ E¯"  
  using split_sym_rel[OF edges_sym edges_irrefl, of g] by metis

  
subsection ‹Connectedness Relation›  
  
lemma rtrancl_edges_sym': "(u,v)∈(edges g)* ⟹ (v,u)∈(edges g)*"  
  by (simp add: edges_sym symD sym_rtrancl)
  
lemma trancl_edges_subset: "(edges g)+ ⊆ nodes g × nodes g"  
  by (simp add: edges_subset trancl_subset_Sigma)
      
lemma find_crossing_edge:
  assumes "(u,v)∈E*" "u∈V" "v∉V"
  obtains u' v' where "(u',v')∈E∩V×-V"
  using assms apply (induction rule: converse_rtrancl_induct)
  by auto


  

subsection ‹Constructing Graphs›
  
definition "graph_empty ≡ graph {} {}"
definition "ins_node v g ≡ graph (insert v (nodes g)) (edges g)"
definition "ins_edge e g ≡ graph (nodes g) (insert e (edges g))"
definition "graph_join g1 g2 ≡ graph (nodes g1 ∪ nodes g2) (edges g1 ∪ edges g2)"
definition "restrict_nodes g V ≡ graph (nodes g ∩ V) (edges g ∩ V×V)"
definition "restrict_edges g E ≡ graph (nodes g) (edges g ∩ (E∪E¯))"


definition "nodes_edges_consistent V E ≡ finite V ∧ irrefl E ∧ sym E ∧ E ⊆ V×V"

lemma [simp]:
  assumes "nodes_edges_consistent V E"
  shows nodes_graph': "nodes (graph V E) = V" (is ?G1)
    and edges_graph': "edges (graph V E) = E" (is ?G2)
proof -
  from assms have [simp]: "finite E" unfolding nodes_edges_consistent_def
    by (meson finite_SigmaI rev_finite_subset) 

  show ?G1 ?G2 using assms
    by (auto simp: nodes_edges_consistent_def nodes_graph edges_graph irrefl_def)
    
qed    

lemma nec_empty[simp]: "nodes_edges_consistent {} {}" 
  by (auto simp: nodes_edges_consistent_def irrefl_def sym_def)

lemma graph_empty_accs[simp]:
  "nodes graph_empty = {}"
  "edges graph_empty = {}"
  unfolding graph_empty_def by (auto)  
  
lemma graph_empty[simp]: "graph {} {} = graph_empty"  
  by (simp add: graph_empty_def)
    
lemma nodes_empty_iff_empty[simp]: 
  "nodes G = {} ⟷ G=graph {} {}"
  "{} = nodes G ⟷ G=graph_empty"
  using edges_subset
  by (auto simp: graph_eq_iff)
  
lemma nodes_ins_nodes[simp]: "nodes (ins_node v g) = insert v (nodes g)"         
  and edges_ins_nodes[simp]: "edges (ins_node v g) = edges g"
  unfolding ins_node_def by (auto simp: graph_accs edges_sym')
  
  
lemma nodes_ins_edge[simp]: "nodes (ins_edge e g) = {fst e, snd e} ∪ nodes g"
  and edges_ins_edge: 
    "edges (ins_edge e g) 
      = (if fst e = snd e then edges g else {e,prod.swap e}∪(edges g))"
  unfolding ins_edge_def
  apply (all ‹cases e›)
  by (auto simp: graph_accs dest: edges_sym')
  
lemma edges_ins_edge'[simp]: 
  "u≠v ⟹ edges (ins_edge (u,v) g) = {(u,v),(v,u)} ∪ edges g"
  by (auto simp: edges_ins_edge)

lemma edges_ins_edge_ss: "edges g ⊆ edges (ins_edge e g)"  
  by (auto simp: edges_ins_edge)
  
  
lemma nodes_join[simp]: "nodes (graph_join g1 g2) = nodes g1 ∪ nodes g2"  
  and edges_join[simp]: "edges (graph_join g1 g2) = edges g1 ∪ edges g2"
  unfolding graph_join_def
  by (auto simp: graph_accs dest: edges_sym')

lemma nodes_restrict_nodes[simp]: "nodes (restrict_nodes g V) = nodes g ∩ V"  
  and edges_restrict_nodes[simp]: "edges (restrict_nodes g V) = edges g ∩ V×V"
  unfolding restrict_nodes_def
  by (auto simp: graph_accs dest: edges_sym')
  
lemma nodes_restrict_edges[simp]: "nodes (restrict_edges g E) = nodes g"
  and edges_restrict_edges[simp]: "edges (restrict_edges g E) = edges g ∩ (E∪E¯)"
  unfolding restrict_edges_def
  by (auto simp: graph_accs dest: edges_sym')

lemma unrestricte_edges: "edges (restrict_edges g E) ⊆ edges g" by auto
lemma unrestrictn_edges: "edges (restrict_nodes g V) ⊆ edges g" by auto

lemma unrestrict_nodes: "nodes (restrict_edges g E) ⊆ nodes g" by auto



subsection ‹Paths›  
    
fun path where
  "path g u [] v ⟷ u=v"  
| "path g u (e#ps) w ⟷ (∃v. e=(u,v) ∧ e∈edges g ∧ path g v ps w)"  

lemma path_emptyI[intro!]: "path g u [] u" by auto
    
lemma path_append[simp]: 
  "path g u (p1@p2) w ⟷ (∃v. path g u p1 v ∧ path g v p2 w)" 
  by (induction p1 arbitrary: u) auto

lemma path_transs1[trans]:
  "path g u p v ⟹ (v,w)∈edges g ⟹ path g u (p@[(v,w)]) w"  
  "(u,v)∈edges g ⟹ path g v p w ⟹ path g u ((u,v)#p) w"
  "path g u p1 v ⟹ path g v p2 w ⟹ path g u (p1@p2) w"
  by auto
  
lemma path_graph_empty[simp]: "path graph_empty u p v ⟷ v=u ∧ p=[]" 
  by (cases p) auto

abbreviation "revp p ≡ rev (map prod.swap p)"
lemma revp_alt: "revp p = rev (map (λ(u,v). (v,u)) p)" by auto
  
lemma path_rev[simp]: "path g u (revp p) v ⟷ path g v p u"  
  by (induction p arbitrary: v) (auto dest: edges_sym')

lemma path_rev_sym[sym]: "path g v p u ⟹ path g u (revp p) v" by simp 

lemma path_transs2[trans]: 
  "path g u p v ⟹ (w,v)∈edges g ⟹ path g u (p@[(v,w)]) w"  
  "(v,u)∈edges g ⟹ path g v p w ⟹ path g u ((u,v)#p) w"
  "path g u p1 v ⟹ path g w p2 v ⟹ path g u (p1@revp p2) w"
  by (auto dest: edges_sym')

  
lemma path_edges: "path g u p v ⟹ set p ⊆ edges g"
  by (induction p arbitrary: u) auto

lemma path_graph_cong: 
  "⟦path g1 u p v; set p ⊆ edges g1 ⟹ set p ⊆ edges g2⟧ ⟹ path g2 u p v"
  apply (frule path_edges; simp)
  apply (induction p arbitrary: u) 
  by auto    
  
                
lemma path_endpoints: 
  assumes "path g u p v" "p≠[]" shows "u∈nodes g" "v∈nodes g"
  subgoal using assms by (cases p) (auto intro: nodesI)
  subgoal using assms by (cases p rule: rev_cases) (auto intro: nodesI)
  done

lemma path_mono: "edges g ⊆ edges g' ⟹ path g u p v ⟹ path g' u p v"  
  by (meson path_edges path_graph_cong subset_trans)

  
  
lemmas unrestricte_path = path_mono[OF unrestricte_edges]
lemmas unrestrictn_path = path_mono[OF unrestrictn_edges]

lemma unrestrict_path_edges: "path (restrict_edges g E) u p v ⟹ path g u p v"  
  by (induction p arbitrary: u) auto
  
lemma unrestrict_path_nodes: "path (restrict_nodes g E) u p v ⟹ path g u p v"  
  by (induction p arbitrary: u) auto
  
      
  
subsubsection ‹Paths and Connectedness›  
  
lemma rtrancl_edges_iff_path: "(u,v)∈(edges g)* ⟷ (∃p. path g u p v)"
  apply rule
  subgoal
    apply (induction rule: converse_rtrancl_induct)
    by (auto dest: path_transs1)
  apply clarify  
  subgoal for p by (induction p arbitrary: u; force)
  done  
  
lemma rtrancl_edges_pathE: 
  assumes "(u,v)∈(edges g)*" obtains p where "path g u p v"
  using assms by (auto simp: rtrancl_edges_iff_path)

lemma path_rtrancl_edgesD: "path g u p v ⟹ (u,v)∈(edges g)*"
  by (auto simp: rtrancl_edges_iff_path)  
      
  
subsubsection ‹Simple Paths›  
  
definition "uedge ≡ λ(a,b). {a,b}"   
  
definition "simple p ≡ distinct (map uedge p)"  


lemma in_uedge_conv[simp]: "x∈uedge (u,v) ⟷ x=u ∨ x=v"
  by (auto simp: uedge_def)

lemma uedge_eq_iff: "uedge (a,b) = uedge (c,d) ⟷ a=c ∧ b=d ∨ a=d ∧ b=c"
  by (auto simp: uedge_def doubleton_eq_iff)
  
lemma uedge_degen[simp]: "uedge (a,a) = {a}"  
  by (auto simp: uedge_def)

lemma uedge_in_set_eq: "uedge (u, v) ∈ uedge ` S ⟷ (u,v)∈S ∨ (v,u)∈S"  
  by (auto simp: uedge_def doubleton_eq_iff)
  
lemma uedge_commute: "uedge (a,b) = uedge (b,a)" by auto 
      
lemma simple_empty[simp]: "simple []"
  by (auto simp: simple_def)

lemma simple_cons[simp]: "simple (e#p) ⟷ uedge e ∉ uedge ` set p ∧ simple p"
  by (auto simp: simple_def)

lemma simple_append[simp]: "simple (p1@p2) 
  ⟷ simple p1 ∧ simple p2 ∧ uedge ` set p1 ∩ uedge ` set p2 = {}"
  by (auto simp: simple_def)

  
lemma simplify_pathD:
  "path g u p v ⟹ ∃p'. path g u p' v ∧ simple p' ∧ set p' ⊆ set p"
proof (induction p arbitrary: u v rule: length_induct)
  case A: (1 p)
  then show ?case proof (cases "simple p")
    assume "simple p" with A.prems show ?case by blast
  next
    assume "¬simple p"  
    then consider p1 a b p2 p3 where "p=p1@[(a,b)]@p2@[(a,b)]@p3"
                | p1 a b p2 p3 where "p=p1@[(a,b)]@p2@[(b,a)]@p3"
      by (auto 
        simp: simple_def map_eq_append_conv uedge_eq_iff 
        dest!: not_distinct_decomp)
    then obtain p' where "path g u p' v" "length p' < length p" "set p' ⊆ set p"
    proof cases
      case [simp]: 1
      from A.prems have "path g u (p1@[(a,b)]@p3) v" by auto
      from that[OF this] show ?thesis by auto
    next
      case [simp]: 2
      from A.prems have "path g u (p1@p3) v" by auto
      from that[OF this] show ?thesis by auto
    qed
    with A.IH show ?thesis by blast
  qed
qed  
    
lemma simplify_pathE: 
  assumes "path g u p v" 
  obtains p' where "path g u p' v" "simple p'" "set p' ⊆ set p"
  using assms by (auto dest: simplify_pathD)
   

subsubsection ‹Splitting Paths›  

lemma find_crossing_edge_on_path:
  assumes "path g u p v" "¬P u" "P v"
  obtains u' v' where "(u',v')∈set p" "¬P u'" "P v'"
  using assms by (induction p arbitrary: u) auto
  
lemma find_crossing_edges_on_path:  
  assumes P: "path g u p v" and "P u" "P v"
  obtains "∀(u,v)∈set p. P u ∧ P v"
        | u1 v1 v2 u2 p1 p2 p3 
          where "p=p1@[(u1,v1)]@p2@[(u2,v2)]@p3" "P u1" "¬P v1" "¬P u2" "P v2"
proof (cases "∀(u,v)∈set p. P u ∧ P v")
  case True with that show ?thesis by blast
next
  case False
  with P ‹P u› have "∃(u1,v1)∈set p. P u1 ∧ ¬P v1"
    apply clarsimp apply (induction p arbitrary: u) by auto
  then obtain u1 v1 where "(u1,v1)∈set p" and PRED1: "P u1" "¬P v1" by blast
  then obtain p1 p23 where [simp]: "p=p1@[(u1,v1)]@p23" 
    by (auto simp: in_set_conv_decomp)
  with P have "path g v1 p23 v" by auto
  from find_crossing_edge_on_path[where P=P, OF this ‹¬P v1› ‹P v›] obtain u2 v2 
    where "(u2,v2)∈set p23" "¬P u2" "P v2" .
  then show thesis using PRED1
    by (auto simp: in_set_conv_decomp intro: that)
qed      
  
lemma find_crossing_edge_rtrancl:
  assumes "(u,v)∈(edges g)*" "¬P u" "P v"
  obtains u' v' where "(u',v')∈edges g" "¬P u'" "P v'"
  using assms
  by (metis converse_rtrancl_induct)
  

lemma path_change: 
  assumes "u∈S" "v∉S" "path g u p v" "simple p"
  obtains x y p1 p2 where 
    "(x,y) ∈ set p" "x ∈ S" "y ∉ S"
    "path (restrict_edges g (-{(x,y),(y,x)})) u p1 x" 
    "path (restrict_edges g (-{(x,y),(y,x)})) y p2 v"
proof -
  from find_crossing_edge_on_path[where P="λx. x∉S"] assms obtain x y where 
    1: "(x,y)∈set p" "x∈S" "y∉S" by blast
  then obtain p1 p2 where [simp]: "p=p1@[(x,y)]@p2" 
    by (auto simp: in_set_conv_decomp)
  
  let ?g' = "restrict_edges g (-{(x,y),(y,x)})"
  
  from ‹path g u p v› have P1: "path g u p1 x" and P2: "path g y p2 v" by auto
  from ‹simple p› 
    have "uedge (x,y)∉set (map uedge p1)" "uedge (x,y)∉set (map uedge p2)" 
  by auto
  then have "path ?g' u p1 x" "path ?g' y p2 v"  
    using path_graph_cong[OF P1, of ?g'] path_graph_cong[OF P2, of ?g']
    by (auto simp: uedge_in_set_eq)
  with 1 show ?thesis by (blast intro: that)
qed
      




subsection ‹Cycles›      
  
definition "cycle_free g ≡ ∄p u. p≠[] ∧ simple p ∧ path g u p u"

lemma cycle_free_alt_in_nodes: 
  "cycle_free g ≡ ∄p u. p≠[] ∧ u∈nodes g ∧ simple p ∧ path g u p u"
  by (smt cycle_free_def path_endpoints(2))

lemma cycle_freeI:
  assumes "⋀p u. ⟦ path g u p u; p≠[]; simple p ⟧ ⟹ False"
  shows "cycle_free g"
  using assms unfolding cycle_free_def by auto

lemma cycle_freeD:
  assumes "cycle_free g" "path g u p u" "p≠[]" "simple p" 
  shows False
  using assms unfolding cycle_free_def by auto

  
lemma cycle_free_antimono: "edges g ⊆ edges g' ⟹ cycle_free g' ⟹ cycle_free g"
  unfolding cycle_free_def
  by (auto dest: path_mono)

lemma cycle_free_empty[simp]: "cycle_free graph_empty" 
  unfolding cycle_free_def by auto
  
lemma cycle_free_no_edges: "edges g = {} ⟹ cycle_free g"
  by (rule cycle_freeI) (auto simp: neq_Nil_conv)
  
lemma simple_path_cycle_free_unique:
  assumes CF: "cycle_free g" 
  assumes P: "path g u p v" "path g u p' v" "simple p" "simple p'"
  shows "p=p'"
  using P 
proof (induction p arbitrary: u p')
  case Nil
  then show ?case using cycle_freeD[OF CF] by auto
next
  case (Cons e p)
  
  note CF = cycle_freeD[OF CF]
  
  from Cons.prems obtain u' where 
    [simp]: "e=(u,u')" 
    and P': "(u,u')∉set p" "(u',u)∉set p" "(u,u')∈edges g"
    by (auto simp: uedge_in_set_eq)
  with Cons.prems obtain sp1 where 
    SP1: "path g u ((u,u')#sp1) v" "simple ((u,u')#sp1)" 
    by blast
  
  from Cons.prems obtain u'' p'' where 
    [simp]: "p' = (u,u'')#p''" 
    and P'': "(u,u'')∉set p''" "(u'',u)∉set p''" "(u,u'')∈edges g"
    apply (cases p')
    subgoal by auto (metis Cons.prems(1) Cons.prems(3) CF list.distinct(1))
    by (auto simp: uedge_in_set_eq)
  with Cons.prems obtain sp2 where 
    SP2: "path g u ((u,u'')#sp2) v" "simple ((u,u'')#sp2)" 
    by blast  
    
  have "u''=u'" proof (rule ccontr)
    assume [simp, symmetric, simp]: "u''≠u'"
    
    have AUX1: "(u,x)∉set sp1" for x 
    proof 
      assume "(u, x) ∈ set sp1" 
      with SP1 obtain sp' where "path g u ((u,u')#sp') u" and "simple ((u,u')#sp')"
        by (clarsimp simp: in_set_conv_decomp; blast)
      with CF show False by blast
    qed  
    
    have AUX2:"(x,u)∉set sp1" for x 
    proof 
      assume "(x, u) ∈ set sp1" 
      
      with SP1 obtain sp' where "path g u ((u,u')#sp') u" and "simple ((u,u')#sp')"
        apply (clarsimp simp: in_set_conv_decomp)
        (* TODO: Do more explicit, like other AUXes*)
        by (metis Cons.prems(1) Cons.prems(3) Un_iff 
        AUX1 ‹e = (u, u')› insert_iff list.simps(15) 
        path.elims(2) path.simps(2) prod.sel(2) set_append simple_cons)
      with CF show False by blast
    qed  
    
    have AUX3:"(u,x)∉set sp2" for x 
    proof 
      assume "(u, x) ∈ set sp2" 
      then obtain sp' sp'' where [simp]: "sp2 = sp'@[(u,x)]@sp''"
        by (auto simp: in_set_conv_decomp)
      from SP2 have "path g u ((u,u'')#sp') u" "simple ((u,u'')#sp')" by auto
      with CF show False by blast
    qed    
    
    have AUX4:"(x,u)∉set sp2" for x 
    proof 
      assume "(x, u) ∈ set sp2" 
      then obtain sp' sp'' where [simp]: "sp2 = sp'@[(x,u)]@sp''"
        by (auto simp: in_set_conv_decomp)
      from SP2 
        have "path g u ((u,u'')#sp'@[(x,u)]) u" "simple ((u,u'')#sp'@[(x,u)])" 
        by auto
      with CF show False by blast
    qed    
    
    have [simp]: "set (revp p) = (set p)¯" by auto
    
    from SP1 SP2 have "path g u' (sp1@revp sp2) u''" by auto
    then obtain sp where 
      SP: "path g u' sp u''" "simple sp" "set sp ⊆ set sp1 ∪ set (revp sp2)"
      by (erule_tac simplify_pathE) auto
    with ‹(u,u')∈edges g› ‹(u,u'')∈edges g› 
      have "path g u ((u,u')#sp@[(u'',u)]) u"
      by (auto dest: edges_sym' simp: uedge_eq_iff)
    moreover
    from SP SP1 SP2 AUX1 AUX2 AUX3 AUX4 have "simple (((u,u')#sp@[(u'',u)]))"
      by (auto 0 3 simp: uedge_eq_iff)
    ultimately show False using CF by blast  
  qed    

  with Cons.IH[of u' p''] Cons.prems show ?case by simp 
qed    
  
              
  
subsubsection ‹Characterization by Removing Edge›      



lemma cycle_free_alt: "cycle_free g 
  ⟷ (∀e∈edges g. e∉(edges (restrict_edges g (-{e,prod.swap e})))*)"
  apply (rule)
  apply (clarsimp simp del: edges_restrict_edges)
  subgoal premises prems for u v proof -
    note edges_restrict_edges[simp del]
    let ?rg = "(restrict_edges g (- {(u,v), (v,u)}))"
    from ‹(u, v) ∈ (edges ?rg)*›
    obtain p where P: "path ?rg u p v" and "simple p" 
      by (auto simp: rtrancl_edges_iff_path elim: simplify_pathE)
    from P have "path g u p v" by (rule unrestricte_path) 
    also note ‹(u, v) ∈ edges g› finally have "path g u (p @ [(v, u)]) u" .
    moreover from path_edges[OF P] have "uedge (u,v) ∉ set (map uedge p)" 
      by (auto simp: uedge_eq_iff edges_restrict_edges)
    with ‹simple p› have "simple (p @ [(v, u)])"
      by (auto simp: uedge_eq_iff uedge_in_set_eq)
    ultimately show ?thesis using ‹cycle_free g›  
      unfolding cycle_free_def by blast
  qed
  apply (clarsimp simp: cycle_free_def)
  subgoal premises prems for p u proof -
    from ‹p≠[]› ‹path g u p u› obtain v p' where 
      [simp]: "p=(u,v)#p'" and "(u,v)∈edges g" "path g v p' u" 
      by (cases p) auto
    from ‹simple p› have "simple p'" "uedge (u,v) ∉ set (map uedge p')" by auto  
    hence "(u,v)∉set p'" "(v,u)∉set p'" by (auto simp: uedge_in_set_eq)
    with ‹path g v p' u› 
      have "path (restrict_edges g (-{(u,v),(v,u)})) v p' u" (is "path ?rg _ _ _")
      by (erule_tac path_graph_cong) auto
      
    hence "(u,v)∈(edges ?rg)*"
      by (meson path_rev rtrancl_edges_iff_path)  
    with prems(1) ‹(u,v)∈edges g› show False by auto
  qed    
  done
  
lemma cycle_free_altI:
  assumes "⋀u v. ⟦ (u,v)∈edges g; (u,v)∈(edges g - {(u,v),(v,u)})* ⟧ ⟹ False"
  shows "cycle_free g"
  unfolding cycle_free_alt using assms by (force)
  
lemma cycle_free_altD:  
  assumes "cycle_free g"
  assumes "(u,v)∈edges g" 
  shows "(u,v)∉(edges g - {(u,v),(v,u)})*"
  using assms unfolding cycle_free_alt by (auto)
  


lemma remove_redundant_edge:
  assumes "(u, v) ∈ (edges g - {(u, v), (v, u)})*"  
  shows "(edges g - {(u, v), (v, u)})* = (edges g)*" (is "?E'* = _")
proof  
  show "?E'* ⊆ (edges g)*"
    by (simp add: Diff_subset rtrancl_mono)
next
  show "(edges g)* ⊆ ?E'*"
  proof clarify
    fix a b assume "(a,b)∈(edges g)*" then 
    show "(a,b)∈?E'*"
    proof induction
      case base
      then show ?case by simp
    next
      case (step b c)
      then show ?case 
      proof (cases "(b,c)∈{(u,v),(v,u)}")
        case True

        have SYME: "sym (?E'*)"
          apply (rule sym_rtrancl)
          using edges_sym[of g] 
          by (auto simp: sym_def)
        with step.IH assms have 
          IH': "(b,a) ∈ ?E'*"
          by (auto intro: symD)
        
        from True show ?thesis apply safe
          subgoal using assms step.IH by simp
          subgoal using assms IH' apply (rule_tac symD[OF SYME]) by simp
          done
        
      next
        case False
        then show ?thesis
          by (meson DiffI rtrancl.rtrancl_into_rtrancl step.IH step.hyps(2))
      qed 
        
    qed
  qed
qed
  
  
  
  
  
subsection ‹Connected Graphs›  
  
  
definition connected 
  where "connected g ≡ nodes g × nodes g ⊆ (edges g)*"  

lemma connectedI[intro?]: 
  assumes "⋀u v. ⟦u∈nodes g; v∈nodes g⟧ ⟹ (u,v)∈(edges g)*"  
  shows "connected g"
  using assms unfolding connected_def by auto
  
lemma connectedD[intro?]: 
  assumes "connected g" "u∈nodes g" "v∈nodes g"
  shows "(u,v)∈(edges g)*"  
  using assms unfolding connected_def by auto
  
lemma connected_empty[simp]: "connected graph_empty" 
  unfolding connected_def by auto

subsection ‹Component Containing Node›
definition "reachable_nodes g r ≡ (edges g)*``{r}"
definition "component_of g r 
  ≡ ins_node r (restrict_nodes g (reachable_nodes g r))"

lemma reachable_nodes_refl[simp, intro!]: "r ∈ reachable_nodes g r" 
  by (auto simp: reachable_nodes_def)
  
lemma reachable_nodes_step: 
  "edges g `` reachable_nodes g r ⊆ reachable_nodes g r"
  by (auto simp: reachable_nodes_def)

lemma reachable_nodes_steps: 
  "(edges g)* `` reachable_nodes g r ⊆ reachable_nodes g r"
  by (auto simp: reachable_nodes_def)

lemma reachable_nodes_step':
  assumes "u ∈ reachable_nodes g r" "(u, v) ∈ edges g" 
  shows "v∈reachable_nodes g r" "(u, v) ∈ edges (component_of g r)" 
proof -
  show "v ∈ reachable_nodes g r"
    by (meson ImageI assms(1) assms(2) reachable_nodes_step rev_subsetD)
  then show "(u, v) ∈ edges (component_of g r)"
    by (simp add: assms(1) assms(2) component_of_def)
qed
  
lemma reachable_nodes_steps':
  assumes "u ∈ reachable_nodes g r" "(u, v) ∈ (edges g)*" 
  shows "v∈reachable_nodes g r" "(u, v) ∈ (edges (component_of g r))*" 
proof -
  show "v∈reachable_nodes g r" using reachable_nodes_steps assms by fast
  show "(u, v) ∈ (edges (component_of g r))*"
    using assms(2,1)
    apply (induction rule: converse_rtrancl_induct)
    subgoal by auto
    subgoal by (smt converse_rtrancl_into_rtrancl reachable_nodes_step')
    done
qed
   
lemma reachable_not_node: "r∉nodes g ⟹ reachable_nodes g r = {r}"
  by (force elim: converse_rtranclE simp: reachable_nodes_def intro: nodesI)
   
  
lemma nodes_of_component[simp]: "nodes (component_of g r) = reachable_nodes g r"
  apply (rule equalityI)
  unfolding component_of_def reachable_nodes_def
  subgoal by auto
  subgoal by clarsimp (metis nodesI(2) rtranclE)
  done

lemma component_connected[simp, intro!]: "connected (component_of g r)"
proof (rule connectedI; simp)
  fix u v
  assume A: "u ∈ reachable_nodes g r" "v ∈ reachable_nodes g r"
  hence "(u,r)∈(edges g)*" "(r,v)∈(edges g)*" 
    by (auto simp: reachable_nodes_def dest: rtrancl_edges_sym')
  hence "(u,v)∈(edges g)*" by (rule rtrancl_trans)
  with A show "(u, v) ∈ (edges (component_of g r))*" 
    by (rule_tac reachable_nodes_steps'(2))
qed  

lemma component_edges_subset: "edges (component_of g r) ⊆ edges g"  
  by (auto simp: component_of_def)

lemma component_path: "u∈nodes (component_of g r) ⟹ 
  path (component_of g r) u p v ⟷ path g u p v"  
  apply rule
  subgoal by (erule path_mono[OF component_edges_subset])     
  subgoal by (induction p arbitrary: u) (auto simp: reachable_nodes_step')
  done  
  
lemma component_cycle_free: "cycle_free g ⟹ cycle_free (component_of g r)"  
  by (meson component_edges_subset cycle_free_antimono)
  
lemma component_of_connected_graph: 
  "⟦connected g; r∈nodes g⟧ ⟹ component_of g r = g"  
  unfolding graph_eq_iff 
  apply safe
  subgoal by simp (metis Image_singleton_iff nodesI(2) reachable_nodes_def rtranclE)
  subgoal by (simp add: connectedD reachable_nodes_def)
  subgoal by (simp add: component_of_def)
  subgoal by (simp add: connectedD reachable_nodes_def reachable_nodes_step'(2))
  done

lemma component_of_not_node: "r∉nodes g ⟹ component_of g r = graph {r} {}"
  by (clarsimp simp: graph_eq_iff component_of_def reachable_not_node graph_accs)

      
subsection ‹Trees›

definition "tree g ≡ connected g ∧ cycle_free g "    

lemma tree_empty[simp]: "tree graph_empty" by (simp add: tree_def)

lemma component_of_tree: "tree T ⟹ tree (component_of T r)"
  unfolding tree_def using component_connected component_cycle_free by auto


subsubsection ‹Joining and Splitting Trees on Single Edge›
      
lemma join_connected:
  assumes CONN: "connected g1" "connected g2"
  assumes IN_NODES: "u∈nodes g1" "v∈nodes g2"
  shows "connected (ins_edge (u,v) (graph_join g1 g2))" (is "connected ?g'") 
  unfolding connected_def
proof clarify
  fix a b
  assume A: "a∈nodes ?g'" "b∈nodes ?g'"
  
  have ESS: "(edges g1)* ⊆ (edges ?g')*" "(edges g2)* ⊆ (edges ?g')*"
    using edges_ins_edge_ss
    by (force intro!: rtrancl_mono)+
  
  have UV: "(u,v)∈(edges ?g')*"
    by (simp add: edges_ins_edge r_into_rtrancl)
    
  show "(a,b)∈(edges ?g')*"
  proof -
    {
      assume "a∈nodes g1" "b∈nodes g1"
      hence ?thesis using ‹connected g1› ESS(1) unfolding connected_def by blast
    } moreover {
      assume "a∈nodes g2" "b∈nodes g2"
      hence ?thesis using ‹connected g2› ESS(2) unfolding connected_def by blast
    } moreover {
      assume "a∈nodes g1" "b∈nodes g2"
      with connectedD[OF CONN(1)] connectedD[OF CONN(2)] ESS
      have ?thesis by (meson UV IN_NODES contra_subsetD rtrancl_trans)
    } moreover {
      assume "a∈nodes g2" "b∈nodes g1"
      with connectedD[OF CONN(1)] connectedD[OF CONN(2)] ESS
      have ?thesis
        by (meson UV IN_NODES contra_subsetD rtrancl_edges_sym' rtrancl_trans)
    }
    ultimately show ?thesis using A IN_NODES by auto
  qed    
qed
  
  
lemma join_cycle_free:  
  assumes CYCF: "cycle_free g1" "cycle_free g2"
  assumes DJ: "nodes g1 ∩ nodes g2 = {}"
  assumes IN_NODES: "u∈nodes g1" "v∈nodes g2"
  shows "cycle_free (ins_edge (u,v) (graph_join g1 g2))" (is "cycle_free ?g'") 
proof (rule cycle_freeI)
  fix p a
  assume P: "path ?g' a p a" "p≠[]" "simple p"
  from path_endpoints[OF this(1,2)] IN_NODES 
    have A_NODE: "a∈nodes g1 ∪ nodes g2" 
    by auto
  thus False proof 
    assume N1: "a∈nodes g1"
    have "set p ⊆ nodes g1 × nodes g1"
    proof (cases 
      rule: find_crossing_edges_on_path[where P="λx. x∈nodes g1", OF P(1) N1 N1])
      case 1
      then show ?thesis by auto
    next
      case (2 u1 v1 v2 u2 p1 p2 p3)
      then show ?thesis using ‹simple p› P
        apply clarsimp
        apply (drule path_edges)+
        apply (cases "u=v"; clarsimp simp: edges_ins_edge uedge_in_set_eq)
        apply (metis DJ IntI IN_NODES empty_iff)
        by (metis DJ IntI empty_iff nodesI uedge_eq_iff)
        
    qed
    hence "set p ⊆ edges g1" using DJ edges_subset path_edges[OF P(1)] IN_NODES
      by (auto simp: edges_ins_edge split: if_splits; blast)
    hence "path g1 a p a" by (meson P(1) path_graph_cong)
    thus False using cycle_freeD[OF CYCF(1)] P(2,3) by blast
  next
    assume N2: "a∈nodes g2"
    have "set p ⊆ nodes g2 × nodes g2"
    proof (cases 
      rule: find_crossing_edges_on_path[where P="λx. x∈nodes g2", OF P(1) N2 N2])
      case 1
      then show ?thesis by auto
    next
      case (2 u1 v1 v2 u2 p1 p2 p3)
      then show ?thesis using ‹simple p› P
        apply clarsimp
        apply (drule path_edges)+
        apply (cases "u=v"; clarsimp simp: edges_ins_edge uedge_in_set_eq)
        apply (metis DJ IntI IN_NODES empty_iff)
        by (metis DJ IntI empty_iff nodesI uedge_eq_iff)
        
    qed
    hence "set p ⊆ edges g2" using DJ edges_subset path_edges[OF P(1)] IN_NODES
      by (auto simp: edges_ins_edge split: if_splits; blast)
    hence "path g2 a p a" by (meson P(1) path_graph_cong)
    thus False using cycle_freeD[OF CYCF(2)] P(2,3) by blast
  qed
qed
      
lemma join_trees:     
  assumes TREE: "tree g1" "tree g2"
  assumes DJ: "nodes g1 ∩ nodes g2 = {}"
  assumes IN_NODES: "u∈nodes g1" "v∈nodes g2"
  shows "tree (ins_edge (u,v) (graph_join g1 g2))"
  using assms join_cycle_free join_connected unfolding tree_def by metis 
  
  
lemma split_tree:
  assumes "tree T" "(x,y)∈edges T"
  defines "E' ≡ (edges T - {(x,y),(y,x)})"
  obtains T1 T2 where 
    "tree T1" "tree T2" 
    "nodes T1 ∩ nodes T2 = {}" "nodes T = nodes T1 ∪ nodes T2"
    "edges T1 ∪ edges T2 = E'"
    "nodes T1 = { u. (x,u)∈E'*}" "nodes T2 = { u. (y,u)∈E'*}"
    "x∈nodes T1" "y∈nodes T2"
proof -
  (* TODO: Use component_of here! *)
  define N1 where "N1 = { u. (x,u)∈E'* }"
  define N2 where "N2 = { u. (y,u)∈E'* }"

  define T1 where "T1 = restrict_nodes T N1"
  define T2 where "T2 = restrict_nodes T N2"
  
  have SYME: "sym (E'*)"
    apply (rule sym_rtrancl) 
    using edges_sym[of T] by (auto simp: sym_def E'_def)
  

  from assms have "connected T" "cycle_free T" unfolding tree_def by auto
  from ‹cycle_free T› have "cycle_free T1" "cycle_free T2"
    unfolding T1_def T2_def
    using cycle_free_antimono unrestrictn_edges by blast+

  from ‹(x,y) ∈ edges T› have XYN: "x∈nodes T" "y∈nodes T" 
    using edges_subset by auto
  from XYN have [simp]: "nodes T1 = N1" "nodes T2 = N2" 
    unfolding T1_def T2_def N1_def N2_def unfolding E'_def
    apply (safe)
    apply (all ‹clarsimp›)
    by (metis DiffD1 nodesI(2) rtrancl.simps)+
  
  have "x∈N1" "y∈N2" by (auto simp: N1_def N2_def)   
  
  have "N1 ∩ N2 = {}" 
  proof (safe;simp)
    fix u
    assume "u∈N1" "u∈N2"
    hence "(x,u)∈E'*" "(u,y)∈E'*" by (auto simp: N1_def N2_def symD[OF SYME])
    with cycle_free_altD[OF ‹cycle_free T› ‹(x,y)∈edges T›] show False 
      unfolding E'_def by (meson rtrancl_trans)
  qed

  
  have N1C: "E'``N1 ⊆ N1"
    unfolding N1_def
    apply clarsimp 
    by (simp add: rtrancl.rtrancl_into_rtrancl)
  
  have N2C: "E'``N2 ⊆ N2"
    unfolding N2_def
    apply clarsimp 
    by (simp add: rtrancl.rtrancl_into_rtrancl)

  have XE1: "(x,u) ∈ (edges T1)*" if "u∈N1" for u
  proof -
    from that have "(x,u)∈E'*" by (auto simp: N1_def)
    then show ?thesis using ‹x∈N1› 
      unfolding T1_def
    proof (induction rule: converse_rtrancl_induct)
      case (step y z)
      with N1C have "z∈N1" by auto
      with step.hyps(1) step.prems have "(y,z)∈Restr (edges T) N1" 
        unfolding E'_def by auto
      with step.IH[OF ‹z∈N1›] show ?case 
        by (metis converse_rtrancl_into_rtrancl edges_restrict_nodes)
    qed auto
  qed    
  
  have XE2: "(y,u) ∈ (edges T2)*" if "u∈N2" for u
  proof -
    from that have "(y,u)∈E'*" by (auto simp: N2_def)
    then show ?thesis using ‹y∈N2› 
      unfolding T2_def
    proof (induction rule: converse_rtrancl_induct)
      case (step y z)
      with N2C have "z∈N2" by auto
      with step.hyps(1) step.prems have "(y,z)∈Restr (edges T) N2" 
        unfolding E'_def by auto
      with step.IH[OF ‹z∈N2›] show ?case 
        by (metis converse_rtrancl_into_rtrancl edges_restrict_nodes)
    qed auto
  qed    
  
  
  have "connected T1" 
    apply rule
    apply simp
    apply (drule XE1)+
    by (meson rtrancl_edges_sym' rtrancl_trans)      
  
  have "connected T2" 
    apply rule
    apply simp
    apply (drule XE2)+
    by (meson rtrancl_edges_sym' rtrancl_trans)      
   
  have "u∈N1 ∪ N2" if "u∈nodes T" for u 
  proof -
    from connectedD[OF ‹connected T› ‹x∈nodes T› that ]
    obtain p where P: "path T x p u" "simple p" 
      by (auto simp: rtrancl_edges_iff_path elim: simplify_pathE)
    show ?thesis proof cases
      assume "(x,y)∉set p ∧ (y,x)∉set p"
      with P(1) have "path (restrict_edges T E') x p u" 
        unfolding E'_def by (erule_tac path_graph_cong) auto
      from path_rtrancl_edgesD[OF this]
      show ?thesis unfolding N1_def E'_def by auto
    next
      assume "¬((x,y)∉set p ∧ (y,x)∉set p)"
      with P obtain p' where 
        "uedge (x,y)∉set (map uedge p')" "path T y p' u ∨ path T x p' u"
        by (auto simp: in_set_conv_decomp uedge_commute)
      hence "path (restrict_edges T E') y p' u ∨ path (restrict_edges T E') x p' u"  
        apply (clarsimp simp: uedge_in_set_eq E'_def)
        by (smt ComplD DiffI Int_iff UnCI edges_restrict_edges insertE 
                path_graph_cong subset_Compl_singleton subset_iff)
      then show ?thesis unfolding N1_def N2_def E'_def 
        by (auto dest: path_rtrancl_edgesD)
    qed
  qed
  then have "nodes T = N1 ∪ N2" 
    unfolding N1_def N2_def using XYN
    unfolding E'_def
    apply (safe)
    subgoal by auto []
    subgoal by (metis DiffD1 nodesI(2) rtrancl.cases)
    subgoal by (metis DiffD1 nodesI(2) rtrancl.cases)
    done

  have "edges T1 ∪ edges T2 ⊆ E'"
    unfolding T1_def T2_def E'_def using ‹N1 ∩ N2 = {}› ‹x ∈ N1› ‹y ∈ N2› 
    by auto  
  also have "edges T1 ∪ edges T2 ⊇ E'"
  proof -
    note ED1 = nodesI[where g=T, unfolded ‹nodes T = N1∪N2›]  
    have "E' ⊆ edges T" by (auto simp: E'_def)
    thus "edges T1 ∪ edges T2 ⊇ E'"
      unfolding T1_def T2_def
      using ED1 N1C N2C by (auto; blast)
  qed 
  finally have "edges T1 ∪ edges T2 = E'" .  
          
  show ?thesis
    apply (rule that[of T1 T2, unfolded tree_def]; (intro conjI)?; fact?)
    apply simp_all
    apply fact+
    done
qed
  
  
  
  
subsection ‹Spanning Trees›    
                                    
definition "is_spanning_tree G T 
  ≡ tree T ∧ nodes T = nodes G ∧ edges T ⊆ edges G"    
  
(* TODO: Move *)
lemma connected_singleton[simp]: "connected (ins_node u graph_empty)"
  unfolding connected_def by auto
  
lemma path_singleton[simp]: "path (ins_node u graph_empty) v p w ⟷ v=w ∧ p=[]"  
  by (cases p) auto

lemma tree_singleton[simp]: "tree (ins_node u graph_empty)"
  by (simp add: cycle_free_no_edges tree_def)

(* TODO: Move *)
lemma tree_add_edge_in_out:
  assumes "tree T"
  assumes "u∈nodes T" "v∉nodes T"
  shows "tree (ins_edge (u,v) T)"
proof -
  from assms have [simp]: "u≠v" by auto
  have "ins_edge (u,v) T = ins_edge (u,v) (graph_join T (ins_node v graph_empty))"
    by (auto simp: graph_eq_iff)
  also have "tree …"
    apply (rule join_trees)
    using assms
    by auto
  finally show ?thesis .
qed
  
text ‹Remove edges on cycles until the graph is cycle free›
lemma ex_spanning_tree: 
  "connected g ⟹ ∃t. is_spanning_tree g t"
  using edges_finite[of g]
proof (induction "edges g" arbitrary: g rule: finite_psubset_induct)
  case psubset
  show ?case proof (cases "cycle_free g")
    case True 
    with ‹connected g› show ?thesis by (auto simp: is_spanning_tree_def tree_def)
  next
    case False 
    then obtain u v where 
          EDGE: "(u,v)∈edges g" 
      and RED: "(u,v)∈(edges g - {(u,v),(v,u)})*" 
      using cycle_free_altI by metis
    from ‹connected g› 
      have "connected (restrict_edges g (- {(u,v),(v,u)}))" (is "connected ?g'")
      unfolding connected_def
      by (auto simp: remove_redundant_edge[OF RED])
    moreover have "edges ?g' ⊂ edges g" using EDGE by auto
    ultimately obtain t where "is_spanning_tree ?g' t" 
      using psubset.hyps(2)[of ?g'] by blast
    hence "is_spanning_tree g t" by (auto simp: is_spanning_tree_def)
    thus ?thesis ..
  qed
qed
  

section ‹Weighted Undirected Graphs›

definition weight :: "('v set ⇒ nat) ⇒ 'v ugraph ⇒ nat" 
  where "weight w g ≡ (∑e∈edges g. w (uedge e)) div 2"

  
lemma weight_alt: "weight w g = (∑e∈uedge`edges g. w e)"  
proof -
  from split_edges_sym[of g] obtain E where 
    "edges g = E ∪ E¯" and "E∩E¯={}" by auto
  hence [simp, intro!]: "finite E" by (metis edges_finite finite_Un) 
  hence [simp, intro!]: "finite (E¯)" by blast

  have [simp]: "(∑e∈E¯. w (uedge e)) = (∑e∈E. w (uedge e))"
    apply (rule sum.reindex_cong[where l=prod.swap and A="E¯" and B="E"])
    by (auto simp: uedge_def insert_commute)

  have [simp]: "inj_on uedge E" using ‹E∩E¯=_›
    by (auto simp: uedge_def inj_on_def doubleton_eq_iff)
        
  have "weight w g = (∑e∈E. w (uedge e))"
    unfolding weight_def ‹edges g = _› using ‹E∩E¯={}›
    by (auto simp: sum.union_disjoint)
  also have "… = (∑e∈uedge`E. w e)" 
    using sum.reindex[of uedge E w]
    by auto 
  also have "uedge`E = uedge`(edges g)"  
    unfolding ‹edges g = _› uedge_def using ‹E∩E¯={}›
    by auto
  finally show ?thesis .
qed 

lemma weight_empty[simp]: "weight w graph_empty = 0" unfolding weight_def by auto
  
lemma weight_ins_edge[simp]: "⟦u≠v; (u,v)∉edges g⟧ 
  ⟹ weight w (ins_edge (u,v) g) = w {u,v} + weight w g"
  unfolding weight_def
  apply clarsimp
  apply (subst sum.insert)
  by (auto dest: edges_sym' simp: uedge_def insert_commute)

lemma uedge_img_disj_iff[simp]: 
  "uedge`edges g1 ∩ uedge`edges g2 = {} ⟷ edges g1 ∩ edges g2 = {}"
  by (auto simp: uedge_eq_iff dest: edges_sym')+  
  
lemma weight_join[simp]: "edges g1 ∩ edges g2 = {} 
  ⟹ weight w (graph_join g1 g2) = weight w g1 + weight w g2"  
  unfolding weight_alt by (auto simp: sum.union_disjoint image_Un)

lemma weight_cong: "edges g1 = edges g2 ⟹ weight w g1 = weight w g2"  
  by (auto simp: weight_def)

lemma weight_mono: "edges g ⊆ edges g' ⟹ weight w g ≤ weight w g'"
  unfolding weight_alt by (rule sum_mono2) auto
  
lemma weight_ge_edge:
  assumes "(x,y)∈edges T"
  shows "weight w T ≥ w {x,y}"
  using assms unfolding weight_alt
  by (auto simp: uedge_def intro: member_le_sum)
  
  
          
lemma weight_del_edge[simp]: 
  assumes "(x,y)∈edges T"  
  shows "weight w (restrict_edges T (- {(x, y), (y, x)})) = weight w T - w {x,y}"
proof -
  define E where "E = uedge ` edges T - {{x,y}}"
  have [simp]: "(uedge ` (edges T - {(x, y), (y, x)})) = E"  
    by (safe; simp add: E_def uedge_def doubleton_eq_iff; blast)
    
  from assms have [simp]: "uedge ` edges T = insert {x,y} E"
    unfolding E_def by force

  have [simp]: "{x,y}∉E" unfolding E_def by blast        

  then show ?thesis
    unfolding weight_alt
    apply simp
    by (metis E_def ‹uedge ` edges T = insert {x, y} E› insertI1 sum_diff1_nat)
qed    
  
        
subsection ‹Minimum Spanning Trees›

definition "is_MST w g t ≡ is_spanning_tree g t 
  ∧ (∀t'. is_spanning_tree g t' ⟶ weight w t ≤ weight w t')"  

lemma exists_MST: "connected g ⟹ ∃t. is_MST w g t"
  using ex_has_least_nat[of "is_spanning_tree g"] ex_spanning_tree 
  unfolding is_MST_def 
  by blast
  
end