--- a/src/HOL/Nat.thy Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Nat.thy Tue Jul 25 00:06:46 2000 +0200
@@ -1,13 +1,15 @@
(* Title: HOL/Nat.thy
ID: $Id$
- Author: Tobias Nipkow
- Copyright 1997 TU Muenchen
+ Author: Tobias Nipkow and Lawrence C Paulson
-Type "nat" is a linear order, and a datatype
+Type "nat" is a linear order, and a datatype; arithmetic operators + -
+and * (for div, mod and dvd, see theory Divides).
*)
Nat = NatDef + Inductive +
+(* type "nat" is a linear order, and a datatype *)
+
rep_datatype nat
distinct Suc_not_Zero, Zero_not_Suc
inject Suc_Suc_eq
@@ -19,4 +21,25 @@
consts
"^" :: ['a::power,nat] => 'a (infixr 80)
+
+(* arithmetic operators + - and * *)
+
+instance
+ nat :: {plus, minus, times, power}
+
+(* size of a datatype value; overloaded *)
+consts size :: 'a => nat
+
+primrec
+ add_0 "0 + n = n"
+ add_Suc "Suc m + n = Suc(m + n)"
+
+primrec
+ diff_0 "m - 0 = m"
+ diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+
+primrec
+ mult_0 "0 * n = 0"
+ mult_Suc "Suc m * n = n + (m * n)"
+
end