src/HOL/Nat.thy
author oheimb
Thu Feb 15 16:00:36 2001 +0100 (2001-02-15)
changeset 11134 8bc06c4202cd
parent 10435 b100e8d2c355
child 11325 a5e0289dd56c
permissions -rw-r--r--
added nat as instance of new wellorder axclass
     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 wellfounded 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 instance nat :: wellorder (wf_less)
    21 
    22 axclass power < term
    23 
    24 consts
    25   power :: ['a::power, nat] => 'a            (infixr "^" 80)
    26 
    27 
    28 (* arithmetic operators + - and * *)
    29 
    30 instance
    31   nat :: {plus, minus, times, power}
    32 
    33 (* size of a datatype value; overloaded *)
    34 consts size :: 'a => nat
    35 
    36 primrec
    37   add_0    "0 + n = n"
    38   add_Suc  "Suc m + n = Suc(m + n)"
    39 
    40 primrec
    41   diff_0   "m - 0 = m"
    42   diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    43 
    44 primrec
    45   mult_0   "0 * n = 0"
    46   mult_Suc "Suc m * n = n + (m * n)"
    47 
    48 end