--- a/NEWS Sun Oct 08 22:28:19 2017 +0200
+++ b/NEWS Sun Oct 08 22:28:20 2017 +0200
@@ -44,6 +44,9 @@
higher-order quantifiers. An 'smt_explicit_application' option has been
added to control this. INCOMPATIBILITY.
+* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
+with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:20 2017 +0200
@@ -446,11 +446,11 @@
where
"divmod_integer k l = (k div l, k mod l)"
-lemma fst_divmod [simp]:
+lemma fst_divmod_integer [simp]:
"fst (divmod_integer k l) = k div l"
by (simp add: divmod_integer_def)
-lemma snd_divmod [simp]:
+lemma snd_divmod_integer [simp]:
"snd (divmod_integer k l) = k mod l"
by (simp add: divmod_integer_def)
--- a/src/HOL/Divides.thy Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Divides.thy Sun Oct 08 22:28:20 2017 +0200
@@ -1627,12 +1627,8 @@
from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
qed
-lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
-proof -
- have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
- also have "... = Suc m mod n" by (rule mod_mult_self3)
- finally show ?thesis .
-qed
+lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
+ using mod_mult_self3 [of k n "Suc m"] by simp
lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
apply (subst mod_Suc [of m])
@@ -2004,6 +2000,10 @@
apply (auto simp add: eucl_rel_int_iff)
done
+lemma div_positive_int:
+ "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
+ using that by (simp add: divide_int_def div_positive)
+
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)
lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a"
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun Oct 08 22:28:20 2017 +0200
@@ -381,7 +381,7 @@
from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x"
by force
from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
- by (auto simp: semiring_numeral_div_class.div_less)
+ by (auto simp: div_pos_pos_trivial)
with * show "f_3 (g_3 x) = x"
by (simp add: f_3_def g_3_def)
qed
--- a/src/HOL/Word/Word_Miscellaneous.thy Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sun Oct 08 22:28:20 2017 +0200
@@ -248,9 +248,7 @@
lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
-lemma int_mod_le: "0 \<le> a \<Longrightarrow> a mod n \<le> a"
- for a :: int
- by (fact Divides.semiring_numeral_div_class.mod_less_eq_dividend) (* FIXME: delete *)
+lemmas int_mod_le = zmod_le_nonneg_dividend (* FIXME: delete *)
lemma mod_add_if_z:
"x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>