Theory Kruskal_Misc

section "Auxilliary Lemmas"  
theory Kruskal_Misc
  imports
    "Collections.Partial_Equivalence_Relation"
    "Automatic_Refinement.Misc"
    Refine_Imperative_HOL.Sepref
begin         
  
lemma card2_get2: assumes "card x = 2"
  obtains a b where  "x = {a, b}" "a ≠ b"
proof -
  from assms have [simp,intro!]: "finite x" apply(rule_tac ccontr) by auto
  from assms obtain a where ax: "a ∈ x"
    by fastforce
  with assms  have "card (x - {a}) = 1" by fastforce
  then obtain b where "x - {a} = {b}" "a ≠ b"
    by (metis Diff_cancel Diff_idemp card_1_singletonE insert_not_empty)
  with that ax show ?thesis by blast
qed

subsection "Lemmas on equivalence relations"
  
lemma equiv_sym: "equiv V R ⟹ (x,y)∈R ⟹ (y,x)∈R"
  by (metis equiv_def symD)

lemma equiv_trans: "equiv V R ⟹ (x,y)∈R ⟹ (y,z)∈R ⟹ (x,z)∈R"
  by (metis equiv_def transD)
    
lemma equiv_trans_sym: 
  "⟦ equiv V R; (a,b)∈R; (c,b)∈R ⟧ ⟹ (a,c)∈R"
  "⟦ equiv V R; (a,b)∈R; (a,c)∈R ⟧ ⟹ (b,c)∈R"
  apply (metis equiv_sym equiv_trans)+
  done
  
lemma union_equiv: 
  "equiv V R ⟹ equiv V (per_union R a b)"
  apply (rule equivI)        
  unfolding per_union_def 
  subgoal unfolding equiv_def refl_on_def by auto
  subgoal apply (rule symI) by (auto dest: equiv_sym)
  subgoal apply (rule transI) by (auto dest: equiv_trans equiv_trans_sym)
  done
  
  
lemma equiv_mono: "E'⊆E ⟹ equiv E R1 ⟹ equiv E' (R1 ∩ E'×E')"
  apply(rule equivI)
  subgoal unfolding equiv_def 
    by (simp add: refl_on_def subset_iff)  
  subgoal unfolding equiv_def 
    by (metis mem_Sigma_iff symI sym_Int)  
  subgoal unfolding equiv_def using trans_Restr by fastforce
  done
    
    

lemma unify2EquivClasses_alt: 
  assumes "R``{x} ≠ R``{y}" and inV: "y∈V" "x∈V" and "R⊆V×V"    
   and eq: "equiv V R" and [simp]: "finite V"
  shows "Suc (card (quotient V (per_union R x y))) = card (quotient V R)"
proof -
   
  from eq have Rtrancl: "R⇧+ = R" by (auto elim: equivE)
  from ‹equiv V R› have sym: "sym R" unfolding equiv_def by auto
  
  let ?R' = "per_union R x y"  

  ― ‹ the equivalence classes not contining x and y, stay unchanged when performing @{term per_union} ›
  have "⋀z. z ∈ V ⟹ z ∉ R `` {x} ⟹ z ∉ R `` {y} ⟹ per_union R x y `` {z} = R `` {z}"
    using sym by(auto simp: sym_def per_union_def)
  then have K: "(⋃x ∈ (V-(R``{x})-(R``{y})). {?R'``{x}}) = (⋃x ∈ (V-(R``{x})-(R``{y})). {R``{x}})"
    by auto 
  
  have R_respect: "(λx. {R `` {x}}) respects R"
    unfolding congruent_def using eq equiv_class_eq_iff by fastforce+
      
  have R'_respect: "(λxa. {?R' `` {xa}}) respects R"
    unfolding congruent_def per_union_def
      using eq equiv_class_eq_iff by force+ 

  ― ‹some facts about the equivalence class of x, before and after the @{term per_union} operation›
  have xdrin: "(R``{x}) ⊆ V" using assms(4) by auto
  have x1: "(⋃x ∈ (R``{x}). {?R'``{x}}) = {?R'``{x}}"
    apply(rule UN_equiv_class) by fact+
  have x2: "(⋃x ∈ (R``{x}). {R``{x}}) = {R``{x}}" 
    apply(rule UN_equiv_class) by fact+
      
  ― ‹some facts about the equivalence class of y, before and after the @{term per_union} operation›
  have ydrin: "(R``{y}) ⊆ V" using assms(4) by auto
  have y1: "(⋃x ∈ (R``{y}). {?R'``{x}}) = {?R'``{y}}"
    apply(rule UN_equiv_class) by fact+
  have y2: "(⋃x ∈ (R``{y}). {R``{x}}) = {R``{y}}" 
    apply(rule UN_equiv_class) by fact+
  
  have z: "(y,x)∈?R'" unfolding per_union_def using sym sym_def
    using assms(2) assms(3) eq eq_equiv_class by fastforce
  have bla: "?R'``{y} = ?R'``{x}" 
    apply(rule equiv_class_eq)
     apply(rule union_equiv) 
     apply fact
    by fact 
      
  let ?Vm = "(⋃x ∈ (V-(R``{x})-(R``{y})). {R``{x}})"  

  ― ‹now consider the set of quotients wrt. the relation after the @{term per_union}›
  have "quotient V ?R' = (⋃x ∈ V. {?R'``{x}})" unfolding quotient_def by auto
  also  ― ‹decompose it into the quotients for elements equivalent to x, y in R, and the rest›
  have "… = (⋃x ∈ (V-(R``{x})-(R``{y})). {?R'``{x}})
             ∪ (⋃x ∈ (R``{y}). {?R'``{x}}) ∪ (⋃x ∈ (R``{x}). {?R'``{x}})"     
    using xdrin ydrin by auto     
  also  ― ‹for the elements equivalent to x and y in R the quotient is 
            the quotient containing x and y respectively ›
  have "… = (⋃x ∈ (V-(R``{x})-(R``{y})). {?R'``{x}}) ∪ {?R'``{y}} ∪ {?R'``{x}}" using x1 y1 by auto 
  also  ― ‹which is after uniting them, the same quotient ›
  have "… = (⋃x ∈ (V-(R``{x})-(R``{y})). {R``{x}}) ∪ {?R'``{y}}" using K bla by auto 
  also
  have "… = insert (?R'``{y}) ?Vm" by auto
  finally have leftside: "quotient V ?R' = insert (?R'``{y}) ?Vm" .
      
  have notin: "?R'``{y} ∉ ?Vm" 
    apply (auto simp: per_union_def)
    by (metis (no_types, lifting) Image_singleton_iff UnI1 assms(2) eq equiv_class_self local.sym symE)  
  
  have o: "card (quotient V ?R') = Suc (card ?Vm)"
    unfolding leftside apply(rule card_insert_disjoint)
     using notin by auto
      
  ― ‹now consider the set of quotients wrt. the relation before the @{term per_union}›
  have "quotient V R = (⋃x ∈ V. {R``{x}})" unfolding quotient_def by auto
  also ― ‹decompose it into the quotients for elements equivalent to x, y in R, and the rest›
  have "… = (⋃x ∈ (V-(R``{x})-(R``{y})). {R``{x}})
           ∪ (⋃x ∈ (R``{y}). {R``{x}}) ∪ (⋃x ∈ (R``{x}). {R``{x}})"     
    using xdrin ydrin by auto     
  also ― ‹for the elements equivalent to x and y in R the quotient is 
            the quotient containing x and y respectively ›
  have "… = (⋃x ∈ (V-(R``{x})-(R``{y})). {R``{x}}) ∪ {R``{y}} ∪ {R``{x}}" using x2 y2 by auto 
  also ― ‹ these are two distinct quotients  ›
  have "… = insert (R``{y}) (insert (R``{x}) ?Vm)" by auto 
  finally have ii: "quotient V R = insert (R``{y}) (insert (R``{x}) ?Vm)" .
      
      
  have "R``{x} ∉ ?Vm"
    using eq equiv_class_self by fastforce   
  have "R``{y} ∉ ?Vm" 
    using eq equiv_class_self by fastforce  
  with assms(1)
  have "R``{y} ∉ (insert (R``{x}) ?Vm)" by blast
  have "card (quotient V R) = Suc (card (insert (R``{x}) ?Vm))" 
    apply(simp only: ii) 
    apply(rule card_insert_disjoint)
     apply simp
    apply fact done
  also have "card (insert (R``{x}) ?Vm) = Suc (card ?Vm)" 
    apply(rule card_insert_disjoint)
     apply simp
    apply fact done
  finally have a: "card (quotient V R) = Suc (Suc (card ?Vm))" by auto
  
  from a o show ?thesis by auto
qed  


  
  
subsection "On the pigeon hole principle"
  
lemma fixes f::"'c⇒'d"
    and g ::"'c⇒'d"
    assumes "finite A" and k: "⋀a b. a∈A ⟹ b∈A ⟹ f a = f b ⟹ g a = g b"
    shows  coarser: "card (f ` A) ≥ card (g ` A)"  
      using assms 
proof - 
  let ?h = "λd. THE x. {x} = g ` {x∈A. f x = d}" 
  term image 
  have z: "⋀x. x∈A ⟹ g ` {y∈A. f y = f x} = {g x} " 
     unfolding image_def apply auto using k  
     by blast
   have uz: "⋀x. x∈A ⟹ ?h (f x) = g x"
      by (simp add: z) 
  have "card (?h ` (f ` A)) ≤ card (f ` A)"
    apply(rule card_image_le)
    apply(rule finite_imageI) by fact
  moreover
    from uz have "?h ` (f ` A)  = g ` A"  
    by force
  ultimately show ?thesis by auto
qed   
       

subsection "On sorting and ‹max_node›"


definition edges_less_eq :: "('a × 'w::{linorder, ordered_comm_monoid_add} × 'a) ⇒ ('a × 'w × 'a) ⇒ bool"
  where "edges_less_eq a b ≡ fst(snd a) ≤ fst(snd b)"

definition "sort_edges ≡ quicksort_by_rel edges_less_eq []"

definition "max_node l ≡ Max (insert 0 (fst`set l ∪ (snd o snd)`set l))"

lemma max_node_impl[code]: "max_node l = fold (λ(u,_,w) x. max u (max w x)) l 0"
proof -
  have "fold (λ(u,_,w) x. max u (max w x)) l a = Max (insert a (fst`set l ∪ (snd o snd)`set l))" for a
    apply (induction l arbitrary: a)
     apply (auto simp:  )
    subgoal for a b l aa
      apply (cases l)
      by (auto simp: ac_simps)
    done
  thus ?thesis unfolding max_node_def by auto
qed

definition "is_linorder_rel R ≡ (∀x y. R x y ∨ R y x) ∧ (∀x y z. R x y ⟶ R y z ⟶ R x z)"

lemma edges_less_eq_linorder: "is_linorder_rel edges_less_eq"
  unfolding edges_less_eq_def is_linorder_rel_def
  by (metis linear order_trans)


lemma sort_edges_correct: "sorted_wrt edges_less_eq (quicksort_by_rel edges_less_eq [] l)"
  by (metis (no_types, opaque_lifting) edges_less_eq_linorder is_linorder_rel_def sorted_wrt_quicksort_by_rel)

lemma distinct_mset_eq:"distinct a ⟹ mset a = mset b ⟹ distinct b"
  by (metis card_distinct distinct_card set_mset_mset size_mset)

lemma quicksort_by_rel_distinct: "distinct l ⟹ distinct (quicksort_by_rel edges_less_eq [] l)"
  by (auto intro: distinct_mset_eq)

 
subsection "On @{term list_rel}"


lemma map_in_list_rel_conv: 
  shows "(l, l') ∈ ⟨br α I⟩list_rel ⟷ ((∀x∈set l. I x) ∧ l'=map α l)"
proof (induction l arbitrary: l') 
  case (Cons a l l')
  then show ?case apply(cases l') by (auto simp add: in_br_conv)
qed simp

lemma list_relD: "(x, y) ∈ ⟨br a I⟩list_rel ⟹ y = map a x" 
  by(auto simp: map_in_list_rel_conv)

lemma list_relD2: "(x, y) ∈ ⟨br a I⟩list_rel ⟹ y = map a x ∧ (∀x∈set x. I x)"
  by(auto simp: map_in_list_rel_conv) 


lemma list_set_rel_append: "(x,s)∈br a I ⟹ (xs,S)∈⟨br a I⟩list_set_rel ⟹ s∉S
     ⟹ (xs@[x],insert s S)∈⟨br a I⟩list_set_rel"
  unfolding list_set_rel_def
  apply(intro relcompI[where b="map a (xs @ [x])"])
   apply (auto simp: in_br_conv)
      apply parametricity by (auto dest: list_relD simp add: in_br_conv)
 
subsection "Auxiliary lemmas for Sepref"


lemma pure_fold: "(λa c. ↑ (c = a)) = pure Id" unfolding pure_def by auto
lemma list_assn_emp: "list_assn id_assn L L = emp" 
  apply(induct L) apply simp by (simp add: pure_def)

end