Quelle Combine_PER.thy Sprache: Isabelle

(*  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
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 \<open>\<approx>\<close> 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

quality95%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.