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