# HG changeset patch
# User paulson
# Date 1111576158 -3600
# Node ID 8ccdc8bc66a2d5ddc1e771382a7234281a5a0945
# Parent  cafa1cc0bb0a74b2a09d2feda7412490f3705ade
replaced bool by a new datatype "bit" for binary numerals

diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Mar 23 12:09:18 2005 +0100
@@ -29,14 +29,14 @@
 
 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
 consts posDivAlg :: "int*int => int*int"
-recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))"
+recdef posDivAlg "measure (%(a,b). nat(a - b + 1))"
     "posDivAlg (a,b) =
        (if (a<b | b\<le>0) then (0,a)
         else adjust b (posDivAlg(a, 2*b)))"
 
 text{*algorithm for the case @{text "a<0, b>0"}*}
 consts negDivAlg :: "int*int => int*int"
-recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
+recdef negDivAlg "measure (%(a,b). nat(- a - b))"
     "negDivAlg (a,b) =
        (if (0\<le>a+b | b\<le>0) then (-1,a+b)
         else adjust b (negDivAlg(a, 2*b)))"
@@ -904,12 +904,13 @@
 by auto
 
 lemma zdiv_number_of_BIT[simp]:
-     "number_of (v BIT b) div number_of (w BIT False) =  
-          (if ~b | (0::int) \<le> number_of w                    
+     "number_of (v BIT b) div number_of (w BIT bit.B0) =  
+          (if b=bit.B0 | (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 Bin_simps UNIV_I split: split_if) 
-apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
+apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
+            split: bit.split)
 done
 
 
@@ -943,19 +944,18 @@
 done
 
 lemma zmod_number_of_BIT [simp]:
-     "number_of (v BIT b) mod number_of (w BIT False) =  
-          (if b then  
-                if (0::int) \<le> number_of w  
+     "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  
                 then 2 * (number_of v mod number_of w) + 1     
-                else 2 * ((number_of v + (1::int)) mod number_of w) - 1   
-           else 2 * (number_of v mod number_of w))"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
+                else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
+apply (simp only: number_of_eq Bin_simps UNIV_I split: bit.split) 
 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
                  not_0_le_lemma neg_zmod_mult_2 add_ac)
 done
 
 
-
 subsection{*Quotients of Signs*}
 
 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Integ/NatBin.thy	Wed Mar 23 12:09:18 2005 +0100
@@ -482,16 +482,17 @@
 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))"
-by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
+apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
                OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0
-            split add: split_if cong: imp_cong) 
-
+            split add: bit.split) 
+apply simp
+done
 
 lemma eq_number_of_BIT_Pls:
      "((number_of (v BIT x) ::int) = Numeral0) =  
-      (x=False & (((number_of v) ::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: split_if cong: imp_cong)
+            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)
@@ -500,9 +501,9 @@
 
 lemma eq_number_of_BIT_Min:
      "((number_of (v BIT x) ::int) = number_of Numeral.Min) =  
-      (x=True & (((number_of v) ::int) = number_of Numeral.Min))"
+      (x=bit.B1 & (((number_of v) ::int) = number_of Numeral.Min))"
 apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
-            split add: split_if cong: imp_cong)
+            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
@@ -532,7 +533,7 @@
 text{*For the integers*}
 
 lemma zpower_number_of_even:
-     "(z::int) ^ number_of (w BIT False) =  
+     "(z::int) ^ number_of (w BIT bit.B0) =  
       (let w = z ^ (number_of w) in  w*w)"
 apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
 apply (simp only: number_of_add) 
@@ -542,7 +543,7 @@
 done
 
 lemma zpower_number_of_odd:
-     "(z::int) ^ number_of (w BIT True) =  
+     "(z::int) ^ number_of (w BIT bit.B1) =  
           (if (0::int) <= number_of w                    
            then (let w = z ^ (number_of w) in  z*w*w)    
            else 1)"
@@ -587,8 +588,8 @@
   apply (simp add: neg_nat)
   done
 
-lemma nat_number_of_BIT_True:
-  "number_of (w BIT True) =
+lemma nat_number_of_BIT_1:
+  "number_of (w BIT bit.B1) =
     (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)
@@ -596,22 +597,24 @@
    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 if_True zadd_assoc)
+  apply (simp only: number_of_BIT zadd_assoc split: bit.split)
+  apply simp
   done
 
-lemma nat_number_of_BIT_False:
-    "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
+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 if_False zadd_0 zadd_assoc)
+  apply (simp only: number_of_BIT zadd_assoc)
+  apply simp
   done
 
 lemmas nat_number =
   nat_number_of_Pls nat_number_of_Min
-  nat_number_of_BIT_True nat_number_of_BIT_False
+  nat_number_of_BIT_1 nat_number_of_BIT_0
 
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (simp add: Let_def)
@@ -780,8 +783,6 @@
 val zpower_number_of_odd = thm"zpower_number_of_odd";
 val nat_number_of_Pls = thm"nat_number_of_Pls";
 val nat_number_of_Min = thm"nat_number_of_Min";
-val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
-val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
 val Let_Suc = thm"Let_Suc";
 
 val nat_number = thms"nat_number";
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Integ/Numeral.thy	Wed Mar 23 12:09:18 2005 +0100
@@ -7,12 +7,13 @@
 header{*Arithmetic on Binary Integers*}
 
 theory Numeral
-imports IntDef
-files "Tools/numeral_syntax.ML"
+imports IntDef Datatype
+files "../Tools/numeral_syntax.ML"
 begin
 
 text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
    Only qualified access Numeral.Pls and Numeral.Min is allowed.
+   The datatype constructors bit.B0 and bit.B1 are similarly hidden.
    We do not hide Bit because we need the BIT infix syntax.*}
 
 text{*This formalization defines binary arithmetic in terms of the integers
@@ -31,6 +32,12 @@
   bin = "UNIV::int set"
     by (auto)
 
+
+text{*This datatype avoids the use of type @{typ bool}, which would make
+all of the rewrite rules higher-order. If the use of datatype causes
+problems, this two-element type can easily be formalized using typedef.*}
+datatype bit = B0 | B1
+
 constdefs
   Pls :: "bin"
    "Pls == Abs_Bin 0"
@@ -38,9 +45,9 @@
   Min :: "bin"
    "Min == Abs_Bin (- 1)"
 
-  Bit :: "[bin,bool] => bin"    (infixl "BIT" 90)
+  Bit :: "[bin,bit] => bin"    (infixl "BIT" 90)
    --{*That is, 2w+b*}
-   "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
+   "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"
 
 
 axclass
@@ -56,7 +63,7 @@
 
 translations
   "Numeral0" == "number_of Numeral.Pls"
-  "Numeral1" == "number_of (Numeral.Pls BIT True)"
+  "Numeral1" == "number_of (Numeral.Pls BIT bit.B1)"
 
 
 setup NumeralSyntax.setup
@@ -105,49 +112,49 @@
        Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
 
 text{*Removal of leading zeroes*}
-lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
+lemma Pls_0_eq [simp]: "Numeral.Pls BIT bit.B0 = Numeral.Pls"
 by (simp add: Bin_simps)
 
-lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
+lemma Min_1_eq [simp]: "Numeral.Min BIT bit.B1 = Numeral.Min"
 by (simp add: Bin_simps)
 
 subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
 
-lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
+lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1"
 by (simp add: Bin_simps) 
 
 lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
 by (simp add: Bin_simps) 
 
-lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
+lemma bin_succ_1 [simp]: "bin_succ(w BIT bit.B1) = (bin_succ w) BIT bit.B0"
 by (simp add: Bin_simps add_ac) 
 
-lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
+lemma bin_succ_0 [simp]: "bin_succ(w BIT bit.B0) = w BIT bit.B1"
 by (simp add: Bin_simps add_ac) 
 
 lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
 by (simp add: Bin_simps) 
 
-lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
+lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT bit.B0"
 by (simp add: Bin_simps diff_minus) 
 
-lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
+lemma bin_pred_1 [simp]: "bin_pred(w BIT bit.B1) = w BIT bit.B0"
 by (simp add: Bin_simps) 
 
-lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
+lemma bin_pred_0 [simp]: "bin_pred(w BIT bit.B0) = (bin_pred w) BIT bit.B1"
 by (simp add: Bin_simps diff_minus add_ac) 
 
 lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
 by (simp add: Bin_simps) 
 
-lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
+lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT bit.B1"
 by (simp add: Bin_simps) 
 
 lemma bin_minus_1 [simp]:
-     "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
+     "bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1"
 by (simp add: Bin_simps add_ac diff_minus) 
 
- lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
+ lemma bin_minus_0 [simp]: "bin_minus(w BIT bit.B0) = (bin_minus w) BIT bit.B0"
 by (simp add: Bin_simps) 
 
 
@@ -161,15 +168,15 @@
 by (simp add: Bin_simps diff_minus add_ac) 
 
 lemma bin_add_BIT_11 [simp]:
-     "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
+     "bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0"
 by (simp add: Bin_simps add_ac)
 
 lemma bin_add_BIT_10 [simp]:
-     "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
+     "bin_add (v BIT bit.B1) (w BIT bit.B0) = (bin_add v w) BIT bit.B1"
 by (simp add: Bin_simps add_ac)
 
 lemma bin_add_BIT_0 [simp]:
-     "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
+     "bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y"
 by (simp add: Bin_simps add_ac)
 
 lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
@@ -185,10 +192,10 @@
 by (simp add: Bin_simps) 
 
 lemma bin_mult_1 [simp]:
-     "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
+     "bin_mult (v BIT bit.B1) w = bin_add ((bin_mult v w) BIT bit.B0) w"
 by (simp add: Bin_simps add_ac left_distrib)
 
-lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
+lemma bin_mult_0 [simp]: "bin_mult (v BIT bit.B0) w = (bin_mult v w) BIT bit.B0"
 by (simp add: Bin_simps left_distrib)
 
 
@@ -221,7 +228,7 @@
 text{*The correctness of shifting.  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 False) ::'a::number_ring)"
+     "(1+1) * number_of w = (number_of (w BIT bit.B0) ::'a::number_ring)"
 by (simp add: number_of_eq Bin_simps left_distrib) 
 
 text{*Converting numerals 0 and 1 to their abstract versions*}
@@ -264,9 +271,9 @@
 by (simp add: number_of_eq Bin_simps) 
 
 lemma number_of_BIT:
-     "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
+     "number_of(w BIT x) = (case x of bit.B0 => 0 | bit.B1 => (1::'a::number_ring)) +
 	                   (number_of w) + (number_of w)"
-by (simp add: number_of_eq Bin_simps) 
+by (simp add: number_of_eq Bin_simps split: bit.split) 
 
 
 
@@ -346,19 +353,18 @@
 
 lemma iszero_number_of_BIT:
      "iszero (number_of (w BIT x)::'a) = 
-      (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
+      (x=bit.B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
 by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
-              Ints_odd_nonzero Ints_def)
+              Ints_odd_nonzero Ints_def split: bit.split)
 
 lemma iszero_number_of_0:
-     "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = 
+     "iszero (number_of (w BIT bit.B0) :: 'a::{ordered_idom,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 True)::'a::{ordered_idom,number_ring})"
-by (simp only: iszero_number_of_BIT simp_thms)
-
+     "~ iszero (number_of (w BIT bit.B1)::'a::{ordered_idom,number_ring})"
+by (simp add: iszero_number_of_BIT) 
 
 
 subsection{*The Less-Than Relation*}
@@ -417,7 +423,7 @@
      "neg (number_of (w BIT x)::'a) = 
       neg (number_of w :: 'a::{ordered_idom,number_ring})"
 by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
-              Ints_odd_less_0 Ints_def)
+              Ints_odd_less_0 Ints_def split: bit.split)
 
 
 text{*Less-Than or Equals*}
@@ -457,8 +463,9 @@
        diff_number_of_eq abs_number_of 
 
 text{*For making a minimal simpset, one must include these default simprules.
-  Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
+  Also include @{text simp_thms} *}
 lemmas bin_arith_simps = 
+       Numeral.bit.distinct
        Pls_0_eq Min_1_eq
        bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
        bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Integ/presburger.ML	Wed Mar 23 12:09:18 2005 +0100
@@ -75,6 +75,7 @@
 
 (* SOME Types*)
 val bT = HOLogic.boolT;
+val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
 val binT = HOLogic.binT;
 val nT = HOLogic.natT;
@@ -120,7 +121,9 @@
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
 
-   ("Numeral.Bit", binT --> bT --> binT),
+   ("Numeral.bit.B0", bitT),
+   ("Numeral.bit.B1", bitT),
+   ("Numeral.Bit", binT --> bitT --> binT),
    ("Numeral.Pls", binT),
    ("Numeral.Min", binT),
    ("Numeral.number_of", binT --> iT),
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Library/Word.thy	Wed Mar 23 12:09:18 2005 +0100
@@ -2608,12 +2608,12 @@
 
 primrec
   fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin"
-  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case False True b))"
+  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case bit.B0 bit.B1 b))"
 
-lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT False)"
+lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)"
   by simp
 
-lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)"
+lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)"
   by simp
 
 lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Wed Mar 23 12:09:18 2005 +0100
@@ -75,6 +75,7 @@
 
 (* SOME Types*)
 val bT = HOLogic.boolT;
+val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
 val binT = HOLogic.binT;
 val nT = HOLogic.natT;
@@ -120,7 +121,9 @@
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
 
-   ("Numeral.Bit", binT --> bT --> binT),
+   ("Numeral.bit.B0", bitT),
+   ("Numeral.bit.B1", bitT),
+   ("Numeral.Bit", binT --> bitT --> binT),
    ("Numeral.Pls", binT),
    ("Numeral.Min", binT),
    ("Numeral.number_of", binT --> iT),
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Wed Mar 23 12:09:18 2005 +0100
@@ -15,29 +15,15 @@
 struct
 
 
-(* bits *)
-
-fun dest_bit (Const ("False", _)) = 0
-  | dest_bit (Const ("True", _)) = 1
-  | dest_bit _ = raise Match;
-
-
 (* bit strings *)   (*we try to handle superfluous leading digits nicely*)
 
 fun prefix_len _ [] = 0
   | prefix_len pred (x :: xs) =
       if pred x then 1 + prefix_len pred xs else 0;
 
-fun bin_of (Const ("Numeral.Pls", _)) = []
-  | bin_of (Const ("Numeral.Min", _)) = [~1]
-  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
-  | bin_of _ = raise Match;
-
-val dest_bin = HOLogic.int_of o bin_of;
-
 fun dest_bin_str tm =
   let
-    val rev_digs = bin_of tm;
+    val rev_digs = HOLogic.bin_of tm handle TERM _ => raise Match
     val (sign, zs) =
       (case rev rev_digs of
         ~1 :: bs => ("-", prefix_len (equal 1) bs)
@@ -70,7 +56,8 @@
 
 val setup =
  [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
-  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
+  Theory.hide_consts false ["Numeral.bit.B0", "Numeral.bit.B1"],
+   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
 
 end;
diff -r cafa1cc0bb0a -r 8ccdc8bc66a2 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Mar 23 12:08:52 2005 +0100
+++ b/src/HOL/hologic.ML	Wed Mar 23 12:09:18 2005 +0100
@@ -70,6 +70,9 @@
   val intT: typ
   val mk_int: int -> term
   val realT: typ
+  val bitT: typ
+  val B0_const: term
+  val B1_const: term
   val binT: typ
   val pls_const: term
   val min_const: term
@@ -80,6 +83,7 @@
   val dest_binum: term -> int
   val mk_bin: int -> term
   val mk_bin_from_intinf: IntInf.int -> term
+  val bin_of : term -> int list
   val mk_list: ('a -> term) -> typ -> 'a list -> term
   val dest_list: term -> term list
 end;
@@ -289,9 +293,14 @@
 
 val binT = Type ("Numeral.bin", []);
 
+val bitT = Type ("Numeral.bit", []);
+
+val B0_const = Const ("Numeral.bit.B0", bitT);
+val B1_const =  Const ("Numeral.bit.B1", bitT);
+
 val pls_const = Const ("Numeral.Pls", binT)
 and min_const = Const ("Numeral.Min", binT)
-and bit_const = Const ("Numeral.Bit", [binT, boolT] ---> binT);
+and bit_const = Const ("Numeral.Bit", [binT, bitT] ---> binT);
 
 fun number_of_const T = Const ("Numeral.number_of", binT --> T);
 
@@ -302,39 +311,33 @@
 fun intinf_of [] = IntInf.fromInt 0
   | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
 
-fun dest_bit (Const ("False", _)) = 0
-  | dest_bit (Const ("True", _)) = 1
+(*When called from a print translation, the Numeral qualifier will probably have
+  been removed from Bit, bin.B0, etc.*)
+fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
+  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
+  | dest_bit (Const ("bit.B0", _)) = 0
+  | dest_bit (Const ("bit.B1", _)) = 1
   | dest_bit t = raise TERM("dest_bit", [t]);
 
 fun bin_of (Const ("Numeral.Pls", _)) = []
   | bin_of (Const ("Numeral.Min", _)) = [~1]
   | bin_of (Const ("Numeral.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of t = raise TERM("bin_of", [t]);
 
 val dest_binum = int_of o bin_of;
 
-fun mk_bit 0 = false_const
-  | mk_bit 1 = true_const
+fun mk_bit 0 = B0_const
+  | mk_bit 1 = B1_const
   | mk_bit _ = sys_error "mk_bit";
 
-fun mk_bin n =
-  let
-    fun bin_of 0  = []
-      | bin_of ~1 = [~1]
-      | bin_of n  = (n mod 2) :: bin_of (n div 2);
-
-    fun term_of []   = pls_const
-      | term_of [~1] = min_const
-      | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
-    in term_of (bin_of n) end;
-
 fun mk_bin_from_intinf  n =
     let
 	val zero = IntInf.fromInt 0
 	val minus_one = IntInf.fromInt ~1
 	val two = IntInf.fromInt 2
 
-	fun mk_bit n = if n = zero then false_const else true_const
+	fun mk_bit n = if n = zero then B0_const else B1_const
 								 
 	fun bin_of n = 
 	    if n = zero then pls_const
@@ -351,6 +354,9 @@
 	bin_of n
     end
 
+val mk_bin = mk_bin_from_intinf o IntInf.fromInt;
+
+
 (* int *)
 
 val intT = Type ("IntDef.int", []);