src/CTT/Arith.thy
 changeset 21404 eb85850d3eb7 parent 21210 c17fd2df4e9e child 27208 5fe899199f85
```--- a/src/CTT/Arith.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/CTT/Arith.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -13,22 +13,27 @@
subsection {* Arithmetic operators and their definitions *}

definition
-  add :: "[i,i]=>i"   (infixr "#+" 65)
+  add :: "[i,i]=>i"   (infixr "#+" 65) where
"a#+b == rec(a, b, %u v. succ(v))"

-  diff :: "[i,i]=>i"   (infixr "-" 65)
+definition
+  diff :: "[i,i]=>i"   (infixr "-" 65) where
"a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"

-  absdiff :: "[i,i]=>i"   (infixr "|-|" 65)
+definition
+  absdiff :: "[i,i]=>i"   (infixr "|-|" 65) where
"a|-|b == (a-b) #+ (b-a)"

-  mult :: "[i,i]=>i"   (infixr "#*" 70)
+definition
+  mult :: "[i,i]=>i"   (infixr "#*" 70) where
"a#*b == rec(a, 0, %u v. b #+ v)"

-  mod :: "[i,i]=>i"   (infixr "mod" 70)
+definition
+  mod :: "[i,i]=>i"   (infixr "mod" 70) where
"a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"

-  div :: "[i,i]=>i"   (infixr "div" 70)
+definition
+  div :: "[i,i]=>i"   (infixr "div" 70) where
"a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"

```