src/ZF/ex/Bin.thy
 author lcp Wed, 07 Sep 1994 17:28:53 +0200 changeset 589 31847a7504ec parent 515 abcc438e7c27 child 753 ec86863e87c8 permissions -rw-r--r--
```
(*  Title: 	ZF/ex/Bin.thy
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

Arithmetic on binary integers.
*)

Bin = Integ + Univ + "twos_compl" +
consts
bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
integ_of_bin     :: "i=>i"
bin_succ         :: "i=>i"
bin_pred         :: "i=>i"
bin_minus        :: "i=>i"

bin		   :: "i"

datatype
"bin" = Plus
| Minus
| "\$\$" ("w: bin", "b: bool")    (infixl 60)
type_intrs "[bool_into_univ]"

rules

bin_rec_def
"bin_rec(z,a,b,h) == \
\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"

integ_of_bin_def
"integ_of_bin(w) == bin_rec(w, \$#0, \$~(\$#1), %w x r. \$#x \$+ r \$+ r)"

bin_succ_def
"bin_succ(w0) == bin_rec(w0, Plus\$\$1, Plus, %w x r. cond(x, r\$\$0, w\$\$1))"

bin_pred_def
"bin_pred(w0) == \
\	bin_rec(w0, Minus, Minus\$\$0, %w x r. cond(x, w\$\$0, r\$\$1))"

bin_minus_def
"bin_minus(w0) == \
\	bin_rec(w0, Plus, Plus\$\$1, %w x r. cond(x, bin_pred(r\$\$0), r\$\$0))"

\       bin_rec(v0, 				\
\         lam w:bin. w,       		\
\         lam w:bin. bin_pred(w),	\
\         %v x r. lam w1:bin. 		\
\	           bin_rec(w1, v\$\$x, bin_pred(v\$\$x),	\
\		     %w y s. (r`cond(x and y, bin_succ(w), w)) \
\		             \$\$ (x xor y)))    ` w0"

bin_mult_def
"bin_mult(v0,w) == 			\
\       bin_rec(v0, Plus, bin_minus(w),		\
\         %v x r. cond(x, bin_add(r\$\$0,w), r\$\$0))"
end
```