--- a/src/HOLCF/Fix.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Fix.ML Fri Jul 24 13:44:27 1998 +0200
@@ -12,24 +12,10 @@
(* derive inductive properties of iterate from primitive recursion *)
(* ------------------------------------------------------------------------ *)
-qed_goal "iterate_0" thy "iterate 0 F x = x"
- (fn prems =>
- [
- (resolve_tac (nat_recs iterate_def) 1)
- ]);
-
-qed_goal "iterate_Suc" thy "iterate (Suc n) F x = F`(iterate n F x)"
- (fn prems =>
- [
- (resolve_tac (nat_recs iterate_def) 1)
- ]);
-
-Addsimps [iterate_0, iterate_Suc];
-
qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
(fn prems =>
[
- (nat_ind_tac "n" 1),
+ (induct_tac "n" 1),
(Simp_tac 1),
(stac iterate_Suc 1),
(stac iterate_Suc 1),
@@ -49,7 +35,7 @@
(cut_facts_tac prems 1),
(strip_tac 1),
(Simp_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(etac monofun_cfun_arg 1)
@@ -103,7 +89,7 @@
(rtac chain_iterate 1),
(rtac ub_rangeI 1),
(strip_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(res_inst_tac [("t","x")] subst 1),
@@ -120,7 +106,7 @@
(fn prems =>
[
(strip_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(rtac (less_fun RS iffD2) 1),
@@ -141,7 +127,7 @@
(fn prems =>
[
(strip_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
(Asm_simp_tac 1),
@@ -185,7 +171,7 @@
[
(rtac monofunI 1),
(strip_tac 1),
- (nat_ind_tac "n" 1),
+ (induct_tac "n" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(etac monofun_cfun_arg 1)
@@ -196,7 +182,7 @@
[
(rtac contlubI 1),
(strip_tac 1),
- (nat_ind_tac "n" 1),
+ (induct_tac "n" 1),
(Simp_tac 1),
(Simp_tac 1),
(res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
@@ -493,7 +479,7 @@
(etac admD 1),
(rtac chain_iterate 1),
(rtac allI 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(stac iterate_0 1),
(atac 1),
(stac iterate_Suc 1),