src/ZF/pair.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 59498 50b60f501b05 permissions -rw-r--r--
proper context for match_tac etc.;
1 (*  Title:      ZF/pair.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1992  University of Cambridge
4 *)
6 section{*Ordered Pairs*}
8 theory pair imports upair
9 begin
11 ML_file "simpdata.ML"
13 setup {*
14   map_theory_simpset
15     (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
16       #> Simplifier.add_cong @{thm if_weak_cong})
17 *}
19 ML {* val ZF_ss = simpset_of @{context} *}
21 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
22   fn _ => Quantifier1.rearrange_bex
23     (fn ctxt =>
24       unfold_tac ctxt @{thms Bex_def} THEN
25       Quantifier1.prove_one_point_ex_tac)
26 *}
28 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
29   fn _ => Quantifier1.rearrange_ball
30     (fn ctxt =>
31       unfold_tac ctxt @{thms Ball_def} THEN
32       Quantifier1.prove_one_point_all_tac)
33 *}
36 (** Lemmas for showing that <a,b> uniquely determines a and b **)
38 lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
39 by (rule extension [THEN iff_trans], blast)
41 lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
42 by (rule extension [THEN iff_trans], blast)
44 lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
45 by (simp add: Pair_def doubleton_eq_iff, blast)
47 lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
49 lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
50 lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
52 lemma Pair_not_0: "<a,b> \<noteq> 0"
53 apply (unfold Pair_def)
54 apply (blast elim: equalityE)
55 done
57 lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
59 declare sym [THEN Pair_neq_0, elim!]
61 lemma Pair_neq_fst: "<a,b>=a ==> P"
62 proof (unfold Pair_def)
63   assume eq: "{{a, a}, {a, b}} = a"
64   have  "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
65   hence "{a, a} \<in> a" by (simp add: eq)
66   moreover have "a \<in> {a, a}" by (rule consI1)
67   ultimately show "P" by (rule mem_asym)
68 qed
70 lemma Pair_neq_snd: "<a,b>=b ==> P"
71 proof (unfold Pair_def)
72   assume eq: "{{a, a}, {a, b}} = b"
73   have  "{a, b} \<in> {{a, a}, {a, b}}" by blast
74   hence "{a, b} \<in> b" by (simp add: eq)
75   moreover have "b \<in> {a, b}" by blast
76   ultimately show "P" by (rule mem_asym)
77 qed
80 subsection{*Sigma: Disjoint Union of a Family of Sets*}
82 text{*Generalizes Cartesian product*}
84 lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a \<in> A & b \<in> B(a)"
85 by (simp add: Sigma_def)
87 lemma SigmaI [TC,intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a,b> \<in> Sigma(A,B)"
88 by simp
90 lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
91 lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
93 (*The general elimination rule*)
94 lemma SigmaE [elim!]:
95     "[| c \<in> Sigma(A,B);
96         !!x y.[| x \<in> A;  y \<in> B(x);  c=<x,y> |] ==> P
97      |] ==> P"
98 by (unfold Sigma_def, blast)
100 lemma SigmaE2 [elim!]:
101     "[| <a,b> \<in> Sigma(A,B);
102         [| a \<in> A;  b \<in> B(a) |] ==> P
103      |] ==> P"
104 by (unfold Sigma_def, blast)
106 lemma Sigma_cong:
107     "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
108      Sigma(A,B) = Sigma(A',B')"
109 by (simp add: Sigma_def)
111 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
112   flex-flex pairs and the "Check your prover" error.  Most
113   Sigmas and Pis are abbreviated as * or -> *)
115 lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
116 by blast
118 lemma Sigma_empty2 [simp]: "A*0 = 0"
119 by blast
121 lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
122 by blast
125 subsection{*Projections @{term fst} and @{term snd}*}
127 lemma fst_conv [simp]: "fst(<a,b>) = a"
128 by (simp add: fst_def)
130 lemma snd_conv [simp]: "snd(<a,b>) = b"
131 by (simp add: snd_def)
133 lemma fst_type [TC]: "p \<in> Sigma(A,B) ==> fst(p) \<in> A"
134 by auto
136 lemma snd_type [TC]: "p \<in> Sigma(A,B) ==> snd(p) \<in> B(fst(p))"
137 by auto
139 lemma Pair_fst_snd_eq: "a \<in> Sigma(A,B) ==> <fst(a),snd(a)> = a"
140 by auto
143 subsection{*The Eliminator, @{term split}*}
145 (*A META-equality, so that it applies to higher types as well...*)
146 lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
147 by (simp add: split_def)
149 lemma split_type [TC]:
150     "[|  p \<in> Sigma(A,B);
151          !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x,y>)
152      |] ==> split(%x y. c(x,y), p) \<in> C(p)"
153 by (erule SigmaE, auto)
155 lemma expand_split:
156   "u \<in> A*B ==>
157         R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
158 by (auto simp add: split_def)
161 subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
163 lemma splitI: "R(a,b) ==> split(R, <a,b>)"
164 by (simp add: split_def)
166 lemma splitE:
167     "[| split(R,z);  z \<in> Sigma(A,B);
168         !!x y. [| z = <x,y>;  R(x,y) |] ==> P
169      |] ==> P"
170 by (auto simp add: split_def)
172 lemma splitD: "split(R,<a,b>) ==> R(a,b)"
173 by (simp add: split_def)
175 text {*
176   \bigskip Complex rules for Sigma.
177 *}
179 lemma split_paired_Bex_Sigma [simp]:
180      "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
181 by blast
183 lemma split_paired_Ball_Sigma [simp]:
184      "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
185 by blast
187 end