1 (* Title: ZF/epsilon.ML |
1 (* Title: ZF/epsilon.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 For epsilon.thy. Epsilon induction and recursion |
6 For epsilon.thy. Epsilon induction and recursion |
7 *) |
7 *) |
8 |
8 |
51 qed "eps_induct"; |
51 qed "eps_induct"; |
52 |
52 |
53 (*Perform epsilon-induction on i. *) |
53 (*Perform epsilon-induction on i. *) |
54 fun eps_ind_tac a = |
54 fun eps_ind_tac a = |
55 EVERY' [res_inst_tac [("a",a)] eps_induct, |
55 EVERY' [res_inst_tac [("a",a)] eps_induct, |
56 rename_last_tac a ["1"]]; |
56 rename_last_tac a ["1"]]; |
57 |
57 |
58 |
58 |
59 (*** Leastness of eclose ***) |
59 (*** Leastness of eclose ***) |
60 |
60 |
61 (** eclose(A) is the least transitive set including A as a subset. **) |
61 (** eclose(A) is the least transitive set including A as a subset. **) |
75 by (REPEAT (assume_tac 1)); |
75 by (REPEAT (assume_tac 1)); |
76 qed "eclose_least"; |
76 qed "eclose_least"; |
77 |
77 |
78 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
78 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
79 val [major,base,step] = goal Epsilon.thy |
79 val [major,base,step] = goal Epsilon.thy |
80 "[| a: eclose(b); \ |
80 "[| a: eclose(b); \ |
81 \ !!y. [| y: b |] ==> P(y); \ |
81 \ !!y. [| y: b |] ==> P(y); \ |
82 \ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) \ |
82 \ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) \ |
83 \ |] ==> P(a)"; |
83 \ |] ==> P(a)"; |
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); |
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 (ZF_ss 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)"; |
135 by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1); |
135 by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1); |
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 (ZF_ss 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 |
148 "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"; |
148 "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"; |
219 |
219 |
220 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))"; |
220 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))"; |
221 by (rtac (rank RS trans) 1); |
221 by (rtac (rank RS trans) 1); |
222 by (rtac le_anti_sym 1); |
222 by (rtac le_anti_sym 1); |
223 by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le), |
223 by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le), |
224 etac (PowD RS rank_mono RS succ_leI)] 1); |
224 etac (PowD RS rank_mono RS succ_leI)] 1); |
225 by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le), |
225 by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le), |
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 (ZF_cs addSIs [equalityI]) 1); |