Theory Partial_Equiv_Rel

(*
  File: Partial_Equiv_Rel.thy
  Author: Bohua Zhan
*)

section ‹Partial equivalence relation›

theory Partial_Equiv_Rel
  imports "Auto2_HOL.Auto2_Main"
begin
  
text ‹
  Partial equivalence relations, following theory
  Lib/Partial\_Equivalence\_Relation in \<^cite>‹"Collections-AFP"›.
›

definition part_equiv :: "('a × 'a) set ⇒ bool" where [rewrite]:
  "part_equiv R ⟷ sym R ∧ trans R"

lemma part_equivI [forward]: "sym R ⟹ trans R ⟹ part_equiv R" by auto2
lemma part_equivD1 [forward]: "part_equiv R ⟹ sym R" by auto2
lemma part_equivD2 [forward]: "part_equiv R ⟹ trans R" by auto2
setup ‹del_prfstep_thm_eqforward @{thm part_equiv_def}›

subsection ‹Combining two elements in a partial equivalence relation›

definition per_union :: "('a × 'a) set ⇒ 'a ⇒ 'a ⇒ ('a × 'a) set" where [rewrite]:
  "per_union R a b = R ∪ { (x,y). (x,a)∈R ∧ (b,y)∈R } ∪ { (x,y). (x,b)∈R ∧ (a,y)∈R }"

lemma per_union_memI1 [backward]:
  "(x, y) ∈ R ⟹ (x, y) ∈ per_union R a b" by (simp add: per_union_def)
setup ‹add_forward_prfstep_cond @{thm per_union_memI1} [with_term "per_union ?R ?a ?b"]›

lemma per_union_memI2 [backward]:
  "(x, a) ∈ R ⟹ (b, y) ∈ R ⟹ (x, y) ∈ per_union R a b" by (simp add: per_union_def)

lemma per_union_memI3 [backward]:
  "(x, b) ∈ R ⟹ (a, y) ∈ R ⟹ (x, y) ∈ per_union R a b" by (simp add: per_union_def)

lemma per_union_memD:
  "(x, y) ∈ per_union R a b ⟹ (x, y) ∈ R ∨ ((x, a) ∈ R ∧ (b, y) ∈ R) ∨ ((x, b) ∈ R ∧ (a, y) ∈ R)"
  by (simp add: per_union_def)
setup ‹add_forward_prfstep_cond @{thm per_union_memD} [with_cond "?x ≠ ?y", with_filt (order_filter "x" "y")]›
setup ‹del_prfstep_thm @{thm per_union_def}›

lemma per_union_is_trans [forward]:
  "trans R ⟹ trans (per_union R a b)" by auto2

lemma per_union_is_part_equiv [forward]:
  "part_equiv R ⟹ part_equiv (per_union R a b)" by auto2

end