src/ZF/ex/Bin.thy
 author lcp Fri Aug 12 12:28:46 1994 +0200 (1994-08-12) changeset 515 abcc438e7c27 child 589 31847a7504ec permissions -rw-r--r--
installation of new inductive/datatype sections
1 (*  Title: 	ZF/ex/Bin.thy
2     ID:         \$Id\$
3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1994  University of Cambridge
6 Arithmetic on binary integers.
7 *)
9 Bin = Integ + Univ +
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"
18   bin		   :: "i"
20 datatype
21   "bin" = Plus
22         | Minus
23         | "\$\$" ("w: bin", "b: bool")    (infixl 60)
24   type_intrs "[bool_into_univ]"
26 rules
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))"
32   integ_of_bin_def
33       "integ_of_bin(w) == bin_rec(w, \$#0, \$~(\$#1), %w x r. \$#x \$+ r \$+ r)"
35   bin_succ_def
36       "bin_succ(w0) == bin_rec(w0, Plus\$\$1, Plus, %w x r. cond(x, r\$\$0, w\$\$1))"
38   bin_pred_def
39       "bin_pred(w0) == \
40 \	bin_rec(w0, Minus, Minus\$\$0, %w x r. cond(x, w\$\$0, r\$\$1))"
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))"