--- a/src/ZF/Arith.thy Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Arith.thy Thu Jan 07 18:30:55 1999 +0100
@@ -7,20 +7,37 @@
*)
Arith = Epsilon +
+
+setup setup_datatypes
+
+(*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
+
+
consts
- rec :: [i, i, [i,i]=>i]=>i
"#*" :: [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)
-defs
- rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+primrec
+ add_0 "0 #+ n = n"
+ add_succ "succ(m) #+ n = succ(m #+ n)"
+
+primrec
+ diff_0 "m #- 0 = m"
+ diff_SUCC "m #- succ(n) = nat_case(0, %x. x, m #- n)"
- add_def "m#+n == rec(m, n, %u v. succ(v))"
- diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y. x))"
- mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
- mod_def "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
- div_def "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-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)))"
end