--- a/NEWS Thu Aug 18 09:29:11 2022 +0200
+++ b/NEWS Wed Aug 17 20:37:16 2022 +0000
@@ -39,7 +39,7 @@
* New Theory Code_Abstract_Char implements characters by target language
integers, sacrificing pattern patching in exchange for dramatically
-increased performance for comparisions.
+increased performance for comparisons.
* New theory HOL-Library.NList of fixed length lists
@@ -49,6 +49,9 @@
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
+* Streamlined primitive definitions of division and modulus on integers.
+INCOMPATIBILITY.
+
* Theory "HOL.Fun":
- Added predicate monotone_on and redefined monotone to be an
abbreviation. Lemma monotone_def is explicitly provided for backward
--- a/src/HOL/Bit_Operations.thy Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Bit_Operations.thy Wed Aug 17 20:37:16 2022 +0000
@@ -7,6 +7,15 @@
imports Presburger Groups_List
begin
+lemma half_nonnegative_int_iff [simp]:
+ \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+ by auto
+
+lemma half_negative_int_iff [simp]:
+ \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+ by auto
+
+
subsection \<open>Abstract bit structures\<close>
class semiring_bits = semiring_parity +
@@ -1465,7 +1474,7 @@
lemma not_int_div_2:
\<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
- by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib)
+ by (simp add: not_int_def)
lemma bit_not_int_iff:
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
@@ -1729,7 +1738,7 @@
case (odd k)
from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
show ?case
- by (simp add: and_int_rec [of _ l]) linarith
+ by (simp add: and_int_rec [of _ l])
qed
lemma or_nonnegative_int_iff [simp]:
@@ -1754,7 +1763,7 @@
case (even k)
from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
show ?case
- by (simp add: or_int_rec [of _ l]) linarith
+ by (simp add: or_int_rec [of _ l])
next
case (odd k)
from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
@@ -2173,22 +2182,6 @@
\<open>\<not> 2 ^ n \<le> (0::int)\<close>
by (simp add: power_le_zero_eq)
-lemma half_nonnegative_int_iff [simp]:
- \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-proof (cases \<open>k \<ge> 0\<close>)
- case True
- then show ?thesis
- by (auto simp add: divide_int_def sgn_1_pos)
-next
- case False
- then show ?thesis
- by (auto simp add: divide_int_def not_le elim!: evenE)
-qed
-
-lemma half_negative_int_iff [simp]:
- \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
- by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
lemma int_bit_bound:
fixes k :: int
obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
--- a/src/HOL/Divides.thy Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Divides.thy Wed Aug 17 20:37:16 2022 +0000
@@ -11,6 +11,43 @@
subsection \<open>More on division\<close>
+subsubsection \<open>Laws for div and mod with Unary Minus\<close>
+
+lemma zmod_zminus1_not_zero:
+ fixes k l :: int
+ shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+ by (simp add: mod_eq_0_iff_dvd)
+
+lemma zmod_zminus2_not_zero:
+ fixes k l :: int
+ shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+ by (simp add: mod_eq_0_iff_dvd)
+
+lemma zdiv_zminus1_eq_if:
+ \<open>(- a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+ if \<open>b \<noteq> 0\<close> for a b :: int
+ using that sgn_not_eq_imp [of b \<open>- a\<close>]
+ by (cases \<open>a = 0\<close>) (auto simp add: div_eq_div_abs [of \<open>- a\<close> b] div_eq_div_abs [of a b] sgn_eq_0_iff)
+
+lemma zdiv_zminus2_eq_if:
+ \<open>a div (- b) = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+ if \<open>b \<noteq> 0\<close> for a b :: int
+ using that by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
+
+lemma zmod_zminus1_eq_if:
+ \<open>(- a) mod b = (if a mod b = 0 then 0 else b - (a mod b))\<close>
+ for a b :: int
+ by (cases \<open>b = 0\<close>)
+ (auto simp flip: minus_div_mult_eq_mod simp add: zdiv_zminus1_eq_if algebra_simps)
+
+lemma zmod_zminus2_eq_if:
+ \<open>a mod (- b) = (if a mod b = 0 then 0 else (a mod b) - b)\<close>
+ for a b :: int
+ by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
+
+
+subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
+
inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
| eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
@@ -91,139 +128,20 @@
using unique_quotient [of k l] unique_remainder [of k l]
by auto
-lemma div_abs_eq_div_nat:
- "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
- by (simp add: divide_int_def)
-
-lemma mod_abs_eq_div_nat:
- "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
- by (simp add: modulo_int_def)
-
-lemma zdiv_int:
- "int (a div b) = int a div int b"
- by (simp add: divide_int_def)
-
-lemma zmod_int:
- "int (a mod b) = int a mod int b"
- by (simp add: modulo_int_def)
-
-lemma div_sgn_abs_cancel:
- fixes k l v :: int
- assumes "v \<noteq> 0"
- shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-proof -
- from assms have "sgn v = - 1 \<or> sgn v = 1"
- by (cases "v \<ge> 0") auto
- then show ?thesis
- using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
- by (fastforce simp add: not_less div_abs_eq_div_nat)
-qed
-
-lemma div_eq_sgn_abs:
- fixes k l v :: int
- assumes "sgn k = sgn l"
- shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
-proof (cases "l = 0")
- case True
- then show ?thesis
- by simp
-next
- case False
- with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
- using div_sgn_abs_cancel [of l k l] by simp
- then show ?thesis
- by (simp add: sgn_mult_abs)
-qed
-
-lemma div_dvd_sgn_abs:
- fixes k l :: int
- assumes "l dvd k"
- shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
-proof (cases "k = 0 \<or> l = 0")
- case True
- then show ?thesis
- by auto
-next
- case False
- then have "k \<noteq> 0" and "l \<noteq> 0"
- by auto
- show ?thesis
- proof (cases "sgn l = sgn k")
- case True
- then show ?thesis
- by (auto simp add: div_eq_sgn_abs)
- next
- case False
- with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
- have "sgn l * sgn k = - 1"
- by (simp add: sgn_if split: if_splits)
- with assms show ?thesis
- unfolding divide_int_def [of k l]
- by (auto simp add: zdiv_int ac_simps)
- qed
-qed
-
-lemma div_noneq_sgn_abs:
- fixes k l :: int
- assumes "l \<noteq> 0"
- assumes "sgn k \<noteq> sgn l"
- shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
- using assms
- by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
-
-
-subsubsection \<open>Laws for div and mod with Unary Minus\<close>
-
lemma zminus1_lemma:
"eucl_rel_int a b (q, r) ==> b \<noteq> 0
==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
if r=0 then 0 else b-r)"
by (force simp add: eucl_rel_int_iff right_diff_distrib)
-
-lemma zdiv_zminus1_eq_if:
- "b \<noteq> (0::int)
- \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)"
-by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
-
-lemma zmod_zminus1_eq_if:
- "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"
-proof (cases "b = 0")
- case False
- then show ?thesis
- by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
-qed auto
-
-lemma zmod_zminus1_not_zero:
- fixes k l :: int
- shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
- by (simp add: mod_eq_0_iff_dvd)
-
-lemma zmod_zminus2_not_zero:
- fixes k l :: int
- shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
- by (simp add: mod_eq_0_iff_dvd)
-
-lemma zdiv_zminus2_eq_if:
- "b \<noteq> (0::int)
- ==> a div (-b) =
- (if a mod b = 0 then - (a div b) else - (a div b) - 1)"
- by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
-
-lemma zmod_zminus2_eq_if:
- "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"
- by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
-
-
-subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
-
lemma zdiv_mono1:
- fixes b::int
- assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b"
+ \<open>a div b \<le> a' div b\<close>
+ if \<open>a \<le> a'\<close> \<open>0 < b\<close>
+ for a b b' :: int
proof (rule unique_quotient_lemma)
show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
- using assms(1) by auto
-qed (use assms in auto)
+ using \<open>a \<le> a'\<close> by auto
+qed (use that in auto)
lemma zdiv_mono1_neg:
fixes b::int
--- a/src/HOL/Euclidean_Division.thy Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy Wed Aug 17 20:37:16 2022 +0000
@@ -321,7 +321,7 @@
lemma div_plus_div_distrib_dvd_left:
"c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
- by (cases "c = 0") (auto elim: dvdE)
+ by (cases "c = 0") auto
lemma div_plus_div_distrib_dvd_right:
"c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
@@ -603,7 +603,7 @@
subsection \<open>Uniquely determined division\<close>
-
+
class unique_euclidean_semiring = euclidean_semiring +
assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
fixes division_segment :: "'a \<Rightarrow> 'a"
@@ -1499,26 +1499,20 @@
instantiation int :: normalization_semidom
begin
-definition normalize_int :: "int \<Rightarrow> int"
- where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int :: "int \<Rightarrow> int"
- where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+definition normalize_int :: \<open>int \<Rightarrow> int\<close>
+ where [simp]: \<open>normalize = (abs :: int \<Rightarrow> int)\<close>
-definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
- where "k div l = (if l = 0 then 0
- else if sgn k = sgn l
- then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
- else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
+definition unit_factor_int :: \<open>int \<Rightarrow> int\<close>
+ where [simp]: \<open>unit_factor = (sgn :: int \<Rightarrow> int)\<close>
+
+definition divide_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>k div l = (sgn k * sgn l * int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
+ - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
lemma divide_int_unfold:
- "(sgn k * int m) div (sgn l * int n) =
- (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
- else if sgn k = sgn l
- then int (m div n)
- else - int (m div n + of_bool (\<not> n dvd m)))"
- by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
- nat_mult_distrib)
+ \<open>(sgn k * int m) div (sgn l * int n) = (sgn k * sgn l * int (m div n)
+ - of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> l \<noteq> 0 \<and> n \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m))\<close>
+ by (simp add: divide_int_def sgn_mult nat_mult_distrib abs_mult sgn_eq_0_iff ac_simps)
instance proof
fix k :: int show "k div 0 = 0"
@@ -1537,6 +1531,21 @@
end
+lemma div_abs_eq_div_nat:
+ "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
+ by (auto simp add: divide_int_def)
+
+lemma div_eq_div_abs:
+ \<open>k div l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)
+ - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+ for k l :: int
+ by (simp add: divide_int_def [of k l] div_abs_eq_div_nat)
+
+lemma div_abs_eq:
+ \<open>\<bar>k\<bar> div \<bar>l\<bar> = sgn k * sgn l * (k div l + of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+ for k l :: int
+ by (simp add: div_eq_div_abs [of k l] ac_simps)
+
lemma coprime_int_iff [simp]:
"coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
proof
@@ -1598,34 +1607,38 @@
instantiation int :: idom_modulo
begin
-definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
- where "k mod l = (if l = 0 then k
- else if sgn k = sgn l
- then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
- else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
+definition modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>k mod l = sgn k * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
lemma modulo_int_unfold:
- "(sgn k * int m) mod (sgn l * int n) =
- (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
- else if sgn k = sgn l
- then sgn l * int (m mod n)
- else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
- by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
- nat_mult_distrib)
+ \<open>(sgn k * int m) mod (sgn l * int n) =
+ sgn k * int (m mod (of_bool (l \<noteq> 0) * n)) + (sgn l * int n) * of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m)\<close>
+ by (auto simp add: modulo_int_def sgn_mult abs_mult)
instance proof
fix k l :: int
obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
by (blast intro: int_sgnE elim: that)
then show "k div l * l + k mod l = k"
- by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
- (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
- distrib_left [symmetric] minus_mult_right
- del: of_nat_mult minus_mult_right [symmetric])
+ by (simp add: divide_int_unfold modulo_int_unfold algebra_simps modulo_nat_def of_nat_diff)
qed
end
+lemma mod_abs_eq_div_nat:
+ "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
+ by (simp add: modulo_int_def)
+
+lemma mod_eq_mod_abs:
+ \<open>k mod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+ for k l :: int
+ by (simp add: modulo_int_def [of k l] mod_abs_eq_div_nat)
+
+lemma mod_abs_eq:
+ \<open>\<bar>k\<bar> mod \<bar>l\<bar> = sgn k * (k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+ for k l :: int
+ by (auto simp: mod_eq_mod_abs [of k l])
+
instantiation int :: unique_euclidean_ring
begin
@@ -1649,8 +1662,9 @@
obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
by (blast intro: int_sgnE elim: that)
with that show ?thesis
- by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
- abs_mult mod_greater_zero_iff_not_dvd)
+ by (auto simp add: modulo_int_unfold abs_mult mod_greater_zero_iff_not_dvd
+ simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
+ (simp add: sgn_0_0)
qed
lemma sgn_mod:
@@ -1659,8 +1673,8 @@
obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
by (blast intro: int_sgnE elim: that)
with that show ?thesis
- by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg sgn_mult)
- (simp add: dvd_eq_mod_eq_0)
+ by (auto simp add: modulo_int_unfold sgn_mult mod_greater_zero_iff_not_dvd
+ simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
qed
instance proof
@@ -1700,8 +1714,8 @@
from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
using q l by (simp add: ac_simps sgn_mult)
from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
- by (simp only: *, simp only: q l divide_int_unfold)
- (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
+ by (simp only: *, simp only: * q l divide_int_unfold)
+ (auto simp add: sgn_mult ac_simps)
qed
next
case False
@@ -1728,6 +1742,12 @@
end
+lemma div_sgn_abs_cancel:
+ fixes k l v :: int
+ assumes "v \<noteq> 0"
+ shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
+ using assms by (simp add: sgn_mult abs_mult sgn_0_0 of_nat_div divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"])
+
lemma pos_mod_bound [simp]:
"k mod l < l" if "l > 0" for k l :: int
proof -
@@ -1739,7 +1759,7 @@
by simp
ultimately show ?thesis
by (simp only: modulo_int_unfold)
- (simp add: mod_greater_zero_iff_not_dvd)
+ (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_pos)
qed
lemma neg_mod_bound [simp]:
@@ -1754,7 +1774,7 @@
by simp
ultimately show ?thesis
by (simp only: modulo_int_unfold)
- (simp add: mod_greater_zero_iff_not_dvd)
+ (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_neg)
qed
lemma pos_mod_sign [simp]:
@@ -1767,7 +1787,7 @@
moreover from this that have "n > 0"
by simp
ultimately show ?thesis
- by (simp only: modulo_int_unfold) simp
+ by (simp only: modulo_int_unfold) (auto simp add: sgn_1_pos)
qed
lemma neg_mod_sign [simp]:
@@ -1780,8 +1800,12 @@
moreover define n where "n = Suc q"
then have "Suc q = n"
by simp
+ moreover have \<open>int (m mod n) \<le> int n\<close>
+ using \<open>Suc q = n\<close> by simp
+ then have \<open>sgn s * int (m mod n) \<le> int n\<close>
+ by (cases s \<open>0::int\<close> rule: linorder_cases) simp_all
ultimately show ?thesis
- by (simp only: modulo_int_unfold) simp
+ by (simp only: modulo_int_unfold) auto
qed
lemma div_pos_pos_trivial [simp]:
@@ -2075,7 +2099,7 @@
proof (cases \<open>n \<le> m\<close>)
case True
then show ?thesis
- by (simp add: Suc_le_lessD min.absorb2)
+ by (simp add: Suc_le_lessD)
next
case False
then have \<open>m < n\<close>
@@ -2109,7 +2133,27 @@
by standard (simp_all add: dvd_eq_mod_eq_0)
instance int :: unique_euclidean_ring_with_nat
- by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
+ by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)
+
+lemma div_eq_sgn_abs:
+ fixes k l v :: int
+ assumes "sgn k = sgn l"
+ shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
+ using assms by (auto simp add: divide_int_def [of k l] of_nat_div)
+
+lemma div_dvd_sgn_abs:
+ fixes k l :: int
+ assumes "l dvd k"
+ shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
+ using assms by (auto simp add: divide_int_def [of k l] of_nat_div)
+
+lemma div_noneq_sgn_abs:
+ fixes k l :: int
+ assumes "l \<noteq> 0"
+ assumes "sgn k \<noteq> sgn l"
+ shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
+ using assms
+ by (simp only: divide_int_def [of k l]) (auto simp add: of_nat_div sgn_0_0 dest!: sgn_not_eq_imp)
lemma zdiv_zmult2_eq:
\<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
@@ -2135,6 +2179,14 @@
using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
qed
+lemma zdiv_int:
+ "int (a div b) = int a div int b"
+ by (fact of_nat_div)
+
+lemma zmod_int:
+ "int (a mod b) = int a mod int b"
+ by (fact of_nat_mod)
+
subsection \<open>Code generation\<close>
--- a/src/HOL/Library/Signed_Division.thy Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Library/Signed_Division.thy Wed Aug 17 20:37:16 2022 +0000
@@ -7,9 +7,58 @@
imports Main
begin
-class signed_division =
- fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "sdiv" 70)
- and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "smod" 70)
+lemma sgn_div_eq_sgn_mult:
+ \<open>sgn (a div b) = sgn (a * b)\<close>
+ if \<open>a div b \<noteq> 0\<close> for a b :: int
+proof -
+ have \<open>0 \<le> \<bar>a\<bar> div \<bar>b\<bar>\<close>
+ by (cases \<open>b = 0\<close>) (simp_all add: pos_imp_zdiv_nonneg_iff)
+ then have \<open>\<bar>a\<bar> div \<bar>b\<bar> \<noteq> 0 \<longleftrightarrow> 0 < \<bar>a\<bar> div \<bar>b\<bar>\<close>
+ by (simp add: less_le)
+ also have \<open>\<dots> \<longleftrightarrow> \<bar>a\<bar> \<ge> \<bar>b\<bar>\<close>
+ using that nonneg1_imp_zdiv_pos_iff by auto
+ finally have *: \<open>\<bar>a\<bar> div \<bar>b\<bar> \<noteq> 0 \<longleftrightarrow> \<bar>b\<bar> \<le> \<bar>a\<bar>\<close> .
+ show ?thesis
+ using \<open>0 \<le> \<bar>a\<bar> div \<bar>b\<bar>\<close> that
+ by (auto simp add: div_eq_div_abs [of a b] div_eq_sgn_abs [of a b]
+ sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp)
+qed
+
+class signed_division = comm_semiring_1_cancel +
+ fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70)
+ and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+ assumes sdiv_mult_smod_eq: \<open>a sdiv b * b + a smod b = a\<close>
+begin
+
+lemma mult_sdiv_smod_eq:
+ \<open>b * (a sdiv b) + a smod b = a\<close>
+ using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma smod_sdiv_mult_eq:
+ \<open>a smod b + a sdiv b * b = a\<close>
+ using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma smod_mult_sdiv_eq:
+ \<open>a smod b + b * (a sdiv b) = a\<close>
+ using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma minus_sdiv_mult_eq_smod:
+ \<open>a - a sdiv b * b = a smod b\<close>
+ by (rule add_implies_diff [symmetric]) (fact smod_sdiv_mult_eq)
+
+lemma minus_mult_sdiv_eq_smod:
+ \<open>a - b * (a sdiv b) = a smod b\<close>
+ by (rule add_implies_diff [symmetric]) (fact smod_mult_sdiv_eq)
+
+lemma minus_smod_eq_sdiv_mult:
+ \<open>a - a smod b = a sdiv b * b\<close>
+ by (rule add_implies_diff [symmetric]) (fact sdiv_mult_smod_eq)
+
+lemma minus_smod_eq_mult_sdiv:
+ \<open>a - a smod b = b * (a sdiv b)\<close>
+ by (rule add_implies_diff [symmetric]) (fact mult_sdiv_smod_eq)
+
+end
instantiation int :: signed_division
begin
@@ -18,12 +67,45 @@
where \<open>k sdiv l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)\<close> for k l :: int
definition signed_modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
- where \<open>k smod l = k - (k sdiv l) * l\<close> for k l :: int
+ where \<open>k smod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>)\<close> for k l :: int
-instance ..
+instance by standard
+ (simp add: signed_divide_int_def signed_modulo_int_def div_abs_eq mod_abs_eq algebra_simps)
end
+lemma divide_int_eq_signed_divide_int:
+ \<open>k div l = k sdiv l - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+ for k l :: int
+ by (simp add: div_eq_div_abs [of k l] signed_divide_int_def)
+
+lemma signed_divide_int_eq_divide_int:
+ \<open>k sdiv l = k div l + of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+ for k l :: int
+ by (simp add: divide_int_eq_signed_divide_int)
+
+lemma modulo_int_eq_signed_modulo_int:
+ \<open>k mod l = k smod l + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+ for k l :: int
+ by (simp add: mod_eq_mod_abs [of k l] signed_modulo_int_def)
+
+lemma signed_modulo_int_eq_modulo_int:
+ \<open>k smod l = k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+ for k l :: int
+ by (simp add: modulo_int_eq_signed_modulo_int)
+
+lemma sdiv_int_div_0:
+ "(x :: int) sdiv 0 = 0"
+ by (clarsimp simp: signed_divide_int_def)
+
+lemma sdiv_int_0_div [simp]:
+ "0 sdiv (x :: int) = 0"
+ by (clarsimp simp: signed_divide_int_def)
+
+lemma smod_int_alt_def:
+ "(a::int) smod b = sgn (a) * (abs a mod abs b)"
+ by (fact signed_modulo_int_def)
+
lemma int_sdiv_simps [simp]:
"(a :: int) sdiv 1 = a"
"(a :: int) sdiv 0 = 0"
@@ -31,11 +113,13 @@
apply (auto simp: signed_divide_int_def sgn_if)
done
-lemma sgn_div_eq_sgn_mult:
- "a div b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) div b) = sgn (a * b)"
- apply (clarsimp simp: sgn_if zero_le_mult_iff neg_imp_zdiv_nonneg_iff not_less)
- apply (metis less_le mult_le_0_iff neg_imp_zdiv_neg_iff not_less pos_imp_zdiv_neg_iff zdiv_eq_0_iff)
- done
+lemma smod_int_mod_0 [simp]:
+ "x smod (0 :: int) = x"
+ by (clarsimp simp: signed_modulo_int_def abs_mult_sgn ac_simps)
+
+lemma smod_int_0_mod [simp]:
+ "0 smod (x :: int) = 0"
+ by (clarsimp simp: smod_int_alt_def)
lemma sgn_sdiv_eq_sgn_mult:
"a sdiv b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) sdiv b) = sgn (a * b)"
@@ -71,38 +155,17 @@
done
lemma sdiv_int_range:
- "(a :: int) sdiv b \<in> { - (abs a) .. (abs a) }"
- apply (unfold signed_divide_int_def)
- apply (subgoal_tac "(abs a) div (abs b) \<le> (abs a)")
- apply (auto simp add: sgn_if not_less)
- apply (metis le_less le_less_trans neg_equal_0_iff_equal neg_less_iff_less not_le pos_imp_zdiv_neg_iff)
- apply (metis add.inverse_neutral div_int_pos_iff le_less neg_le_iff_le order_trans)
- apply (metis div_minus_right le_less_trans neg_imp_zdiv_neg_iff neg_less_0_iff_less not_le)
- using div_int_pos_iff apply fastforce
- apply (auto simp add: abs_if not_less)
- apply (metis add.inverse_inverse add_0_left div_by_1 div_minus_right less_le neg_0_le_iff_le not_le not_one_le_zero zdiv_mono2 zless_imp_add1_zle)
- apply (metis div_by_1 neg_0_less_iff_less pos_imp_zdiv_pos_iff zdiv_mono2 zero_less_one)
- apply (metis add.inverse_neutral div_by_0 div_by_1 int_div_less_self int_one_le_iff_zero_less less_le less_minus_iff order_refl)
- apply (metis div_by_1 divide_int_def int_div_less_self less_le linorder_neqE_linordered_idom order_refl unique_euclidean_semiring_numeral_class.div_less)
- done
-
-lemma sdiv_int_div_0 [simp]:
- "(x :: int) sdiv 0 = 0"
- by (clarsimp simp: signed_divide_int_def)
-
-lemma sdiv_int_0_div [simp]:
- "0 sdiv (x :: int) = 0"
- by (clarsimp simp: signed_divide_int_def)
-
-lemma smod_int_alt_def:
- "(a::int) smod b = sgn (a) * (abs a mod abs b)"
- apply (clarsimp simp: signed_modulo_int_def signed_divide_int_def)
- apply (clarsimp simp: minus_div_mult_eq_mod [symmetric] abs_sgn sgn_mult sgn_if algebra_split_simps)
- done
+ \<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int
+ using zdiv_mono2 [of \<open>\<bar>a\<bar>\<close> 1 \<open>\<bar>b\<bar>\<close>]
+ by (cases \<open>b = 0\<close>; cases \<open>sgn b = sgn a\<close>)
+ (auto simp add: signed_divide_int_def pos_imp_zdiv_nonneg_iff
+ dest!: sgn_not_eq_imp intro: order_trans [of _ 0])
lemma smod_int_range:
- "b \<noteq> 0 \<Longrightarrow> (a::int) smod b \<in> { - abs b + 1 .. abs b - 1 }"
- apply (case_tac "b > 0")
+ \<open>a smod b \<in> {- \<bar>b\<bar> + 1..\<bar>b\<bar> - 1}\<close>
+ if \<open>b \<noteq> 0\<close> for a b :: int
+ using that
+ apply (cases \<open>b > 0\<close>)
apply (insert pos_mod_conj [where a=a and b=b])[1]
apply (insert pos_mod_conj [where a="-a" and b=b])[1]
apply (auto simp: smod_int_alt_def algebra_simps sgn_if
@@ -129,14 +192,6 @@
apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
done
-lemma smod_int_mod_0 [simp]:
- "x smod (0 :: int) = x"
- by (clarsimp simp: signed_modulo_int_def)
-
-lemma smod_int_0_mod [simp]:
- "0 smod (x :: int) = 0"
- by (clarsimp simp: smod_int_alt_def)
-
lemma smod_mod_positive:
"\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"
by (clarsimp simp: smod_int_alt_def zsgn_def)
--- a/src/HOL/Rings.thy Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Rings.thy Wed Aug 17 20:37:16 2022 +0000
@@ -2567,6 +2567,10 @@
"sgn a * sgn a = of_bool (a \<noteq> 0)"
by (cases "a > 0") simp_all
+lemma left_sgn_mult_self_eq [simp]:
+ \<open>sgn a * (sgn a * b) = of_bool (a \<noteq> 0) * b\<close>
+ by (simp flip: mult.assoc)
+
lemma abs_mult_self_eq [simp]:
"\<bar>a\<bar> * \<bar>a\<bar> = a * a"
by (cases "a > 0") simp_all