--- 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"
--- 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";
--- 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
--- 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),
--- 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)"
--- 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),
--- 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;
--- 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", []);