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