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 +
```