src/CTT/Arith.thy
author wenzelm
Fri Sep 16 23:01:29 2005 +0200 (2005-09-16)
changeset 17441 5b5feca0344a
parent 12110 f8b4b11cd79d
child 19761 5cd82054c2c6
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      CTT/Arith.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 header {* Arithmetic operators and their definitions *}
     8 
     9 theory Arith
    10 imports Bool
    11 begin
    12 
    13 text {*
    14   Proves about elementary arithmetic: addition, multiplication, etc.
    15   Tests definitions and simplifier.
    16 *}
    17 
    18 consts
    19   "#+"  :: "[i,i]=>i"   (infixr 65)
    20   "-"   :: "[i,i]=>i"   (infixr 65)
    21   "|-|" :: "[i,i]=>i"   (infixr 65)
    22   "#*"  :: "[i,i]=>i"   (infixr 70)
    23   div   :: "[i,i]=>i"   (infixr 70)
    24   mod   :: "[i,i]=>i"   (infixr 70)
    25 
    26 syntax (xsymbols)
    27   "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
    28 
    29 syntax (HTML output)
    30   "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
    31 
    32 defs
    33   add_def:     "a#+b == rec(a, b, %u v. succ(v))"
    34   diff_def:    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
    35   absdiff_def: "a|-|b == (a-b) #+ (b-a)"
    36   mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
    37   mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    38   div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    39 
    40 ML {* use_legacy_bindings (the_context ()) *}
    41 
    42 end