New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
authorhuffman
Sun Feb 17 06:49:53 2008 +0100 (2008-02-17)
changeset 260863c243098b64a
parent 26085 4ce22e7a81bd
child 26087 454a5456a4b5
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
NEWS
src/HOL/Groebner_Basis.thy
src/HOL/Import/HOL/HOL4Prob.thy
src/HOL/Import/HOL/HOL4Real.thy
src/HOL/Import/HOL/HOL4Vec.thy
src/HOL/Import/HOL/HOL4Word32.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Word.thy
src/HOL/NatBin.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/Presburger.thy
src/HOL/Real/Float.thy
src/HOL/Tools/ComputeNumeral.thy
src/HOL/Tools/Qelim/cooper_data.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/Word/BinBoolList.thy
src/HOL/Word/BinGeneral.thy
src/HOL/Word/BinOperations.thy
src/HOL/Word/BitSyntax.thy
src/HOL/Word/Examples/WordExamples.thy
src/HOL/Word/Num_Lemmas.thy
src/HOL/Word/WordArith.thy
src/HOL/Word/WordMain.thy
src/HOL/Word/WordShift.thy
src/HOL/hologic.ML
src/HOL/int_arith1.ML
src/HOL/int_factor_simprocs.ML
src/Tools/code/code_target.ML
     1.1 --- a/NEWS	Sat Feb 16 16:52:09 2008 +0100
     1.2 +++ b/NEWS	Sun Feb 17 06:49:53 2008 +0100
     1.3 @@ -35,6 +35,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Int: The representation of numerals has changed.  The infix operator
     1.8 +BIT and the bit datatype with constructors B0 and B1 have disappeared.
     1.9 +INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in place of "x BIT bit.B0"
    1.10 +and "y BIT bit.B1", respectively.  Theorems involving BIT, B0, or B1 have been
    1.11 +renamed with "Bit0" or "Bit1" accordingly.
    1.12 +
    1.13  * Theory Nat: definition of <= and < on natural numbers no longer depend
    1.14  on well-founded relations.  INCOMPATIBILITY.  Definitions le_def and less_def
    1.15  have disappeared.  Consider lemmas not_less [symmetric, where ?'a = nat]
     2.1 --- a/src/HOL/Groebner_Basis.thy	Sat Feb 16 16:52:09 2008 +0100
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Feb 17 06:49:53 2008 +0100
     2.3 @@ -179,7 +179,7 @@
     2.4    if_True add_0 add_Suc add_number_of_left mult_number_of_left
     2.5    numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
     2.6    numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
     2.7 -  iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
     2.8 +  iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
     2.9    iszero_number_of_Pls iszero_0 not_iszero_Numeral1
    2.10  
    2.11  lemmas semiring_norm = comp_arith
     3.1 --- a/src/HOL/Import/HOL/HOL4Prob.thy	Sat Feb 16 16:52:09 2008 +0100
     3.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy	Sun Feb 17 06:49:53 2008 +0100
     3.3 @@ -36,28 +36,24 @@
     3.4   ((op =::nat => nat => bool)
     3.5     ((op div::nat => nat => nat) (0::nat)
     3.6       ((number_of \<Colon> int => nat)
     3.7 -       ((op BIT \<Colon> int => bit => int)
     3.8 -         ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
     3.9 -         (bit.B0::bit))))
    3.10 +       ((Int.Bit0 \<Colon> int => int)
    3.11 +         ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
    3.12     (0::nat))
    3.13   ((op &::bool => bool => bool)
    3.14     ((op =::nat => nat => bool)
    3.15       ((op div::nat => nat => nat) (1::nat)
    3.16         ((number_of \<Colon> int => nat)
    3.17 -         ((op BIT \<Colon> int => bit => int)
    3.18 -           ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.19 -           (bit.B0::bit))))
    3.20 +         ((Int.Bit0 \<Colon> int => int)
    3.21 +           ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
    3.22       (0::nat))
    3.23     ((op =::nat => nat => bool)
    3.24       ((op div::nat => nat => nat)
    3.25         ((number_of \<Colon> int => nat)
    3.26 -         ((op BIT \<Colon> int => bit => int)
    3.27 -           ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.28 -           (bit.B0::bit)))
    3.29 +         ((Int.Bit0 \<Colon> int => int)
    3.30 +           ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    3.31         ((number_of \<Colon> int => nat)
    3.32 -         ((op BIT \<Colon> int => bit => int)
    3.33 -           ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.34 -           (bit.B0::bit))))
    3.35 +         ((Int.Bit0 \<Colon> int => int)
    3.36 +           ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
    3.37       (1::nat)))"
    3.38    by (import prob_extra DIV_TWO_BASIC)
    3.39  
    3.40 @@ -76,19 +72,16 @@
    3.41        ((op div::nat => nat => nat)
    3.42          ((op ^::nat => nat => nat)
    3.43            ((number_of \<Colon> int => nat)
    3.44 -            ((op BIT \<Colon> int => bit => int)
    3.45 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.46 -              (bit.B0::bit)))
    3.47 +            ((Int.Bit0 \<Colon> int => int)
    3.48 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    3.49            ((Suc::nat => nat) n))
    3.50          ((number_of \<Colon> int => nat)
    3.51 -          ((op BIT \<Colon> int => bit => int)
    3.52 -            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.53 -            (bit.B0::bit))))
    3.54 +          ((Int.Bit0 \<Colon> int => int)
    3.55 +            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
    3.56        ((op ^::nat => nat => nat)
    3.57          ((number_of \<Colon> int => nat)
    3.58 -          ((op BIT \<Colon> int => bit => int)
    3.59 -            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.60 -            (bit.B0::bit)))
    3.61 +          ((Int.Bit0 \<Colon> int => int)
    3.62 +            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    3.63          n))"
    3.64    by (import prob_extra EXP_DIV_TWO)
    3.65  
    3.66 @@ -126,22 +119,19 @@
    3.67  lemma HALF_POS: "(op <::real => real => bool) (0::real)
    3.68   ((op /::real => real => real) (1::real)
    3.69     ((number_of \<Colon> int => real)
    3.70 -     ((op BIT \<Colon> int => bit => int)
    3.71 -       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.72 -       (bit.B0::bit))))"
    3.73 +     ((Int.Bit0 \<Colon> int => int)
    3.74 +       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))"
    3.75    by (import prob_extra HALF_POS)
    3.76  
    3.77  lemma HALF_CANCEL: "(op =::real => real => bool)
    3.78   ((op *::real => real => real)
    3.79     ((number_of \<Colon> int => real)
    3.80 -     ((op BIT \<Colon> int => bit => int)
    3.81 -       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.82 -       (bit.B0::bit)))
    3.83 +     ((Int.Bit0 \<Colon> int => int)
    3.84 +       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    3.85     ((op /::real => real => real) (1::real)
    3.86       ((number_of \<Colon> int => real)
    3.87 -       ((op BIT \<Colon> int => bit => int)
    3.88 -         ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    3.89 -         (bit.B0::bit)))))
    3.90 +       ((Int.Bit0 \<Colon> int => int)
    3.91 +         ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))))
    3.92   (1::real)"
    3.93    by (import prob_extra HALF_CANCEL)
    3.94  
    3.95 @@ -151,9 +141,8 @@
    3.96        ((op ^::real => nat => real)
    3.97          ((op /::real => real => real) (1::real)
    3.98            ((number_of \<Colon> int => real)
    3.99 -            ((op BIT \<Colon> int => bit => int)
   3.100 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.101 -              (bit.B0::bit))))
   3.102 +            ((Int.Bit0 \<Colon> int => int)
   3.103 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.104          n))"
   3.105    by (import prob_extra POW_HALF_POS)
   3.106  
   3.107 @@ -166,18 +155,14 @@
   3.108               ((op ^::real => nat => real)
   3.109                 ((op /::real => real => real) (1::real)
   3.110                   ((number_of \<Colon> int => real)
   3.111 -                   ((op BIT \<Colon> int => bit => int)
   3.112 -                     ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   3.113 -                       (bit.B1::bit))
   3.114 -                     (bit.B0::bit))))
   3.115 +                   ((Int.Bit0 \<Colon> int => int)
   3.116 +                     ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.117                 n)
   3.118               ((op ^::real => nat => real)
   3.119                 ((op /::real => real => real) (1::real)
   3.120                   ((number_of \<Colon> int => real)
   3.121 -                   ((op BIT \<Colon> int => bit => int)
   3.122 -                     ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   3.123 -                       (bit.B1::bit))
   3.124 -                     (bit.B0::bit))))
   3.125 +                   ((Int.Bit0 \<Colon> int => int)
   3.126 +                     ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.127                 m))))"
   3.128    by (import prob_extra POW_HALF_MONO)
   3.129  
   3.130 @@ -187,22 +172,18 @@
   3.131        ((op ^::real => nat => real)
   3.132          ((op /::real => real => real) (1::real)
   3.133            ((number_of \<Colon> int => real)
   3.134 -            ((op BIT \<Colon> int => bit => int)
   3.135 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.136 -              (bit.B0::bit))))
   3.137 +            ((Int.Bit0 \<Colon> int => int)
   3.138 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.139          n)
   3.140        ((op *::real => real => real)
   3.141          ((number_of \<Colon> int => real)
   3.142 -          ((op BIT \<Colon> int => bit => int)
   3.143 -            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.144 -            (bit.B0::bit)))
   3.145 +          ((Int.Bit0 \<Colon> int => int)
   3.146 +            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
   3.147          ((op ^::real => nat => real)
   3.148            ((op /::real => real => real) (1::real)
   3.149              ((number_of \<Colon> int => real)
   3.150 -              ((op BIT \<Colon> int => bit => int)
   3.151 -                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   3.152 -                  (bit.B1::bit))
   3.153 -                (bit.B0::bit))))
   3.154 +              ((Int.Bit0 \<Colon> int => int)
   3.155 +                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.156            ((Suc::nat => nat) n))))"
   3.157    by (import prob_extra POW_HALF_TWICE)
   3.158  
   3.159 @@ -228,22 +209,19 @@
   3.160   ((op -::real => real => real) (1::real)
   3.161     ((op /::real => real => real) (1::real)
   3.162       ((number_of \<Colon> int => real)
   3.163 -       ((op BIT \<Colon> int => bit => int)
   3.164 -         ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.165 -         (bit.B0::bit)))))
   3.166 +       ((Int.Bit0 \<Colon> int => int)
   3.167 +         ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))))
   3.168   ((op /::real => real => real) (1::real)
   3.169     ((number_of \<Colon> int => real)
   3.170 -     ((op BIT \<Colon> int => bit => int)
   3.171 -       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.172 -       (bit.B0::bit))))"
   3.173 +     ((Int.Bit0 \<Colon> int => int)
   3.174 +       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))"
   3.175    by (import prob_extra ONE_MINUS_HALF)
   3.176  
   3.177  lemma HALF_LT_1: "(op <::real => real => bool)
   3.178   ((op /::real => real => real) (1::real)
   3.179     ((number_of \<Colon> int => real)
   3.180 -     ((op BIT \<Colon> int => bit => int)
   3.181 -       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.182 -       (bit.B0::bit))))
   3.183 +     ((Int.Bit0 \<Colon> int => int)
   3.184 +       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.185   (1::real)"
   3.186    by (import prob_extra HALF_LT_1)
   3.187  
   3.188 @@ -253,18 +231,15 @@
   3.189        ((op ^::real => nat => real)
   3.190          ((op /::real => real => real) (1::real)
   3.191            ((number_of \<Colon> int => real)
   3.192 -            ((op BIT \<Colon> int => bit => int)
   3.193 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.194 -              (bit.B0::bit))))
   3.195 +            ((Int.Bit0 \<Colon> int => int)
   3.196 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.197          n)
   3.198        ((inverse::real => real)
   3.199          ((real::nat => real)
   3.200            ((op ^::nat => nat => nat)
   3.201              ((number_of \<Colon> int => nat)
   3.202 -              ((op BIT \<Colon> int => bit => int)
   3.203 -                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   3.204 -                  (bit.B1::bit))
   3.205 -                (bit.B0::bit)))
   3.206 +              ((Int.Bit0 \<Colon> int => int)
   3.207 +                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
   3.208              n))))"
   3.209    by (import prob_extra POW_HALF_EXP)
   3.210  
   3.211 @@ -1406,27 +1381,22 @@
   3.212          ((op ^::real => nat => real)
   3.213            ((op /::real => real => real) (1::real)
   3.214              ((number_of \<Colon> int => real)
   3.215 -              ((op BIT \<Colon> int => bit => int)
   3.216 -                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   3.217 -                  (bit.B1::bit))
   3.218 -                (bit.B0::bit))))
   3.219 +              ((Int.Bit0 \<Colon> int => int)
   3.220 +                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.221            ((size::bool list => nat)
   3.222              ((SNOC::bool => bool list => bool list) (True::bool) l)))
   3.223          ((op ^::real => nat => real)
   3.224            ((op /::real => real => real) (1::real)
   3.225              ((number_of \<Colon> int => real)
   3.226 -              ((op BIT \<Colon> int => bit => int)
   3.227 -                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   3.228 -                  (bit.B1::bit))
   3.229 -                (bit.B0::bit))))
   3.230 +              ((Int.Bit0 \<Colon> int => int)
   3.231 +                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.232            ((size::bool list => nat)
   3.233              ((SNOC::bool => bool list => bool list) (False::bool) l))))
   3.234        ((op ^::real => nat => real)
   3.235          ((op /::real => real => real) (1::real)
   3.236            ((number_of \<Colon> int => real)
   3.237 -            ((op BIT \<Colon> int => bit => int)
   3.238 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
   3.239 -              (bit.B0::bit))))
   3.240 +            ((Int.Bit0 \<Colon> int => int)
   3.241 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
   3.242          ((size::bool list => nat) l)))"
   3.243    by (import prob ALG_TWINS_MEASURE)
   3.244  
     4.1 --- a/src/HOL/Import/HOL/HOL4Real.thy	Sat Feb 16 16:52:09 2008 +0100
     4.2 +++ b/src/HOL/Import/HOL/HOL4Real.thy	Sun Feb 17 06:49:53 2008 +0100
     4.3 @@ -526,9 +526,8 @@
     4.4        ((op <=::real => real => bool) (1::real)
     4.5          ((op ^::real => nat => real) x
     4.6            ((number_of \<Colon> int => nat)
     4.7 -            ((op BIT \<Colon> int => bit => int)
     4.8 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
     4.9 -              (bit.B0::bit))))))"
    4.10 +            ((Int.Bit0 \<Colon> int => int)
    4.11 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))))"
    4.12    by (import real REAL_LE1_POW2)
    4.13  
    4.14  lemma REAL_LT1_POW2: "(All::(real => bool) => bool)
    4.15 @@ -538,9 +537,8 @@
    4.16        ((op <::real => real => bool) (1::real)
    4.17          ((op ^::real => nat => real) x
    4.18            ((number_of \<Colon> int => nat)
    4.19 -            ((op BIT \<Colon> int => bit => int)
    4.20 -              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
    4.21 -              (bit.B0::bit))))))"
    4.22 +            ((Int.Bit0 \<Colon> int => int)
    4.23 +              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))))"
    4.24    by (import real REAL_LT1_POW2)
    4.25  
    4.26  lemma POW_POS_LT: "ALL (x::real) n::nat. 0 < x --> 0 < x ^ Suc n"
     5.1 --- a/src/HOL/Import/HOL/HOL4Vec.thy	Sat Feb 16 16:52:09 2008 +0100
     5.2 +++ b/src/HOL/Import/HOL/HOL4Vec.thy	Sun Feb 17 06:49:53 2008 +0100
     5.3 @@ -1283,9 +1283,8 @@
     5.4       (op -->::bool => bool => bool)
     5.5        ((op <::nat => nat => bool) x
     5.6          ((number_of \<Colon> int => nat)
     5.7 -          ((op BIT \<Colon> int => bit => int)
     5.8 -            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
     5.9 -            (bit.B0::bit))))
    5.10 +          ((Int.Bit0 \<Colon> int => int)
    5.11 +            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
    5.12        ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
    5.13          x))"
    5.14    by (import bword_num BV_VB)
    5.15 @@ -1500,10 +1499,9 @@
    5.16                             ((BV::bool => nat) cin))
    5.17                           ((op ^::nat => nat => nat)
    5.18                             ((number_of \<Colon> int => nat)
    5.19 -                             ((op BIT \<Colon> int => bit => int)
    5.20 -                               ((op BIT \<Colon> int => bit => int)
    5.21 -                                 (Int.Pls \<Colon> int) (bit.B1::bit))
    5.22 -                               (bit.B0::bit)))
    5.23 +                             ((Int.Bit0 \<Colon> int => int)
    5.24 +                               ((Int.Bit1 \<Colon> int => int)
    5.25 +                                 (Int.Pls \<Colon> int))))
    5.26                             k)))))))"
    5.27    by (import bword_arith ACARRY_EQ_ADD_DIV)
    5.28  
     6.1 --- a/src/HOL/Import/HOL/HOL4Word32.thy	Sat Feb 16 16:52:09 2008 +0100
     6.2 +++ b/src/HOL/Import/HOL/HOL4Word32.thy	Sun Feb 17 06:49:53 2008 +0100
     6.3 @@ -117,9 +117,8 @@
     6.4       (op <::nat => nat => bool) (0::nat)
     6.5        ((op ^::nat => nat => nat)
     6.6          ((number_of \<Colon> int => nat)
     6.7 -          ((op BIT \<Colon> int => bit => int)
     6.8 -            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
     6.9 -            (bit.B0::bit)))
    6.10 +          ((Int.Bit0 \<Colon> int => int)
    6.11 +            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.12          n))"
    6.13    by (import bits ZERO_LT_TWOEXP)
    6.14  
    6.15 @@ -137,17 +136,13 @@
    6.16             ((op <::nat => nat => bool)
    6.17               ((op ^::nat => nat => nat)
    6.18                 ((number_of \<Colon> int => nat)
    6.19 -                 ((op BIT \<Colon> int => bit => int)
    6.20 -                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.21 -                     (bit.B1::bit))
    6.22 -                   (bit.B0::bit)))
    6.23 +                 ((Int.Bit0 \<Colon> int => int)
    6.24 +                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.25                 a)
    6.26               ((op ^::nat => nat => nat)
    6.27                 ((number_of \<Colon> int => nat)
    6.28 -                 ((op BIT \<Colon> int => bit => int)
    6.29 -                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.30 -                     (bit.B1::bit))
    6.31 -                   (bit.B0::bit)))
    6.32 +                 ((Int.Bit0 \<Colon> int => int)
    6.33 +                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.34                 b))))"
    6.35    by (import bits TWOEXP_MONO)
    6.36  
    6.37 @@ -159,17 +154,13 @@
    6.38             ((op <=::nat => nat => bool)
    6.39               ((op ^::nat => nat => nat)
    6.40                 ((number_of \<Colon> int => nat)
    6.41 -                 ((op BIT \<Colon> int => bit => int)
    6.42 -                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.43 -                     (bit.B1::bit))
    6.44 -                   (bit.B0::bit)))
    6.45 +                 ((Int.Bit0 \<Colon> int => int)
    6.46 +                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.47                 a)
    6.48               ((op ^::nat => nat => nat)
    6.49                 ((number_of \<Colon> int => nat)
    6.50 -                 ((op BIT \<Colon> int => bit => int)
    6.51 -                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.52 -                     (bit.B1::bit))
    6.53 -                   (bit.B0::bit)))
    6.54 +                 ((Int.Bit0 \<Colon> int => int)
    6.55 +                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.56                 b))))"
    6.57    by (import bits TWOEXP_MONO2)
    6.58  
    6.59 @@ -180,17 +171,13 @@
    6.60            (op <=::nat => nat => bool)
    6.61             ((op ^::nat => nat => nat)
    6.62               ((number_of \<Colon> int => nat)
    6.63 -               ((op BIT \<Colon> int => bit => int)
    6.64 -                 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.65 -                   (bit.B1::bit))
    6.66 -                 (bit.B0::bit)))
    6.67 +               ((Int.Bit0 \<Colon> int => int)
    6.68 +                 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.69               ((op -::nat => nat => nat) a b))
    6.70             ((op ^::nat => nat => nat)
    6.71               ((number_of \<Colon> int => nat)
    6.72 -               ((op BIT \<Colon> int => bit => int)
    6.73 -                 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.74 -                   (bit.B1::bit))
    6.75 -                 (bit.B0::bit)))
    6.76 +               ((Int.Bit0 \<Colon> int => int)
    6.77 +                 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.78               a)))"
    6.79    by (import bits EXP_SUB_LESS_EQ)
    6.80  
    6.81 @@ -349,25 +336,19 @@
    6.82                   (op =::nat => nat => bool)
    6.83                    ((op ^::nat => nat => nat)
    6.84                      ((number_of \<Colon> int => nat)
    6.85 -                      ((op BIT \<Colon> int => bit => int)
    6.86 -                        ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.87 -                          (bit.B1::bit))
    6.88 -                        (bit.B0::bit)))
    6.89 +                      ((Int.Bit0 \<Colon> int => int)
    6.90 +                        ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    6.91                      b)
    6.92                    ((op *::nat => nat => nat)
    6.93                      ((op ^::nat => nat => nat)
    6.94                        ((number_of \<Colon> int => nat)
    6.95 -                        ((op BIT \<Colon> int => bit => int)
    6.96 -                          ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
    6.97 -                            (bit.B1::bit))
    6.98 -                          (bit.B0::bit)))
    6.99 +                        ((Int.Bit0 \<Colon> int => int)
   6.100 +                          ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
   6.101                        ((op +::nat => nat => nat) x (1::nat)))
   6.102                      ((op ^::nat => nat => nat)
   6.103                        ((number_of \<Colon> int => nat)
   6.104 -                        ((op BIT \<Colon> int => bit => int)
   6.105 -                          ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
   6.106 -                            (bit.B1::bit))
   6.107 -                          (bit.B0::bit)))
   6.108 +                        ((Int.Bit0 \<Colon> int => int)
   6.109 +                          ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
   6.110                        a))))))"
   6.111    by (import bits LESS_EXP_MULT2)
   6.112  
     7.1 --- a/src/HOL/Int.thy	Sat Feb 16 16:52:09 2008 +0100
     7.2 +++ b/src/HOL/Int.thy	Sun Feb 17 06:49:53 2008 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     7.5  
     7.6  theory Int
     7.7 -imports Equiv_Relations Datatype Nat Wellfounded_Relations
     7.8 +imports Equiv_Relations Nat Wellfounded_Relations
     7.9  uses
    7.10    ("Tools/numeral.ML")
    7.11    ("Tools/numeral_syntax.ML")
    7.12 @@ -583,13 +583,6 @@
    7.13    Springer LNCS 488 (240-251), 1991.
    7.14  *}
    7.15  
    7.16 -datatype bit = B0 | B1
    7.17 -
    7.18 -text{*
    7.19 -  Type @{typ bit} avoids the use of type @{typ bool}, which would make
    7.20 -  all of the rewrite rules higher-order.
    7.21 -*}
    7.22 -
    7.23  definition
    7.24    Pls :: int where
    7.25    [code func del]: "Pls = 0"
    7.26 @@ -599,8 +592,12 @@
    7.27    [code func del]: "Min = - 1"
    7.28  
    7.29  definition
    7.30 -  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
    7.31 -  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
    7.32 +  Bit0 :: "int \<Rightarrow> int" where
    7.33 +  [code func del]: "Bit0 k = k + k"
    7.34 +
    7.35 +definition
    7.36 +  Bit1 :: "int \<Rightarrow> int" where
    7.37 +  [code func del]: "Bit1 k = 1 + k + k"
    7.38  
    7.39  class number = type + -- {* for numeric types: nat, int, real, \dots *}
    7.40    fixes number_of :: "int \<Rightarrow> 'a"
    7.41 @@ -617,7 +614,7 @@
    7.42    "Numeral0 \<equiv> number_of Pls"
    7.43  
    7.44  abbreviation
    7.45 -  "Numeral1 \<equiv> number_of (Pls BIT B1)"
    7.46 +  "Numeral1 \<equiv> number_of (Bit1 Pls)"
    7.47  
    7.48  lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
    7.49    -- {* Unfold all @{text let}s involving constants *}
    7.50 @@ -640,80 +637,80 @@
    7.51    -- {* unfolding @{text minx} and @{text max} on numerals *}
    7.52  
    7.53  lemmas numeral_simps = 
    7.54 -  succ_def pred_def Pls_def Min_def Bit_def
    7.55 +  succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
    7.56  
    7.57  text {* Removal of leading zeroes *}
    7.58  
    7.59 -lemma Pls_0_eq [simp, code post]:
    7.60 -  "Pls BIT B0 = Pls"
    7.61 +lemma Bit0_Pls [simp, code post]:
    7.62 +  "Bit0 Pls = Pls"
    7.63    unfolding numeral_simps by simp
    7.64  
    7.65 -lemma Min_1_eq [simp, code post]:
    7.66 -  "Min BIT B1 = Min"
    7.67 +lemma Bit1_Min [simp, code post]:
    7.68 +  "Bit1 Min = Min"
    7.69    unfolding numeral_simps by simp
    7.70  
    7.71  lemmas normalize_bin_simps =
    7.72 -  Pls_0_eq Min_1_eq
    7.73 +  Bit0_Pls Bit1_Min
    7.74  
    7.75  
    7.76  subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
    7.77  
    7.78  lemma succ_Pls [simp]:
    7.79 -  "succ Pls = Pls BIT B1"
    7.80 +  "succ Pls = Bit1 Pls"
    7.81    unfolding numeral_simps by simp
    7.82  
    7.83  lemma succ_Min [simp]:
    7.84    "succ Min = Pls"
    7.85    unfolding numeral_simps by simp
    7.86  
    7.87 -lemma succ_1 [simp]:
    7.88 -  "succ (k BIT B1) = succ k BIT B0"
    7.89 +lemma succ_Bit0 [simp]:
    7.90 +  "succ (Bit0 k) = Bit1 k"
    7.91    unfolding numeral_simps by simp
    7.92  
    7.93 -lemma succ_0 [simp]:
    7.94 -  "succ (k BIT B0) = k BIT B1"
    7.95 +lemma succ_Bit1 [simp]:
    7.96 +  "succ (Bit1 k) = Bit0 (succ k)"
    7.97    unfolding numeral_simps by simp
    7.98  
    7.99  lemmas succ_bin_simps =
   7.100 -  succ_Pls succ_Min succ_1 succ_0
   7.101 +  succ_Pls succ_Min succ_Bit0 succ_Bit1
   7.102  
   7.103  lemma pred_Pls [simp]:
   7.104    "pred Pls = Min"
   7.105    unfolding numeral_simps by simp
   7.106  
   7.107  lemma pred_Min [simp]:
   7.108 -  "pred Min = Min BIT B0"
   7.109 -  unfolding numeral_simps by simp
   7.110 -
   7.111 -lemma pred_1 [simp]:
   7.112 -  "pred (k BIT B1) = k BIT B0"
   7.113 +  "pred Min = Bit0 Min"
   7.114    unfolding numeral_simps by simp
   7.115  
   7.116 -lemma pred_0 [simp]:
   7.117 -  "pred (k BIT B0) = pred k BIT B1"
   7.118 +lemma pred_Bit0 [simp]:
   7.119 +  "pred (Bit0 k) = Bit1 (pred k)"
   7.120    unfolding numeral_simps by simp 
   7.121  
   7.122 +lemma pred_Bit1 [simp]:
   7.123 +  "pred (Bit1 k) = Bit0 k"
   7.124 +  unfolding numeral_simps by simp
   7.125 +
   7.126  lemmas pred_bin_simps =
   7.127 -  pred_Pls pred_Min pred_1 pred_0
   7.128 +  pred_Pls pred_Min pred_Bit0 pred_Bit1
   7.129  
   7.130  lemma minus_Pls [simp]:
   7.131    "- Pls = Pls"
   7.132    unfolding numeral_simps by simp 
   7.133  
   7.134  lemma minus_Min [simp]:
   7.135 -  "- Min = Pls BIT B1"
   7.136 +  "- Min = Bit1 Pls"
   7.137    unfolding numeral_simps by simp 
   7.138  
   7.139 -lemma minus_1 [simp]:
   7.140 -  "- (k BIT B1) = pred (- k) BIT B1"
   7.141 +lemma minus_Bit0 [simp]:
   7.142 +  "- (Bit0 k) = Bit0 (- k)"
   7.143    unfolding numeral_simps by simp 
   7.144  
   7.145 -lemma minus_0 [simp]:
   7.146 -  "- (k BIT B0) = (- k) BIT B0"
   7.147 -  unfolding numeral_simps by simp 
   7.148 +lemma minus_Bit1 [simp]:
   7.149 +  "- (Bit1 k) = Bit1 (pred (- k))"
   7.150 +  unfolding numeral_simps by simp
   7.151  
   7.152  lemmas minus_bin_simps =
   7.153 -  minus_Pls minus_Min minus_1 minus_0
   7.154 +  minus_Pls minus_Min minus_Bit0 minus_Bit1
   7.155  
   7.156  
   7.157  subsection {*
   7.158 @@ -729,29 +726,33 @@
   7.159    "Min + k = pred k"
   7.160    unfolding numeral_simps by simp
   7.161  
   7.162 -lemma add_BIT_11 [simp]:
   7.163 -  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
   7.164 +lemma add_Bit0_Bit0 [simp]:
   7.165 +  "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
   7.166 +  unfolding numeral_simps by simp_all 
   7.167 +
   7.168 +lemma add_Bit0_Bit1 [simp]:
   7.169 +  "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
   7.170 +  unfolding numeral_simps by simp_all 
   7.171 +
   7.172 +lemma add_Bit1_Bit0 [simp]:
   7.173 +  "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
   7.174    unfolding numeral_simps by simp
   7.175  
   7.176 -lemma add_BIT_10 [simp]:
   7.177 -  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
   7.178 +lemma add_Bit1_Bit1 [simp]:
   7.179 +  "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
   7.180    unfolding numeral_simps by simp
   7.181  
   7.182 -lemma add_BIT_0 [simp]:
   7.183 -  "(k BIT B0) + (l BIT b) = (k + l) BIT b"
   7.184 -  unfolding numeral_simps by simp 
   7.185 -
   7.186  lemma add_Pls_right [simp]:
   7.187    "k + Pls = k"
   7.188    unfolding numeral_simps by simp 
   7.189  
   7.190  lemma add_Min_right [simp]:
   7.191    "k + Min = pred k"
   7.192 -  unfolding numeral_simps by simp 
   7.193 +  unfolding numeral_simps by simp
   7.194  
   7.195  lemmas add_bin_simps =
   7.196 -  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
   7.197 -  add_Pls_right add_Min_right
   7.198 +  add_Pls add_Min add_Pls_right add_Min_right
   7.199 +  add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
   7.200  
   7.201  lemma mult_Pls [simp]:
   7.202    "Pls * w = Pls"
   7.203 @@ -761,16 +762,16 @@
   7.204    "Min * k = - k"
   7.205    unfolding numeral_simps by simp
   7.206  
   7.207 -lemma mult_num1 [simp]:
   7.208 -  "(k BIT B1) * l = ((k * l) BIT B0) + l"
   7.209 -  unfolding numeral_simps int_distrib by simp 
   7.210 +lemma mult_Bit0 [simp]:
   7.211 +  "(Bit0 k) * l = Bit0 (k * l)"
   7.212 +  unfolding numeral_simps int_distrib by simp
   7.213  
   7.214 -lemma mult_num0 [simp]:
   7.215 -  "(k BIT B0) * l = (k * l) BIT B0"
   7.216 +lemma mult_Bit1 [simp]:
   7.217 +  "(Bit1 k) * l = (Bit0 (k * l)) + l"
   7.218    unfolding numeral_simps int_distrib by simp 
   7.219  
   7.220  lemmas mult_bin_simps =
   7.221 -  mult_Pls mult_Min mult_num1 mult_num0 
   7.222 +  mult_Pls mult_Min mult_Bit0 mult_Bit1
   7.223  
   7.224  
   7.225  subsection {* Converting Numerals to Rings: @{term number_of} *}
   7.226 @@ -820,8 +821,8 @@
   7.227    But it doesn't seem to give a measurable speed-up.
   7.228  *}
   7.229  
   7.230 -lemma double_number_of_BIT:
   7.231 -  "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
   7.232 +lemma double_number_of_Bit0:
   7.233 +  "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
   7.234    unfolding number_of_eq numeral_simps left_distrib by simp
   7.235  
   7.236  text {*
   7.237 @@ -877,10 +878,13 @@
   7.238    "number_of Min = (- 1::'a::number_ring)"
   7.239    unfolding number_of_eq numeral_simps by simp
   7.240  
   7.241 -lemma number_of_BIT:
   7.242 -  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
   7.243 -    + (number_of w) + (number_of w)"
   7.244 -  unfolding number_of_eq numeral_simps by (simp split: bit.split)
   7.245 +lemma number_of_Bit0:
   7.246 +  "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
   7.247 +  unfolding number_of_eq numeral_simps by simp
   7.248 +
   7.249 +lemma number_of_Bit1:
   7.250 +  "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
   7.251 +  unfolding number_of_eq numeral_simps by simp
   7.252  
   7.253  
   7.254  subsection {* Equality of Binary Numbers *}
   7.255 @@ -979,9 +983,9 @@
   7.256    qed
   7.257  qed
   7.258  
   7.259 -lemma iszero_number_of_BIT:
   7.260 -  "iszero (number_of (w BIT x)::'a) = 
   7.261 -   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
   7.262 +lemma iszero_number_of_Bit0:
   7.263 +  "iszero (number_of (Bit0 w)::'a) = 
   7.264 +   iszero (number_of w::'a::{ring_char_0,number_ring})"
   7.265  proof -
   7.266    have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
   7.267    proof -
   7.268 @@ -990,27 +994,24 @@
   7.269      then have "w + w = 0" by (simp only: of_int_eq_iff)
   7.270      then show "w = 0" by (simp only: double_eq_0_iff)
   7.271    qed
   7.272 -  moreover have "1 + of_int w + of_int w \<noteq> (0::'a)"
   7.273 +  thus ?thesis
   7.274 +    by (auto simp add: iszero_def number_of_eq numeral_simps)
   7.275 +qed
   7.276 +
   7.277 +lemma iszero_number_of_Bit1:
   7.278 +  "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
   7.279 +proof -
   7.280 +  have "1 + of_int w + of_int w \<noteq> (0::'a)"
   7.281    proof
   7.282      assume eq: "1 + of_int w + of_int w = (0::'a)"
   7.283      hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 
   7.284      hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
   7.285      with odd_nonzero show False by blast
   7.286    qed
   7.287 -  ultimately show ?thesis
   7.288 -    by (auto simp add: iszero_def number_of_eq numeral_simps 
   7.289 -     split: bit.split)
   7.290 +  thus ?thesis
   7.291 +    by (auto simp add: iszero_def number_of_eq numeral_simps)
   7.292  qed
   7.293  
   7.294 -lemma iszero_number_of_0:
   7.295 -  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 
   7.296 -  iszero (number_of w :: 'a)"
   7.297 -  by (simp only: iszero_number_of_BIT simp_thms)
   7.298 -
   7.299 -lemma iszero_number_of_1:
   7.300 -  "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
   7.301 -  by (simp add: iszero_number_of_BIT) 
   7.302 -
   7.303  
   7.304  subsection {* The Less-Than Relation *}
   7.305  
   7.306 @@ -1056,16 +1057,20 @@
   7.307      add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
   7.308  qed
   7.309  
   7.310 -lemma neg_number_of_BIT:
   7.311 -  "neg (number_of (w BIT x)::'a) = 
   7.312 +lemma neg_number_of_Bit0:
   7.313 +  "neg (number_of (Bit0 w)::'a) = 
   7.314 +  neg (number_of w :: 'a::{ordered_idom,number_ring})"
   7.315 +by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
   7.316 +
   7.317 +lemma neg_number_of_Bit1:
   7.318 +  "neg (number_of (Bit1 w)::'a) = 
   7.319    neg (number_of w :: 'a::{ordered_idom,number_ring})"
   7.320  proof -
   7.321    have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
   7.322      by simp
   7.323    also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
   7.324    finally show ?thesis
   7.325 -  by ( simp add: neg_def number_of_eq numeral_simps double_less_0_iff
   7.326 -    split: bit.split)
   7.327 +  by (simp add: neg_def number_of_eq numeral_simps)
   7.328  qed
   7.329  
   7.330  
   7.331 @@ -1112,7 +1117,6 @@
   7.332  *}
   7.333  
   7.334  lemmas arith_simps = 
   7.335 -  bit.distinct
   7.336    normalize_bin_simps pred_bin_simps succ_bin_simps
   7.337    add_bin_simps minus_bin_simps mult_bin_simps
   7.338    abs_zero abs_one arith_extra_simps
   7.339 @@ -1121,10 +1125,10 @@
   7.340  
   7.341  lemmas rel_simps [simp] = 
   7.342    eq_number_of_eq iszero_0 nonzero_number_of_Min
   7.343 -  iszero_number_of_0 iszero_number_of_1
   7.344 +  iszero_number_of_Bit0 iszero_number_of_Bit1
   7.345    less_number_of_eq_neg
   7.346    not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
   7.347 -  neg_number_of_Min neg_number_of_BIT
   7.348 +  neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
   7.349    le_number_of_eq
   7.350  (* iszero_number_of_Pls would never be used
   7.351     because its lhs simplifies to "iszero 0" *)
   7.352 @@ -1795,7 +1799,7 @@
   7.353  
   7.354  instance int :: eq ..
   7.355  
   7.356 -code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
   7.357 +code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
   7.358  
   7.359  definition
   7.360    int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
   7.361 @@ -1883,7 +1887,7 @@
   7.362  
   7.363  (*setup continues in theory Presburger*)
   7.364  
   7.365 -hide (open) const Pls Min B0 B1 succ pred
   7.366 +hide (open) const Pls Min Bit0 Bit1 succ pred
   7.367  
   7.368  
   7.369  subsection {* Legacy theorems *}
     8.1 --- a/src/HOL/IntDiv.thy	Sat Feb 16 16:52:09 2008 +0100
     8.2 +++ b/src/HOL/IntDiv.thy	Sun Feb 17 06:49:53 2008 +0100
     8.3 @@ -1062,14 +1062,18 @@
     8.4  lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
     8.5  by auto
     8.6  
     8.7 -lemma zdiv_number_of_BIT[simp]:
     8.8 -     "number_of (v BIT b) div number_of (w BIT bit.B0) =  
     8.9 -          (if b=bit.B0 | (0::int) \<le> number_of w                    
    8.10 +lemma zdiv_number_of_Bit0 [simp]:
    8.11 +     "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
    8.12 +          number_of v div (number_of w :: int)"
    8.13 +by (simp only: number_of_eq numeral_simps) simp
    8.14 +
    8.15 +lemma zdiv_number_of_Bit1 [simp]:
    8.16 +     "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =  
    8.17 +          (if (0::int) \<le> number_of w                    
    8.18             then number_of v div (number_of w)     
    8.19             else (number_of v + (1::int)) div (number_of w))"
    8.20  apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
    8.21 -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
    8.22 -            split: bit.split)
    8.23 +apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
    8.24  done
    8.25  
    8.26  
    8.27 @@ -1087,7 +1091,7 @@
    8.28  apply (subst zmod_zadd1_eq)
    8.29  apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
    8.30  apply (rule mod_pos_pos_trivial)
    8.31 -apply (auto simp add: mod_pos_pos_trivial left_distrib)
    8.32 +apply (auto simp add: mod_pos_pos_trivial ring_distribs)
    8.33  apply (subgoal_tac "0 \<le> b mod a", arith, simp)
    8.34  done
    8.35  
    8.36 @@ -1102,14 +1106,20 @@
    8.37  apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
    8.38  done
    8.39  
    8.40 -lemma zmod_number_of_BIT [simp]:
    8.41 -     "number_of (v BIT b) mod number_of (w BIT bit.B0) =  
    8.42 -      (case b of
    8.43 -          bit.B0 => 2 * (number_of v mod number_of w)
    8.44 -        | bit.B1 => if (0::int) \<le> number_of w  
    8.45 +lemma zmod_number_of_Bit0 [simp]:
    8.46 +     "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =  
    8.47 +      (2::int) * (number_of v mod number_of w)"
    8.48 +apply (simp only: number_of_eq numeral_simps) 
    8.49 +apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    8.50 +                 not_0_le_lemma neg_zmod_mult_2 add_ac)
    8.51 +done
    8.52 +
    8.53 +lemma zmod_number_of_Bit1 [simp]:
    8.54 +     "number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) =  
    8.55 +      (if (0::int) \<le> number_of w  
    8.56                  then 2 * (number_of v mod number_of w) + 1     
    8.57                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
    8.58 -apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 
    8.59 +apply (simp only: number_of_eq numeral_simps) 
    8.60  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    8.61                   not_0_le_lemma neg_zmod_mult_2 add_ac)
    8.62  done
     9.1 --- a/src/HOL/Library/Char_nat.thy	Sat Feb 16 16:52:09 2008 +0100
     9.2 +++ b/src/HOL/Library/Char_nat.thy	Sun Feb 17 06:49:53 2008 +0100
     9.3 @@ -76,7 +76,7 @@
     9.4    unfolding nibble_of_nat_def Let_def by auto
     9.5  
     9.6  lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
     9.7 -  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_BIT if_False add_0 add_Suc]
     9.8 +  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
     9.9  
    9.10  lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
    9.11    by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
    10.1 --- a/src/HOL/Library/Code_Index.thy	Sat Feb 16 16:52:09 2008 +0100
    10.2 +++ b/src/HOL/Library/Code_Index.thy	Sun Feb 17 06:49:53 2008 +0100
    10.3 @@ -88,7 +88,7 @@
    10.4  
    10.5  lemma one_index_code [code inline, code func]:
    10.6    "(1\<Colon>index) = Numeral1"
    10.7 -  by (simp add: number_of_index_def Pls_def Bit_def)
    10.8 +  by (simp add: number_of_index_def Pls_def Bit1_def)
    10.9  lemma [code post]: "Numeral1 = (1\<Colon>index)"
   10.10    using one_index_code ..
   10.11  
    11.1 --- a/src/HOL/Library/Code_Integer.thy	Sat Feb 16 16:52:09 2008 +0100
    11.2 +++ b/src/HOL/Library/Code_Integer.thy	Sun Feb 17 06:49:53 2008 +0100
    11.3 @@ -28,16 +28,19 @@
    11.4      true true) ["SML", "OCaml", "Haskell"]
    11.5  *}
    11.6  
    11.7 -code_const "Int.Pls" and "Int.Min" and "Int.Bit"
    11.8 +code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
    11.9    (SML "raise/ Fail/ \"Pls\""
   11.10       and "raise/ Fail/ \"Min\""
   11.11 -     and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
   11.12 +     and "!((_);/ raise/ Fail/ \"Bit0\")"
   11.13 +     and "!((_);/ raise/ Fail/ \"Bit1\")")
   11.14    (OCaml "failwith/ \"Pls\""
   11.15       and "failwith/ \"Min\""
   11.16 -     and "!((_);/ (_);/ failwith/ \"Bit\")")
   11.17 +     and "!((_);/ failwith/ \"Bit0\")"
   11.18 +     and "!((_);/ failwith/ \"Bit1\")")
   11.19    (Haskell "error/ \"Pls\""
   11.20       and "error/ \"Min\""
   11.21 -     and "error/ \"Bit\"")
   11.22 +     and "error/ \"Bit0\""
   11.23 +     and "error/ \"Bit1\"")
   11.24  
   11.25  code_const Int.pred
   11.26    (SML "IntInf.- ((_), 1)")
    12.1 --- a/src/HOL/Library/Word.thy	Sat Feb 16 16:52:09 2008 +0100
    12.2 +++ b/src/HOL/Library/Word.thy	Sun Feb 17 06:49:53 2008 +0100
    12.3 @@ -2265,14 +2265,14 @@
    12.4  primrec
    12.5    fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
    12.6    fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
    12.7 -    fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))"
    12.8 +    fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
    12.9  
   12.10  lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
   12.11 -    fast_bv_to_nat_helper bs (bin BIT bit.B0)"
   12.12 +    fast_bv_to_nat_helper bs (Int.Bit0 bin)"
   12.13    by simp
   12.14  
   12.15  lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
   12.16 -    fast_bv_to_nat_helper bs (bin BIT bit.B1)"
   12.17 +    fast_bv_to_nat_helper bs (Int.Bit1 bin)"
   12.18    by simp
   12.19  
   12.20  lemma fast_bv_to_nat_def:
   12.21 @@ -2301,8 +2301,10 @@
   12.22      | is_const_bit _ = false
   12.23    fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
   12.24      | num_is_usable (Const(@{const_name Int.Min},_)) = false
   12.25 -    | num_is_usable (Const(@{const_name Int.Bit},_) $ w $ b) =
   12.26 -        num_is_usable w andalso is_const_bool b
   12.27 +    | num_is_usable (Const(@{const_name Int.Bit0},_) $ w) =
   12.28 +        num_is_usable w
   12.29 +    | num_is_usable (Const(@{const_name Int.Bit1},_) $ w) =
   12.30 +        num_is_usable w
   12.31      | num_is_usable _ = false
   12.32    fun vec_is_usable (Const("List.list.Nil",_)) = true
   12.33      | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
    13.1 --- a/src/HOL/NatBin.thy	Sat Feb 16 16:52:09 2008 +0100
    13.2 +++ b/src/HOL/NatBin.thy	Sun Feb 17 06:49:53 2008 +0100
    13.3 @@ -524,44 +524,6 @@
    13.4  by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
    13.5  
    13.6  
    13.7 -lemma lemma1: "(m+m = n+n) = (m = (n::int))"
    13.8 -by auto
    13.9 -
   13.10 -lemma lemma2: "m+m ~= (1::int) + (n + n)"
   13.11 -apply auto
   13.12 -apply (drule_tac f = "%x. x mod 2" in arg_cong)
   13.13 -apply (simp add: zmod_zadd1_eq)
   13.14 -done
   13.15 -
   13.16 -lemma eq_number_of_BIT_BIT:
   13.17 -     "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
   13.18 -      (x=y & (((number_of v) ::int) = number_of w))"
   13.19 -apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
   13.20 -               OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0_left
   13.21 -            split add: bit.split)
   13.22 -apply simp
   13.23 -done
   13.24 -
   13.25 -lemma eq_number_of_BIT_Pls:
   13.26 -     "((number_of (v BIT x) ::int) = Numeral0) =  
   13.27 -      (x=bit.B0 & (((number_of v) ::int) = Numeral0))"
   13.28 -apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
   13.29 -            split add: bit.split cong: imp_cong)
   13.30 -apply (rule_tac x = "number_of v" in spec, safe)
   13.31 -apply (simp_all (no_asm_use))
   13.32 -apply (drule_tac f = "%x. x mod 2" in arg_cong)
   13.33 -apply (simp add: zmod_zadd1_eq)
   13.34 -done
   13.35 -
   13.36 -lemma eq_number_of_BIT_Min:
   13.37 -     "((number_of (v BIT x) ::int) = number_of Int.Min) =  
   13.38 -      (x=bit.B1 & (((number_of v) ::int) = number_of Int.Min))"
   13.39 -apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
   13.40 -            split add: bit.split cong: imp_cong)
   13.41 -apply (rule_tac x = "number_of v" in spec, auto)
   13.42 -apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
   13.43 -done
   13.44 -
   13.45  lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   13.46  by auto
   13.47  
   13.48 @@ -632,8 +594,8 @@
   13.49  
   13.50  lemma power_number_of_even:
   13.51    fixes z :: "'a::{number_ring,recpower}"
   13.52 -  shows "z ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
   13.53 -unfolding Let_def nat_number_of_def number_of_BIT bit.cases
   13.54 +  shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   13.55 +unfolding Let_def nat_number_of_def number_of_Bit0
   13.56  apply (rule_tac x = "number_of w" in spec, clarify)
   13.57  apply (case_tac " (0::int) <= x")
   13.58  apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
   13.59 @@ -641,9 +603,9 @@
   13.60  
   13.61  lemma power_number_of_odd:
   13.62    fixes z :: "'a::{number_ring,recpower}"
   13.63 -  shows "z ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w
   13.64 +  shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   13.65       then (let w = z ^ (number_of w) in z * w * w) else 1)"
   13.66 -unfolding Let_def nat_number_of_def number_of_BIT bit.cases
   13.67 +unfolding Let_def nat_number_of_def number_of_Bit1
   13.68  apply (rule_tac x = "number_of w" in spec, auto)
   13.69  apply (simp only: nat_add_distrib nat_mult_distrib)
   13.70  apply simp
   13.71 @@ -673,7 +635,7 @@
   13.72        lessD = lessD, neqE = neqE,
   13.73        simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
   13.74          @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
   13.75 -        @{thm neg_number_of_BIT}]})
   13.76 +        @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
   13.77  *}
   13.78  
   13.79  declaration {* K nat_bin_arith_setup *}
   13.80 @@ -689,33 +651,32 @@
   13.81    apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   13.82    done
   13.83  
   13.84 -lemma nat_number_of_BIT_1:
   13.85 -  "number_of (w BIT bit.B1) =
   13.86 +lemma nat_number_of_Bit0:
   13.87 +    "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   13.88 +  apply (simp only: nat_number_of_def Let_def)
   13.89 +  apply (cases "neg (number_of w :: int)")
   13.90 +   apply (simp add: neg_nat neg_number_of_Bit0)
   13.91 +  apply (rule int_int_eq [THEN iffD1])
   13.92 +  apply (simp only: not_neg_nat neg_number_of_Bit0 int_Suc zadd_int [symmetric] simp_thms)
   13.93 +  apply (simp only: number_of_Bit0 zadd_assoc)
   13.94 +  apply simp
   13.95 +  done
   13.96 +
   13.97 +lemma nat_number_of_Bit1:
   13.98 +  "number_of (Int.Bit1 w) =
   13.99      (if neg (number_of w :: int) then 0
  13.100       else let n = number_of w in Suc (n + n))"
  13.101    apply (simp only: nat_number_of_def Let_def split: split_if)
  13.102    apply (intro conjI impI)
  13.103 -   apply (simp add: neg_nat neg_number_of_BIT)
  13.104 +   apply (simp add: neg_nat neg_number_of_Bit1)
  13.105    apply (rule int_int_eq [THEN iffD1])
  13.106 -  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
  13.107 -  apply (simp only: number_of_BIT zadd_assoc split: bit.split)
  13.108 -  apply simp
  13.109 -  done
  13.110 -
  13.111 -lemma nat_number_of_BIT_0:
  13.112 -    "number_of (w BIT bit.B0) = (let n::nat = number_of w in n + n)"
  13.113 -  apply (simp only: nat_number_of_def Let_def)
  13.114 -  apply (cases "neg (number_of w :: int)")
  13.115 -   apply (simp add: neg_nat neg_number_of_BIT)
  13.116 -  apply (rule int_int_eq [THEN iffD1])
  13.117 -  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
  13.118 -  apply (simp only: number_of_BIT zadd_assoc)
  13.119 -  apply simp
  13.120 +  apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms)
  13.121 +  apply (simp only: number_of_Bit1 zadd_assoc)
  13.122    done
  13.123  
  13.124  lemmas nat_number =
  13.125    nat_number_of_Pls nat_number_of_Min
  13.126 -  nat_number_of_BIT_1 nat_number_of_BIT_0
  13.127 +  nat_number_of_Bit0 nat_number_of_Bit1
  13.128  
  13.129  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
  13.130    by (simp add: Let_def)
    14.1 --- a/src/HOL/NumberTheory/Euler.thy	Sat Feb 16 16:52:09 2008 +0100
    14.2 +++ b/src/HOL/NumberTheory/Euler.thy	Sun Feb 17 06:49:53 2008 +0100
    14.3 @@ -77,7 +77,7 @@
    14.4          by (auto simp add: zcong_zmult_prop2)
    14.5      qed
    14.6    then have "[j^2 = a] (mod p)"
    14.7 -    by (metis  number_of_is_id power2_eq_square succ_1 succ_Pls)
    14.8 +    by (metis  number_of_is_id power2_eq_square succ_bin_simps)
    14.9    with prems show False
   14.10      by (simp add: QuadRes_def)
   14.11  qed
   14.12 @@ -288,7 +288,7 @@
   14.13    apply (auto simp add: zpower_zpower) 
   14.14    apply (rule zcong_trans)
   14.15    apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
   14.16 -  apply (metis Little_Fermat even_div_2_prop2 mult_num0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)
   14.17 +  apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)
   14.18    done
   14.19  
   14.20  
    15.1 --- a/src/HOL/Presburger.thy	Sat Feb 16 16:52:09 2008 +0100
    15.2 +++ b/src/HOL/Presburger.thy	Sun Feb 17 06:49:53 2008 +0100
    15.3 @@ -394,7 +394,8 @@
    15.4    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
    15.5    by (case_tac "y \<le> x", simp_all add: zdiff_int)
    15.6  
    15.7 -lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
    15.8 +lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
    15.9 +by simp
   15.10  lemma number_of2: "(0::int) <= Numeral0" by simp
   15.11  lemma Suc_plus1: "Suc n = n + 1" by simp
   15.12  
   15.13 @@ -503,12 +504,12 @@
   15.14    unfolding Pls_def Int.Min_def by presburger
   15.15  
   15.16  lemma eq_Pls_Bit0:
   15.17 -  "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
   15.18 -  unfolding Pls_def Bit_def bit.cases by presburger
   15.19 +  "Int.Pls = Int.Bit0 k \<longleftrightarrow> Int.Pls = k"
   15.20 +  unfolding Pls_def Bit0_def by presburger
   15.21  
   15.22  lemma eq_Pls_Bit1:
   15.23 -  "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
   15.24 -  unfolding Pls_def Bit_def bit.cases by presburger
   15.25 +  "Int.Pls = Int.Bit1 k \<longleftrightarrow> False"
   15.26 +  unfolding Pls_def Bit1_def by presburger
   15.27  
   15.28  lemma eq_Min_Pls:
   15.29    "Int.Min = Int.Pls \<longleftrightarrow> False"
   15.30 @@ -518,43 +519,44 @@
   15.31    "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
   15.32  
   15.33  lemma eq_Min_Bit0:
   15.34 -  "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
   15.35 -  unfolding Int.Min_def Bit_def bit.cases by presburger
   15.36 +  "Int.Min = Int.Bit0 k \<longleftrightarrow> False"
   15.37 +  unfolding Int.Min_def Bit0_def by presburger
   15.38  
   15.39  lemma eq_Min_Bit1:
   15.40 -  "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
   15.41 -  unfolding Int.Min_def Bit_def bit.cases by presburger
   15.42 +  "Int.Min = Int.Bit1 k \<longleftrightarrow> Int.Min = k"
   15.43 +  unfolding Int.Min_def Bit1_def by presburger
   15.44  
   15.45  lemma eq_Bit0_Pls:
   15.46 -  "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
   15.47 -  unfolding Pls_def Bit_def bit.cases by presburger
   15.48 +  "Int.Bit0 k = Int.Pls \<longleftrightarrow> Int.Pls = k"
   15.49 +  unfolding Pls_def Bit0_def by presburger
   15.50  
   15.51  lemma eq_Bit1_Pls:
   15.52 -  "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
   15.53 -  unfolding Pls_def Bit_def bit.cases  by presburger
   15.54 +  "Int.Bit1 k = Int.Pls \<longleftrightarrow> False"
   15.55 +  unfolding Pls_def Bit1_def by presburger
   15.56  
   15.57  lemma eq_Bit0_Min:
   15.58 -  "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
   15.59 -  unfolding Int.Min_def Bit_def bit.cases  by presburger
   15.60 +  "Int.Bit0 k = Int.Min \<longleftrightarrow> False"
   15.61 +  unfolding Int.Min_def Bit0_def by presburger
   15.62  
   15.63  lemma eq_Bit1_Min:
   15.64 -  "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
   15.65 -  unfolding Int.Min_def Bit_def bit.cases  by presburger
   15.66 +  "Int.Bit1 k = Int.Min \<longleftrightarrow> Int.Min = k"
   15.67 +  unfolding Int.Min_def Bit1_def by presburger
   15.68 +
   15.69 +lemma eq_Bit0_Bit0:
   15.70 +  "Int.Bit0 k1 = Int.Bit0 k2 \<longleftrightarrow> k1 = k2"
   15.71 +  unfolding Bit0_def by presburger
   15.72  
   15.73 -lemma eq_Bit_Bit:
   15.74 -  "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
   15.75 -    v1 = v2 \<and> k1 = k2" 
   15.76 -  unfolding Bit_def
   15.77 -  apply (cases v1)
   15.78 -  apply (cases v2)
   15.79 -  apply auto
   15.80 -  apply presburger
   15.81 -  apply (cases v2)
   15.82 -  apply auto
   15.83 -  apply presburger
   15.84 -  apply (cases v2)
   15.85 -  apply auto
   15.86 -  done
   15.87 +lemma eq_Bit0_Bit1:
   15.88 +  "Int.Bit0 k1 = Int.Bit1 k2 \<longleftrightarrow> False"
   15.89 +  unfolding Bit0_def Bit1_def by presburger
   15.90 +
   15.91 +lemma eq_Bit1_Bit0:
   15.92 +  "Int.Bit1 k1 = Int.Bit0 k2 \<longleftrightarrow> False"
   15.93 +  unfolding Bit0_def Bit1_def by presburger
   15.94 +
   15.95 +lemma eq_Bit1_Bit1:
   15.96 +  "Int.Bit1 k1 = Int.Bit1 k2 \<longleftrightarrow> k1 = k2"
   15.97 +  unfolding Bit1_def by presburger
   15.98  
   15.99  lemma eq_number_of:
  15.100    "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
  15.101 @@ -568,9 +570,13 @@
  15.102    "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
  15.103    unfolding Pls_def Int.Min_def by presburger
  15.104  
  15.105 -lemma less_eq_Pls_Bit:
  15.106 -  "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
  15.107 -  unfolding Pls_def Bit_def by (cases v) auto
  15.108 +lemma less_eq_Pls_Bit0:
  15.109 +  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
  15.110 +  unfolding Pls_def Bit0_def by auto
  15.111 +
  15.112 +lemma less_eq_Pls_Bit1:
  15.113 +  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  15.114 +  unfolding Pls_def Bit1_def by auto
  15.115  
  15.116  lemma less_eq_Min_Pls:
  15.117    "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
  15.118 @@ -580,36 +586,44 @@
  15.119    "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
  15.120  
  15.121  lemma less_eq_Min_Bit0:
  15.122 -  "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
  15.123 -  unfolding Int.Min_def Bit_def by auto
  15.124 +  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  15.125 +  unfolding Int.Min_def Bit0_def by auto
  15.126  
  15.127  lemma less_eq_Min_Bit1:
  15.128 -  "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
  15.129 -  unfolding Int.Min_def Bit_def by auto
  15.130 +  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
  15.131 +  unfolding Int.Min_def Bit1_def by auto
  15.132  
  15.133  lemma less_eq_Bit0_Pls:
  15.134 -  "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
  15.135 -  unfolding Pls_def Bit_def by simp
  15.136 +  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
  15.137 +  unfolding Pls_def Bit0_def by simp
  15.138  
  15.139  lemma less_eq_Bit1_Pls:
  15.140 -  "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
  15.141 -  unfolding Pls_def Bit_def by auto
  15.142 +  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
  15.143 +  unfolding Pls_def Bit1_def by auto
  15.144  
  15.145 -lemma less_eq_Bit_Min:
  15.146 -  "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  15.147 -  unfolding Int.Min_def Bit_def by (cases v) auto
  15.148 +lemma less_eq_Bit0_Min:
  15.149 +  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  15.150 +  unfolding Int.Min_def Bit0_def by auto
  15.151  
  15.152 -lemma less_eq_Bit0_Bit:
  15.153 -  "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
  15.154 -  unfolding Bit_def bit.cases by (cases v) auto
  15.155 +lemma less_eq_Bit1_Min:
  15.156 +  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  15.157 +  unfolding Int.Min_def Bit1_def by auto
  15.158  
  15.159 -lemma less_eq_Bit_Bit1:
  15.160 -  "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
  15.161 -  unfolding Bit_def bit.cases by (cases v) auto
  15.162 +lemma less_eq_Bit0_Bit0:
  15.163 +  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
  15.164 +  unfolding Bit0_def by auto
  15.165 +
  15.166 +lemma less_eq_Bit0_Bit1:
  15.167 +  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  15.168 +  unfolding Bit0_def Bit1_def by auto
  15.169  
  15.170  lemma less_eq_Bit1_Bit0:
  15.171 -  "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
  15.172 -  unfolding Bit_def by (auto split: bit.split)
  15.173 +  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  15.174 +  unfolding Bit0_def Bit1_def by auto
  15.175 +
  15.176 +lemma less_eq_Bit1_Bit1:
  15.177 +  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  15.178 +  unfolding Bit1_def by auto
  15.179  
  15.180  lemma less_eq_number_of:
  15.181    "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  15.182 @@ -624,12 +638,12 @@
  15.183    unfolding Pls_def Int.Min_def  by presburger 
  15.184  
  15.185  lemma less_Pls_Bit0:
  15.186 -  "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
  15.187 -  unfolding Pls_def Bit_def by auto
  15.188 +  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
  15.189 +  unfolding Pls_def Bit0_def by auto
  15.190  
  15.191  lemma less_Pls_Bit1:
  15.192 -  "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
  15.193 -  unfolding Pls_def Bit_def by auto
  15.194 +  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  15.195 +  unfolding Pls_def Bit1_def by auto
  15.196  
  15.197  lemma less_Min_Pls:
  15.198    "Int.Min < Int.Pls \<longleftrightarrow> True"
  15.199 @@ -638,33 +652,45 @@
  15.200  lemma less_Min_Min:
  15.201    "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
  15.202  
  15.203 -lemma less_Min_Bit:
  15.204 -  "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
  15.205 -  unfolding Int.Min_def Bit_def by (auto split: bit.split)
  15.206 +lemma less_Min_Bit0:
  15.207 +  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  15.208 +  unfolding Int.Min_def Bit0_def by auto
  15.209 +
  15.210 +lemma less_Min_Bit1:
  15.211 +  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
  15.212 +  unfolding Int.Min_def Bit1_def by auto
  15.213  
  15.214 -lemma less_Bit_Pls:
  15.215 -  "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
  15.216 -  unfolding Pls_def Bit_def by (auto split: bit.split)
  15.217 +lemma less_Bit0_Pls:
  15.218 +  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  15.219 +  unfolding Pls_def Bit0_def by auto
  15.220 +
  15.221 +lemma less_Bit1_Pls:
  15.222 +  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  15.223 +  unfolding Pls_def Bit1_def by auto
  15.224  
  15.225  lemma less_Bit0_Min:
  15.226 -  "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
  15.227 -  unfolding Int.Min_def Bit_def by auto
  15.228 +  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
  15.229 +  unfolding Int.Min_def Bit0_def by auto
  15.230  
  15.231  lemma less_Bit1_Min:
  15.232 -  "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
  15.233 -  unfolding Int.Min_def Bit_def by auto
  15.234 +  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
  15.235 +  unfolding Int.Min_def Bit1_def by auto
  15.236  
  15.237 -lemma less_Bit_Bit0:
  15.238 -  "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
  15.239 -  unfolding Bit_def by (auto split: bit.split)
  15.240 -
  15.241 -lemma less_Bit1_Bit:
  15.242 -  "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
  15.243 -  unfolding Bit_def by (auto split: bit.split)
  15.244 +lemma less_Bit0_Bit0:
  15.245 +  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  15.246 +  unfolding Bit0_def by auto
  15.247  
  15.248  lemma less_Bit0_Bit1:
  15.249 -  "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
  15.250 -  unfolding Bit_def bit.cases  by arith
  15.251 +  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  15.252 +  unfolding Bit0_def Bit1_def by auto
  15.253 +
  15.254 +lemma less_Bit1_Bit0:
  15.255 +  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  15.256 +  unfolding Bit0_def Bit1_def by auto
  15.257 +
  15.258 +lemma less_Bit1_Bit1:
  15.259 +  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
  15.260 +  unfolding Bit1_def by auto
  15.261  
  15.262  lemma less_number_of:
  15.263    "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  15.264 @@ -689,17 +715,22 @@
  15.265  lemmas eq_numeral_code [code func] =
  15.266    eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
  15.267    eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
  15.268 -  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
  15.269 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min
  15.270 +  eq_Bit0_Bit0 eq_Bit0_Bit1 eq_Bit1_Bit0 eq_Bit1_Bit1
  15.271    eq_number_of
  15.272  
  15.273 -lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
  15.274 +lemmas less_eq_numeral_code [code func] =
  15.275 +  less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit0 less_eq_Pls_Bit1
  15.276    less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
  15.277 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
  15.278 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit0_Min less_eq_Bit1_Min
  15.279 +  less_eq_Bit0_Bit0 less_eq_Bit0_Bit1 less_eq_Bit1_Bit0 less_eq_Bit1_Bit1
  15.280    less_eq_number_of
  15.281  
  15.282 -lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
  15.283 -  less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
  15.284 -  less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
  15.285 +lemmas less_numeral_code [code func] =
  15.286 +  less_Pls_Pls less_Pls_Min less_Pls_Bit0 less_Pls_Bit1
  15.287 +  less_Min_Pls less_Min_Min less_Min_Bit0 less_Min_Bit1
  15.288 +  less_Bit0_Pls less_Bit1_Pls less_Bit0_Min less_Bit1_Min
  15.289 +  less_Bit0_Bit0 less_Bit0_Bit1 less_Bit1_Bit0 less_Bit1_Bit1
  15.290    less_number_of
  15.291  
  15.292  context ring_1
    16.1 --- a/src/HOL/Real/Float.thy	Sat Feb 16 16:52:09 2008 +0100
    16.2 +++ b/src/HOL/Real/Float.thy	Sun Feb 17 06:49:53 2008 +0100
    16.3 @@ -518,10 +518,10 @@
    16.4  lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
    16.5    by simp
    16.6  
    16.7 -lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
    16.8 +lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)"
    16.9    by simp
   16.10  
   16.11 -lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
   16.12 +lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)"
   16.13    by simp
   16.14  
   16.15  lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   16.16 @@ -533,7 +533,10 @@
   16.17  lemma int_neg_number_of_Min: "neg (-1::int)"
   16.18    by simp
   16.19  
   16.20 -lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   16.21 +lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)"
   16.22 +  by simp
   16.23 +
   16.24 +lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)"
   16.25    by simp
   16.26  
   16.27  lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   16.28 @@ -541,9 +544,9 @@
   16.29  
   16.30  lemmas intarithrel =
   16.31    int_eq_number_of_eq
   16.32 -  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
   16.33 -  lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   16.34 -  int_neg_number_of_BIT int_le_number_of_eq
   16.35 +  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0
   16.36 +  lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   16.37 +  int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq
   16.38  
   16.39  lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   16.40    by simp
    17.1 --- a/src/HOL/Tools/ComputeNumeral.thy	Sat Feb 16 16:52:09 2008 +0100
    17.2 +++ b/src/HOL/Tools/ComputeNumeral.thy	Sun Feb 17 06:49:53 2008 +0100
    17.3 @@ -8,15 +8,15 @@
    17.4  (* neg for bit strings *)
    17.5  lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
    17.6  lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
    17.7 -lemma neg3: "neg (x BIT Int.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
    17.8 -lemma neg4: "neg (x BIT Int.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto  
    17.9 +lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto
   17.10 +lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto  
   17.11  lemmas bitneg = neg1 neg2 neg3 neg4
   17.12  
   17.13  (* iszero for bit strings *)
   17.14  lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
   17.15  lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
   17.16 -lemma iszero3: "iszero (x BIT Int.B0) = iszero x" apply (subst Int.Bit_def) apply (subst iszero_def)+ by auto
   17.17 -lemma iszero4: "iszero (x BIT Int.B1) = False" apply (subst Int.Bit_def) apply (subst iszero_def)+  apply simp by arith
   17.18 +lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto
   17.19 +lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+  apply simp by arith
   17.20  lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
   17.21  
   17.22  (* lezero for bit strings *)
   17.23 @@ -24,66 +24,66 @@
   17.24    "lezero x == (x \<le> 0)"
   17.25  lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
   17.26  lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
   17.27 -lemma lezero3: "lezero (x BIT Int.B0) = lezero x" unfolding Int.Bit_def lezero_def by auto
   17.28 -lemma lezero4: "lezero (x BIT Int.B1) = neg x" unfolding Int.Bit_def lezero_def neg_def by auto
   17.29 +lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
   17.30 +lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto
   17.31  lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
   17.32  
   17.33  (* equality for bit strings *)
   17.34 -lemma biteq1: "(Int.Pls = Int.Pls) = True" by auto
   17.35 -lemma biteq2: "(Int.Min = Int.Min) = True" by auto
   17.36 -lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def by auto
   17.37 -lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def by auto
   17.38 -lemma biteq5: "(x BIT Int.B0 = y BIT Int.B0) = (x = y)" unfolding Bit_def by auto
   17.39 -lemma biteq6: "(x BIT Int.B1 = y BIT Int.B1) = (x = y)" unfolding Bit_def by auto
   17.40 -lemma biteq7: "(x BIT Int.B0 = y BIT Int.B1) = False" unfolding Bit_def by (simp, arith) 
   17.41 -lemma biteq8: "(x BIT Int.B1 = y BIT Int.B0) = False" unfolding Bit_def by (simp, arith)
   17.42 -lemma biteq9: "(Int.Pls = x BIT Int.B0) = (Int.Pls = x)" unfolding Bit_def Pls_def by auto
   17.43 -lemma biteq10: "(Int.Pls = x BIT Int.B1) = False" unfolding Bit_def Pls_def by (simp, arith) 
   17.44 -lemma biteq11: "(Int.Min = x BIT Int.B0) = False" unfolding Bit_def Min_def by (simp, arith)
   17.45 -lemma biteq12: "(Int.Min = x BIT Int.B1) = (Int.Min = x)" unfolding Bit_def Min_def by auto
   17.46 -lemma biteq13: "(x BIT Int.B0 = Int.Pls) = (x = Int.Pls)" unfolding Bit_def Pls_def by auto
   17.47 -lemma biteq14: "(x BIT Int.B1 = Int.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
   17.48 -lemma biteq15: "(x BIT Int.B0 = Int.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
   17.49 -lemma biteq16: "(x BIT Int.B1 = Int.Min) = (x = Int.Min)" unfolding Bit_def Min_def by (simp, arith)
   17.50 +lemma biteq1: "(Int.Pls = Int.Pls) = True" by (rule eq_Pls_Pls)
   17.51 +lemma biteq2: "(Int.Min = Int.Min) = True" by (rule eq_Min_Min)
   17.52 +lemma biteq3: "(Int.Pls = Int.Min) = False" by (rule eq_Pls_Min)
   17.53 +lemma biteq4: "(Int.Min = Int.Pls) = False" by (rule eq_Min_Pls)
   17.54 +lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" by (rule eq_Bit0_Bit0)
   17.55 +lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" by (rule eq_Bit1_Bit1)
   17.56 +lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" by (rule eq_Bit0_Bit1)
   17.57 +lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" by (rule eq_Bit1_Bit0)
   17.58 +lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" by (rule eq_Pls_Bit0)
   17.59 +lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" by (rule eq_Pls_Bit1)
   17.60 +lemma biteq11: "(Int.Min = Int.Bit0 x) = False" by (rule eq_Min_Bit0)
   17.61 +lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" by (rule eq_Min_Bit1)
   17.62 +lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" by (subst eq_Bit0_Pls) auto
   17.63 +lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" by (rule eq_Bit1_Pls)
   17.64 +lemma biteq15: "(Int.Bit0 x = Int.Min) = False" by (rule eq_Bit0_Min)
   17.65 +lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" by (subst eq_Bit1_Min) auto
   17.66  lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
   17.67  
   17.68  (* x < y for bit strings *)
   17.69 -lemma bitless1: "(Int.Pls < Int.Min) = False" unfolding Pls_def Min_def by auto
   17.70 -lemma bitless2: "(Int.Pls < Int.Pls) = False" by auto
   17.71 -lemma bitless3: "(Int.Min < Int.Pls) = True" unfolding Pls_def Min_def by auto
   17.72 -lemma bitless4: "(Int.Min < Int.Min) = False" unfolding Pls_def Min_def by auto
   17.73 -lemma bitless5: "(x BIT Int.B0 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
   17.74 -lemma bitless6: "(x BIT Int.B1 < y BIT Int.B1) = (x < y)" unfolding Bit_def by auto
   17.75 -lemma bitless7: "(x BIT Int.B0 < y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
   17.76 -lemma bitless8: "(x BIT Int.B1 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
   17.77 -lemma bitless9: "(Int.Pls < x BIT Int.B0) = (Int.Pls < x)" unfolding Bit_def Pls_def by auto
   17.78 -lemma bitless10: "(Int.Pls < x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
   17.79 -lemma bitless11: "(Int.Min < x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
   17.80 -lemma bitless12: "(Int.Min < x BIT Int.B1) = (Int.Min < x)" unfolding Bit_def Min_def by auto
   17.81 -lemma bitless13: "(x BIT Int.B0 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
   17.82 -lemma bitless14: "(x BIT Int.B1 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
   17.83 -lemma bitless15: "(x BIT Int.B0 < Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
   17.84 -lemma bitless16: "(x BIT Int.B1 < Int.Min) = (x < Int.Min)" unfolding Bit_def Min_def by auto
   17.85 +lemma bitless1: "(Int.Pls < Int.Min) = False" by (rule less_Pls_Min)
   17.86 +lemma bitless2: "(Int.Pls < Int.Pls) = False" by (rule less_Pls_Pls)
   17.87 +lemma bitless3: "(Int.Min < Int.Pls) = True" by (rule less_Min_Pls)
   17.88 +lemma bitless4: "(Int.Min < Int.Min) = False" by (rule less_Min_Min)
   17.89 +lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (rule less_Bit0_Bit0)
   17.90 +lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (rule less_Bit1_Bit1)
   17.91 +lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \<le> y)" by (rule less_Bit0_Bit1)
   17.92 +lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (rule less_Bit1_Bit0)
   17.93 +lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (rule less_Pls_Bit0)
   17.94 +lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_Pls_Bit1)
   17.95 +lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
   17.96 +lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (rule less_Min_Bit1)
   17.97 +lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit0_Pls)
   17.98 +lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit1_Pls)
   17.99 +lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
  17.100 +lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (rule less_Bit1_Min)
  17.101  lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8 
  17.102                   bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
  17.103  
  17.104  (* x \<le> y for bit strings *)
  17.105 -lemma bitle1: "(Int.Pls \<le> Int.Min) = False" unfolding Pls_def Min_def by auto
  17.106 -lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by auto
  17.107 -lemma bitle3: "(Int.Min \<le> Int.Pls) = True" unfolding Pls_def Min_def by auto
  17.108 -lemma bitle4: "(Int.Min \<le> Int.Min) = True" unfolding Pls_def Min_def by auto
  17.109 -lemma bitle5: "(x BIT Int.B0 \<le> y BIT Int.B0) = (x \<le> y)" unfolding Bit_def by auto
  17.110 -lemma bitle6: "(x BIT Int.B1 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
  17.111 -lemma bitle7: "(x BIT Int.B0 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
  17.112 -lemma bitle8: "(x BIT Int.B1 \<le> y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
  17.113 -lemma bitle9: "(Int.Pls \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
  17.114 -lemma bitle10: "(Int.Pls \<le> x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
  17.115 -lemma bitle11: "(Int.Min \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
  17.116 -lemma bitle12: "(Int.Min \<le> x BIT Int.B1) = (Int.Min \<le> x)" unfolding Bit_def Min_def by auto
  17.117 -lemma bitle13: "(x BIT Int.B0 \<le> Int.Pls) = (x \<le> Int.Pls)" unfolding Bit_def Pls_def by auto
  17.118 -lemma bitle14: "(x BIT Int.B1 \<le> Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
  17.119 -lemma bitle15: "(x BIT Int.B0 \<le> Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
  17.120 -lemma bitle16: "(x BIT Int.B1 \<le> Int.Min) = (x \<le> Int.Min)" unfolding Bit_def Min_def by auto
  17.121 +lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (rule less_eq_Pls_Min)
  17.122 +lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (rule less_eq_Pls_Pls)
  17.123 +lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (rule less_eq_Min_Pls)
  17.124 +lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (rule less_eq_Min_Min)
  17.125 +lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit0)
  17.126 +lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit1_Bit1)
  17.127 +lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit1)
  17.128 +lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (rule less_eq_Bit1_Bit0)
  17.129 +lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit0)
  17.130 +lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit1)
  17.131 +lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
  17.132 +lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (rule less_eq_Min_Bit1)
  17.133 +lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (rule less_eq_Bit0_Pls)
  17.134 +lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (rule less_eq_Bit1_Pls)
  17.135 +lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
  17.136 +lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> Int.Min)" by (rule less_eq_Bit1_Min)
  17.137  lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8 
  17.138                   bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
  17.139  
  17.140 @@ -97,15 +97,15 @@
  17.141  lemmas bituminus = minus_bin_simps
  17.142  
  17.143  (* addition for bit strings *)
  17.144 -lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Int.B0"] add_BIT_0[where b="Int.B1"]
  17.145 +lemmas bitadd = add_bin_simps
  17.146  
  17.147  (* multiplication for bit strings *) 
  17.148  lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
  17.149  lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
  17.150 -lemma multb0x: "(x BIT Int.B0) * y = (x * y) BIT Int.B0" unfolding Bit_def by simp
  17.151 -lemma multxb0: "x * (y BIT Int.B0) = (x * y) BIT Int.B0" unfolding Bit_def by simp
  17.152 -lemma multb1: "(x BIT Int.B1) * (y BIT Int.B1) = (((x * y) BIT Int.B0) + x + y) BIT Int.B1"
  17.153 -  unfolding Bit_def by (simp add: ring_simps)
  17.154 +lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
  17.155 +lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
  17.156 +lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"
  17.157 +  unfolding Bit0_def Bit1_def by (simp add: ring_simps)
  17.158  lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
  17.159  
  17.160  lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
  17.161 @@ -121,7 +121,7 @@
  17.162  
  17.163  (* Normalization of nat literals *)
  17.164  lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
  17.165 -lemma natnorm1: "(1 :: nat) = number_of (Int.Pls BIT Int.B1)"  by auto 
  17.166 +lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)"  by auto 
  17.167  lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
  17.168  
  17.169  (* Suc *)
  17.170 @@ -228,12 +228,12 @@
  17.171    apply (unfold Min_def even_def)
  17.172    by simp
  17.173  
  17.174 -lemma even_B0: "even (x BIT Int.B0) = True"
  17.175 -  apply (unfold Bit_def)
  17.176 +lemma even_B0: "even (Int.Bit0 x) = True"
  17.177 +  apply (unfold Bit0_def)
  17.178    by simp
  17.179  
  17.180 -lemma even_B1: "even (x BIT Int.B1) = False"
  17.181 -  apply (unfold Bit_def)
  17.182 +lemma even_B1: "even (Int.Bit1 x) = False"
  17.183 +  apply (unfold Bit1_def)
  17.184    by simp
  17.185  
  17.186  lemma even_number_of: "even ((number_of w)::int) = even w"
    18.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Feb 16 16:52:09 2008 +0100
    18.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sun Feb 17 06:49:53 2008 +0100
    18.3 @@ -24,7 +24,7 @@
    18.4     @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    18.5     @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    18.6     @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    18.7 -   @{term "Int.Bit"},
    18.8 +   @{term "Int.Bit0"}, @{term "Int.Bit1"},
    18.9     @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
   18.10     @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
   18.11     @{term "op < :: int => _"}, @{term "op < :: nat => _"},
   18.12 @@ -38,8 +38,8 @@
   18.13     @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
   18.14     @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
   18.15     @{term "nat"}, @{term "int"},
   18.16 -   @{term "Int.bit.B0"},@{term "Int.bit.B1"}, 
   18.17 -   @{term "Int.Bit"}, @{term "Int.Pls"}, @{term "Int.Min"},
   18.18 +   @{term "Int.Bit0"}, @{term "Int.Bit1"},
   18.19 +   @{term "Int.Pls"}, @{term "Int.Min"},
   18.20     @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
   18.21     @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
   18.22     @{term "True"}, @{term "False"}];
    19.1 --- a/src/HOL/Tools/numeral.ML	Sat Feb 16 16:52:09 2008 +0100
    19.2 +++ b/src/HOL/Tools/numeral.ML	Sun Feb 17 06:49:53 2008 +0100
    19.3 @@ -17,15 +17,15 @@
    19.4  
    19.5  (* numeral *)
    19.6  
    19.7 -fun mk_cbit 0 = @{cterm "Int.bit.B0"}
    19.8 -  | mk_cbit 1 = @{cterm "Int.bit.B1"}
    19.9 +fun mk_cbit 0 = @{cterm "Int.Bit0"}
   19.10 +  | mk_cbit 1 = @{cterm "Int.Bit1"}
   19.11    | mk_cbit _ = raise CTERM ("mk_cbit", []);
   19.12  
   19.13  fun mk_cnumeral 0 = @{cterm "Int.Pls"}
   19.14    | mk_cnumeral ~1 = @{cterm "Int.Min"}
   19.15    | mk_cnumeral i =
   19.16        let val (q, r) = Integer.div_mod i 2 in
   19.17 -        Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r)
   19.18 +        Thm.capply (mk_cbit r) (mk_cnumeral q)
   19.19        end;
   19.20  
   19.21  
   19.22 @@ -57,8 +57,7 @@
   19.23  
   19.24  fun add_code number_of negative unbounded target =
   19.25    CodeTarget.add_pretty_numeral target negative unbounded number_of
   19.26 -  @{const_name Int.B0} @{const_name Int.B1}
   19.27    @{const_name Int.Pls} @{const_name Int.Min}
   19.28 -  @{const_name Int.Bit};
   19.29 +  @{const_name Int.Bit0} @{const_name Int.Bit1};
   19.30  
   19.31  end;
    20.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sat Feb 16 16:52:09 2008 +0100
    20.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sun Feb 17 06:49:53 2008 +0100
    20.3 @@ -20,7 +20,7 @@
    20.4  fun mk_bin num =
    20.5    let
    20.6      val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
    20.7 -    fun bit b bs = Syntax.const @{const_name Int.Bit} $ bs $ HOLogic.mk_bit b;
    20.8 +    fun bit b bs = HOLogic.mk_bit b $ bs;
    20.9      fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
   20.10        | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
   20.11        | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
   20.12 @@ -39,15 +39,10 @@
   20.13  
   20.14  local
   20.15  
   20.16 -fun dest_bit (Const (@{const_syntax Int.bit.B0}, _)) = 0
   20.17 -  | dest_bit (Const (@{const_syntax Int.bit.B1}, _)) = 1
   20.18 -  | dest_bit (Const ("bit.B0", _)) = 0
   20.19 -  | dest_bit (Const ("bit.B1", _)) = 1
   20.20 -  | dest_bit _ = raise Match;
   20.21 -
   20.22  fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
   20.23    | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
   20.24 -  | dest_bin (Const (@{const_syntax "Int.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
   20.25 +  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
   20.26 +  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
   20.27    | dest_bin _ = raise Match;
   20.28  
   20.29  fun leading _ [] = 0
    21.1 --- a/src/HOL/Word/BinBoolList.thy	Sat Feb 16 16:52:09 2008 +0100
    21.2 +++ b/src/HOL/Word/BinBoolList.thy	Sun Feb 17 06:49:53 2008 +0100
    21.3 @@ -75,24 +75,30 @@
    21.4    "(butlast ^ n) bl = take (length bl - n) bl"
    21.5    by (induct n) (auto simp: butlast_take)
    21.6  
    21.7 -lemma bin_to_bl_aux_Pls_minus_simp:
    21.8 +lemma bin_to_bl_aux_Pls_minus_simp [simp]:
    21.9    "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
   21.10      bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
   21.11    by (cases n) auto
   21.12  
   21.13 -lemma bin_to_bl_aux_Min_minus_simp:
   21.14 +lemma bin_to_bl_aux_Min_minus_simp [simp]:
   21.15    "0 < n ==> bin_to_bl_aux n Int.Min bl = 
   21.16      bin_to_bl_aux (n - 1) Int.Min (True # bl)"
   21.17    by (cases n) auto
   21.18  
   21.19 -lemma bin_to_bl_aux_Bit_minus_simp:
   21.20 +lemma bin_to_bl_aux_Bit_minus_simp [simp]:
   21.21    "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
   21.22      bin_to_bl_aux (n - 1) w ((b = bit.B1) # bl)"
   21.23    by (cases n) auto
   21.24  
   21.25 -declare bin_to_bl_aux_Pls_minus_simp [simp]
   21.26 -  bin_to_bl_aux_Min_minus_simp [simp]
   21.27 -  bin_to_bl_aux_Bit_minus_simp [simp]
   21.28 +lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
   21.29 +  "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl = 
   21.30 +    bin_to_bl_aux (n - 1) w (False # bl)"
   21.31 +  by (cases n) auto
   21.32 +
   21.33 +lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
   21.34 +  "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl = 
   21.35 +    bin_to_bl_aux (n - 1) w (True # bl)"
   21.36 +  by (cases n) auto
   21.37  
   21.38  (** link between bin and bool list **)
   21.39  
   21.40 @@ -308,7 +314,7 @@
   21.41    apply clarsimp
   21.42    apply safe
   21.43     apply (erule allE, erule xtr8 [rotated],
   21.44 -          simp add: Bit_def ring_simps cong add : number_of_False_cong)+
   21.45 +          simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   21.46    done
   21.47  
   21.48  lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
   21.49 @@ -326,7 +332,7 @@
   21.50    apply clarsimp
   21.51    apply safe
   21.52     apply (erule allE, erule less_eq_less.order_trans [rotated],
   21.53 -          simp add: Bit_def ring_simps cong add : number_of_False_cong)+
   21.54 +          simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   21.55    done
   21.56  
   21.57  lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
   21.58 @@ -370,13 +376,13 @@
   21.59     apply (case_tac "m - size list")
   21.60      apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
   21.61     apply simp
   21.62 -   apply (rule_tac f = "%nat. bl_to_bin_aux (bintrunc nat w BIT bit.B1) list" 
   21.63 +   apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit1 (bintrunc nat w)) list" 
   21.64                     in arg_cong) 
   21.65     apply simp
   21.66    apply (case_tac "m - size list")
   21.67     apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
   21.68    apply simp
   21.69 -  apply (rule_tac f = "%nat. bl_to_bin_aux (bintrunc nat w BIT bit.B0) list" 
   21.70 +  apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit0 (bintrunc nat w)) list" 
   21.71                    in arg_cong) 
   21.72    apply simp
   21.73    done
    22.1 --- a/src/HOL/Word/BinGeneral.thy	Sat Feb 16 16:52:09 2008 +0100
    22.2 +++ b/src/HOL/Word/BinGeneral.thy	Sun Feb 17 06:49:53 2008 +0100
    22.3 @@ -49,21 +49,37 @@
    22.4     apply (auto intro: bin_rec'.simps [THEN trans])
    22.5    done
    22.6  
    22.7 -lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]
    22.8 -lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
    22.9 +lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
   22.10 +  unfolding bin_rec_def by simp
   22.11 +
   22.12 +lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
   22.13 +  unfolding bin_rec_def by simp
   22.14 +
   22.15 +lemma bin_rec_Bit0:
   22.16 +  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
   22.17 +    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
   22.18 +  apply (unfold bin_rec_def)
   22.19 +  apply (rule bin_rec'.simps [THEN trans])
   22.20 +  apply (fold bin_rec_def)
   22.21 +  apply (simp add: eq_Bit0_Pls eq_Bit0_Min bin_rec_Pls)
   22.22 +  done
   22.23 +
   22.24 +lemma bin_rec_Bit1:
   22.25 +  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
   22.26 +    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
   22.27 +  apply (unfold bin_rec_def)
   22.28 +  apply (rule bin_rec'.simps [THEN trans])
   22.29 +  apply (fold bin_rec_def)
   22.30 +  apply (simp add: eq_Bit1_Pls eq_Bit1_Min bin_rec_Min)
   22.31 +  done
   22.32  
   22.33  lemma bin_rec_Bit:
   22.34    "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
   22.35      f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
   22.36 -  apply clarify
   22.37 -  apply (unfold bin_rec_def)
   22.38 -  apply (rule bin_rec'.simps [THEN trans])
   22.39 -  apply auto
   22.40 -       apply (unfold Pls_def Min_def Bit_def)
   22.41 -       apply (cases b, auto)+
   22.42 -  done
   22.43 +  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
   22.44  
   22.45  lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
   22.46 +  bin_rec_Bit0 bin_rec_Bit1
   22.47  
   22.48  subsection {* Destructors for binary integers *}
   22.49  
   22.50 @@ -92,18 +108,24 @@
   22.51    "bin_rest Int.Pls = Int.Pls"
   22.52    "bin_rest Int.Min = Int.Min"
   22.53    "bin_rest (w BIT b) = w"
   22.54 +  "bin_rest (Int.Bit0 w) = w"
   22.55 +  "bin_rest (Int.Bit1 w) = w"
   22.56    unfolding bin_rest_def by auto
   22.57  
   22.58  lemma bin_last_simps [simp]: 
   22.59    "bin_last Int.Pls = bit.B0"
   22.60    "bin_last Int.Min = bit.B1"
   22.61    "bin_last (w BIT b) = b"
   22.62 +  "bin_last (Int.Bit0 w) = bit.B0"
   22.63 +  "bin_last (Int.Bit1 w) = bit.B1"
   22.64    unfolding bin_last_def by auto
   22.65 -    
   22.66 +
   22.67  lemma bin_sign_simps [simp]:
   22.68    "bin_sign Int.Pls = Int.Pls"
   22.69    "bin_sign Int.Min = Int.Min"
   22.70    "bin_sign (w BIT b) = bin_sign w"
   22.71 +  "bin_sign (Int.Bit0 w) = bin_sign w"
   22.72 +  "bin_sign (Int.Bit1 w) = bin_sign w"
   22.73    unfolding bin_sign_def by (auto simp: bin_rec_simps)
   22.74  
   22.75  lemma bin_r_l_extras [simp]:
   22.76 @@ -142,6 +164,12 @@
   22.77  lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   22.78    unfolding bin_rest_div [symmetric] by auto
   22.79  
   22.80 +lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
   22.81 +  using Bit_div2 [where b=bit.B0] by simp
   22.82 +
   22.83 +lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
   22.84 +  using Bit_div2 [where b=bit.B1] by simp
   22.85 +
   22.86  lemma bin_nth_lem [rule_format]:
   22.87    "ALL y. bin_nth x = bin_nth y --> x = y"
   22.88    apply (induct x rule: bin_induct)
   22.89 @@ -191,11 +219,20 @@
   22.90  lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
   22.91    by (cases n) auto
   22.92  
   22.93 +lemma bin_nth_minus_Bit0 [simp]:
   22.94 +  "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
   22.95 +  using bin_nth_minus [where b=bit.B0] by simp
   22.96 +
   22.97 +lemma bin_nth_minus_Bit1 [simp]:
   22.98 +  "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
   22.99 +  using bin_nth_minus [where b=bit.B1] by simp
  22.100 +
  22.101  lemmas bin_nth_0 = bin_nth.simps(1)
  22.102  lemmas bin_nth_Suc = bin_nth.simps(2)
  22.103  
  22.104  lemmas bin_nth_simps = 
  22.105    bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
  22.106 +  bin_nth_minus_Bit0 bin_nth_minus_Bit1
  22.107  
  22.108  lemma bin_sign_rest [simp]: 
  22.109    "bin_sign (bin_rest w) = (bin_sign w)"
  22.110 @@ -277,6 +314,14 @@
  22.111    "bin_nth (w BIT b) n = (n = 0 & b = bit.B1 | (EX m. n = Suc m & bin_nth w m))"
  22.112    by (cases n) auto
  22.113  
  22.114 +lemma bin_nth_Bit0:
  22.115 +  "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
  22.116 +  using bin_nth_Bit [where b=bit.B0] by simp
  22.117 +
  22.118 +lemma bin_nth_Bit1:
  22.119 +  "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
  22.120 +  using bin_nth_Bit [where b=bit.B1] by simp
  22.121 +
  22.122  lemma bintrunc_bintrunc_l:
  22.123    "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
  22.124    by (rule bin_eqI) (auto simp add : nth_bintr)
  22.125 @@ -312,7 +357,16 @@
  22.126  lemmas bintrunc_BIT  [simp] = 
  22.127    bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
  22.128  
  22.129 +lemma bintrunc_Bit0 [simp]:
  22.130 +  "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
  22.131 +  using bintrunc_BIT [where b=bit.B0] by simp
  22.132 +
  22.133 +lemma bintrunc_Bit1 [simp]:
  22.134 +  "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
  22.135 +  using bintrunc_BIT [where b=bit.B1] by simp
  22.136 +
  22.137  lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
  22.138 +  bintrunc_Bit0 bintrunc_Bit1
  22.139  
  22.140  lemmas sbintrunc_Suc_Pls = 
  22.141    sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
  22.142 @@ -323,7 +377,16 @@
  22.143  lemmas sbintrunc_Suc_BIT [simp] = 
  22.144    sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
  22.145  
  22.146 +lemma sbintrunc_Suc_Bit0 [simp]:
  22.147 +  "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
  22.148 +  using sbintrunc_Suc_BIT [where b=bit.B0] by simp
  22.149 +
  22.150 +lemma sbintrunc_Suc_Bit1 [simp]:
  22.151 +  "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
  22.152 +  using sbintrunc_Suc_BIT [where b=bit.B1] by simp
  22.153 +
  22.154  lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
  22.155 +  sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
  22.156  
  22.157  lemmas sbintrunc_Pls = 
  22.158    sbintrunc.Z [where bin="Int.Pls", 
  22.159 @@ -341,8 +404,15 @@
  22.160    sbintrunc.Z [where bin="w BIT bit.B1", 
  22.161                 simplified bin_last_simps bin_rest_simps bit.simps, standard]
  22.162  
  22.163 +lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
  22.164 +  using sbintrunc_0_BIT_B0 by simp
  22.165 +
  22.166 +lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
  22.167 +  using sbintrunc_0_BIT_B1 by simp
  22.168 +
  22.169  lemmas sbintrunc_0_simps =
  22.170    sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
  22.171 +  sbintrunc_0_Bit0 sbintrunc_0_Bit1
  22.172  
  22.173  lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
  22.174  lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
  22.175 @@ -374,7 +444,7 @@
  22.176  lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
  22.177  lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
  22.178  
  22.179 -lemmas bmsts = bintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
  22.180 +lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
  22.181  lemmas bintrunc_Pls_minus_I = bmsts(1)
  22.182  lemmas bintrunc_Min_minus_I = bmsts(2)
  22.183  lemmas bintrunc_BIT_minus_I = bmsts(3)
  22.184 @@ -394,10 +464,10 @@
  22.185  lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
  22.186  
  22.187  lemmas sbintrunc_Suc_Is = 
  22.188 -  sbintrunc_Sucs [THEN thobini1 [THEN [2] trans], standard]
  22.189 +  sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard]
  22.190  
  22.191  lemmas sbintrunc_Suc_minus_Is = 
  22.192 -  sbintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
  22.193 +  sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
  22.194  
  22.195  lemma sbintrunc_Suc_lem:
  22.196    "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
  22.197 @@ -573,11 +643,11 @@
  22.198  
  22.199  lemma sign_Pls_ge_0: 
  22.200    "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
  22.201 -  by (induct bin rule: bin_induct) auto
  22.202 +  by (induct bin rule: numeral_induct) auto
  22.203  
  22.204  lemma sign_Min_lt_0: 
  22.205    "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
  22.206 -  by (induct bin rule: bin_induct) auto
  22.207 +  by (induct bin rule: numeral_induct) auto
  22.208  
  22.209  lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
  22.210  
  22.211 @@ -725,5 +795,4 @@
  22.212  
  22.213  lemmas s2n_ths = n2s_ths [symmetric]
  22.214  
  22.215 -
  22.216  end
    23.1 --- a/src/HOL/Word/BinOperations.thy	Sat Feb 16 16:52:09 2008 +0100
    23.2 +++ b/src/HOL/Word/BinOperations.thy	Sun Feb 17 06:49:53 2008 +0100
    23.3 @@ -44,7 +44,9 @@
    23.4    "NOT Int.Pls = Int.Min"
    23.5    "NOT Int.Min = Int.Pls"
    23.6    "NOT (w BIT b) = (NOT w) BIT (NOT b)"
    23.7 -  by (unfold int_not_def) (auto intro: bin_rec_simps)
    23.8 +  "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
    23.9 +  "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
   23.10 +  unfolding int_not_def by (simp_all add: bin_rec_simps)
   23.11  
   23.12  lemma int_xor_Pls [simp]: 
   23.13    "Int.Pls XOR x = x"
   23.14 @@ -65,6 +67,13 @@
   23.15    apply (simp add: int_not_simps [symmetric])
   23.16    done
   23.17  
   23.18 +lemma int_xor_Bits2 [simp]: 
   23.19 +  "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
   23.20 +  "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
   23.21 +  "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
   23.22 +  "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
   23.23 +  unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
   23.24 +
   23.25  lemma int_xor_x_simps':
   23.26    "w XOR (Int.Pls BIT bit.B0) = w"
   23.27    "w XOR (Int.Min BIT bit.B1) = NOT w"
   23.28 @@ -74,7 +83,10 @@
   23.29     apply clarsimp+
   23.30    done
   23.31  
   23.32 -lemmas int_xor_extra_simps [simp] = int_xor_x_simps' [simplified arith_simps]
   23.33 +lemma int_xor_extra_simps [simp]:
   23.34 +  "w XOR Int.Pls = w"
   23.35 +  "w XOR Int.Min = NOT w"
   23.36 +  using int_xor_x_simps' by simp_all
   23.37  
   23.38  lemma int_or_Pls [simp]: 
   23.39    "Int.Pls OR x = x"
   23.40 @@ -88,6 +100,13 @@
   23.41    "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
   23.42    unfolding int_or_def by (simp add: bin_rec_simps)
   23.43  
   23.44 +lemma int_or_Bits2 [simp]: 
   23.45 +  "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
   23.46 +  "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   23.47 +  "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
   23.48 +  "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   23.49 +  unfolding BIT_simps [symmetric] int_or_Bits by simp_all
   23.50 +
   23.51  lemma int_or_x_simps': 
   23.52    "w OR (Int.Pls BIT bit.B0) = w"
   23.53    "w OR (Int.Min BIT bit.B1) = Int.Min"
   23.54 @@ -97,8 +116,10 @@
   23.55     apply clarsimp+
   23.56    done
   23.57  
   23.58 -lemmas int_or_extra_simps [simp] = int_or_x_simps' [simplified arith_simps]
   23.59 -
   23.60 +lemma int_or_extra_simps [simp]:
   23.61 +  "w OR Int.Pls = w"
   23.62 +  "w OR Int.Min = Int.Min"
   23.63 +  using int_or_x_simps' by simp_all
   23.64  
   23.65  lemma int_and_Pls [simp]:
   23.66    "Int.Pls AND x = Int.Pls"
   23.67 @@ -112,6 +133,13 @@
   23.68    "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
   23.69    unfolding int_and_def by (simp add: bin_rec_simps)
   23.70  
   23.71 +lemma int_and_Bits2 [simp]: 
   23.72 +  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   23.73 +  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
   23.74 +  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   23.75 +  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
   23.76 +  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
   23.77 +
   23.78  lemma int_and_x_simps': 
   23.79    "w AND (Int.Pls BIT bit.B0) = Int.Pls"
   23.80    "w AND (Int.Min BIT bit.B1) = w"
   23.81 @@ -121,7 +149,10 @@
   23.82     apply clarsimp+
   23.83    done
   23.84  
   23.85 -lemmas int_and_extra_simps [simp] = int_and_x_simps' [simplified arith_simps]
   23.86 +lemma int_and_extra_simps [simp]:
   23.87 +  "w AND Int.Pls = Int.Pls"
   23.88 +  "w AND Int.Min = w"
   23.89 +  using int_and_x_simps' by simp_all
   23.90  
   23.91  (* commutativity of the above *)
   23.92  lemma bin_ops_comm:
   23.93 @@ -194,7 +225,7 @@
   23.94      apply (case_tac [!] z rule: bin_exhaust)
   23.95      apply (case_tac [!] bit)
   23.96         apply (case_tac [!] b)
   23.97 -             apply auto
   23.98 +             apply (auto simp del: BIT_simps)
   23.99    done
  23.100  
  23.101  lemma int_and_assoc:
  23.102 @@ -225,7 +256,7 @@
  23.103    apply (induct x rule: bin_induct)
  23.104         apply auto
  23.105     apply (case_tac [!] y rule: bin_exhaust)
  23.106 -   apply (case_tac [!] bit, auto)
  23.107 +   apply (case_tac [!] bit, auto simp del: BIT_simps)
  23.108    done
  23.109  
  23.110  lemma bbw_oa_dist: 
  23.111 @@ -235,7 +266,7 @@
  23.112      apply auto
  23.113    apply (case_tac y rule: bin_exhaust)
  23.114    apply (case_tac z rule: bin_exhaust)
  23.115 -  apply (case_tac ba, auto)
  23.116 +  apply (case_tac ba, auto simp del: BIT_simps)
  23.117    done
  23.118  
  23.119  lemma bbw_ao_dist: 
  23.120 @@ -245,7 +276,7 @@
  23.121      apply auto
  23.122    apply (case_tac y rule: bin_exhaust)
  23.123    apply (case_tac z rule: bin_exhaust)
  23.124 -  apply (case_tac ba, auto)
  23.125 +  apply (case_tac ba, auto simp del: BIT_simps)
  23.126    done
  23.127  
  23.128  (*
  23.129 @@ -289,9 +320,9 @@
  23.130    apply (induct n)
  23.131           apply safe
  23.132                           apply (case_tac [!] x rule: bin_exhaust)
  23.133 -                         apply simp_all
  23.134 +                         apply (simp_all del: BIT_simps)
  23.135                        apply (case_tac [!] y rule: bin_exhaust)
  23.136 -                      apply simp_all
  23.137 +                      apply (simp_all del: BIT_simps)
  23.138          apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
  23.139    done
  23.140  
  23.141 @@ -392,7 +423,7 @@
  23.142    "!!w. bin_sc n bit.B0 w <= w"
  23.143    apply (induct n) 
  23.144     apply (case_tac [!] w rule: bin_exhaust)
  23.145 -   apply auto
  23.146 +   apply (auto simp del: BIT_simps)
  23.147     apply (unfold Bit_def)
  23.148     apply (simp_all split: bit.split)
  23.149    done
  23.150 @@ -401,7 +432,7 @@
  23.151    "!!w. bin_sc n bit.B1 w >= w"
  23.152    apply (induct n) 
  23.153     apply (case_tac [!] w rule: bin_exhaust)
  23.154 -   apply auto
  23.155 +   apply (auto simp del: BIT_simps)
  23.156     apply (unfold Bit_def)
  23.157     apply (simp_all split: bit.split)
  23.158    done
  23.159 @@ -412,7 +443,7 @@
  23.160     apply simp
  23.161    apply (case_tac w rule: bin_exhaust)
  23.162    apply (case_tac m)
  23.163 -   apply auto
  23.164 +   apply (auto simp del: BIT_simps)
  23.165     apply (unfold Bit_def)
  23.166     apply (simp_all split: bit.split)
  23.167    done
  23.168 @@ -423,7 +454,7 @@
  23.169     apply simp
  23.170    apply (case_tac w rule: bin_exhaust)
  23.171    apply (case_tac m)
  23.172 -   apply auto
  23.173 +   apply (auto simp del: BIT_simps)
  23.174     apply (unfold Bit_def)
  23.175     apply (simp_all split: bit.split)
  23.176    done
    24.1 --- a/src/HOL/Word/BitSyntax.thy	Sat Feb 16 16:52:09 2008 +0100
    24.2 +++ b/src/HOL/Word/BitSyntax.thy	Sun Feb 17 06:49:53 2008 +0100
    24.3 @@ -9,7 +9,7 @@
    24.4  header {* Syntactic class for bitwise operations *}
    24.5  
    24.6  theory BitSyntax
    24.7 -imports Main
    24.8 +imports Main Num_Lemmas
    24.9  begin
   24.10  
   24.11  class bit = type +
   24.12 @@ -43,7 +43,7 @@
   24.13    shiftr   :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
   24.14  
   24.15  
   24.16 -subsection {* Bitwise operations on type @{typ bit} *}
   24.17 +subsection {* Bitwise operations on @{typ bit} *}
   24.18  
   24.19  instantiation bit :: bit
   24.20  begin
    25.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Sat Feb 16 16:52:09 2008 +0100
    25.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Sun Feb 17 06:49:53 2008 +0100
    25.3 @@ -92,7 +92,7 @@
    25.4  lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
    25.5  
    25.6  lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" 
    25.7 -  by (auto simp add: bin_nth_Bit)
    25.8 +  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
    25.9  
   25.10  lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
   25.11  lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
    26.1 --- a/src/HOL/Word/Num_Lemmas.thy	Sat Feb 16 16:52:09 2008 +0100
    26.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Sun Feb 17 06:49:53 2008 +0100
    26.3 @@ -9,6 +9,22 @@
    26.4  imports Main Parity
    26.5  begin
    26.6  
    26.7 +datatype bit = B0 | B1
    26.8 +
    26.9 +definition
   26.10 +  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
   26.11 +  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
   26.12 +
   26.13 +lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
   26.14 +  unfolding Bit_def Bit0_def by simp
   26.15 +
   26.16 +lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
   26.17 +  unfolding Bit_def Bit1_def by simp
   26.18 +
   26.19 +lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
   26.20 +
   26.21 +hide (open) const B0 B1
   26.22 +
   26.23  lemma contentsI: "y = {x} ==> contents y = x" 
   26.24    unfolding contents_def by auto
   26.25  
   26.26 @@ -197,8 +213,13 @@
   26.27     apply auto
   26.28    done
   26.29  
   26.30 -lemmas bin_rl_simps [THEN bin_rl_char [THEN iffD2], standard, simp] =
   26.31 -  Pls_0_eq Min_1_eq refl 
   26.32 +lemma bin_rl_simps [simp]:
   26.33 +  "bin_rl Int.Pls = (Int.Pls, bit.B0)"
   26.34 +  "bin_rl Int.Min = (Int.Min, bit.B1)"
   26.35 +  "bin_rl (r BIT b) = (r, b)"
   26.36 +  "bin_rl (Int.Bit0 r) = (r, bit.B0)"
   26.37 +  "bin_rl (Int.Bit1 r) = (r, bit.B1)"
   26.38 +  unfolding bin_rl_char by simp_all
   26.39  
   26.40  lemma bin_abs_lem:
   26.41    "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
   26.42 @@ -223,6 +244,24 @@
   26.43    apply (auto simp add : PPls PMin PBit)
   26.44    done
   26.45  
   26.46 +lemma numeral_induct:
   26.47 +  assumes Pls: "P Int.Pls"
   26.48 +  assumes Min: "P Int.Min"
   26.49 +  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
   26.50 +  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
   26.51 +  shows "P x"
   26.52 +  apply (induct x rule: bin_induct)
   26.53 +    apply (rule Pls)
   26.54 +   apply (rule Min)
   26.55 +  apply (case_tac bit)
   26.56 +   apply (case_tac "bin = Int.Pls")
   26.57 +    apply simp
   26.58 +   apply (simp add: Bit0)
   26.59 +  apply (case_tac "bin = Int.Min")
   26.60 +   apply simp
   26.61 +  apply (simp add: Bit1)
   26.62 +  done
   26.63 +
   26.64  lemma no_no [simp]: "number_of (number_of i) = i"
   26.65    unfolding number_of_eq by simp
   26.66  
   26.67 @@ -245,9 +284,12 @@
   26.68    apply (simp (no_asm) only: Bit_B0 Bit_B1)
   26.69    apply (simp add: z1pmod2)
   26.70    done
   26.71 -    
   26.72 -lemmas B1_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct1, standard]
   26.73 -lemmas B0_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct2, standard]
   26.74 +
   26.75 +lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
   26.76 +  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
   26.77 +
   26.78 +lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
   26.79 +  unfolding numeral_simps number_of_is_id by simp
   26.80  
   26.81  lemma axxbyy:
   26.82    "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>  
    27.1 --- a/src/HOL/Word/WordArith.thy	Sat Feb 16 16:52:09 2008 +0100
    27.2 +++ b/src/HOL/Word/WordArith.thy	Sun Feb 17 06:49:53 2008 +0100
    27.3 @@ -395,7 +395,7 @@
    27.4  
    27.5  lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
    27.6    unfolding word_arith_wis
    27.7 -  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
    27.8 +  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc eq_Bit0_Bit1)
    27.9  
   27.10  lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
   27.11  
    28.1 --- a/src/HOL/Word/WordMain.thy	Sat Feb 16 16:52:09 2008 +0100
    28.2 +++ b/src/HOL/Word/WordMain.thy	Sun Feb 17 06:49:53 2008 +0100
    28.3 @@ -10,7 +10,7 @@
    28.4  theory WordMain imports WordGenLib
    28.5  begin
    28.6  
    28.7 -lemmas word_no_1 [simp] = word_1_no [symmetric]
    28.8 +lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
    28.9  lemmas word_no_0 [simp] = word_0_no [symmetric]
   28.10  
   28.11  declare word_0_bl [simp]
    29.1 --- a/src/HOL/Word/WordShift.thy	Sat Feb 16 16:52:09 2008 +0100
    29.2 +++ b/src/HOL/Word/WordShift.thy	Sun Feb 17 06:49:53 2008 +0100
    29.3 @@ -14,7 +14,8 @@
    29.4  lemma shiftl1_number [simp] :
    29.5    "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
    29.6    apply (unfold shiftl1_def word_number_of_def)
    29.7 -  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
    29.8 +  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
    29.9 +              del: BIT_simps)
   29.10    apply (subst refl [THEN bintrunc_BIT_I, symmetric])
   29.11    apply (subst bintrunc_bintrunc_min)
   29.12    apply simp
   29.13 @@ -331,13 +332,13 @@
   29.14  
   29.15  lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
   29.16    apply (simp add: shiftl1_def_u)
   29.17 -  apply (simp only:  double_number_of_BIT [symmetric])
   29.18 +  apply (simp only:  double_number_of_Bit0 [symmetric])
   29.19    apply simp
   29.20    done
   29.21  
   29.22  lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
   29.23    apply (simp add: shiftl1_def_u)
   29.24 -  apply (simp only: double_number_of_BIT [symmetric])
   29.25 +  apply (simp only: double_number_of_Bit0 [symmetric])
   29.26    apply simp
   29.27    done
   29.28  
    30.1 --- a/src/HOL/hologic.ML	Sat Feb 16 16:52:09 2008 +0100
    30.2 +++ b/src/HOL/hologic.ML	Sun Feb 17 06:49:53 2008 +0100
    30.3 @@ -88,15 +88,13 @@
    30.4    val class_size: string
    30.5    val size_const: typ -> term
    30.6    val indexT: typ
    30.7 -  val bitT: typ
    30.8 -  val B0_const: term
    30.9 -  val B1_const: term
   30.10 -  val mk_bit: int -> term
   30.11 -  val dest_bit: term -> int
   30.12    val intT: typ
   30.13    val pls_const: term
   30.14    val min_const: term
   30.15 -  val bit_const: term
   30.16 +  val bit0_const: term
   30.17 +  val bit1_const: term
   30.18 +  val mk_bit: int -> term
   30.19 +  val dest_bit: term -> int
   30.20    val mk_numeral: int -> term
   30.21    val dest_numeral: term -> int
   30.22    val number_of_const: typ -> term
   30.23 @@ -452,39 +450,33 @@
   30.24  val indexT = Type ("Code_Index.index", []);
   30.25  
   30.26  
   30.27 -(* bit *)
   30.28 -
   30.29 -val bitT = Type ("Int.bit", []);
   30.30 -
   30.31 -val B0_const = Const ("Int.bit.B0", bitT);
   30.32 -val B1_const =  Const ("Int.bit.B1", bitT);
   30.33 -
   30.34 -fun mk_bit 0 = B0_const
   30.35 -  | mk_bit 1 = B1_const
   30.36 -  | mk_bit _ = raise TERM ("mk_bit", []);
   30.37 -
   30.38 -fun dest_bit (Const ("Int.bit.B0", _)) = 0
   30.39 -  | dest_bit (Const ("Int.bit.B1", _)) = 1
   30.40 -  | dest_bit t = raise TERM ("dest_bit", [t]);
   30.41 -
   30.42 -
   30.43  (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
   30.44  
   30.45  val intT = Type ("Int.int", []);
   30.46  
   30.47  val pls_const = Const ("Int.Pls", intT)
   30.48  and min_const = Const ("Int.Min", intT)
   30.49 -and bit_const = Const ("Int.Bit", intT --> bitT --> intT);
   30.50 +and bit0_const = Const ("Int.Bit0", intT --> intT)
   30.51 +and bit1_const = Const ("Int.Bit1", intT --> intT);
   30.52 +
   30.53 +fun mk_bit 0 = bit0_const
   30.54 +  | mk_bit 1 = bit1_const
   30.55 +  | mk_bit _ = raise TERM ("mk_bit", []);
   30.56 +
   30.57 +fun dest_bit (Const ("Int.Bit0", _)) = 0
   30.58 +  | dest_bit (Const ("Int.Bit1", _)) = 1
   30.59 +  | dest_bit t = raise TERM ("dest_bit", [t]);
   30.60  
   30.61  fun mk_numeral 0 = pls_const
   30.62    | mk_numeral ~1 = min_const
   30.63    | mk_numeral i =
   30.64        let val (q, r) = Integer.div_mod i 2;
   30.65 -      in bit_const $ mk_numeral q $ mk_bit r end;
   30.66 +      in mk_bit r $ mk_numeral q end;
   30.67  
   30.68  fun dest_numeral (Const ("Int.Pls", _)) = 0
   30.69    | dest_numeral (Const ("Int.Min", _)) = ~1
   30.70 -  | dest_numeral (Const ("Int.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
   30.71 +  | dest_numeral (Const ("Int.Bit0", _) $ bs) = 2 * dest_numeral bs
   30.72 +  | dest_numeral (Const ("Int.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
   30.73    | dest_numeral t = raise TERM ("dest_numeral", [t]);
   30.74  
   30.75  fun number_of_const T = Const ("Int.number_class.number_of", intT --> T);
    31.1 --- a/src/HOL/int_arith1.ML	Sat Feb 16 16:52:09 2008 +0100
    31.2 +++ b/src/HOL/int_arith1.ML	Sun Feb 17 06:49:53 2008 +0100
    31.3 @@ -548,7 +548,7 @@
    31.4      simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
    31.5      [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
    31.6       @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
    31.7 -     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
    31.8 +     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
    31.9       @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
   31.10       @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
   31.11       @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
    32.1 --- a/src/HOL/int_factor_simprocs.ML	Sat Feb 16 16:52:09 2008 +0100
    32.2 +++ b/src/HOL/int_factor_simprocs.ML	Sun Feb 17 06:49:53 2008 +0100
    32.3 @@ -43,7 +43,7 @@
    32.4    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    32.5    val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
    32.6      [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
    32.7 -      @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
    32.8 +      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
    32.9    end
   32.10  
   32.11  (*Version for integer division*)
    33.1 --- a/src/Tools/code/code_target.ML	Sat Feb 16 16:52:09 2008 +0100
    33.2 +++ b/src/Tools/code/code_target.ML	Sun Feb 17 06:49:53 2008 +0100
    33.3 @@ -23,7 +23,7 @@
    33.4    val add_pretty_list_string: string -> string -> string
    33.5      -> string -> string list -> theory -> theory;
    33.6    val add_pretty_char: string -> string -> string list -> theory -> theory
    33.7 -  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string -> string
    33.8 +  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
    33.9      -> string -> string -> theory -> theory;
   33.10    val add_pretty_message: string -> string -> string list -> string
   33.11      -> string -> string -> theory -> theory;
   33.12 @@ -234,7 +234,7 @@
   33.13      else NONE
   33.14    end;
   33.15  
   33.16 -fun implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit =
   33.17 +fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =
   33.18    let
   33.19      fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
   33.20            else if c = c_bit1 then 1
   33.21 @@ -244,10 +244,9 @@
   33.22            else if c = c_min then
   33.23              if negative then SOME ~1 else NONE
   33.24            else error "Illegal numeral expression: illegal leading digit"
   33.25 -      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
   33.26 -          if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
   33.27 -            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
   33.28 -          else error "Illegal numeral expression: illegal bit shift operator"
   33.29 +      | dest_numeral (t1 `$ t2) =
   33.30 +          let val (n, b) = (dest_numeral t2, dest_bit t1)
   33.31 +          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
   33.32        | dest_numeral _ = error "Illegal numeral expression: illegal constant";
   33.33    in dest_numeral #> the_default 0 end;
   33.34  
   33.35 @@ -1825,11 +1824,11 @@
   33.36          | NONE => error "Illegal character expression";
   33.37    in (2, pretty) end;
   33.38  
   33.39 -fun pretty_numeral unbounded negative c_bit0 c_bit1 c_pls c_min c_bit target =
   33.40 +fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
   33.41    let
   33.42      val mk_numeral = #pretty_numeral (pr_pretty target);
   33.43      fun pretty _ _ _ [(t, _)] =
   33.44 -      (str o mk_numeral unbounded o implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit) t;
   33.45 +      (str o mk_numeral unbounded o implode_numeral negative c_pls c_min c_bit0 c_bit1) t;
   33.46    in (1, pretty) end;
   33.47  
   33.48  fun pretty_message c_char c_nibbles c_nil c_cons target =
   33.49 @@ -2100,14 +2099,13 @@
   33.50      |> add_syntax_const target charr (SOME pr)
   33.51    end;
   33.52  
   33.53 -fun add_pretty_numeral target unbounded negative number_of b0 b1 pls min bit thy =
   33.54 +fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   33.55    let
   33.56 -    val b0' = CodeName.const thy b0;
   33.57 -    val b1' = CodeName.const thy b1;
   33.58      val pls' = CodeName.const thy pls;
   33.59      val min' = CodeName.const thy min;
   33.60 -    val bit' = CodeName.const thy bit;
   33.61 -    val pr = pretty_numeral unbounded negative b0' b1' pls' min' bit' target;
   33.62 +    val bit0' = CodeName.const thy bit0;
   33.63 +    val bit1' = CodeName.const thy bit1;
   33.64 +    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
   33.65    in
   33.66      thy
   33.67      |> add_syntax_const target number_of (SOME pr)