introduced mk/dest_numeral/number for mk/dest_binum etc.
(* Title: HOL/Integ/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 IntDef Datatype
uses "../Tools/numeral_syntax.ML"
begin
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/Integ/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"}.
*}
text{*
This datatype avoids the use of type @{typ bool}, which would make
all of the rewrite rules higher-order.
*}
datatype bit = B0 | B1
definition
Pls :: int where
"Pls = 0"
definition
Min :: int where
"Min = - 1"
definition
Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
"k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
class number = -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
syntax
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
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 ..
lemma Let_0 [simp]: "Let 0 f = f 0"
unfolding Let_def ..
lemma Let_1 [simp]: "Let 1 f = f 1"
unfolding Let_def ..
definition
succ :: "int \<Rightarrow> int" where
"succ k = k + 1"
definition
pred :: "int \<Rightarrow> int" where
"pred k = k - 1"
lemmas numeral_simps =
succ_def pred_def Pls_def Min_def Bit_def
text {* Removal of leading zeroes *}
lemma Pls_0_eq [simp, code func]:
"Pls BIT B0 = Pls"
unfolding numeral_simps by simp
lemma Min_1_eq [simp, code func]:
"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} *}
axclass number_ring \<subseteq> number, comm_ring_1
number_of_eq: "number_of k = of_int k"
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 *}
lemma double_eq_0_iff:
"(a + a = 0) = (a = (0::'a::ordered_idom))"
proof -
have "a + a = (1 + 1) * a" unfolding left_distrib by simp
with zero_less_two [where 'a = 'a]
show ?thesis by force
qed
lemma le_imp_0_less:
assumes le: "0 \<le> z"
shows "(0::int) < 1 + z"
proof -
have "0 \<le> z" .
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_odd_nonzero:
assumes in_Ints: "a \<in> Ints"
shows "1 + a + a \<noteq> (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" ..
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::{ordered_idom,number_ring}))"
by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff
Ints_odd_nonzero Ints_def split: bit.split)
lemma iszero_number_of_0:
"iszero (number_of (w 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 B1)::'a::{ordered_idom,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: int_Suc
add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
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] =
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 =
eq_number_of_eq iszero_number_of_Pls 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
declare arith_extra_simps [simp]
declare rel_simps [simp]
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
hide (open) const Pls Min B0 B1 succ pred
end