author | nipkow |
Sun, 05 Jan 2003 21:03:14 +0100 | |
changeset 13771 | 6cd59cc885a1 |
parent 13544 | 895994073bdf |
child 13780 | af7b79271364 |
permissions | -rw-r--r-- |
2469 | 1 |
(* Title: ZF/upair.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
13259 | 5 |
|
6 |
Observe the order of dependence: |
|
7 |
Upair is defined in terms of Replace |
|
8 |
Un is defined in terms of Upair and Union (similarly for Int) |
|
9 |
cons is defined in terms of Upair and Un |
|
10 |
Ordered pairs and descriptions are defined using cons ("set notation") |
|
2469 | 11 |
*) |
12 |
||
13357 | 13 |
header{*Unordered Pairs*} |
14 |
||
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
6153
diff
changeset
|
15 |
theory upair = ZF |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
6153
diff
changeset
|
16 |
files "Tools/typechk": |
6153 | 17 |
|
9907 | 18 |
setup TypeCheck.setup |
11770 | 19 |
declare atomize_ball [symmetric, rulify] |
6153 | 20 |
|
13356 | 21 |
(*belongs to theory ZF*) |
22 |
declare bspec [dest?] |
|
23 |
||
13259 | 24 |
lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *) |
25 |
lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *) |
|
26 |
||
27 |
||
13357 | 28 |
subsection{*Unordered Pairs: constant @{term Upair}*} |
13259 | 29 |
|
30 |
lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)" |
|
31 |
by (unfold Upair_def, blast) |
|
32 |
||
33 |
lemma UpairI1: "a : Upair(a,b)" |
|
34 |
by simp |
|
35 |
||
36 |
lemma UpairI2: "b : Upair(a,b)" |
|
37 |
by simp |
|
38 |
||
39 |
lemma UpairE: |
|
40 |
"[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P" |
|
41 |
apply simp |
|
42 |
apply blast |
|
43 |
done |
|
44 |
||
13357 | 45 |
subsection{*Rules for Binary Union, Defined via @{term Upair}*} |
13259 | 46 |
|
47 |
lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)" |
|
48 |
apply (simp add: Un_def) |
|
49 |
apply (blast intro: UpairI1 UpairI2 elim: UpairE) |
|
50 |
done |
|
51 |
||
52 |
lemma UnI1: "c : A ==> c : A Un B" |
|
53 |
by simp |
|
54 |
||
55 |
lemma UnI2: "c : B ==> c : A Un B" |
|
56 |
by simp |
|
57 |
||
13356 | 58 |
declare UnI1 [elim?] UnI2 [elim?] |
59 |
||
13259 | 60 |
lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
61 |
apply simp |
|
62 |
apply blast |
|
63 |
done |
|
64 |
||
65 |
(*Stronger version of the rule above*) |
|
66 |
lemma UnE': "[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P" |
|
67 |
apply simp |
|
68 |
apply blast |
|
69 |
done |
|
70 |
||
71 |
(*Classical introduction rule: no commitment to A vs B*) |
|
72 |
lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B" |
|
73 |
apply simp |
|
74 |
apply blast |
|
75 |
done |
|
76 |
||
77 |
||
13357 | 78 |
subsection{*Rules for Binary Intersection, Defined via @{term Upair}*} |
13259 | 79 |
|
80 |
lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)" |
|
81 |
apply (unfold Int_def) |
|
82 |
apply (blast intro: UpairI1 UpairI2 elim: UpairE) |
|
83 |
done |
|
84 |
||
85 |
lemma IntI [intro!]: "[| c : A; c : B |] ==> c : A Int B" |
|
86 |
by simp |
|
87 |
||
88 |
lemma IntD1: "c : A Int B ==> c : A" |
|
89 |
by simp |
|
90 |
||
91 |
lemma IntD2: "c : A Int B ==> c : B" |
|
92 |
by simp |
|
93 |
||
94 |
lemma IntE [elim!]: "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" |
|
95 |
by simp |
|
96 |
||
97 |
||
13357 | 98 |
subsection{*Rules for Set Difference, Defined via @{term Upair}*} |
13259 | 99 |
|
100 |
lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)" |
|
101 |
by (unfold Diff_def, blast) |
|
102 |
||
103 |
lemma DiffI [intro!]: "[| c : A; c ~: B |] ==> c : A - B" |
|
104 |
by simp |
|
105 |
||
106 |
lemma DiffD1: "c : A - B ==> c : A" |
|
107 |
by simp |
|
108 |
||
109 |
lemma DiffD2: "c : A - B ==> c ~: B" |
|
110 |
by simp |
|
111 |
||
112 |
lemma DiffE [elim!]: "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" |
|
113 |
by simp |
|
114 |
||
115 |
||
13357 | 116 |
subsection{*Rules for @{term cons}*} |
13259 | 117 |
|
118 |
lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)" |
|
119 |
apply (unfold cons_def) |
|
120 |
apply (blast intro: UpairI1 UpairI2 elim: UpairE) |
|
121 |
done |
|
122 |
||
123 |
(*risky as a typechecking rule, but solves otherwise unconstrained goals of |
|
124 |
the form x : ?A*) |
|
125 |
lemma consI1 [simp,TC]: "a : cons(a,B)" |
|
126 |
by simp |
|
127 |
||
128 |
||
129 |
lemma consI2: "a : B ==> a : cons(b,B)" |
|
130 |
by simp |
|
131 |
||
132 |
lemma consE [elim!]: |
|
133 |
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P" |
|
134 |
apply simp |
|
135 |
apply blast |
|
136 |
done |
|
137 |
||
138 |
(*Stronger version of the rule above*) |
|
139 |
lemma consE': |
|
140 |
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P" |
|
141 |
apply simp |
|
142 |
apply blast |
|
143 |
done |
|
144 |
||
145 |
(*Classical introduction rule*) |
|
146 |
lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)" |
|
147 |
apply simp |
|
148 |
apply blast |
|
149 |
done |
|
150 |
||
151 |
lemma cons_not_0 [simp]: "cons(a,B) ~= 0" |
|
152 |
by (blast elim: equalityE) |
|
153 |
||
154 |
lemmas cons_neq_0 = cons_not_0 [THEN notE, standard] |
|
155 |
||
156 |
declare cons_not_0 [THEN not_sym, simp] |
|
157 |
||
158 |
||
13357 | 159 |
subsection{*Singletons*} |
13259 | 160 |
|
161 |
lemma singleton_iff: "a : {b} <-> a=b" |
|
162 |
by simp |
|
163 |
||
164 |
lemma singletonI [intro!]: "a : {a}" |
|
165 |
by (rule consI1) |
|
166 |
||
167 |
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!] |
|
168 |
||
169 |
||
13357 | 170 |
subsection{*Rules for Descriptions*} |
13259 | 171 |
|
172 |
lemma the_equality [intro]: |
|
173 |
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" |
|
174 |
apply (unfold the_def) |
|
175 |
apply (fast dest: subst) |
|
176 |
done |
|
177 |
||
178 |
(* Only use this if you already know EX!x. P(x) *) |
|
179 |
lemma the_equality2: "[| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a" |
|
180 |
by blast |
|
181 |
||
182 |
lemma theI: "EX! x. P(x) ==> P(THE x. P(x))" |
|
183 |
apply (erule ex1E) |
|
184 |
apply (subst the_equality) |
|
185 |
apply (blast+) |
|
186 |
done |
|
187 |
||
188 |
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then |
|
189 |
(THE x.P(x)) rewrites to (THE x. Q(x)) *) |
|
190 |
||
191 |
(*If it's "undefined", it's zero!*) |
|
192 |
lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0" |
|
193 |
apply (unfold the_def) |
|
194 |
apply (blast elim!: ReplaceE) |
|
195 |
done |
|
196 |
||
197 |
(*Easier to apply than theI: conclusion has only one occurrence of P*) |
|
198 |
lemma theI2: |
|
199 |
assumes p1: "~ Q(0) ==> EX! x. P(x)" |
|
200 |
and p2: "!!x. P(x) ==> Q(x)" |
|
201 |
shows "Q(THE x. P(x))" |
|
202 |
apply (rule classical) |
|
203 |
apply (rule p2) |
|
204 |
apply (rule theI) |
|
205 |
apply (rule classical) |
|
206 |
apply (rule p1) |
|
207 |
apply (erule the_0 [THEN subst], assumption) |
|
208 |
done |
|
209 |
||
13357 | 210 |
lemma the_eq_trivial [simp]: "(THE x. x = a) = a" |
211 |
by blast |
|
212 |
||
13544 | 213 |
lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a" |
214 |
by blast |
|
215 |
||
13357 | 216 |
subsection{*Conditional Terms: @{text "if-then-else"}*} |
13259 | 217 |
|
218 |
lemma if_true [simp]: "(if True then a else b) = a" |
|
219 |
by (unfold if_def, blast) |
|
220 |
||
221 |
lemma if_false [simp]: "(if False then a else b) = b" |
|
222 |
by (unfold if_def, blast) |
|
223 |
||
224 |
(*Never use with case splitting, or if P is known to be true or false*) |
|
225 |
lemma if_cong: |
|
226 |
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] |
|
227 |
==> (if P then a else b) = (if Q then c else d)" |
|
228 |
by (simp add: if_def cong add: conj_cong) |
|
229 |
||
230 |
(*Prevents simplification of x and y: faster and allows the execution |
|
231 |
of functional programs. NOW THE DEFAULT.*) |
|
232 |
lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)" |
|
233 |
by simp |
|
234 |
||
235 |
(*Not needed for rewriting, since P would rewrite to True anyway*) |
|
236 |
lemma if_P: "P ==> (if P then a else b) = a" |
|
237 |
by (unfold if_def, blast) |
|
238 |
||
239 |
(*Not needed for rewriting, since P would rewrite to False anyway*) |
|
240 |
lemma if_not_P: "~P ==> (if P then a else b) = b" |
|
241 |
by (unfold if_def, blast) |
|
242 |
||
243 |
lemma split_if: "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
|
244 |
(*no case_tac yet!*) |
|
245 |
apply (rule_tac P=Q in case_split_thm, simp_all) |
|
246 |
done |
|
247 |
||
248 |
(** Rewrite rules for boolean case-splitting: faster than |
|
249 |
addsplits[split_if] |
|
250 |
**) |
|
251 |
||
252 |
lemmas split_if_eq1 = split_if [of "%x. x = b", standard] |
|
253 |
lemmas split_if_eq2 = split_if [of "%x. a = x", standard] |
|
254 |
||
255 |
lemmas split_if_mem1 = split_if [of "%x. x : b", standard] |
|
256 |
lemmas split_if_mem2 = split_if [of "%x. a : x", standard] |
|
257 |
||
258 |
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 |
|
259 |
||
260 |
(*Logically equivalent to split_if_mem2*) |
|
261 |
lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y" |
|
262 |
by (simp split add: split_if) |
|
263 |
||
264 |
lemma if_type [TC]: |
|
265 |
"[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A" |
|
266 |
by (simp split add: split_if) |
|
267 |
||
268 |
||
13357 | 269 |
subsection{*Consequences of Foundation*} |
13259 | 270 |
|
271 |
(*was called mem_anti_sym*) |
|
272 |
lemma mem_asym: "[| a:b; ~P ==> b:a |] ==> P" |
|
273 |
apply (rule classical) |
|
274 |
apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE]) |
|
275 |
apply (blast elim!: equalityE)+ |
|
276 |
done |
|
277 |
||
278 |
(*was called mem_anti_refl*) |
|
279 |
lemma mem_irrefl: "a:a ==> P" |
|
280 |
by (blast intro: mem_asym) |
|
281 |
||
282 |
(*mem_irrefl should NOT be added to default databases: |
|
283 |
it would be tried on most goals, making proofs slower!*) |
|
284 |
||
285 |
lemma mem_not_refl: "a ~: a" |
|
286 |
apply (rule notI) |
|
287 |
apply (erule mem_irrefl) |
|
288 |
done |
|
289 |
||
290 |
(*Good for proving inequalities by rewriting*) |
|
291 |
lemma mem_imp_not_eq: "a:A ==> a ~= A" |
|
292 |
by (blast elim!: mem_irrefl) |
|
293 |
||
13357 | 294 |
lemma eq_imp_not_mem: "a=A ==> a ~: A" |
295 |
by (blast intro: elim: mem_irrefl) |
|
296 |
||
297 |
subsection{*Rules for Successor*} |
|
13259 | 298 |
|
299 |
lemma succ_iff: "i : succ(j) <-> i=j | i:j" |
|
300 |
by (unfold succ_def, blast) |
|
301 |
||
302 |
lemma succI1 [simp]: "i : succ(i)" |
|
303 |
by (simp add: succ_iff) |
|
304 |
||
305 |
lemma succI2: "i : j ==> i : succ(j)" |
|
306 |
by (simp add: succ_iff) |
|
307 |
||
308 |
lemma succE [elim!]: |
|
309 |
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P" |
|
310 |
apply (simp add: succ_iff, blast) |
|
311 |
done |
|
312 |
||
313 |
(*Classical introduction rule*) |
|
314 |
lemma succCI [intro!]: "(i~:j ==> i=j) ==> i: succ(j)" |
|
315 |
by (simp add: succ_iff, blast) |
|
316 |
||
317 |
lemma succ_not_0 [simp]: "succ(n) ~= 0" |
|
318 |
by (blast elim!: equalityE) |
|
319 |
||
320 |
lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!] |
|
321 |
||
322 |
declare succ_not_0 [THEN not_sym, simp] |
|
323 |
declare sym [THEN succ_neq_0, elim!] |
|
324 |
||
325 |
(* succ(c) <= B ==> c : B *) |
|
326 |
lemmas succ_subsetD = succI1 [THEN [2] subsetD] |
|
327 |
||
328 |
(* succ(b) ~= b *) |
|
329 |
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard] |
|
330 |
||
331 |
lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n" |
|
332 |
by (blast elim: mem_asym elim!: equalityE) |
|
333 |
||
334 |
lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!] |
|
335 |
||
336 |
ML |
|
337 |
{* |
|
338 |
val Pow_bottom = thm "Pow_bottom"; |
|
339 |
val Pow_top = thm "Pow_top"; |
|
340 |
val Upair_iff = thm "Upair_iff"; |
|
341 |
val UpairI1 = thm "UpairI1"; |
|
342 |
val UpairI2 = thm "UpairI2"; |
|
343 |
val UpairE = thm "UpairE"; |
|
344 |
val Un_iff = thm "Un_iff"; |
|
345 |
val UnI1 = thm "UnI1"; |
|
346 |
val UnI2 = thm "UnI2"; |
|
347 |
val UnE = thm "UnE"; |
|
348 |
val UnE' = thm "UnE'"; |
|
349 |
val UnCI = thm "UnCI"; |
|
350 |
val Int_iff = thm "Int_iff"; |
|
351 |
val IntI = thm "IntI"; |
|
352 |
val IntD1 = thm "IntD1"; |
|
353 |
val IntD2 = thm "IntD2"; |
|
354 |
val IntE = thm "IntE"; |
|
355 |
val Diff_iff = thm "Diff_iff"; |
|
356 |
val DiffI = thm "DiffI"; |
|
357 |
val DiffD1 = thm "DiffD1"; |
|
358 |
val DiffD2 = thm "DiffD2"; |
|
359 |
val DiffE = thm "DiffE"; |
|
360 |
val cons_iff = thm "cons_iff"; |
|
361 |
val consI1 = thm "consI1"; |
|
362 |
val consI2 = thm "consI2"; |
|
363 |
val consE = thm "consE"; |
|
364 |
val consE' = thm "consE'"; |
|
365 |
val consCI = thm "consCI"; |
|
366 |
val cons_not_0 = thm "cons_not_0"; |
|
367 |
val cons_neq_0 = thm "cons_neq_0"; |
|
368 |
val singleton_iff = thm "singleton_iff"; |
|
369 |
val singletonI = thm "singletonI"; |
|
370 |
val singletonE = thm "singletonE"; |
|
371 |
val the_equality = thm "the_equality"; |
|
372 |
val the_equality2 = thm "the_equality2"; |
|
373 |
val theI = thm "theI"; |
|
374 |
val the_0 = thm "the_0"; |
|
375 |
val theI2 = thm "theI2"; |
|
376 |
val if_true = thm "if_true"; |
|
377 |
val if_false = thm "if_false"; |
|
378 |
val if_cong = thm "if_cong"; |
|
379 |
val if_weak_cong = thm "if_weak_cong"; |
|
380 |
val if_P = thm "if_P"; |
|
381 |
val if_not_P = thm "if_not_P"; |
|
382 |
val split_if = thm "split_if"; |
|
383 |
val split_if_eq1 = thm "split_if_eq1"; |
|
384 |
val split_if_eq2 = thm "split_if_eq2"; |
|
385 |
val split_if_mem1 = thm "split_if_mem1"; |
|
386 |
val split_if_mem2 = thm "split_if_mem2"; |
|
387 |
val if_iff = thm "if_iff"; |
|
388 |
val if_type = thm "if_type"; |
|
389 |
val mem_asym = thm "mem_asym"; |
|
390 |
val mem_irrefl = thm "mem_irrefl"; |
|
391 |
val mem_not_refl = thm "mem_not_refl"; |
|
392 |
val mem_imp_not_eq = thm "mem_imp_not_eq"; |
|
393 |
val succ_iff = thm "succ_iff"; |
|
394 |
val succI1 = thm "succI1"; |
|
395 |
val succI2 = thm "succI2"; |
|
396 |
val succE = thm "succE"; |
|
397 |
val succCI = thm "succCI"; |
|
398 |
val succ_not_0 = thm "succ_not_0"; |
|
399 |
val succ_neq_0 = thm "succ_neq_0"; |
|
400 |
val succ_subsetD = thm "succ_subsetD"; |
|
401 |
val succ_neq_self = thm "succ_neq_self"; |
|
402 |
val succ_inject_iff = thm "succ_inject_iff"; |
|
403 |
val succ_inject = thm "succ_inject"; |
|
404 |
||
405 |
val split_ifs = thms "split_ifs"; |
|
406 |
*} |
|
407 |
||
6153 | 408 |
end |