6 Ordered pairs in Zermelo-Fraenkel Set Theory |
6 Ordered pairs in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
9 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
10 |
10 |
11 qed_goal "singleton_eq_iff" ZF.thy |
11 qed_goal "singleton_eq_iff" thy |
12 "{a} = {b} <-> a=b" |
12 "{a} = {b} <-> a=b" |
13 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
13 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
14 (fast_tac upair_cs 1) ]); |
14 (Fast_tac 1) ]); |
15 |
15 |
16 qed_goal "doubleton_eq_iff" ZF.thy |
16 qed_goal "doubleton_eq_iff" thy |
17 "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)" |
17 "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)" |
18 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
18 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
19 (fast_tac upair_cs 1) ]); |
19 (Fast_tac 1) ]); |
20 |
20 |
21 qed_goalw "Pair_iff" ZF.thy [Pair_def] |
21 qed_goalw "Pair_iff" thy [Pair_def] |
22 "<a,b> = <c,d> <-> a=c & b=d" |
22 "<a,b> = <c,d> <-> a=c & b=d" |
23 (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_eq_iff]) 1), |
23 (fn _=> [ (simp_tac (!simpset addsimps [doubleton_eq_iff]) 1), |
24 (fast_tac FOL_cs 1) ]); |
24 (Fast_tac 1) ]); |
25 |
25 |
26 bind_thm ("Pair_inject", (Pair_iff RS iffD1 RS conjE)); |
26 Addsimps [Pair_iff]; |
27 |
27 |
28 qed_goal "Pair_inject1" ZF.thy "<a,b> = <c,d> ==> a=c" |
28 bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE); |
29 (fn [major]=> |
|
30 [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]); |
|
31 |
29 |
32 qed_goal "Pair_inject2" ZF.thy "<a,b> = <c,d> ==> b=d" |
30 AddSEs [Pair_inject]; |
33 (fn [major]=> |
|
34 [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]); |
|
35 |
31 |
36 qed_goalw "Pair_neq_0" ZF.thy [Pair_def] "<a,b>=0 ==> P" |
32 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1); |
37 (fn [major]=> |
33 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2); |
38 [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1), |
|
39 (rtac consI1 1) ]); |
|
40 |
34 |
41 qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P" |
35 qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0" |
|
36 (fn _ => [ (fast_tac (!claset addEs [equalityE]) 1) ]); |
|
37 |
|
38 bind_thm ("Pair_neq_0", Pair_not_0 RS notE); |
|
39 |
|
40 AddSEs [Pair_neq_0, sym RS Pair_neq_0]; |
|
41 |
|
42 qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P" |
42 (fn [major]=> |
43 (fn [major]=> |
43 [ (rtac (consI1 RS mem_asym RS FalseE) 1), |
44 [ (rtac (consI1 RS mem_asym RS FalseE) 1), |
44 (rtac (major RS subst) 1), |
45 (rtac (major RS subst) 1), |
45 (rtac consI1 1) ]); |
46 (rtac consI1 1) ]); |
46 |
47 |
47 qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P" |
48 qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P" |
48 (fn [major]=> |
49 (fn [major]=> |
49 [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1), |
50 [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1), |
50 (rtac (major RS subst) 1), |
51 (rtac (major RS subst) 1), |
51 (rtac (consI1 RS consI2) 1) ]); |
52 (rtac (consI1 RS consI2) 1) ]); |
52 |
53 |
53 |
54 |
54 (*** Sigma: Disjoint union of a family of sets |
55 (*** Sigma: Disjoint union of a family of sets |
55 Generalizes Cartesian product ***) |
56 Generalizes Cartesian product ***) |
56 |
57 |
57 qed_goalw "SigmaI" ZF.thy [Sigma_def] |
58 qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)" |
58 "[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)" |
59 (fn _ => [ Fast_tac 1 ]); |
59 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); |
60 |
|
61 Addsimps [Sigma_iff]; |
|
62 |
|
63 qed_goal "SigmaI" thy |
|
64 "!!a b. [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)" |
|
65 (fn _ => [ Asm_simp_tac 1 ]); |
|
66 |
|
67 bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1); |
|
68 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2); |
60 |
69 |
61 (*The general elimination rule*) |
70 (*The general elimination rule*) |
62 qed_goalw "SigmaE" ZF.thy [Sigma_def] |
71 qed_goalw "SigmaE" thy [Sigma_def] |
63 "[| c: Sigma(A,B); \ |
72 "[| c: Sigma(A,B); \ |
64 \ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \ |
73 \ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \ |
65 \ |] ==> P" |
74 \ |] ==> P" |
66 (fn major::prems=> |
75 (fn major::prems=> |
67 [ (cut_facts_tac [major] 1), |
76 [ (cut_facts_tac [major] 1), |
68 (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
77 (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
69 |
78 |
70 (** Elimination of <a,b>:A*B -- introduces no eigenvariables **) |
79 qed_goal "SigmaE2" thy |
71 qed_goal "SigmaD1" ZF.thy "<a,b> : Sigma(A,B) ==> a : A" |
|
72 (fn [major]=> |
|
73 [ (rtac (major RS SigmaE) 1), |
|
74 (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
75 |
|
76 qed_goal "SigmaD2" ZF.thy "<a,b> : Sigma(A,B) ==> b : B(a)" |
|
77 (fn [major]=> |
|
78 [ (rtac (major RS SigmaE) 1), |
|
79 (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
80 |
|
81 (*Also provable via |
|
82 rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac) |
|
83 THEN prune_params_tac) |
|
84 (read_instantiate [("c","<a,b>")] SigmaE); *) |
|
85 qed_goal "SigmaE2" ZF.thy |
|
86 "[| <a,b> : Sigma(A,B); \ |
80 "[| <a,b> : Sigma(A,B); \ |
87 \ [| a:A; b:B(a) |] ==> P \ |
81 \ [| a:A; b:B(a) |] ==> P \ |
88 \ |] ==> P" |
82 \ |] ==> P" |
89 (fn [major,minor]=> |
83 (fn [major,minor]=> |
90 [ (rtac minor 1), |
84 [ (rtac minor 1), |
91 (rtac (major RS SigmaD1) 1), |
85 (rtac (major RS SigmaD1) 1), |
92 (rtac (major RS SigmaD2) 1) ]); |
86 (rtac (major RS SigmaD2) 1) ]); |
93 |
87 |
94 qed_goalw "Sigma_cong" ZF.thy [Sigma_def] |
88 qed_goalw "Sigma_cong" thy [Sigma_def] |
95 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
89 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
96 \ Sigma(A,B) = Sigma(A',B')" |
90 \ Sigma(A,B) = Sigma(A',B')" |
97 (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]); |
91 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
98 |
92 |
99 qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0" |
|
100 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]); |
|
101 |
93 |
102 qed_goal "Sigma_empty2" ZF.thy "A*0 = 0" |
94 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
103 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]); |
95 flex-flex pairs and the "Check your prover" error. Most |
|
96 Sigmas and Pis are abbreviated as * or -> *) |
104 |
97 |
105 val pair_cs = upair_cs |
98 AddSIs [SigmaI]; |
106 addSIs [SigmaI] |
99 AddSEs [SigmaE2, SigmaE]; |
107 addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject, |
100 |
108 Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0]; |
101 qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0" |
|
102 (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]); |
|
103 |
|
104 qed_goal "Sigma_empty2" thy "A*0 = 0" |
|
105 (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]); |
|
106 |
|
107 Addsimps [Sigma_empty1, Sigma_empty2]; |
109 |
108 |
110 |
109 |
111 (*** Projections: fst, snd ***) |
110 (*** Projections: fst, snd ***) |
112 |
111 |
113 qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a" |
112 qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a" |
114 (fn _=> |
113 (fn _=> [ (fast_tac (!claset addIs [the_equality]) 1) ]); |
115 [ (fast_tac (pair_cs addIs [the_equality]) 1) ]); |
|
116 |
114 |
117 qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b" |
115 qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b" |
118 (fn _=> |
116 (fn _=> [ (fast_tac (!claset addIs [the_equality]) 1) ]); |
119 [ (fast_tac (pair_cs addIs [the_equality]) 1) ]); |
|
120 |
117 |
121 val pair_ss = FOL_ss addsimps [fst_conv,snd_conv]; |
118 Addsimps [fst_conv,snd_conv]; |
122 |
119 |
123 qed_goal "fst_type" ZF.thy |
120 qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A" |
124 "!!p. p:Sigma(A,B) ==> fst(p) : A" |
121 (fn _=> [ Auto_tac() ]); |
125 (fn _=> [ (fast_tac (pair_cs addss pair_ss) 1) ]); |
|
126 |
122 |
127 qed_goal "snd_type" ZF.thy |
123 qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))" |
128 "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))" |
124 (fn _=> [ Auto_tac() ]); |
129 (fn _=> [ (fast_tac (pair_cs addss pair_ss) 1) ]); |
|
130 |
125 |
131 goal ZF.thy "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"; |
126 qed_goal "Pair_fst_snd_eq" thy |
132 by (etac SigmaE 1); |
127 "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a" |
133 by (asm_simp_tac pair_ss 1); |
128 (fn _=> [ Auto_tac() ]); |
134 qed "Pair_fst_snd_eq"; |
|
135 |
129 |
136 |
130 |
137 (*** Eliminator - split ***) |
131 (*** Eliminator - split ***) |
138 |
132 |
139 (*A META-equality, so that it applies to higher types as well...*) |
133 (*A META-equality, so that it applies to higher types as well...*) |
140 qed_goalw "split" ZF.thy [split_def] |
134 qed_goalw "split" thy [split_def] "split(%x y.c(x,y), <a,b>) == c(a,b)" |
141 "split(%x y.c(x,y), <a,b>) == c(a,b)" |
135 (fn _ => [ (Simp_tac 1), |
142 (fn _ => [ (simp_tac pair_ss 1), |
|
143 (rtac reflexive_thm 1) ]); |
136 (rtac reflexive_thm 1) ]); |
144 |
137 |
145 qed_goal "split_type" ZF.thy |
138 Addsimps [split]; |
|
139 |
|
140 qed_goal "split_type" thy |
146 "[| p:Sigma(A,B); \ |
141 "[| p:Sigma(A,B); \ |
147 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
142 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
148 \ |] ==> split(%x y.c(x,y), p) : C(p)" |
143 \ |] ==> split(%x y.c(x,y), p) : C(p)" |
149 (fn major::prems=> |
144 (fn major::prems=> |
150 [ (rtac (major RS SigmaE) 1), |
145 [ (rtac (major RS SigmaE) 1), |
151 (asm_simp_tac (pair_ss addsimps (split::prems)) 1) ]); |
146 (asm_simp_tac (!simpset addsimps prems) 1) ]); |
152 |
147 |
153 goalw ZF.thy [split_def] |
148 goalw thy [split_def] |
154 "!!u. u: A*B ==> \ |
149 "!!u. u: A*B ==> \ |
155 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
150 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
156 by (etac SigmaE 1); |
151 by (Auto_tac()); |
157 by (asm_simp_tac pair_ss 1); |
|
158 by (fast_tac pair_cs 1); |
|
159 qed "expand_split"; |
152 qed "expand_split"; |
160 |
153 |
161 |
154 |
162 (*** split for predicates: result type o ***) |
155 (*** split for predicates: result type o ***) |
163 |
156 |
164 goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)"; |
157 goalw thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)"; |
165 by (asm_simp_tac pair_ss 1); |
158 by (Asm_simp_tac 1); |
166 qed "splitI"; |
159 qed "splitI"; |
167 |
160 |
168 val major::sigma::prems = goalw ZF.thy [split_def] |
161 val major::sigma::prems = goalw thy [split_def] |
169 "[| split(R,z); z:Sigma(A,B); \ |
162 "[| split(R,z); z:Sigma(A,B); \ |
170 \ !!x y. [| z = <x,y>; R(x,y) |] ==> P \ |
163 \ !!x y. [| z = <x,y>; R(x,y) |] ==> P \ |
171 \ |] ==> P"; |
164 \ |] ==> P"; |
172 by (rtac (sigma RS SigmaE) 1); |
165 by (rtac (sigma RS SigmaE) 1); |
173 by (cut_facts_tac [major] 1); |
166 by (cut_facts_tac [major] 1); |
174 by (asm_full_simp_tac (pair_ss addsimps prems) 1); |
167 by (REPEAT (ares_tac prems 1)); |
|
168 by (Asm_full_simp_tac 1); |
175 qed "splitE"; |
169 qed "splitE"; |
176 |
170 |
177 goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)"; |
171 goalw thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)"; |
178 by (asm_full_simp_tac pair_ss 1); |
172 by (Full_simp_tac 1); |
179 qed "splitD"; |
173 qed "splitD"; |
180 |
174 |
181 |
175 |
182 (*** Basic simplification for ZF; see simpdata.ML for full version ***) |
|
183 |
176 |
184 fun prove_fun s = |
|
185 (writeln s; prove_goal ZF.thy s |
|
186 (fn prems => [ (cut_facts_tac prems 1), |
|
187 (fast_tac (pair_cs addSIs [equalityI]) 1) ])); |
|
188 |
|
189 (*INCLUDED IN ZF_ss*) |
|
190 val mem_simps = map prove_fun |
|
191 [ "a : 0 <-> False", |
|
192 "a : A Un B <-> a:A | a:B", |
|
193 "a : A Int B <-> a:A & a:B", |
|
194 "a : A-B <-> a:A & ~a:B", |
|
195 "<a,b>: Sigma(A,B) <-> a:A & b:B(a)", |
|
196 "a : Collect(A,P) <-> a:A & P(a)" ]; |
|
197 |
|
198 goal ZF.thy "{x.x:A} = A"; |
|
199 by (fast_tac (pair_cs addSIs [equalityI]) 1); |
|
200 qed "triv_RepFun"; |
|
201 |
|
202 (*INCLUDED: should be? And what about cons(a,b)?*) |
|
203 val bquant_simps = map prove_fun |
|
204 [ "(ALL x:0.P(x)) <-> True", |
|
205 "(EX x:0.P(x)) <-> False", |
|
206 "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))", |
|
207 "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))", |
|
208 "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))", |
|
209 "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))" ]; |
|
210 |
|
211 val Collect_simps = map prove_fun |
|
212 [ "{x:0. P(x)} = 0", |
|
213 "{x:A. False} = 0", |
|
214 "{x:A. True} = A", |
|
215 "RepFun(0,f) = 0", |
|
216 "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))", |
|
217 "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))" ]; |
|
218 |
|
219 val UnInt_simps = map prove_fun |
|
220 [ "0 Un A = A", "A Un 0 = A", |
|
221 "0 Int A = 0", "A Int 0 = 0", |
|
222 "0-A = 0", "A-0 = A", |
|
223 "Union(0) = 0", |
|
224 "Union(cons(b,A)) = b Un Union(A)", |
|
225 "Inter({b}) = b"]; |
|
226 |
|