src/HOL/Nat.thy
author berghofe
Fri Jul 24 13:34:59 1998 +0200 (1998-07-24)
changeset 5188 633ec5f6c155
parent 4640 ac6cf9f18653
child 5499 1787c44ae4ed
permissions -rw-r--r--
Declaration of type 'nat' as a datatype (this allows usage of
exhaust_tac and induct_tac on type 'nat'). Moved some proofs
using natE from NatDef.ML to Nat.ML.
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
berghofe@5188
     9
Nat = NatDef + Inductive +
clasohm@923
    10
berghofe@5188
    11
setup
berghofe@5188
    12
  DatatypePackage.setup
wenzelm@4104
    13
berghofe@5188
    14
rep_datatype nat
berghofe@5188
    15
  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
berghofe@5188
    16
  inject   "[[Suc_Suc_eq]]"
berghofe@5188
    17
  induct   nat_induct
wenzelm@4104
    18
nipkow@2608
    19
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
nipkow@4640
    20
instance nat :: linorder (nat_le_linear)
oheimb@1660
    21
paulson@3370
    22
consts
paulson@3370
    23
  "^"           :: ['a::power,nat] => 'a            (infixr 80)
paulson@3370
    24
clasohm@923
    25
end