Theory Kruskal

section ‹Kruskal interface›

theory Kruskal
imports Kruskal_Misc MinWeightBasis  
begin

text ‹In order to instantiate Kruskal's algorithm for different graph formalizations we provide
  an interface consisting of the relevant concepts needed for the algorithm, but hiding the concrete
  structure of the graph formalization.
  We thus enable using both undirected graphs and symmetric directed graphs.

  Based on the interface, we show that the set of edges together with the predicate of being 
  cycle free (i.e. a forest) forms the cycle matroid.
  Together with a weight function on the edges we obtain a ‹weighted_matroid› and thus
  an instance of the minimum weight basis algorithm, which is an abstract version of Kruskal.›
 
  
locale Kruskal_interface = 
  fixes E :: "'edge set"
    and V :: "'a set"
    and vertices :: "'edge ⇒ 'a set"
    and joins :: "'a ⇒ 'a ⇒ 'edge ⇒ bool"
    and forest :: "'edge set ⇒ bool"
    and connected :: "'edge set ⇒ ('a*'a) set"
    and weight :: "'edge ⇒ 'b::{linorder, ordered_comm_monoid_add}"
 assumes 
      finiteE[simp]: "finite E"  
   and forest_subE: "forest E' ⟹ E' ⊆ E" 
   and forest_empty: "forest {}"
   and forest_mono: "forest X ⟹ Y ⊆ X ⟹ forest Y"  
   and connected_same: "(u,v) ∈ connected {} ⟷ u=v ∧ v∈V" 
   and findaugmenting_aux: "E1 ⊆ E ⟹ E2 ⊆ E ⟹ (u,v) ∈ connected E1 ⟹ (u,v)∉ connected E2
           ⟹ ∃a b e. (a,b) ∉ connected E2 ∧ e ∉ E2 ∧ e ∈ E1 ∧ joins a b e" 
   and augment_forest: "forest F ⟹ e ∈ E-F ⟹ joins u v e
           ⟹ forest (insert e F) ⟷ (u,v) ∉ connected F"  
   and equiv: "F ⊆ E ⟹ equiv V (connected F)"
   and connected_in: "F ⊆ E ⟹ connected F ⊆ V × V"      
   and insert_reachable: "x ∈ V ⟹ y ∈ V ⟹ F ⊆ E ⟹ e∈E ⟹ joins x y e
           ⟹ connected (insert e F) = per_union (connected F) x y"   
   and exhaust: "⋀x. x∈E ⟹ ∃a b. joins a b x"
   and vertices_constr: "⋀a b e. joins a b e ⟹ {a,b} ⊆ vertices e"
   and joins_sym: "⋀a b e. joins a b e = joins b a e"
   and selfloop_no_forest: "⋀e. e∈E ⟹ joins a a e ⟹ ~forest (insert e F)"
   and finite_vertices: "⋀e. e∈E ⟹ finite (vertices e)"
  
  and edgesinvertices: "⋃( vertices ` E) ⊆ V"
  and finiteV[simp]: "finite V"
  and joins_connected: "joins a b e ⟹ T⊆E ⟹ e∈T ⟹ (a,b) ∈ connected T"

begin

subsection ‹Derived facts› 

lemma joins_in_V: "joins a b e ⟹ e∈E ⟹ a∈V ∧ b∈V"
  apply(frule vertices_constr) using edgesinvertices by blast

  lemma finiteE_finiteV: "finite E ⟹ finite V"
    using finite_vertices by auto
 
lemma E_inV: "⋀e. e∈E ⟹ vertices e ⊆ V"
  using edgesinvertices by auto  

definition "CC E' x = (connected E')``{x}"      

lemma sameCC_reachable: "E' ⊆ E ⟹ u∈V ⟹ v∈V ⟹ CC E' u = CC E' v ⟷ (u,v) ∈ connected E'"
  unfolding CC_def using  equiv_class_eq_iff[OF equiv ] by auto

definition "CCs E' = quotient V (connected E')"  

lemma "quotient V Id = {{v}|v. v∈V}" unfolding quotient_def by auto  

lemma CCs_empty: "CCs {} = {{v}|v. v∈V}"   
  unfolding CCs_def unfolding quotient_def using connected_same by auto

lemma CCs_empty_card: "card (CCs {}) = card V"   
proof -
  have i: "{{v}|v. v∈V} = (λv. {v})`V"  
    by blast 
  have "card (CCs {}) = card {{v}|v. v∈V}" 
    using CCs_empty  by auto
  also have "… = card ((λv. {v})`V)" by(simp only: i) 
  also have "… = card V"
    apply(rule card_image)
    unfolding inj_on_def by auto
  finally show ?thesis .
qed

lemma CCs_imageCC: "CCs F = (CC F) ` V"
  unfolding CCs_def CC_def quotient_def  
  by blast


lemma union_eqclass_decreases_components: 
  assumes "CC F x ≠ CC F y" "e ∉ F" "x∈V" "y∈V" "F ⊆ E" "e∈E" "joins x y e" 
  shows "Suc (card (CCs (insert e F))) = card (CCs F)"
proof -  
  from assms(1) have xny: "x≠y" by blast   
  show ?thesis unfolding CCs_def
    apply(simp only: insert_reachable[OF   assms(3-7)])
    apply(rule unify2EquivClasses_alt)          
         apply(fact assms(1)[unfolded CC_def])                           
        apply fact+
      apply (rule connected_in)  
      apply fact    
     apply(rule equiv) 
     apply fact  
    by (fact finiteV)      
qed

lemma forest_CCs: assumes "forest E'" shows "card (CCs E') + card E' = card V"
proof -
  from assms have "finite E'" using forest_subE
    using finiteE finite_subset by blast
  from this assms show ?thesis
  proof(induct E') 
    case (insert x F)
    then have xE: "x∈E" using forest_subE by auto
    from this obtain a b where xab: "joins a b x"  using exhaust by blast
    { assume "a=b"
      with xab xE selfloop_no_forest insert(4) have "False" by auto
    }
    then have xab': "a≠b" by auto
    from insert(4) forest_mono have fF: "forest F" by auto
    with insert(3) have eq: "card (CCs F) + card F = card V" by auto 

    from insert(4) forest_subE have k: "F ⊆ E" by auto     
    from xab xab' have abV: "a∈V" "b∈V" using vertices_constr E_inV xE by fastforce+

    have "(a,b) ∉ connected F" 
      apply(subst augment_forest[symmetric])
         apply (rule fF)
      using xE xab xab insert by auto
    with k abV sameCC_reachable have "CC F a ≠ CC F b" by auto 
    have "Suc (card (CCs (insert x F))) = card (CCs F)" 
      apply(rule union_eqclass_decreases_components)  
      by fact+ 
    then show ?case using xab insert(1,2) eq   by auto 
  qed (simp add: CCs_empty_card)
qed

lemma pigeonhole_CCs: 
  assumes finiteV: "finite V" and cardlt: "card (CCs E1) < card (CCs E2)"
  shows "(∃u v. u∈V ∧ v∈V ∧ CC E1 u = CC E1 v ∧ CC E2 u ≠ CC E2 v)"  
proof (rule ccontr, clarsimp)
  assume "∀u. u ∈ V ⟶ (∀v. CC E1 u = CC E1 v ⟶ v ∈ V ⟶ CC E2 u = CC E2 v)"
  then have "⋀u v. u∈V ⟹ v∈V ⟹ CC E1 u = CC E1 v ⟹ CC E2 u = CC E2 v" by blast

  with coarser[OF finiteV] have "card ((CC E1) ` V) ≥ card ((CC E2) ` V)" by blast

  with CCs_imageCC cardlt show "False" by auto
qed

subsection ‹The edge set and forest form the cycle matroid› 
 

theorem assumes f1: "forest E1"
  and f2: "forest E2"  
  and c: "card E1 > card E2"
shows augment: "∃e∈E1-E2. forest (insert e E2)"
proof -
  ― ‹as E1 and E2 are both forests, and E1 has more edges than E2, E2 has more connected
        components than E1› 
  from forest_CCs[OF f1] forest_CCs[OF f2] c have "card (CCs E1) < card (CCs E2)" by linarith

  ― ‹by an pigeonhole argument, we can obtain two vertices u and v
     that are in the same components of E1, but in different components of E2›
  then obtain u v where sameCCinE1: "CC E1 u = CC E1 v" and
    diffCCinE2: "CC E2 u ≠ CC E2 v" and k: "u ∈ V" "v ∈ V"
    using pigeonhole_CCs[OF finiteV] by blast   

  from diffCCinE2 have unv: "u ≠ v" by auto

  ― ‹this means that there is a path from u to v in E1 ...›   
  from f1 forest_subE have e1: "E1 ⊆ E" by auto    
  with   sameCC_reachable k sameCCinE1 have pathinE1: "(u, v) ∈ connected E1" 
    by auto 
      ― ‹... but none in E2›  
  from f2 forest_subE have e2: "E2 ⊆ E" by auto    
  with   sameCC_reachable k diffCCinE2
  have nopathinE2: "(u, v) ∉ connected E2" 
    by auto

  ― ‹hence, we can find vertices a and b that are not connected in E2,
          but are connected by an edge in E1›    
  obtain a b e where pe: "(a,b) ∉ connected E2" and abE2: "e ∉ E2"
    and abE1: "e ∈ E1" and "joins a b e"
    using findaugmenting_aux[OF e1 e2 pathinE1 nopathinE2]    by auto

  with forest_subE[OF f1] have "e ∈ E" by auto
  from abE1 abE2 have abdif: "e ∈ E1 - E2" by auto
  with e1 have "e ∈ E - E2" by auto

  ― ‹we can savely add this edge between a and b to E2 and obtain a bigger forest›    
  have "forest (insert e E2)" apply(subst augment_forest)
    by fact+
  then show "∃e∈E1-E2. forest (insert e E2)" using abdif
    by blast
qed

sublocale weighted_matroid E forest weight
proof             
  have "forest {}" using forest_empty by auto
  then show "∃X. forest X" by blast 
qed (auto simp: forest_subE forest_mono augment)

end ― ‹locale @{text Kruskal_interface}›

end