src/HOL/Nat.thy
author berghofe
Fri, 24 Jul 1998 13:34:59 +0200
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.
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
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2541
diff changeset
     6
Nat is a partial order
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