Theory 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