# HG changeset patch
# User haftmann
# Date 1507494500 -7200
# Node ID f3fda9777f9a0259ee4768683c7df97ff8d9b859
# Parent  128e9ed9f63c8db568a0982603646b4a0c2a8cb7
avoid fact name clashes

diff -r 128e9ed9f63c -r f3fda9777f9a NEWS
--- 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 ***
 
diff -r 128e9ed9f63c -r f3fda9777f9a src/HOL/Code_Numeral.thy
--- 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)
 
diff -r 128e9ed9f63c -r f3fda9777f9a src/HOL/Divides.thy
--- 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"
diff -r 128e9ed9f63c -r f3fda9777f9a src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- 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
diff -r 128e9ed9f63c -r f3fda9777f9a src/HOL/Word/Word_Miscellaneous.thy
--- 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>