(* Title: HOL/Numeral.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
header {* Arithmetic on Binary Integers *}
theory Numeral
imports Datatype IntDef
uses
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
begin
subsection {* Binary representation *}
text {*
This formalization defines binary arithmetic in terms of the integers
rather than using a datatype. This avoids multiple representations (leading
zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
int_of_binary}, for the numerical interpretation.
The representation expects that @{text "(m mod 2)"} is 0 or 1,
even if m is negative;
For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
@{text "-5 = (-3)*2 + 1"}.
This two's complement binary representation derives from the paper
"An Efficient Representation of Arithmetic for Term Rewriting" by
Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
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"
definition
Min :: int where
[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"
class number = type + -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
use "Tools/numeral.ML"
syntax
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
use "Tools/numeral_syntax.ML"
setup NumeralSyntax.setup
abbreviation
"Numeral0 \<equiv> number_of Pls"
abbreviation
"Numeral1 \<equiv> number_of (Pls BIT B1)"
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
definition
succ :: "int \<Rightarrow> int" where
[code func del]: "succ k = k + 1"
definition
pred :: "int \<Rightarrow> int" where
[code func del]: "pred k = k - 1"
lemmas
max_number_of [simp] = max_def
[of "number_of u" "number_of v", standard, simp]
and
min_number_of [simp] = min_def
[of "number_of u" "number_of v", standard, simp]
-- {* unfolding @{text minx} and @{text max} on numerals *}
lemmas numeral_simps =
succ_def pred_def Pls_def Min_def Bit_def
text {* Removal of leading zeroes *}
lemma Pls_0_eq [simp, code post]:
"Pls BIT B0 = Pls"
unfolding numeral_simps by simp
lemma Min_1_eq [simp, code post]:
"Min BIT B1 = Min"
unfolding numeral_simps by simp
subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
lemma succ_Pls [simp]:
"succ Pls = Pls BIT B1"
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"
unfolding numeral_simps by simp
lemma succ_0 [simp]:
"succ (k BIT B0) = k BIT B1"
unfolding numeral_simps by simp
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"
unfolding numeral_simps by simp
lemma pred_0 [simp]:
"pred (k BIT B0) = pred k BIT B1"
unfolding numeral_simps by simp
lemma minus_Pls [simp]:
"- Pls = Pls"
unfolding numeral_simps by simp
lemma minus_Min [simp]:
"- Min = Pls BIT B1"
unfolding numeral_simps by simp
lemma minus_1 [simp]:
"- (k BIT B1) = pred (- k) BIT B1"
unfolding numeral_simps by simp
lemma minus_0 [simp]:
"- (k BIT B0) = (- k) BIT B0"
unfolding numeral_simps by simp
subsection {*
Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
*}
lemma add_Pls [simp]:
"Pls + k = k"
unfolding numeral_simps by simp
lemma add_Min [simp]:
"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"
unfolding numeral_simps by simp
lemma add_BIT_10 [simp]:
"(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
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
lemma mult_Pls [simp]:
"Pls * w = Pls"
unfolding numeral_simps by simp
lemma mult_Min [simp]:
"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_num0 [simp]:
"(k BIT B0) * l = (k * l) BIT B0"
unfolding numeral_simps int_distrib by simp
subsection {* Converting Numerals to Rings: @{term number_of} *}
class number_ring = number + comm_ring_1 +
assumes number_of_eq: "number_of k = of_int k"
text {* self-embedding of the integers *}
instance int :: number_ring
int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
by intro_classes (simp only: int_number_of_def)
lemmas [code func del] = int_number_of_def
lemma number_of_is_id:
"number_of (k::int) = k"
unfolding int_number_of_def by simp
lemma number_of_succ:
"number_of (succ k) = (1 + number_of k ::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma number_of_pred:
"number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma number_of_minus:
"number_of (uminus w) = (- (number_of w)::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma number_of_add:
"number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma number_of_mult:
"number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
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 B0) ::'a::number_ring)"
unfolding number_of_eq numeral_simps left_distrib by simp
text {*
Converting numerals 0 and 1 to their abstract versions.
*}
lemma numeral_0_eq_0 [simp]:
"Numeral0 = (0::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma numeral_1_eq_1 [simp]:
"Numeral1 = (1::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
text {*
Special-case simplification for small constants.
*}
text{*
Unary minus for the abstract constant 1. Cannot be inserted
as a simprule until later: it is @{text number_of_Min} re-oriented!
*}
lemma numeral_m1_eq_minus_1:
"(-1::'a::number_ring) = - 1"
unfolding number_of_eq numeral_simps by simp
lemma mult_minus1 [simp]:
"-1 * z = -(z::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma mult_minus1_right [simp]:
"z * -1 = -(z::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
(*Negation of a coefficient*)
lemma minus_number_of_mult [simp]:
"- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
unfolding number_of_eq by simp
text {* Subtraction *}
lemma diff_number_of_eq:
"number_of v - number_of w =
(number_of (v + uminus w)::'a::number_ring)"
unfolding number_of_eq by simp
lemma number_of_Pls:
"number_of Pls = (0::'a::number_ring)"
unfolding number_of_eq numeral_simps by simp
lemma number_of_Min:
"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)
subsection {* Equality of Binary Numbers *}
text {* First version by Norbert Voelker *}
lemma eq_number_of_eq:
"((number_of x::'a::number_ring) = number_of y) =
iszero (number_of (x + uminus y) :: 'a)"
unfolding iszero_def number_of_add number_of_minus
by (simp add: compare_rls)
lemma iszero_number_of_Pls:
"iszero ((number_of Pls)::'a::number_ring)"
unfolding iszero_def numeral_0_eq_0 ..
lemma nonzero_number_of_Min:
"~ iszero ((number_of Min)::'a::number_ring)"
unfolding iszero_def numeral_m1_eq_minus_1 by simp
subsection {* Comparisons, for Ordered Rings *}
lemmas double_eq_0_iff = double_zero
lemma le_imp_0_less:
assumes le: "0 \<le> z"
shows "(0::int) < 1 + z"
proof -
have "0 \<le> z" by fact
also have "... < z + 1" by (rule less_add_one)
also have "... = 1 + z" by (simp add: add_ac)
finally show "0 < 1 + z" .
qed
lemma odd_nonzero:
"1 + z + z \<noteq> (0::int)";
proof (cases z rule: int_cases)
case (nonneg n)
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
thus ?thesis using le_imp_0_less [OF le]
by (auto simp add: add_assoc)
next
case (neg n)
show ?thesis
proof
assume eq: "1 + z + z = 0"
have "0 < 1 + (int n + int n)"
by (simp add: le_imp_0_less add_increasing)
also have "... = - (1 + z + z)"
by (simp add: neg add_assoc [symmetric])
also have "... = 0" by (simp add: eq)
finally have "0<0" ..
thus False by blast
qed
qed
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
lemma Ints_double_eq_0_iff:
assumes in_Ints: "a \<in> Ints"
shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
then obtain z where a: "a = of_int z" ..
show ?thesis
proof
assume "a = 0"
thus "a + a = 0" by simp
next
assume eq: "a + a = 0"
hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
hence "z + z = 0" by (simp only: of_int_eq_iff)
hence "z = 0" by (simp only: double_eq_0_iff)
thus "a = 0" by (simp add: a)
qed
qed
lemma Ints_odd_nonzero:
assumes in_Ints: "a \<in> Ints"
shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
then obtain z where a: "a = of_int z" ..
show ?thesis
proof
assume eq: "1 + a + a = 0"
hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
with odd_nonzero show False by blast
qed
qed
lemma Ints_number_of:
"(number_of w :: 'a::number_ring) \<in> Ints"
unfolding number_of_eq Ints_def by simp
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}))"
by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff
Ints_odd_nonzero Ints_def split: bit.split)
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 *}
lemma less_number_of_eq_neg:
"((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
= neg (number_of (x + uminus y) :: 'a)"
apply (subst less_iff_diff_less_0)
apply (simp add: neg_def diff_minus number_of_add number_of_minus)
done
text {*
If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
@{term Numeral0} IS @{term "number_of Pls"}
*}
lemma not_neg_number_of_Pls:
"~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
by (simp add: neg_def numeral_0_eq_0)
lemma neg_number_of_Min:
"neg (number_of Min ::'a::{ordered_idom,number_ring})"
by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
lemma double_less_0_iff:
"(a + a < 0) = (a < (0::'a::ordered_idom))"
proof -
have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
also have "... = (a < 0)"
by (simp add: mult_less_0_iff zero_less_two
order_less_not_sym [OF zero_less_two])
finally show ?thesis .
qed
lemma odd_less_0:
"(1 + z + z < 0) = (z < (0::int))";
proof (cases z rule: int_cases)
case (nonneg n)
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
thus ?thesis by (simp del: of_nat_Suc of_nat_add
add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
qed
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
then obtain z where a: "a = of_int z" ..
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
by (simp add: a)
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
also have "... = (a < 0)" by (simp add: a)
finally show ?thesis .
qed
lemma neg_number_of_BIT:
"neg (number_of (w BIT x)::'a) =
neg (number_of w :: 'a::{ordered_idom,number_ring})"
by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
Ints_odd_less_0 Ints_def split: bit.split)
text {* Less-Than or Equals *}
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
lemmas le_number_of_eq_not_less =
linorder_not_less [of "number_of w" "number_of v", symmetric,
standard]
lemma le_number_of_eq:
"((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
= (~ (neg (number_of (y + uminus x) :: 'a)))"
by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
text {* Absolute value (@{term abs}) *}
lemma abs_number_of:
"abs(number_of x::'a::{ordered_idom,number_ring}) =
(if number_of x < (0::'a) then -number_of x else number_of x)"
by (simp add: abs_if)
text {* Re-orientation of the equation nnn=x *}
lemma number_of_reorient:
"(number_of w = x) = (x = number_of w)"
by auto
subsection {* Simplification of arithmetic operations on integer constants. *}
lemmas arith_extra_simps [standard, simp] =
number_of_add [symmetric]
number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
number_of_mult [symmetric]
diff_number_of_eq abs_number_of
text {*
For making a minimal simpset, one must include these default simprules.
Also include @{text simp_thms}.
*}
lemmas arith_simps =
bit.distinct
Pls_0_eq Min_1_eq
pred_Pls pred_Min pred_1 pred_0
succ_Pls succ_Min succ_1 succ_0
add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
minus_Pls minus_Min minus_1 minus_0
mult_Pls mult_Min mult_num1 mult_num0
add_Pls_right add_Min_right
abs_zero abs_one arith_extra_simps
text {* Simplification of relational operations *}
lemmas rel_simps [simp] =
eq_number_of_eq iszero_0 nonzero_number_of_Min
iszero_number_of_0 iszero_number_of_1
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
le_number_of_eq
(* iszero_number_of_Pls would never be used
because its lhs simplifies to "iszero 0" *)
subsection {* Simplification of arithmetic when nested to the right. *}
lemma add_number_of_left [simp]:
"number_of v + (number_of w + z) =
(number_of(v + w) + z::'a::number_ring)"
by (simp add: add_assoc [symmetric])
lemma mult_number_of_left [simp]:
"number_of v * (number_of w * z) =
(number_of(v * w) * z::'a::number_ring)"
by (simp add: mult_assoc [symmetric])
lemma add_number_of_diff1:
"number_of v + (number_of w - c) =
number_of(v + w) - (c::'a::number_ring)"
by (simp add: diff_minus add_number_of_left)
lemma add_number_of_diff2 [simp]:
"number_of v + (c - number_of w) =
number_of (v + uminus w) + (c::'a::number_ring)"
apply (subst diff_number_of_eq [symmetric])
apply (simp only: compare_rls)
done
subsection {* Configuration of the code generator *}
instance int :: eq ..
code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
definition
int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
"int_aux n i = int n + i"
lemma [code]:
"int_aux 0 i = i"
"int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
by (simp add: int_aux_def)+
lemma [code, code unfold, code inline del]:
"int n = int_aux n 0"
by (simp add: int_aux_def)
definition
nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
"nat_aux i n = nat i + n"
lemma [code]:
"nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *}
by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
dest: zless_imp_add1_zle)
lemma [code]: "nat i = nat_aux i 0"
by (simp add: nat_aux_def)
lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
"(0\<Colon>int) = Numeral0"
by simp
lemma one_is_num_one [code func, code inline, symmetric, code post]:
"(1\<Colon>int) = Numeral1"
by simp
code_modulename SML
IntDef Integer
code_modulename OCaml
IntDef Integer
code_modulename Haskell
IntDef Integer
code_modulename SML
Numeral Integer
code_modulename OCaml
Numeral Integer
code_modulename Haskell
Numeral Integer
types_code
"int" ("int")
attach (term_of) {*
val term_of_int = HOLogic.mk_number HOLogic.intT;
*}
attach (test) {*
fun gen_int i = one_of [~1, 1] * random_range 0 i;
*}
setup {*
let
fun strip_number_of (@{term "Numeral.number_of :: int => int"} $ t) = t
| strip_number_of t = t;
fun numeral_codegen thy defs gr dep module b t =
let val i = HOLogic.dest_numeral (strip_number_of t)
in
SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
Pretty.str (string_of_int i))
end handle TERM _ => NONE;
in
Codegen.add_codegen "numeral_codegen" numeral_codegen
end
*}
consts_code
"number_of :: int \<Rightarrow> int" ("(_)")
"0 :: int" ("0")
"1 :: int" ("1")
"uminus :: int => int" ("~")
"op + :: int => int => int" ("(_ +/ _)")
"op * :: int => int => int" ("(_ */ _)")
"op \<le> :: int => int => bool" ("(_ <=/ _)")
"op < :: int => int => bool" ("(_ </ _)")
quickcheck_params [default_type = int]
(*setup continues in theory Presburger*)
hide (open) const Pls Min B0 B1 succ pred
end