0
|
1 |
(* Title: ZF/upair
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
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 |
|
|
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 *)
|
|
20 |
|
|
21 |
|
|
22 |
(*** Unordered pairs - Upair ***)
|
|
23 |
|
|
24 |
val pairing = prove_goalw ZF.thy [Upair_def]
|
|
25 |
"c : Upair(a,b) <-> (c=a | c=b)"
|
|
26 |
(fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
|
|
27 |
|
|
28 |
val UpairI1 = prove_goal ZF.thy "a : Upair(a,b)"
|
|
29 |
(fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]);
|
|
30 |
|
|
31 |
val UpairI2 = prove_goal ZF.thy "b : Upair(a,b)"
|
|
32 |
(fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]);
|
|
33 |
|
|
34 |
val UpairE = prove_goal ZF.thy
|
|
35 |
"[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"
|
|
36 |
(fn major::prems=>
|
|
37 |
[ (rtac (major RS (pairing RS iffD1 RS disjE)) 1),
|
|
38 |
(REPEAT (eresolve_tac prems 1)) ]);
|
|
39 |
|
|
40 |
(*** Rules for binary union -- Un -- defined via Upair ***)
|
|
41 |
|
|
42 |
val UnI1 = prove_goalw ZF.thy [Un_def] "c : A ==> c : A Un B"
|
|
43 |
(fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]);
|
|
44 |
|
|
45 |
val UnI2 = prove_goalw ZF.thy [Un_def] "c : B ==> c : A Un B"
|
|
46 |
(fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]);
|
|
47 |
|
|
48 |
val UnE = prove_goalw ZF.thy [Un_def]
|
|
49 |
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
|
|
50 |
(fn major::prems=>
|
|
51 |
[ (rtac (major RS UnionE) 1),
|
|
52 |
(etac UpairE 1),
|
|
53 |
(REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]);
|
|
54 |
|
|
55 |
val Un_iff = prove_goal ZF.thy "c : A Un B <-> (c:A | c:B)"
|
|
56 |
(fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);
|
|
57 |
|
|
58 |
(*Classical introduction rule: no commitment to A vs B*)
|
|
59 |
val UnCI = prove_goal ZF.thy "(~c : B ==> c : A) ==> c : A Un B"
|
|
60 |
(fn [prem]=>
|
|
61 |
[ (rtac (disjCI RS (Un_iff RS iffD2)) 1),
|
|
62 |
(etac prem 1) ]);
|
|
63 |
|
|
64 |
|
|
65 |
(*** Rules for small intersection -- Int -- defined via Upair ***)
|
|
66 |
|
|
67 |
val IntI = prove_goalw ZF.thy [Int_def]
|
|
68 |
"[| c : A; c : B |] ==> c : A Int B"
|
|
69 |
(fn prems=>
|
|
70 |
[ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1
|
|
71 |
ORELSE eresolve_tac [UpairE, ssubst] 1)) ]);
|
|
72 |
|
|
73 |
val IntD1 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : A"
|
|
74 |
(fn [major]=>
|
|
75 |
[ (rtac (UpairI1 RS (major RS InterD)) 1) ]);
|
|
76 |
|
|
77 |
val IntD2 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : B"
|
|
78 |
(fn [major]=>
|
|
79 |
[ (rtac (UpairI2 RS (major RS InterD)) 1) ]);
|
|
80 |
|
|
81 |
val IntE = prove_goal ZF.thy
|
|
82 |
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"
|
|
83 |
(fn prems=>
|
|
84 |
[ (resolve_tac prems 1),
|
|
85 |
(REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);
|
|
86 |
|
|
87 |
val Int_iff = prove_goal ZF.thy "c : A Int B <-> (c:A & c:B)"
|
|
88 |
(fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]);
|
|
89 |
|
|
90 |
|
|
91 |
(*** Rules for set difference -- defined via Upair ***)
|
|
92 |
|
|
93 |
val DiffI = prove_goalw ZF.thy [Diff_def]
|
|
94 |
"[| c : A; ~ c : B |] ==> c : A - B"
|
|
95 |
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]);
|
|
96 |
|
|
97 |
val DiffD1 = prove_goalw ZF.thy [Diff_def]
|
|
98 |
"c : A - B ==> c : A"
|
|
99 |
(fn [major]=> [ (rtac (major RS CollectD1) 1) ]);
|
|
100 |
|
|
101 |
val DiffD2 = prove_goalw ZF.thy [Diff_def]
|
|
102 |
"[| c : A - B; c : B |] ==> P"
|
|
103 |
(fn [major,minor]=> [ (rtac (minor RS (major RS CollectD2 RS notE)) 1) ]);
|
|
104 |
|
|
105 |
val DiffE = prove_goal ZF.thy
|
|
106 |
"[| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P"
|
|
107 |
(fn prems=>
|
|
108 |
[ (resolve_tac prems 1),
|
|
109 |
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
|
|
110 |
|
|
111 |
val Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & ~ c:B)"
|
|
112 |
(fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
|
|
113 |
|
|
114 |
(*** Rules for cons -- defined via Un and Upair ***)
|
|
115 |
|
|
116 |
val consI1 = prove_goalw ZF.thy [cons_def] "a : cons(a,B)"
|
|
117 |
(fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]);
|
|
118 |
|
|
119 |
val consI2 = prove_goalw ZF.thy [cons_def] "a : B ==> a : cons(b,B)"
|
|
120 |
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);
|
|
121 |
|
|
122 |
val consE = prove_goalw ZF.thy [cons_def]
|
|
123 |
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"
|
|
124 |
(fn major::prems=>
|
|
125 |
[ (rtac (major RS UnE) 1),
|
|
126 |
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
|
|
127 |
|
|
128 |
val cons_iff = prove_goal ZF.thy "a : cons(b,A) <-> (a=b | a:A)"
|
|
129 |
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);
|
|
130 |
|
|
131 |
(*Classical introduction rule*)
|
|
132 |
val consCI = prove_goal ZF.thy "(~ a:B ==> a=b) ==> a: cons(b,B)"
|
|
133 |
(fn [prem]=>
|
|
134 |
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1),
|
|
135 |
(etac prem 1) ]);
|
|
136 |
|
|
137 |
(*** Singletons - using cons ***)
|
|
138 |
|
|
139 |
val singletonI = prove_goal ZF.thy "a : {a}"
|
|
140 |
(fn _=> [ (rtac consI1 1) ]);
|
|
141 |
|
|
142 |
val singletonE = prove_goal ZF.thy "[| a: {b}; a=b ==> P |] ==> P"
|
|
143 |
(fn major::prems=>
|
|
144 |
[ (rtac (major RS consE) 1),
|
|
145 |
(REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
|
|
146 |
|
|
147 |
|
|
148 |
(*** Rules for Descriptions ***)
|
|
149 |
|
|
150 |
val the_equality = prove_goalw ZF.thy [the_def]
|
|
151 |
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
|
|
152 |
(fn prems=>
|
|
153 |
[ (fast_tac (lemmas_cs addIs ([equalityI,singletonI]@prems)
|
|
154 |
addEs (prems RL [subst])) 1) ]);
|
|
155 |
|
|
156 |
(* Only use this if you already know EX!x. P(x) *)
|
|
157 |
val the_equality2 = prove_goal ZF.thy
|
|
158 |
"[| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a"
|
|
159 |
(fn major::prems=>
|
|
160 |
[ (rtac the_equality 1),
|
|
161 |
(rtac (major RS ex1_equalsE) 2),
|
|
162 |
(REPEAT (ares_tac prems 1)) ]);
|
|
163 |
|
|
164 |
val theI = prove_goal ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
|
|
165 |
(fn [major]=>
|
|
166 |
[ (rtac (major RS ex1E) 1),
|
|
167 |
(resolve_tac [major RS the_equality2 RS ssubst] 1),
|
|
168 |
(REPEAT (assume_tac 1)) ]);
|
|
169 |
|
|
170 |
val the_cong = prove_goalw ZF.thy [the_def]
|
|
171 |
"[| !!y. P(y) <-> Q(y) |] ==> (THE x. P(x)) = (THE x. Q(x))"
|
|
172 |
(fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
|
|
173 |
|
|
174 |
|
|
175 |
(*** if -- a conditional expression for formulae ***)
|
|
176 |
|
|
177 |
goalw ZF.thy [if_def] "if(True,a,b) = a";
|
|
178 |
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
|
|
179 |
val if_true = result();
|
|
180 |
|
|
181 |
goalw ZF.thy [if_def] "if(False,a,b) = b";
|
|
182 |
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
|
|
183 |
val if_false = result();
|
|
184 |
|
|
185 |
val prems = goalw ZF.thy [if_def]
|
|
186 |
"[| P<->Q; a=c; b=d |] ==> if(P,a,b) = if(Q,c,d)";
|
|
187 |
by (REPEAT (resolve_tac (prems@[refl,the_cong]@FOL_congs) 1));
|
|
188 |
val if_cong = result();
|
|
189 |
|
|
190 |
(*Not needed for rewriting, since P would rewrite to True anyway*)
|
|
191 |
val prems = goalw ZF.thy [if_def] "P ==> if(P,a,b) = a";
|
|
192 |
by (cut_facts_tac prems 1);
|
|
193 |
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
|
|
194 |
val if_P = result();
|
|
195 |
|
|
196 |
(*Not needed for rewriting, since P would rewrite to False anyway*)
|
|
197 |
val prems = goalw ZF.thy [if_def] "~P ==> if(P,a,b) = b";
|
|
198 |
by (cut_facts_tac prems 1);
|
|
199 |
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
|
|
200 |
val if_not_P = result();
|
|
201 |
|
|
202 |
val if_ss =
|
|
203 |
FOL_ss addcongs (if_cong :: mk_typed_congs ZF.thy [("P", "i=>o")]
|
|
204 |
@ basic_ZF_congs)
|
|
205 |
addrews [if_true,if_false];
|
|
206 |
|
|
207 |
val expand_if = prove_goal ZF.thy
|
|
208 |
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
|
|
209 |
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
|
|
210 |
(ASM_SIMP_TAC if_ss 1),
|
|
211 |
(ASM_SIMP_TAC if_ss 1) ]);
|
|
212 |
|
|
213 |
val prems = goal ZF.thy
|
|
214 |
"[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A";
|
|
215 |
by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);
|
|
216 |
by (ALLGOALS (ASM_SIMP_TAC (if_ss addrews prems)));
|
|
217 |
val if_type = result();
|
|
218 |
|
|
219 |
|
|
220 |
(*** Foundation lemmas ***)
|
|
221 |
|
|
222 |
val mem_anti_sym = prove_goal ZF.thy "[| a:b; b:a |] ==> P"
|
|
223 |
(fn prems=>
|
|
224 |
[ (rtac disjE 1),
|
|
225 |
(res_inst_tac [("A","{a,b}")] foundation 1),
|
|
226 |
(etac equals0D 1),
|
|
227 |
(rtac consI1 1),
|
|
228 |
(fast_tac (lemmas_cs addIs (prems@[consI1,consI2])
|
|
229 |
addSEs [consE,equalityE]) 1) ]);
|
|
230 |
|
|
231 |
val mem_anti_refl = prove_goal ZF.thy "a:a ==> P"
|
|
232 |
(fn [major]=> [ (rtac (major RS (major RS mem_anti_sym)) 1) ]);
|
|
233 |
|
|
234 |
val mem_not_refl = prove_goal ZF.thy "~ a:a"
|
|
235 |
(K [ (rtac notI 1), (etac mem_anti_refl 1) ]);
|
|
236 |
|
|
237 |
(*** Rules for succ ***)
|
|
238 |
|
|
239 |
val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"
|
|
240 |
(fn _=> [ (rtac consI1 1) ]);
|
|
241 |
|
|
242 |
val succI2 = prove_goalw ZF.thy [succ_def]
|
|
243 |
"i : j ==> i : succ(j)"
|
|
244 |
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
|
|
245 |
|
|
246 |
(*Classical introduction rule*)
|
|
247 |
val succCI = prove_goalw ZF.thy [succ_def]
|
|
248 |
"(~ i:j ==> i=j) ==> i: succ(j)"
|
|
249 |
(fn prems=> [ (rtac consCI 1), (eresolve_tac prems 1) ]);
|
|
250 |
|
|
251 |
val succE = prove_goalw ZF.thy [succ_def]
|
|
252 |
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"
|
|
253 |
(fn major::prems=>
|
|
254 |
[ (rtac (major RS consE) 1),
|
|
255 |
(REPEAT (eresolve_tac prems 1)) ]);
|
|
256 |
|
|
257 |
val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"
|
|
258 |
(fn [major]=>
|
|
259 |
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
|
|
260 |
(rtac succI1 1) ]);
|
|
261 |
|
|
262 |
(*Useful for rewriting*)
|
|
263 |
val succ_not_0 = prove_goal ZF.thy "~ succ(n)=0"
|
|
264 |
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);
|
|
265 |
|
|
266 |
(* succ(c) <= B ==> c : B *)
|
|
267 |
val succ_subsetD = succI1 RSN (2,subsetD);
|
|
268 |
|
|
269 |
val succ_inject = prove_goal ZF.thy "succ(m) = succ(n) ==> m=n"
|
|
270 |
(fn [major]=>
|
|
271 |
[ (rtac (major RS equalityE) 1),
|
|
272 |
(REPEAT (eresolve_tac [asm_rl, sym, succE, make_elim succ_subsetD,
|
|
273 |
mem_anti_sym] 1)) ]);
|
|
274 |
|
|
275 |
val succ_inject_iff = prove_goal ZF.thy "succ(m) = succ(n) <-> m=n"
|
|
276 |
(fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);
|
|
277 |
|
|
278 |
(*UpairI1/2 should become UpairCI; mem_anti_refl as a hazE? *)
|
|
279 |
val upair_cs = lemmas_cs
|
|
280 |
addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]
|
|
281 |
addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];
|
|
282 |
|