# 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 \ 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) \ 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 \ a \ a mod n \ 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 \ y < z \ 0 \ y \ 0 \ x \ 0 \ z \