src/HOL/Arith.thy
changeset 923 ff1574a81019
child 965 24eef3860714
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Arith.thy	Fri Mar 03 12:02:25 1995 +0100
     1.3 @@ -0,0 +1,31 @@
     1.4 +(*  Title:      HOL/Arith.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Arithmetic operators and their definitions
    1.10 +*)
    1.11 +
    1.12 +Arith = Nat +
    1.13 +
    1.14 +instance
    1.15 +  nat :: {plus, minus, times}
    1.16 +
    1.17 +consts
    1.18 +  pred      :: "nat => nat"
    1.19 +  div, mod  :: "[nat, nat] => nat"  (infixl 70)
    1.20 +
    1.21 +defs
    1.22 +  pred_def  "pred(m) == nat_rec m 0 (%n r.n)"
    1.23 +  add_def   "m+n == nat_rec m n (%u v. Suc(v))"
    1.24 +  diff_def  "m-n == nat_rec n m (%u v. pred(v))"
    1.25 +  mult_def  "m*n == nat_rec m 0 (%u v. n + v)"
    1.26 +  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.(if (j<n) j (f (j-n))))"
    1.27 +  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.(if (j<n) 0 (Suc (f (j-n)))))"
    1.28 +end
    1.29 +
    1.30 +(*"Difference" is subtraction of natural numbers.
    1.31 +  There are no negative numbers; we have
    1.32 +     m - n = 0  iff  m<=n   and     m - n = Suc(k) iff m>n.
    1.33 +  Also, nat_rec(m, 0, %z w.z) is pred(m).   *)
    1.34 +