author  wenzelm 
Wed, 05 Dec 2001 03:07:44 +0100  
changeset 12372  cd3a09c7dac9 
parent 11589  9a6d4511bb3c 
permissions  rwrr 
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 ZermeloFraenkel 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 

9907  17 
bind_thm ("Pow_bottom", empty_subsetI RS PowI); (* 0 : Pow(B) *) 
18 
bind_thm ("Pow_top", subset_refl RS PowI); (* A : Pow(A) *) 

0  19 

20 

21 
(*** Unordered pairs  Upair ***) 

22 

9211  23 
Goalw [Upair_def] "c : Upair(a,b) <> (c=a  c=b)"; 
24 
by (Blast_tac 1) ; 

25 
qed "Upair_iff"; 

2469  26 

27 
Addsimps [Upair_iff]; 

0  28 

9180  29 
Goal "a : Upair(a,b)"; 
30 
by (Simp_tac 1); 

31 
qed "UpairI1"; 

0  32 

9180  33 
Goal "b : Upair(a,b)"; 
34 
by (Simp_tac 1); 

35 
qed "UpairI2"; 

36 

37 
val major::prems= Goal 

38 
"[ a : Upair(b,c); a=b ==> P; a=c ==> P ] ==> P"; 

39 
by (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1); 

40 
by (REPEAT (eresolve_tac prems 1)) ; 

41 
qed "UpairE"; 

0  42 

2469  43 
AddSIs [UpairI1,UpairI2]; 
44 
AddSEs [UpairE]; 

45 

0  46 
(*** Rules for binary union  Un  defined via Upair ***) 
47 

9211  48 
Goalw [Un_def] "c : A Un B <> (c:A  c:B)"; 
49 
by (Blast_tac 1); 

50 
qed "Un_iff"; 

2469  51 

52 
Addsimps [Un_iff]; 

0  53 

9180  54 
Goal "c : A ==> c : A Un B"; 
55 
by (Asm_simp_tac 1); 

56 
qed "UnI1"; 

2469  57 

9180  58 
Goal "c : B ==> c : A Un B"; 
59 
by (Asm_simp_tac 1); 

60 
qed "UnI2"; 

61 

62 
val major::prems= Goal 

63 
"[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P"; 

64 
by (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1); 

65 
by (REPEAT (eresolve_tac prems 1)) ; 

66 
qed "UnE"; 

0  67 

572  68 
(*Stronger version of the rule above*) 
9180  69 
val major::prems = Goal 
70 
"[ c : A Un B; c:A ==> P; [ c:B; c~:A ] ==> P ] ==> P"; 

71 
by (rtac (major RS UnE) 1); 

72 
by (eresolve_tac prems 1); 

73 
by (rtac classical 1); 

74 
by (eresolve_tac prems 1); 

75 
by (swap_res_tac prems 1); 

76 
by (etac notnotD 1); 

77 
qed "UnE'"; 

572  78 

2469  79 
(*Classical introduction rule: no commitment to A vs B*) 
9180  80 
val prems = Goal "(c ~: B ==> c : A) ==> c : A Un B"; 
81 
by (Simp_tac 1); 

82 
by (blast_tac (claset() addSIs prems) 1); 

83 
qed "UnCI"; 

0  84 

2469  85 
AddSIs [UnCI]; 
86 
AddSEs [UnE]; 

0  87 

88 

89 
(*** Rules for small intersection  Int  defined via Upair ***) 

90 

9211  91 
Goalw [Int_def] "c : A Int B <> (c:A & c:B)"; 
92 
by (Blast_tac 1); 

93 
qed "Int_iff"; 

2469  94 

95 
Addsimps [Int_iff]; 

96 

9180  97 
Goal "[ c : A; c : B ] ==> c : A Int B"; 
98 
by (Asm_simp_tac 1); 

99 
qed "IntI"; 

0  100 

9180  101 
Goal "c : A Int B ==> c : A"; 
102 
by (Asm_full_simp_tac 1); 

103 
qed "IntD1"; 

0  104 

9180  105 
Goal "c : A Int B ==> c : B"; 
106 
by (Asm_full_simp_tac 1); 

107 
qed "IntD2"; 

0  108 

9180  109 
val prems = Goal "[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P"; 
110 
by (resolve_tac prems 1); 

111 
by (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ; 

112 
qed "IntE"; 

0  113 

2469  114 
AddSIs [IntI]; 
115 
AddSEs [IntE]; 

0  116 

117 
(*** Rules for set difference  defined via Upair ***) 

118 

9211  119 
Goalw [Diff_def] "c : AB <> (c:A & c~:B)"; 
120 
by (Blast_tac 1); 

121 
qed "Diff_iff"; 

2469  122 

123 
Addsimps [Diff_iff]; 

124 

9180  125 
Goal "[ c : A; c ~: B ] ==> c : A  B"; 
126 
by (Asm_simp_tac 1); 

127 
qed "DiffI"; 

0  128 

9180  129 
Goal "c : A  B ==> c : A"; 
130 
by (Asm_full_simp_tac 1); 

131 
qed "DiffD1"; 

0  132 

9180  133 
Goal "c : A  B ==> c ~: B"; 
134 
by (Asm_full_simp_tac 1); 

135 
qed "DiffD2"; 

0  136 

9180  137 
val prems = Goal "[ c : A  B; [ c:A; c~:B ] ==> P ] ==> P"; 
138 
by (resolve_tac prems 1); 

139 
by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ; 

140 
qed "DiffE"; 

0  141 

2469  142 
AddSIs [DiffI]; 
143 
AddSEs [DiffE]; 

0  144 

145 
(*** Rules for cons  defined via Un and Upair ***) 

146 

9211  147 
Goalw [cons_def] "a : cons(b,A) <> (a=b  a:A)"; 
148 
by (Blast_tac 1); 

149 
qed "cons_iff"; 

2469  150 

151 
Addsimps [cons_iff]; 

0  152 

9180  153 
Goal "a : cons(a,B)"; 
154 
by (Simp_tac 1); 

155 
qed "consI1"; 

2469  156 

157 
Addsimps [consI1]; 

6153  158 
AddTCs [consI1]; (*risky as a typechecking rule, but solves otherwise 
159 
unconstrained goals of the form x : ?A*) 

0  160 

9180  161 
Goal "a : B ==> a : cons(b,B)"; 
162 
by (Asm_simp_tac 1); 

163 
qed "consI2"; 

2469  164 

9180  165 
val major::prems= Goal 
166 
"[ a : cons(b,A); a=b ==> P; a:A ==> P ] ==> P"; 

167 
by (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1); 

168 
by (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ; 

169 
qed "consE"; 

0  170 

572  171 
(*Stronger version of the rule above*) 
9180  172 
val major::prems = Goal 
173 
"[ a : cons(b,A); a=b ==> P; [ a:A; a~=b ] ==> P ] ==> P"; 

174 
by (rtac (major RS consE) 1); 

175 
by (eresolve_tac prems 1); 

176 
by (rtac classical 1); 

177 
by (eresolve_tac prems 1); 

178 
by (swap_res_tac prems 1); 

179 
by (etac notnotD 1); 

180 
qed "consE'"; 

572  181 

2469  182 
(*Classical introduction rule*) 
9180  183 
val prems = Goal "(a~:B ==> a=b) ==> a: cons(b,B)"; 
184 
by (Simp_tac 1); 

185 
by (blast_tac (claset() addSIs prems) 1); 

186 
qed "consCI"; 

0  187 

2469  188 
AddSIs [consCI]; 
189 
AddSEs [consE]; 

0  190 

9180  191 
Goal "cons(a,B) ~= 0"; 
192 
by (blast_tac (claset() addEs [equalityE]) 1) ; 

193 
qed "cons_not_0"; 

1609  194 

2469  195 
bind_thm ("cons_neq_0", cons_not_0 RS notE); 
196 

197 
Addsimps [cons_not_0, cons_not_0 RS not_sym]; 

198 

1609  199 

0  200 
(*** Singletons  using cons ***) 
201 

9180  202 
Goal "a : {b} <> a=b"; 
203 
by (Simp_tac 1); 

204 
qed "singleton_iff"; 

2469  205 

9180  206 
Goal "a : {a}"; 
207 
by (rtac consI1 1) ; 

208 
qed "singletonI"; 

0  209 

2469  210 
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1)); 
0  211 

2469  212 
AddSIs [singletonI]; 
213 
AddSEs [singletonE]; 

0  214 

215 
(*** Rules for Descriptions ***) 

216 

9211  217 
val [pa,eq] = Goalw [the_def] 
218 
"[ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a"; 

219 
by (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ; 

220 
qed "the_equality"; 

0  221 

5506  222 
AddIs [the_equality]; 
223 

0  224 
(* Only use this if you already know EX!x. P(x) *) 
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

225 
Goal "[ EX! x. P(x); P(a) ] ==> (THE x. P(x)) = a"; 
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

226 
by (Blast_tac 1); 
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

227 
qed "the_equality2"; 
0  228 

8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

229 
Goal "EX! x. P(x) ==> P(THE x. P(x))"; 
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

230 
by (etac ex1E 1); 
8183  231 
by (stac the_equality 1); 
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

232 
by (REPEAT (Blast_tac 1)); 
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

233 
qed "theI"; 
0  234 

435  235 
(*the_cong is no longer necessary: if (ALL y.P(y)<>Q(y)) then 
236 
(THE x.P(x)) rewrites to (THE x. Q(x)) *) 

237 

238 
(*If it's "undefined", it's zero!*) 

9180  239 
Goalw [the_def] "~ (EX! x. P(x)) ==> (THE x. P(x))=0"; 
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

240 
by (blast_tac (claset() addSEs [ReplaceE]) 1); 
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset

241 
qed "the_0"; 
0  242 

5506  243 
(*Easier to apply than theI: conclusion has only one occurrence of P*) 
244 
val prems = 

245 
Goal "[ ~ Q(0) ==> EX! x. P(x); !!x. P(x) ==> Q(x) ] ==> Q(THE x. P(x))"; 

246 
by (rtac classical 1); 

247 
by (resolve_tac prems 1); 

248 
by (rtac theI 1); 

249 
by (rtac classical 1); 

250 
by (resolve_tac prems 1); 

6163  251 
by (etac (the_0 RS subst) 1); 
252 
by (assume_tac 1); 

5506  253 
qed "theI2"; 
254 

0  255 
(*** if  a conditional expression for formulae ***) 
256 

6068  257 
Goalw [if_def] "(if True then a else b) = a"; 
5506  258 
by (Blast_tac 1); 
760  259 
qed "if_true"; 
0  260 

6068  261 
Goalw [if_def] "(if False then a else b) = b"; 
5506  262 
by (Blast_tac 1); 
760  263 
qed "if_false"; 
0  264 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

265 
(*Never use with case splitting, or if P is known to be true or false*) 
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset

266 
val prems = Goalw [if_def] 
6068  267 
"[ P<>Q; Q ==> a=c; ~Q ==> b=d ] \ 
268 
\ ==> (if P then a else b) = (if Q then c else d)"; 

4091  269 
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1); 
760  270 
qed "if_cong"; 
0  271 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9211
diff
changeset

272 
(*Prevents simplification of x and y: faster and allows the execution 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9211
diff
changeset

273 
of functional programs. NOW THE DEFAULT.*) 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9211
diff
changeset

274 
Goal "P<>Q ==> (if P then x else y) = (if Q then x else y)"; 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9211
diff
changeset

275 
by (Asm_simp_tac 1); 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9211
diff
changeset

276 
qed "if_weak_cong"; 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9211
diff
changeset

277 

0  278 
(*Not needed for rewriting, since P would rewrite to True anyway*) 
6068  279 
Goalw [if_def] "P ==> (if P then a else b) = a"; 
5506  280 
by (Blast_tac 1); 
760  281 
qed "if_P"; 
0  282 

283 
(*Not needed for rewriting, since P would rewrite to False anyway*) 

6068  284 
Goalw [if_def] "~P ==> (if P then a else b) = b"; 
5506  285 
by (Blast_tac 1); 
760  286 
qed "if_not_P"; 
0  287 

2469  288 
Addsimps [if_true, if_false]; 
0  289 

9180  290 
Goal "P(if Q then x else y) <> ((Q > P(x)) & (~Q > P(y)))"; 
291 
by (case_tac "Q" 1); 

292 
by (Asm_simp_tac 1); 

293 
by (Asm_simp_tac 1) ; 

294 
qed "split_if"; 

0  295 

3914  296 
(** Rewrite rules for boolean casesplitting: faster than 
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset

297 
addsplits[split_if] 
3914  298 
**) 
299 

8551  300 
bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if); 
301 
bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if); 

3914  302 

8551  303 
bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if); 
304 
bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if); 

3914  305 

9907  306 
bind_thms ("split_ifs", [split_if_eq1, split_if_eq2, split_if_mem1, split_if_mem2]); 
3914  307 

5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset

308 
(*Logically equivalent to split_if_mem2*) 
9180  309 
Goal "a: (if P then x else y) <> P & a:x  ~P & a:y"; 
310 
by (simp_tac (simpset() addsplits [split_if]) 1) ; 

311 
qed "if_iff"; 

1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset

312 

9180  313 
val prems = Goal 
314 
"[ P ==> a: A; ~P ==> b: A ] ==> (if P then a else b): A"; 

315 
by (simp_tac (simpset() addsimps prems addsplits [split_if]) 1) ; 

316 
qed "if_type"; 

317 

6153  318 
AddTCs [if_type]; 
0  319 

320 
(*** Foundation lemmas ***) 

321 

437  322 
(*was called mem_anti_sym*) 
9180  323 
val prems = Goal "[ a:b; ~P ==> b:a ] ==> P"; 
324 
by (rtac classical 1); 

325 
by (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1); 

326 
by (REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1)); 

327 
qed "mem_asym"; 

0  328 

437  329 
(*was called mem_anti_refl*) 
9180  330 
Goal "a:a ==> P"; 
331 
by (blast_tac (claset() addIs [mem_asym]) 1); 

332 
qed "mem_irrefl"; 

0  333 

2469  334 
(*mem_irrefl should NOT be added to default databases: 
335 
it would be tried on most goals, making proofs slower!*) 

336 

9180  337 
Goal "a ~: a"; 
338 
by (rtac notI 1); 

339 
by (etac mem_irrefl 1); 

340 
qed "mem_not_refl"; 

0  341 

435  342 
(*Good for proving inequalities by rewriting*) 
9180  343 
Goal "a:A ==> a ~= A"; 
344 
by (blast_tac (claset() addSEs [mem_irrefl]) 1); 

345 
qed "mem_imp_not_eq"; 

435  346 

0  347 
(*** Rules for succ ***) 
348 

9211  349 
Goalw [succ_def] "i : succ(j) <> i=j  i:j"; 
350 
by (Blast_tac 1); 

351 
qed "succ_iff"; 

2469  352 

9211  353 
Goalw [succ_def] "i : succ(i)"; 
354 
by (rtac consI1 1) ; 

355 
qed "succI1"; 

0  356 

2469  357 
Addsimps [succI1]; 
358 

9211  359 
Goalw [succ_def] "i : j ==> i : succ(j)"; 
360 
by (etac consI2 1) ; 

361 
qed "succI2"; 

0  362 

9211  363 
val major::prems= Goalw [succ_def] 
364 
"[ i : succ(j); i=j ==> P; i:j ==> P ] ==> P"; 

365 
by (rtac (major RS consE) 1); 

366 
by (REPEAT (eresolve_tac prems 1)) ; 

367 
qed "succE"; 

0  368 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

369 
(*Classical introduction rule*) 
9180  370 
val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)"; 
371 
by (rtac (disjCI RS (succ_iff RS iffD2)) 1); 

372 
by (etac prem 1) ; 

373 
qed "succCI"; 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

374 

2469  375 
AddSIs [succCI]; 
376 
AddSEs [succE]; 

377 

9180  378 
Goal "succ(n) ~= 0"; 
379 
by (blast_tac (claset() addSEs [equalityE]) 1) ; 

380 
qed "succ_not_0"; 

0  381 

2469  382 
bind_thm ("succ_neq_0", succ_not_0 RS notE); 
383 

384 
Addsimps [succ_not_0, succ_not_0 RS not_sym]; 

385 
AddSEs [succ_neq_0, sym RS succ_neq_0]; 

386 

0  387 

388 
(* succ(c) <= B ==> c : B *) 

9907  389 
bind_thm ("succ_subsetD", succI1 RSN (2,subsetD)); 
0  390 

1609  391 
(* succ(b) ~= b *) 
392 
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym); 

393 

9180  394 
Goal "succ(m) = succ(n) <> m=n"; 
395 
by (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ; 

396 
qed "succ_inject_iff"; 

0  397 

2469  398 
bind_thm ("succ_inject", succ_inject_iff RS iffD1); 
0  399 

2469  400 
Addsimps [succ_inject_iff]; 
401 
AddSDs [succ_inject]; 

0  402 

2877  403 
(*Not needed now that cons is available. Deletion reduces the search space.*) 
404 
Delrules [UpairI1,UpairI2,UpairE]; 