(* Author: Florian Haftmann, TU Muenchen *)
section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
theory Combine_PER
imports Main Lattice_Syntax
begin
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 \<open>\<exists>x. P x\<close> obtain x where "P x" ..
moreover from \<open>equivp R\<close> have "x \<approx> x"
by (rule equivp_reflp)
ultimately have "\x. P x \ x \ x"
by blast
with \<open>equivp R\<close> show ?thesis
by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp
elim: equivpE)
qed
end
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
