--- a/src/ZF/Arith.thy Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Arith.thy Tue Aug 01 15:28:21 2000 +0200
@@ -6,38 +6,47 @@
Arithmetic operators and their definitions
*)
-Arith = Epsilon +
-
-setup setup_datatypes
+Arith = Univ +
-(*The natural numbers as a datatype*)
-rep_datatype
- elim natE
- induct nat_induct
- case_eqns nat_case_0, nat_case_succ
- recursor_eqns recursor_0, recursor_succ
+constdefs
+ pred :: i=>i (*inverse of succ*)
+ "pred(y) == THE x. y = succ(x)"
+ natify :: i=>i (*coerces non-nats to nats*)
+ "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
+ else 0)"
consts
- "#*" :: [i,i]=>i (infixl 70)
- div :: [i,i]=>i (infixl 70)
- mod :: [i,i]=>i (infixl 70)
- "#+" :: [i,i]=>i (infixl 65)
- "#-" :: [i,i]=>i (infixl 65)
+ "##*" :: [i,i]=>i (infixl 70)
+ "##+" :: [i,i]=>i (infixl 65)
+ "##-" :: [i,i]=>i (infixl 65)
primrec
- add_0 "0 #+ n = n"
- add_succ "succ(m) #+ n = succ(m #+ n)"
+ raw_add_0 "0 ##+ n = n"
+ raw_add_succ "succ(m) ##+ n = succ(m ##+ n)"
+
+primrec
+ raw_diff_0 "m ##- 0 = m"
+ raw_diff_succ "m ##- succ(n) = nat_case(0, %x. x, m ##- n)"
primrec
- diff_0 "m #- 0 = m"
- diff_SUCC "m #- succ(n) = nat_case(0, %x. x, m #- n)"
+ raw_mult_0 "0 ##* n = 0"
+ raw_mult_succ "succ(m) ##* n = n ##+ (m ##* n)"
+
+constdefs
+ add :: [i,i]=>i (infixl "#+" 65)
+ "m #+ n == natify(m) ##+ natify(n)"
+
+ diff :: [i,i]=>i (infixl "#-" 65)
+ "m #- n == natify(m) ##- natify(n)"
-primrec
- mult_0 "0 #* n = 0"
- mult_succ "succ(m) #* n = n #+ (m #* n)"
-
-defs
- mod_def "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
- div_def "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
+ mult :: [i,i]=>i (infixl "#*" 70)
+ "m #* n == natify(m) ##* natify(n)"
+
+ div :: [i,i]=>i (infixl "div" 70)
+ "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
+
+ mod :: [i,i]=>i (infixl "mod" 70)
+ "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
+
end