# HG changeset patch
# User huffman
# Date 1203227393 -3600
# Node ID 3c243098b64aedc43d516e151b48c3af09e6f715
# Parent  4ce22e7a81bdcaaf4b946d4dd93aa0edc0197b05
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1

diff -r 4ce22e7a81bd -r 3c243098b64a NEWS
--- a/NEWS	Sat Feb 16 16:52:09 2008 +0100
+++ b/NEWS	Sun Feb 17 06:49:53 2008 +0100
@@ -35,6 +35,12 @@
 
 *** HOL ***
 
+* Theory Int: The representation of numerals has changed.  The infix operator
+BIT and the bit datatype with constructors B0 and B1 have disappeared.
+INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in place of "x BIT bit.B0"
+and "y BIT bit.B1", respectively.  Theorems involving BIT, B0, or B1 have been
+renamed with "Bit0" or "Bit1" accordingly.
+
 * Theory Nat: definition of <= and < on natural numbers no longer depend
 on well-founded relations.  INCOMPATIBILITY.  Definitions le_def and less_def
 have disappeared.  Consider lemmas not_less [symmetric, where ?'a = nat]
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -179,7 +179,7 @@
   if_True add_0 add_Suc add_number_of_left mult_number_of_left
   numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
   numeral_0_eq_0[symmetric] numerals[symmetric] not_iszero_1
-  iszero_number_of_1 iszero_number_of_0 nonzero_number_of_Min
+  iszero_number_of_Bit1 iszero_number_of_Bit0 nonzero_number_of_Min
   iszero_number_of_Pls iszero_0 not_iszero_Numeral1
 
 lemmas semiring_norm = comp_arith
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Import/HOL/HOL4Prob.thy
--- a/src/HOL/Import/HOL/HOL4Prob.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -36,28 +36,24 @@
  ((op =::nat => nat => bool)
    ((op div::nat => nat => nat) (0::nat)
      ((number_of \<Colon> int => nat)
-       ((op BIT \<Colon> int => bit => int)
-         ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-         (bit.B0::bit))))
+       ((Int.Bit0 \<Colon> int => int)
+         ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
    (0::nat))
  ((op &::bool => bool => bool)
    ((op =::nat => nat => bool)
      ((op div::nat => nat => nat) (1::nat)
        ((number_of \<Colon> int => nat)
-         ((op BIT \<Colon> int => bit => int)
-           ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-           (bit.B0::bit))))
+         ((Int.Bit0 \<Colon> int => int)
+           ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
      (0::nat))
    ((op =::nat => nat => bool)
      ((op div::nat => nat => nat)
        ((number_of \<Colon> int => nat)
-         ((op BIT \<Colon> int => bit => int)
-           ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-           (bit.B0::bit)))
+         ((Int.Bit0 \<Colon> int => int)
+           ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
        ((number_of \<Colon> int => nat)
-         ((op BIT \<Colon> int => bit => int)
-           ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-           (bit.B0::bit))))
+         ((Int.Bit0 \<Colon> int => int)
+           ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
      (1::nat)))"
   by (import prob_extra DIV_TWO_BASIC)
 
@@ -76,19 +72,16 @@
       ((op div::nat => nat => nat)
         ((op ^::nat => nat => nat)
           ((number_of \<Colon> int => nat)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit)))
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
           ((Suc::nat => nat) n))
         ((number_of \<Colon> int => nat)
-          ((op BIT \<Colon> int => bit => int)
-            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-            (bit.B0::bit))))
+          ((Int.Bit0 \<Colon> int => int)
+            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
       ((op ^::nat => nat => nat)
         ((number_of \<Colon> int => nat)
-          ((op BIT \<Colon> int => bit => int)
-            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-            (bit.B0::bit)))
+          ((Int.Bit0 \<Colon> int => int)
+            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
         n))"
   by (import prob_extra EXP_DIV_TWO)
 
@@ -126,22 +119,19 @@
 lemma HALF_POS: "(op <::real => real => bool) (0::real)
  ((op /::real => real => real) (1::real)
    ((number_of \<Colon> int => real)
-     ((op BIT \<Colon> int => bit => int)
-       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-       (bit.B0::bit))))"
+     ((Int.Bit0 \<Colon> int => int)
+       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))"
   by (import prob_extra HALF_POS)
 
 lemma HALF_CANCEL: "(op =::real => real => bool)
  ((op *::real => real => real)
    ((number_of \<Colon> int => real)
-     ((op BIT \<Colon> int => bit => int)
-       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-       (bit.B0::bit)))
+     ((Int.Bit0 \<Colon> int => int)
+       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
    ((op /::real => real => real) (1::real)
      ((number_of \<Colon> int => real)
-       ((op BIT \<Colon> int => bit => int)
-         ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-         (bit.B0::bit)))))
+       ((Int.Bit0 \<Colon> int => int)
+         ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))))
  (1::real)"
   by (import prob_extra HALF_CANCEL)
 
@@ -151,9 +141,8 @@
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
           ((number_of \<Colon> int => real)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit))))
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
         n))"
   by (import prob_extra POW_HALF_POS)
 
@@ -166,18 +155,14 @@
              ((op ^::real => nat => real)
                ((op /::real => real => real) (1::real)
                  ((number_of \<Colon> int => real)
-                   ((op BIT \<Colon> int => bit => int)
-                     ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                       (bit.B1::bit))
-                     (bit.B0::bit))))
+                   ((Int.Bit0 \<Colon> int => int)
+                     ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
                n)
              ((op ^::real => nat => real)
                ((op /::real => real => real) (1::real)
                  ((number_of \<Colon> int => real)
-                   ((op BIT \<Colon> int => bit => int)
-                     ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                       (bit.B1::bit))
-                     (bit.B0::bit))))
+                   ((Int.Bit0 \<Colon> int => int)
+                     ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
                m))))"
   by (import prob_extra POW_HALF_MONO)
 
@@ -187,22 +172,18 @@
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
           ((number_of \<Colon> int => real)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit))))
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
         n)
       ((op *::real => real => real)
         ((number_of \<Colon> int => real)
-          ((op BIT \<Colon> int => bit => int)
-            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-            (bit.B0::bit)))
+          ((Int.Bit0 \<Colon> int => int)
+            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
         ((op ^::real => nat => real)
           ((op /::real => real => real) (1::real)
             ((number_of \<Colon> int => real)
-              ((op BIT \<Colon> int => bit => int)
-                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                  (bit.B1::bit))
-                (bit.B0::bit))))
+              ((Int.Bit0 \<Colon> int => int)
+                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
           ((Suc::nat => nat) n))))"
   by (import prob_extra POW_HALF_TWICE)
 
@@ -228,22 +209,19 @@
  ((op -::real => real => real) (1::real)
    ((op /::real => real => real) (1::real)
      ((number_of \<Colon> int => real)
-       ((op BIT \<Colon> int => bit => int)
-         ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-         (bit.B0::bit)))))
+       ((Int.Bit0 \<Colon> int => int)
+         ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))))
  ((op /::real => real => real) (1::real)
    ((number_of \<Colon> int => real)
-     ((op BIT \<Colon> int => bit => int)
-       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-       (bit.B0::bit))))"
+     ((Int.Bit0 \<Colon> int => int)
+       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))"
   by (import prob_extra ONE_MINUS_HALF)
 
 lemma HALF_LT_1: "(op <::real => real => bool)
  ((op /::real => real => real) (1::real)
    ((number_of \<Colon> int => real)
-     ((op BIT \<Colon> int => bit => int)
-       ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-       (bit.B0::bit))))
+     ((Int.Bit0 \<Colon> int => int)
+       ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
  (1::real)"
   by (import prob_extra HALF_LT_1)
 
@@ -253,18 +231,15 @@
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
           ((number_of \<Colon> int => real)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit))))
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
         n)
       ((inverse::real => real)
         ((real::nat => real)
           ((op ^::nat => nat => nat)
             ((number_of \<Colon> int => nat)
-              ((op BIT \<Colon> int => bit => int)
-                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                  (bit.B1::bit))
-                (bit.B0::bit)))
+              ((Int.Bit0 \<Colon> int => int)
+                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
             n))))"
   by (import prob_extra POW_HALF_EXP)
 
@@ -1406,27 +1381,22 @@
         ((op ^::real => nat => real)
           ((op /::real => real => real) (1::real)
             ((number_of \<Colon> int => real)
-              ((op BIT \<Colon> int => bit => int)
-                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                  (bit.B1::bit))
-                (bit.B0::bit))))
+              ((Int.Bit0 \<Colon> int => int)
+                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
           ((size::bool list => nat)
             ((SNOC::bool => bool list => bool list) (True::bool) l)))
         ((op ^::real => nat => real)
           ((op /::real => real => real) (1::real)
             ((number_of \<Colon> int => real)
-              ((op BIT \<Colon> int => bit => int)
-                ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                  (bit.B1::bit))
-                (bit.B0::bit))))
+              ((Int.Bit0 \<Colon> int => int)
+                ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
           ((size::bool list => nat)
             ((SNOC::bool => bool list => bool list) (False::bool) l))))
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
           ((number_of \<Colon> int => real)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit))))
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
         ((size::bool list => nat) l)))"
   by (import prob ALG_TWINS_MEASURE)
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Import/HOL/HOL4Real.thy
--- a/src/HOL/Import/HOL/HOL4Real.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -526,9 +526,8 @@
       ((op <=::real => real => bool) (1::real)
         ((op ^::real => nat => real) x
           ((number_of \<Colon> int => nat)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit))))))"
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))))"
   by (import real REAL_LE1_POW2)
 
 lemma REAL_LT1_POW2: "(All::(real => bool) => bool)
@@ -538,9 +537,8 @@
       ((op <::real => real => bool) (1::real)
         ((op ^::real => nat => real) x
           ((number_of \<Colon> int => nat)
-            ((op BIT \<Colon> int => bit => int)
-              ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-              (bit.B0::bit))))))"
+            ((Int.Bit0 \<Colon> int => int)
+              ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))))"
   by (import real REAL_LT1_POW2)
 
 lemma POW_POS_LT: "ALL (x::real) n::nat. 0 < x --> 0 < x ^ Suc n"
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Import/HOL/HOL4Vec.thy
--- a/src/HOL/Import/HOL/HOL4Vec.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -1283,9 +1283,8 @@
      (op -->::bool => bool => bool)
       ((op <::nat => nat => bool) x
         ((number_of \<Colon> int => nat)
-          ((op BIT \<Colon> int => bit => int)
-            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-            (bit.B0::bit))))
+          ((Int.Bit0 \<Colon> int => int)
+            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
       ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
         x))"
   by (import bword_num BV_VB)
@@ -1500,10 +1499,9 @@
                            ((BV::bool => nat) cin))
                          ((op ^::nat => nat => nat)
                            ((number_of \<Colon> int => nat)
-                             ((op BIT \<Colon> int => bit => int)
-                               ((op BIT \<Colon> int => bit => int)
-                                 (Int.Pls \<Colon> int) (bit.B1::bit))
-                               (bit.B0::bit)))
+                             ((Int.Bit0 \<Colon> int => int)
+                               ((Int.Bit1 \<Colon> int => int)
+                                 (Int.Pls \<Colon> int))))
                            k)))))))"
   by (import bword_arith ACARRY_EQ_ADD_DIV)
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Import/HOL/HOL4Word32.thy
--- a/src/HOL/Import/HOL/HOL4Word32.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -117,9 +117,8 @@
      (op <::nat => nat => bool) (0::nat)
       ((op ^::nat => nat => nat)
         ((number_of \<Colon> int => nat)
-          ((op BIT \<Colon> int => bit => int)
-            ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
-            (bit.B0::bit)))
+          ((Int.Bit0 \<Colon> int => int)
+            ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
         n))"
   by (import bits ZERO_LT_TWOEXP)
 
@@ -137,17 +136,13 @@
            ((op <::nat => nat => bool)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                a)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                b))))"
   by (import bits TWOEXP_MONO)
 
@@ -159,17 +154,13 @@
            ((op <=::nat => nat => bool)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                a)
              ((op ^::nat => nat => nat)
                ((number_of \<Colon> int => nat)
-                 ((op BIT \<Colon> int => bit => int)
-                   ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                     (bit.B1::bit))
-                   (bit.B0::bit)))
+                 ((Int.Bit0 \<Colon> int => int)
+                   ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                b))))"
   by (import bits TWOEXP_MONO2)
 
@@ -180,17 +171,13 @@
           (op <=::nat => nat => bool)
            ((op ^::nat => nat => nat)
              ((number_of \<Colon> int => nat)
-               ((op BIT \<Colon> int => bit => int)
-                 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                   (bit.B1::bit))
-                 (bit.B0::bit)))
+               ((Int.Bit0 \<Colon> int => int)
+                 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
              ((op -::nat => nat => nat) a b))
            ((op ^::nat => nat => nat)
              ((number_of \<Colon> int => nat)
-               ((op BIT \<Colon> int => bit => int)
-                 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                   (bit.B1::bit))
-                 (bit.B0::bit)))
+               ((Int.Bit0 \<Colon> int => int)
+                 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
              a)))"
   by (import bits EXP_SUB_LESS_EQ)
 
@@ -349,25 +336,19 @@
                  (op =::nat => nat => bool)
                   ((op ^::nat => nat => nat)
                     ((number_of \<Colon> int => nat)
-                      ((op BIT \<Colon> int => bit => int)
-                        ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                          (bit.B1::bit))
-                        (bit.B0::bit)))
+                      ((Int.Bit0 \<Colon> int => int)
+                        ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                     b)
                   ((op *::nat => nat => nat)
                     ((op ^::nat => nat => nat)
                       ((number_of \<Colon> int => nat)
-                        ((op BIT \<Colon> int => bit => int)
-                          ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                            (bit.B1::bit))
-                          (bit.B0::bit)))
+                        ((Int.Bit0 \<Colon> int => int)
+                          ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                       ((op +::nat => nat => nat) x (1::nat)))
                     ((op ^::nat => nat => nat)
                       ((number_of \<Colon> int => nat)
-                        ((op BIT \<Colon> int => bit => int)
-                          ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int)
-                            (bit.B1::bit))
-                          (bit.B0::bit)))
+                        ((Int.Bit0 \<Colon> int => int)
+                          ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int))))
                       a))))))"
   by (import bits LESS_EXP_MULT2)
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Int.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -9,7 +9,7 @@
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
 
 theory Int
-imports Equiv_Relations Datatype Nat Wellfounded_Relations
+imports Equiv_Relations Nat Wellfounded_Relations
 uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
@@ -583,13 +583,6 @@
   Springer LNCS 488 (240-251), 1991.
 *}
 
-datatype bit = B0 | B1
-
-text{*
-  Type @{typ bit} avoids the use of type @{typ bool}, which would make
-  all of the rewrite rules higher-order.
-*}
-
 definition
   Pls :: int where
   [code func del]: "Pls = 0"
@@ -599,8 +592,12 @@
   [code func del]: "Min = - 1"
 
 definition
-  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
-  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+  Bit0 :: "int \<Rightarrow> int" where
+  [code func del]: "Bit0 k = k + k"
+
+definition
+  Bit1 :: "int \<Rightarrow> int" where
+  [code func del]: "Bit1 k = 1 + k + k"
 
 class number = type + -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
@@ -617,7 +614,7 @@
   "Numeral0 \<equiv> number_of Pls"
 
 abbreviation
-  "Numeral1 \<equiv> number_of (Pls BIT B1)"
+  "Numeral1 \<equiv> number_of (Bit1 Pls)"
 
 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
   -- {* Unfold all @{text let}s involving constants *}
@@ -640,80 +637,80 @@
   -- {* unfolding @{text minx} and @{text max} on numerals *}
 
 lemmas numeral_simps = 
-  succ_def pred_def Pls_def Min_def Bit_def
+  succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
 
 text {* Removal of leading zeroes *}
 
-lemma Pls_0_eq [simp, code post]:
-  "Pls BIT B0 = Pls"
+lemma Bit0_Pls [simp, code post]:
+  "Bit0 Pls = Pls"
   unfolding numeral_simps by simp
 
-lemma Min_1_eq [simp, code post]:
-  "Min BIT B1 = Min"
+lemma Bit1_Min [simp, code post]:
+  "Bit1 Min = Min"
   unfolding numeral_simps by simp
 
 lemmas normalize_bin_simps =
-  Pls_0_eq Min_1_eq
+  Bit0_Pls Bit1_Min
 
 
 subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
 
 lemma succ_Pls [simp]:
-  "succ Pls = Pls BIT B1"
+  "succ Pls = Bit1 Pls"
   unfolding numeral_simps by simp
 
 lemma succ_Min [simp]:
   "succ Min = Pls"
   unfolding numeral_simps by simp
 
-lemma succ_1 [simp]:
-  "succ (k BIT B1) = succ k BIT B0"
+lemma succ_Bit0 [simp]:
+  "succ (Bit0 k) = Bit1 k"
   unfolding numeral_simps by simp
 
-lemma succ_0 [simp]:
-  "succ (k BIT B0) = k BIT B1"
+lemma succ_Bit1 [simp]:
+  "succ (Bit1 k) = Bit0 (succ k)"
   unfolding numeral_simps by simp
 
 lemmas succ_bin_simps =
-  succ_Pls succ_Min succ_1 succ_0
+  succ_Pls succ_Min succ_Bit0 succ_Bit1
 
 lemma pred_Pls [simp]:
   "pred Pls = Min"
   unfolding numeral_simps by simp
 
 lemma pred_Min [simp]:
-  "pred Min = Min BIT B0"
-  unfolding numeral_simps by simp
-
-lemma pred_1 [simp]:
-  "pred (k BIT B1) = k BIT B0"
+  "pred Min = Bit0 Min"
   unfolding numeral_simps by simp
 
-lemma pred_0 [simp]:
-  "pred (k BIT B0) = pred k BIT B1"
+lemma pred_Bit0 [simp]:
+  "pred (Bit0 k) = Bit1 (pred k)"
   unfolding numeral_simps by simp 
 
+lemma pred_Bit1 [simp]:
+  "pred (Bit1 k) = Bit0 k"
+  unfolding numeral_simps by simp
+
 lemmas pred_bin_simps =
-  pred_Pls pred_Min pred_1 pred_0
+  pred_Pls pred_Min pred_Bit0 pred_Bit1
 
 lemma minus_Pls [simp]:
   "- Pls = Pls"
   unfolding numeral_simps by simp 
 
 lemma minus_Min [simp]:
-  "- Min = Pls BIT B1"
+  "- Min = Bit1 Pls"
   unfolding numeral_simps by simp 
 
-lemma minus_1 [simp]:
-  "- (k BIT B1) = pred (- k) BIT B1"
+lemma minus_Bit0 [simp]:
+  "- (Bit0 k) = Bit0 (- k)"
   unfolding numeral_simps by simp 
 
-lemma minus_0 [simp]:
-  "- (k BIT B0) = (- k) BIT B0"
-  unfolding numeral_simps by simp 
+lemma minus_Bit1 [simp]:
+  "- (Bit1 k) = Bit1 (pred (- k))"
+  unfolding numeral_simps by simp
 
 lemmas minus_bin_simps =
-  minus_Pls minus_Min minus_1 minus_0
+  minus_Pls minus_Min minus_Bit0 minus_Bit1
 
 
 subsection {*
@@ -729,29 +726,33 @@
   "Min + k = pred k"
   unfolding numeral_simps by simp
 
-lemma add_BIT_11 [simp]:
-  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
+lemma add_Bit0_Bit0 [simp]:
+  "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
+  unfolding numeral_simps by simp_all 
+
+lemma add_Bit0_Bit1 [simp]:
+  "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
+  unfolding numeral_simps by simp_all 
+
+lemma add_Bit1_Bit0 [simp]:
+  "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
   unfolding numeral_simps by simp
 
-lemma add_BIT_10 [simp]:
-  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
+lemma add_Bit1_Bit1 [simp]:
+  "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
   unfolding numeral_simps by simp
 
-lemma add_BIT_0 [simp]:
-  "(k BIT B0) + (l BIT b) = (k + l) BIT b"
-  unfolding numeral_simps by simp 
-
 lemma add_Pls_right [simp]:
   "k + Pls = k"
   unfolding numeral_simps by simp 
 
 lemma add_Min_right [simp]:
   "k + Min = pred k"
-  unfolding numeral_simps by simp 
+  unfolding numeral_simps by simp
 
 lemmas add_bin_simps =
-  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
-  add_Pls_right add_Min_right
+  add_Pls add_Min add_Pls_right add_Min_right
+  add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
 
 lemma mult_Pls [simp]:
   "Pls * w = Pls"
@@ -761,16 +762,16 @@
   "Min * k = - k"
   unfolding numeral_simps by simp
 
-lemma mult_num1 [simp]:
-  "(k BIT B1) * l = ((k * l) BIT B0) + l"
-  unfolding numeral_simps int_distrib by simp 
+lemma mult_Bit0 [simp]:
+  "(Bit0 k) * l = Bit0 (k * l)"
+  unfolding numeral_simps int_distrib by simp
 
-lemma mult_num0 [simp]:
-  "(k BIT B0) * l = (k * l) BIT B0"
+lemma mult_Bit1 [simp]:
+  "(Bit1 k) * l = (Bit0 (k * l)) + l"
   unfolding numeral_simps int_distrib by simp 
 
 lemmas mult_bin_simps =
-  mult_Pls mult_Min mult_num1 mult_num0 
+  mult_Pls mult_Min mult_Bit0 mult_Bit1
 
 
 subsection {* Converting Numerals to Rings: @{term number_of} *}
@@ -820,8 +821,8 @@
   But it doesn't seem to give a measurable speed-up.
 *}
 
-lemma double_number_of_BIT:
-  "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
+lemma double_number_of_Bit0:
+  "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
   unfolding number_of_eq numeral_simps left_distrib by simp
 
 text {*
@@ -877,10 +878,13 @@
   "number_of Min = (- 1::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp
 
-lemma number_of_BIT:
-  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
-    + (number_of w) + (number_of w)"
-  unfolding number_of_eq numeral_simps by (simp split: bit.split)
+lemma number_of_Bit0:
+  "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
+  unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_Bit1:
+  "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
+  unfolding number_of_eq numeral_simps by simp
 
 
 subsection {* Equality of Binary Numbers *}
@@ -979,9 +983,9 @@
   qed
 qed
 
-lemma iszero_number_of_BIT:
-  "iszero (number_of (w BIT x)::'a) = 
-   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
+lemma iszero_number_of_Bit0:
+  "iszero (number_of (Bit0 w)::'a) = 
+   iszero (number_of w::'a::{ring_char_0,number_ring})"
 proof -
   have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
   proof -
@@ -990,27 +994,24 @@
     then have "w + w = 0" by (simp only: of_int_eq_iff)
     then show "w = 0" by (simp only: double_eq_0_iff)
   qed
-  moreover have "1 + of_int w + of_int w \<noteq> (0::'a)"
+  thus ?thesis
+    by (auto simp add: iszero_def number_of_eq numeral_simps)
+qed
+
+lemma iszero_number_of_Bit1:
+  "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
+proof -
+  have "1 + of_int w + of_int w \<noteq> (0::'a)"
   proof
     assume eq: "1 + of_int w + of_int w = (0::'a)"
     hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 
     hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
     with odd_nonzero show False by blast
   qed
-  ultimately show ?thesis
-    by (auto simp add: iszero_def number_of_eq numeral_simps 
-     split: bit.split)
+  thus ?thesis
+    by (auto simp add: iszero_def number_of_eq numeral_simps)
 qed
 
-lemma iszero_number_of_0:
-  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 
-  iszero (number_of w :: 'a)"
-  by (simp only: iszero_number_of_BIT simp_thms)
-
-lemma iszero_number_of_1:
-  "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
-  by (simp add: iszero_number_of_BIT) 
-
 
 subsection {* The Less-Than Relation *}
 
@@ -1056,16 +1057,20 @@
     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
-lemma neg_number_of_BIT:
-  "neg (number_of (w BIT x)::'a) = 
+lemma neg_number_of_Bit0:
+  "neg (number_of (Bit0 w)::'a) = 
+  neg (number_of w :: 'a::{ordered_idom,number_ring})"
+by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
+
+lemma neg_number_of_Bit1:
+  "neg (number_of (Bit1 w)::'a) = 
   neg (number_of w :: 'a::{ordered_idom,number_ring})"
 proof -
   have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
     by simp
   also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
   finally show ?thesis
-  by ( simp add: neg_def number_of_eq numeral_simps double_less_0_iff
-    split: bit.split)
+  by (simp add: neg_def number_of_eq numeral_simps)
 qed
 
 
@@ -1112,7 +1117,6 @@
 *}
 
 lemmas arith_simps = 
-  bit.distinct
   normalize_bin_simps pred_bin_simps succ_bin_simps
   add_bin_simps minus_bin_simps mult_bin_simps
   abs_zero abs_one arith_extra_simps
@@ -1121,10 +1125,10 @@
 
 lemmas rel_simps [simp] = 
   eq_number_of_eq iszero_0 nonzero_number_of_Min
-  iszero_number_of_0 iszero_number_of_1
+  iszero_number_of_Bit0 iszero_number_of_Bit1
   less_number_of_eq_neg
   not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
-  neg_number_of_Min neg_number_of_BIT
+  neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
   le_number_of_eq
 (* iszero_number_of_Pls would never be used
    because its lhs simplifies to "iszero 0" *)
@@ -1795,7 +1799,7 @@
 
 instance int :: eq ..
 
-code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
+code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
 
 definition
   int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
@@ -1883,7 +1887,7 @@
 
 (*setup continues in theory Presburger*)
 
-hide (open) const Pls Min B0 B1 succ pred
+hide (open) const Pls Min Bit0 Bit1 succ pred
 
 
 subsection {* Legacy theorems *}
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/IntDiv.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -1062,14 +1062,18 @@
 lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
 by auto
 
-lemma zdiv_number_of_BIT[simp]:
-     "number_of (v BIT b) div number_of (w BIT bit.B0) =  
-          (if b=bit.B0 | (0::int) \<le> number_of w                    
+lemma zdiv_number_of_Bit0 [simp]:
+     "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
+          number_of v div (number_of w :: int)"
+by (simp only: number_of_eq numeral_simps) simp
+
+lemma zdiv_number_of_Bit1 [simp]:
+     "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =  
+          (if (0::int) \<le> number_of w                    
            then number_of v div (number_of w)     
            else (number_of v + (1::int)) div (number_of w))"
 apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
-apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
-            split: bit.split)
+apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
 done
 
 
@@ -1087,7 +1091,7 @@
 apply (subst zmod_zadd1_eq)
 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
 apply (rule mod_pos_pos_trivial)
-apply (auto simp add: mod_pos_pos_trivial left_distrib)
+apply (auto simp add: mod_pos_pos_trivial ring_distribs)
 apply (subgoal_tac "0 \<le> b mod a", arith, simp)
 done
 
@@ -1102,14 +1106,20 @@
 apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
 done
 
-lemma zmod_number_of_BIT [simp]:
-     "number_of (v BIT b) mod number_of (w BIT bit.B0) =  
-      (case b of
-          bit.B0 => 2 * (number_of v mod number_of w)
-        | bit.B1 => if (0::int) \<le> number_of w  
+lemma zmod_number_of_Bit0 [simp]:
+     "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =  
+      (2::int) * (number_of v mod number_of w)"
+apply (simp only: number_of_eq numeral_simps) 
+apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
+                 not_0_le_lemma neg_zmod_mult_2 add_ac)
+done
+
+lemma zmod_number_of_Bit1 [simp]:
+     "number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) =  
+      (if (0::int) \<le> number_of w  
                 then 2 * (number_of v mod number_of w) + 1     
                 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
-apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 
+apply (simp only: number_of_eq numeral_simps) 
 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
                  not_0_le_lemma neg_zmod_mult_2 add_ac)
 done
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Char_nat.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -76,7 +76,7 @@
   unfolding nibble_of_nat_def Let_def by auto
 
 lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
-  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_BIT if_False add_0 add_Suc]
+  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
 
 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
   by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -88,7 +88,7 @@
 
 lemma one_index_code [code inline, code func]:
   "(1\<Colon>index) = Numeral1"
-  by (simp add: number_of_index_def Pls_def Bit_def)
+  by (simp add: number_of_index_def Pls_def Bit1_def)
 lemma [code post]: "Numeral1 = (1\<Colon>index)"
   using one_index_code ..
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -28,16 +28,19 @@
     true true) ["SML", "OCaml", "Haskell"]
 *}
 
-code_const "Int.Pls" and "Int.Min" and "Int.Bit"
+code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
   (SML "raise/ Fail/ \"Pls\""
      and "raise/ Fail/ \"Min\""
-     and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
+     and "!((_);/ raise/ Fail/ \"Bit0\")"
+     and "!((_);/ raise/ Fail/ \"Bit1\")")
   (OCaml "failwith/ \"Pls\""
      and "failwith/ \"Min\""
-     and "!((_);/ (_);/ failwith/ \"Bit\")")
+     and "!((_);/ failwith/ \"Bit0\")"
+     and "!((_);/ failwith/ \"Bit1\")")
   (Haskell "error/ \"Pls\""
      and "error/ \"Min\""
-     and "error/ \"Bit\"")
+     and "error/ \"Bit0\""
+     and "error/ \"Bit1\"")
 
 code_const Int.pred
   (SML "IntInf.- ((_), 1)")
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Library/Word.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -2265,14 +2265,14 @@
 primrec
   fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
   fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
-    fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))"
+    fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
 
 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
-    fast_bv_to_nat_helper bs (bin BIT bit.B0)"
+    fast_bv_to_nat_helper bs (Int.Bit0 bin)"
   by simp
 
 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
-    fast_bv_to_nat_helper bs (bin BIT bit.B1)"
+    fast_bv_to_nat_helper bs (Int.Bit1 bin)"
   by simp
 
 lemma fast_bv_to_nat_def:
@@ -2301,8 +2301,10 @@
     | is_const_bit _ = false
   fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
     | num_is_usable (Const(@{const_name Int.Min},_)) = false
-    | num_is_usable (Const(@{const_name Int.Bit},_) $ w $ b) =
-        num_is_usable w andalso is_const_bool b
+    | num_is_usable (Const(@{const_name Int.Bit0},_) $ w) =
+        num_is_usable w
+    | num_is_usable (Const(@{const_name Int.Bit1},_) $ w) =
+        num_is_usable w
     | num_is_usable _ = false
   fun vec_is_usable (Const("List.list.Nil",_)) = true
     | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/NatBin.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -524,44 +524,6 @@
 by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
 
 
-lemma lemma1: "(m+m = n+n) = (m = (n::int))"
-by auto
-
-lemma lemma2: "m+m ~= (1::int) + (n + n)"
-apply auto
-apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp add: zmod_zadd1_eq)
-done
-
-lemma eq_number_of_BIT_BIT:
-     "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
-      (x=y & (((number_of v) ::int) = number_of w))"
-apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
-               OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0_left
-            split add: bit.split)
-apply simp
-done
-
-lemma eq_number_of_BIT_Pls:
-     "((number_of (v BIT x) ::int) = Numeral0) =  
-      (x=bit.B0 & (((number_of v) ::int) = Numeral0))"
-apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
-            split add: bit.split cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec, safe)
-apply (simp_all (no_asm_use))
-apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp add: zmod_zadd1_eq)
-done
-
-lemma eq_number_of_BIT_Min:
-     "((number_of (v BIT x) ::int) = number_of Int.Min) =  
-      (x=bit.B1 & (((number_of v) ::int) = number_of Int.Min))"
-apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
-            split add: bit.split cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec, auto)
-apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
-done
-
 lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
 by auto
 
@@ -632,8 +594,8 @@
 
 lemma power_number_of_even:
   fixes z :: "'a::{number_ring,recpower}"
-  shows "z ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
-unfolding Let_def nat_number_of_def number_of_BIT bit.cases
+  shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
+unfolding Let_def nat_number_of_def number_of_Bit0
 apply (rule_tac x = "number_of w" in spec, clarify)
 apply (case_tac " (0::int) <= x")
 apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
@@ -641,9 +603,9 @@
 
 lemma power_number_of_odd:
   fixes z :: "'a::{number_ring,recpower}"
-  shows "z ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w
+  shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
      then (let w = z ^ (number_of w) in z * w * w) else 1)"
-unfolding Let_def nat_number_of_def number_of_BIT bit.cases
+unfolding Let_def nat_number_of_def number_of_Bit1
 apply (rule_tac x = "number_of w" in spec, auto)
 apply (simp only: nat_add_distrib nat_mult_distrib)
 apply simp
@@ -673,7 +635,7 @@
       lessD = lessD, neqE = neqE,
       simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
         @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
-        @{thm neg_number_of_BIT}]})
+        @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
 *}
 
 declaration {* K nat_bin_arith_setup *}
@@ -689,33 +651,32 @@
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   done
 
-lemma nat_number_of_BIT_1:
-  "number_of (w BIT bit.B1) =
+lemma nat_number_of_Bit0:
+    "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
+  apply (simp only: nat_number_of_def Let_def)
+  apply (cases "neg (number_of w :: int)")
+   apply (simp add: neg_nat neg_number_of_Bit0)
+  apply (rule int_int_eq [THEN iffD1])
+  apply (simp only: not_neg_nat neg_number_of_Bit0 int_Suc zadd_int [symmetric] simp_thms)
+  apply (simp only: number_of_Bit0 zadd_assoc)
+  apply simp
+  done
+
+lemma nat_number_of_Bit1:
+  "number_of (Int.Bit1 w) =
     (if neg (number_of w :: int) then 0
      else let n = number_of w in Suc (n + n))"
   apply (simp only: nat_number_of_def Let_def split: split_if)
   apply (intro conjI impI)
-   apply (simp add: neg_nat neg_number_of_BIT)
+   apply (simp add: neg_nat neg_number_of_Bit1)
   apply (rule int_int_eq [THEN iffD1])
-  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
-  apply (simp only: number_of_BIT zadd_assoc split: bit.split)
-  apply simp
-  done
-
-lemma nat_number_of_BIT_0:
-    "number_of (w BIT bit.B0) = (let n::nat = number_of w in n + n)"
-  apply (simp only: nat_number_of_def Let_def)
-  apply (cases "neg (number_of w :: int)")
-   apply (simp add: neg_nat neg_number_of_BIT)
-  apply (rule int_int_eq [THEN iffD1])
-  apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
-  apply (simp only: number_of_BIT zadd_assoc)
-  apply simp
+  apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms)
+  apply (simp only: number_of_Bit1 zadd_assoc)
   done
 
 lemmas nat_number =
   nat_number_of_Pls nat_number_of_Min
-  nat_number_of_BIT_1 nat_number_of_BIT_0
+  nat_number_of_Bit0 nat_number_of_Bit1
 
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (simp add: Let_def)
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/NumberTheory/Euler.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -77,7 +77,7 @@
         by (auto simp add: zcong_zmult_prop2)
     qed
   then have "[j^2 = a] (mod p)"
-    by (metis  number_of_is_id power2_eq_square succ_1 succ_Pls)
+    by (metis  number_of_is_id power2_eq_square succ_bin_simps)
   with prems show False
     by (simp add: QuadRes_def)
 qed
@@ -288,7 +288,7 @@
   apply (auto simp add: zpower_zpower) 
   apply (rule zcong_trans)
   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
-  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)
+  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)
   done
 
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Presburger.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -394,7 +394,8 @@
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   by (case_tac "y \<le> x", simp_all add: zdiff_int)
 
-lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
+lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
+by simp
 lemma number_of2: "(0::int) <= Numeral0" by simp
 lemma Suc_plus1: "Suc n = n + 1" by simp
 
@@ -503,12 +504,12 @@
   unfolding Pls_def Int.Min_def by presburger
 
 lemma eq_Pls_Bit0:
-  "Int.Pls = Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls = k"
-  unfolding Pls_def Bit_def bit.cases by presburger
+  "Int.Pls = Int.Bit0 k \<longleftrightarrow> Int.Pls = k"
+  unfolding Pls_def Bit0_def by presburger
 
 lemma eq_Pls_Bit1:
-  "Int.Pls = Int.Bit k bit.B1 \<longleftrightarrow> False"
-  unfolding Pls_def Bit_def bit.cases by presburger
+  "Int.Pls = Int.Bit1 k \<longleftrightarrow> False"
+  unfolding Pls_def Bit1_def by presburger
 
 lemma eq_Min_Pls:
   "Int.Min = Int.Pls \<longleftrightarrow> False"
@@ -518,43 +519,44 @@
   "Int.Min = Int.Min \<longleftrightarrow> True" by presburger
 
 lemma eq_Min_Bit0:
-  "Int.Min = Int.Bit k bit.B0 \<longleftrightarrow> False"
-  unfolding Int.Min_def Bit_def bit.cases by presburger
+  "Int.Min = Int.Bit0 k \<longleftrightarrow> False"
+  unfolding Int.Min_def Bit0_def by presburger
 
 lemma eq_Min_Bit1:
-  "Int.Min = Int.Bit k bit.B1 \<longleftrightarrow> Int.Min = k"
-  unfolding Int.Min_def Bit_def bit.cases by presburger
+  "Int.Min = Int.Bit1 k \<longleftrightarrow> Int.Min = k"
+  unfolding Int.Min_def Bit1_def by presburger
 
 lemma eq_Bit0_Pls:
-  "Int.Bit k bit.B0 = Int.Pls \<longleftrightarrow> Int.Pls = k"
-  unfolding Pls_def Bit_def bit.cases by presburger
+  "Int.Bit0 k = Int.Pls \<longleftrightarrow> Int.Pls = k"
+  unfolding Pls_def Bit0_def by presburger
 
 lemma eq_Bit1_Pls:
-  "Int.Bit k bit.B1 = Int.Pls \<longleftrightarrow> False"
-  unfolding Pls_def Bit_def bit.cases  by presburger
+  "Int.Bit1 k = Int.Pls \<longleftrightarrow> False"
+  unfolding Pls_def Bit1_def by presburger
 
 lemma eq_Bit0_Min:
-  "Int.Bit k bit.B0 = Int.Min \<longleftrightarrow> False"
-  unfolding Int.Min_def Bit_def bit.cases  by presburger
+  "Int.Bit0 k = Int.Min \<longleftrightarrow> False"
+  unfolding Int.Min_def Bit0_def by presburger
 
 lemma eq_Bit1_Min:
-  "(Int.Bit k bit.B1) = Int.Min \<longleftrightarrow> Int.Min = k"
-  unfolding Int.Min_def Bit_def bit.cases  by presburger
+  "Int.Bit1 k = Int.Min \<longleftrightarrow> Int.Min = k"
+  unfolding Int.Min_def Bit1_def by presburger
+
+lemma eq_Bit0_Bit0:
+  "Int.Bit0 k1 = Int.Bit0 k2 \<longleftrightarrow> k1 = k2"
+  unfolding Bit0_def by presburger
 
-lemma eq_Bit_Bit:
-  "Int.Bit k1 v1 = Int.Bit k2 v2 \<longleftrightarrow>
-    v1 = v2 \<and> k1 = k2" 
-  unfolding Bit_def
-  apply (cases v1)
-  apply (cases v2)
-  apply auto
-  apply presburger
-  apply (cases v2)
-  apply auto
-  apply presburger
-  apply (cases v2)
-  apply auto
-  done
+lemma eq_Bit0_Bit1:
+  "Int.Bit0 k1 = Int.Bit1 k2 \<longleftrightarrow> False"
+  unfolding Bit0_def Bit1_def by presburger
+
+lemma eq_Bit1_Bit0:
+  "Int.Bit1 k1 = Int.Bit0 k2 \<longleftrightarrow> False"
+  unfolding Bit0_def Bit1_def by presburger
+
+lemma eq_Bit1_Bit1:
+  "Int.Bit1 k1 = Int.Bit1 k2 \<longleftrightarrow> k1 = k2"
+  unfolding Bit1_def by presburger
 
 lemma eq_number_of:
   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
@@ -568,9 +570,13 @@
   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
   unfolding Pls_def Int.Min_def by presburger
 
-lemma less_eq_Pls_Bit:
-  "Int.Pls \<le> Int.Bit k v \<longleftrightarrow> Int.Pls \<le> k"
-  unfolding Pls_def Bit_def by (cases v) auto
+lemma less_eq_Pls_Bit0:
+  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
+  unfolding Pls_def Bit0_def by auto
+
+lemma less_eq_Pls_Bit1:
+  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
+  unfolding Pls_def Bit1_def by auto
 
 lemma less_eq_Min_Pls:
   "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
@@ -580,36 +586,44 @@
   "Int.Min \<le> Int.Min \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Min_Bit0:
-  "Int.Min \<le> Int.Bit k bit.B0 \<longleftrightarrow> Int.Min < k"
-  unfolding Int.Min_def Bit_def by auto
+  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
+  unfolding Int.Min_def Bit0_def by auto
 
 lemma less_eq_Min_Bit1:
-  "Int.Min \<le> Int.Bit k bit.B1 \<longleftrightarrow> Int.Min \<le> k"
-  unfolding Int.Min_def Bit_def by auto
+  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
+  unfolding Int.Min_def Bit1_def by auto
 
 lemma less_eq_Bit0_Pls:
-  "Int.Bit k bit.B0 \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
-  unfolding Pls_def Bit_def by simp
+  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
+  unfolding Pls_def Bit0_def by simp
 
 lemma less_eq_Bit1_Pls:
-  "Int.Bit k bit.B1 \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
-  unfolding Pls_def Bit_def by auto
+  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
+  unfolding Pls_def Bit1_def by auto
 
-lemma less_eq_Bit_Min:
-  "Int.Bit k v \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
-  unfolding Int.Min_def Bit_def by (cases v) auto
+lemma less_eq_Bit0_Min:
+  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+  unfolding Int.Min_def Bit0_def by auto
 
-lemma less_eq_Bit0_Bit:
-  "Int.Bit k1 bit.B0 \<le> Int.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit_def bit.cases by (cases v) auto
+lemma less_eq_Bit1_Min:
+  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+  unfolding Int.Min_def Bit1_def by auto
 
-lemma less_eq_Bit_Bit1:
-  "Int.Bit k1 v \<le> Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit_def bit.cases by (cases v) auto
+lemma less_eq_Bit0_Bit0:
+  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
+  unfolding Bit0_def by auto
+
+lemma less_eq_Bit0_Bit1:
+  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+  unfolding Bit0_def Bit1_def by auto
 
 lemma less_eq_Bit1_Bit0:
-  "Int.Bit k1 bit.B1 \<le> Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
-  unfolding Bit_def by (auto split: bit.split)
+  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+  unfolding Bit0_def Bit1_def by auto
+
+lemma less_eq_Bit1_Bit1:
+  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+  unfolding Bit1_def by auto
 
 lemma less_eq_number_of:
   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
@@ -624,12 +638,12 @@
   unfolding Pls_def Int.Min_def  by presburger 
 
 lemma less_Pls_Bit0:
-  "Int.Pls < Int.Bit k bit.B0 \<longleftrightarrow> Int.Pls < k"
-  unfolding Pls_def Bit_def by auto
+  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
+  unfolding Pls_def Bit0_def by auto
 
 lemma less_Pls_Bit1:
-  "Int.Pls < Int.Bit k bit.B1 \<longleftrightarrow> Int.Pls \<le> k"
-  unfolding Pls_def Bit_def by auto
+  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
+  unfolding Pls_def Bit1_def by auto
 
 lemma less_Min_Pls:
   "Int.Min < Int.Pls \<longleftrightarrow> True"
@@ -638,33 +652,45 @@
 lemma less_Min_Min:
   "Int.Min < Int.Min \<longleftrightarrow> False"  by simp
 
-lemma less_Min_Bit:
-  "Int.Min < Int.Bit k v \<longleftrightarrow> Int.Min < k"
-  unfolding Int.Min_def Bit_def by (auto split: bit.split)
+lemma less_Min_Bit0:
+  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
+  unfolding Int.Min_def Bit0_def by auto
+
+lemma less_Min_Bit1:
+  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
+  unfolding Int.Min_def Bit1_def by auto
 
-lemma less_Bit_Pls:
-  "Int.Bit k v < Int.Pls \<longleftrightarrow> k < Int.Pls"
-  unfolding Pls_def Bit_def by (auto split: bit.split)
+lemma less_Bit0_Pls:
+  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
+  unfolding Pls_def Bit0_def by auto
+
+lemma less_Bit1_Pls:
+  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
+  unfolding Pls_def Bit1_def by auto
 
 lemma less_Bit0_Min:
-  "Int.Bit k bit.B0 < Int.Min \<longleftrightarrow> k \<le> Int.Min"
-  unfolding Int.Min_def Bit_def by auto
+  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
+  unfolding Int.Min_def Bit0_def by auto
 
 lemma less_Bit1_Min:
-  "Int.Bit k bit.B1 < Int.Min \<longleftrightarrow> k < Int.Min"
-  unfolding Int.Min_def Bit_def by auto
+  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
+  unfolding Int.Min_def Bit1_def by auto
 
-lemma less_Bit_Bit0:
-  "Int.Bit k1 v < Int.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
-  unfolding Bit_def by (auto split: bit.split)
-
-lemma less_Bit1_Bit:
-  "Int.Bit k1 bit.B1 < Int.Bit k2 v \<longleftrightarrow> k1 < k2"
-  unfolding Bit_def by (auto split: bit.split)
+lemma less_Bit0_Bit0:
+  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+  unfolding Bit0_def by auto
 
 lemma less_Bit0_Bit1:
-  "Int.Bit k1 bit.B0 < Int.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit_def bit.cases  by arith
+  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+  unfolding Bit0_def Bit1_def by auto
+
+lemma less_Bit1_Bit0:
+  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+  unfolding Bit0_def Bit1_def by auto
+
+lemma less_Bit1_Bit1:
+  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
+  unfolding Bit1_def by auto
 
 lemma less_number_of:
   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
@@ -689,17 +715,22 @@
 lemmas eq_numeral_code [code func] =
   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
-  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min
+  eq_Bit0_Bit0 eq_Bit0_Bit1 eq_Bit1_Bit0 eq_Bit1_Bit1
   eq_number_of
 
-lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
+lemmas less_eq_numeral_code [code func] =
+  less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit0 less_eq_Pls_Bit1
   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
-  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
+  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit0_Min less_eq_Bit1_Min
+  less_eq_Bit0_Bit0 less_eq_Bit0_Bit1 less_eq_Bit1_Bit0 less_eq_Bit1_Bit1
   less_eq_number_of
 
-lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
-  less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
-  less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
+lemmas less_numeral_code [code func] =
+  less_Pls_Pls less_Pls_Min less_Pls_Bit0 less_Pls_Bit1
+  less_Min_Pls less_Min_Min less_Min_Bit0 less_Min_Bit1
+  less_Bit0_Pls less_Bit1_Pls less_Bit0_Min less_Bit1_Min
+  less_Bit0_Bit0 less_Bit0_Bit1 less_Bit1_Bit0 less_Bit1_Bit1
   less_number_of
 
 context ring_1
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Real/Float.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -518,10 +518,10 @@
 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
   by simp
 
-lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
+lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)"
   by simp
 
-lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
+lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)"
   by simp
 
 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
@@ -533,7 +533,10 @@
 lemma int_neg_number_of_Min: "neg (-1::int)"
   by simp
 
-lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
+lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)"
+  by simp
+
+lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)"
   by simp
 
 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
@@ -541,9 +544,9 @@
 
 lemmas intarithrel =
   int_eq_number_of_eq
-  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
-  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]
-  int_neg_number_of_BIT int_le_number_of_eq
+  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0
+  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]
+  int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq
 
 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   by simp
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Tools/ComputeNumeral.thy
--- a/src/HOL/Tools/ComputeNumeral.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -8,15 +8,15 @@
 (* neg for bit strings *)
 lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
 lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
-lemma neg3: "neg (x BIT Int.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
-lemma neg4: "neg (x BIT Int.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto  
+lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto
+lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto  
 lemmas bitneg = neg1 neg2 neg3 neg4
 
 (* iszero for bit strings *)
 lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
 lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
-lemma iszero3: "iszero (x BIT Int.B0) = iszero x" apply (subst Int.Bit_def) apply (subst iszero_def)+ by auto
-lemma iszero4: "iszero (x BIT Int.B1) = False" apply (subst Int.Bit_def) apply (subst iszero_def)+  apply simp by arith
+lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto
+lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+  apply simp by arith
 lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
 
 (* lezero for bit strings *)
@@ -24,66 +24,66 @@
   "lezero x == (x \<le> 0)"
 lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
 lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
-lemma lezero3: "lezero (x BIT Int.B0) = lezero x" unfolding Int.Bit_def lezero_def by auto
-lemma lezero4: "lezero (x BIT Int.B1) = neg x" unfolding Int.Bit_def lezero_def neg_def by auto
+lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
+lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto
 lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
 
 (* equality for bit strings *)
-lemma biteq1: "(Int.Pls = Int.Pls) = True" by auto
-lemma biteq2: "(Int.Min = Int.Min) = True" by auto
-lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def by auto
-lemma biteq5: "(x BIT Int.B0 = y BIT Int.B0) = (x = y)" unfolding Bit_def by auto
-lemma biteq6: "(x BIT Int.B1 = y BIT Int.B1) = (x = y)" unfolding Bit_def by auto
-lemma biteq7: "(x BIT Int.B0 = y BIT Int.B1) = False" unfolding Bit_def by (simp, arith) 
-lemma biteq8: "(x BIT Int.B1 = y BIT Int.B0) = False" unfolding Bit_def by (simp, arith)
-lemma biteq9: "(Int.Pls = x BIT Int.B0) = (Int.Pls = x)" unfolding Bit_def Pls_def by auto
-lemma biteq10: "(Int.Pls = x BIT Int.B1) = False" unfolding Bit_def Pls_def by (simp, arith) 
-lemma biteq11: "(Int.Min = x BIT Int.B0) = False" unfolding Bit_def Min_def by (simp, arith)
-lemma biteq12: "(Int.Min = x BIT Int.B1) = (Int.Min = x)" unfolding Bit_def Min_def by auto
-lemma biteq13: "(x BIT Int.B0 = Int.Pls) = (x = Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma biteq14: "(x BIT Int.B1 = Int.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
-lemma biteq15: "(x BIT Int.B0 = Int.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
-lemma biteq16: "(x BIT Int.B1 = Int.Min) = (x = Int.Min)" unfolding Bit_def Min_def by (simp, arith)
+lemma biteq1: "(Int.Pls = Int.Pls) = True" by (rule eq_Pls_Pls)
+lemma biteq2: "(Int.Min = Int.Min) = True" by (rule eq_Min_Min)
+lemma biteq3: "(Int.Pls = Int.Min) = False" by (rule eq_Pls_Min)
+lemma biteq4: "(Int.Min = Int.Pls) = False" by (rule eq_Min_Pls)
+lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" by (rule eq_Bit0_Bit0)
+lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" by (rule eq_Bit1_Bit1)
+lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" by (rule eq_Bit0_Bit1)
+lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" by (rule eq_Bit1_Bit0)
+lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" by (rule eq_Pls_Bit0)
+lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" by (rule eq_Pls_Bit1)
+lemma biteq11: "(Int.Min = Int.Bit0 x) = False" by (rule eq_Min_Bit0)
+lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" by (rule eq_Min_Bit1)
+lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" by (subst eq_Bit0_Pls) auto
+lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" by (rule eq_Bit1_Pls)
+lemma biteq15: "(Int.Bit0 x = Int.Min) = False" by (rule eq_Bit0_Min)
+lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" by (subst eq_Bit1_Min) auto
 lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
 
 (* x < y for bit strings *)
-lemma bitless1: "(Int.Pls < Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitless2: "(Int.Pls < Int.Pls) = False" by auto
-lemma bitless3: "(Int.Min < Int.Pls) = True" unfolding Pls_def Min_def by auto
-lemma bitless4: "(Int.Min < Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitless5: "(x BIT Int.B0 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitless6: "(x BIT Int.B1 < y BIT Int.B1) = (x < y)" unfolding Bit_def by auto
-lemma bitless7: "(x BIT Int.B0 < y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitless8: "(x BIT Int.B1 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitless9: "(Int.Pls < x BIT Int.B0) = (Int.Pls < x)" unfolding Bit_def Pls_def by auto
-lemma bitless10: "(Int.Pls < x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitless11: "(Int.Min < x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitless12: "(Int.Min < x BIT Int.B1) = (Int.Min < x)" unfolding Bit_def Min_def by auto
-lemma bitless13: "(x BIT Int.B0 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitless14: "(x BIT Int.B1 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitless15: "(x BIT Int.B0 < Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitless16: "(x BIT Int.B1 < Int.Min) = (x < Int.Min)" unfolding Bit_def Min_def by auto
+lemma bitless1: "(Int.Pls < Int.Min) = False" by (rule less_Pls_Min)
+lemma bitless2: "(Int.Pls < Int.Pls) = False" by (rule less_Pls_Pls)
+lemma bitless3: "(Int.Min < Int.Pls) = True" by (rule less_Min_Pls)
+lemma bitless4: "(Int.Min < Int.Min) = False" by (rule less_Min_Min)
+lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (rule less_Bit0_Bit0)
+lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (rule less_Bit1_Bit1)
+lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \<le> y)" by (rule less_Bit0_Bit1)
+lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (rule less_Bit1_Bit0)
+lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (rule less_Pls_Bit0)
+lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_Pls_Bit1)
+lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (rule less_Min_Bit1)
+lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit0_Pls)
+lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit1_Pls)
+lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (rule less_Bit1_Min)
 lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8 
                  bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
 
 (* x \<le> y for bit strings *)
-lemma bitle1: "(Int.Pls \<le> Int.Min) = False" unfolding Pls_def Min_def by auto
-lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by auto
-lemma bitle3: "(Int.Min \<le> Int.Pls) = True" unfolding Pls_def Min_def by auto
-lemma bitle4: "(Int.Min \<le> Int.Min) = True" unfolding Pls_def Min_def by auto
-lemma bitle5: "(x BIT Int.B0 \<le> y BIT Int.B0) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle6: "(x BIT Int.B1 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle7: "(x BIT Int.B0 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
-lemma bitle8: "(x BIT Int.B1 \<le> y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
-lemma bitle9: "(Int.Pls \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitle10: "(Int.Pls \<le> x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
-lemma bitle11: "(Int.Min \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitle12: "(Int.Min \<le> x BIT Int.B1) = (Int.Min \<le> x)" unfolding Bit_def Min_def by auto
-lemma bitle13: "(x BIT Int.B0 \<le> Int.Pls) = (x \<le> Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitle14: "(x BIT Int.B1 \<le> Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
-lemma bitle15: "(x BIT Int.B0 \<le> Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
-lemma bitle16: "(x BIT Int.B1 \<le> Int.Min) = (x \<le> Int.Min)" unfolding Bit_def Min_def by auto
+lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (rule less_eq_Pls_Min)
+lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (rule less_eq_Pls_Pls)
+lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (rule less_eq_Min_Pls)
+lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (rule less_eq_Min_Min)
+lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit0)
+lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit1_Bit1)
+lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit1)
+lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (rule less_eq_Bit1_Bit0)
+lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit0)
+lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit1)
+lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (rule less_eq_Min_Bit1)
+lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (rule less_eq_Bit0_Pls)
+lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (rule less_eq_Bit1_Pls)
+lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
+lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> Int.Min)" by (rule less_eq_Bit1_Min)
 lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8 
                  bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
 
@@ -97,15 +97,15 @@
 lemmas bituminus = minus_bin_simps
 
 (* addition for bit strings *)
-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"]
+lemmas bitadd = add_bin_simps
 
 (* multiplication for bit strings *) 
 lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
 lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
-lemma multb0x: "(x BIT Int.B0) * y = (x * y) BIT Int.B0" unfolding Bit_def by simp
-lemma multxb0: "x * (y BIT Int.B0) = (x * y) BIT Int.B0" unfolding Bit_def by simp
-lemma multb1: "(x BIT Int.B1) * (y BIT Int.B1) = (((x * y) BIT Int.B0) + x + y) BIT Int.B1"
-  unfolding Bit_def by (simp add: ring_simps)
+lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
+lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
+lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"
+  unfolding Bit0_def Bit1_def by (simp add: ring_simps)
 lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
 
 lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
@@ -121,7 +121,7 @@
 
 (* Normalization of nat literals *)
 lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
-lemma natnorm1: "(1 :: nat) = number_of (Int.Pls BIT Int.B1)"  by auto 
+lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)"  by auto 
 lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
 
 (* Suc *)
@@ -228,12 +228,12 @@
   apply (unfold Min_def even_def)
   by simp
 
-lemma even_B0: "even (x BIT Int.B0) = True"
-  apply (unfold Bit_def)
+lemma even_B0: "even (Int.Bit0 x) = True"
+  apply (unfold Bit0_def)
   by simp
 
-lemma even_B1: "even (x BIT Int.B1) = False"
-  apply (unfold Bit_def)
+lemma even_B1: "even (Int.Bit1 x) = False"
+  apply (unfold Bit1_def)
   by simp
 
 lemma even_number_of: "even ((number_of w)::int) = even w"
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -24,7 +24,7 @@
    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
-   @{term "Int.Bit"},
+   @{term "Int.Bit0"}, @{term "Int.Bit1"},
    @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
@@ -38,8 +38,8 @@
    @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
    @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
    @{term "nat"}, @{term "int"},
-   @{term "Int.bit.B0"},@{term "Int.bit.B1"}, 
-   @{term "Int.Bit"}, @{term "Int.Pls"}, @{term "Int.Min"},
+   @{term "Int.Bit0"}, @{term "Int.Bit1"},
+   @{term "Int.Pls"}, @{term "Int.Min"},
    @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
    @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    @{term "True"}, @{term "False"}];
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/numeral.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -17,15 +17,15 @@
 
 (* numeral *)
 
-fun mk_cbit 0 = @{cterm "Int.bit.B0"}
-  | mk_cbit 1 = @{cterm "Int.bit.B1"}
+fun mk_cbit 0 = @{cterm "Int.Bit0"}
+  | mk_cbit 1 = @{cterm "Int.Bit1"}
   | mk_cbit _ = raise CTERM ("mk_cbit", []);
 
 fun mk_cnumeral 0 = @{cterm "Int.Pls"}
   | mk_cnumeral ~1 = @{cterm "Int.Min"}
   | mk_cnumeral i =
       let val (q, r) = Integer.div_mod i 2 in
-        Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r)
+        Thm.capply (mk_cbit r) (mk_cnumeral q)
       end;
 
 
@@ -57,8 +57,7 @@
 
 fun add_code number_of negative unbounded target =
   CodeTarget.add_pretty_numeral target negative unbounded number_of
-  @{const_name Int.B0} @{const_name Int.B1}
   @{const_name Int.Pls} @{const_name Int.Min}
-  @{const_name Int.Bit};
+  @{const_name Int.Bit0} @{const_name Int.Bit1};
 
 end;
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -20,7 +20,7 @@
 fun mk_bin num =
   let
     val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
-    fun bit b bs = Syntax.const @{const_name Int.Bit} $ bs $ HOLogic.mk_bit b;
+    fun bit b bs = HOLogic.mk_bit b $ bs;
     fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
       | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
       | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
@@ -39,15 +39,10 @@
 
 local
 
-fun dest_bit (Const (@{const_syntax Int.bit.B0}, _)) = 0
-  | dest_bit (Const (@{const_syntax Int.bit.B1}, _)) = 1
-  | dest_bit (Const ("bit.B0", _)) = 0
-  | dest_bit (Const ("bit.B1", _)) = 1
-  | dest_bit _ = raise Match;
-
 fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
   | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
-  | dest_bin (Const (@{const_syntax "Int.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
+  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
+  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
   | dest_bin _ = raise Match;
 
 fun leading _ [] = 0
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BinBoolList.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -75,24 +75,30 @@
   "(butlast ^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)
 
-lemma bin_to_bl_aux_Pls_minus_simp:
+lemma bin_to_bl_aux_Pls_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
     bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
   by (cases n) auto
 
-lemma bin_to_bl_aux_Min_minus_simp:
+lemma bin_to_bl_aux_Min_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n Int.Min bl = 
     bin_to_bl_aux (n - 1) Int.Min (True # bl)"
   by (cases n) auto
 
-lemma bin_to_bl_aux_Bit_minus_simp:
+lemma bin_to_bl_aux_Bit_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
     bin_to_bl_aux (n - 1) w ((b = bit.B1) # bl)"
   by (cases n) auto
 
-declare bin_to_bl_aux_Pls_minus_simp [simp]
-  bin_to_bl_aux_Min_minus_simp [simp]
-  bin_to_bl_aux_Bit_minus_simp [simp]
+lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
+  "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl = 
+    bin_to_bl_aux (n - 1) w (False # bl)"
+  by (cases n) auto
+
+lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
+  "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl = 
+    bin_to_bl_aux (n - 1) w (True # bl)"
+  by (cases n) auto
 
 (** link between bin and bool list **)
 
@@ -308,7 +314,7 @@
   apply clarsimp
   apply safe
    apply (erule allE, erule xtr8 [rotated],
-          simp add: Bit_def ring_simps cong add : number_of_False_cong)+
+          simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   done
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
@@ -326,7 +332,7 @@
   apply clarsimp
   apply safe
    apply (erule allE, erule less_eq_less.order_trans [rotated],
-          simp add: Bit_def ring_simps cong add : number_of_False_cong)+
+          simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   done
 
 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
@@ -370,13 +376,13 @@
    apply (case_tac "m - size list")
     apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
    apply simp
-   apply (rule_tac f = "%nat. bl_to_bin_aux (bintrunc nat w BIT bit.B1) list" 
+   apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit1 (bintrunc nat w)) list" 
                    in arg_cong) 
    apply simp
   apply (case_tac "m - size list")
    apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
   apply simp
-  apply (rule_tac f = "%nat. bl_to_bin_aux (bintrunc nat w BIT bit.B0) list" 
+  apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit0 (bintrunc nat w)) list" 
                   in arg_cong) 
   apply simp
   done
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BinGeneral.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -49,21 +49,37 @@
    apply (auto intro: bin_rec'.simps [THEN trans])
   done
 
-lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]
-lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
+lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
+  unfolding bin_rec_def by simp
+
+lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
+  unfolding bin_rec_def by simp
+
+lemma bin_rec_Bit0:
+  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
+    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
+  apply (unfold bin_rec_def)
+  apply (rule bin_rec'.simps [THEN trans])
+  apply (fold bin_rec_def)
+  apply (simp add: eq_Bit0_Pls eq_Bit0_Min bin_rec_Pls)
+  done
+
+lemma bin_rec_Bit1:
+  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
+    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
+  apply (unfold bin_rec_def)
+  apply (rule bin_rec'.simps [THEN trans])
+  apply (fold bin_rec_def)
+  apply (simp add: eq_Bit1_Pls eq_Bit1_Min bin_rec_Min)
+  done
 
 lemma bin_rec_Bit:
   "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
     f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
-  apply clarify
-  apply (unfold bin_rec_def)
-  apply (rule bin_rec'.simps [THEN trans])
-  apply auto
-       apply (unfold Pls_def Min_def Bit_def)
-       apply (cases b, auto)+
-  done
+  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
 
 lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
+  bin_rec_Bit0 bin_rec_Bit1
 
 subsection {* Destructors for binary integers *}
 
@@ -92,18 +108,24 @@
   "bin_rest Int.Pls = Int.Pls"
   "bin_rest Int.Min = Int.Min"
   "bin_rest (w BIT b) = w"
+  "bin_rest (Int.Bit0 w) = w"
+  "bin_rest (Int.Bit1 w) = w"
   unfolding bin_rest_def by auto
 
 lemma bin_last_simps [simp]: 
   "bin_last Int.Pls = bit.B0"
   "bin_last Int.Min = bit.B1"
   "bin_last (w BIT b) = b"
+  "bin_last (Int.Bit0 w) = bit.B0"
+  "bin_last (Int.Bit1 w) = bit.B1"
   unfolding bin_last_def by auto
-    
+
 lemma bin_sign_simps [simp]:
   "bin_sign Int.Pls = Int.Pls"
   "bin_sign Int.Min = Int.Min"
   "bin_sign (w BIT b) = bin_sign w"
+  "bin_sign (Int.Bit0 w) = bin_sign w"
+  "bin_sign (Int.Bit1 w) = bin_sign w"
   unfolding bin_sign_def by (auto simp: bin_rec_simps)
 
 lemma bin_r_l_extras [simp]:
@@ -142,6 +164,12 @@
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   unfolding bin_rest_div [symmetric] by auto
 
+lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
+  using Bit_div2 [where b=bit.B0] by simp
+
+lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
+  using Bit_div2 [where b=bit.B1] by simp
+
 lemma bin_nth_lem [rule_format]:
   "ALL y. bin_nth x = bin_nth y --> x = y"
   apply (induct x rule: bin_induct)
@@ -191,11 +219,20 @@
 lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
   by (cases n) auto
 
+lemma bin_nth_minus_Bit0 [simp]:
+  "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
+  using bin_nth_minus [where b=bit.B0] by simp
+
+lemma bin_nth_minus_Bit1 [simp]:
+  "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
+  using bin_nth_minus [where b=bit.B1] by simp
+
 lemmas bin_nth_0 = bin_nth.simps(1)
 lemmas bin_nth_Suc = bin_nth.simps(2)
 
 lemmas bin_nth_simps = 
   bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
+  bin_nth_minus_Bit0 bin_nth_minus_Bit1
 
 lemma bin_sign_rest [simp]: 
   "bin_sign (bin_rest w) = (bin_sign w)"
@@ -277,6 +314,14 @@
   "bin_nth (w BIT b) n = (n = 0 & b = bit.B1 | (EX m. n = Suc m & bin_nth w m))"
   by (cases n) auto
 
+lemma bin_nth_Bit0:
+  "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
+  using bin_nth_Bit [where b=bit.B0] by simp
+
+lemma bin_nth_Bit1:
+  "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
+  using bin_nth_Bit [where b=bit.B1] by simp
+
 lemma bintrunc_bintrunc_l:
   "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
   by (rule bin_eqI) (auto simp add : nth_bintr)
@@ -312,7 +357,16 @@
 lemmas bintrunc_BIT  [simp] = 
   bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
 
+lemma bintrunc_Bit0 [simp]:
+  "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
+  using bintrunc_BIT [where b=bit.B0] by simp
+
+lemma bintrunc_Bit1 [simp]:
+  "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
+  using bintrunc_BIT [where b=bit.B1] by simp
+
 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
+  bintrunc_Bit0 bintrunc_Bit1
 
 lemmas sbintrunc_Suc_Pls = 
   sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
@@ -323,7 +377,16 @@
 lemmas sbintrunc_Suc_BIT [simp] = 
   sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
 
+lemma sbintrunc_Suc_Bit0 [simp]:
+  "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
+  using sbintrunc_Suc_BIT [where b=bit.B0] by simp
+
+lemma sbintrunc_Suc_Bit1 [simp]:
+  "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
+  using sbintrunc_Suc_BIT [where b=bit.B1] by simp
+
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
+  sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
 
 lemmas sbintrunc_Pls = 
   sbintrunc.Z [where bin="Int.Pls", 
@@ -341,8 +404,15 @@
   sbintrunc.Z [where bin="w BIT bit.B1", 
                simplified bin_last_simps bin_rest_simps bit.simps, standard]
 
+lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
+  using sbintrunc_0_BIT_B0 by simp
+
+lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
+  using sbintrunc_0_BIT_B1 by simp
+
 lemmas sbintrunc_0_simps =
   sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
+  sbintrunc_0_Bit0 sbintrunc_0_Bit1
 
 lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
 lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
@@ -374,7 +444,7 @@
 lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
 lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
 
-lemmas bmsts = bintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
+lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
 lemmas bintrunc_Pls_minus_I = bmsts(1)
 lemmas bintrunc_Min_minus_I = bmsts(2)
 lemmas bintrunc_BIT_minus_I = bmsts(3)
@@ -394,10 +464,10 @@
 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
 
 lemmas sbintrunc_Suc_Is = 
-  sbintrunc_Sucs [THEN thobini1 [THEN [2] trans], standard]
+  sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard]
 
 lemmas sbintrunc_Suc_minus_Is = 
-  sbintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
+  sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
 
 lemma sbintrunc_Suc_lem:
   "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
@@ -573,11 +643,11 @@
 
 lemma sign_Pls_ge_0: 
   "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
-  by (induct bin rule: bin_induct) auto
+  by (induct bin rule: numeral_induct) auto
 
 lemma sign_Min_lt_0: 
   "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
-  by (induct bin rule: bin_induct) auto
+  by (induct bin rule: numeral_induct) auto
 
 lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
 
@@ -725,5 +795,4 @@
 
 lemmas s2n_ths = n2s_ths [symmetric]
 
-
 end
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BinOperations.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -44,7 +44,9 @@
   "NOT Int.Pls = Int.Min"
   "NOT Int.Min = Int.Pls"
   "NOT (w BIT b) = (NOT w) BIT (NOT b)"
-  by (unfold int_not_def) (auto intro: bin_rec_simps)
+  "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
+  "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
+  unfolding int_not_def by (simp_all add: bin_rec_simps)
 
 lemma int_xor_Pls [simp]: 
   "Int.Pls XOR x = x"
@@ -65,6 +67,13 @@
   apply (simp add: int_not_simps [symmetric])
   done
 
+lemma int_xor_Bits2 [simp]: 
+  "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
+  "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
+  "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
+  "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
+  unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
+
 lemma int_xor_x_simps':
   "w XOR (Int.Pls BIT bit.B0) = w"
   "w XOR (Int.Min BIT bit.B1) = NOT w"
@@ -74,7 +83,10 @@
    apply clarsimp+
   done
 
-lemmas int_xor_extra_simps [simp] = int_xor_x_simps' [simplified arith_simps]
+lemma int_xor_extra_simps [simp]:
+  "w XOR Int.Pls = w"
+  "w XOR Int.Min = NOT w"
+  using int_xor_x_simps' by simp_all
 
 lemma int_or_Pls [simp]: 
   "Int.Pls OR x = x"
@@ -88,6 +100,13 @@
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
   unfolding int_or_def by (simp add: bin_rec_simps)
 
+lemma int_or_Bits2 [simp]: 
+  "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
+  "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+  "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
+  "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+  unfolding BIT_simps [symmetric] int_or_Bits by simp_all
+
 lemma int_or_x_simps': 
   "w OR (Int.Pls BIT bit.B0) = w"
   "w OR (Int.Min BIT bit.B1) = Int.Min"
@@ -97,8 +116,10 @@
    apply clarsimp+
   done
 
-lemmas int_or_extra_simps [simp] = int_or_x_simps' [simplified arith_simps]
-
+lemma int_or_extra_simps [simp]:
+  "w OR Int.Pls = w"
+  "w OR Int.Min = Int.Min"
+  using int_or_x_simps' by simp_all
 
 lemma int_and_Pls [simp]:
   "Int.Pls AND x = Int.Pls"
@@ -112,6 +133,13 @@
   "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
   unfolding int_and_def by (simp add: bin_rec_simps)
 
+lemma int_and_Bits2 [simp]: 
+  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
+  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
+
 lemma int_and_x_simps': 
   "w AND (Int.Pls BIT bit.B0) = Int.Pls"
   "w AND (Int.Min BIT bit.B1) = w"
@@ -121,7 +149,10 @@
    apply clarsimp+
   done
 
-lemmas int_and_extra_simps [simp] = int_and_x_simps' [simplified arith_simps]
+lemma int_and_extra_simps [simp]:
+  "w AND Int.Pls = Int.Pls"
+  "w AND Int.Min = w"
+  using int_and_x_simps' by simp_all
 
 (* commutativity of the above *)
 lemma bin_ops_comm:
@@ -194,7 +225,7 @@
     apply (case_tac [!] z rule: bin_exhaust)
     apply (case_tac [!] bit)
        apply (case_tac [!] b)
-             apply auto
+             apply (auto simp del: BIT_simps)
   done
 
 lemma int_and_assoc:
@@ -225,7 +256,7 @@
   apply (induct x rule: bin_induct)
        apply auto
    apply (case_tac [!] y rule: bin_exhaust)
-   apply (case_tac [!] bit, auto)
+   apply (case_tac [!] bit, auto simp del: BIT_simps)
   done
 
 lemma bbw_oa_dist: 
@@ -235,7 +266,7 @@
     apply auto
   apply (case_tac y rule: bin_exhaust)
   apply (case_tac z rule: bin_exhaust)
-  apply (case_tac ba, auto)
+  apply (case_tac ba, auto simp del: BIT_simps)
   done
 
 lemma bbw_ao_dist: 
@@ -245,7 +276,7 @@
     apply auto
   apply (case_tac y rule: bin_exhaust)
   apply (case_tac z rule: bin_exhaust)
-  apply (case_tac ba, auto)
+  apply (case_tac ba, auto simp del: BIT_simps)
   done
 
 (*
@@ -289,9 +320,9 @@
   apply (induct n)
          apply safe
                          apply (case_tac [!] x rule: bin_exhaust)
-                         apply simp_all
+                         apply (simp_all del: BIT_simps)
                       apply (case_tac [!] y rule: bin_exhaust)
-                      apply simp_all
+                      apply (simp_all del: BIT_simps)
         apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
   done
 
@@ -392,7 +423,7 @@
   "!!w. bin_sc n bit.B0 w <= w"
   apply (induct n) 
    apply (case_tac [!] w rule: bin_exhaust)
-   apply auto
+   apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
    apply (simp_all split: bit.split)
   done
@@ -401,7 +432,7 @@
   "!!w. bin_sc n bit.B1 w >= w"
   apply (induct n) 
    apply (case_tac [!] w rule: bin_exhaust)
-   apply auto
+   apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
    apply (simp_all split: bit.split)
   done
@@ -412,7 +443,7 @@
    apply simp
   apply (case_tac w rule: bin_exhaust)
   apply (case_tac m)
-   apply auto
+   apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
    apply (simp_all split: bit.split)
   done
@@ -423,7 +454,7 @@
    apply simp
   apply (case_tac w rule: bin_exhaust)
   apply (case_tac m)
-   apply auto
+   apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
    apply (simp_all split: bit.split)
   done
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/BitSyntax.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -9,7 +9,7 @@
 header {* Syntactic class for bitwise operations *}
 
 theory BitSyntax
-imports Main
+imports Main Num_Lemmas
 begin
 
 class bit = type +
@@ -43,7 +43,7 @@
   shiftr   :: "'a::bit \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
 
 
-subsection {* Bitwise operations on type @{typ bit} *}
+subsection {* Bitwise operations on @{typ bit} *}
 
 instantiation bit :: bit
 begin
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -92,7 +92,7 @@
 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
 
 lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" 
-  by (auto simp add: bin_nth_Bit)
+  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
 
 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
 lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -9,6 +9,22 @@
 imports Main Parity
 begin
 
+datatype bit = B0 | B1
+
+definition
+  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+
+lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
+  unfolding Bit_def Bit0_def by simp
+
+lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
+  unfolding Bit_def Bit1_def by simp
+
+lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
+
+hide (open) const B0 B1
+
 lemma contentsI: "y = {x} ==> contents y = x" 
   unfolding contents_def by auto
 
@@ -197,8 +213,13 @@
    apply auto
   done
 
-lemmas bin_rl_simps [THEN bin_rl_char [THEN iffD2], standard, simp] =
-  Pls_0_eq Min_1_eq refl 
+lemma bin_rl_simps [simp]:
+  "bin_rl Int.Pls = (Int.Pls, bit.B0)"
+  "bin_rl Int.Min = (Int.Min, bit.B1)"
+  "bin_rl (r BIT b) = (r, b)"
+  "bin_rl (Int.Bit0 r) = (r, bit.B0)"
+  "bin_rl (Int.Bit1 r) = (r, bit.B1)"
+  unfolding bin_rl_char by simp_all
 
 lemma bin_abs_lem:
   "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
@@ -223,6 +244,24 @@
   apply (auto simp add : PPls PMin PBit)
   done
 
+lemma numeral_induct:
+  assumes Pls: "P Int.Pls"
+  assumes Min: "P Int.Min"
+  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
+  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
+  shows "P x"
+  apply (induct x rule: bin_induct)
+    apply (rule Pls)
+   apply (rule Min)
+  apply (case_tac bit)
+   apply (case_tac "bin = Int.Pls")
+    apply simp
+   apply (simp add: Bit0)
+  apply (case_tac "bin = Int.Min")
+   apply simp
+  apply (simp add: Bit1)
+  done
+
 lemma no_no [simp]: "number_of (number_of i) = i"
   unfolding number_of_eq by simp
 
@@ -245,9 +284,12 @@
   apply (simp (no_asm) only: Bit_B0 Bit_B1)
   apply (simp add: z1pmod2)
   done
-    
-lemmas B1_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct1, standard]
-lemmas B0_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct2, standard]
+
+lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
+  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
+
+lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
+  unfolding numeral_simps number_of_is_id by simp
 
 lemma axxbyy:
   "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>  
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/WordArith.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -395,7 +395,7 @@
 
 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
   unfolding word_arith_wis
-  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc eq_Bit0_Bit1)
 
 lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/WordMain.thy
--- a/src/HOL/Word/WordMain.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/WordMain.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -10,7 +10,7 @@
 theory WordMain imports WordGenLib
 begin
 
-lemmas word_no_1 [simp] = word_1_no [symmetric]
+lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
 lemmas word_no_0 [simp] = word_0_no [symmetric]
 
 declare word_0_bl [simp]
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Word/WordShift.thy	Sun Feb 17 06:49:53 2008 +0100
@@ -14,7 +14,8 @@
 lemma shiftl1_number [simp] :
   "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
   apply (unfold shiftl1_def word_number_of_def)
-  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
+  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
+              del: BIT_simps)
   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
   apply (subst bintrunc_bintrunc_min)
   apply simp
@@ -331,13 +332,13 @@
 
 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
   apply (simp add: shiftl1_def_u)
-  apply (simp only:  double_number_of_BIT [symmetric])
+  apply (simp only:  double_number_of_Bit0 [symmetric])
   apply simp
   done
 
 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
   apply (simp add: shiftl1_def_u)
-  apply (simp only: double_number_of_BIT [symmetric])
+  apply (simp only: double_number_of_Bit0 [symmetric])
   apply simp
   done
 
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/hologic.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -88,15 +88,13 @@
   val class_size: string
   val size_const: typ -> term
   val indexT: typ
-  val bitT: typ
-  val B0_const: term
-  val B1_const: term
-  val mk_bit: int -> term
-  val dest_bit: term -> int
   val intT: typ
   val pls_const: term
   val min_const: term
-  val bit_const: term
+  val bit0_const: term
+  val bit1_const: term
+  val mk_bit: int -> term
+  val dest_bit: term -> int
   val mk_numeral: int -> term
   val dest_numeral: term -> int
   val number_of_const: typ -> term
@@ -452,39 +450,33 @@
 val indexT = Type ("Code_Index.index", []);
 
 
-(* bit *)
-
-val bitT = Type ("Int.bit", []);
-
-val B0_const = Const ("Int.bit.B0", bitT);
-val B1_const =  Const ("Int.bit.B1", bitT);
-
-fun mk_bit 0 = B0_const
-  | mk_bit 1 = B1_const
-  | mk_bit _ = raise TERM ("mk_bit", []);
-
-fun dest_bit (Const ("Int.bit.B0", _)) = 0
-  | dest_bit (Const ("Int.bit.B1", _)) = 1
-  | dest_bit t = raise TERM ("dest_bit", [t]);
-
-
 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
 
 val intT = Type ("Int.int", []);
 
 val pls_const = Const ("Int.Pls", intT)
 and min_const = Const ("Int.Min", intT)
-and bit_const = Const ("Int.Bit", intT --> bitT --> intT);
+and bit0_const = Const ("Int.Bit0", intT --> intT)
+and bit1_const = Const ("Int.Bit1", intT --> intT);
+
+fun mk_bit 0 = bit0_const
+  | mk_bit 1 = bit1_const
+  | mk_bit _ = raise TERM ("mk_bit", []);
+
+fun dest_bit (Const ("Int.Bit0", _)) = 0
+  | dest_bit (Const ("Int.Bit1", _)) = 1
+  | dest_bit t = raise TERM ("dest_bit", [t]);
 
 fun mk_numeral 0 = pls_const
   | mk_numeral ~1 = min_const
   | mk_numeral i =
       let val (q, r) = Integer.div_mod i 2;
-      in bit_const $ mk_numeral q $ mk_bit r end;
+      in mk_bit r $ mk_numeral q end;
 
 fun dest_numeral (Const ("Int.Pls", _)) = 0
   | dest_numeral (Const ("Int.Min", _)) = ~1
-  | dest_numeral (Const ("Int.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
+  | dest_numeral (Const ("Int.Bit0", _) $ bs) = 2 * dest_numeral bs
+  | dest_numeral (Const ("Int.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
 fun number_of_const T = Const ("Int.number_class.number_of", intT --> T);
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/int_arith1.ML
--- a/src/HOL/int_arith1.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/int_arith1.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -548,7 +548,7 @@
     simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
     [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
      @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
-     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
+     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
      @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
      @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
      @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
diff -r 4ce22e7a81bd -r 3c243098b64a src/HOL/int_factor_simprocs.ML
--- a/src/HOL/int_factor_simprocs.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/int_factor_simprocs.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -43,7 +43,7 @@
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
     [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
-      @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
+      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
   end
 
 (*Version for integer division*)
diff -r 4ce22e7a81bd -r 3c243098b64a src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Sat Feb 16 16:52:09 2008 +0100
+++ b/src/Tools/code/code_target.ML	Sun Feb 17 06:49:53 2008 +0100
@@ -23,7 +23,7 @@
   val add_pretty_list_string: string -> string -> string
     -> string -> string list -> theory -> theory;
   val add_pretty_char: string -> string -> string list -> theory -> theory
-  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string -> string
+  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
     -> string -> string -> theory -> theory;
   val add_pretty_message: string -> string -> string list -> string
     -> string -> string -> theory -> theory;
@@ -234,7 +234,7 @@
     else NONE
   end;
 
-fun implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit =
+fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =
   let
     fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
           else if c = c_bit1 then 1
@@ -244,10 +244,9 @@
           else if c = c_min then
             if negative then SOME ~1 else NONE
           else error "Illegal numeral expression: illegal leading digit"
-      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
-          if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
-            in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
-          else error "Illegal numeral expression: illegal bit shift operator"
+      | dest_numeral (t1 `$ t2) =
+          let val (n, b) = (dest_numeral t2, dest_bit t1)
+          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
       | dest_numeral _ = error "Illegal numeral expression: illegal constant";
   in dest_numeral #> the_default 0 end;
 
@@ -1825,11 +1824,11 @@
         | NONE => error "Illegal character expression";
   in (2, pretty) end;
 
-fun pretty_numeral unbounded negative c_bit0 c_bit1 c_pls c_min c_bit target =
+fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
   let
     val mk_numeral = #pretty_numeral (pr_pretty target);
     fun pretty _ _ _ [(t, _)] =
-      (str o mk_numeral unbounded o implode_numeral negative c_bit0 c_bit1 c_pls c_min c_bit) t;
+      (str o mk_numeral unbounded o implode_numeral negative c_pls c_min c_bit0 c_bit1) t;
   in (1, pretty) end;
 
 fun pretty_message c_char c_nibbles c_nil c_cons target =
@@ -2100,14 +2099,13 @@
     |> add_syntax_const target charr (SOME pr)
   end;
 
-fun add_pretty_numeral target unbounded negative number_of b0 b1 pls min bit thy =
+fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
   let
-    val b0' = CodeName.const thy b0;
-    val b1' = CodeName.const thy b1;
     val pls' = CodeName.const thy pls;
     val min' = CodeName.const thy min;
-    val bit' = CodeName.const thy bit;
-    val pr = pretty_numeral unbounded negative b0' b1' pls' min' bit' target;
+    val bit0' = CodeName.const thy bit0;
+    val bit1' = CodeName.const thy bit1;
+    val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
   in
     thy
     |> add_syntax_const target number_of (SOME pr)