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
     5 
     6 Arithmetic on binary integers.
     7 *)
     8 
     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"
    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   
    26 rules
    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