author paulson Wed Mar 23 12:09:18 2005 +0100 (2005-03-23) changeset 15620 8ccdc8bc66a2 parent 15619 cafa1cc0bb0a child 15621 4c964b85df5c
replaced bool by a new datatype "bit" for binary numerals
 src/HOL/Integ/IntDiv.thy file | annotate | diff | revisions src/HOL/Integ/NatBin.thy file | annotate | diff | revisions src/HOL/Integ/Numeral.thy file | annotate | diff | revisions src/HOL/Integ/presburger.ML file | annotate | diff | revisions src/HOL/Library/Word.thy file | annotate | diff | revisions src/HOL/Tools/Presburger/presburger.ML file | annotate | diff | revisions src/HOL/Tools/numeral_syntax.ML file | annotate | diff | revisions src/HOL/hologic.ML file | annotate | diff | revisions
```     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.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.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.10 -            split add: split_if cong: imp_cong)
2.11 -
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.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.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.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.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.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.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.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.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.70
3.71  lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
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.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.81
3.82  lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
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.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.96
3.97  lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
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.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.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.112
3.113
3.114 @@ -161,15 +168,15 @@
3.116
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.121
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.126
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.131
3.133 @@ -185,10 +192,10 @@
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.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.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", []);
```