Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Combine_PER.thy Sprache: Isabelle

Original von: 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 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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.