src/HOL/Arith.thy
 changeset 3366 2402c6ab1561 parent 3308 da002cef7090 child 4360 40e5c97e988d
```     1.1 --- a/src/HOL/Arith.thy	Fri May 30 15:14:59 1997 +0200
1.2 +++ b/src/HOL/Arith.thy	Fri May 30 15:15:57 1997 +0200
1.3 @@ -3,38 +3,32 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1993  University of Cambridge
1.6
1.7 -Arithmetic operators and their definitions
1.8 +Arithmetic operators + - and * (for div, mod and dvd, see Divides)
1.9  *)
1.10
1.11  Arith = Nat +
1.12
1.13  instance
1.14 -  nat :: {plus, minus, times}
1.15 +  nat :: {plus, minus, times, power}
1.16
1.17  consts
1.18    pred      :: nat => nat
1.19 -  div, mod  :: [nat, nat] => nat  (infixl 70)
1.20    (* size of a datatype value; overloaded *)
1.21    size      :: 'a => nat
1.22
1.23  defs
1.24    pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
1.25
1.26 -  mod_def   "m mod n == wfrec (trancl pred_nat)
1.27 -                          (%f j. if j<n then j else f (j-n)) m"
1.28 -  div_def   "m div n == wfrec (trancl pred_nat)
1.29 -                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
1.30 -
1.31  primrec "op +" nat
1.32 -  "0 + n = n"
1.33 -  "Suc m + n = Suc(m + n)"
1.34 +  add_0    "0 + n = n"
1.35 +  add_Suc  "Suc m + n = Suc(m + n)"
1.36
1.37  primrec "op -" nat
1.38    diff_0   "m - 0 = m"
1.39    diff_Suc "m - Suc n = pred(m - n)"
1.40
1.41  primrec "op *"  nat
1.42 -  "0 * n = 0"
1.43 -  "Suc m * n = n + (m * n)"
1.44 +  mult_0   "0 * n = 0"
1.45 +  mult_Suc "Suc m * n = n + (m * n)"
1.46
1.47  end
```