replaced bool by a new datatype "bit" for binary numerals
authorpaulson
Wed Mar 23 12:09:18 2005 +0100 (2005-03-23)
changeset 156208ccdc8bc66a2
parent 15619 cafa1cc0bb0a
child 15621 4c964b85df5c
replaced bool by a new datatype "bit" for binary numerals
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Numeral.thy
src/HOL/Integ/presburger.ML
src/HOL/Library/Word.thy
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Integ/IntDiv.thy	Wed Mar 23 12:08:52 2005 +0100
     1.2 +++ b/src/HOL/Integ/IntDiv.thy	Wed Mar 23 12:09:18 2005 +0100
     1.3 @@ -29,14 +29,14 @@
     1.4  
     1.5  text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
     1.6  consts posDivAlg :: "int*int => int*int"
     1.7 -recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))"
     1.8 +recdef posDivAlg "measure (%(a,b). nat(a - b + 1))"
     1.9      "posDivAlg (a,b) =
    1.10         (if (a<b | b\<le>0) then (0,a)
    1.11          else adjust b (posDivAlg(a, 2*b)))"
    1.12  
    1.13  text{*algorithm for the case @{text "a<0, b>0"}*}
    1.14  consts negDivAlg :: "int*int => int*int"
    1.15 -recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
    1.16 +recdef negDivAlg "measure (%(a,b). nat(- a - b))"
    1.17      "negDivAlg (a,b) =
    1.18         (if (0\<le>a+b | b\<le>0) then (-1,a+b)
    1.19          else adjust b (negDivAlg(a, 2*b)))"
    1.20 @@ -904,12 +904,13 @@
    1.21  by auto
    1.22  
    1.23  lemma zdiv_number_of_BIT[simp]:
    1.24 -     "number_of (v BIT b) div number_of (w BIT False) =  
    1.25 -          (if ~b | (0::int) \<le> number_of w                    
    1.26 +     "number_of (v BIT b) div number_of (w BIT bit.B0) =  
    1.27 +          (if b=bit.B0 | (0::int) \<le> number_of w                    
    1.28             then number_of v div (number_of w)     
    1.29             else (number_of v + (1::int)) div (number_of w))"
    1.30  apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
    1.31 -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
    1.32 +apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
    1.33 +            split: bit.split)
    1.34  done
    1.35  
    1.36  
    1.37 @@ -943,19 +944,18 @@
    1.38  done
    1.39  
    1.40  lemma zmod_number_of_BIT [simp]:
    1.41 -     "number_of (v BIT b) mod number_of (w BIT False) =  
    1.42 -          (if b then  
    1.43 -                if (0::int) \<le> number_of w  
    1.44 +     "number_of (v BIT b) mod number_of (w BIT bit.B0) =  
    1.45 +      (case b of
    1.46 +          bit.B0 => 2 * (number_of v mod number_of w)
    1.47 +        | bit.B1 => if (0::int) \<le> number_of w  
    1.48                  then 2 * (number_of v mod number_of w) + 1     
    1.49 -                else 2 * ((number_of v + (1::int)) mod number_of w) - 1   
    1.50 -           else 2 * (number_of v mod number_of w))"
    1.51 -apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
    1.52 +                else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
    1.53 +apply (simp only: number_of_eq Bin_simps UNIV_I split: bit.split) 
    1.54  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    1.55                   not_0_le_lemma neg_zmod_mult_2 add_ac)
    1.56  done
    1.57  
    1.58  
    1.59 -
    1.60  subsection{*Quotients of Signs*}
    1.61  
    1.62  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
     2.1 --- a/src/HOL/Integ/NatBin.thy	Wed Mar 23 12:08:52 2005 +0100
     2.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Mar 23 12:09:18 2005 +0100
     2.3 @@ -482,16 +482,17 @@
     2.4  lemma eq_number_of_BIT_BIT:
     2.5       "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
     2.6        (x=y & (((number_of v) ::int) = number_of w))"
     2.7 -by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
     2.8 +apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
     2.9                 OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0
    2.10 -            split add: split_if cong: imp_cong) 
    2.11 -
    2.12 +            split add: bit.split) 
    2.13 +apply simp
    2.14 +done
    2.15  
    2.16  lemma eq_number_of_BIT_Pls:
    2.17       "((number_of (v BIT x) ::int) = Numeral0) =  
    2.18 -      (x=False & (((number_of v) ::int) = Numeral0))"
    2.19 +      (x=bit.B0 & (((number_of v) ::int) = Numeral0))"
    2.20  apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
    2.21 -            split add: split_if cong: imp_cong)
    2.22 +            split add: bit.split cong: imp_cong)
    2.23  apply (rule_tac x = "number_of v" in spec, safe)
    2.24  apply (simp_all (no_asm_use))
    2.25  apply (drule_tac f = "%x. x mod 2" in arg_cong)
    2.26 @@ -500,9 +501,9 @@
    2.27  
    2.28  lemma eq_number_of_BIT_Min:
    2.29       "((number_of (v BIT x) ::int) = number_of Numeral.Min) =  
    2.30 -      (x=True & (((number_of v) ::int) = number_of Numeral.Min))"
    2.31 +      (x=bit.B1 & (((number_of v) ::int) = number_of Numeral.Min))"
    2.32  apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
    2.33 -            split add: split_if cong: imp_cong)
    2.34 +            split add: bit.split cong: imp_cong)
    2.35  apply (rule_tac x = "number_of v" in spec, auto)
    2.36  apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
    2.37  done
    2.38 @@ -532,7 +533,7 @@
    2.39  text{*For the integers*}
    2.40  
    2.41  lemma zpower_number_of_even:
    2.42 -     "(z::int) ^ number_of (w BIT False) =  
    2.43 +     "(z::int) ^ number_of (w BIT bit.B0) =  
    2.44        (let w = z ^ (number_of w) in  w*w)"
    2.45  apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
    2.46  apply (simp only: number_of_add) 
    2.47 @@ -542,7 +543,7 @@
    2.48  done
    2.49  
    2.50  lemma zpower_number_of_odd:
    2.51 -     "(z::int) ^ number_of (w BIT True) =  
    2.52 +     "(z::int) ^ number_of (w BIT bit.B1) =  
    2.53            (if (0::int) <= number_of w                    
    2.54             then (let w = z ^ (number_of w) in  z*w*w)    
    2.55             else 1)"
    2.56 @@ -587,8 +588,8 @@
    2.57    apply (simp add: neg_nat)
    2.58    done
    2.59  
    2.60 -lemma nat_number_of_BIT_True:
    2.61 -  "number_of (w BIT True) =
    2.62 +lemma nat_number_of_BIT_1:
    2.63 +  "number_of (w BIT bit.B1) =
    2.64      (if neg (number_of w :: int) then 0
    2.65       else let n = number_of w in Suc (n + n))"
    2.66    apply (simp only: nat_number_of_def Let_def split: split_if)
    2.67 @@ -596,22 +597,24 @@
    2.68     apply (simp add: neg_nat neg_number_of_BIT)
    2.69    apply (rule int_int_eq [THEN iffD1])
    2.70    apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
    2.71 -  apply (simp only: number_of_BIT if_True zadd_assoc)
    2.72 +  apply (simp only: number_of_BIT zadd_assoc split: bit.split)
    2.73 +  apply simp
    2.74    done
    2.75  
    2.76 -lemma nat_number_of_BIT_False:
    2.77 -    "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
    2.78 +lemma nat_number_of_BIT_0:
    2.79 +    "number_of (w BIT bit.B0) = (let n::nat = number_of w in n + n)"
    2.80    apply (simp only: nat_number_of_def Let_def)
    2.81    apply (cases "neg (number_of w :: int)")
    2.82     apply (simp add: neg_nat neg_number_of_BIT)
    2.83    apply (rule int_int_eq [THEN iffD1])
    2.84    apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
    2.85 -  apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc)
    2.86 +  apply (simp only: number_of_BIT zadd_assoc)
    2.87 +  apply simp
    2.88    done
    2.89  
    2.90  lemmas nat_number =
    2.91    nat_number_of_Pls nat_number_of_Min
    2.92 -  nat_number_of_BIT_True nat_number_of_BIT_False
    2.93 +  nat_number_of_BIT_1 nat_number_of_BIT_0
    2.94  
    2.95  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    2.96    by (simp add: Let_def)
    2.97 @@ -780,8 +783,6 @@
    2.98  val zpower_number_of_odd = thm"zpower_number_of_odd";
    2.99  val nat_number_of_Pls = thm"nat_number_of_Pls";
   2.100  val nat_number_of_Min = thm"nat_number_of_Min";
   2.101 -val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
   2.102 -val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
   2.103  val Let_Suc = thm"Let_Suc";
   2.104  
   2.105  val nat_number = thms"nat_number";
     3.1 --- a/src/HOL/Integ/Numeral.thy	Wed Mar 23 12:08:52 2005 +0100
     3.2 +++ b/src/HOL/Integ/Numeral.thy	Wed Mar 23 12:09:18 2005 +0100
     3.3 @@ -7,12 +7,13 @@
     3.4  header{*Arithmetic on Binary Integers*}
     3.5  
     3.6  theory Numeral
     3.7 -imports IntDef
     3.8 -files "Tools/numeral_syntax.ML"
     3.9 +imports IntDef Datatype
    3.10 +files "../Tools/numeral_syntax.ML"
    3.11  begin
    3.12  
    3.13  text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
    3.14     Only qualified access Numeral.Pls and Numeral.Min is allowed.
    3.15 +   The datatype constructors bit.B0 and bit.B1 are similarly hidden.
    3.16     We do not hide Bit because we need the BIT infix syntax.*}
    3.17  
    3.18  text{*This formalization defines binary arithmetic in terms of the integers
    3.19 @@ -31,6 +32,12 @@
    3.20    bin = "UNIV::int set"
    3.21      by (auto)
    3.22  
    3.23 +
    3.24 +text{*This datatype avoids the use of type @{typ bool}, which would make
    3.25 +all of the rewrite rules higher-order. If the use of datatype causes
    3.26 +problems, this two-element type can easily be formalized using typedef.*}
    3.27 +datatype bit = B0 | B1
    3.28 +
    3.29  constdefs
    3.30    Pls :: "bin"
    3.31     "Pls == Abs_Bin 0"
    3.32 @@ -38,9 +45,9 @@
    3.33    Min :: "bin"
    3.34     "Min == Abs_Bin (- 1)"
    3.35  
    3.36 -  Bit :: "[bin,bool] => bin"    (infixl "BIT" 90)
    3.37 +  Bit :: "[bin,bit] => bin"    (infixl "BIT" 90)
    3.38     --{*That is, 2w+b*}
    3.39 -   "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
    3.40 +   "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"
    3.41  
    3.42  
    3.43  axclass
    3.44 @@ -56,7 +63,7 @@
    3.45  
    3.46  translations
    3.47    "Numeral0" == "number_of Numeral.Pls"
    3.48 -  "Numeral1" == "number_of (Numeral.Pls BIT True)"
    3.49 +  "Numeral1" == "number_of (Numeral.Pls BIT bit.B1)"
    3.50  
    3.51  
    3.52  setup NumeralSyntax.setup
    3.53 @@ -105,49 +112,49 @@
    3.54         Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
    3.55  
    3.56  text{*Removal of leading zeroes*}
    3.57 -lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
    3.58 +lemma Pls_0_eq [simp]: "Numeral.Pls BIT bit.B0 = Numeral.Pls"
    3.59  by (simp add: Bin_simps)
    3.60  
    3.61 -lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
    3.62 +lemma Min_1_eq [simp]: "Numeral.Min BIT bit.B1 = Numeral.Min"
    3.63  by (simp add: Bin_simps)
    3.64  
    3.65  subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
    3.66  
    3.67 -lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
    3.68 +lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1"
    3.69  by (simp add: Bin_simps) 
    3.70  
    3.71  lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
    3.72  by (simp add: Bin_simps) 
    3.73  
    3.74 -lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
    3.75 +lemma bin_succ_1 [simp]: "bin_succ(w BIT bit.B1) = (bin_succ w) BIT bit.B0"
    3.76  by (simp add: Bin_simps add_ac) 
    3.77  
    3.78 -lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
    3.79 +lemma bin_succ_0 [simp]: "bin_succ(w BIT bit.B0) = w BIT bit.B1"
    3.80  by (simp add: Bin_simps add_ac) 
    3.81  
    3.82  lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
    3.83  by (simp add: Bin_simps) 
    3.84  
    3.85 -lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
    3.86 +lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT bit.B0"
    3.87  by (simp add: Bin_simps diff_minus) 
    3.88  
    3.89 -lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
    3.90 +lemma bin_pred_1 [simp]: "bin_pred(w BIT bit.B1) = w BIT bit.B0"
    3.91  by (simp add: Bin_simps) 
    3.92  
    3.93 -lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
    3.94 +lemma bin_pred_0 [simp]: "bin_pred(w BIT bit.B0) = (bin_pred w) BIT bit.B1"
    3.95  by (simp add: Bin_simps diff_minus add_ac) 
    3.96  
    3.97  lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
    3.98  by (simp add: Bin_simps) 
    3.99  
   3.100 -lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
   3.101 +lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT bit.B1"
   3.102  by (simp add: Bin_simps) 
   3.103  
   3.104  lemma bin_minus_1 [simp]:
   3.105 -     "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
   3.106 +     "bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1"
   3.107  by (simp add: Bin_simps add_ac diff_minus) 
   3.108  
   3.109 - lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
   3.110 + lemma bin_minus_0 [simp]: "bin_minus(w BIT bit.B0) = (bin_minus w) BIT bit.B0"
   3.111  by (simp add: Bin_simps) 
   3.112  
   3.113  
   3.114 @@ -161,15 +168,15 @@
   3.115  by (simp add: Bin_simps diff_minus add_ac) 
   3.116  
   3.117  lemma bin_add_BIT_11 [simp]:
   3.118 -     "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
   3.119 +     "bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0"
   3.120  by (simp add: Bin_simps add_ac)
   3.121  
   3.122  lemma bin_add_BIT_10 [simp]:
   3.123 -     "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
   3.124 +     "bin_add (v BIT bit.B1) (w BIT bit.B0) = (bin_add v w) BIT bit.B1"
   3.125  by (simp add: Bin_simps add_ac)
   3.126  
   3.127  lemma bin_add_BIT_0 [simp]:
   3.128 -     "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
   3.129 +     "bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y"
   3.130  by (simp add: Bin_simps add_ac)
   3.131  
   3.132  lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
   3.133 @@ -185,10 +192,10 @@
   3.134  by (simp add: Bin_simps) 
   3.135  
   3.136  lemma bin_mult_1 [simp]:
   3.137 -     "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
   3.138 +     "bin_mult (v BIT bit.B1) w = bin_add ((bin_mult v w) BIT bit.B0) w"
   3.139  by (simp add: Bin_simps add_ac left_distrib)
   3.140  
   3.141 -lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
   3.142 +lemma bin_mult_0 [simp]: "bin_mult (v BIT bit.B0) w = (bin_mult v w) BIT bit.B0"
   3.143  by (simp add: Bin_simps left_distrib)
   3.144  
   3.145  
   3.146 @@ -221,7 +228,7 @@
   3.147  text{*The correctness of shifting.  But it doesn't seem to give a measurable
   3.148    speed-up.*}
   3.149  lemma double_number_of_BIT:
   3.150 -     "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
   3.151 +     "(1+1) * number_of w = (number_of (w BIT bit.B0) ::'a::number_ring)"
   3.152  by (simp add: number_of_eq Bin_simps left_distrib) 
   3.153  
   3.154  text{*Converting numerals 0 and 1 to their abstract versions*}
   3.155 @@ -264,9 +271,9 @@
   3.156  by (simp add: number_of_eq Bin_simps) 
   3.157  
   3.158  lemma number_of_BIT:
   3.159 -     "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
   3.160 +     "number_of(w BIT x) = (case x of bit.B0 => 0 | bit.B1 => (1::'a::number_ring)) +
   3.161  	                   (number_of w) + (number_of w)"
   3.162 -by (simp add: number_of_eq Bin_simps) 
   3.163 +by (simp add: number_of_eq Bin_simps split: bit.split) 
   3.164  
   3.165  
   3.166  
   3.167 @@ -346,19 +353,18 @@
   3.168  
   3.169  lemma iszero_number_of_BIT:
   3.170       "iszero (number_of (w BIT x)::'a) = 
   3.171 -      (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
   3.172 +      (x=bit.B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
   3.173  by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
   3.174 -              Ints_odd_nonzero Ints_def)
   3.175 +              Ints_odd_nonzero Ints_def split: bit.split)
   3.176  
   3.177  lemma iszero_number_of_0:
   3.178 -     "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = 
   3.179 +     "iszero (number_of (w BIT bit.B0) :: 'a::{ordered_idom,number_ring}) = 
   3.180        iszero (number_of w :: 'a)"
   3.181  by (simp only: iszero_number_of_BIT simp_thms)
   3.182  
   3.183  lemma iszero_number_of_1:
   3.184 -     "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
   3.185 -by (simp only: iszero_number_of_BIT simp_thms)
   3.186 -
   3.187 +     "~ iszero (number_of (w BIT bit.B1)::'a::{ordered_idom,number_ring})"
   3.188 +by (simp add: iszero_number_of_BIT) 
   3.189  
   3.190  
   3.191  subsection{*The Less-Than Relation*}
   3.192 @@ -417,7 +423,7 @@
   3.193       "neg (number_of (w BIT x)::'a) = 
   3.194        neg (number_of w :: 'a::{ordered_idom,number_ring})"
   3.195  by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
   3.196 -              Ints_odd_less_0 Ints_def)
   3.197 +              Ints_odd_less_0 Ints_def split: bit.split)
   3.198  
   3.199  
   3.200  text{*Less-Than or Equals*}
   3.201 @@ -457,8 +463,9 @@
   3.202         diff_number_of_eq abs_number_of 
   3.203  
   3.204  text{*For making a minimal simpset, one must include these default simprules.
   3.205 -  Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
   3.206 +  Also include @{text simp_thms} *}
   3.207  lemmas bin_arith_simps = 
   3.208 +       Numeral.bit.distinct
   3.209         Pls_0_eq Min_1_eq
   3.210         bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
   3.211         bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
     4.1 --- a/src/HOL/Integ/presburger.ML	Wed Mar 23 12:08:52 2005 +0100
     4.2 +++ b/src/HOL/Integ/presburger.ML	Wed Mar 23 12:09:18 2005 +0100
     4.3 @@ -75,6 +75,7 @@
     4.4  
     4.5  (* SOME Types*)
     4.6  val bT = HOLogic.boolT;
     4.7 +val bitT = HOLogic.bitT;
     4.8  val iT = HOLogic.intT;
     4.9  val binT = HOLogic.binT;
    4.10  val nT = HOLogic.natT;
    4.11 @@ -120,7 +121,9 @@
    4.12     ("HOL.max", nT --> nT --> nT),
    4.13     ("HOL.min", nT --> nT --> nT),
    4.14  
    4.15 -   ("Numeral.Bit", binT --> bT --> binT),
    4.16 +   ("Numeral.bit.B0", bitT),
    4.17 +   ("Numeral.bit.B1", bitT),
    4.18 +   ("Numeral.Bit", binT --> bitT --> binT),
    4.19     ("Numeral.Pls", binT),
    4.20     ("Numeral.Min", binT),
    4.21     ("Numeral.number_of", binT --> iT),
     5.1 --- a/src/HOL/Library/Word.thy	Wed Mar 23 12:08:52 2005 +0100
     5.2 +++ b/src/HOL/Library/Word.thy	Wed Mar 23 12:09:18 2005 +0100
     5.3 @@ -2608,12 +2608,12 @@
     5.4  
     5.5  primrec
     5.6    fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin"
     5.7 -  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))"
     5.8 +  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))"
     5.9  
    5.10 -lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT False)"
    5.11 +lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)"
    5.12    by simp
    5.13  
    5.14 -lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)"
    5.15 +lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)"
    5.16    by simp
    5.17  
    5.18  lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
     6.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Wed Mar 23 12:08:52 2005 +0100
     6.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Wed Mar 23 12:09:18 2005 +0100
     6.3 @@ -75,6 +75,7 @@
     6.4  
     6.5  (* SOME Types*)
     6.6  val bT = HOLogic.boolT;
     6.7 +val bitT = HOLogic.bitT;
     6.8  val iT = HOLogic.intT;
     6.9  val binT = HOLogic.binT;
    6.10  val nT = HOLogic.natT;
    6.11 @@ -120,7 +121,9 @@
    6.12     ("HOL.max", nT --> nT --> nT),
    6.13     ("HOL.min", nT --> nT --> nT),
    6.14  
    6.15 -   ("Numeral.Bit", binT --> bT --> binT),
    6.16 +   ("Numeral.bit.B0", bitT),
    6.17 +   ("Numeral.bit.B1", bitT),
    6.18 +   ("Numeral.Bit", binT --> bitT --> binT),
    6.19     ("Numeral.Pls", binT),
    6.20     ("Numeral.Min", binT),
    6.21     ("Numeral.number_of", binT --> iT),
     7.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Mar 23 12:08:52 2005 +0100
     7.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Mar 23 12:09:18 2005 +0100
     7.3 @@ -15,29 +15,15 @@
     7.4  struct
     7.5  
     7.6  
     7.7 -(* bits *)
     7.8 -
     7.9 -fun dest_bit (Const ("False", _)) = 0
    7.10 -  | dest_bit (Const ("True", _)) = 1
    7.11 -  | dest_bit _ = raise Match;
    7.12 -
    7.13 -
    7.14  (* bit strings *)   (*we try to handle superfluous leading digits nicely*)
    7.15  
    7.16  fun prefix_len _ [] = 0
    7.17    | prefix_len pred (x :: xs) =
    7.18        if pred x then 1 + prefix_len pred xs else 0;
    7.19  
    7.20 -fun bin_of (Const ("Numeral.Pls", _)) = []
    7.21 -  | bin_of (Const ("Numeral.Min", _)) = [~1]
    7.22 -  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    7.23 -  | bin_of _ = raise Match;
    7.24 -
    7.25 -val dest_bin = HOLogic.int_of o bin_of;
    7.26 -
    7.27  fun dest_bin_str tm =
    7.28    let
    7.29 -    val rev_digs = bin_of tm;
    7.30 +    val rev_digs = HOLogic.bin_of tm handle TERM _ => raise Match
    7.31      val (sign, zs) =
    7.32        (case rev rev_digs of
    7.33          ~1 :: bs => ("-", prefix_len (equal 1) bs)
    7.34 @@ -70,7 +56,8 @@
    7.35  
    7.36  val setup =
    7.37   [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
    7.38 -  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    7.39 +  Theory.hide_consts false ["Numeral.bit.B0", "Numeral.bit.B1"],
    7.40 +   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    7.41    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    7.42  
    7.43  end;
     8.1 --- a/src/HOL/hologic.ML	Wed Mar 23 12:08:52 2005 +0100
     8.2 +++ b/src/HOL/hologic.ML	Wed Mar 23 12:09:18 2005 +0100
     8.3 @@ -70,6 +70,9 @@
     8.4    val intT: typ
     8.5    val mk_int: int -> term
     8.6    val realT: typ
     8.7 +  val bitT: typ
     8.8 +  val B0_const: term
     8.9 +  val B1_const: term
    8.10    val binT: typ
    8.11    val pls_const: term
    8.12    val min_const: term
    8.13 @@ -80,6 +83,7 @@
    8.14    val dest_binum: term -> int
    8.15    val mk_bin: int -> term
    8.16    val mk_bin_from_intinf: IntInf.int -> term
    8.17 +  val bin_of : term -> int list
    8.18    val mk_list: ('a -> term) -> typ -> 'a list -> term
    8.19    val dest_list: term -> term list
    8.20  end;
    8.21 @@ -289,9 +293,14 @@
    8.22  
    8.23  val binT = Type ("Numeral.bin", []);
    8.24  
    8.25 +val bitT = Type ("Numeral.bit", []);
    8.26 +
    8.27 +val B0_const = Const ("Numeral.bit.B0", bitT);
    8.28 +val B1_const =  Const ("Numeral.bit.B1", bitT);
    8.29 +
    8.30  val pls_const = Const ("Numeral.Pls", binT)
    8.31  and min_const = Const ("Numeral.Min", binT)
    8.32 -and bit_const = Const ("Numeral.Bit", [binT, boolT] ---> binT);
    8.33 +and bit_const = Const ("Numeral.Bit", [binT, bitT] ---> binT);
    8.34  
    8.35  fun number_of_const T = Const ("Numeral.number_of", binT --> T);
    8.36  
    8.37 @@ -302,39 +311,33 @@
    8.38  fun intinf_of [] = IntInf.fromInt 0
    8.39    | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
    8.40  
    8.41 -fun dest_bit (Const ("False", _)) = 0
    8.42 -  | dest_bit (Const ("True", _)) = 1
    8.43 +(*When called from a print translation, the Numeral qualifier will probably have
    8.44 +  been removed from Bit, bin.B0, etc.*)
    8.45 +fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
    8.46 +  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
    8.47 +  | dest_bit (Const ("bit.B0", _)) = 0
    8.48 +  | dest_bit (Const ("bit.B1", _)) = 1
    8.49    | dest_bit t = raise TERM("dest_bit", [t]);
    8.50  
    8.51  fun bin_of (Const ("Numeral.Pls", _)) = []
    8.52    | bin_of (Const ("Numeral.Min", _)) = [~1]
    8.53    | bin_of (Const ("Numeral.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    8.54 +  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    8.55    | bin_of t = raise TERM("bin_of", [t]);
    8.56  
    8.57  val dest_binum = int_of o bin_of;
    8.58  
    8.59 -fun mk_bit 0 = false_const
    8.60 -  | mk_bit 1 = true_const
    8.61 +fun mk_bit 0 = B0_const
    8.62 +  | mk_bit 1 = B1_const
    8.63    | mk_bit _ = sys_error "mk_bit";
    8.64  
    8.65 -fun mk_bin n =
    8.66 -  let
    8.67 -    fun bin_of 0  = []
    8.68 -      | bin_of ~1 = [~1]
    8.69 -      | bin_of n  = (n mod 2) :: bin_of (n div 2);
    8.70 -
    8.71 -    fun term_of []   = pls_const
    8.72 -      | term_of [~1] = min_const
    8.73 -      | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
    8.74 -    in term_of (bin_of n) end;
    8.75 -
    8.76  fun mk_bin_from_intinf  n =
    8.77      let
    8.78  	val zero = IntInf.fromInt 0
    8.79  	val minus_one = IntInf.fromInt ~1
    8.80  	val two = IntInf.fromInt 2
    8.81  
    8.82 -	fun mk_bit n = if n = zero then false_const else true_const
    8.83 +	fun mk_bit n = if n = zero then B0_const else B1_const
    8.84  								 
    8.85  	fun bin_of n = 
    8.86  	    if n = zero then pls_const
    8.87 @@ -351,6 +354,9 @@
    8.88  	bin_of n
    8.89      end
    8.90  
    8.91 +val mk_bin = mk_bin_from_intinf o IntInf.fromInt;
    8.92 +
    8.93 +
    8.94  (* int *)
    8.95  
    8.96  val intT = Type ("IntDef.int", []);