src/HOL/Nat.thy
author paulson
Fri, 18 Sep 1998 14:36:54 +0200
changeset 5499 1787c44ae4ed
parent 5188 633ec5f6c155
child 5714 b4f2e281a907
permissions -rw-r--r--
updated comments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/Nat.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2541
diff changeset
     3
    Author:     Tobias Nipkow
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2541
diff changeset
     4
    Copyright   1997 TU Muenchen
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
5499
1787c44ae4ed updated comments
paulson
parents: 5188
diff changeset
     6
Type "nat" is a linear order, and a datatype
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
     9
Nat = NatDef + Inductive +
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
    11
setup
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
    12
  DatatypePackage.setup
4104
84433b1ab826 nat datatype_info moved to Nat.thy;
wenzelm
parents: 3370
diff changeset
    13
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
    14
rep_datatype nat
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
    15
  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
    16
  inject   "[[Suc_Suc_eq]]"
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 4640
diff changeset
    17
  induct   nat_induct
4104
84433b1ab826 nat datatype_info moved to Nat.thy;
wenzelm
parents: 3370
diff changeset
    18
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2541
diff changeset
    19
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4613
diff changeset
    20
instance nat :: linorder (nat_le_linear)
1660
8cb42cd97579 *** empty log message ***
oheimb
parents: 1625
diff changeset
    21
3370
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents: 2608
diff changeset
    22
consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents: 2608
diff changeset
    23
  "^"           :: ['a::power,nat] => 'a            (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents: 2608
diff changeset
    24
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
end