62 |
62 |
63 goalw Epsilon.thy [Transset_def] |
63 goalw Epsilon.thy [Transset_def] |
64 "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \ |
64 "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \ |
65 \ nat_rec(n, A, %m r. Union(r)) <= X"; |
65 \ nat_rec(n, A, %m r. Union(r)) <= X"; |
66 by (etac nat_induct 1); |
66 by (etac nat_induct 1); |
67 by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1); |
67 by (asm_simp_tac (!simpset addsimps [nat_rec_0]) 1); |
68 by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1); |
68 by (asm_simp_tac (!simpset addsimps [nat_rec_succ]) 1); |
69 by (fast_tac ZF_cs 1); |
69 by (Fast_tac 1); |
70 qed "eclose_least_lemma"; |
70 qed "eclose_least_lemma"; |
71 |
71 |
72 goalw Epsilon.thy [eclose_def] |
72 goalw Epsilon.thy [eclose_def] |
73 "!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X"; |
73 "!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X"; |
74 by (rtac (eclose_least_lemma RS UN_least) 1); |
74 by (rtac (eclose_least_lemma RS UN_least) 1); |
84 by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1); |
84 by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1); |
85 by (rtac (CollectI RS subsetI) 2); |
85 by (rtac (CollectI RS subsetI) 2); |
86 by (etac (arg_subset_eclose RS subsetD) 2); |
86 by (etac (arg_subset_eclose RS subsetD) 2); |
87 by (etac base 2); |
87 by (etac base 2); |
88 by (rewtac Transset_def); |
88 by (rewtac Transset_def); |
89 by (fast_tac (ZF_cs addEs [step,ecloseD]) 1); |
89 by (fast_tac (!claset addEs [step,ecloseD]) 1); |
90 qed "eclose_induct_down"; |
90 qed "eclose_induct_down"; |
91 |
91 |
92 goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X"; |
92 goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X"; |
93 by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1); |
93 by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1); |
94 by (rtac subset_refl 1); |
94 by (rtac subset_refl 1); |
116 qed "under_Memrel"; |
116 qed "under_Memrel"; |
117 |
117 |
118 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
118 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
119 val under_Memrel_eclose = Transset_eclose RS under_Memrel; |
119 val under_Memrel_eclose = Transset_eclose RS under_Memrel; |
120 |
120 |
121 bind_thm ("wfrec_ssubst", wf_Memrel RS wfrec RS ssubst); |
121 val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst); |
122 |
122 |
123 val [kmemj,jmemi] = goal Epsilon.thy |
123 val [kmemj,jmemi] = goal Epsilon.thy |
124 "[| k:eclose({j}); j:eclose({i}) |] ==> \ |
124 "[| k:eclose({j}); j:eclose({i}) |] ==> \ |
125 \ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"; |
125 \ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"; |
126 by (rtac (kmemj RS eclose_induct) 1); |
126 by (rtac (kmemj RS eclose_induct) 1); |
127 by (rtac wfrec_ssubst 1); |
127 by (rtac wfrec_ssubst 1); |
128 by (rtac wfrec_ssubst 1); |
128 by (rtac wfrec_ssubst 1); |
129 by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose, |
129 by (asm_simp_tac (!simpset addsimps [under_Memrel_eclose, |
130 jmemi RSN (2,mem_eclose_sing_trans)]) 1); |
130 jmemi RSN (2,mem_eclose_sing_trans)]) 1); |
131 qed "wfrec_eclose_eq"; |
131 qed "wfrec_eclose_eq"; |
132 |
132 |
133 val [prem] = goal Epsilon.thy |
133 val [prem] = goal Epsilon.thy |
134 "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"; |
134 "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"; |
137 qed "wfrec_eclose_eq2"; |
137 qed "wfrec_eclose_eq2"; |
138 |
138 |
139 goalw Epsilon.thy [transrec_def] |
139 goalw Epsilon.thy [transrec_def] |
140 "transrec(a,H) = H(a, lam x:a. transrec(x,H))"; |
140 "transrec(a,H) = H(a, lam x:a. transrec(x,H))"; |
141 by (rtac wfrec_ssubst 1); |
141 by (rtac wfrec_ssubst 1); |
142 by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing, |
142 by (simp_tac (!simpset addsimps [wfrec_eclose_eq2, arg_in_eclose_sing, |
143 under_Memrel_eclose]) 1); |
143 under_Memrel_eclose]) 1); |
144 qed "transrec"; |
144 qed "transrec"; |
145 |
145 |
146 (*Avoids explosions in proofs; resolve it with a meta-level definition.*) |
146 (*Avoids explosions in proofs; resolve it with a meta-level definition.*) |
147 val rew::prems = goal Epsilon.thy |
147 val rew::prems = goal Epsilon.thy |
176 (*** Rank ***) |
176 (*** Rank ***) |
177 |
177 |
178 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
178 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
179 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))"; |
179 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))"; |
180 by (stac (rank_def RS def_transrec) 1); |
180 by (stac (rank_def RS def_transrec) 1); |
181 by (simp_tac ZF_ss 1); |
181 by (Simp_tac 1); |
182 qed "rank"; |
182 qed "rank"; |
183 |
183 |
184 goal Epsilon.thy "Ord(rank(a))"; |
184 goal Epsilon.thy "Ord(rank(a))"; |
185 by (eps_ind_tac "a" 1); |
185 by (eps_ind_tac "a" 1); |
186 by (stac rank 1); |
186 by (stac rank 1); |
190 qed "Ord_rank"; |
190 qed "Ord_rank"; |
191 |
191 |
192 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i"; |
192 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i"; |
193 by (rtac (major RS trans_induct) 1); |
193 by (rtac (major RS trans_induct) 1); |
194 by (stac rank 1); |
194 by (stac rank 1); |
195 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1); |
195 by (asm_simp_tac (!simpset addsimps [Ord_equality]) 1); |
196 qed "rank_of_Ord"; |
196 qed "rank_of_Ord"; |
197 |
197 |
198 goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)"; |
198 goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)"; |
199 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); |
199 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); |
200 by (etac (UN_I RS ltI) 1); |
200 by (etac (UN_I RS ltI) 1); |
226 REPEAT o rtac (Ord_rank RS Ord_succ)] 1); |
226 REPEAT o rtac (Ord_rank RS Ord_succ)] 1); |
227 qed "rank_Pow"; |
227 qed "rank_Pow"; |
228 |
228 |
229 goal Epsilon.thy "rank(0) = 0"; |
229 goal Epsilon.thy "rank(0) = 0"; |
230 by (rtac (rank RS trans) 1); |
230 by (rtac (rank RS trans) 1); |
231 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
231 by (fast_tac (!claset addSIs [equalityI]) 1); |
232 qed "rank_0"; |
232 qed "rank_0"; |
233 |
233 |
234 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))"; |
234 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))"; |
235 by (rtac (rank RS trans) 1); |
235 by (rtac (rank RS trans) 1); |
236 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1); |
236 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1); |
237 by (etac succE 1); |
237 by (etac succE 1); |
238 by (fast_tac ZF_cs 1); |
238 by (Fast_tac 1); |
239 by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1); |
239 by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1); |
240 qed "rank_succ"; |
240 qed "rank_succ"; |
241 |
241 |
242 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))"; |
242 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))"; |
243 by (rtac equalityI 1); |
243 by (rtac equalityI 1); |
295 goal Epsilon.thy "eclose(eclose(A)) = eclose(A)"; |
295 goal Epsilon.thy "eclose(eclose(A)) = eclose(A)"; |
296 by (rtac equalityI 1); |
296 by (rtac equalityI 1); |
297 by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1); |
297 by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1); |
298 by (rtac arg_subset_eclose 1); |
298 by (rtac arg_subset_eclose 1); |
299 qed "eclose_idem"; |
299 qed "eclose_idem"; |
|
300 |
|
301 (*Transfinite recursion for definitions based on the three cases of ordinals. |
|
302 *) |
|
303 |
|
304 goal thy "transrec2(0,a,b) = a"; |
|
305 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
|
306 by (Simp_tac 1); |
|
307 qed "transrec2_0"; |
|
308 |
|
309 goal thy "(THE j. i=j) = i"; |
|
310 by (fast_tac (!claset addSIs [the_equality]) 1); |
|
311 qed "THE_eq"; |
|
312 |
|
313 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; |
|
314 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
|
315 by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P] |
|
316 setsolver K Fast_tac) 1); |
|
317 qed "transrec2_succ"; |
|
318 |
|
319 goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"; |
|
320 by (rtac (transrec2_def RS def_transrec RS trans) 1); |
|
321 by (resolve_tac [if_not_P RS trans] 1 THEN |
|
322 fast_tac (!claset addSDs [Limit_has_0] addSEs [ltE]) 1); |
|
323 by (resolve_tac [if_not_P RS trans] 1 THEN |
|
324 fast_tac (!claset addSEs [succ_LimitE]) 1); |
|
325 by (Simp_tac 1); |
|
326 qed "transrec2_Limit"; |
|
327 |
|
328 Addsimps [transrec2_0, transrec2_succ]; |