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;
clasohm@923
     1
(*  Title:      HOL/Nat.thy
clasohm@923
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow
nipkow@2608
     4
    Copyright   1997 TU Muenchen
clasohm@923
     5
nipkow@2608
     6
Nat is a partial order
clasohm@923
     7
*)
clasohm@923
     8
nipkow@2608
     9
Nat = NatDef +
clasohm@923
    10
wenzelm@4104
    11
(*install 'automatic' induction tactic, pretending nat is a datatype
wenzelm@4104
    12
  except for induct_tac and exhaust_tac, everything is dummy*)
wenzelm@4104
    13
wenzelm@4104
    14
MLtext {|
wenzelm@4104
    15
|> Dtype.add_datatype_info
wenzelm@4104
    16
("nat", {case_const = Bound 0, case_rewrites = [],
wenzelm@4104
    17
  constructors = [], induct_tac = nat_ind_tac,
wenzelm@4104
    18
  exhaustion = natE,
wenzelm@4104
    19
  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
wenzelm@4104
    20
                                       (rotate_tac ~1),
wenzelm@4104
    21
  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
wenzelm@4104
    22
|}
wenzelm@4104
    23
wenzelm@4104
    24
nipkow@2608
    25
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
oheimb@1660
    26
paulson@3370
    27
consts
paulson@3370
    28
  "^"           :: ['a::power,nat] => 'a            (infixr 80)
paulson@3370
    29
clasohm@923
    30
end