src/HOL/Nat.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10435 b100e8d2c355
child 11134 8bc06c4202cd
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Nat.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Lawrence C Paulson
     4 
     5 Type "nat" is a linear order, and a datatype; arithmetic operators + -
     6 and * (for div, mod and dvd, see theory Divides).
     7 *)
     8 
     9 Nat = NatDef + Inductive +
    10 
    11 (* type "nat" is a linear order, and a datatype *)
    12 
    13 rep_datatype nat
    14   distinct Suc_not_Zero, Zero_not_Suc
    15   inject   Suc_Suc_eq
    16   induct   nat_induct
    17 
    18 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
    19 instance nat :: linorder (nat_le_linear)
    20 
    21 axclass power < term
    22 
    23 consts
    24   power :: ['a::power, nat] => 'a            (infixr "^" 80)
    25 
    26 
    27 (* arithmetic operators + - and * *)
    28 
    29 instance
    30   nat :: {plus, minus, times, power}
    31 
    32 (* size of a datatype value; overloaded *)
    33 consts size :: 'a => nat
    34 
    35 primrec
    36   add_0    "0 + n = n"
    37   add_Suc  "Suc m + n = Suc(m + n)"
    38 
    39 primrec
    40   diff_0   "m - 0 = m"
    41   diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    42 
    43 primrec
    44   mult_0   "0 * n = 0"
    45   mult_Suc "Suc m * n = n + (m * n)"
    46 
    47 end