avoid fact name clashes
authorhaftmann
Sun Oct 08 22:28:20 2017 +0200 (19 months ago)
changeset 66801f3fda9777f9a
parent 66800 128e9ed9f63c
child 66802 627511c13164
avoid fact name clashes
NEWS
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/NEWS	Sun Oct 08 22:28:19 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -44,6 +44,9 @@
     1.4      higher-order quantifiers. An 'smt_explicit_application' option has been
     1.5      added to control this. INCOMPATIBILITY.
     1.6  
     1.7 +* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
     1.8 +with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:19 2017 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:20 2017 +0200
     2.3 @@ -446,11 +446,11 @@
     2.4  where
     2.5    "divmod_integer k l = (k div l, k mod l)"
     2.6  
     2.7 -lemma fst_divmod [simp]:
     2.8 +lemma fst_divmod_integer [simp]:
     2.9    "fst (divmod_integer k l) = k div l"
    2.10    by (simp add: divmod_integer_def)
    2.11  
    2.12 -lemma snd_divmod [simp]:
    2.13 +lemma snd_divmod_integer [simp]:
    2.14    "snd (divmod_integer k l) = k mod l"
    2.15    by (simp add: divmod_integer_def)
    2.16  
     3.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:19 2017 +0200
     3.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:20 2017 +0200
     3.3 @@ -1627,12 +1627,8 @@
     3.4    from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
     3.5  qed
     3.6  
     3.7 -lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
     3.8 -proof -
     3.9 -  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
    3.10 -  also have "... = Suc m mod n" by (rule mod_mult_self3)
    3.11 -  finally show ?thesis .
    3.12 -qed
    3.13 +lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
    3.14 +  using mod_mult_self3 [of k n "Suc m"] by simp
    3.15  
    3.16  lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
    3.17  apply (subst mod_Suc [of m])
    3.18 @@ -2004,6 +2000,10 @@
    3.19  apply (auto simp add: eucl_rel_int_iff)
    3.20  done
    3.21  
    3.22 +lemma div_positive_int:
    3.23 +  "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
    3.24 +  using that by (simp add: divide_int_def div_positive)
    3.25 +
    3.26  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
    3.27  
    3.28  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
     4.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 08 22:28:19 2017 +0200
     4.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 08 22:28:20 2017 +0200
     4.3 @@ -381,7 +381,7 @@
     4.4        from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x"
     4.5          by force
     4.6        from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
     4.7 -        by (auto simp: semiring_numeral_div_class.div_less)
     4.8 +        by (auto simp: div_pos_pos_trivial)
     4.9        with * show "f_3 (g_3 x) = x"
    4.10          by (simp add: f_3_def g_3_def)
    4.11      qed
     5.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:19 2017 +0200
     5.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:20 2017 +0200
     5.3 @@ -248,9 +248,7 @@
     5.4  
     5.5  lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
     5.6  
     5.7 -lemma int_mod_le: "0 \<le> a \<Longrightarrow> a mod n \<le> a"
     5.8 -  for a :: int
     5.9 -  by (fact Divides.semiring_numeral_div_class.mod_less_eq_dividend) (* FIXME: delete *)
    5.10 +lemmas int_mod_le = zmod_le_nonneg_dividend (* FIXME: delete *)
    5.11  
    5.12  lemma mod_add_if_z:
    5.13    "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>