Theory Collections.Partial_Equivalence_Relation

theory Partial_Equivalence_Relation
imports Main
begin

subsection ‹Partial Equivalence Relations›
text ‹
  The abstract datatype for a union-find structure is a partial equivalence
  relation.
›

definition "part_equiv R  sym R  trans R"

lemma part_equivI[intro?]: "sym R; trans R  part_equiv R" 
  by (simp add: part_equiv_def)

lemma part_equiv_refl:
  "part_equiv R  (x,y)R  (x,x)R"
  "part_equiv R  (x,y)R  (y,y)R"
  by (metis part_equiv_def symD transD)+

lemma part_equiv_sym: "part_equiv R  (x,y)R  (y,x)R"
  by (metis part_equiv_def symD)

lemma part_equiv_trans: "part_equiv R  (x,y)R  (y,z)R  (x,z)R"
  by (metis part_equiv_def transD)

lemma part_equiv_trans_sym: 
  " part_equiv R; (a,b)R; (c,b)R   (a,c)R"
  " part_equiv R; (a,b)R; (a,c)R   (b,c)R"
  apply (metis part_equiv_sym part_equiv_trans)+
  done

text ‹We define a shortcut for symmetric closure.›
definition "symcl R  R  R¯"

lemma sym_symcl[simp, intro!]: "sym (symcl R)"
  by (metis sym_Un_converse symcl_def)
lemma sym_trans_is_part_equiv[simp, intro!]: "part_equiv ((symcl R)*)"
  by (metis part_equiv_def sym_rtrancl sym_symcl trans_rtrancl)

text ‹We also define a shortcut for melding the equivalence classes of
  two given elements›
definition per_union where "per_union R a b  R  
  { (x,y). (x,a)R  (y,b)R }  { (y,x). (x,a)R  (y,b)R }"

lemma union_part_equivp: 
  "part_equiv R  part_equiv (per_union R a b)"
  apply rule
  unfolding per_union_def
  apply (rule symI)
  apply (auto dest: part_equiv_sym) []

  apply (rule transI)
  apply (auto dest: part_equiv_trans part_equiv_trans_sym)
  done

lemma per_union_cmp: 
  " part_equiv R; (l,j)R   per_union R l j = R"
  unfolding per_union_def by (auto dest: part_equiv_trans_sym)

lemma per_union_same[simp]: "part_equiv R  per_union R l l = R"
  unfolding per_union_def by (auto dest: part_equiv_trans_sym)

lemma per_union_commute[simp]: "per_union R i j = per_union R j i"
  unfolding per_union_def by auto

lemma per_union_dom[simp]: "Domain (per_union R i j) = Domain R"
  unfolding per_union_def by auto

lemma per_classes_dj: 
  "part_equiv R; (i,j)R  R``{i}  R``{j} = {}"
  by (auto dest: part_equiv_trans_sym)

lemma per_class_in_dom: "part_equiv R  R``{i}  Domain R"
  by (auto dest: part_equiv_trans_sym)

end