author  paulson 
Tue, 01 Aug 2000 18:26:34 +0200  
changeset 9492  72e429c66608 
parent 9491  1a36151ee2fc 
child 9654  9754ba005b64 
permissions  rwrr 
1478  1 
(* Title: ZF/arith.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Arithmetic operators and their definitions 

7 
*) 

8 

9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

9 
Arith = Univ + 
6070  10 

9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

11 
constdefs 
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

12 
pred :: i=>i (*inverse of succ*) 
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

13 
"pred(y) == THE x. y = succ(x)" 
6070  14 

9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

15 
natify :: i=>i (*coerces nonnats to nats*) 
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

16 
"natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a)) 
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

17 
else 0)" 
6070  18 

0  19 
consts 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

20 
raw_add, raw_diff, raw_mult :: [i,i]=>i 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

21 

72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

22 
primrec 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

23 
"raw_add (0, n) = n" 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

24 
"raw_add (succ(m), n) = succ(raw_add(m, n))" 
0  25 

6070  26 
primrec 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

27 
raw_diff_0 "raw_diff(m, 0) = m" 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

28 
raw_diff_succ "raw_diff(m, succ(n)) = 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

29 
nat_case(0, %x. x, raw_diff(m, n))" 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

30 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

31 
primrec 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

32 
"raw_mult(0, n) = 0" 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

33 
"raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))" 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

34 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

35 
constdefs 
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

36 
add :: [i,i]=>i (infixl "#+" 65) 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

37 
"m #+ n == raw_add (natify(m), natify(n))" 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

38 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

39 
diff :: [i,i]=>i (infixl "#" 65) 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

40 
"m # n == raw_diff (natify(m), natify(n))" 
0  41 

9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

42 
mult :: [i,i]=>i (infixl "#*" 70) 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

43 
"m #* n == raw_mult (natify(m), natify(n))" 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

44 

72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

45 
raw_div :: [i,i]=>i 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

46 
"raw_div (m, n) == 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

47 
transrec(m, %j f. if j<n  n=0 then 0 else succ(f`(j#n)))" 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

48 

72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

49 
raw_mod :: [i,i]=>i 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

50 
"raw_mod (m, n) == 
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

51 
transrec(m, %j f. if j<n  n=0 then j else f`(j#n))" 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

52 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

53 
div :: [i,i]=>i (infixl "div" 70) 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

54 
"m div n == raw_div (natify(m), natify(n))" 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

55 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

56 
mod :: [i,i]=>i (infixl "mod" 70) 
9492
72e429c66608
used natify with div and mod; also put in the dividebyzero trick
paulson
parents:
9491
diff
changeset

57 
"m mod n == raw_mod (natify(m), natify(n))" 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6070
diff
changeset

58 

0  59 
end 