src/CTT/arith.thy
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 0 a5a9c433f639
permissions -rw-r--r--
Cosmetic re-ordering of declarations
clasohm@0
     1
(*  Title: 	CTT/arith
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Arithmetic operators and their definitions
clasohm@0
     7
clasohm@0
     8
Proves about elementary arithmetic: addition, multiplication, etc.
clasohm@0
     9
Tests definitions and simplifier.
clasohm@0
    10
*)
clasohm@0
    11
clasohm@0
    12
Arith = CTT +
clasohm@0
    13
clasohm@0
    14
consts "#+","-","|-|"	:: "[i,i]=>i"	(infixr 65)
clasohm@0
    15
       "#*",div,mod     :: "[i,i]=>i"	(infixr 70)
clasohm@0
    16
clasohm@0
    17
rules
clasohm@0
    18
  add_def     "a#+b == rec(a, b, %u v.succ(v))"  
clasohm@0
    19
  diff_def    "a-b == rec(b, a, %u v.rec(v, 0, %x y.x))"  
clasohm@0
    20
  absdiff_def "a|-|b == (a-b) #+ (b-a)"  
clasohm@0
    21
  mult_def    "a#*b == rec(a, 0, %u v. b #+ v)"  
clasohm@0
    22
  mod_def     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))"
clasohm@0
    23
  div_def     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y.v))"
clasohm@0
    24
end