src/HOL/NatDef.ML
changeset 3282 c31e6239d4c9
parent 3236 882e125ed7da
child 3292 8b143c196d42
     1.1 --- a/src/HOL/NatDef.ML	Wed May 21 17:31:12 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Thu May 22 09:20:28 1997 +0200
     1.3 @@ -46,13 +46,6 @@
     1.4            COND (Datatype.occs_in_prems a (i+1)) all_tac
     1.5                 (rename_last_tac a [""] (i+1))];
     1.6  
     1.7 -(*Install 'automatic' induction tactic, pretending nat is a datatype *)
     1.8 -(*except for induct_tac, everything is dummy*)
     1.9 -datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    1.10 -  constructors = [], induct_tac = nat_ind_tac,
    1.11 -  nchotomy = flexpair_def, case_cong = flexpair_def})];
    1.12 -
    1.13 -
    1.14  (*A special form of induction for reasoning about m<n and m-n*)
    1.15  val prems = goal thy
    1.16      "[| !!x. P x 0;  \
    1.17 @@ -76,6 +69,14 @@
    1.18  by (Blast_tac 1);
    1.19  qed "natE";
    1.20  
    1.21 +(*Install 'automatic' induction tactic, pretending nat is a datatype *)
    1.22 +(*except for induct_tac, everything is dummy*)
    1.23 +datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    1.24 +  constructors = [], induct_tac = nat_ind_tac,
    1.25 +  exhaustion = natE, exhaust_tac = fn v => res_inst_tac [("n",v)] natE,
    1.26 +  nchotomy = flexpair_def, case_cong = flexpair_def})];
    1.27 +
    1.28 +
    1.29  (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    1.30  
    1.31  (*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat),