src/ZF/ex/binfn.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 0 a5a9c433f639
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
clasohm@0
     1
(*  Title: 	ZF/bin
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Arithmetic on binary integers.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
BinFn = Integ + Bin +
clasohm@0
    10
consts
clasohm@0
    11
  bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
clasohm@0
    12
  integ_of_bin     :: "i=>i"
clasohm@0
    13
  bin_succ         :: "i=>i"
clasohm@0
    14
  bin_pred         :: "i=>i"
clasohm@0
    15
  bin_minus        :: "i=>i"
clasohm@0
    16
  bin_add,bin_mult :: "[i,i]=>i"
clasohm@0
    17
clasohm@0
    18
rules
clasohm@0
    19
clasohm@0
    20
  bin_rec_def
clasohm@0
    21
      "bin_rec(z,a,b,h) == \
clasohm@0
    22
\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
clasohm@0
    23
clasohm@0
    24
  integ_of_bin_def 
clasohm@0
    25
      "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
clasohm@0
    26
clasohm@0
    27
  bin_succ_def
clasohm@0
    28
      "bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))"
clasohm@0
    29
clasohm@0
    30
  bin_pred_def
clasohm@0
    31
      "bin_pred(w0) == \
clasohm@0
    32
\	bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))"
clasohm@0
    33
clasohm@0
    34
  bin_minus_def
clasohm@0
    35
      "bin_minus(w0) == \
clasohm@0
    36
\	bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))"
clasohm@0
    37
clasohm@0
    38
  bin_add_def
clasohm@0
    39
      "bin_add(v0,w0) == 			\
clasohm@0
    40
\       bin_rec(v0, 				\
clasohm@0
    41
\         lam w:bin. w,       		\
clasohm@0
    42
\         lam w:bin. bin_pred(w),	\
clasohm@0
    43
\         %v x r. lam w1:bin. 		\
clasohm@0
    44
\	           bin_rec(w1, v$$x, bin_pred(v$$x),	\
clasohm@0
    45
\		     %w y s. (r`cond(x and y, bin_succ(w), w)) \
clasohm@0
    46
\		             $$ (x xor y)))    ` w0"
clasohm@0
    47
clasohm@0
    48
  bin_mult_def
clasohm@0
    49
      "bin_mult(v0,w) == 			\
clasohm@0
    50
\       bin_rec(v0, Plus, bin_minus(w),		\
clasohm@0
    51
\         %v x r. cond(x, bin_add(r$$0,w), r$$0))"
clasohm@0
    52
end