|
1 (* Title: ZF/epsilon.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 For epsilon.thy. Epsilon induction and recursion |
|
7 *) |
|
8 |
|
9 open Epsilon; |
|
10 |
|
11 (*** Basic closure properties ***) |
|
12 |
|
13 goalw Epsilon.thy [eclose_def] "A <= eclose(A)"; |
|
14 by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1); |
|
15 br (nat_0I RS UN_upper) 1; |
|
16 val arg_subset_eclose = result(); |
|
17 |
|
18 val arg_into_eclose = arg_subset_eclose RS subsetD; |
|
19 |
|
20 goalw Epsilon.thy [eclose_def,Transset_def] "Transset(eclose(A))"; |
|
21 by (rtac (subsetI RS ballI) 1); |
|
22 by (etac UN_E 1); |
|
23 by (rtac (nat_succI RS UN_I) 1); |
|
24 by (assume_tac 1); |
|
25 by (etac (nat_rec_succ RS ssubst) 1); |
|
26 by (etac UnionI 1); |
|
27 by (assume_tac 1); |
|
28 val Transset_eclose = result(); |
|
29 |
|
30 (* x : eclose(A) ==> x <= eclose(A) *) |
|
31 val eclose_subset = |
|
32 standard (rewrite_rule [Transset_def] Transset_eclose RS bspec); |
|
33 |
|
34 (* [| A : eclose(B); c : A |] ==> c : eclose(B) *) |
|
35 val ecloseD = standard (eclose_subset RS subsetD); |
|
36 |
|
37 val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD; |
|
38 val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD; |
|
39 |
|
40 (* This is epsilon-induction for eclose(A); see also eclose_induct_down... |
|
41 [| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) |
|
42 |] ==> P(a) |
|
43 *) |
|
44 val eclose_induct = standard (Transset_eclose RSN (2, Transset_induct)); |
|
45 |
|
46 (*Epsilon induction*) |
|
47 val prems = goal Epsilon.thy |
|
48 "[| !!x. ALL y:x. P(y) ==> P(x) |] ==> P(a)"; |
|
49 by (rtac (arg_in_eclose_sing RS eclose_induct) 1); |
|
50 by (eresolve_tac prems 1); |
|
51 val eps_induct = result(); |
|
52 |
|
53 (*Perform epsilon-induction on i. *) |
|
54 fun eps_ind_tac a = |
|
55 EVERY' [res_inst_tac [("a",a)] eps_induct, |
|
56 rename_last_tac a ["1"]]; |
|
57 |
|
58 |
|
59 (*** Leastness of eclose ***) |
|
60 |
|
61 (** eclose(A) is the least transitive set including A as a subset. **) |
|
62 |
|
63 goalw Epsilon.thy [Transset_def] |
|
64 "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \ |
|
65 \ nat_rec(n, A, %m r. Union(r)) <= X"; |
|
66 by (etac nat_induct 1); |
|
67 by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1); |
|
68 by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1); |
|
69 by (fast_tac ZF_cs 1); |
|
70 val eclose_least_lemma = result(); |
|
71 |
|
72 goalw Epsilon.thy [eclose_def] |
|
73 "!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X"; |
|
74 br (eclose_least_lemma RS UN_least) 1; |
|
75 by (REPEAT (assume_tac 1)); |
|
76 val eclose_least = result(); |
|
77 |
|
78 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
|
79 val [major,base,step] = goal Epsilon.thy |
|
80 "[| a: eclose(b); \ |
|
81 \ !!y. [| y: b |] ==> P(y); \ |
|
82 \ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) \ |
|
83 \ |] ==> P(a)"; |
|
84 by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1); |
|
85 by (rtac (CollectI RS subsetI) 2); |
|
86 by (etac (arg_subset_eclose RS subsetD) 2); |
|
87 by (etac base 2); |
|
88 by (rewtac Transset_def); |
|
89 by (fast_tac (ZF_cs addEs [step,ecloseD]) 1); |
|
90 val eclose_induct_down = result(); |
|
91 |
|
92 goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X"; |
|
93 be ([eclose_least, arg_subset_eclose] MRS equalityI) 1; |
|
94 br subset_refl 1; |
|
95 val Transset_eclose_eq_arg = result(); |
|
96 |
|
97 |
|
98 (*** Epsilon recursion ***) |
|
99 |
|
100 (*Unused...*) |
|
101 goal Epsilon.thy "!!A B C. [| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)"; |
|
102 by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1); |
|
103 by (REPEAT (assume_tac 1)); |
|
104 val mem_eclose_trans = result(); |
|
105 |
|
106 (*Variant of the previous lemma in a useable form for the sequel*) |
|
107 goal Epsilon.thy |
|
108 "!!A B C. [| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})"; |
|
109 by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1); |
|
110 by (REPEAT (assume_tac 1)); |
|
111 val mem_eclose_sing_trans = result(); |
|
112 |
|
113 goalw Epsilon.thy [Transset_def] |
|
114 "!!i j. [| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; |
|
115 by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1); |
|
116 val under_Memrel = result(); |
|
117 |
|
118 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
|
119 val under_Memrel_eclose = Transset_eclose RS under_Memrel; |
|
120 |
|
121 val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst); |
|
122 |
|
123 val [kmemj,jmemi] = goal Epsilon.thy |
|
124 "[| k:eclose({j}); j:eclose({i}) |] ==> \ |
|
125 \ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"; |
|
126 by (rtac (kmemj RS eclose_induct) 1); |
|
127 by (rtac wfrec_ssubst 1); |
|
128 by (rtac wfrec_ssubst 1); |
|
129 by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose, |
|
130 jmemi RSN (2,mem_eclose_sing_trans)]) 1); |
|
131 val wfrec_eclose_eq = result(); |
|
132 |
|
133 val [prem] = goal Epsilon.thy |
|
134 "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"; |
|
135 by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1); |
|
136 by (rtac (prem RS arg_into_eclose_sing) 1); |
|
137 val wfrec_eclose_eq2 = result(); |
|
138 |
|
139 goalw Epsilon.thy [transrec_def] |
|
140 "transrec(a,H) = H(a, lam x:a. transrec(x,H))"; |
|
141 by (rtac wfrec_ssubst 1); |
|
142 by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2, |
|
143 arg_in_eclose_sing, under_Memrel_eclose]) 1); |
|
144 val transrec = result(); |
|
145 |
|
146 (*Avoids explosions in proofs; resolve it with a meta-level definition.*) |
|
147 val rew::prems = goal Epsilon.thy |
|
148 "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"; |
|
149 by (rewtac rew); |
|
150 by (REPEAT (resolve_tac (prems@[transrec]) 1)); |
|
151 val def_transrec = result(); |
|
152 |
|
153 val prems = goal Epsilon.thy |
|
154 "[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) \ |
|
155 \ |] ==> transrec(a,H) : B(a)"; |
|
156 by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1); |
|
157 by (rtac (transrec RS ssubst) 1); |
|
158 by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1)); |
|
159 val transrec_type = result(); |
|
160 |
|
161 goal Epsilon.thy "!!i. Ord(i) ==> eclose({i}) <= succ(i)"; |
|
162 by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1); |
|
163 by (rtac (succI1 RS singleton_subsetI) 1); |
|
164 val eclose_sing_Ord = result(); |
|
165 |
|
166 val prems = goal Epsilon.thy |
|
167 "[| j: i; Ord(i); \ |
|
168 \ !!x u. [| x: i; u: Pi(x,B) |] ==> H(x,u) : B(x) \ |
|
169 \ |] ==> transrec(j,H) : B(j)"; |
|
170 by (rtac transrec_type 1); |
|
171 by (resolve_tac prems 1); |
|
172 by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1); |
|
173 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1)); |
|
174 val Ord_transrec_type = result(); |
|
175 |
|
176 (*Congruence*) |
|
177 val prems = goalw Epsilon.thy [transrec_def,Memrel_def] |
|
178 "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> transrec(a,H)=transrec(a',H')"; |
|
179 val transrec_ss = |
|
180 ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"]) |
|
181 addrews (prems RL [sym]); |
|
182 by (SIMP_TAC transrec_ss 1); |
|
183 val transrec_cong = result(); |
|
184 |
|
185 (*** Rank ***) |
|
186 |
|
187 val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]); |
|
188 |
|
189 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
|
190 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))"; |
|
191 by (rtac (rank_def RS def_transrec RS ssubst) 1); |
|
192 by (SIMP_TAC ZF_ss 1); |
|
193 val rank = result(); |
|
194 |
|
195 goal Epsilon.thy "Ord(rank(a))"; |
|
196 by (eps_ind_tac "a" 1); |
|
197 by (rtac (rank RS ssubst) 1); |
|
198 by (rtac (Ord_succ RS Ord_UN) 1); |
|
199 by (etac bspec 1); |
|
200 by (assume_tac 1); |
|
201 val Ord_rank = result(); |
|
202 |
|
203 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i"; |
|
204 by (rtac (major RS trans_induct) 1); |
|
205 by (rtac (rank RS ssubst) 1); |
|
206 by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1); |
|
207 val rank_of_Ord = result(); |
|
208 |
|
209 val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)"; |
|
210 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); |
|
211 by (rtac (prem RS UN_I) 1); |
|
212 by (rtac succI1 1); |
|
213 val rank_lt = result(); |
|
214 |
|
215 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)"; |
|
216 by (rtac (major RS eclose_induct_down) 1); |
|
217 by (etac rank_lt 1); |
|
218 by (etac (rank_lt RS Ord_trans) 1); |
|
219 by (assume_tac 1); |
|
220 by (rtac Ord_rank 1); |
|
221 val eclose_rank_lt = result(); |
|
222 |
|
223 goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)"; |
|
224 by (rtac (rank RS ssubst) 1); |
|
225 by (rtac (rank RS ssubst) 1); |
|
226 by (etac UN_mono 1); |
|
227 by (rtac subset_refl 1); |
|
228 val rank_mono = result(); |
|
229 |
|
230 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))"; |
|
231 by (rtac (rank RS trans) 1); |
|
232 by (rtac equalityI 1); |
|
233 by (fast_tac ZF_cs 2); |
|
234 by (rtac UN_least 1); |
|
235 by (etac (PowD RS rank_mono RS Ord_succ_mono) 1); |
|
236 by (rtac Ord_rank 1); |
|
237 by (rtac Ord_rank 1); |
|
238 val rank_Pow = result(); |
|
239 |
|
240 goal Epsilon.thy "rank(0) = 0"; |
|
241 by (rtac (rank RS trans) 1); |
|
242 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
|
243 val rank_0 = result(); |
|
244 |
|
245 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))"; |
|
246 by (rtac (rank RS trans) 1); |
|
247 br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1; |
|
248 be succE 1; |
|
249 by (fast_tac ZF_cs 1); |
|
250 by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1)); |
|
251 val rank_succ = result(); |
|
252 |
|
253 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))"; |
|
254 by (rtac equalityI 1); |
|
255 by (rtac (rank_mono RS UN_least) 2); |
|
256 by (etac Union_upper 2); |
|
257 by (rtac (rank RS ssubst) 1); |
|
258 by (rtac UN_least 1); |
|
259 by (etac UnionE 1); |
|
260 by (rtac subset_trans 1); |
|
261 by (etac (RepFunI RS Union_upper) 2); |
|
262 by (etac (rank_lt RS Ord_succ_subsetI) 1); |
|
263 by (rtac Ord_rank 1); |
|
264 val rank_Union = result(); |
|
265 |
|
266 goal Epsilon.thy "rank(eclose(a)) = rank(a)"; |
|
267 by (rtac equalityI 1); |
|
268 by (rtac (arg_subset_eclose RS rank_mono) 2); |
|
269 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1); |
|
270 by (rtac UN_least 1); |
|
271 by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1); |
|
272 val rank_eclose = result(); |
|
273 |
|
274 (* [| i: j; j: rank(a) |] ==> i: rank(a) *) |
|
275 val rank_trans = Ord_rank RSN (3, Ord_trans); |
|
276 |
|
277 goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)"; |
|
278 by (rtac (consI1 RS rank_lt RS Ord_trans) 1); |
|
279 by (rtac (consI1 RS consI2 RS rank_lt) 1); |
|
280 by (rtac Ord_rank 1); |
|
281 val rank_pair1 = result(); |
|
282 |
|
283 goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)"; |
|
284 by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1); |
|
285 by (rtac (consI1 RS consI2 RS rank_lt) 1); |
|
286 by (rtac Ord_rank 1); |
|
287 val rank_pair2 = result(); |
|
288 |
|
289 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))"; |
|
290 by (rtac rank_pair2 1); |
|
291 val rank_Inl = result(); |
|
292 |
|
293 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))"; |
|
294 by (rtac rank_pair2 1); |
|
295 val rank_Inr = result(); |
|
296 |
|
297 val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))"; |
|
298 by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1); |
|
299 by (rtac bexI 1); |
|
300 by (etac member_succD 1); |
|
301 by (rtac Ord_rank 1); |
|
302 by (assume_tac 1); |
|
303 val rank_implies_mem = result(); |
|
304 |
|
305 |
|
306 (*** Corollaries of leastness ***) |
|
307 |
|
308 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)"; |
|
309 by (rtac (Transset_eclose RS eclose_least) 1); |
|
310 by (etac (arg_into_eclose RS eclose_subset) 1); |
|
311 val mem_eclose_subset = result(); |
|
312 |
|
313 goal Epsilon.thy "!!A B. A<=B ==> eclose(A) <= eclose(B)"; |
|
314 by (rtac (Transset_eclose RS eclose_least) 1); |
|
315 by (etac subset_trans 1); |
|
316 by (rtac arg_subset_eclose 1); |
|
317 val eclose_mono = result(); |
|
318 |
|
319 (** Idempotence of eclose **) |
|
320 |
|
321 goal Epsilon.thy "eclose(eclose(A)) = eclose(A)"; |
|
322 by (rtac equalityI 1); |
|
323 by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1); |
|
324 by (rtac arg_subset_eclose 1); |
|
325 val eclose_idem = result(); |