# HG changeset patch
# User paulson
# Date 915730255 -3600
# Node ID 032babd0120b0e43d52e2699f6816677ae0d0a31
# Parent  a99879bd9f1344565c3b24ebc5c54dfa088519ec
ZF: the natural numbers as a datatype

diff -r a99879bd9f13 -r 032babd0120b NEWS
--- a/NEWS	Thu Jan 07 11:08:29 1999 +0100
+++ b/NEWS	Thu Jan 07 18:30:55 1999 +0100
@@ -61,10 +61,10 @@
 *** ZF ***
 
 * new primrec section allows primitive recursive functions to be given
-  directly, as in HOL;
+  directly (as in HOL) over datatypes and the natural numbers;
 
 * new tactics induct_tac and exhaust_tac for induction (or case analysis)
-  on a datatype;
+  over datatypes and the natural numbers;
 
 * the datatype declaration of type T now defines the recursor T_rec;
 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/AC10_AC15.ML
--- a/src/ZF/AC/AC10_AC15.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC10_AC15.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -197,8 +197,8 @@
 (* AC13(m) ==> AC13(n) for m <= n                                         *)
 (* ********************************************************************** *)
 
-Goalw AC_defs "[| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)";
-by (dtac nat_le_imp_lepoll 1 THEN REPEAT (assume_tac 1));
+Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)";
+by (dtac le_imp_lepoll 1);
 by (fast_tac (claset() addSEs [lepoll_trans]) 1);
 qed "AC13_mono";
 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
   The proof of AC16(n, k) ==> WO4(n-k)
 *)
 
-open AC16_WO4;
-
 (* ********************************************************************** *)
 (* The case of finite set                                                 *)
 (* ********************************************************************** *)
@@ -150,7 +148,7 @@
 
 Goal "[| k:nat; m:nat |] ==>  \
 \       ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
-by (eres_inst_tac [("n","k")] nat_induct 1);
+by (induct_tac "k" 1);
 by (simp_tac (simpset() addsimps [add_0]) 1);
 by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS
         (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1);
@@ -180,7 +178,7 @@
 
 Goal "[| k:nat; m:nat |] ==>  \
 \       ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m";
-by (eres_inst_tac [("n","k")] nat_induct 1);
+by (induct_tac "k" 1);
 by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0]
         addss (simpset() addsimps [add_0])) 1);
 by (REPEAT (resolve_tac [allI,impI] 1));
@@ -419,9 +417,9 @@
 qed "well_ord_subsets_eqpoll_n";
 
 Goal "n:nat ==> EX R. well_ord({z:Pow(y). z lepoll n}, R)";
-by (etac nat_induct 1);
-by (fast_tac (claset() addSIs [well_ord_unit]
-        addss (simpset() addsimps [subsets_lepoll_0_eq_unit])) 1);
+by (induct_tac "n" 1);
+by (force_tac (claset() addSIs [well_ord_unit],
+	       simpset() addsimps [subsets_lepoll_0_eq_unit]) 1);
 by (etac exE 1);
 by (resolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 THEN assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [subsets_lepoll_succ]) 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/AC16_lemmas.ML
--- a/src/ZF/AC/AC16_lemmas.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC16_lemmas.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
 Lemmas used in the proofs concerning AC16
 *)
 
-open AC16_lemmas;
-
 Goal "a~:A ==> cons(a,A)-{a}=A";
 by (Fast_tac 1);
 qed "cons_Diff_eq";
@@ -126,7 +124,7 @@
 
 Goal "n:nat ==>  \
 \       ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
 by (etac natE 1);
@@ -189,7 +187,7 @@
 
 Goal "[| InfCard(X); n:nat |]  \
 \       ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (rtac subsets_eqpoll_1_eqpoll 1);
 by (rtac eqpollI 1);
 by (resolve_tac [subsets_lepoll_lemma1 RS lepoll_trans] 1 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -16,23 +16,6 @@
  
 val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
  
-(* ******************************************** *)
-
-(* Theorems analogous to ones presented in "ZF/Ordinal.ML" *)
-
-(* lemma for nat_le_imp_lepoll *)
-val [prem] = goalw Cardinal.thy [lepoll_def]
-             "m:nat ==> ALL n: nat. m le n --> m lepoll n";
-by (nat_ind_tac "m" [prem] 1);
-by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("n","n")] natE 1);
-by (asm_simp_tac (simpset() addsimps [inj_def, succI1 RS Pi_empty2]) 1);
-by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1);
-qed "nat_le_imp_lepoll_lemma";
-
-(* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*)
-val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard;
 
 (* ********************************************************************** *)
 (*             lemmas concerning FOL and pure ZF theory                   *)
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
 Auxiliary lemmas concerning cardinalities
 *)
 
-open Cardinal_aux;
-
 (* ********************************************************************** *)
 (* Lemmas involving ordinals and cardinalities used in the proofs         *)
 (* concerning AC16 and DC                                                 *)
@@ -113,7 +111,7 @@
 
 Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==>  \
 \       ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (rtac allI 1);
 by (rtac impI 1);
 by (res_inst_tac [("b","UN b:a. f`b")] subst 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/DC.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
 The proofs concerning the Axiom of Dependent Choice
 *)
 
-open DC;
-
 (* ********************************************************************** *)
 (* DC ==> DC(omega)                                                       *)
 (*                                                                        *)
@@ -80,7 +78,7 @@
 Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR;  f: nat -> XX;  n:nat |]  \
 \     ==> EX k:nat. f`succ(n) : k -> X & n:k  \
 \                 & <f`succ(n)``n, f`succ(n)`n> : R";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (dresolve_tac [nat_1I RSN (2, apply_type)] 1);
 by (dresolve_tac [nat_0I RSN (2, bspec)] 1);
 by (asm_full_simp_tac (simpset() addsimps [XX_def]) 1);
@@ -112,7 +110,7 @@
 \     ==>  {f`succ(x)`x. x:m} = {f`succ(m)`x. x:m}";
 by (subgoal_tac "ALL x:m. f`succ(m)`x = f`succ(x)`x" 1);
 by (Asm_full_simp_tac 1);
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
 by (Fast_tac 1);
 by (rtac ballI 1);
 by (etac succE 1);
@@ -207,7 +205,7 @@
 qed "lesspoll_nat_is_Finite";
 
 Goal "n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (rtac allI 1);
 by (fast_tac (claset() addSIs [Fin.emptyI]
         addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/WO1_WO6.ML
--- a/src/ZF/AC/WO1_WO6.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/WO1_WO6.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -61,10 +61,9 @@
 
 (* ********************************************************************** *)
 
-Goalw WO_defs "[| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
-by (rtac allI 1);
-by (dtac spec 1);
-by (blast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
+Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)";
+by (blast_tac (claset() addSDs [spec] 
+                        addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1);
 qed "WO4_mono";
 
 (* ********************************************************************** *)
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/WO2_AC16.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -137,7 +137,7 @@
 
 Goal "n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
 \       --> Finite(Union(X))";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]
         addSIs [nat_0I RS nat_into_Finite] addss (simpset())) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
@@ -396,7 +396,7 @@
 
 
 Goal "m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
 by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
 by (REPEAT (etac conjE 1));
diff -r a99879bd9f13 -r 032babd0120b src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/WO6_WO1.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -411,8 +411,7 @@
 val [prem1, prem2] = goal thy
         "[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |]  \
 \       ==> n~=0 --> P(n) --> P(1)";
-by (res_inst_tac [("n","n")] nat_induct 1);
-by (rtac prem1 1);
+by (rtac (prem1 RS nat_induct) 1);
 by (Blast_tac 1);
 by (excluded_middle_tac "x=0" 1);
 by (Blast_tac 2);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Arith.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -6,50 +6,20 @@
 Arithmetic operators and their definitions
 
 Proofs about elementary arithmetic: addition, multiplication, etc.
-
-Could prove def_rec_0, def_rec_succ...
 *)
 
-open Arith;
-
 (*"Difference" is subtraction of natural numbers.
   There are no negative numbers; we have
      m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
   Also, rec(m, 0, %z w.z) is pred(m).   
 *)
 
-(** rec -- better than nat_rec; the succ case has no type requirement! **)
-
-val rec_trans = rec_def RS def_transrec RS trans;
-
-Goal "rec(0,a,b) = a";
-by (rtac rec_trans 1);
-by (rtac nat_case_0 1);
-qed "rec_0";
-
-Goal "rec(succ(m),a,b) = b(m, rec(m,a,b))";
-by (rtac rec_trans 1);
-by (Simp_tac 1);
-qed "rec_succ";
-
-Addsimps [rec_0, rec_succ];
-
-val major::prems = Goal
-    "[| n: nat;  \
-\       a: C(0);  \
-\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
-\    |] ==> rec(n,a,b) : C(n)";
-by (rtac (major RS nat_induct) 1);
-by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps prems)));
-qed "rec_type";
-
 Addsimps [rec_type, nat_0_le, nat_le_refl];
 val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
 
 Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
 by (etac rev_mp 1);
-by (etac nat_induct 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Blast_tac 1);
 val lemma = result();
@@ -60,63 +30,46 @@
 
 (** Addition **)
 
-qed_goalw "add_type" Arith.thy [add_def]
-    "[| m:nat;  n:nat |] ==> m #+ n : nat"
- (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
-
-qed_goalw "add_0" Arith.thy [add_def]
-    "0 #+ n = n"
- (fn _ => [ (rtac rec_0 1) ]);
-
-qed_goalw "add_succ" Arith.thy [add_def]
-    "succ(m) #+ n = succ(m #+ n)"
- (fn _=> [ (rtac rec_succ 1) ]); 
-
-Addsimps [add_0, add_succ];
+Goal "[| m:nat;  n:nat |] ==> m #+ n : nat";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_type";
+Addsimps [add_type];
 
 (** Multiplication **)
 
-qed_goalw "mult_type" Arith.thy [mult_def]
-    "[| m:nat;  n:nat |] ==> m #* n : nat"
- (fn prems=>
-  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
+Goal "[| m:nat;  n:nat |] ==> m #* n : nat";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "mult_type";
+Addsimps [mult_type];
 
-qed_goalw "mult_0" Arith.thy [mult_def]
-    "0 #* n = 0"
- (fn _ => [ (rtac rec_0 1) ]);
-
-qed_goalw "mult_succ" Arith.thy [mult_def]
-    "succ(m) #* n = n #+ (m #* n)"
- (fn _ => [ (rtac rec_succ 1) ]); 
-
-Addsimps [mult_0, mult_succ];
 
 (** Difference **)
 
-qed_goalw "diff_type" Arith.thy [diff_def]
-    "[| m:nat;  n:nat |] ==> m #- n : nat"
- (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
+Goal "[| m:nat;  n:nat |] ==> m #- n : nat";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (fast_tac (claset() addIs [nat_case_type]) 1);
+qed "diff_type";
+Addsimps [diff_type];
 
-qed_goalw "diff_0" Arith.thy [diff_def]
-    "m #- 0 = m"
- (fn _ => [ (rtac rec_0 1) ]);
+Goal "n:nat ==> 0 #- n = 0";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "diff_0_eq_0";
 
-qed_goalw "diff_0_eq_0" Arith.thy [diff_def]
-    "n:nat ==> 0 #- n = 0"
- (fn [prem]=>
-  [ (rtac (prem RS nat_induct) 1),
-    (ALLGOALS (Asm_simp_tac)) ]);
+(*Must simplify BEFORE the induction: else we get a critical pair*)
+Goal "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n";
+by (Asm_simp_tac 1);
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "diff_succ_succ";
 
-(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
-  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
-qed_goalw "diff_succ_succ" Arith.thy [diff_def]
-    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
- (fn prems=>
-  [ (asm_simp_tac (simpset() addsimps prems) 1),
-    (nat_ind_tac "n" prems 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Addsimps [diff_0_eq_0, diff_succ_succ];
 
-Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
+(*This defining property is no longer wanted*)
+Delsimps [diff_SUCC];  
 
 val prems = goal Arith.thy 
     "[| m:nat;  n:nat |] ==> m #- n le m";
@@ -129,72 +82,64 @@
 (*** Simplification over add, mult, diff ***)
 
 val arith_typechecks = [add_type, mult_type, diff_type];
-Addsimps arith_typechecks;
 
 
 (*** Addition ***)
 
 (*Associative law for addition*)
-qed_goal "add_assoc" Arith.thy 
-    "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
- (fn prems=>
-  [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Goal "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_assoc";
 
 (*The following two lemmas are used for add_commute and sometimes
   elsewhere, since they are safe for rewriting.*)
-qed_goal "add_0_right" Arith.thy
-    "m:nat ==> m #+ 0 = m"
- (fn prems=>
-  [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); 
+Goal "m:nat ==> m #+ 0 = m";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_0_right";
 
-qed_goal "add_succ_right" Arith.thy
-    "m:nat ==> m #+ succ(n) = succ(m #+ n)"
- (fn prems=>
-  [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]); 
+Goal "m:nat ==> m #+ succ(n) = succ(m #+ n)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_succ_right";
 
 Addsimps [add_0_right, add_succ_right];
 
 (*Commutative law for addition*)  
-qed_goal "add_commute" Arith.thy 
-    "!!m n. [| m:nat;  n:nat |] ==> m #+ n = n #+ m"
- (fn _ =>
-  [ (nat_ind_tac "n" [] 1),
-    (ALLGOALS Asm_simp_tac) ]);
+Goal "[| m:nat;  n:nat |] ==> m #+ n = n #+ m";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "add_commute";
 
 (*for a/c rewriting*)
-qed_goal "add_left_commute" Arith.thy
-    "!!m n k. [| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)"
- (fn _ => [asm_simp_tac(simpset() addsimps [add_assoc RS sym, add_commute]) 1]);
+Goal "[| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)";
+by (asm_simp_tac (simpset() addsimps [add_assoc RS sym, add_commute]) 1);
+qed "add_left_commute";
 
 (*Addition is an AC-operator*)
 val add_ac = [add_assoc, add_commute, add_left_commute];
 
 (*Cancellation law on the left*)
-val [eqn,knat] = goal Arith.thy 
-    "[| k #+ m = k #+ n;  k:nat |] ==> m=n";
-by (rtac (eqn RS rev_mp) 1);
-by (nat_ind_tac "k" [knat] 1);
-by (ALLGOALS (Simp_tac));
+Goal "[| k #+ m = k #+ n;  k:nat |] ==> m=n";
+by (etac rev_mp 1);
+by (induct_tac "k" 1);
+by Auto_tac;
 qed "add_left_cancel";
 
 (*** Multiplication ***)
 
 (*right annihilation in product*)
-qed_goal "mult_0_right" Arith.thy 
-    "!!m. m:nat ==> m #* 0 = 0"
- (fn _=>
-  [ (nat_ind_tac "m" [] 1),
-    (ALLGOALS (Asm_simp_tac))  ]);
+Goal "m:nat ==> m #* 0 = 0";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "mult_0_right";
 
 (*right successor law for multiplication*)
-qed_goal "mult_succ_right" Arith.thy 
-    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
- (fn _ =>
-  [ (nat_ind_tac "m" [] 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac))) ]);
+Goal "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
+qed "mult_succ_right";
 
 Addsimps [mult_0_right, mult_succ_right];
 
@@ -206,53 +151,49 @@
 by (Asm_simp_tac 1);
 qed "mult_1_right";
 
+Addsimps [mult_1, mult_1_right];
+
 (*Commutative law for multiplication*)
-qed_goal "mult_commute" Arith.thy 
-    "!!m n. [| m:nat;  n:nat |] ==> m #* n = n #* m"
- (fn _=>
-  [ (nat_ind_tac "m" [] 1),
-    (ALLGOALS Asm_simp_tac) ]);
+Goal "[| m:nat;  n:nat |] ==> m #* n = n #* m";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "mult_commute";
 
 (*addition distributes over multiplication*)
-qed_goal "add_mult_distrib" Arith.thy 
-    "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
- (fn _=>
-  [ (etac nat_induct 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))) ]);
+Goal "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
+qed "add_mult_distrib";
 
 (*Distributive law on the left; requires an extra typing premise*)
-qed_goal "add_mult_distrib_left" Arith.thy 
-    "!!m. [| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
- (fn prems=>
-  [ (nat_ind_tac "m" [] 1),
-    (Asm_simp_tac 1),
-    (asm_simp_tac (simpset() addsimps add_ac) 1) ]);
+Goal "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
+qed "add_mult_distrib_left";
 
 (*Associative law for multiplication*)
-qed_goal "mult_assoc" Arith.thy 
-    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
- (fn _=>
-  [ (etac nat_induct 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))) ]);
+Goal "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
+qed "mult_assoc";
 
 (*for a/c rewriting*)
-qed_goal "mult_left_commute" Arith.thy 
-    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)"
- (fn _ => [rtac (mult_commute RS trans) 1, 
-           rtac (mult_assoc RS trans) 3, 
-           rtac (mult_commute RS subst_context) 6,
-           REPEAT (ares_tac [mult_type] 1)]);
+Goal "[| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)";
+by (rtac (mult_commute RS trans) 1);
+by (rtac (mult_assoc RS trans) 3);
+by (rtac (mult_commute RS subst_context) 6);
+by (REPEAT (ares_tac [mult_type] 1));
+qed "mult_left_commute";
 
 val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
 
 
 (*** Difference ***)
 
-qed_goal "diff_self_eq_0" Arith.thy 
-    "m:nat ==> m #- m = 0"
- (fn prems=>
-  [ (nat_ind_tac "m" prems 1),
-    (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Goal "m:nat ==> m #- m = 0";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "diff_self_eq_0";
 
 (*Addition is the inverse of subtraction*)
 Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
@@ -287,10 +228,9 @@
 
 (** Subtraction is the inverse of addition. **)
 
-val [mnat,nnat] = goal Arith.thy
-    "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
-by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
+Goal "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
+by (induct_tac "n" 1);
+by Auto_tac;
 qed "diff_add_inverse";
 
 Goal "[| m:nat;  n:nat |] ==> (m#+n) #- n = m";
@@ -299,7 +239,7 @@
 qed "diff_add_inverse2";
 
 Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n";
-by (nat_ind_tac "k" [] 1);
+by (induct_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_cancel";
 
@@ -308,10 +248,9 @@
 by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
 qed "diff_cancel2";
 
-val [mnat,nnat] = goal Arith.thy
-    "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
-by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
+Goal "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
+by (induct_tac "n" 1);
+by Auto_tac;
 qed "diff_add_0";
 
 (** Difference distributes over multiplication **)
@@ -334,7 +273,7 @@
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
 qed "div_termination";
 
 val div_rls =   (*for mod and div*)
@@ -342,8 +281,8 @@
     [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
      nat_into_Ord, not_lt_iff_le RS iffD1];
 
-val div_ss = (simpset()) addsimps [nat_into_Ord, div_termination RS ltD,
-                                  not_lt_iff_le RS iffD2];
+val div_ss = simpset() addsimps [nat_into_Ord, div_termination RS ltD,
+				 not_lt_iff_le RS iffD2];
 
 (*Type checking depends upon termination!*)
 Goalw [mod_def] "[| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
@@ -442,7 +381,7 @@
 qed "mod2_succ_succ";
 
 Goal "m:nat ==> (m#+m) mod 2 = 0";
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
 by (simp_tac (simpset() addsimps [mod_less]) 1);
 by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1);
 qed "mod2_add_self";
@@ -451,7 +390,7 @@
 (**** Additional theorems about "le" ****)
 
 Goal "[| m:nat;  n:nat |] ==> m le m #+ n";
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_le_self";
 
@@ -510,7 +449,7 @@
 
 Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
 by (forward_tac [lt_nat_in_nat] 1);
-by (nat_ind_tac "k" [] 2);
+by (induct_tac "k" 2);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
 qed "mult_le_mono1";
 
@@ -529,7 +468,7 @@
 by (etac zero_lt_natE 1);
 by (forward_tac [lt_nat_in_nat] 2);
 by (ALLGOALS Asm_simp_tac);
-by (nat_ind_tac "x" [] 1);
+by (induct_tac "x" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
 qed "mult_lt_mono2";
 
@@ -571,38 +510,28 @@
                          div_termination RS ltD]) 1);
 qed "mult_mod_distrib";
 
-(** Lemma for gcd **)
-
-val mono_lemma = (nat_into_Ord RS Ord_0_lt) RSN (2,mult_lt_mono2);
-
+(*Lemma for gcd*)
 Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
 by (rtac disjCI 1);
 by (dtac sym 1);
 by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (fast_tac (claset() addss (simpset())) 1);
-by (fast_tac (le_cs addDs [mono_lemma] 
-                    addss (simpset() addsimps [mult_1_right])) 1);
+by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2);
+by Auto_tac;
 qed "mult_eq_self_implies_10";
 
-
 (*Thanks to Sten Agerholm*)
 Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
 by (etac rev_mp 1);
-by (eres_inst_tac [("n","n")] nat_induct 1);
+by (induct_tac "m" 1);
 by (Asm_simp_tac 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1);
-by (etac lt_asym 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [le_iff, nat_into_Ord]) 1);
-by (Blast_tac 1);
 qed "add_le_elim1";
 
 Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
 by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
 be rev_mp 1;
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
 by (blast_tac (claset() addSEs [leE] 
                         addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Arith.thy	Thu Jan 07 18:30:55 1999 +0100
@@ -7,20 +7,37 @@
 *)
 
 Arith = Epsilon + 
+
+setup setup_datatypes
+
+(*The natural numbers as a datatype*)
+rep_datatype 
+  elim		natE
+  induct	nat_induct
+  case_eqns	nat_case_0, nat_case_succ
+  recursor_eqns recursor_0, recursor_succ
+
+
 consts
-    rec  :: [i, i, [i,i]=>i]=>i
     "#*" :: [i,i]=>i                    (infixl 70)
     div  :: [i,i]=>i                    (infixl 70) 
     mod  :: [i,i]=>i                    (infixl 70)
     "#+" :: [i,i]=>i                    (infixl 65)
     "#-" :: [i,i]=>i                    (infixl 65)
 
-defs
-    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+primrec
+  add_0     "0 #+ n = n"
+  add_succ  "succ(m) #+ n = succ(m #+ n)"
+
+primrec
+  diff_0     "m #- 0 = m"
+  diff_SUCC  "m #- succ(n) = nat_case(0, %x. x, m #- n)"
 
-    add_def  "m#+n == rec(m, n, %u v. succ(v))"
-    diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y. x))"
-    mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
-    mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
-    div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
+primrec
+  mult_0    "0 #* n = 0"
+  mult_succ "succ(m) #* n = n #+ (m #* n)"
+ 
+defs
+    mod_def  "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
+    div_def  "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
 end
diff -r a99879bd9f13 -r 032babd0120b src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/CardinalArith.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -59,6 +59,7 @@
 by (asm_simp_tac (simpset() addsimps [sum_0_eqpoll RS cardinal_cong, 
 				      Card_cardinal_eq]) 1);
 qed "cadd_0";
+Addsimps [cadd_0];
 
 (** Addition by another cardinal **)
 
@@ -120,10 +121,8 @@
 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
 qed "cadd_succ_lemma";
 
-val [mnat,nnat] = goal CardinalArith.thy
-    "[| m: nat;  n: nat |] ==> m |+| n = m#+n";
-by (cut_facts_tac [nnat] 1);
-by (nat_ind_tac "m" [mnat] 1);
+Goal "[| m: nat;  n: nat |] ==> m |+| n = m#+n";
+by (induct_tac "m" 1);
 by (asm_simp_tac (simpset() addsimps [nat_into_Card RS cadd_0]) 1);
 by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cadd_succ_lemma,
 				      nat_into_Card RS Card_cardinal_eq]) 1);
@@ -198,6 +197,7 @@
 by (asm_simp_tac (simpset() addsimps [prod_0_eqpoll RS cardinal_cong, 
 				      Card_0 RS Card_cardinal_eq]) 1);
 qed "cmult_0";
+Addsimps [cmult_0];
 
 (** 1 is the identity for multiplication **)
 
@@ -210,6 +210,7 @@
 by (asm_simp_tac (simpset() addsimps [prod_singleton_eqpoll RS cardinal_cong, 
 				      Card_cardinal_eq]) 1);
 qed "cmult_1";
+Addsimps [cmult_1];
 
 (*** Some inequalities for multiplication ***)
 
@@ -285,19 +286,16 @@
 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
 qed "cmult_succ_lemma";
 
-val [mnat,nnat] = goal CardinalArith.thy
-    "[| m: nat;  n: nat |] ==> m |*| n = m#*n";
-by (cut_facts_tac [nnat] 1);
-by (nat_ind_tac "m" [mnat] 1);
-by (asm_simp_tac (simpset() addsimps [cmult_0]) 1);
+Goal "[| m: nat;  n: nat |] ==> m |*| n = m#*n";
+by (induct_tac "m" 1);
+by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cmult_succ_lemma,
 				      nat_cadd_eq_add]) 1);
 qed "nat_cmult_eq_mult";
 
 Goal "Card(n) ==> 2 |*| n = n |+| n";
 by (asm_simp_tac 
-    (simpset() addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, 
-			 Card_is_Ord, cadd_0,
+    (simpset() addsimps [Ord_0, Ord_succ, cmult_succ_lemma, Card_is_Ord,
 			 read_instantiate [("j","0")] cadd_commute]) 1);
 qed "cmult_2";
 
@@ -708,7 +706,7 @@
 (*** Finite sets ***)
 
 Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
 by (Clarify_tac 1);
 by (subgoal_tac "EX u. u:A" 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Datatype.thy	Thu Jan 07 18:30:55 1999 +0100
@@ -8,9 +8,4 @@
 	"Datatype" must be capital to avoid conflicts with ML's "datatype"
 *)
 
-Datatype = Inductive + Univ + QUniv +
-
-setup setup_datatypes
-
-end
-
+Datatype = Inductive + Univ + QUniv
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Epsilon.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -287,7 +287,8 @@
 by (rtac arg_subset_eclose 1);
 qed "eclose_idem";
 
-(*Transfinite recursion for definitions based on the three cases of ordinals*)
+(** Transfinite recursion for definitions based on the 
+    three cases of ordinals **)
 
 Goal "transrec2(0,a,b) = a";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
@@ -312,3 +313,40 @@
 
 Addsimps [transrec2_0, transrec2_succ];
 
+
+(** recursor -- better than nat_rec; the succ case has no type requirement! **)
+
+(*NOT suitable for rewriting*)
+val lemma = recursor_def RS def_transrec RS trans;
+
+Goal "recursor(a,b,0) = a";
+by (rtac (nat_case_0 RS lemma) 1);
+qed "recursor_0";
+
+Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
+by (rtac lemma 1);
+by (Simp_tac 1);
+qed "recursor_succ";
+
+
+(** rec: old version for compatibility **)
+
+Goalw [rec_def] "rec(0,a,b) = a";
+by (rtac recursor_0 1);
+qed "rec_0";
+
+Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
+by (rtac recursor_succ 1);
+qed "rec_succ";
+
+Addsimps [rec_0, rec_succ];
+
+val major::prems = Goal
+    "[| n: nat;  \
+\       a: C(0);  \
+\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
+\    |] ==> rec(n,a,b) : C(n)";
+by (rtac (major RS nat_induct) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
+qed "rec_type";
+
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Epsilon.thy	Thu Jan 07 18:30:55 1999 +0100
@@ -25,4 +25,10 @@
                            b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
                            UN j<i. r`j)))"
 
+    recursor  :: [i, [i,i]=>i, i]=>i
+     "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+
+    rec  :: [i, i, [i,i]=>i]=>i
+     "rec(k,a,b) ==  recursor(a,b,k)"
+
 end
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Finite.ML
--- a/src/ZF/Finite.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Finite.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -10,8 +10,6 @@
 prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
 *)
 
-open Finite;
-
 (*** Finite powerset operator ***)
 
 Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
@@ -104,7 +102,7 @@
 
 (*Functions from a finite ordinal*)
 Goal "n: nat ==> n->A <= Fin(nat*A)";
-by (nat_ind_tac "n" [] 1);
+by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
 by (asm_simp_tac 
     (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/List.ML
--- a/src/ZF/List.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/List.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -63,31 +63,27 @@
 
 (** drop **)
 
-Goalw [drop_def] "drop(0, l) = l";
-by (rtac rec_0 1);
-qed "drop_0";
-
-Goalw [drop_def] "i:nat ==> drop(i, Nil) = Nil";
-by (etac nat_induct 1);
+Goal "i:nat ==> drop(i, Nil) = Nil";
+by (induct_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "drop_Nil";
 
-Goalw [drop_def]
-    "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
+Goal "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
 by (rtac sym 1);
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "drop_succ_Cons";
 
-Addsimps [drop_0, drop_Nil, drop_succ_Cons];
+Addsimps [drop_Nil, drop_succ_Cons];
 
-Goalw [drop_def] 
-    "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
-by (etac nat_induct 1);
+Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
+by (induct_tac "i" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
 qed "drop_type";
 
+Delsimps [drop_SUCC];
+
 
 (** Type checking -- proved by induction, as usual **)
 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/List.thy	Thu Jan 07 18:30:55 1999 +0100
@@ -33,12 +33,6 @@
   length :: i=>i
   hd      :: i=>i
   tl      :: i=>i
-  map        :: [i=>i, i] => i
-  set_of_list :: i=>i
-  "@"        :: [i,i]=>i                        (infixr 60)
-  rev :: i=>i
-  flat       :: i=>i
-  list_add   :: i=>i
 
 primrec
   "length([]) = 0"
@@ -51,6 +45,12 @@
   "tl([]) = []"
   "tl(Cons(a,l)) = l"
 
+
+consts
+  map        :: [i=>i, i] => i
+  set_of_list :: i=>i
+  "@"        :: [i,i]=>i                        (infixr 60)
+  
 primrec
   "map(f,[]) = []"
   "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
@@ -63,6 +63,12 @@
   "[] @ ys = ys"
   "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
   
+
+consts
+  rev :: i=>i
+  flat       :: i=>i
+  list_add   :: i=>i
+
 primrec
   "rev([]) = []"
   "rev(Cons(a,l)) = rev(l) @ [a]"
@@ -75,8 +81,11 @@
   "list_add([]) = 0"
   "list_add(Cons(a,l)) = a #+ list_add(l)"
        
-constdefs
+consts
   drop       :: [i,i]=>i
-  "drop(i,l)   == rec(i, l, %j r. tl(r))"
+
+primrec
+  drop_0    "drop(0,l) = l"
+  drop_SUCC "drop(succ(i), l) = tl (drop(i,l))"
 
 end
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Nat.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -213,17 +213,16 @@
 (** nat_rec -- used to define eclose and transrec, then obsolete;
     rec, from arith.ML, has fewer typing conditions **)
 
-val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
+val lemma = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
 
 Goal "nat_rec(0,a,b) = a";
-by (rtac nat_rec_trans 1);
+by (rtac lemma 1);
 by (rtac nat_case_0 1);
 qed "nat_rec_0";
 
-val [prem] = goal Nat.thy 
-    "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
-by (rtac nat_rec_trans 1);
-by (simp_tac (simpset() addsimps [prem, Memrel_iff, vimage_singleton_iff]) 1);
+Goal "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
+by (rtac lemma 1);
+by (asm_simp_tac (simpset() addsimps [Memrel_iff, vimage_singleton_iff]) 1);
 qed "nat_rec_succ";
 
 (** The union of two natural numbers is a natural number -- their maximum **)
diff -r a99879bd9f13 -r 032babd0120b src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/QUniv.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -193,6 +193,6 @@
 by (rtac (succI1 RS UN_upper) 1);
 (*Limit(i) case*)
 by (asm_simp_tac
-    (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
+    (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, 
 			 UN_mono, QPair_Int_Vset_subset_trans]) 1);
 qed "QPair_Int_Vset_subset_UN";
diff -r a99879bd9f13 -r 032babd0120b src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ROOT.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -42,11 +42,11 @@
 use_thy "Fixedpt";
 use     "Tools/inductive_package";
 use_thy "Inductive";
+use "Tools/induct_tacs";
+use "Tools/primrec_package";
 use_thy "QUniv";
 use "Tools/datatype_package";
-use "Tools/primrec_package";
 use_thy "Datatype";
-use "Tools/induct_tacs";
 use_thy "InfDatatype";
 use_thy "List";
 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Resid/Substitution.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -16,7 +16,7 @@
 
 val succ_pred = prove_goal Arith.thy 
     "!!i.[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j"
- (fn prems =>[(etac nat_induct 1),
+ (fn prems =>[(induct_tac "j" 1),
               (Fast_tac 1),
               (Asm_simp_tac 1)]);
 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -13,59 +13,6 @@
 *)
 
 
-(** Datatype information, e.g. associated theorems **)
-
-type datatype_info =
-  {inductive: bool,		(*true if inductive, not coinductive*)
-   constructors : term list,    (*the constructors, as Consts*)
-   rec_rewrites : thm list,     (*recursor equations*)
-   case_rewrites : thm list,    (*case equations*)
-   induct : thm,
-   mutual_induct : thm,
-   exhaustion : thm};
-
-structure DatatypesArgs =
-  struct
-  val name = "ZF/datatypes";
-  type T = datatype_info Symtab.table;
-
-  val empty = Symtab.empty;
-  val prep_ext = I;
-  val merge: T * T -> T = Symtab.merge (K true);
-
-  fun print sg tab =
-    Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
-  end;
-
-structure DatatypesData = TheoryDataFun(DatatypesArgs);
-
-
-(** Constructor information: needed to map constructors to datatypes **)
-
-type constructor_info =
-  {big_rec_name : string,     (*name of the mutually recursive set*)
-   constructors : term list,  (*the constructors, as Consts*)
-   rec_rewrites : thm list};  (*recursor equations*)
-
-
-structure ConstructorsArgs =
-struct
-  val name = "ZF/constructors"
-  type T = constructor_info Symtab.table
-
-  val empty = Symtab.empty
-  val prep_ext = I
-  val merge: T * T -> T = Symtab.merge (K true)
-
-  fun print sg tab = ()   (*nothing extra to print*)
-end;
-
-structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
-
-val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
-
-
 type datatype_result =
    {con_defs   : thm list,             (*definitions made in thy*)
     case_eqns  : thm list,             (*equations for case operator*)
diff -r a99879bd9f13 -r 032babd0120b src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -1,9 +1,13 @@
-(*  Title:      HOL/Tools/induct_tacs.ML
+(*  Title:      ZF/Tools/induct_tacs.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Induction and exhaustion tactics for Isabelle/ZF
+
+The theory information needed to support them (and to support primrec)
+
+Also, a function to install other sets as if they were datatypes
 *)
 
 
@@ -11,9 +15,65 @@
 sig
   val induct_tac : string -> int -> tactic
   val exhaust_tac : string -> int -> tactic
+  val rep_datatype_i : thm -> thm -> thm list -> thm list -> theory -> theory
 end;
 
 
+
+(** Datatype information, e.g. associated theorems **)
+
+type datatype_info =
+  {inductive: bool,		(*true if inductive, not coinductive*)
+   constructors : term list,    (*the constructors, as Consts*)
+   rec_rewrites : thm list,     (*recursor equations*)
+   case_rewrites : thm list,    (*case equations*)
+   induct : thm,
+   mutual_induct : thm,
+   exhaustion : thm};
+
+structure DatatypesArgs =
+  struct
+  val name = "ZF/datatypes";
+  type T = datatype_info Symtab.table;
+
+  val empty = Symtab.empty;
+  val prep_ext = I;
+  val merge: T * T -> T = Symtab.merge (K true);
+
+  fun print sg tab =
+    Pretty.writeln (Pretty.strs ("datatypes:" ::
+      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+  end;
+
+structure DatatypesData = TheoryDataFun(DatatypesArgs);
+
+
+(** Constructor information: needed to map constructors to datatypes **)
+
+type constructor_info =
+  {big_rec_name : string,     (*name of the mutually recursive set*)
+   constructors : term list,  (*the constructors, as Consts*)
+   rec_rewrites : thm list};  (*recursor equations*)
+
+
+structure ConstructorsArgs =
+struct
+  val name = "ZF/constructors"
+  type T = constructor_info Symtab.table
+
+  val empty = Symtab.empty
+  val prep_ext = I
+  val merge: T * T -> T = Symtab.merge (K true)
+
+  fun print sg tab = ()   (*nothing extra to print*)
+end;
+
+structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
+
+val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
+
+
+
 structure DatatypeTactics : DATATYPE_TACTICS =
 struct
 
@@ -62,7 +122,62 @@
 val exhaust_tac = exhaust_induct_tac true;
 val induct_tac = exhaust_induct_tac false;
 
+
+
+(**** declare non-datatype as datatype ****)
+
+fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
+  let
+    val sign = sign_of thy;
+
+    (*analyze the LHS of a case equation to get a constructor*)
+    fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
+      | const_of eqn = error ("Ill-formed case equation: " ^
+			      Sign.string_of_term sign eqn);
+
+    val constructors =
+	map (head_of o const_of o FOLogic.dest_Trueprop o
+	     #prop o rep_thm) case_eqns;
+
+    val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
+	FOLogic.dest_Trueprop (hd (prems_of elim));	
+    
+    val simps = case_eqns @ recursor_eqns;
+
+    val dt_info =
+	  {inductive = true,
+	   constructors = constructors,
+	   rec_rewrites = recursor_eqns,
+	   case_rewrites = case_eqns,
+	   induct = induct,
+	   mutual_induct = TrueI,  (*No need for mutual induction*)
+	   exhaustion = elim};
+
+    val con_info =
+	  {big_rec_name = big_rec_name,
+	   constructors = constructors,
+	      (*let primrec handle definition by cases*)
+	   rec_rewrites = (case recursor_eqns of
+			       [] => case_eqns | _ => recursor_eqns)};
+
+    (*associate with each constructor the datatype name and rewrites*)
+    val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
+
+  in
+      thy |> Theory.add_path (Sign.base_name big_rec_name)
+	  |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), 
+				  [Simplifier.simp_add_global])] 
+	  |> DatatypesData.put 
+	      (Symtab.update
+	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
+	  |> ConstructorsData.put
+	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
+	  |> Theory.parent_path
+  end
+  handle _ => error "Failure in rep_datatype";
+
 end;
 
 
-open DatatypeTactics;
+val exhaust_tac = DatatypeTactics.exhaust_tac;
+val induct_tac  = DatatypeTactics.induct_tac;
diff -r a99879bd9f13 -r 032babd0120b src/ZF/ex/Limit.ML
--- a/src/ZF/ex/Limit.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Limit.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -174,7 +174,7 @@
 Addsimps [chain_in, chain_rel];
 
 Goal "[|chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,(X`(m #+ n)))";
-by (res_inst_tac [("n","m")] nat_induct 1);
+by (induct_tac "m" 1);
 by (ALLGOALS Simp_tac);
 by (rtac cpo_trans 2); (* loops if repeated *)
 by (REPEAT (ares_tac [cpo_refl,chain_in,chain_rel,nat_succI,add_type] 1));
@@ -191,7 +191,7 @@
 by (rtac impE 1);  (* The first three steps prepare for the induction proof *)
 by (assume_tac 3);
 by (assume_tac 2);
-by (res_inst_tac [("n","m")] nat_induct 1);
+by (induct_tac "m" 1);
 by Safe_tac;
 by (Asm_full_simp_tac 1);
 by (rtac cpo_trans 2);
@@ -1456,36 +1456,25 @@
 qed "e_less_add";
 
 (* Again, would like more theorems about arithmetic. *)
-(* Well, HOL has much better support and automation of natural numbers. *)
 
 val add1 = prove_goal Limit.thy
     "!!x. n:nat ==> succ(n) = n #+ 1"
-  (fn prems => 
-      [asm_simp_tac (simpset() addsimps[add_succ_right,add_0_right]) 1]);
+  (fn prems => [Asm_simp_tac 1]);
 
 Goal  (* succ_sub1 *)
     "x:nat ==> 0 < x --> succ(x #- 1)=x";
-by (res_inst_tac[("n","x")]nat_induct 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-by Safe_tac;
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by (induct_tac "x" 1);
+by Auto_tac;
 qed "succ_sub1";
 
 Goal (* succ_le_pos *)
     "[|m:nat; k:nat|] ==> succ(m) le m #+ k --> 0 < k";
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (assume_tac 1);
-by (rtac impI 1);
-by (Asm_full_simp_tac 1);
-by Safe_tac;
-by (Asm_full_simp_tac 1); (* Surprise, surprise. *)
+by (induct_tac "m" 1);
+by Auto_tac;
 qed "succ_le_pos";
 
 Goal "[|n:nat; m:nat|] ==> m le n --> (EX k:nat. n = m #+ k)";
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (assume_tac 1);
+by (induct_tac "m" 1);
 by Safe_tac;
 by (rtac bexI 1);
 by (rtac (add_0 RS sym) 1);
@@ -1539,11 +1528,10 @@
 
 Goal "[|emb_chain(DD,ee); m:nat; k:nat|] ==>   \
 \    emb(DD`m,DD`(m#+k),e_less(DD,ee,m,m#+k))";
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
-by (asm_simp_tac(simpset() addsimps[add_0_right,e_less_eq]) 1);
+by (induct_tac "k" 1);
+by (asm_simp_tac(simpset() addsimps[e_less_eq]) 1);
 brr[emb_id,emb_chain_cpo] 1;
-by (asm_simp_tac(simpset() addsimps[add_succ_right,e_less_add]) 1);
+by (asm_simp_tac(simpset() addsimps[e_less_add]) 1);
 by (auto_tac (claset() addIs [emb_comp,emb_chain_emb,emb_chain_cpo,add_type],
 	      simpset()));
 qed "emb_e_less_add";
@@ -1571,7 +1559,7 @@
     "[| emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
 \    n le k --> \
 \    e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)";
-by (eres_inst_tac[("n","k")]nat_induct 1);
+by (induct_tac "k" 1);
 by (asm_full_simp_tac(simpset() addsimps [e_less_eq, id_type RS id_comp]) 1);
 by (asm_simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
 by (rtac impI 1);
@@ -1631,10 +1619,9 @@
 Goal  (* e_gr_fun_add *)
     "[|emb_chain(DD,ee); n:nat; k:nat|] ==>   \
 \    e_gr(DD,ee,n#+k,n): set(DD`(n#+k))->set(DD`n)";
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
-by (asm_simp_tac(simpset() addsimps[add_0_right,e_gr_eq,id_type]) 1);
-by (asm_simp_tac(simpset() addsimps[add_succ_right,e_gr_add]) 1);
+by (induct_tac "k" 1);
+by (asm_simp_tac(simpset() addsimps[e_gr_eq,id_type]) 1);
+by (asm_simp_tac(simpset() addsimps[e_gr_add]) 1);
 brr[comp_fun, Rp_cont, cont_fun, emb_chain_emb, emb_chain_cpo, add_type, nat_succI] 1;
 qed "e_gr_fun_add";
 
@@ -1651,11 +1638,10 @@
     "[| emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
 \    m le k --> \
 \    e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)";
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
+by (induct_tac "k" 1);
 by (rtac impI 1);
-by (asm_full_simp_tac(ZF_ss addsimps
-    [le0_iff, add_0_right, e_gr_eq, id_type RS comp_id]) 1);
+by (asm_full_simp_tac(simpset() addsimps
+		      [le0_iff, e_gr_eq, id_type RS comp_id]) 1);
 by (asm_simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
 by (rtac impI 1);
 by (etac disjE 1);
@@ -1683,13 +1669,12 @@
 by (blast_tac (claset() addIs [emb_cont, emb_e_less]) 1);
 qed "e_less_cont";
 
-Goal  (* e_gr_cont_lemma *)
-    "[|emb_chain(DD,ee); m:nat; n:nat|] ==>   \
-\    n le m --> e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (assume_tac 1);
-by (asm_full_simp_tac(simpset() addsimps
-    [le0_iff,e_gr_eq,nat_0I]) 1);
+Goal  (* e_gr_cont *)
+    "[|n le m; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
+\    e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
+by (etac rev_mp 1);
+by (induct_tac "m" 1);
+by (asm_full_simp_tac(simpset() addsimps [le0_iff,e_gr_eq,nat_0I]) 1);
 brr[impI,id_cont,emb_chain_cpo,nat_0I] 1;
 by (asm_full_simp_tac(simpset() addsimps[le_succ_iff]) 1);
 by (etac disjE 1);
@@ -1699,12 +1684,6 @@
 brr[comp_pres_cont,Rp_cont,emb_chain_cpo,emb_chain_emb,nat_succI] 1;
 by (asm_simp_tac(simpset() addsimps[e_gr_eq,nat_succI]) 1);
 by (auto_tac (claset() addIs [id_cont,emb_chain_cpo], simpset()));
-qed "e_gr_cont_lemma";
-
-Goal  (* e_gr_cont *)
-    "[|n le m; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
-\    e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
-brr[e_gr_cont_lemma RS mp] 1;
 qed "e_gr_cont";
 
 (* Considerably shorter.... 57 against 26 *)
@@ -1713,12 +1692,11 @@
     "[|n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>   \
 \    e_less(DD,ee,m,m#+n) = e_gr(DD,ee,m#+k,m#+n) O e_less(DD,ee,m,m#+k)";
 (* Use mp to prepare for induction. *)
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
-by (asm_full_simp_tac(ZF_ss addsimps
-    [le0_iff, add_0_right, e_gr_eq, e_less_eq, id_type RS id_comp]) 1);by (simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
+by (etac rev_mp 1);
+by (induct_tac "k" 1);
+by (asm_full_simp_tac(simpset() addsimps
+		      [e_gr_eq, e_less_eq, id_type RS id_comp]) 1);
+by (simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
 by (rtac impI 1);
 by (etac disjE 1);
 by (etac impE 1);
@@ -1742,12 +1720,10 @@
     "[|m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>   \
 \    e_gr(DD,ee,n#+m,n) = e_gr(DD,ee,n#+k,n) O e_less(DD,ee,n#+m,n#+k)";
 (* Use mp to prepare for induction. *)
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
+by (etac rev_mp 1);
+by (induct_tac "k" 1);
 by (asm_full_simp_tac(simpset() addsimps
-    [add_0_right, e_gr_eq, e_less_eq, id_type RS id_comp]) 1);
+		      [e_gr_eq, e_less_eq, id_type RS id_comp]) 1);
 by (simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
 by (rtac impI 1);
 by (etac disjE 1);
@@ -2042,10 +2018,10 @@
     "[|m le n; emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==>   \
 \    rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)";
 by (etac rev_mp 1);  (* For induction proof *)
-by (res_inst_tac[("n","n")]nat_induct 1);
-by (rtac impI 2);
-by (asm_full_simp_tac (simpset() addsimps [e_less_eq]) 2);
-by (stac id_thm 2);
+by (induct_tac "n" 1);
+by (rtac impI 1);
+by (asm_full_simp_tac (simpset() addsimps [e_less_eq]) 1);
+by (stac id_thm 1);
 brr[apply_type,Dinf_prod,cpo_refl,emb_chain_cpo,nat_0I] 1;
 by (asm_full_simp_tac (simpset() addsimps [le_succ_iff]) 1);
 by (rtac impI 1);
@@ -2080,10 +2056,10 @@
     "[|n le m; emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==>   \
 \    rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)";
 by (etac rev_mp 1);  (* For induction proof *)
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (rtac impI 2);
-by (asm_full_simp_tac (simpset() addsimps [e_gr_eq]) 2);
-by (stac id_thm 2);
+by (induct_tac "m" 1);
+by (rtac impI 1);
+by (asm_full_simp_tac (simpset() addsimps [e_gr_eq]) 1);
+by (stac id_thm 1);
 brr[apply_type,Dinf_prod,cpo_refl,emb_chain_cpo,nat_0I] 1;
 by (asm_full_simp_tac (simpset() addsimps [le_succ_iff]) 1);
 by (rtac impI 1);
@@ -2429,22 +2405,17 @@
 	      simpset()));
 qed "mono_lemma";
 
-(* PAINFUL: wish condrew with difficult conds on term bound in lam-abs. *)
-(* Introduces need for lemmas. *)
-
 Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \        emb_chain(DD,ee); cpo(E); cpo(G); n:nat |] ==>  \  
 \     (lam na:nat. (lam f:cont(E, G). f O r(n)) `  \
 \      ((lam n:nat. f(n) O Rp(DD ` n, E, r(n))) ` na))  = \
 \     (lam na:nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
 by (rtac fun_extension 1);
-by (stac beta 3);
-by (stac beta 4);
-by (stac beta 5);
-by (rtac lam_type 1);
-by (stac beta 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addIs [lam_type, comp_pres_cont, Rp_cont, emb_cont, commute_emb, emb_chain_cpo])));
+by (fast_tac (claset() addIs [lam_type]) 1);
+by (ALLGOALS 
+    (asm_simp_tac 
+     (simpset() setSolver (type_auto_tac [lam_type, comp_pres_cont, Rp_cont, 
+			        emb_cont, commute_emb, emb_chain_cpo]))));
 val lemma = result();
 
 Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
diff -r a99879bd9f13 -r 032babd0120b src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Mutil.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -96,20 +96,21 @@
 qed "tiling_domino_0_1";
 
 Goal "[| i: nat;  n: nat |] ==> {i} * (n #+ n) : tiling(domino)";
-by (nat_ind_tac "n" [] 1);
+by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps tiling.intrs) 1);
 by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
 by (resolve_tac tiling.intrs 1);
 by (assume_tac 2);
+by (rename_tac "n'" 1);
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
-    "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
+    "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {<i,n'#+n'>, <i,succ(n'#+n')>}" 1);
 by (Blast_tac 2);
 by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
 by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1);
 qed "dominoes_tile_row";
 
 Goal "[| m: nat;  n: nat |] ==> m * (n #+ n) : tiling(domino)";
-by (nat_ind_tac "m" [] 1);
+by (induct_tac "m" 1);
 by (simp_tac (simpset() addsimps tiling.intrs) 1);
 by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1);
 by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] 
diff -r a99879bd9f13 -r 032babd0120b src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Primrec.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -23,7 +23,7 @@
 					      pr_typechecks @ prim_rec.intrs));
 
 Goalw [ACK_def] "i:nat ==> ACK(i): prim_rec";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "ACK_in_prim_rec";
 
@@ -64,10 +64,10 @@
 
 (*PROPERTY A 4*)
 Goal "i:nat ==> ALL j:nat. j < ack(i,j)";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
 by (Asm_simp_tac 1);
 by (rtac ballI 1);
-by (eres_inst_tac [("n","j")] nat_induct 1);
+by (induct_tac "j" 1);
 by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
              Asm_simp_tac] 1);
 by (DO_GOAL [etac (succ_leI RS lt_trans1),
@@ -77,7 +77,7 @@
 
 (*PROPERTY A 5-, the single-step lemma*)
 Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2])));
 qed "ack_lt_ack_succ2";
 
@@ -98,7 +98,7 @@
 
 (*PROPERTY A 6*)
 Goal "[| i:nat;  j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
-by (nat_ind_tac "j" [] 1);
+by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac ack_le_mono2 1);
 by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
@@ -129,13 +129,13 @@
 
 (*PROPERTY A 8*)
 Goal "j:nat ==> ack(1,j) = succ(succ(j))";
-by (etac nat_induct 1);
+by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "ack_1";
 
 (*PROPERTY A 9*)
 Goal "j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
-by (etac nat_induct 1);
+by (induct_tac "j" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right])));
 qed "ack_2";
 
@@ -183,7 +183,7 @@
 
 (*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
 Goal "[| i:nat; j:nat |] ==> i < ack(i,j)";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
 by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
 by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
 by (tc_tac []);
@@ -261,7 +261,7 @@
 by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
 by (Asm_simp_tac 1);
 by (etac ssubst 1);  (*get rid of the needless assumption*)
-by (eres_inst_tac [("n","a")] nat_induct 1);
+by (induct_tac "a" 1);
 (*base case*)
 by (DO_GOAL [Asm_simp_tac, rtac lt_trans, etac bspec,
              assume_tac, rtac (add_le_self RS ack_lt_mono1),
diff -r a99879bd9f13 -r 032babd0120b src/ZF/ex/Ramsey.ML
--- a/src/ZF/ex/Ramsey.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Ramsey.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -18,16 +18,13 @@
     Available from the author: kaufmann@cli.com
 *)
 
-open Ramsey;
-
 (*** Cliques and Independent sets ***)
 
 Goalw [Clique_def] "Clique(0,V,E)";
 by (Fast_tac 1);
 qed "Clique0";
 
-Goalw [Clique_def]
-    "[| Clique(C,V',E);  V'<=V |] ==> Clique(C,V,E)";
+Goalw [Clique_def] "[| Clique(C,V',E);  V'<=V |] ==> Clique(C,V,E)";
 by (Fast_tac 1);
 qed "Clique_superset";
 
@@ -74,37 +71,37 @@
 
 (*The #-succ(0) strengthens the original theorem statement, but precisely
   the same proof could be used!!*)
-val prems = goal Ramsey.thy
-    "m: nat ==> \
-\    ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
-\                         Atleast(m,A) | Atleast(n,B)";
-by (nat_ind_tac "m" prems 1);
+Goal "m: nat ==> \
+\     ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
+\                          Atleast(m,A) | Atleast(n,B)";
+by (induct_tac "m" 1);
 by (fast_tac (claset() addSIs [Atleast0]) 1);
 by (Asm_simp_tac 1);
 by (rtac ballI 1);
-by (rename_tac "n" 1);          (*simplifier does NOT preserve bound names!*)
-by (nat_ind_tac "n" [] 1);
+by (rename_tac "m' n" 1);       (*simplifier does NOT preserve bound names!*)
+by (induct_tac "n" 1);
 by (fast_tac (claset() addSIs [Atleast0]) 1);
-by (asm_simp_tac (simpset() addsimps [add_succ_right]) 1);
+by (Asm_simp_tac 1);
 by Safe_tac;
 by (etac (Atleast_succD RS bexE) 1);
+by (rename_tac "n' A B z" 1);
 by (etac UnE 1);
-(**case x:B.  Instantiate the 'ALL A B' induction hypothesis. **)
-by (dres_inst_tac [("x1","A"), ("x","B-{x}")] (spec RS spec) 2);
+(**case z:B.  Instantiate the 'ALL A B' induction hypothesis. **)
+by (dres_inst_tac [("x1","A"), ("x","B-{z}")] (spec RS spec) 2);
 by (etac (mp RS disjE) 2);
-(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
+(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
 by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
 (*proving the condition*)
 by (etac Atleast_superset 2 THEN Fast_tac 2);
-(**case x:A.  Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
-by (dres_inst_tac [("x2","succ(n1)"), ("x1","A-{x}"), ("x","B")] 
+(**case z:A.  Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
+by (dres_inst_tac [("x2","succ(n')"), ("x1","A-{z}"), ("x","B")] 
     (bspec RS spec RS spec) 1);
 by (etac nat_succI 1);
 by (etac (mp RS disjE) 1);
-(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
+(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
 by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
 (*proving the condition*)
-by (asm_simp_tac (simpset() addsimps [add_succ_right]) 1);
+by (Asm_simp_tac 1);
 by (etac Atleast_superset 1 THEN Fast_tac 1);
 qed "pigeon2_lemma";
 
@@ -129,31 +126,27 @@
 
 (*The use of succ(m) here, rather than #-succ(0), simplifies the proof of 
   Ramsey_step_lemma.*)
-val prems = goal Ramsey.thy
-    "[| Atleast(m #+ n, A);  m: nat;  n: nat |] ==> \
-\    Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
+Goal "[| Atleast(m #+ n, A);  m: nat;  n: nat |]  \
+\     ==> Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
 by (rtac (nat_succI RS pigeon2) 1);
-by (simp_tac (simpset() addsimps prems) 3);
+by (Asm_simp_tac 3);
 by (rtac Atleast_superset 3);
-by (REPEAT (resolve_tac prems 1));
-by (Fast_tac 1);
+by Auto_tac;
 qed "Atleast_partition";
 
 (*For the Atleast part, proves ~(a:I) from the second premise!*)
-val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
+Goalw [Symmetric_def,Indept_def]
     "[| Symmetric(E);  Indept(I, {z: V-{a}. <a,z> ~: E}, E);  a: V;  \
 \       Atleast(j,I) |] ==>   \
 \    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
-by (cut_facts_tac prems 1);
-by (fast_tac (claset() addSEs [Atleast_succI]) 1);  (*34 secs*)
+by (blast_tac (claset() addSIs [Atleast_succI]) 1);
 qed "Indept_succ";
 
-val prems = goalw Ramsey.thy [Symmetric_def,Clique_def]
+Goalw [Symmetric_def,Clique_def]
     "[| Symmetric(E);  Clique(C, {z: V-{a}. <a,z>:E}, E);  a: V;  \
 \       Atleast(j,C) |] ==>   \
 \    Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
-by (cut_facts_tac prems 1);
-by (fast_tac (claset() addSEs [Atleast_succI]) 1);  (*41 secs*)
+by (blast_tac (claset() addSIs [Atleast_succI]) 1);
 qed "Clique_succ";
 
 (** Induction step **)
@@ -187,12 +180,11 @@
 (** The actual proof **)
 
 (*Again, the induction requires Ramsey numbers to be positive.*)
-val prems = goal Ramsey.thy
-    "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
-by (nat_ind_tac "i" prems 1);
+Goal "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
+by (induct_tac "i" 1);
 by (fast_tac (claset() addSIs [Ramsey0j]) 1);
 by (rtac ballI 1);
-by (nat_ind_tac "j" [] 1);
+by (induct_tac "j" 1);
 by (fast_tac (claset() addSIs [Ramseyi0]) 1);
 by (fast_tac (claset() addSDs [bspec]
  		       addSIs [add_type,Ramsey_step_lemma]) 1);
diff -r a99879bd9f13 -r 032babd0120b src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/thy_syntax.ML	Thu Jan 07 18:30:55 1999 +0100
@@ -130,6 +130,19 @@
 end;
 
 
+(** rep_datatype **)
+
+fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
+  "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n    " ^
+  mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
+
+val rep_datatype_decl =
+  (("elim" $$-- ident) -- 
+   ("induct" $$-- ident) --
+   ("case_eqns" $$-- list1 ident) -- 
+   ("recursor_eqns" $$-- list1 ident)) >> mk_rep_dt_string;
+
+
 (** primrec **)
 
 fun mk_primrec_decl eqns =
@@ -154,12 +167,14 @@
 
 val _ = ThySyn.add_syntax
  ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
-  "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
-  "type_elims"]
- [section "inductive"   "" (inductive_decl false),
-  section "coinductive" "" (inductive_decl true),
-  section "datatype"    "" (datatype_decl false),
-  section "codatatype"  "" (datatype_decl true),
-  section "primrec"     "" primrec_decl];
+  "<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims",
+  (*rep_datatype*)
+  "elim", "induct", "case_eqns", "recursor_eqns"]
+ [section "inductive"    "" (inductive_decl false),
+  section "coinductive"  "" (inductive_decl true),
+  section "datatype"     "" (datatype_decl false),
+  section "codatatype"   "" (datatype_decl true),
+  section "rep_datatype" "" rep_datatype_decl,
+  section "primrec"      "" primrec_decl];
 
 end;