1(*  Title:      ZF/pair.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1992  University of Cambridge
4*)
5
6section\<open>Ordered Pairs\<close>
7
8theory pair imports upair
9begin
10
11ML_file \<open>simpdata.ML\<close>
12
13setup \<open>
14  map_theory_simpset
15    (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
16      #> Simplifier.add_cong @{thm if_weak_cong})
17\<close>
18
19ML \<open>val ZF_ss = simpset_of \<^context>\<close>
20
21simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open>
22  fn _ => Quantifier1.rearrange_bex
23    (fn ctxt =>
24      unfold_tac ctxt @{thms Bex_def} THEN
25      Quantifier1.prove_one_point_ex_tac ctxt)
26\<close>
27
28simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
29  fn _ => Quantifier1.rearrange_ball
30    (fn ctxt =>
31      unfold_tac ctxt @{thms Ball_def} THEN
32      Quantifier1.prove_one_point_all_tac ctxt)
33\<close>
34
35
36(** Lemmas for showing that <a,b> uniquely determines a and b **)
37
38lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
39by (rule extension [THEN iff_trans], blast)
40
41lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
42by (rule extension [THEN iff_trans], blast)
43
44lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
45by (simp add: Pair_def doubleton_eq_iff, blast)
46
47lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
48
49lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
50lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
51
52lemma Pair_not_0: "<a,b> \<noteq> 0"
53apply (unfold Pair_def)
54apply (blast elim: equalityE)
55done
56
57lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
58
59declare sym [THEN Pair_neq_0, elim!]
60
61lemma Pair_neq_fst: "<a,b>=a ==> P"
62proof (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)
68qed
69
70lemma Pair_neq_snd: "<a,b>=b ==> P"
71proof (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)
77qed
78
79
80subsection\<open>Sigma: Disjoint Union of a Family of Sets\<close>
81
82text\<open>Generalizes Cartesian product\<close>
83
84lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a \<in> A & b \<in> B(a)"
85by (simp add: Sigma_def)
86
87lemma SigmaI [TC,intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a,b> \<in> Sigma(A,B)"
88by simp
89
90lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
91lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
92
93(*The general elimination rule*)
94lemma SigmaE [elim!]:
95    "[| c \<in> Sigma(A,B);
96        !!x y.[| x \<in> A;  y \<in> B(x);  c=<x,y> |] ==> P
97     |] ==> P"
98by (unfold Sigma_def, blast)
99
100lemma SigmaE2 [elim!]:
101    "[| <a,b> \<in> Sigma(A,B);
102        [| a \<in> A;  b \<in> B(a) |] ==> P
103     |] ==> P"
104by (unfold Sigma_def, blast)
105
106lemma Sigma_cong:
107    "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
108     Sigma(A,B) = Sigma(A',B')"
109by (simp add: Sigma_def)
110
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 -> *)
114
115lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
116by blast
117
118lemma Sigma_empty2 [simp]: "A*0 = 0"
119by blast
120
121lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
122by blast
123
124
125subsection\<open>Projections \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close>\<close>
126
127lemma fst_conv [simp]: "fst(<a,b>) = a"
128by (simp add: fst_def)
129
130lemma snd_conv [simp]: "snd(<a,b>) = b"
131by (simp add: snd_def)
132
133lemma fst_type [TC]: "p \<in> Sigma(A,B) ==> fst(p) \<in> A"
134by auto
135
136lemma snd_type [TC]: "p \<in> Sigma(A,B) ==> snd(p) \<in> B(fst(p))"
137by auto
138
139lemma Pair_fst_snd_eq: "a \<in> Sigma(A,B) ==> <fst(a),snd(a)> = a"
140by auto
141
142
143subsection\<open>The Eliminator, \<^term>\<open>split\<close>\<close>
144
145(*A META-equality, so that it applies to higher types as well...*)
146lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
147by (simp add: split_def)
148
149lemma 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)"
153by (erule SigmaE, auto)
154
155lemma 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)))"
158by (auto simp add: split_def)
159
160
161subsection\<open>A version of \<^term>\<open>split\<close> for Formulae: Result Type \<^typ>\<open>o\<close>\<close>
162
163lemma splitI: "R(a,b) ==> split(R, <a,b>)"
164by (simp add: split_def)
165
166lemma splitE:
167    "[| split(R,z);  z \<in> Sigma(A,B);
168        !!x y. [| z = <x,y>;  R(x,y) |] ==> P
169     |] ==> P"
170by (auto simp add: split_def)
171
172lemma splitD: "split(R,<a,b>) ==> R(a,b)"
173by (simp add: split_def)
174
175text \<open>
176  \bigskip Complex rules for Sigma.
177\<close>
178
179lemma 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>))"
181by blast
182
183lemma 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>))"
185by blast
186
187end
188
189
190