|
515
|
1 |
(* Title: ZF/ex/Bin.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1994 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Arithmetic on binary integers.
|
|
|
7 |
*)
|
|
|
8 |
|
|
589
|
9 |
Bin = Integ + Univ + "twos_compl" +
|
|
515
|
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 |
bin :: "i"
|
|
|
19 |
|
|
|
20 |
datatype
|
|
|
21 |
"bin" = Plus
|
|
|
22 |
| Minus
|
|
|
23 |
| "$$" ("w: bin", "b: bool") (infixl 60)
|
|
|
24 |
type_intrs "[bool_into_univ]"
|
|
|
25 |
|
|
753
|
26 |
defs
|
|
515
|
27 |
|
|
|
28 |
bin_rec_def
|
|
|
29 |
"bin_rec(z,a,b,h) == \
|
|
|
30 |
\ Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
|
|
|
31 |
|
|
|
32 |
integ_of_bin_def
|
|
|
33 |
"integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
|
|
|
34 |
|
|
|
35 |
bin_succ_def
|
|
|
36 |
"bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))"
|
|
|
37 |
|
|
|
38 |
bin_pred_def
|
|
|
39 |
"bin_pred(w0) == \
|
|
|
40 |
\ bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))"
|
|
|
41 |
|
|
|
42 |
bin_minus_def
|
|
|
43 |
"bin_minus(w0) == \
|
|
|
44 |
\ bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))"
|
|
|
45 |
|
|
|
46 |
bin_add_def
|
|
|
47 |
"bin_add(v0,w0) == \
|
|
|
48 |
\ bin_rec(v0, \
|
|
|
49 |
\ lam w:bin. w, \
|
|
|
50 |
\ lam w:bin. bin_pred(w), \
|
|
|
51 |
\ %v x r. lam w1:bin. \
|
|
|
52 |
\ bin_rec(w1, v$$x, bin_pred(v$$x), \
|
|
|
53 |
\ %w y s. (r`cond(x and y, bin_succ(w), w)) \
|
|
|
54 |
\ $$ (x xor y))) ` w0"
|
|
|
55 |
|
|
|
56 |
bin_mult_def
|
|
|
57 |
"bin_mult(v0,w) == \
|
|
|
58 |
\ bin_rec(v0, Plus, bin_minus(w), \
|
|
|
59 |
\ %v x r. cond(x, bin_add(r$$0,w), r$$0))"
|
|
|
60 |
end
|