src/HOL/Nat.thy
author nipkow
Fri Feb 20 17:56:39 1998 +0100 (1998-02-20)
changeset 4640 ac6cf9f18653
parent 4613 67a726003cf8
child 5188 633ec5f6c155
permissions -rw-r--r--
Congruence rules use == in premises now.
New class linord.
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,
nipkow@4613
    19
  exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
nipkow@4613
    20
                        THEN_ALL_NEW (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)
nipkow@4640
    26
instance nat :: linorder (nat_le_linear)
oheimb@1660
    27
paulson@3370
    28
consts
paulson@3370
    29
  "^"           :: ['a::power,nat] => 'a            (infixr 80)
paulson@3370
    30
clasohm@923
    31
end