# Theory Combine_PER

```(*  Author:     Florian Haftmann, TU Muenchen *)

section ‹A combinator to build partial equivalence relations from a predicate and an equivalence relation›

theory Combine_PER
imports Main
begin

unbundle lattice_syntax

definition combine_per :: "('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where "combine_per P R = (λx y. P x ∧ P y) ⊓ R"

lemma combine_per_simp [simp]:
"combine_per P R x y ⟷ P x ∧ P y ∧ x ≈ y" for R (infixl "≈" 50)

lemma combine_per_top [simp]: "combine_per ⊤ R = R"

lemma combine_per_eq [simp]: "combine_per P HOL.eq = HOL.eq ⊓ (λx y. P x)"

lemma symp_combine_per: "symp R ⟹ symp (combine_per P R)"
by (auto simp add: symp_def sym_def combine_per_def)

lemma transp_combine_per: "transp R ⟹ transp (combine_per P R)"
by (auto simp add: transp_def trans_def combine_per_def)

lemma combine_perI: "P x ⟹ P y ⟹ x ≈ y ⟹ combine_per P R x y" for R (infixl "≈" 50)

lemma symp_combine_per_symp: "symp R ⟹ symp (combine_per P R)"
by (auto intro!: sympI elim: sympE)

lemma transp_combine_per_transp: "transp R ⟹ transp (combine_per P R)"
by (auto intro!: transpI elim: transpE)

lemma equivp_combine_per_part_equivp [intro?]:
fixes R (infixl "≈" 50)
assumes "∃x. P x" and "equivp R"
shows "part_equivp (combine_per P R)"
proof -
from ‹∃x. P x› obtain x where "P x" ..
moreover from ‹equivp R› have "x ≈ x"
by (rule equivp_reflp)
ultimately have "∃x. P x ∧ x ≈ x"
by blast
with ‹equivp R› show ?thesis
by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp
elim: equivpE)
qed

end
```