author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
parent 9211 | 6236c5285bd8 |
child 9907 | 473a6604da94 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/epsilon.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
5809 | 6 |
Epsilon induction and recursion |
0 | 7 |
*) |
8 |
||
9 |
(*** Basic closure properties ***) |
|
10 |
||
5067 | 11 |
Goalw [eclose_def] "A <= eclose(A)"; |
0 | 12 |
by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1); |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
13 |
by (rtac (nat_0I RS UN_upper) 1); |
760 | 14 |
qed "arg_subset_eclose"; |
0 | 15 |
|
16 |
val arg_into_eclose = arg_subset_eclose RS subsetD; |
|
17 |
||
5067 | 18 |
Goalw [eclose_def,Transset_def] "Transset(eclose(A))"; |
0 | 19 |
by (rtac (subsetI RS ballI) 1); |
20 |
by (etac UN_E 1); |
|
21 |
by (rtac (nat_succI RS UN_I) 1); |
|
22 |
by (assume_tac 1); |
|
23 |
by (etac (nat_rec_succ RS ssubst) 1); |
|
24 |
by (etac UnionI 1); |
|
25 |
by (assume_tac 1); |
|
760 | 26 |
qed "Transset_eclose"; |
0 | 27 |
|
28 |
(* x : eclose(A) ==> x <= eclose(A) *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
29 |
bind_thm ("eclose_subset", |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
30 |
rewrite_rule [Transset_def] Transset_eclose RS bspec); |
0 | 31 |
|
32 |
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
33 |
bind_thm ("ecloseD", eclose_subset RS subsetD); |
0 | 34 |
|
35 |
val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD; |
|
36 |
val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD; |
|
37 |
||
38 |
(* This is epsilon-induction for eclose(A); see also eclose_induct_down... |
|
39 |
[| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) |
|
40 |
|] ==> P(a) |
|
41 |
*) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
42 |
bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct)); |
0 | 43 |
|
44 |
(*Epsilon induction*) |
|
9211 | 45 |
val prems = Goal |
0 | 46 |
"[| !!x. ALL y:x. P(y) ==> P(x) |] ==> P(a)"; |
47 |
by (rtac (arg_in_eclose_sing RS eclose_induct) 1); |
|
48 |
by (eresolve_tac prems 1); |
|
760 | 49 |
qed "eps_induct"; |
0 | 50 |
|
51 |
(*Perform epsilon-induction on i. *) |
|
52 |
fun eps_ind_tac a = |
|
53 |
EVERY' [res_inst_tac [("a",a)] eps_induct, |
|
1461 | 54 |
rename_last_tac a ["1"]]; |
0 | 55 |
|
56 |
||
57 |
(*** Leastness of eclose ***) |
|
58 |
||
59 |
(** eclose(A) is the least transitive set including A as a subset. **) |
|
60 |
||
5067 | 61 |
Goalw [Transset_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
62 |
"[| Transset(X); A<=X; n: nat |] ==> \ |
0 | 63 |
\ nat_rec(n, A, %m r. Union(r)) <= X"; |
64 |
by (etac nat_induct 1); |
|
4091 | 65 |
by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1); |
66 |
by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1); |
|
3016 | 67 |
by (Blast_tac 1); |
760 | 68 |
qed "eclose_least_lemma"; |
0 | 69 |
|
5067 | 70 |
Goalw [eclose_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
71 |
"[| Transset(X); A<=X |] ==> eclose(A) <= X"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
72 |
by (rtac (eclose_least_lemma RS UN_least) 1); |
0 | 73 |
by (REPEAT (assume_tac 1)); |
760 | 74 |
qed "eclose_least"; |
0 | 75 |
|
76 |
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
|
9211 | 77 |
val [major,base,step] = Goal |
1461 | 78 |
"[| a: eclose(b); \ |
79 |
\ !!y. [| y: b |] ==> P(y); \ |
|
80 |
\ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) \ |
|
0 | 81 |
\ |] ==> P(a)"; |
82 |
by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1); |
|
83 |
by (rtac (CollectI RS subsetI) 2); |
|
84 |
by (etac (arg_subset_eclose RS subsetD) 2); |
|
85 |
by (etac base 2); |
|
86 |
by (rewtac Transset_def); |
|
4091 | 87 |
by (blast_tac (claset() addIs [step,ecloseD]) 1); |
760 | 88 |
qed "eclose_induct_down"; |
0 | 89 |
|
5137 | 90 |
Goal "Transset(X) ==> eclose(X) = X"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
91 |
by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
92 |
by (rtac subset_refl 1); |
760 | 93 |
qed "Transset_eclose_eq_arg"; |
0 | 94 |
|
95 |
||
96 |
(*** Epsilon recursion ***) |
|
97 |
||
98 |
(*Unused...*) |
|
5137 | 99 |
Goal "[| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)"; |
0 | 100 |
by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1); |
101 |
by (REPEAT (assume_tac 1)); |
|
760 | 102 |
qed "mem_eclose_trans"; |
0 | 103 |
|
104 |
(*Variant of the previous lemma in a useable form for the sequel*) |
|
5268 | 105 |
Goal "[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})"; |
0 | 106 |
by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1); |
107 |
by (REPEAT (assume_tac 1)); |
|
760 | 108 |
qed "mem_eclose_sing_trans"; |
0 | 109 |
|
8201 | 110 |
Goalw [Transset_def] "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; |
111 |
by (Blast_tac 1); |
|
760 | 112 |
qed "under_Memrel"; |
0 | 113 |
|
114 |
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
|
115 |
val under_Memrel_eclose = Transset_eclose RS under_Memrel; |
|
116 |
||
2469 | 117 |
val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst); |
0 | 118 |
|
119 |
val [kmemj,jmemi] = goal Epsilon.thy |
|
120 |
"[| k:eclose({j}); j:eclose({i}) |] ==> \ |
|
121 |
\ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"; |
|
122 |
by (rtac (kmemj RS eclose_induct) 1); |
|
123 |
by (rtac wfrec_ssubst 1); |
|
124 |
by (rtac wfrec_ssubst 1); |
|
4091 | 125 |
by (asm_simp_tac (simpset() addsimps [under_Memrel_eclose, |
1461 | 126 |
jmemi RSN (2,mem_eclose_sing_trans)]) 1); |
760 | 127 |
qed "wfrec_eclose_eq"; |
0 | 128 |
|
9211 | 129 |
Goal |
0 | 130 |
"k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"; |
131 |
by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1); |
|
9211 | 132 |
by (etac arg_into_eclose_sing 1); |
760 | 133 |
qed "wfrec_eclose_eq2"; |
0 | 134 |
|
5067 | 135 |
Goalw [transrec_def] |
0 | 136 |
"transrec(a,H) = H(a, lam x:a. transrec(x,H))"; |
137 |
by (rtac wfrec_ssubst 1); |
|
4091 | 138 |
by (simp_tac (simpset() addsimps [wfrec_eclose_eq2, arg_in_eclose_sing, |
1461 | 139 |
under_Memrel_eclose]) 1); |
760 | 140 |
qed "transrec"; |
0 | 141 |
|
142 |
(*Avoids explosions in proofs; resolve it with a meta-level definition.*) |
|
9211 | 143 |
val rew::prems = Goal |
0 | 144 |
"[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"; |
145 |
by (rewtac rew); |
|
146 |
by (REPEAT (resolve_tac (prems@[transrec]) 1)); |
|
760 | 147 |
qed "def_transrec"; |
0 | 148 |
|
9211 | 149 |
val prems = Goal |
0 | 150 |
"[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) \ |
151 |
\ |] ==> transrec(a,H) : B(a)"; |
|
152 |
by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1); |
|
2033 | 153 |
by (stac transrec 1); |
0 | 154 |
by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1)); |
760 | 155 |
qed "transrec_type"; |
0 | 156 |
|
5137 | 157 |
Goal "Ord(i) ==> eclose({i}) <= succ(i)"; |
0 | 158 |
by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1); |
159 |
by (rtac (succI1 RS singleton_subsetI) 1); |
|
760 | 160 |
qed "eclose_sing_Ord"; |
0 | 161 |
|
9211 | 162 |
val prems = Goal |
0 | 163 |
"[| j: i; Ord(i); \ |
164 |
\ !!x u. [| x: i; u: Pi(x,B) |] ==> H(x,u) : B(x) \ |
|
165 |
\ |] ==> transrec(j,H) : B(j)"; |
|
166 |
by (rtac transrec_type 1); |
|
167 |
by (resolve_tac prems 1); |
|
168 |
by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1); |
|
169 |
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1)); |
|
760 | 170 |
qed "Ord_transrec_type"; |
0 | 171 |
|
172 |
(*** Rank ***) |
|
173 |
||
174 |
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
|
5067 | 175 |
Goal "rank(a) = (UN y:a. succ(rank(y)))"; |
2033 | 176 |
by (stac (rank_def RS def_transrec) 1); |
2469 | 177 |
by (Simp_tac 1); |
760 | 178 |
qed "rank"; |
0 | 179 |
|
5067 | 180 |
Goal "Ord(rank(a))"; |
0 | 181 |
by (eps_ind_tac "a" 1); |
2033 | 182 |
by (stac rank 1); |
0 | 183 |
by (rtac (Ord_succ RS Ord_UN) 1); |
184 |
by (etac bspec 1); |
|
185 |
by (assume_tac 1); |
|
760 | 186 |
qed "Ord_rank"; |
6071 | 187 |
Addsimps [Ord_rank]; |
0 | 188 |
|
9211 | 189 |
Goal "Ord(i) ==> rank(i) = i"; |
190 |
by (etac trans_induct 1); |
|
2033 | 191 |
by (stac rank 1); |
4091 | 192 |
by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1); |
760 | 193 |
qed "rank_of_Ord"; |
0 | 194 |
|
5137 | 195 |
Goal "a:b ==> rank(a) < rank(b)"; |
0 | 196 |
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); |
129 | 197 |
by (etac (UN_I RS ltI) 1); |
6071 | 198 |
by (rtac Ord_UN 2); |
199 |
by Auto_tac; |
|
760 | 200 |
qed "rank_lt"; |
0 | 201 |
|
9211 | 202 |
Goal "a: eclose(b) ==> rank(a) < rank(b)"; |
203 |
by (etac eclose_induct_down 1); |
|
0 | 204 |
by (etac rank_lt 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
205 |
by (etac (rank_lt RS lt_trans) 1); |
0 | 206 |
by (assume_tac 1); |
760 | 207 |
qed "eclose_rank_lt"; |
0 | 208 |
|
5137 | 209 |
Goal "a<=b ==> rank(a) le rank(b)"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
210 |
by (rtac subset_imp_le 1); |
2033 | 211 |
by (stac rank 1); |
212 |
by (stac rank 1); |
|
6071 | 213 |
by Auto_tac; |
760 | 214 |
qed "rank_mono"; |
0 | 215 |
|
5067 | 216 |
Goal "rank(Pow(a)) = succ(rank(a))"; |
0 | 217 |
by (rtac (rank RS trans) 1); |
437 | 218 |
by (rtac le_anti_sym 1); |
6163 | 219 |
by (rtac UN_upper_le 2); |
220 |
by (rtac UN_least_le 1); |
|
6071 | 221 |
by (auto_tac (claset() addIs [rank_mono], simpset())); |
760 | 222 |
qed "rank_Pow"; |
0 | 223 |
|
5067 | 224 |
Goal "rank(0) = 0"; |
0 | 225 |
by (rtac (rank RS trans) 1); |
3016 | 226 |
by (Blast_tac 1); |
760 | 227 |
qed "rank_0"; |
0 | 228 |
|
5067 | 229 |
Goal "rank(succ(x)) = succ(rank(x))"; |
0 | 230 |
by (rtac (rank RS trans) 1); |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
231 |
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
232 |
by (etac succE 1); |
3016 | 233 |
by (Blast_tac 1); |
129 | 234 |
by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1); |
760 | 235 |
qed "rank_succ"; |
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
236 |
Addsimps [rank_0, rank_succ]; |
0 | 237 |
|
5067 | 238 |
Goal "rank(Union(A)) = (UN x:A. rank(x))"; |
0 | 239 |
by (rtac equalityI 1); |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
240 |
by (rtac (rank_mono RS le_imp_subset RS UN_least) 2); |
0 | 241 |
by (etac Union_upper 2); |
2033 | 242 |
by (stac rank 1); |
0 | 243 |
by (rtac UN_least 1); |
244 |
by (etac UnionE 1); |
|
245 |
by (rtac subset_trans 1); |
|
246 |
by (etac (RepFunI RS Union_upper) 2); |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
247 |
by (etac (rank_lt RS succ_leI RS le_imp_subset) 1); |
760 | 248 |
qed "rank_Union"; |
0 | 249 |
|
5067 | 250 |
Goal "rank(eclose(a)) = rank(a)"; |
437 | 251 |
by (rtac le_anti_sym 1); |
0 | 252 |
by (rtac (arg_subset_eclose RS rank_mono) 2); |
253 |
by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1); |
|
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
254 |
by (rtac (Ord_rank RS UN_least_le) 1); |
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
255 |
by (etac (eclose_rank_lt RS succ_leI) 1); |
760 | 256 |
qed "rank_eclose"; |
0 | 257 |
|
5067 | 258 |
Goalw [Pair_def] "rank(a) < rank(<a,b>)"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
259 |
by (rtac (consI1 RS rank_lt RS lt_trans) 1); |
0 | 260 |
by (rtac (consI1 RS consI2 RS rank_lt) 1); |
760 | 261 |
qed "rank_pair1"; |
0 | 262 |
|
5067 | 263 |
Goalw [Pair_def] "rank(b) < rank(<a,b>)"; |
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset
|
264 |
by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1); |
0 | 265 |
by (rtac (consI1 RS consI2 RS rank_lt) 1); |
760 | 266 |
qed "rank_pair2"; |
0 | 267 |
|
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
268 |
(*Not clear how to remove the P(a) condition, since the "then" part |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
269 |
must refer to "a"*) |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
270 |
Goal "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
271 |
by (asm_simp_tac (simpset() addsimps [the_0, the_equality2]) 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
272 |
qed "the_equality_if"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
273 |
|
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
274 |
(*The premise is needed not just to fix i but to ensure f~=0*) |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
275 |
Goalw [apply_def] "i : domain(f) ==> rank(f`i) < rank(f)"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
276 |
by (Clarify_tac 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
277 |
by (subgoal_tac "rank(y) < rank(f)" 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
278 |
by (blast_tac (claset() addIs [lt_trans, rank_lt, rank_pair2]) 2); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
279 |
by (subgoal_tac "0 < rank(f)" 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
280 |
by (etac (Ord_rank RS Ord_0_le RS lt_trans1) 2); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
281 |
by (asm_simp_tac (simpset() addsimps [the_equality_if]) 1); |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
282 |
qed "rank_apply"; |
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
283 |
|
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6163
diff
changeset
|
284 |
|
0 | 285 |
(*** Corollaries of leastness ***) |
286 |
||
5137 | 287 |
Goal "A:B ==> eclose(A)<=eclose(B)"; |
0 | 288 |
by (rtac (Transset_eclose RS eclose_least) 1); |
289 |
by (etac (arg_into_eclose RS eclose_subset) 1); |
|
760 | 290 |
qed "mem_eclose_subset"; |
0 | 291 |
|
5137 | 292 |
Goal "A<=B ==> eclose(A) <= eclose(B)"; |
0 | 293 |
by (rtac (Transset_eclose RS eclose_least) 1); |
294 |
by (etac subset_trans 1); |
|
295 |
by (rtac arg_subset_eclose 1); |
|
760 | 296 |
qed "eclose_mono"; |
0 | 297 |
|
298 |
(** Idempotence of eclose **) |
|
299 |
||
5067 | 300 |
Goal "eclose(eclose(A)) = eclose(A)"; |
0 | 301 |
by (rtac equalityI 1); |
302 |
by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1); |
|
303 |
by (rtac arg_subset_eclose 1); |
|
760 | 304 |
qed "eclose_idem"; |
2469 | 305 |
|
6070 | 306 |
(** Transfinite recursion for definitions based on the |
307 |
three cases of ordinals **) |
|
2469 | 308 |
|
5067 | 309 |
Goal "transrec2(0,a,b) = a"; |
2469 | 310 |
by (rtac (transrec2_def RS def_transrec RS trans) 1); |
311 |
by (Simp_tac 1); |
|
312 |
qed "transrec2_0"; |
|
313 |
||
5067 | 314 |
Goal "(THE j. i=j) = i"; |
5505 | 315 |
by (Blast_tac 1); |
2469 | 316 |
qed "THE_eq"; |
317 |
||
5067 | 318 |
Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; |
2469 | 319 |
by (rtac (transrec2_def RS def_transrec RS trans) 1); |
8201 | 320 |
by (simp_tac (simpset() addsimps [THE_eq, if_P]) 1); |
3016 | 321 |
by (Blast_tac 1); |
2469 | 322 |
qed "transrec2_succ"; |
323 |
||
5137 | 324 |
Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"; |
2469 | 325 |
by (rtac (transrec2_def RS def_transrec RS trans) 1); |
5137 | 326 |
by (Simp_tac 1); |
4091 | 327 |
by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1); |
2469 | 328 |
qed "transrec2_Limit"; |
329 |
||
330 |
Addsimps [transrec2_0, transrec2_succ]; |
|
3016 | 331 |
|
6070 | 332 |
|
333 |
(** recursor -- better than nat_rec; the succ case has no type requirement! **) |
|
334 |
||
335 |
(*NOT suitable for rewriting*) |
|
336 |
val lemma = recursor_def RS def_transrec RS trans; |
|
337 |
||
338 |
Goal "recursor(a,b,0) = a"; |
|
339 |
by (rtac (nat_case_0 RS lemma) 1); |
|
340 |
qed "recursor_0"; |
|
341 |
||
342 |
Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"; |
|
343 |
by (rtac lemma 1); |
|
344 |
by (Simp_tac 1); |
|
345 |
qed "recursor_succ"; |
|
346 |
||
347 |
||
348 |
(** rec: old version for compatibility **) |
|
349 |
||
350 |
Goalw [rec_def] "rec(0,a,b) = a"; |
|
351 |
by (rtac recursor_0 1); |
|
352 |
qed "rec_0"; |
|
353 |
||
354 |
Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))"; |
|
355 |
by (rtac recursor_succ 1); |
|
356 |
qed "rec_succ"; |
|
357 |
||
358 |
Addsimps [rec_0, rec_succ]; |
|
359 |
||
360 |
val major::prems = Goal |
|
361 |
"[| n: nat; \ |
|
362 |
\ a: C(0); \ |
|
363 |
\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \ |
|
364 |
\ |] ==> rec(n,a,b) : C(n)"; |
|
365 |
by (rtac (major RS nat_induct) 1); |
|
366 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
|
367 |
qed "rec_type"; |
|
368 |