author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5506 | e07254044384 |
child 6068 | 2d8f3e1f1151 |
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]; |
|
0 | 144 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
145 |
qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)" |
2469 | 146 |
(fn _ => [ Asm_simp_tac 1 ]); |
147 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
148 |
qed_goal "consE" thy |
0 | 149 |
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P" |
150 |
(fn major::prems=> |
|
2469 | 151 |
[ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1), |
0 | 152 |
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]); |
153 |
||
572 | 154 |
(*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
|
155 |
qed_goal "consE'" thy |
572 | 156 |
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P" |
157 |
(fn major::prems => |
|
158 |
[(rtac (major RS consE) 1), |
|
159 |
(eresolve_tac prems 1), |
|
160 |
(rtac classical 1), |
|
161 |
(eresolve_tac prems 1), |
|
162 |
(swap_res_tac prems 1), |
|
163 |
(etac notnotD 1)]); |
|
164 |
||
2469 | 165 |
(*Classical introduction rule*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
166 |
qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)" |
2469 | 167 |
(fn prems=> |
4091 | 168 |
[ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]); |
0 | 169 |
|
2469 | 170 |
AddSIs [consCI]; |
171 |
AddSEs [consE]; |
|
0 | 172 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
173 |
qed_goal "cons_not_0" thy "cons(a,B) ~= 0" |
4091 | 174 |
(fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]); |
1609 | 175 |
|
2469 | 176 |
bind_thm ("cons_neq_0", cons_not_0 RS notE); |
177 |
||
178 |
Addsimps [cons_not_0, cons_not_0 RS not_sym]; |
|
179 |
||
1609 | 180 |
|
0 | 181 |
(*** Singletons - using cons ***) |
182 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
183 |
qed_goal "singleton_iff" thy "a : {b} <-> a=b" |
2469 | 184 |
(fn _ => [ Simp_tac 1 ]); |
185 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
186 |
qed_goal "singletonI" thy "a : {a}" |
0 | 187 |
(fn _=> [ (rtac consI1 1) ]); |
188 |
||
2469 | 189 |
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1)); |
0 | 190 |
|
2469 | 191 |
AddSIs [singletonI]; |
192 |
AddSEs [singletonE]; |
|
0 | 193 |
|
194 |
(*** Rules for Descriptions ***) |
|
195 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
196 |
qed_goalw "the_equality" thy [the_def] |
0 | 197 |
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" |
738 | 198 |
(fn [pa,eq] => |
4091 | 199 |
[ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]); |
0 | 200 |
|
5506 | 201 |
AddIs [the_equality]; |
202 |
||
0 | 203 |
(* Only use this if you already know EX!x. P(x) *) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
204 |
qed_goal "the_equality2" thy |
673 | 205 |
"!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" |
5506 | 206 |
(fn _ => [ (Blast_tac 1) ]); |
0 | 207 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
208 |
qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))" |
0 | 209 |
(fn [major]=> |
210 |
[ (rtac (major RS ex1E) 1), |
|
211 |
(resolve_tac [major RS the_equality2 RS ssubst] 1), |
|
212 |
(REPEAT (assume_tac 1)) ]); |
|
213 |
||
435 | 214 |
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then |
215 |
(THE x.P(x)) rewrites to (THE x. Q(x)) *) |
|
216 |
||
217 |
(*If it's "undefined", it's zero!*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
218 |
qed_goalw "the_0" thy [the_def] |
435 | 219 |
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" |
5488 | 220 |
(fn _ => [ (blast_tac (claset() addSEs [ReplaceE]) 1) ]); |
435 | 221 |
|
0 | 222 |
|
5506 | 223 |
(*Easier to apply than theI: conclusion has only one occurrence of P*) |
224 |
val prems = |
|
225 |
Goal "[| ~ Q(0) ==> EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"; |
|
226 |
by (rtac classical 1); |
|
227 |
by (resolve_tac prems 1); |
|
228 |
by (rtac theI 1); |
|
229 |
by (rtac classical 1); |
|
230 |
by (resolve_tac prems 1); |
|
231 |
be (the_0 RS subst) 1; |
|
232 |
ba 1; |
|
233 |
qed "theI2"; |
|
234 |
||
0 | 235 |
(*** if -- a conditional expression for formulae ***) |
236 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
237 |
Goalw [if_def] "if(True,a,b) = a"; |
5506 | 238 |
by (Blast_tac 1); |
760 | 239 |
qed "if_true"; |
0 | 240 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
241 |
Goalw [if_def] "if(False,a,b) = b"; |
5506 | 242 |
by (Blast_tac 1); |
760 | 243 |
qed "if_false"; |
0 | 244 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
245 |
(*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
|
246 |
val prems = Goalw [if_def] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
247 |
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)"; |
4091 | 248 |
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1); |
760 | 249 |
qed "if_cong"; |
0 | 250 |
|
251 |
(*Not needed for rewriting, since P would rewrite to True anyway*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
252 |
Goalw [if_def] "P ==> if(P,a,b) = a"; |
5506 | 253 |
by (Blast_tac 1); |
760 | 254 |
qed "if_P"; |
0 | 255 |
|
256 |
(*Not needed for rewriting, since P would rewrite to False anyway*) |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
257 |
Goalw [if_def] "~P ==> if(P,a,b) = b"; |
5506 | 258 |
by (Blast_tac 1); |
760 | 259 |
qed "if_not_P"; |
0 | 260 |
|
2469 | 261 |
Addsimps [if_true, if_false]; |
0 | 262 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
263 |
qed_goal "split_if" thy |
0 | 264 |
"P(if(Q,x,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
|
265 |
(fn _=> [ (case_tac "Q" 1), |
2469 | 266 |
(Asm_simp_tac 1), |
267 |
(Asm_simp_tac 1) ]); |
|
0 | 268 |
|
3914 | 269 |
(** 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
|
270 |
addsplits[split_if] |
3914 | 271 |
**) |
272 |
||
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
273 |
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
|
274 |
bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if); |
3914 | 275 |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
276 |
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
|
277 |
bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if); |
3914 | 278 |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
279 |
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
|
280 |
split_if_mem1, split_if_mem2]; |
3914 | 281 |
|
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
282 |
(*Logically equivalent to split_if_mem2*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
283 |
qed_goal "if_iff" thy "a: if(P,x,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
|
284 |
(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
|
285 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
286 |
qed_goal "if_type" thy |
1017
6a402dc505cf
Proved if_iff and used it to simplify proof of if_type.
lcp
parents:
985
diff
changeset
|
287 |
"[| 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
|
288 |
(fn prems=> [ (simp_tac |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
4091
diff
changeset
|
289 |
(simpset() addsimps prems addsplits [split_if]) 1) ]); |
0 | 290 |
|
291 |
||
292 |
(*** Foundation lemmas ***) |
|
293 |
||
437 | 294 |
(*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
|
295 |
qed_goal "mem_asym" thy "[| a:b; ~P ==> b:a |] ==> P" |
2877 | 296 |
(fn prems=> |
297 |
[ (rtac classical 1), |
|
298 |
(res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1), |
|
4091 | 299 |
REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]); |
0 | 300 |
|
437 | 301 |
(*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
|
302 |
qed_goal "mem_irrefl" thy "a:a ==> P" |
2469 | 303 |
(fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]); |
0 | 304 |
|
2469 | 305 |
(*mem_irrefl should NOT be added to default databases: |
306 |
it would be tried on most goals, making proofs slower!*) |
|
307 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
308 |
qed_goal "mem_not_refl" thy "a ~: a" |
437 | 309 |
(K [ (rtac notI 1), (etac mem_irrefl 1) ]); |
0 | 310 |
|
435 | 311 |
(*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
|
312 |
qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A" |
4091 | 313 |
(fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]); |
435 | 314 |
|
0 | 315 |
(*** Rules for succ ***) |
316 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
317 |
qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j" |
2877 | 318 |
(fn _ => [ Blast_tac 1 ]); |
2469 | 319 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
320 |
qed_goalw "succI1" thy [succ_def] "i : succ(i)" |
0 | 321 |
(fn _=> [ (rtac consI1 1) ]); |
322 |
||
2469 | 323 |
Addsimps [succI1]; |
324 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
325 |
qed_goalw "succI2" thy [succ_def] |
0 | 326 |
"i : j ==> i : succ(j)" |
327 |
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]); |
|
328 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
329 |
qed_goalw "succE" thy [succ_def] |
0 | 330 |
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P" |
331 |
(fn major::prems=> |
|
332 |
[ (rtac (major RS consE) 1), |
|
333 |
(REPEAT (eresolve_tac prems 1)) ]); |
|
334 |
||
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
335 |
(*Classical introduction rule*) |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
336 |
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
|
337 |
(fn [prem]=> |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
338 |
[ (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
|
339 |
(etac prem 1) ]); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
340 |
|
2469 | 341 |
AddSIs [succCI]; |
342 |
AddSEs [succE]; |
|
343 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
344 |
qed_goal "succ_not_0" thy "succ(n) ~= 0" |
4091 | 345 |
(fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]); |
0 | 346 |
|
2469 | 347 |
bind_thm ("succ_neq_0", succ_not_0 RS notE); |
348 |
||
349 |
Addsimps [succ_not_0, succ_not_0 RS not_sym]; |
|
350 |
AddSEs [succ_neq_0, sym RS succ_neq_0]; |
|
351 |
||
0 | 352 |
|
353 |
(* succ(c) <= B ==> c : B *) |
|
354 |
val succ_subsetD = succI1 RSN (2,subsetD); |
|
355 |
||
1609 | 356 |
(* succ(b) ~= b *) |
357 |
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym); |
|
358 |
||
359 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5242
diff
changeset
|
360 |
qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n" |
4091 | 361 |
(fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]); |
0 | 362 |
|
2469 | 363 |
bind_thm ("succ_inject", succ_inject_iff RS iffD1); |
0 | 364 |
|
2469 | 365 |
Addsimps [succ_inject_iff]; |
366 |
AddSDs [succ_inject]; |
|
0 | 367 |
|
2877 | 368 |
(*Not needed now that cons is available. Deletion reduces the search space.*) |
369 |
Delrules [UpairI1,UpairI2,UpairE]; |
|
2469 | 370 |
|
371 |
use"simpdata.ML"; |