src/ZF/arith.thy
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/arith.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Arithmetic operators and their definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
Arith = Epsilon +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    rec  :: "[i, i, [i,i]=>i]=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    "#*" :: "[i,i]=>i"      		(infixl 70)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
    div  :: "[i,i]=>i"      		(infixl 70) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
    mod  :: "[i,i]=>i"      		(infixl 70)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
    "#+" :: "[i,i]=>i"      		(infixl 65)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    "#-" :: "[i,i]=>i"      		(infixl 65)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
rules
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    19
    rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    add_def  "m#+n == rec(m, n, %u v.succ(v))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
    diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
    mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
end