(* 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)") = \
fn _ => Quantifier1.rearrange_Bex
(fn ctxt => unfold_tac ctxt @{thms Bex_def})
\<close>
simproc_setup defined_Ball ("\x\A. P(x) \ Q(x)") = \
fn _ => Quantifier1.rearrange_Ball
(fn ctxt => unfold_tac ctxt @{thms Ball_def})
\<close>
(** Lemmas for showing that <a,b> 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=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: " \ 0"
apply (unfold 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 ==> 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: "=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]: ": Sigma(A,B) \ a \ A & b \ B(a)"
by (simp add: Sigma_def)
lemma SigmaI [TC,intro!]: "[| a \ A; b \ B(a) |] ==> \ 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);
!!x y.[| x \<in> A; y \<in> B(x); c=<x,y> |] ==> P
|] ==> P"
by (unfold Sigma_def, blast)
lemma SigmaE2 [elim!]:
"[| \ Sigma(A,B);
[| a \<in> A; b \<in> B(a) |] ==> P
|] ==> 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"
by (simp add: fst_def)
lemma snd_conv [simp]: "snd() = 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), ) == c(a,b)"
by (simp add: split_def)
lemma split_type [TC]:
"[| p \ Sigma(A,B);
!!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x,y>)
|] ==> split(%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 = <x,y> \<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, )"
by (simp add: split_def)
lemma splitE:
"[| split(R,z); z \ Sigma(A,B);
!!x y. [| z = <x,y>; R(x,y) |] ==> P
|] ==> P"
by (auto simp add: split_def)
lemma splitD: "split(R,) ==> 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())"
by blast
lemma split_paired_Ball_Sigma [simp]:
"(\z \ Sigma(A,B). P(z)) \ (\x \ A. \y \ B(x). P())"
by blast
end
¤ Dauer der Verarbeitung: 0.1 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.
|
