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