src/CTT/Arith.thy
changeset 19762 957bcf55c98f
parent 19761 5cd82054c2c6
child 21210 c17fd2df4e9e
     1.1 --- a/src/CTT/Arith.thy	Fri Jun 02 18:15:38 2006 +0200
     1.2 +++ b/src/CTT/Arith.thy	Fri Jun 02 18:24:48 2006 +0200
     1.3 @@ -12,27 +12,32 @@
     1.4  
     1.5  subsection {* Arithmetic operators and their definitions *}
     1.6  
     1.7 -consts
     1.8 -  "#+"  :: "[i,i]=>i"   (infixr 65)
     1.9 -  "-"   :: "[i,i]=>i"   (infixr 65)
    1.10 -  "|-|" :: "[i,i]=>i"   (infixr 65)
    1.11 -  "#*"  :: "[i,i]=>i"   (infixr 70)
    1.12 -  div   :: "[i,i]=>i"   (infixr 70)
    1.13 -  mod   :: "[i,i]=>i"   (infixr 70)
    1.14 +definition
    1.15 +  add :: "[i,i]=>i"   (infixr "#+" 65)
    1.16 +  "a#+b == rec(a, b, %u v. succ(v))"
    1.17  
    1.18 -syntax (xsymbols)
    1.19 -  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
    1.20 +  diff :: "[i,i]=>i"   (infixr "-" 65)
    1.21 +  "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
    1.22 +
    1.23 +  absdiff :: "[i,i]=>i"   (infixr "|-|" 65)
    1.24 +  "a|-|b == (a-b) #+ (b-a)"
    1.25 +
    1.26 +  mult :: "[i,i]=>i"   (infixr "#*" 70)
    1.27 +  "a#*b == rec(a, 0, %u v. b #+ v)"
    1.28  
    1.29 -syntax (HTML output)
    1.30 -  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
    1.31 +  mod :: "[i,i]=>i"   (infixr "mod" 70)
    1.32 +  "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    1.33 +
    1.34 +  div :: "[i,i]=>i"   (infixr "div" 70)
    1.35 +  "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    1.36 +
    1.37  
    1.38 -defs
    1.39 -  add_def:     "a#+b == rec(a, b, %u v. succ(v))"
    1.40 -  diff_def:    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
    1.41 -  absdiff_def: "a|-|b == (a-b) #+ (b-a)"
    1.42 -  mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
    1.43 -  mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    1.44 -  div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    1.45 +const_syntax (xsymbols)
    1.46 +  mult  (infixr "#\<times>" 70)
    1.47 +
    1.48 +const_syntax (HTML output)
    1.49 +  mult (infixr "#\<times>" 70)
    1.50 +
    1.51  
    1.52  lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
    1.53