src/ZF/Integ/Bin.thy
author wenzelm
Wed, 14 Nov 2001 18:46:07 +0100
changeset 12182 3f820a21dcc1
parent 11381 4ab3b7b0938f
child 13560 d9651081578b
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     1
(*  Title:      ZF/ex/Bin.thy
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     2
    ID:         $Id$
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     5
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     6
Arithmetic on binary integers.
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     7
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     8
   The sign Pls stands for an infinite string of leading 0's.
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
     9
   The sign Min stands for an infinite string of leading 1's.
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    10
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    11
A number can have multiple representations, namely leading 0's with sign
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    12
Pls and leading 1's with sign Min.  See twos-compl.ML/int_of_binary for
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    13
the numerical interpretation.
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    14
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    15
The representation expects that (m mod 2) is 0 or 1, even if m is negative;
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    16
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    17
*)
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    18
9570
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9548
diff changeset
    19
Bin = Int + Datatype +
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    20
6117
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    21
consts  bin :: i
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    22
datatype
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    23
  "bin" = Pls
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    24
        | Min
9570
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9548
diff changeset
    25
        | Bit ("w: bin", "b: bool")	(infixl "BIT" 90)
6117
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    26
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    27
syntax
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    28
  "_Int"           :: xnum => i        ("_")
f9aad8ccd590 tidying of datatype and inductive definitions
paulson
parents: 6046
diff changeset
    29
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    30
consts
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    31
  integ_of  :: i=>i
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    32
  NCons     :: [i,i]=>i
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    33
  bin_succ  :: i=>i
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    34
  bin_pred  :: i=>i
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    35
  bin_minus :: i=>i
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    36
  bin_add   :: [i,i]=>i
9207
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    37
  bin_adder :: i=>i
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    38
  bin_mult  :: [i,i]=>i
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    39
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    40
primrec
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    41
  integ_of_Pls  "integ_of (Pls)     = $# 0"
9548
15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF
paulson
parents: 9207
diff changeset
    42
  integ_of_Min  "integ_of (Min)     = $-($#1)"
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    43
  integ_of_BIT  "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    44
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    45
    (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    46
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    47
primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    48
  NCons_Pls "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    49
  NCons_Min "NCons (Min,b)     = cond(b,Min,Min BIT b)"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    50
  NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b"
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    51
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    52
primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    53
  bin_succ_Pls  "bin_succ (Pls)     = Pls BIT 1"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    54
  bin_succ_Min  "bin_succ (Min)     = Pls"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    55
  bin_succ_BIT  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    56
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    57
primrec (*predecessor*)
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    58
  bin_pred_Pls  "bin_pred (Pls)     = Min"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    59
  bin_pred_Min  "bin_pred (Min)     = Min BIT 0"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    60
  bin_pred_BIT  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    61
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    62
primrec (*unary negation*)
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    63
  bin_minus_Pls
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    64
    "bin_minus (Pls)       = Pls"
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    65
  bin_minus_Min
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    66
    "bin_minus (Min)       = Pls BIT 1"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    67
  bin_minus_BIT
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    68
    "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    69
				bin_minus(w) BIT 0)"
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    70
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    71
primrec (*sum*)
9207
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    72
  bin_adder_Pls
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    73
    "bin_adder (Pls)     = (lam w:bin. w)"
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    74
  bin_adder_Min
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    75
    "bin_adder (Min)     = (lam w:bin. bin_pred(w))"
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    76
  bin_adder_BIT
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    77
    "bin_adder (v BIT x) = 
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    78
       (lam w:bin. 
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    79
         bin_case (v BIT x, bin_pred(v BIT x), 
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    80
                   %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w),  
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    81
                               x xor y),
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    82
                   w))"
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    83
9207
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    84
(*The bin_case above replaces the following mutually recursive function:
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    85
primrec
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    86
  "adding (v,x,Pls)     = v BIT x"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    87
  "adding (v,x,Min)     = bin_pred(v BIT x)"
9207
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    88
  "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)), 
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    89
				x xor y)"
9207
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    90
*)
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    91
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    92
defs
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    93
  bin_add_def "bin_add(v,w) == bin_adder(v)`w"
0c294bd701ea removed the mutual recursion from "bin_add"
paulson
parents: 6153
diff changeset
    94
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
    95
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    96
primrec
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    97
  bin_mult_Pls
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
    98
    "bin_mult (Pls,w)     = Pls"
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
    99
  bin_mult_Min
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
   100
    "bin_mult (Min,w)     = bin_minus(w)"
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
   101
  bin_mult_BIT
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
   102
    "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6117
diff changeset
   103
				 NCons(bin_mult(v,w),0))"
6046
2c8a8be36c94 converted to use new primrec section
paulson
parents: 5561
diff changeset
   104
9570
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9548
diff changeset
   105
setup NumeralSyntax.setup
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9548
diff changeset
   106
5528
4896b4e4077b new directory for Integers
paulson
parents:
diff changeset
   107
end