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 (Vfst`Esnd`E, (EE¯)-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) = Vfst`Esnd`E"    
  unfolding edges_def nodes_def graph_def by transfer auto
  
lemma edges_graph: "finite V; finite E  edges (graph V E) = (EE¯)-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) = EE¯ - 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" "EV×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  uv" 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 "unodes g" "vnodes g"
  using assms edges_subset by auto
  
lemma split_edges_sym: "E. EE¯ = {}  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*" "uV" "vV"
  obtains u' v' where "(u',v')EV×-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  (EE¯))"


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]: 
  "uv  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  (EE¯)"
  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)  eedges 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 "unodes g" "vnodes 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]: "xuedge (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 "uS" "vS" "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. xS"] assms obtain x y where 
    1: "(x,y)set p" "xS" "yS" 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[]  unodes 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 
   (eedges 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. unodes g; vnodes g  (u,v)(edges g)*"  
  shows "connected g"
  using assms unfolding connected_def by auto
  
lemma connectedD[intro?]: 
  assumes "connected g" "unodes g" "vnodes 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 "vreachable_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 "vreachable_nodes g r" "(u, v)  (edges (component_of g r))*" 
proof -
  show "vreachable_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: "rnodes 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: "unodes (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; rnodes 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: "rnodes 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: "unodes g1" "vnodes g2"
  shows "connected (ins_edge (u,v) (graph_join g1 g2))" (is "connected ?g'") 
  unfolding connected_def
proof clarify
  fix a b
  assume A: "anodes ?g'" "bnodes ?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 "anodes g1" "bnodes g1"
      hence ?thesis using connected g1 ESS(1) unfolding connected_def by blast
    } moreover {
      assume "anodes g2" "bnodes g2"
      hence ?thesis using connected g2 ESS(2) unfolding connected_def by blast
    } moreover {
      assume "anodes g1" "bnodes g2"
      with connectedD[OF CONN(1)] connectedD[OF CONN(2)] ESS
      have ?thesis by (meson UV IN_NODES contra_subsetD rtrancl_trans)
    } moreover {
      assume "anodes g2" "bnodes 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: "unodes g1" "vnodes 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: "anodes g1  nodes g2" 
    by auto
  thus False proof 
    assume N1: "anodes g1"
    have "set p  nodes g1 × nodes g1"
    proof (cases 
      rule: find_crossing_edges_on_path[where P="λx. xnodes 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: "anodes g2"
    have "set p  nodes g2 × nodes g2"
    proof (cases 
      rule: find_crossing_edges_on_path[where P="λx. xnodes 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: "unodes g1" "vnodes 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'*}"
    "xnodes T1" "ynodes 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: "xnodes T" "ynodes 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 "xN1" "yN2" by (auto simp: N1_def N2_def)   
  
  have "N1  N2 = {}" 
  proof (safe;simp)
    fix u
    assume "uN1" "uN2"
    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 "uN1" for u
  proof -
    from that have "(x,u)E'*" by (auto simp: N1_def)
    then show ?thesis using xN1 
      unfolding T1_def
    proof (induction rule: converse_rtrancl_induct)
      case (step y z)
      with N1C have "zN1" by auto
      with step.hyps(1) step.prems have "(y,z)Restr (edges T) N1" 
        unfolding E'_def by auto
      with step.IH[OF zN1] show ?case 
        by (metis converse_rtrancl_into_rtrancl edges_restrict_nodes)
    qed auto
  qed    
  
  have XE2: "(y,u)  (edges T2)*" if "uN2" for u
  proof -
    from that have "(y,u)E'*" by (auto simp: N2_def)
    then show ?thesis using yN2 
      unfolding T2_def
    proof (induction rule: converse_rtrancl_induct)
      case (step y z)
      with N2C have "zN2" by auto
      with step.hyps(1) step.prems have "(y,z)Restr (edges T) N2" 
        unfolding E'_def by auto
      with step.IH[OF zN2] 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 "uN1  N2" if "unodes T" for u 
  proof -
    from connectedD[OF connected T xnodes 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 = N1N2]  
    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 "unodes T" "vnodes T"
  shows "tree (ins_edge (u,v) T)"
proof -
  from assms have [simp]: "uv" 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  (eedges g. w (uedge e)) div 2"

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

  have [simp]: "(eE¯. w (uedge e)) = (eE. 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 EE¯=_
    by (auto simp: uedge_def inj_on_def doubleton_eq_iff)
        
  have "weight w g = (eE. w (uedge e))"
    unfolding weight_def edges g = _ using EE¯={}
    by (auto simp: sum.union_disjoint)
  also have " = (euedge`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 EE¯={}
    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]: "uv; (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