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)
  by (simp add: combine_per_def)

lemma combine_per_top [simp]: "combine_per ⊤ R = R"
  by (simp add: fun_eq_iff)

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

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)
  by (simp add: combine_per_def)

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