Quelle  Kruskal_Misc.thy

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: 
  assumes "equiv V R"
  shows "equiv V (per_union R a b)"
proof (rule equivI)
  have "R ⊆ V × V" and "refl_on V R" and "sym R" and "trans R"
    using ‹equiv V R› by (auto elim: equivE)

  show "per_union R a b ⊆ V × V"
    using ‹R ⊆ V × V› by (auto simp: per_union_def)

  show "refl_on V (per_union R a b)"
    using ‹refl_on V R› by (auto simp: per_union_def refl_on_def)

  show "sym (per_union R a b)"
    using ‹sym R› by (auto simp: per_union_def sym_def)

  show "trans (per_union R a b)"
    using ‹trans R› by (metis ‹sym R› part_equiv_def union_part_equivp)
qed

lemma equiv_mono:
  assumes "E' ⊆ E" and "equiv E R1"
  shows "equiv E' (R1 ∩ E'×E')"
proof (rule equivI)
  show "Restr R1 E' ⊆ E' × E'"
    by simp
next
  have "refl_on E R1"
    using ‹equiv E R1› by (auto elim: equivE)
  thus "refl_on E' (Restr R1 E')"
    by (metis (lifting) ext Field_square Refl_Restr UNIV_I assms(1) inf.absorb_iff2 refl_on_Int
        refl_on_def subsetI)
next
  have "sym R1"
    using ‹equiv E R1› by (auto elim: equivE)
  thus "sym (Restr R1 E')"
    by (metis mem_Sigma_iff symI sym_Int)
next
  have "trans R1"
    using ‹equiv E R1› by (auto elim: equivE)
  thus "trans (Restr R1 E')"
    using trans_Restr by fastforce
qed 

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