--- 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>