src/ZF/Arith.thy
author paulson
Tue, 01 Aug 2000 18:26:34 +0200
changeset 9492 72e429c66608
parent 9491 1a36151ee2fc
child 9654 9754ba005b64
permissions -rw-r--r--
used natify with div and mod; also put in the divide-by-zero trick
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/arith.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
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
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
     9
Arith = Univ + 
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 3840
diff changeset
    10
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    11
constdefs
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    12
  pred   :: i=>i    (*inverse of succ*)
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    13
    "pred(y) == THE x. y = succ(x)"
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 3840
diff changeset
    14
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    15
  natify :: i=>i    (*coerces non-nats to nats*)
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    16
    "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    17
                                                    else 0)"
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 3840
diff changeset
    18
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
consts
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    20
    raw_add, raw_diff, raw_mult  :: [i,i]=>i
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    21
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    22
primrec
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    23
  "raw_add (0, n) = n"
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    24
  "raw_add (succ(m), n) = succ(raw_add(m, n))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 3840
diff changeset
    26
primrec
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    27
  raw_diff_0     "raw_diff(m, 0) = m"
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    28
  raw_diff_succ  "raw_diff(m, succ(n)) = 
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    29
                    nat_case(0, %x. x, raw_diff(m, n))"
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    30
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    31
primrec
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    32
  "raw_mult(0, n) = 0"
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    33
  "raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))"
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    34
 
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    35
constdefs
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    36
  add :: [i,i]=>i                    (infixl "#+" 65)
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    37
    "m #+ n == raw_add (natify(m), natify(n))"
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    38
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    39
  diff :: [i,i]=>i                    (infixl "#-" 65)
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    40
    "m #- n == raw_diff (natify(m), natify(n))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    42
  mult :: [i,i]=>i                    (infixl "#*" 70)
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    43
    "m #* n == raw_mult (natify(m), natify(n))"
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    44
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    45
  raw_div  :: [i,i]=>i
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    46
    "raw_div (m, n) == 
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    47
       transrec(m, %j f. if j<n | n=0 then 0 else succ(f`(j#-n)))"
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    48
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    49
  raw_mod  :: [i,i]=>i
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    50
    "raw_mod (m, n) == 
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    51
       transrec(m, %j f. if j<n | n=0 then j else f`(j#-n))"
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    52
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    53
  div  :: [i,i]=>i                    (infixl "div" 70) 
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    54
    "m div n == raw_div (natify(m), natify(n))"
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    55
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    56
  mod  :: [i,i]=>i                    (infixl "mod" 70)
9492
72e429c66608 used natify with div and mod; also put in the divide-by-zero trick
paulson
parents: 9491
diff changeset
    57
    "m mod n == raw_mod (natify(m), natify(n))"
9491
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents: 6070
diff changeset
    58
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
end