author | paulson |
Fri, 03 Jan 1997 15:01:55 +0100 | |
changeset 2469 | b50b8c0eec01 |
parent 1609 | 5324067d993f |
child 2493 | bdeb5024353a |
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 |
||
2469 | 24 |
qed_goalw "Upair_iff" thy [Upair_def] |
0 | 25 |
"c : Upair(a,b) <-> (c=a | c=b)" |
2469 | 26 |
(fn _ => [ (fast_tac (!claset addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]); |
27 |
||
28 |
Addsimps [Upair_iff]; |
|
0 | 29 |
|
2469 | 30 |
qed_goal "UpairI1" thy "a : Upair(a,b)" |
31 |
(fn _ => [ Simp_tac 1 ]); |
|
0 | 32 |
|
2469 | 33 |
qed_goal "UpairI2" thy "b : Upair(a,b)" |
34 |
(fn _ => [ Simp_tac 1 ]); |
|
0 | 35 |
|
2469 | 36 |
qed_goal "UpairE" thy |
0 | 37 |
"[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P" |
38 |
(fn major::prems=> |
|
2469 | 39 |
[ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1), |
0 | 40 |
(REPEAT (eresolve_tac prems 1)) ]); |
41 |
||
2469 | 42 |
(*UpairI1/2 should become UpairCI?*) |
43 |
AddSIs [UpairI1,UpairI2]; |
|
44 |
AddSEs [UpairE]; |
|
45 |
||
0 | 46 |
(*** Rules for binary union -- Un -- defined via Upair ***) |
47 |
||
2469 | 48 |
qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)" |
49 |
(fn _ => [ Fast_tac 1 ]); |
|
50 |
||
51 |
Addsimps [Un_iff]; |
|
0 | 52 |
|
2469 | 53 |
qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B" |
54 |
(fn _ => [ Asm_simp_tac 1 ]); |
|
0 | 55 |
|
2469 | 56 |
qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B" |
57 |
(fn _ => [ Asm_simp_tac 1 ]); |
|
58 |
||
59 |
qed_goal "UnE" thy |
|
0 | 60 |
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
61 |
(fn major::prems=> |
|
2469 | 62 |
[ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1), |
63 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
0 | 64 |
|
572 | 65 |
(*Stronger version of the rule above*) |
2469 | 66 |
qed_goal "UnE'" thy |
572 | 67 |
"[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P" |
68 |
(fn major::prems => |
|
69 |
[(rtac (major RS UnE) 1), |
|
70 |
(eresolve_tac prems 1), |
|
71 |
(rtac classical 1), |
|
72 |
(eresolve_tac prems 1), |
|
73 |
(swap_res_tac prems 1), |
|
74 |
(etac notnotD 1)]); |
|
75 |
||
2469 | 76 |
(*Classical introduction rule: no commitment to A vs B*) |
77 |
qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B" |
|
78 |
(fn prems=> |
|
79 |
[ Simp_tac 1, fast_tac (!claset addIs prems) 1 ]); |
|
0 | 80 |
|
2469 | 81 |
AddSIs [UnCI]; |
82 |
AddSEs [UnE]; |
|
0 | 83 |
|
84 |
||
85 |
(*** Rules for small intersection -- Int -- defined via Upair ***) |
|
86 |
||
2469 | 87 |
qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)" |
88 |
(fn _ => [ Fast_tac 1 ]); |
|
89 |
||
90 |
Addsimps [Int_iff]; |
|
91 |
||
92 |
qed_goal "IntI" thy "!!c. [| c : A; c : B |] ==> c : A Int B" |
|
93 |
(fn _ => [ Asm_simp_tac 1 ]); |
|
0 | 94 |
|
2469 | 95 |
qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A" |
96 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
|
0 | 97 |
|
2469 | 98 |
qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B" |
99 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
|
0 | 100 |
|
2469 | 101 |
qed_goal "IntE" thy |
0 | 102 |
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" |
103 |
(fn prems=> |
|
104 |
[ (resolve_tac prems 1), |
|
105 |
(REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]); |
|
106 |
||
2469 | 107 |
AddSIs [IntI]; |
108 |
AddSEs [IntE]; |
|
0 | 109 |
|
110 |
(*** Rules for set difference -- defined via Upair ***) |
|
111 |
||
2469 | 112 |
qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)" |
113 |
(fn _ => [ Fast_tac 1 ]); |
|
114 |
||
115 |
Addsimps [Diff_iff]; |
|
116 |
||
117 |
qed_goal "DiffI" thy "!!c. [| c : A; c ~: B |] ==> c : A - B" |
|
118 |
(fn _ => [ Asm_simp_tac 1 ]); |
|
0 | 119 |
|
2469 | 120 |
qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A" |
121 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
|
0 | 122 |
|
2469 | 123 |
qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B" |
124 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
|
0 | 125 |
|
2469 | 126 |
qed_goal "DiffE" thy |
37 | 127 |
"[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
0 | 128 |
(fn prems=> |
129 |
[ (resolve_tac prems 1), |
|
485 | 130 |
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]); |
0 | 131 |
|
2469 | 132 |
AddSIs [DiffI]; |
133 |
AddSEs [DiffE]; |
|
0 | 134 |
|
135 |
(*** Rules for cons -- defined via Un and Upair ***) |
|
136 |
||
2469 | 137 |
qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)" |
138 |
(fn _ => [ Fast_tac 1 ]); |
|
139 |
||
140 |
Addsimps [cons_iff]; |
|
0 | 141 |
|
2469 | 142 |
qed_goal "consI1" thy "a : cons(a,B)" |
143 |
(fn _ => [ Simp_tac 1 ]); |
|
144 |
||
145 |
Addsimps [consI1]; |
|
0 | 146 |
|
2469 | 147 |
qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)" |
148 |
(fn _ => [ Asm_simp_tac 1 ]); |
|
149 |
||
150 |
qed_goal "consE" thy |
|
0 | 151 |
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P" |
152 |
(fn major::prems=> |
|
2469 | 153 |
[ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1), |
0 | 154 |
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]); |
155 |
||
572 | 156 |
(*Stronger version of the rule above*) |
2469 | 157 |
qed_goal "consE'" thy |
572 | 158 |
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P" |
159 |
(fn major::prems => |
|
160 |
[(rtac (major RS consE) 1), |
|
161 |
(eresolve_tac prems 1), |
|
162 |
(rtac classical 1), |
|
163 |
(eresolve_tac prems 1), |
|
164 |
(swap_res_tac prems 1), |
|
165 |
(etac notnotD 1)]); |
|
166 |
||
2469 | 167 |
(*Classical introduction rule*) |
168 |
qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)" |
|
169 |
(fn prems=> |
|
170 |
[ Simp_tac 1, fast_tac (!claset addIs prems) 1 ]); |
|
0 | 171 |
|
2469 | 172 |
AddSIs [consCI]; |
173 |
AddSEs [consE]; |
|
0 | 174 |
|
2469 | 175 |
qed_goal "cons_not_0" thy "cons(a,B) ~= 0" |
176 |
(fn _ => [ (fast_tac (!claset addEs [equalityE]) 1) ]); |
|
1609 | 177 |
|
2469 | 178 |
bind_thm ("cons_neq_0", cons_not_0 RS notE); |
179 |
||
180 |
Addsimps [cons_not_0, cons_not_0 RS not_sym]; |
|
181 |
||
1609 | 182 |
|
0 | 183 |
(*** Singletons - using cons ***) |
184 |
||
2469 | 185 |
qed_goal "singleton_iff" thy "a : {b} <-> a=b" |
186 |
(fn _ => [ Simp_tac 1 ]); |
|
187 |
||
188 |
qed_goal "singletonI" thy "a : {a}" |
|
0 | 189 |
(fn _=> [ (rtac consI1 1) ]); |
190 |
||
2469 | 191 |
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1)); |
0 | 192 |
|
2469 | 193 |
AddSIs [singletonI]; |
194 |
AddSEs [singletonE]; |
|
0 | 195 |
|
196 |
(*** Rules for Descriptions ***) |
|
197 |
||
2469 | 198 |
qed_goalw "the_equality" thy [the_def] |
0 | 199 |
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" |
738 | 200 |
(fn [pa,eq] => |
2469 | 201 |
[ (fast_tac (!claset addSIs [pa] addIs [equalityI] |
202 |
addEs [eq RS subst]) 1) ]); |
|
0 | 203 |
|
204 |
(* Only use this if you already know EX!x. P(x) *) |
|
2469 | 205 |
qed_goal "the_equality2" thy |
673 | 206 |
"!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" |
207 |
(fn _ => |
|
2469 | 208 |
[ (deepen_tac (!claset addSIs [the_equality]) 1 1) ]); |
0 | 209 |
|
2469 | 210 |
qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))" |
0 | 211 |
(fn [major]=> |
212 |
[ (rtac (major RS ex1E) 1), |
|
213 |
(resolve_tac [major RS the_equality2 RS ssubst] 1), |
|
214 |
(REPEAT (assume_tac 1)) ]); |
|
215 |
||
686 | 216 |
(*Easier to apply than theI: conclusion has only one occurrence of P*) |
2469 | 217 |
qed_goal "theI2" thy |
686 | 218 |
"[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))" |
219 |
(fn prems => [ resolve_tac prems 1, |
|
1461 | 220 |
rtac theI 1, |
221 |
resolve_tac prems 1 ]); |
|
686 | 222 |
|
435 | 223 |
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then |
224 |
(THE x.P(x)) rewrites to (THE x. Q(x)) *) |
|
225 |
||
226 |
(*If it's "undefined", it's zero!*) |
|
2469 | 227 |
qed_goalw "the_0" thy [the_def] |
435 | 228 |
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" |
2469 | 229 |
(fn _ => [ (fast_tac (!claset addIs [equalityI] addSEs [ReplaceE]) 1) ]); |
435 | 230 |
|
0 | 231 |
|
232 |
(*** if -- a conditional expression for formulae ***) |
|
233 |
||
2469 | 234 |
goalw thy [if_def] "if(True,a,b) = a"; |
235 |
by (fast_tac (!claset addIs [the_equality]) 1); |
|
760 | 236 |
qed "if_true"; |
0 | 237 |
|
2469 | 238 |
goalw thy [if_def] "if(False,a,b) = b"; |
239 |
by (fast_tac (!claset addIs [the_equality]) 1); |
|
760 | 240 |
qed "if_false"; |
0 | 241 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
242 |
(*Never use with case splitting, or if P is known to be true or false*) |
2469 | 243 |
val prems = goalw thy [if_def] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
244 |
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)"; |
2469 | 245 |
by (simp_tac (!simpset addsimps prems addcongs [conj_cong]) 1); |
760 | 246 |
qed "if_cong"; |
0 | 247 |
|
248 |
(*Not needed for rewriting, since P would rewrite to True anyway*) |
|
2469 | 249 |
goalw thy [if_def] "!!P. P ==> if(P,a,b) = a"; |
250 |
by (fast_tac (!claset addSIs [the_equality]) 1); |
|
760 | 251 |
qed "if_P"; |
0 | 252 |
|
253 |
(*Not needed for rewriting, since P would rewrite to False anyway*) |
|
2469 | 254 |
goalw thy [if_def] "!!P. ~P ==> if(P,a,b) = b"; |
255 |
by (fast_tac (!claset addSIs [the_equality]) 1); |
|
760 | 256 |
qed "if_not_P"; |
0 | 257 |
|
2469 | 258 |
Addsimps [if_true, if_false]; |
0 | 259 |
|
2469 | 260 |
qed_goal "expand_if" thy |
0 | 261 |
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
437 | 262 |
(fn _=> [ (excluded_middle_tac "Q" 1), |
2469 | 263 |
(Asm_simp_tac 1), |
264 |
(Asm_simp_tac 1) ]); |
|
0 | 265 |
|
2469 | 266 |
qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y" |
267 |
(fn _=> [ (simp_tac (!simpset setloop split_tac [expand_if]) 1) ]); |
|
1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
268 |
|
2469 | 269 |
qed_goal "if_type" thy |
1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
270 |
"[| 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
|
271 |
(fn prems=> [ (simp_tac |
2469 | 272 |
(!simpset addsimps prems setloop split_tac [expand_if]) 1) ]); |
0 | 273 |
|
274 |
||
275 |
(*** Foundation lemmas ***) |
|
276 |
||
437 | 277 |
(*was called mem_anti_sym*) |
2469 | 278 |
qed_goal "mem_asym" thy "!!P. [| a:b; b:a |] ==> P" |
673 | 279 |
(fn _=> |
280 |
[ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1), |
|
2469 | 281 |
REPEAT (fast_tac (!claset addSEs [equalityE]) 1) ]); |
0 | 282 |
|
437 | 283 |
(*was called mem_anti_refl*) |
2469 | 284 |
qed_goal "mem_irrefl" thy "a:a ==> P" |
285 |
(fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]); |
|
0 | 286 |
|
2469 | 287 |
(*mem_irrefl should NOT be added to default databases: |
288 |
it would be tried on most goals, making proofs slower!*) |
|
289 |
||
290 |
qed_goal "mem_not_refl" thy "a ~: a" |
|
437 | 291 |
(K [ (rtac notI 1), (etac mem_irrefl 1) ]); |
0 | 292 |
|
435 | 293 |
(*Good for proving inequalities by rewriting*) |
2469 | 294 |
qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A" |
295 |
(fn _=> [ fast_tac (!claset addSEs [mem_irrefl]) 1 ]); |
|
435 | 296 |
|
0 | 297 |
(*** Rules for succ ***) |
298 |
||
2469 | 299 |
qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j" |
300 |
(fn _ => [ Fast_tac 1 ]); |
|
301 |
||
302 |
qed_goalw "succI1" thy [succ_def] "i : succ(i)" |
|
0 | 303 |
(fn _=> [ (rtac consI1 1) ]); |
304 |
||
2469 | 305 |
Addsimps [succI1]; |
306 |
||
307 |
qed_goalw "succI2" thy [succ_def] |
|
0 | 308 |
"i : j ==> i : succ(j)" |
309 |
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]); |
|
310 |
||
2469 | 311 |
qed_goalw "succE" thy [succ_def] |
0 | 312 |
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P" |
313 |
(fn major::prems=> |
|
314 |
[ (rtac (major RS consE) 1), |
|
315 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
316 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
317 |
(*Classical introduction rule*) |
2469 | 318 |
qed_goal "succCI" 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
|
319 |
(fn [prem]=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
320 |
[ (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
|
321 |
(etac prem 1) ]); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
322 |
|
2469 | 323 |
AddSIs [succCI]; |
324 |
AddSEs [succE]; |
|
325 |
||
326 |
qed_goal "succ_not_0" thy "succ(n) ~= 0" |
|
327 |
(fn _=> [ (fast_tac (!claset addSEs [equalityE]) 1) ]); |
|
0 | 328 |
|
2469 | 329 |
bind_thm ("succ_neq_0", succ_not_0 RS notE); |
330 |
||
331 |
Addsimps [succ_not_0, succ_not_0 RS not_sym]; |
|
332 |
AddSEs [succ_neq_0, sym RS succ_neq_0]; |
|
333 |
||
0 | 334 |
|
335 |
(* succ(c) <= B ==> c : B *) |
|
336 |
val succ_subsetD = succI1 RSN (2,subsetD); |
|
337 |
||
1609 | 338 |
(* succ(b) ~= b *) |
339 |
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym); |
|
340 |
||
341 |
||
2469 | 342 |
qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n" |
343 |
(fn _=> [ (fast_tac (!claset addEs [mem_asym, equalityE]) 1) ]); |
|
0 | 344 |
|
2469 | 345 |
bind_thm ("succ_inject", succ_inject_iff RS iffD1); |
0 | 346 |
|
2469 | 347 |
Addsimps [succ_inject_iff]; |
348 |
AddSDs [succ_inject]; |
|
0 | 349 |
|
2469 | 350 |
|
351 |
use"simpdata.ML"; |