Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/ZF/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle pair.thy Sprache: Isabelle

(*  Title:      ZF/pair.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section\<open>Ordered Pairs\<close>

theory pair imports upair
begin

ML_file \<open>simpdata.ML\<close>

setup \<open>
  map_theory_simpset
    (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
      #> Simplifier.add_cong @{thm if_weak_cong})
\<close>

ML \<open>val ZF_ss = simpset_of \<^context>\<close>

simproc_setup defined_Bex ("\x\A. P(x) \ Q(x)") = \
  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
\<close>

simproc_setup defined_Ball ("\x\A. P(x) \ Q(x)") = \
  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
\<close>

(** Lemmas for showing that \<langle>a,b\<rangle> uniquely determines a and b **)

lemma singleton_eq_iff [iff]: "{a} = {b} \ a=b"
by (rule extension [THEN iff_trans], blast)

lemma doubleton_eq_iff: "{a,b} = {c,d} \ (a=c \ b=d) | (a=d \ b=c)"
by (rule extension [THEN iff_trans], blast)

lemma Pair_iff [simp]: "\a,b\ = \c,d\ \ a=c \ b=d"
by (simp add: Pair_def doubleton_eq_iff, blast)

lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]

lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]

lemma Pair_not_0: "\a,b\ \ 0"
  unfolding Pair_def
apply (blast elim: equalityE)
done

lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]

declare sym [THEN Pair_neq_0, elim!]

lemma Pair_neq_fst: "\a,b\=a \ P"
proof (unfold Pair_def)
  assume eq: "{{a, a}, {a, b}} = a"
  have  "{a, a} \ {{a, a}, {a, b}}" by (rule consI1)
  hence "{a, a} \ a" by (simp add: eq)
  moreover have "a \ {a, a}" by (rule consI1)
  ultimately show "P" by (rule mem_asym)
qed

lemma Pair_neq_snd: "\a,b\=b \ P"
proof (unfold Pair_def)
  assume eq: "{{a, a}, {a, b}} = b"
  have  "{a, b} \ {{a, a}, {a, b}}" by blast
  hence "{a, b} \ b" by (simp add: eq)
  moreover have "b \ {a, b}" by blast
  ultimately show "P" by (rule mem_asym)
qed

subsection\<open>Sigma: Disjoint Union of a Family of Sets\<close>

text\<open>Generalizes Cartesian product\<close>

lemma Sigma_iff [simp]: "\a,b\: Sigma(A,B) \ a \ A \ b \ B(a)"
by (simp add: Sigma_def)

lemma SigmaI [TC,intro!]: "\a \ A; b \ B(a)\ \ \a,b\ \ Sigma(A,B)"
by simp

lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]

(*The general elimination rule*)
lemma SigmaE [elim!]:
    "\c \ Sigma(A,B);
        \<And>x y.\<lbrakk>x \<in> A;  y \<in> B(x);  c=\<langle>x,y\<rangle>\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (unfold Sigma_def, blast)

lemma SigmaE2 [elim!]:
    "\\a,b\ \ Sigma(A,B);
        \<lbrakk>a \<in> A;  b \<in> B(a)\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (unfold Sigma_def, blast)

lemma Sigma_cong:
    "\A=A'; \x. x \ A' \ B(x)=B'(x)\ \
     Sigma(A,B) = Sigma(A',B')"
by (simp add: Sigma_def)

(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
  flex-flex pairs and the "Check your prover" error.  Most
  Sigmas and Pis are abbreviated as * or -> *)

lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
by blast

lemma Sigma_empty2 [simp]: "A*0 = 0"
by blast

lemma Sigma_empty_iff: "A*B=0 \ A=0 | B=0"
by blast

subsection\<open>Projections \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close>\<close>

lemma fst_conv [simp]: "fst(\a,b\) = a"
by (simp add: fst_def)

lemma snd_conv [simp]: "snd(\a,b\) = b"
by (simp add: snd_def)

lemma fst_type [TC]: "p \ Sigma(A,B) \ fst(p) \ A"
by auto

lemma snd_type [TC]: "p \ Sigma(A,B) \ snd(p) \ B(fst(p))"
by auto

lemma Pair_fst_snd_eq: "a \ Sigma(A,B) \ = a"
by auto

subsection\<open>The Eliminator, \<^term>\<open>split\<close>\<close>

(*A META-equality, so that it applies to higher types as well...*)
lemma split [simp]: "split(\x y. c(x,y), \a,b\) \ c(a,b)"
by (simp add: split_def)

lemma split_type [TC]:
    "\p \ Sigma(A,B);
         \<And>x y.\<lbrakk>x \<in> A; y \<in> B(x)\<rbrakk> \<Longrightarrow> c(x,y):C(\<langle>x,y\<rangle>)
\<rbrakk> \<Longrightarrow> split(\<lambda>x y. c(x,y), p) \<in> C(p)"
by (erule SigmaE, auto)

lemma expand_split:
  "u \ A*B \
        R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = \<langle>x,y\<rangle> \<longrightarrow> R(c(x,y)))"
by (auto simp add: split_def)

subsection\<open>A version of \<^term>\<open>split\<close> for Formulae: Result Type \<^typ>\<open>o\<close>\<close>

lemma splitI: "R(a,b) \ split(R, \a,b\)"
by (simp add: split_def)

lemma splitE:
    "\split(R,z); z \ Sigma(A,B);
        \<And>x y. \<lbrakk>z = \<langle>x,y\<rangle>;  R(x,y)\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (auto simp add: split_def)

lemma splitD: "split(R,\a,b\) \ R(a,b)"
by (simp add: split_def)

text \<open>
  \bigskip Complex rules for Sigma.
\<close>

lemma split_paired_Bex_Sigma [simp]:
     "(\z \ Sigma(A,B). P(z)) \ (\x \ A. \y \ B(x). P(\x,y\))"
by blast

lemma split_paired_Ball_Sigma [simp]:
     "(\z \ Sigma(A,B). P(z)) \ (\x \ A. \y \ B(x). P(\x,y\))"
by blast

end

quality100%

¤ Dauer der Verarbeitung: 0.17 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.