author | wenzelm |
Sat, 02 Sep 2000 21:51:14 +0200 | |
changeset 9805 | 10b617bdd028 |
parent 9570 | e16e168984e1 |
child 11381 | 4ab3b7b0938f |
permissions | -rw-r--r-- |
5528 | 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 |
The sign Pls stands for an infinite string of leading 0's. |
|
9 |
The sign Min stands for an infinite string of leading 1's. |
|
10 |
||
11 |
A number can have multiple representations, namely leading 0's with sign |
|
12 |
Pls and leading 1's with sign Min. See twos-compl.ML/int_of_binary for |
|
13 |
the numerical interpretation. |
|
14 |
||
15 |
The representation expects that (m mod 2) is 0 or 1, even if m is negative; |
|
16 |
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 |
|
17 |
||
18 |
Division is not defined yet! |
|
19 |
*) |
|
20 |
||
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
21 |
Bin = Int + Datatype + |
5528 | 22 |
|
6117 | 23 |
consts bin :: i |
24 |
datatype |
|
25 |
"bin" = Pls |
|
26 |
| Min |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
27 |
| Bit ("w: bin", "b: bool") (infixl "BIT" 90) |
6117 | 28 |
|
29 |
syntax |
|
30 |
"_Int" :: xnum => i ("_") |
|
31 |
||
5528 | 32 |
consts |
33 |
integ_of :: i=>i |
|
34 |
NCons :: [i,i]=>i |
|
35 |
bin_succ :: i=>i |
|
36 |
bin_pred :: i=>i |
|
37 |
bin_minus :: i=>i |
|
38 |
bin_add :: [i,i]=>i |
|
9207 | 39 |
bin_adder :: i=>i |
5528 | 40 |
bin_mult :: [i,i]=>i |
41 |
||
6046 | 42 |
primrec |
6153 | 43 |
integ_of_Pls "integ_of (Pls) = $# 0" |
9548 | 44 |
integ_of_Min "integ_of (Min) = $-($#1)" |
6153 | 45 |
integ_of_BIT "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)" |
5528 | 46 |
|
47 |
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **) |
|
48 |
||
6046 | 49 |
primrec (*NCons adds a bit, suppressing leading 0s and 1s*) |
6153 | 50 |
NCons_Pls "NCons (Pls,b) = cond(b,Pls BIT b,Pls)" |
51 |
NCons_Min "NCons (Min,b) = cond(b,Min,Min BIT b)" |
|
52 |
NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b" |
|
5528 | 53 |
|
6153 | 54 |
primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*) |
55 |
bin_succ_Pls "bin_succ (Pls) = Pls BIT 1" |
|
56 |
bin_succ_Min "bin_succ (Min) = Pls" |
|
57 |
bin_succ_BIT "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))" |
|
5528 | 58 |
|
6046 | 59 |
primrec (*predecessor*) |
6153 | 60 |
bin_pred_Pls "bin_pred (Pls) = Min" |
61 |
bin_pred_Min "bin_pred (Min) = Min BIT 0" |
|
62 |
bin_pred_BIT "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)" |
|
5528 | 63 |
|
6046 | 64 |
primrec (*unary negation*) |
65 |
bin_minus_Pls |
|
66 |
"bin_minus (Pls) = Pls" |
|
67 |
bin_minus_Min |
|
6153 | 68 |
"bin_minus (Min) = Pls BIT 1" |
69 |
bin_minus_BIT |
|
70 |
"bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)), |
|
71 |
bin_minus(w) BIT 0)" |
|
6046 | 72 |
|
73 |
primrec (*sum*) |
|
9207 | 74 |
bin_adder_Pls |
75 |
"bin_adder (Pls) = (lam w:bin. w)" |
|
76 |
bin_adder_Min |
|
77 |
"bin_adder (Min) = (lam w:bin. bin_pred(w))" |
|
78 |
bin_adder_BIT |
|
79 |
"bin_adder (v BIT x) = |
|
80 |
(lam w:bin. |
|
81 |
bin_case (v BIT x, bin_pred(v BIT x), |
|
82 |
%w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w), |
|
83 |
x xor y), |
|
84 |
w))" |
|
5528 | 85 |
|
9207 | 86 |
(*The bin_case above replaces the following mutually recursive function: |
87 |
primrec |
|
6153 | 88 |
"adding (v,x,Pls) = v BIT x" |
89 |
"adding (v,x,Min) = bin_pred(v BIT x)" |
|
9207 | 90 |
"adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)), |
6153 | 91 |
x xor y)" |
9207 | 92 |
*) |
93 |
||
94 |
defs |
|
95 |
bin_add_def "bin_add(v,w) == bin_adder(v)`w" |
|
96 |
||
5528 | 97 |
|
6046 | 98 |
primrec |
99 |
bin_mult_Pls |
|
6153 | 100 |
"bin_mult (Pls,w) = Pls" |
6046 | 101 |
bin_mult_Min |
6153 | 102 |
"bin_mult (Min,w) = bin_minus(w)" |
103 |
bin_mult_BIT |
|
104 |
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w), |
|
105 |
NCons(bin_mult(v,w),0))" |
|
6046 | 106 |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
107 |
setup NumeralSyntax.setup |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
108 |
|
5528 | 109 |
end |
110 |
||
111 |
||
112 |
ML |