Tuned looping simp rules in semiring_div

--- a/src/HOL/Divides.thy	Wed Jul 13 15:46:52 2016 +0200
+++ b/src/HOL/Divides.thy	Thu Jul 14 14:43:09 2016 +0200
@@ -128,12 +128,12 @@
   "a mod a = 0"
   using mod_mult_self2_is_0 [of 1] by simp
 
-lemma div_add_self1 [simp]:
+lemma div_add_self1:
   assumes "b \<noteq> 0"
   shows "(b + a) div b = a div b + 1"
   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
 
-lemma div_add_self2 [simp]:
+lemma div_add_self2:
   assumes "b \<noteq> 0"
   shows "(a + b) div b = a div b + 1"
   using assms div_add_self1 [of b a] by (simp add: add.commute)
@@ -1116,7 +1116,7 @@
 proof -
   from \<open>m \<ge> n\<close> obtain q where "m = n + q"
     by (auto simp add: le_iff_add)
-  with \<open>n > 0\<close> show ?thesis by simp
+  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
 qed
 
 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
@@ -2154,7 +2154,7 @@
 proof -
   have "k = (k - l) + l" by simp
   then obtain j where k: "k = j + l" ..
-  with assms show ?thesis by simp
+  with assms show ?thesis by (simp add: div_add_self2)
 qed
 
 lemma mod_pos_geq:

--- a/src/HOL/Number_Theory/Polynomial_Factorial.thy	Wed Jul 13 15:46:52 2016 +0200
+++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy	Thu Jul 14 14:43:09 2016 +0200
@@ -1343,6 +1343,7 @@
   by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
 end
 
+
 instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
   by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
 

--- a/src/HOL/Rat.thy	Wed Jul 13 15:46:52 2016 +0200
+++ b/src/HOL/Rat.thy	Thu Jul 14 14:43:09 2016 +0200
@@ -200,6 +200,17 @@
 
 end
 
+(* We cannot state these two rules earlier because of pending sort hypotheses *)
+lemma div_add_self1_no_field [simp]:
+  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
+  shows "(b + a) div b = a div b + 1"
+  using assms(2) by (fact div_add_self1)
+
+lemma div_add_self2_no_field [simp]:
+  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
+  shows "(a + b) div b = a div b + 1"
+  using assms(2) by (fact div_add_self2)
+
 lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
   by (induct k) (simp_all add: Zero_rat_def One_rat_def)