src/ZF/ex/Bin.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 589 31847a7504ec
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp@515
     1
(*  Title: 	ZF/ex/Bin.thy
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Arithmetic on binary integers.
lcp@515
     7
*)
lcp@515
     8
lcp@515
     9
Bin = Integ + Univ + 
lcp@515
    10
consts
lcp@515
    11
  bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
lcp@515
    12
  integ_of_bin     :: "i=>i"
lcp@515
    13
  bin_succ         :: "i=>i"
lcp@515
    14
  bin_pred         :: "i=>i"
lcp@515
    15
  bin_minus        :: "i=>i"
lcp@515
    16
  bin_add,bin_mult :: "[i,i]=>i"
lcp@515
    17
lcp@515
    18
  bin		   :: "i"
lcp@515
    19
lcp@515
    20
datatype
lcp@515
    21
  "bin" = Plus
lcp@515
    22
        | Minus
lcp@515
    23
        | "$$" ("w: bin", "b: bool")    (infixl 60)
lcp@515
    24
  type_intrs "[bool_into_univ]"
lcp@515
    25
  
lcp@515
    26
rules
lcp@515
    27
lcp@515
    28
  bin_rec_def
lcp@515
    29
      "bin_rec(z,a,b,h) == \
lcp@515
    30
\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
lcp@515
    31
lcp@515
    32
  integ_of_bin_def 
lcp@515
    33
      "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
lcp@515
    34
lcp@515
    35
  bin_succ_def
lcp@515
    36
      "bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))"
lcp@515
    37
lcp@515
    38
  bin_pred_def
lcp@515
    39
      "bin_pred(w0) == \
lcp@515
    40
\	bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))"
lcp@515
    41
lcp@515
    42
  bin_minus_def
lcp@515
    43
      "bin_minus(w0) == \
lcp@515
    44
\	bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))"
lcp@515
    45
lcp@515
    46
  bin_add_def
lcp@515
    47
      "bin_add(v0,w0) == 			\
lcp@515
    48
\       bin_rec(v0, 				\
lcp@515
    49
\         lam w:bin. w,       		\
lcp@515
    50
\         lam w:bin. bin_pred(w),	\
lcp@515
    51
\         %v x r. lam w1:bin. 		\
lcp@515
    52
\	           bin_rec(w1, v$$x, bin_pred(v$$x),	\
lcp@515
    53
\		     %w y s. (r`cond(x and y, bin_succ(w), w)) \
lcp@515
    54
\		             $$ (x xor y)))    ` w0"
lcp@515
    55
lcp@515
    56
  bin_mult_def
lcp@515
    57
      "bin_mult(v0,w) == 			\
lcp@515
    58
\       bin_rec(v0, Plus, bin_minus(w),		\
lcp@515
    59
\         %v x r. cond(x, bin_add(r$$0,w), r$$0))"
lcp@515
    60
end