author | paulson |
Thu, 21 Mar 1996 13:02:26 +0100 | |
changeset 1601 | 0ef6ea27ab15 |
parent 1461 | 6bcb44e4d6e5 |
child 1609 | 5324067d993f |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/upair |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
UNORDERED pairs in Zermelo-Fraenkel Set Theory |
|
7 |
||
8 |
Observe the order of dependence: |
|
9 |
Upair is defined in terms of Replace |
|
10 |
Un is defined in terms of Upair and Union (similarly for Int) |
|
11 |
cons is defined in terms of Upair and Un |
|
12 |
Ordered pairs and descriptions are defined using cons ("set notation") |
|
13 |
*) |
|
14 |
||
15 |
(*** Lemmas about power sets ***) |
|
16 |
||
1461 | 17 |
val Pow_bottom = empty_subsetI RS PowI; (* 0 : Pow(B) *) |
18 |
val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) |
|
19 |
val Pow_neq_0 = Pow_top RSN (2,equals0D); (* Pow(a)=0 ==> P *) |
|
0 | 20 |
|
21 |
||
22 |
(*** Unordered pairs - Upair ***) |
|
23 |
||
760 | 24 |
qed_goalw "pairing" ZF.thy [Upair_def] |
0 | 25 |
"c : Upair(a,b) <-> (c=a | c=b)" |
26 |
(fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]); |
|
27 |
||
760 | 28 |
qed_goal "UpairI1" ZF.thy "a : Upair(a,b)" |
0 | 29 |
(fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]); |
30 |
||
760 | 31 |
qed_goal "UpairI2" ZF.thy "b : Upair(a,b)" |
0 | 32 |
(fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]); |
33 |
||
760 | 34 |
qed_goal "UpairE" ZF.thy |
0 | 35 |
"[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P" |
36 |
(fn major::prems=> |
|
37 |
[ (rtac (major RS (pairing RS iffD1 RS disjE)) 1), |
|
38 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
39 |
||
40 |
(*** Rules for binary union -- Un -- defined via Upair ***) |
|
41 |
||
760 | 42 |
qed_goalw "UnI1" ZF.thy [Un_def] "c : A ==> c : A Un B" |
0 | 43 |
(fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]); |
44 |
||
760 | 45 |
qed_goalw "UnI2" ZF.thy [Un_def] "c : B ==> c : A Un B" |
0 | 46 |
(fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]); |
47 |
||
760 | 48 |
qed_goalw "UnE" ZF.thy [Un_def] |
0 | 49 |
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
50 |
(fn major::prems=> |
|
51 |
[ (rtac (major RS UnionE) 1), |
|
52 |
(etac UpairE 1), |
|
53 |
(REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]); |
|
54 |
||
572 | 55 |
(*Stronger version of the rule above*) |
760 | 56 |
qed_goal "UnE'" ZF.thy |
572 | 57 |
"[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P" |
58 |
(fn major::prems => |
|
59 |
[(rtac (major RS UnE) 1), |
|
60 |
(eresolve_tac prems 1), |
|
61 |
(rtac classical 1), |
|
62 |
(eresolve_tac prems 1), |
|
63 |
(swap_res_tac prems 1), |
|
64 |
(etac notnotD 1)]); |
|
65 |
||
760 | 66 |
qed_goal "Un_iff" ZF.thy "c : A Un B <-> (c:A | c:B)" |
0 | 67 |
(fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]); |
68 |
||
69 |
(*Classical introduction rule: no commitment to A vs B*) |
|
760 | 70 |
qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B" |
0 | 71 |
(fn [prem]=> |
72 |
[ (rtac (disjCI RS (Un_iff RS iffD2)) 1), |
|
73 |
(etac prem 1) ]); |
|
74 |
||
75 |
||
76 |
(*** Rules for small intersection -- Int -- defined via Upair ***) |
|
77 |
||
760 | 78 |
qed_goalw "IntI" ZF.thy [Int_def] |
0 | 79 |
"[| c : A; c : B |] ==> c : A Int B" |
80 |
(fn prems=> |
|
81 |
[ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1 |
|
82 |
ORELSE eresolve_tac [UpairE, ssubst] 1)) ]); |
|
83 |
||
760 | 84 |
qed_goalw "IntD1" ZF.thy [Int_def] "c : A Int B ==> c : A" |
0 | 85 |
(fn [major]=> |
86 |
[ (rtac (UpairI1 RS (major RS InterD)) 1) ]); |
|
87 |
||
760 | 88 |
qed_goalw "IntD2" ZF.thy [Int_def] "c : A Int B ==> c : B" |
0 | 89 |
(fn [major]=> |
90 |
[ (rtac (UpairI2 RS (major RS InterD)) 1) ]); |
|
91 |
||
760 | 92 |
qed_goal "IntE" ZF.thy |
0 | 93 |
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" |
94 |
(fn prems=> |
|
95 |
[ (resolve_tac prems 1), |
|
96 |
(REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]); |
|
97 |
||
760 | 98 |
qed_goal "Int_iff" ZF.thy "c : A Int B <-> (c:A & c:B)" |
0 | 99 |
(fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]); |
100 |
||
101 |
||
102 |
(*** Rules for set difference -- defined via Upair ***) |
|
103 |
||
760 | 104 |
qed_goalw "DiffI" ZF.thy [Diff_def] |
37 | 105 |
"[| c : A; c ~: B |] ==> c : A - B" |
0 | 106 |
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]); |
107 |
||
760 | 108 |
qed_goalw "DiffD1" ZF.thy [Diff_def] |
0 | 109 |
"c : A - B ==> c : A" |
110 |
(fn [major]=> [ (rtac (major RS CollectD1) 1) ]); |
|
111 |
||
760 | 112 |
qed_goalw "DiffD2" ZF.thy [Diff_def] |
485 | 113 |
"c : A - B ==> c ~: B" |
114 |
(fn [major]=> [ (rtac (major RS CollectD2) 1) ]); |
|
0 | 115 |
|
760 | 116 |
qed_goal "DiffE" ZF.thy |
37 | 117 |
"[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
0 | 118 |
(fn prems=> |
119 |
[ (resolve_tac prems 1), |
|
485 | 120 |
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]); |
0 | 121 |
|
760 | 122 |
qed_goal "Diff_iff" ZF.thy "c : A-B <-> (c:A & c~:B)" |
0 | 123 |
(fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]); |
124 |
||
125 |
(*** Rules for cons -- defined via Un and Upair ***) |
|
126 |
||
760 | 127 |
qed_goalw "consI1" ZF.thy [cons_def] "a : cons(a,B)" |
0 | 128 |
(fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]); |
129 |
||
760 | 130 |
qed_goalw "consI2" ZF.thy [cons_def] "a : B ==> a : cons(b,B)" |
0 | 131 |
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]); |
132 |
||
760 | 133 |
qed_goalw "consE" ZF.thy [cons_def] |
0 | 134 |
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P" |
135 |
(fn major::prems=> |
|
136 |
[ (rtac (major RS UnE) 1), |
|
137 |
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]); |
|
138 |
||
572 | 139 |
(*Stronger version of the rule above*) |
760 | 140 |
qed_goal "consE'" ZF.thy |
572 | 141 |
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P" |
142 |
(fn major::prems => |
|
143 |
[(rtac (major RS consE) 1), |
|
144 |
(eresolve_tac prems 1), |
|
145 |
(rtac classical 1), |
|
146 |
(eresolve_tac prems 1), |
|
147 |
(swap_res_tac prems 1), |
|
148 |
(etac notnotD 1)]); |
|
149 |
||
760 | 150 |
qed_goal "cons_iff" ZF.thy "a : cons(b,A) <-> (a=b | a:A)" |
0 | 151 |
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]); |
152 |
||
153 |
(*Classical introduction rule*) |
|
760 | 154 |
qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)" |
0 | 155 |
(fn [prem]=> |
156 |
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1), |
|
157 |
(etac prem 1) ]); |
|
158 |
||
159 |
(*** Singletons - using cons ***) |
|
160 |
||
760 | 161 |
qed_goal "singletonI" ZF.thy "a : {a}" |
0 | 162 |
(fn _=> [ (rtac consI1 1) ]); |
163 |
||
760 | 164 |
qed_goal "singletonE" ZF.thy "[| a: {b}; a=b ==> P |] ==> P" |
0 | 165 |
(fn major::prems=> |
166 |
[ (rtac (major RS consE) 1), |
|
167 |
(REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]); |
|
168 |
||
834 | 169 |
qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b" |
170 |
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1] addSEs [consE]) 1) ]); |
|
171 |
||
0 | 172 |
|
173 |
(*** Rules for Descriptions ***) |
|
174 |
||
760 | 175 |
qed_goalw "the_equality" ZF.thy [the_def] |
0 | 176 |
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" |
738 | 177 |
(fn [pa,eq] => |
178 |
[ (fast_tac (lemmas_cs addSIs [singletonI,pa] addIs [equalityI] |
|
1461 | 179 |
addEs [eq RS subst]) 1) ]); |
0 | 180 |
|
181 |
(* Only use this if you already know EX!x. P(x) *) |
|
760 | 182 |
qed_goal "the_equality2" ZF.thy |
673 | 183 |
"!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" |
184 |
(fn _ => |
|
185 |
[ (deepen_tac (lemmas_cs addSIs [the_equality]) 1 1) ]); |
|
0 | 186 |
|
760 | 187 |
qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))" |
0 | 188 |
(fn [major]=> |
189 |
[ (rtac (major RS ex1E) 1), |
|
190 |
(resolve_tac [major RS the_equality2 RS ssubst] 1), |
|
191 |
(REPEAT (assume_tac 1)) ]); |
|
192 |
||
686 | 193 |
(*Easier to apply than theI: conclusion has only one occurrence of P*) |
760 | 194 |
qed_goal "theI2" ZF.thy |
686 | 195 |
"[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))" |
196 |
(fn prems => [ resolve_tac prems 1, |
|
1461 | 197 |
rtac theI 1, |
198 |
resolve_tac prems 1 ]); |
|
686 | 199 |
|
435 | 200 |
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then |
201 |
(THE x.P(x)) rewrites to (THE x. Q(x)) *) |
|
202 |
||
203 |
(*If it's "undefined", it's zero!*) |
|
760 | 204 |
qed_goalw "the_0" ZF.thy [the_def] |
435 | 205 |
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" |
206 |
(fn _ => |
|
485 | 207 |
[ (fast_tac (lemmas_cs addIs [equalityI] addSEs [ReplaceE]) 1) ]); |
435 | 208 |
|
0 | 209 |
|
210 |
(*** if -- a conditional expression for formulae ***) |
|
211 |
||
212 |
goalw ZF.thy [if_def] "if(True,a,b) = a"; |
|
213 |
by (fast_tac (lemmas_cs addIs [the_equality]) 1); |
|
760 | 214 |
qed "if_true"; |
0 | 215 |
|
216 |
goalw ZF.thy [if_def] "if(False,a,b) = b"; |
|
217 |
by (fast_tac (lemmas_cs addIs [the_equality]) 1); |
|
760 | 218 |
qed "if_false"; |
0 | 219 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
220 |
(*Never use with case splitting, or if P is known to be true or false*) |
0 | 221 |
val prems = goalw ZF.thy [if_def] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
222 |
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)"; |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
223 |
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1); |
760 | 224 |
qed "if_cong"; |
0 | 225 |
|
226 |
(*Not needed for rewriting, since P would rewrite to True anyway*) |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
227 |
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a"; |
0 | 228 |
by (fast_tac (lemmas_cs addSIs [the_equality]) 1); |
760 | 229 |
qed "if_P"; |
0 | 230 |
|
231 |
(*Not needed for rewriting, since P would rewrite to False anyway*) |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
232 |
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b"; |
0 | 233 |
by (fast_tac (lemmas_cs addSIs [the_equality]) 1); |
760 | 234 |
qed "if_not_P"; |
0 | 235 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
236 |
val if_ss = FOL_ss addsimps [if_true,if_false]; |
0 | 237 |
|
760 | 238 |
qed_goal "expand_if" ZF.thy |
0 | 239 |
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
437 | 240 |
(fn _=> [ (excluded_middle_tac "Q" 1), |
1461 | 241 |
(asm_simp_tac if_ss 1), |
242 |
(asm_simp_tac if_ss 1) ]); |
|
0 | 243 |
|
1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
244 |
qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y" |
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
245 |
(fn _=> [ (simp_tac (if_ss setloop split_tac [expand_if]) 1) ]); |
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
246 |
|
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
247 |
qed_goal "if_type" ZF.thy |
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
248 |
"[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A" |
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
249 |
(fn prems=> [ (simp_tac |
1461 | 250 |
(if_ss addsimps prems setloop split_tac [expand_if]) 1) ]); |
0 | 251 |
|
252 |
||
253 |
(*** Foundation lemmas ***) |
|
254 |
||
437 | 255 |
(*was called mem_anti_sym*) |
760 | 256 |
qed_goal "mem_asym" ZF.thy "!!P. [| a:b; b:a |] ==> P" |
673 | 257 |
(fn _=> |
258 |
[ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1), |
|
0 | 259 |
(etac equals0D 1), |
260 |
(rtac consI1 1), |
|
673 | 261 |
(fast_tac (lemmas_cs addIs [consI1,consI2] |
1461 | 262 |
addSEs [consE,equalityE]) 1) ]); |
0 | 263 |
|
437 | 264 |
(*was called mem_anti_refl*) |
760 | 265 |
qed_goal "mem_irrefl" ZF.thy "a:a ==> P" |
437 | 266 |
(fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]); |
0 | 267 |
|
760 | 268 |
qed_goal "mem_not_refl" ZF.thy "a ~: a" |
437 | 269 |
(K [ (rtac notI 1), (etac mem_irrefl 1) ]); |
0 | 270 |
|
435 | 271 |
(*Good for proving inequalities by rewriting*) |
760 | 272 |
qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A" |
437 | 273 |
(fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]); |
435 | 274 |
|
0 | 275 |
(*** Rules for succ ***) |
276 |
||
760 | 277 |
qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)" |
0 | 278 |
(fn _=> [ (rtac consI1 1) ]); |
279 |
||
760 | 280 |
qed_goalw "succI2" ZF.thy [succ_def] |
0 | 281 |
"i : j ==> i : succ(j)" |
282 |
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]); |
|
283 |
||
760 | 284 |
qed_goalw "succE" ZF.thy [succ_def] |
0 | 285 |
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P" |
286 |
(fn major::prems=> |
|
287 |
[ (rtac (major RS consE) 1), |
|
288 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
289 |
||
760 | 290 |
qed_goal "succ_iff" ZF.thy "i : succ(j) <-> i=j | i:j" |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
291 |
(fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
292 |
|
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
293 |
(*Classical introduction rule*) |
760 | 294 |
qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)" |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
295 |
(fn [prem]=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
296 |
[ (rtac (disjCI RS (succ_iff RS iffD2)) 1), |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
297 |
(etac prem 1) ]); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
298 |
|
760 | 299 |
qed_goal "succ_neq_0" ZF.thy "succ(n)=0 ==> P" |
0 | 300 |
(fn [major]=> |
301 |
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1), |
|
302 |
(rtac succI1 1) ]); |
|
303 |
||
304 |
(*Useful for rewriting*) |
|
760 | 305 |
qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0" |
0 | 306 |
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]); |
307 |
||
308 |
(* succ(c) <= B ==> c : B *) |
|
309 |
val succ_subsetD = succI1 RSN (2,subsetD); |
|
310 |
||
760 | 311 |
qed_goal "succ_inject" ZF.thy "!!m n. succ(m) = succ(n) ==> m=n" |
673 | 312 |
(fn _ => |
313 |
[ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD] |
|
314 |
addEs [mem_asym]) 1) ]); |
|
0 | 315 |
|
760 | 316 |
qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n" |
0 | 317 |
(fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]); |
318 |
||
985
2e50c5124ca3
Added comment about why mem_irrefl should not be a safeE.
lcp
parents:
834
diff
changeset
|
319 |
(*UpairI1/2 should become UpairCI? |
2e50c5124ca3
Added comment about why mem_irrefl should not be a safeE.
lcp
parents:
834
diff
changeset
|
320 |
mem_irrefl should NOT be added as an elim-rule here; |
2e50c5124ca3
Added comment about why mem_irrefl should not be a safeE.
lcp
parents:
834
diff
changeset
|
321 |
it would be tried on most goals, making proof slower!*) |
0 | 322 |
val upair_cs = lemmas_cs |
323 |
addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2] |
|
324 |
addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE]; |
|
325 |