src/HOL/NatDef.ML
changeset 3040 7d48671753da
parent 3023 01364e2f30ad
child 3085 f45074fab9c7
     1.1 --- a/src/HOL/NatDef.ML	Thu Apr 24 18:03:23 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Thu Apr 24 18:06:46 1997 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  val prems = goalw thy [Zero_def,Suc_def]
     1.6      "[| P(0);   \
     1.7 -\       !!k. P(k) ==> P(Suc(k)) |]  ==> P(n)";
     1.8 +\       !!n. P(n) ==> P(Suc(n)) |]  ==> P(n)";
     1.9  by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
    1.10  by (rtac (Rep_Nat RS Nat_induct) 1);
    1.11  by (REPEAT (ares_tac prems 1
    1.12 @@ -42,8 +42,16 @@
    1.13  
    1.14  (*Perform induction on n. *)
    1.15  fun nat_ind_tac a i = 
    1.16 -    EVERY [res_inst_tac [("n",a)] nat_induct i,
    1.17 -           rename_last_tac a ["1"] (i+1)];
    1.18 +    EVERY[res_inst_tac [("n",a)] nat_induct i,
    1.19 +          COND (Datatype.occs_in_prems a (i+1)) all_tac
    1.20 +               (rename_last_tac a [""] (i+1))];
    1.21 +
    1.22 +(*Install 'automatic' induction tactic, pretending nat is a datatype *)
    1.23 +(*except for induct_tac, everything is dummy*)
    1.24 +datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    1.25 +  constructors = [], induct_tac = nat_ind_tac,
    1.26 +  nchotomy = flexpair_def, case_cong = flexpair_def})];
    1.27 +
    1.28  
    1.29  (*A special form of induction for reasoning about m<n and m-n*)
    1.30  val prems = goal thy