--- a/src/HOL/Divides.thy Sat Jan 19 20:31:00 2019 +0100
+++ b/src/HOL/Divides.thy Sat Jan 19 20:40:17 2019 +0000
@@ -97,11 +97,11 @@
lemma zdiv_int:
"int (a div b) = int a div int b"
- by (simp add: divide_int_def sgn_1_pos)
+ by (simp add: divide_int_def)
lemma zmod_int:
"int (a mod b) = int a mod int b"
- by (simp add: modulo_int_def sgn_1_pos)
+ by (simp add: modulo_int_def)
lemma div_sgn_abs_cancel:
fixes k l v :: int
@@ -167,54 +167,40 @@
using assms
by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
-text\<open>Basic laws about division and remainder\<close>
-
-lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
- using eucl_rel_int [of a b]
- by (auto simp add: eucl_rel_int_iff prod_eq_iff)
-
-lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1]
- and pos_mod_bound = pos_mod_conj [THEN conjunct2]
-
-lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
- using eucl_rel_int [of a b]
- by (auto simp add: eucl_rel_int_iff prod_eq_iff)
-
-lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
- and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
-
subsubsection \<open>General Properties of div and mod\<close>
lemma div_pos_pos_trivial [simp]:
"k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
- using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
+ using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_pos_pos_trivial [simp]:
+ "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
+ using that by (simp add: mod_eq_self_iff_div_eq_0)
lemma div_neg_neg_trivial [simp]:
"k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
- using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
-
-lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1"
-apply (rule div_int_unique)
-apply (auto simp add: eucl_rel_int_iff)
-done
-
-(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)
-
-lemma mod_pos_pos_trivial [simp]:
- "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
- using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
+ using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
lemma mod_neg_neg_trivial [simp]:
"k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
- using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
+ using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_pos_neg_trivial:
+ "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
+ apply (rule div_int_unique [of _ _ _ "k + l"])
+ apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>)
+ done
-lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b"
-apply (rule_tac q = "-1" in mod_int_unique)
-apply (auto simp add: eucl_rel_int_iff)
-done
+lemma mod_pos_neg_trivial:
+ "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
+ apply (rule mod_int_unique [of _ _ "- 1"])
+ apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>)
+ done
-text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
+text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
+ because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
+
subsubsection \<open>Laws for div and mod with Unary Minus\<close>
@@ -345,15 +331,6 @@
qed (use assms in auto)
-subsubsection \<open>More Algebraic Laws for div and mod\<close>
-
-lemma zmod_eq_0_iff: "(m mod d = 0) = (\<exists>q::int. m = d*q)"
- by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
-
-(* REVISIT: should this be generalized to all semiring_div types? *)
-lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
-
-
subsubsection \<open>Proving \<^term>\<open>a div (b * c) = (a div b) div c\<close>\<close>
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but
@@ -697,7 +674,7 @@
proof (cases "l > 0")
case False
then show ?thesis
- by (simp add: dvd_eq_mod_eq_0) (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
+ by (simp add: dvd_eq_mod_eq_0) (use neg_mod_sign [of l k] in \<open>auto simp add: le_less not_less\<close>)
qed auto
text \<open>Simplify expressions in which div and mod combine numerical constants\<close>
@@ -1341,4 +1318,17 @@
lemma mod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
using that by (auto simp add: mod_eq_0_iff_dvd)
+lemma pos_mod_conj: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int
+ by simp
+
+lemma neg_mod_conj: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int
+ by simp
+
+lemma zmod_eq_0_iff: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int
+ by (auto simp add: mod_eq_0_iff_dvd)
+
+(* REVISIT: should this be generalized to all semiring_div types? *)
+lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
+ using that by auto
+
end
--- a/src/HOL/Euclidean_Division.thy Sat Jan 19 20:31:00 2019 +0100
+++ b/src/HOL/Euclidean_Division.thy Sat Jan 19 20:40:17 2019 +0000
@@ -125,6 +125,18 @@
"a mod b = 0" if "is_unit b"
using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
+lemma mod_eq_self_iff_div_eq_0:
+ "a mod b = a \<longleftrightarrow> a div b = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ with div_mult_mod_eq [of a b] show ?Q
+ by auto
+next
+ assume ?Q
+ with div_mult_mod_eq [of a b] show ?P
+ by simp
+qed
+
lemma coprime_mod_left_iff [simp]:
"coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
by (rule; rule coprimeI)
@@ -1646,11 +1658,28 @@
"k mod l < l" if "l > 0" for k l :: int
proof -
obtain m and s where "k = sgn s * int m"
- by (blast intro: int_sgnE elim: that)
+ by (rule int_sgnE)
moreover from that obtain n where "l = sgn 1 * int n"
- by (cases l) auto
+ by (cases l) simp_all
+ moreover from this that have "n > 0"
+ by simp
ultimately show ?thesis
- using that by (simp only: modulo_int_unfold)
+ by (simp only: modulo_int_unfold)
+ (simp add: mod_greater_zero_iff_not_dvd)
+qed
+
+lemma neg_mod_bound [simp]:
+ "l < k mod l" if "l < 0" for k l :: int
+proof -
+ obtain m and s where "k = sgn s * int m"
+ by (rule int_sgnE)
+ moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
+ by (cases l) simp_all
+ moreover define n where "n = Suc q"
+ then have "Suc q = n"
+ by simp
+ ultimately show ?thesis
+ by (simp only: modulo_int_unfold)
(simp add: mod_greater_zero_iff_not_dvd)
qed
@@ -1658,11 +1687,27 @@
"0 \<le> k mod l" if "l > 0" for k l :: int
proof -
obtain m and s where "k = sgn s * int m"
- by (blast intro: int_sgnE elim: that)
+ by (rule int_sgnE)
moreover from that obtain n where "l = sgn 1 * int n"
by (cases l) auto
+ moreover from this that have "n > 0"
+ by simp
ultimately show ?thesis
- using that by (simp only: modulo_int_unfold) simp
+ by (simp only: modulo_int_unfold) simp
+qed
+
+lemma neg_mod_sign [simp]:
+ "k mod l \<le> 0" if "l < 0" for k l :: int
+proof -
+ obtain m and s where "k = sgn s * int m"
+ by (rule int_sgnE)
+ moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
+ by (cases l) simp_all
+ moreover define n where "n = Suc q"
+ then have "Suc q = n"
+ by simp
+ ultimately show ?thesis
+ by (simp only: modulo_int_unfold) simp
qed