Theory Kruskal

theory Kruskal
imports Kruskal_Misc  MinWeightBasis "HOL-Library.Uprod"   
begin


abbreviation "α'' == (λ(a,_,b). (a,b))"
abbreviation "α' == (λ(a,_,b). Upair a b)"

definition "lst_graph_P' w l S ≡ distinct (map α' l) ∧ (λ(a,_,b). Upair a b) ` set l = S 
                            ∧ (∀(a,wv,b)∈set l.  w (Upair a b) = wv)"


definition "lst_graph_rel' w ≡ {(l,S). lst_graph_P' w l S }"

locale Kruskal_intermediate_defs =
  fixes  E :: "('a uprod) set"
   and forest :: "('a uprod) set ⇒ bool"
   and connected :: "('a uprod) set ⇒ ('a*'a) set"
   and path :: "('a uprod) set ⇒ 'a ⇒ ('a uprod) list ⇒ 'a ⇒ bool"
   and weight :: "'a uprod ⇒ 'b::{linorder, ordered_comm_monoid_add}" 
begin

  definition "V = ⋃( set_uprod ` E)"

  lemma finiteE_finiteV: "finite E ⟹ finite V"
    by(auto simp: V_def)


end
  
locale Kruskal_intermediate = Kruskal_intermediate_defs   E forest connected path weight for
     E :: "('a uprod) set"
   and forest :: "('a uprod) set ⇒ bool"
   and connected :: "('a uprod) set ⇒ ('a*'a) set"
   and path :: "('a uprod) set ⇒ 'a ⇒ ('a uprod) list ⇒ 'a ⇒ bool"
   and weight :: "'a uprod ⇒ 'b::{linorder, ordered_comm_monoid_add}" +
 assumes Eproper: "⋀e. e∈E ⟹ proper_uprod e" 
   and 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_Epath: "(u,v) ∈ connected E'  ⟷ (∃p. path E' u p v ∧ u ∈ V ∧ v ∈ V)" 
   and connected_same: "(u,v) ∈ connected {} ⟷ u=v ∧ v∈V"
   and findaugmenting_aux: "path E1 u p v ⟹ ¬(∃p. path E2 u p v)
           ⟹ ∃a b. (a,b) ∉ connected E2 ∧ Upair a b ∉ E2 ∧ Upair a b ∈ E1"
   and augment_forest: "forest F ⟹ Upair u v ∈ E-F
           ⟹ forest (insert (Upair u v) F) ⟷ (u,v) ∉ connected F"
   and equiv: "F ⊆ E ⟹ equiv V (connected F)"
   and connected_in: "connected F ⊆ V × V"      
   and insert_reachable: "x≠y ⟹ x ∈ V ⟹ y ∈ V ⟹ F ⊆ E
           ⟹ connected (insert (Upair x y) F) = per_union (connected F) x y"  
begin

lemma E_inV: "⋀e. e∈E ⟹ set_uprod e ⊆ V"
  using V_def by auto

lemma finiteV[simp]: "finite V"
  by(auto intro: finiteE_finiteV)

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" "(Upair x y) ∉ F" "x∈V" "y∈V" "F ⊆ E"
  shows "Suc (card (CCs (insert (Upair x y) 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 xny assms(3-5)])
    apply(rule unify2EquivClasses_alt)          
         apply(fact assms(1)[unfolded CC_def])                           
        apply fact+      
      apply (fact connected_in)      
     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: "x = Upair a b"  using uprod_exhaust by blast
    then have xab': "a≠b" using  Eproper[OF xE]  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 E_inV xE by fastforce+
    from insert(2) xab have "Upair a b ∉ F" by auto

    have "(a,b) ∉ connected F" apply(subst augment_forest[symmetric])
        apply fact
      using xE xab apply simp
      using xab insert by auto
    with k abV sameCC_reachable have "CC F a ≠ CC F b" by auto 
    have "Suc (card (CCs (insert (Upair a b) 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 auto

  with CCs_imageCC cardlt show "False" by auto
qed


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 connected_Epath sameCC_reachable k sameCCinE1 obtain p
    where pathinE1: "path E1 u p v"
    by auto 
      ― ‹... but none in E2›  
  from f2 forest_subE have "E2 ⊆ E" by auto    
  with connected_Epath sameCC_reachable k diffCCinE2
  have nopathinE2: "¬(∃p. path E2 u p v)"
    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 where pe: "(a,b) ∉ connected E2" and abE2: "Upair a b ∉ E2"
    and abE1: "Upair a b ∈ E1"
    using findaugmenting_aux[OF pathinE1 nopathinE2] by auto

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

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

sublocale minWeightBasis 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 Kruskal_intermediate_time = Kruskal_intermediate +
 fixes     
       empty_forest_time  empty_uf_time indep_test_time insert_time insert_uf_time :: nat 
    and getEdges_time sort_time :: nat 
begin


sublocale minWeightBasis_time E forest weight      "getEdges_time + sort_time"
     "empty_forest_time + empty_uf_time" indep_test_time "insert_time+insert_uf_time" 
  apply unfold_locales .


end

end