# HG changeset patch # User eberlm # Date 1468500189 -7200 # Node ID 9c9a599498873c645dc559cb75a3d365f2970479 # Parent a3fe3250d05d9c9292ecc7407e1533e03510e66f Tuned looping simp rules in semiring_div diff -r a3fe3250d05d -r 9c9a59949887 src/HOL/Divides.thy --- 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 \ 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 \ 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 \m \ n\ obtain q where "m = n + q" by (auto simp add: le_iff_add) - with \n > 0\ show ?thesis by simp + with \n > 0\ show ?thesis by (simp add: div_add_self1) qed lemma div_eq_0_iff: "(a div b::nat) = 0 \ a < b \ 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: diff -r a3fe3250d05d -r 9c9a59949887 src/HOL/Number_Theory/Polynomial_Factorial.thy --- 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) diff -r a3fe3250d05d -r 9c9a59949887 src/HOL/Rat.thy --- 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) \ 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) \ 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)