author | wenzelm |
Mon, 13 Mar 2000 13:21:39 +0100 | |
changeset 8434 | 5e4bba59bfaa |
parent 8183 | 344888de76c4 |
child 8551 | 5c22595bc599 |
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) *) |
|
0 | 19 |
|
20 |
||
21 |
(*** Unordered pairs - Upair ***) |
|
22 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
23 |
qed_goalw "Upair_iff" thy [Upair_def] |
0 | 24 |
"c : Upair(a,b) <-> (c=a | c=b)" |
5468 | 25 |
(fn _ => [ (Blast_tac 1) ]); |
2469 | 26 |
|
27 |
Addsimps [Upair_iff]; |
|
0 | 28 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
29 |
qed_goal "UpairI1" thy "a : Upair(a,b)" |
2469 | 30 |
(fn _ => [ Simp_tac 1 ]); |
0 | 31 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
32 |
qed_goal "UpairI2" thy "b : Upair(a,b)" |
2469 | 33 |
(fn _ => [ Simp_tac 1 ]); |
0 | 34 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
35 |
qed_goal "UpairE" thy |
0 | 36 |
"[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P" |
37 |
(fn major::prems=> |
|
2469 | 38 |
[ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1), |
0 | 39 |
(REPEAT (eresolve_tac prems 1)) ]); |
40 |
||
2469 | 41 |
AddSIs [UpairI1,UpairI2]; |
42 |
AddSEs [UpairE]; |
|
43 |
||
0 | 44 |
(*** Rules for binary union -- Un -- defined via Upair ***) |
45 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
46 |
qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)" |
2877 | 47 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 48 |
|
49 |
Addsimps [Un_iff]; |
|
0 | 50 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
51 |
qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B" |
2469 | 52 |
(fn _ => [ Asm_simp_tac 1 ]); |
0 | 53 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
54 |
qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B" |
2469 | 55 |
(fn _ => [ Asm_simp_tac 1 ]); |
56 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
57 |
qed_goal "UnE" thy |
0 | 58 |
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
59 |
(fn major::prems=> |
|
2469 | 60 |
[ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1), |
61 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
0 | 62 |
|
572 | 63 |
(*Stronger version of the rule above*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
64 |
qed_goal "UnE'" thy |
572 | 65 |
"[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P" |
66 |
(fn major::prems => |
|
67 |
[(rtac (major RS UnE) 1), |
|
68 |
(eresolve_tac prems 1), |
|
69 |
(rtac classical 1), |
|
70 |
(eresolve_tac prems 1), |
|
71 |
(swap_res_tac prems 1), |
|
72 |
(etac notnotD 1)]); |
|
73 |
||
2469 | 74 |
(*Classical introduction rule: no commitment to A vs B*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
75 |
qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B" |
2469 | 76 |
(fn prems=> |
4091 | 77 |
[ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]); |
0 | 78 |
|
2469 | 79 |
AddSIs [UnCI]; |
80 |
AddSEs [UnE]; |
|
0 | 81 |
|
82 |
||
83 |
(*** Rules for small intersection -- Int -- defined via Upair ***) |
|
84 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
85 |
qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)" |
2877 | 86 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 87 |
|
88 |
Addsimps [Int_iff]; |
|
89 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
90 |
qed_goal "IntI" thy "!!c. [| c : A; c : B |] ==> c : A Int B" |
2469 | 91 |
(fn _ => [ Asm_simp_tac 1 ]); |
0 | 92 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
93 |
qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A" |
2469 | 94 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
0 | 95 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
96 |
qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B" |
2469 | 97 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
0 | 98 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
99 |
qed_goal "IntE" thy |
0 | 100 |
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" |
101 |
(fn prems=> |
|
102 |
[ (resolve_tac prems 1), |
|
103 |
(REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]); |
|
104 |
||
2469 | 105 |
AddSIs [IntI]; |
106 |
AddSEs [IntE]; |
|
0 | 107 |
|
108 |
(*** Rules for set difference -- defined via Upair ***) |
|
109 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
110 |
qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)" |
2877 | 111 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 112 |
|
113 |
Addsimps [Diff_iff]; |
|
114 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
115 |
qed_goal "DiffI" thy "!!c. [| c : A; c ~: B |] ==> c : A - B" |
2469 | 116 |
(fn _ => [ Asm_simp_tac 1 ]); |
0 | 117 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
118 |
qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A" |
2469 | 119 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
0 | 120 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
121 |
qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B" |
2469 | 122 |
(fn _ => [ Asm_full_simp_tac 1 ]); |
0 | 123 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
124 |
qed_goal "DiffE" thy |
37 | 125 |
"[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
0 | 126 |
(fn prems=> |
127 |
[ (resolve_tac prems 1), |
|
485 | 128 |
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]); |
0 | 129 |
|
2469 | 130 |
AddSIs [DiffI]; |
131 |
AddSEs [DiffE]; |
|
0 | 132 |
|
133 |
(*** Rules for cons -- defined via Un and Upair ***) |
|
134 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
135 |
qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)" |
2877 | 136 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 137 |
|
138 |
Addsimps [cons_iff]; |
|
0 | 139 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
140 |
qed_goal "consI1" thy "a : cons(a,B)" |
2469 | 141 |
(fn _ => [ Simp_tac 1 ]); |
142 |
||
143 |
Addsimps [consI1]; |
|
6153 | 144 |
AddTCs [consI1]; (*risky as a typechecking rule, but solves otherwise |
145 |
unconstrained goals of the form x : ?A*) |
|
0 | 146 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
147 |
qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)" |
2469 | 148 |
(fn _ => [ Asm_simp_tac 1 ]); |
149 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
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*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
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*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
168 |
qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)" |
2469 | 169 |
(fn prems=> |
4091 | 170 |
[ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]); |
0 | 171 |
|
2469 | 172 |
AddSIs [consCI]; |
173 |
AddSEs [consE]; |
|
0 | 174 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
175 |
qed_goal "cons_not_0" thy "cons(a,B) ~= 0" |
4091 | 176 |
(fn _ => [ (blast_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 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
185 |
qed_goal "singleton_iff" thy "a : {b} <-> a=b" |
2469 | 186 |
(fn _ => [ Simp_tac 1 ]); |
187 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
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 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
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] => |
4091 | 201 |
[ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]); |
0 | 202 |
|
5506 | 203 |
AddIs [the_equality]; |
204 |
||
0 | 205 |
(* 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
|
206 |
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
|
207 |
by (Blast_tac 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
208 |
qed "the_equality2"; |
0 | 209 |
|
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
210 |
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
|
211 |
by (etac ex1E 1); |
8183 | 212 |
by (stac the_equality 1); |
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
213 |
by (REPEAT (Blast_tac 1)); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
214 |
qed "theI"; |
0 | 215 |
|
435 | 216 |
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then |
217 |
(THE x.P(x)) rewrites to (THE x. Q(x)) *) |
|
218 |
||
219 |
(*If it's "undefined", it's zero!*) |
|
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
220 |
Goalw [the_def] "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
221 |
by (blast_tac (claset() addSEs [ReplaceE]) 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
222 |
qed "the_0"; |
0 | 223 |
|
5506 | 224 |
(*Easier to apply than theI: conclusion has only one occurrence of P*) |
225 |
val prems = |
|
226 |
Goal "[| ~ Q(0) ==> EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"; |
|
227 |
by (rtac classical 1); |
|
228 |
by (resolve_tac prems 1); |
|
229 |
by (rtac theI 1); |
|
230 |
by (rtac classical 1); |
|
231 |
by (resolve_tac prems 1); |
|
6163 | 232 |
by (etac (the_0 RS subst) 1); |
233 |
by (assume_tac 1); |
|
5506 | 234 |
qed "theI2"; |
235 |
||
0 | 236 |
(*** if -- a conditional expression for formulae ***) |
237 |
||
6068 | 238 |
Goalw [if_def] "(if True then a else b) = a"; |
5506 | 239 |
by (Blast_tac 1); |
760 | 240 |
qed "if_true"; |
0 | 241 |
|
6068 | 242 |
Goalw [if_def] "(if False then a else b) = b"; |
5506 | 243 |
by (Blast_tac 1); |
760 | 244 |
qed "if_false"; |
0 | 245 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
246 |
(*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
|
247 |
val prems = Goalw [if_def] |
6068 | 248 |
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] \ |
249 |
\ ==> (if P then a else b) = (if Q then c else d)"; |
|
4091 | 250 |
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1); |
760 | 251 |
qed "if_cong"; |
0 | 252 |
|
253 |
(*Not needed for rewriting, since P would rewrite to True anyway*) |
|
6068 | 254 |
Goalw [if_def] "P ==> (if P then a else b) = a"; |
5506 | 255 |
by (Blast_tac 1); |
760 | 256 |
qed "if_P"; |
0 | 257 |
|
258 |
(*Not needed for rewriting, since P would rewrite to False anyway*) |
|
6068 | 259 |
Goalw [if_def] "~P ==> (if P then a else b) = b"; |
5506 | 260 |
by (Blast_tac 1); |
760 | 261 |
qed "if_not_P"; |
0 | 262 |
|
2469 | 263 |
Addsimps [if_true, if_false]; |
0 | 264 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
265 |
qed_goal "split_if" thy |
6068 | 266 |
"P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
267 |
(fn _=> [ (case_tac "Q" 1), |
2469 | 268 |
(Asm_simp_tac 1), |
269 |
(Asm_simp_tac 1) ]); |
|
0 | 270 |
|
3914 | 271 |
(** Rewrite rules for boolean case-splitting: faster than |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
272 |
addsplits[split_if] |
3914 | 273 |
**) |
274 |
||
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
275 |
bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if); |
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
276 |
bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if); |
3914 | 277 |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
278 |
bind_thm ("split_if_mem1", read_instantiate [("P", "%x. x : ?b")] split_if); |
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
279 |
bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if); |
3914 | 280 |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
281 |
val split_ifs = [split_if_eq1, split_if_eq2, |
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
282 |
split_if_mem1, split_if_mem2]; |
3914 | 283 |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
284 |
(*Logically equivalent to split_if_mem2*) |
6068 | 285 |
qed_goal "if_iff" thy "a: (if P then x else y) <-> P & a:x | ~P & a:y" |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
286 |
(fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]); |
1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
287 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
288 |
qed_goal "if_type" thy |
6068 | 289 |
"[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A" |
1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
290 |
(fn prems=> [ (simp_tac |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
291 |
(simpset() addsimps prems addsplits [split_if]) 1) ]); |
6153 | 292 |
AddTCs [if_type]; |
0 | 293 |
|
294 |
(*** Foundation lemmas ***) |
|
295 |
||
437 | 296 |
(*was called mem_anti_sym*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
297 |
qed_goal "mem_asym" thy "[| a:b; ~P ==> b:a |] ==> P" |
2877 | 298 |
(fn prems=> |
299 |
[ (rtac classical 1), |
|
300 |
(res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1), |
|
4091 | 301 |
REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]); |
0 | 302 |
|
437 | 303 |
(*was called mem_anti_refl*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
304 |
qed_goal "mem_irrefl" thy "a:a ==> P" |
2469 | 305 |
(fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]); |
0 | 306 |
|
2469 | 307 |
(*mem_irrefl should NOT be added to default databases: |
308 |
it would be tried on most goals, making proofs slower!*) |
|
309 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
310 |
qed_goal "mem_not_refl" thy "a ~: a" |
437 | 311 |
(K [ (rtac notI 1), (etac mem_irrefl 1) ]); |
0 | 312 |
|
435 | 313 |
(*Good for proving inequalities by rewriting*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
314 |
qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A" |
4091 | 315 |
(fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]); |
435 | 316 |
|
0 | 317 |
(*** Rules for succ ***) |
318 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
319 |
qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j" |
2877 | 320 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 321 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
322 |
qed_goalw "succI1" thy [succ_def] "i : succ(i)" |
0 | 323 |
(fn _=> [ (rtac consI1 1) ]); |
324 |
||
2469 | 325 |
Addsimps [succI1]; |
326 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
327 |
qed_goalw "succI2" thy [succ_def] |
0 | 328 |
"i : j ==> i : succ(j)" |
329 |
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]); |
|
330 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
331 |
qed_goalw "succE" thy [succ_def] |
0 | 332 |
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P" |
333 |
(fn major::prems=> |
|
334 |
[ (rtac (major RS consE) 1), |
|
335 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
336 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
337 |
(*Classical introduction rule*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
338 |
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
|
339 |
(fn [prem]=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
340 |
[ (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
|
341 |
(etac prem 1) ]); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
342 |
|
2469 | 343 |
AddSIs [succCI]; |
344 |
AddSEs [succE]; |
|
345 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
346 |
qed_goal "succ_not_0" thy "succ(n) ~= 0" |
4091 | 347 |
(fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]); |
0 | 348 |
|
2469 | 349 |
bind_thm ("succ_neq_0", succ_not_0 RS notE); |
350 |
||
351 |
Addsimps [succ_not_0, succ_not_0 RS not_sym]; |
|
352 |
AddSEs [succ_neq_0, sym RS succ_neq_0]; |
|
353 |
||
0 | 354 |
|
355 |
(* succ(c) <= B ==> c : B *) |
|
356 |
val succ_subsetD = succI1 RSN (2,subsetD); |
|
357 |
||
1609 | 358 |
(* succ(b) ~= b *) |
359 |
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym); |
|
360 |
||
361 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
362 |
qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n" |
4091 | 363 |
(fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]); |
0 | 364 |
|
2469 | 365 |
bind_thm ("succ_inject", succ_inject_iff RS iffD1); |
0 | 366 |
|
2469 | 367 |
Addsimps [succ_inject_iff]; |
368 |
AddSDs [succ_inject]; |
|
0 | 369 |
|
2877 | 370 |
(*Not needed now that cons is available. Deletion reduces the search space.*) |
371 |
Delrules [UpairI1,UpairI2,UpairE]; |
|
2469 | 372 |
|
373 |
use"simpdata.ML"; |