author  paulson 
Wed, 15 May 2002 10:42:32 +0200  
changeset 13149  773657d466cb 
parent 12814  2f5edb146f7e 
permissions  rwrr 
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 

9907  16 
bind_thm ("arg_into_eclose", arg_subset_eclose RS subsetD); 
0  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 

9907  35 
bind_thm ("arg_in_eclose_sing", arg_subset_eclose RS singleton_subsetD); 
36 
bind_thm ("arg_into_eclose_sing", arg_in_eclose_sing RS ecloseD); 

0  37 

38 
(* This is epsiloninduction 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 epsiloninduction 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 *) 

9907  115 
bind_thm ("under_Memrel_eclose", Transset_eclose RS under_Memrel); 
0  116 

9907  117 
bind_thm ("wfrec_ssubst", standard (wf_Memrel RS wfrec RS ssubst)); 
0  118 

9907  119 
val [kmemj,jmemi] = goal (the_context ()) 
0  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 metalevel 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); 

12485  221 
by (auto_tac (claset() addIs [rank_mono], simpset() addsimps [Ord_UN])); 
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 "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; 
2469  315 
by (rtac (transrec2_def RS def_transrec RS trans) 1); 
12814  316 
by (simp_tac (simpset() addsimps [the_equality, if_P]) 1); 
2469  317 
qed "transrec2_succ"; 
318 

5137  319 
Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"; 
2469  320 
by (rtac (transrec2_def RS def_transrec RS trans) 1); 
5137  321 
by (Simp_tac 1); 
4091  322 
by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1); 
2469  323 
qed "transrec2_Limit"; 
324 

325 
Addsimps [transrec2_0, transrec2_succ]; 

3016  326 

6070  327 

328 
(** recursor  better than nat_rec; the succ case has no type requirement! **) 

329 

330 
(*NOT suitable for rewriting*) 

331 
val lemma = recursor_def RS def_transrec RS trans; 

332 

333 
Goal "recursor(a,b,0) = a"; 

334 
by (rtac (nat_case_0 RS lemma) 1); 

335 
qed "recursor_0"; 

336 

337 
Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"; 

338 
by (rtac lemma 1); 

339 
by (Simp_tac 1); 

340 
qed "recursor_succ"; 

341 

342 

343 
(** rec: old version for compatibility **) 

344 

345 
Goalw [rec_def] "rec(0,a,b) = a"; 

346 
by (rtac recursor_0 1); 

347 
qed "rec_0"; 

348 

349 
Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))"; 

350 
by (rtac recursor_succ 1); 

351 
qed "rec_succ"; 

352 

353 
Addsimps [rec_0, rec_succ]; 

354 

355 
val major::prems = Goal 

356 
"[ n: nat; \ 

357 
\ a: C(0); \ 

358 
\ !!m z. [ m: nat; z: C(m) ] ==> b(m,z): C(succ(m)) \ 

359 
\ ] ==> rec(n,a,b) : C(n)"; 

360 
by (rtac (major RS nat_induct) 1); 

361 
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); 

362 
qed "rec_type"; 

363 