src/HOL/Nat.thy
changeset 9436 62bb04ab4b01
parent 7702 35c7e0df749f
child 10435 b100e8d2c355
     1.1 --- a/src/HOL/Nat.thy	Tue Jul 25 00:03:39 2000 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jul 25 00:06:46 2000 +0200
     1.3 @@ -1,13 +1,15 @@
     1.4  (*  Title:      HOL/Nat.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1997 TU Muenchen
     1.8 +    Author:     Tobias Nipkow and Lawrence C Paulson
     1.9  
    1.10 -Type "nat" is a linear order, and a datatype
    1.11 +Type "nat" is a linear order, and a datatype; arithmetic operators + -
    1.12 +and * (for div, mod and dvd, see theory Divides).
    1.13  *)
    1.14  
    1.15  Nat = NatDef + Inductive +
    1.16  
    1.17 +(* type "nat" is a linear order, and a datatype *)
    1.18 +
    1.19  rep_datatype nat
    1.20    distinct Suc_not_Zero, Zero_not_Suc
    1.21    inject   Suc_Suc_eq
    1.22 @@ -19,4 +21,25 @@
    1.23  consts
    1.24    "^"           :: ['a::power,nat] => 'a            (infixr 80)
    1.25  
    1.26 +
    1.27 +(* arithmetic operators + - and * *)
    1.28 +
    1.29 +instance
    1.30 +  nat :: {plus, minus, times, power}
    1.31 +
    1.32 +(* size of a datatype value; overloaded *)
    1.33 +consts size :: 'a => nat
    1.34 +
    1.35 +primrec
    1.36 +  add_0    "0 + n = n"
    1.37 +  add_Suc  "Suc m + n = Suc(m + n)"
    1.38 +
    1.39 +primrec
    1.40 +  diff_0   "m - 0 = m"
    1.41 +  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.42 +
    1.43 +primrec
    1.44 +  mult_0   "0 * n = 0"
    1.45 +  mult_Suc "Suc m * n = n + (m * n)"
    1.46 +
    1.47  end