(*  Title:      CTT/Arith.thy
    ID:         $Id: Arith.thy,v 1.6 2005/09/16 21:01:29 wenzelm Exp $
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

header {* Arithmetic operators and their definitions *}

theory Arith
imports Bool
begin

text {*
  Proves about elementary arithmetic: addition, multiplication, etc.
  Tests definitions and simplifier.
*}

consts
  "#+"  :: "[i,i]=>i"   (infixr 65)
  "-"   :: "[i,i]=>i"   (infixr 65)
  "|-|" :: "[i,i]=>i"   (infixr 65)
  "#*"  :: "[i,i]=>i"   (infixr 70)
  div   :: "[i,i]=>i"   (infixr 70)
  mod   :: "[i,i]=>i"   (infixr 70)

syntax (xsymbols)
  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)

syntax (HTML output)
  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)

defs
  add_def:     "a#+b == rec(a, b, %u v. succ(v))"
  diff_def:    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
  absdiff_def: "a|-|b == (a-b) #+ (b-a)"
  mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
  mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
  div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"

ML {* use_legacy_bindings (the_context ()) *}

end