src/HOL/Nat.thy
author wenzelm
Mon Nov 03 21:12:21 1997 +0100 (1997-11-03)
changeset 4104 84433b1ab826
parent 3370 5c5fdce3a4e4
child 4613 67a726003cf8
permissions -rw-r--r--
nat datatype_info moved to Nat.thy;
     1 (*  Title:      HOL/Nat.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TU Muenchen
     5 
     6 Nat is a partial order
     7 *)
     8 
     9 Nat = NatDef +
    10 
    11 (*install 'automatic' induction tactic, pretending nat is a datatype
    12   except for induct_tac and exhaust_tac, everything is dummy*)
    13 
    14 MLtext {|
    15 |> Dtype.add_datatype_info
    16 ("nat", {case_const = Bound 0, case_rewrites = [],
    17   constructors = [], induct_tac = nat_ind_tac,
    18   exhaustion = natE,
    19   exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
    20                                        (rotate_tac ~1),
    21   nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
    22 |}
    23 
    24 
    25 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
    26 
    27 consts
    28   "^"           :: ['a::power,nat] => 'a            (infixr 80)
    29 
    30 end