src/ZF/Arith.thy
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 25 3ac1c0c0016e
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
clasohm@0
     1
(*  Title: 	ZF/arith.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Arithmetic operators and their definitions
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
Arith = Epsilon +
clasohm@0
    10
consts
clasohm@0
    11
    rec  :: "[i, i, [i,i]=>i]=>i"
clasohm@0
    12
    "#*" :: "[i,i]=>i"      		(infixl 70)
clasohm@0
    13
    div  :: "[i,i]=>i"      		(infixl 70) 
clasohm@0
    14
    mod  :: "[i,i]=>i"      		(infixl 70)
clasohm@0
    15
    "#+" :: "[i,i]=>i"      		(infixl 65)
clasohm@0
    16
    "#-" :: "[i,i]=>i"      		(infixl 65)
clasohm@0
    17
clasohm@0
    18
rules
lcp@6
    19
    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
clasohm@0
    20
clasohm@0
    21
    add_def  "m#+n == rec(m, n, %u v.succ(v))"
clasohm@0
    22
    diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
clasohm@0
    23
    mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
clasohm@0
    24
    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
clasohm@0
    25
    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
clasohm@0
    26
end