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