src/ZF/ex/binfn.thy
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/binfn.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,52 @@
     1.4 +(*  Title: 	ZF/bin
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Arithmetic on binary integers.
    1.10 +*)
    1.11 +
    1.12 +BinFn = Integ + Bin +
    1.13 +consts
    1.14 +  bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
    1.15 +  integ_of_bin     :: "i=>i"
    1.16 +  bin_succ         :: "i=>i"
    1.17 +  bin_pred         :: "i=>i"
    1.18 +  bin_minus        :: "i=>i"
    1.19 +  bin_add,bin_mult :: "[i,i]=>i"
    1.20 +
    1.21 +rules
    1.22 +
    1.23 +  bin_rec_def
    1.24 +      "bin_rec(z,a,b,h) == \
    1.25 +\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
    1.26 +
    1.27 +  integ_of_bin_def 
    1.28 +      "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
    1.29 +
    1.30 +  bin_succ_def
    1.31 +      "bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))"
    1.32 +
    1.33 +  bin_pred_def
    1.34 +      "bin_pred(w0) == \
    1.35 +\	bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))"
    1.36 +
    1.37 +  bin_minus_def
    1.38 +      "bin_minus(w0) == \
    1.39 +\	bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))"
    1.40 +
    1.41 +  bin_add_def
    1.42 +      "bin_add(v0,w0) == 			\
    1.43 +\       bin_rec(v0, 				\
    1.44 +\         lam w:bin. w,       		\
    1.45 +\         lam w:bin. bin_pred(w),	\
    1.46 +\         %v x r. lam w1:bin. 		\
    1.47 +\	           bin_rec(w1, v$$x, bin_pred(v$$x),	\
    1.48 +\		     %w y s. (r`cond(x and y, bin_succ(w), w)) \
    1.49 +\		             $$ (x xor y)))    ` w0"
    1.50 +
    1.51 +  bin_mult_def
    1.52 +      "bin_mult(v0,w) == 			\
    1.53 +\       bin_rec(v0, Plus, bin_minus(w),		\
    1.54 +\         %v x r. cond(x, bin_add(r$$0,w), r$$0))"
    1.55 +end