# HG changeset patch # User haftmann # Date 1476603065 -7200 # Node ID 93c6f0da5c702d2dc7f4fcddfa147b9762f462ba # Parent 430d74089d4d1db75494c63ebdf80ba9af6a7c25 more standardized theorem names for facts involving the div and mod identity diff -r 430d74089d4d -r 93c6f0da5c70 NEWS --- a/NEWS Sun Oct 16 09:31:04 2016 +0200 +++ b/NEWS Sun Oct 16 09:31:05 2016 +0200 @@ -262,6 +262,14 @@ div_mult_self2_is_id ~> nonzero_mult_div_cancel_right is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right + mod_div_equality ~> div_mult_mod_eq + mod_div_equality2 ~> mult_div_mod_eq + mod_div_equality3 ~> mod_div_mult_eq + mod_div_equality4 ~> mod_mult_div_eq + minus_div_eq_mod ~> minus_div_mult_eq_mod + minus_div_eq_mod2 ~> minus_mult_div_eq_mod + minus_mod_eq_div ~> minus_mod_eq_div_mult + minus_mod_eq_div2 ~> minus_mod_eq_mult_div INCOMPATIBILITY. * Dedicated syntax LENGTH('a) for length of types. diff -r 430d74089d4d -r 93c6f0da5c70 src/Doc/Tutorial/Rules/Force.thy --- a/src/Doc/Tutorial/Rules/Force.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/Doc/Tutorial/Rules/Force.thy Sun Oct 16 09:31:05 2016 +0200 @@ -6,7 +6,7 @@ lemma div_mult_self_is_m: "0 (m*n) div n = (m::nat)" -apply (insert mod_div_equality [of "m*n" n]) +apply (insert div_mult_mod_eq [of "m*n" n]) apply simp done diff -r 430d74089d4d -r 93c6f0da5c70 src/Doc/Tutorial/Rules/Forward.thy --- a/src/Doc/Tutorial/Rules/Forward.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/Doc/Tutorial/Rules/Forward.thy Sun Oct 16 09:31:05 2016 +0200 @@ -183,8 +183,8 @@ Another example of "insert" -@{thm[display] mod_div_equality} -\rulename{mod_div_equality} +@{thm[display] div_mult_mod_eq} +\rulename{div_mult_mod_eq} *} (*MOVED to Force.thy, which now depends only on Divides.thy diff -r 430d74089d4d -r 93c6f0da5c70 src/Doc/Tutorial/Types/Numbers.thy --- a/src/Doc/Tutorial/Types/Numbers.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/Doc/Tutorial/Types/Numbers.thy Sun Oct 16 09:31:05 2016 +0200 @@ -86,8 +86,8 @@ @{thm[display] mod_if[no_vars]} \rulename{mod_if} -@{thm[display] mod_div_equality[no_vars]} -\rulename{mod_div_equality} +@{thm[display] div_mult_mod_eq[no_vars]} +\rulename{div_mult_mod_eq} @{thm[display] div_mult1_eq[no_vars]} diff -r 430d74089d4d -r 93c6f0da5c70 src/Doc/Tutorial/document/numerics.tex --- a/src/Doc/Tutorial/document/numerics.tex Sun Oct 16 09:31:04 2016 +0200 +++ b/src/Doc/Tutorial/document/numerics.tex Sun Oct 16 09:31:05 2016 +0200 @@ -143,7 +143,7 @@ m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) \rulename{mod_if}\isanewline m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% -\rulenamedx{mod_div_equality} +\rulenamedx{div_mult_mod_eq} \end{isabelle} Many less obvious facts about quotient and remainder are also provided. diff -r 430d74089d4d -r 93c6f0da5c70 src/Doc/Tutorial/document/rules.tex --- a/src/Doc/Tutorial/document/rules.tex Sun Oct 16 09:31:04 2016 +0200 +++ b/src/Doc/Tutorial/document/rules.tex Sun Oct 16 09:31:05 2016 +0200 @@ -2175,7 +2175,7 @@ remainder obey a well-known law: \begin{isabelle} (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m -\rulename{mod_div_equality} +\rulename{div_mult_mod_eq} \end{isabelle} We refer to this law explicitly in the following proof: @@ -2183,7 +2183,7 @@ \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline \ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\ (m::nat)"\isanewline -\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline +\isacommand{apply}\ (insert\ div_mult_mod_eq\ [of\ "m*n"\ n])\isanewline \isacommand{apply}\ (simp)\isanewline \isacommand{done} \end{isabelle} diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Data_Structures/RBT_Set.thy Sun Oct 16 09:31:05 2016 +0200 @@ -419,7 +419,7 @@ next case (2 h t t') with RB_mod obtain n where "2*n + 1 = h" - by (metis color.distinct(1) mod_div_equality2 parity) + by (metis color.distinct(1) mult_div_mod_eq parity) with 2 balB_h RB_h show ?case by auto next case (3 h t t') diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 09:31:05 2016 +0200 @@ -4426,7 +4426,7 @@ "n \ m \ real n \ real m" "n < m \ real n < real m" "n \ {m .. l} \ real n \ {real m .. real l}" - by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality') + by (simp_all add: real_div_nat_eq_floor_of_divide div_mult_mod_eq') ML_file "approximation.ML" diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200 @@ -56,7 +56,7 @@ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] val simpset0 = put_simpset HOL_basic_ss ctxt - addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms} + addsimps @{thms div_mult_mod_eq' Suc_eq_plus1 simp_thms} |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max} (* Simp rules for changing (n::int) to int n *) val simpset1 = diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200 @@ -31,7 +31,7 @@ @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}] val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms}); -val mod_div_equality' = @{thm "mod_div_equality'"}; +val div_mult_mod_eq' = @{thm "div_mult_mod_eq'"}; val mod_add_eq = @{thm "mod_add_eq"} RS sym; fun prepare_for_mir q fm = @@ -80,7 +80,7 @@ addsimps @{thms add.assoc add.commute add.left_commute} addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] val simpset0 = put_simpset HOL_basic_ss ctxt - addsimps [mod_div_equality', @{thm Suc_eq_plus1}] + addsimps [div_mult_mod_eq', @{thm Suc_eq_plus1}] addsimps comp_ths |> fold Splitter.add_split [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200 @@ -29,16 +29,16 @@ text \@{const divide} and @{const modulo}\ lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c" - by (simp add: mod_div_equality) + by (simp add: div_mult_mod_eq) lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c" - by (simp add: mod_div_equality2) + by (simp add: mult_div_mod_eq) lemma mod_by_0 [simp]: "a mod 0 = a" - using mod_div_equality [of a zero] by simp + using div_mult_mod_eq [of a zero] by simp lemma mod_0 [simp]: "0 mod a = 0" - using mod_div_equality [of zero a] div_0 by simp + using div_mult_mod_eq [of zero a] div_0 by simp lemma div_mult_self2 [simp]: assumes "b \ 0" @@ -61,14 +61,14 @@ next case False have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b" - by (simp add: mod_div_equality) + by (simp add: div_mult_mod_eq) also from False div_mult_self1 [of b a c] have "\ = (c + a div b) * b + (a + c * b) mod b" by (simp add: algebra_simps) finally have "a = a div b * b + (a + c * b) mod b" by (simp add: add.commute [of a] add.assoc distrib_right) then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b" - by (simp add: mod_div_equality) + by (simp add: div_mult_mod_eq) then show ?thesis by simp qed @@ -95,7 +95,7 @@ lemma mod_by_1 [simp]: "a mod 1 = 0" proof - - from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp + from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp then have "a + a mod 1 = a + 0" by simp then show ?thesis by (rule add_left_imp_eq) qed @@ -138,7 +138,7 @@ then show "a mod b = 0" by simp next assume "a mod b = 0" - with mod_div_equality [of a b] have "a div b * b = a" by simp + with div_mult_mod_eq [of a b] have "a div b * b = a" by simp then have "a = b * (a div b)" by (simp add: ac_simps) then show "b dvd a" .. qed @@ -157,7 +157,7 @@ hence "a div b + a mod b div b = (a mod b + a div b * b) div b" by (rule div_mult_self1 [symmetric]) also have "\ = a div b" - by (simp only: mod_div_equality3) + by (simp only: mod_div_mult_eq) also have "\ = a div b + 0" by simp finally show ?thesis @@ -170,7 +170,7 @@ have "a mod b mod b = (a mod b + a div b * b) mod b" by (simp only: mod_mult_self1) also have "\ = a mod b" - by (simp only: mod_div_equality3) + by (simp only: mod_div_mult_eq) finally show ?thesis . qed @@ -180,7 +180,7 @@ proof - from assms have "k dvd (m div n) * n + m mod n" by (simp only: dvd_add dvd_mult) - then show ?thesis by (simp add: mod_div_equality) + then show ?thesis by (simp add: div_mult_mod_eq) qed text \Addition respects modular equivalence.\ @@ -189,7 +189,7 @@ "(a + b) mod c = (a mod c + b) mod c" proof - have "(a + b) mod c = (a div c * c + a mod c + b) mod c" - by (simp only: mod_div_equality) + by (simp only: div_mult_mod_eq) also have "\ = (a mod c + b + a div c * c) mod c" by (simp only: ac_simps) also have "\ = (a mod c + b) mod c" @@ -201,7 +201,7 @@ "(a + b) mod c = (a + b mod c) mod c" proof - have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c" - by (simp only: mod_div_equality) + by (simp only: div_mult_mod_eq) also have "\ = (a + b mod c + b div c * c) mod c" by (simp only: ac_simps) also have "\ = (a + b mod c) mod c" @@ -230,7 +230,7 @@ "(a * b) mod c = ((a mod c) * b) mod c" proof - have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c" - by (simp only: mod_div_equality) + by (simp only: div_mult_mod_eq) also have "\ = (a mod c * b + a div c * b * c) mod c" by (simp only: algebra_simps) also have "\ = (a mod c * b) mod c" @@ -242,7 +242,7 @@ "(a * b) mod c = (a * (b mod c)) mod c" proof - have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c" - by (simp only: mod_div_equality) + by (simp only: div_mult_mod_eq) also have "\ = (a * (b mod c) + a * (b div c) * c) mod c" by (simp only: algebra_simps) also have "\ = (a * (b mod c)) mod c" @@ -287,7 +287,7 @@ also have "\ = (a div (c * k) * (c * k) + a mod (c * k)) mod c" by (simp only: ac_simps) also have "\ = a mod c" - by (simp only: mod_div_equality) + by (simp only: div_mult_mod_eq) finally show ?thesis . qed @@ -305,11 +305,11 @@ case True then show ?thesis by simp next case False - from mod_div_equality + from div_mult_mod_eq have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" . with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b) = c * a + c * (a mod b)" by (simp add: algebra_simps) - with mod_div_equality show ?thesis by simp + with div_mult_mod_eq show ?thesis by simp qed lemma mod_mult_mult2: @@ -357,7 +357,7 @@ lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b" proof - have "(- a) mod b = (- (a div b * b + a mod b)) mod b" - by (simp only: mod_div_equality) + by (simp only: div_mult_mod_eq) also have "\ = (- (a mod b) + - (a div b) * b) mod b" by (simp add: ac_simps) also have "\ = (- (a mod b)) mod b" @@ -467,7 +467,7 @@ case True then show ?thesis by simp next case False - from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" . + from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" . with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff) then have "1 div 2 = 0 \ 2 = 0" by simp @@ -502,7 +502,7 @@ next fix a assume "a mod 2 = 1" - then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp + then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp then show "\b. a = b + 1" .. qed @@ -528,7 +528,7 @@ lemma odd_two_times_div_two_succ [simp]: "odd a \ 2 * (a div 2) + 1 = a" - using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero) + using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero) end @@ -569,7 +569,7 @@ "b * (a div b) = a - a mod b" proof - have "b * (a div b) + a mod b = a" - using mod_div_equality [of a b] by (simp add: ac_simps) + using div_mult_mod_eq [of a b] by (simp add: ac_simps) then have "b * (a div b) + a mod b - a mod b = a - a mod b" by simp then show ?thesis @@ -1107,7 +1107,7 @@ fixes m n :: nat shows "m mod n \ m" proof (rule add_leD2) - from mod_div_equality have "m div n * n + m mod n = m" . + from div_mult_mod_eq have "m div n * n + m mod n = m" . then show "m div n * n + m mod n \ m" by auto qed @@ -1120,9 +1120,9 @@ lemma mod_1 [simp]: "m mod Suc 0 = 0" by (induct m) (simp_all add: mod_geq) -(* a simple rearrangement of mod_div_equality: *) +(* a simple rearrangement of div_mult_mod_eq: *) lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)" - using mod_div_equality2 [of n m] by arith + using mult_div_mod_eq [of n m] by arith lemma mod_le_divisor[simp]: "0 < n \ m mod n \ (n::nat)" apply (drule mod_less_divisor [where m = m]) @@ -1279,7 +1279,7 @@ assumes "m mod d = r" shows "\q. m = r + q * d" proof - - from mod_div_equality obtain q where "q * d + m mod d = m" by blast + from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast with assms have "m = r + q * d" by simp then show ?thesis .. qed @@ -1387,11 +1387,11 @@ qed qed -theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n" - using mod_div_equality [of m n] by arith +theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n" + using div_mult_mod_eq [of m n] by arith lemma div_mod_equality': "(m::nat) div n * n = m - m mod n" - using mod_div_equality [of m n] by arith + using div_mult_mod_eq [of m n] by arith (* FIXME: very similar to mult_div_cancel *) lemma div_eq_dividend_iff: "a \ 0 \ (a :: nat) div b = a \ b = 1" @@ -1812,7 +1812,7 @@ text\Basic laws about division and remainder\ lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" - by (fact mod_div_equality2 [symmetric]) + by (fact mult_div_mod_eq [symmetric]) lemma zdiv_int: "int (a div b) = int a div int b" by (simp add: divide_int_def) @@ -2051,7 +2051,7 @@ lemma zmod_zdiv_equality' [nitpick_unfold]: "(m::int) mod n = m - (m div n) * n" - using mod_div_equality [of m n] by arith + using div_mult_mod_eq [of m n] by arith subsubsection \Proving @{term "a div (b * c) = (a div b) div c"}\ @@ -2282,7 +2282,7 @@ shows "i mod k = i \ k = 0 \ 0 \ i \ i < k \ i \ 0 \ k < i" proof - have "i mod k = i \ i div k = 0" - by safe (insert mod_div_equality [of i k], auto) + by safe (insert div_mult_mod_eq [of i k], auto) with zdiv_eq_0_iff show ?thesis by simp diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/GCD.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1920,7 +1920,7 @@ apply (simp add: bezw_non_0 gcd_non_0_nat) apply (erule subst) apply (simp add: field_simps) - apply (subst mod_div_equality [of m n, symmetric]) + apply (subst div_mult_mod_eq [of m n, symmetric]) (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *) apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult) done diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 16 09:31:05 2016 +0200 @@ -347,10 +347,10 @@ lemma mod_lemma: "\ (c::nat) \ a; a < b; b - c < n \ \ b mod n \ a mod n" apply(subgoal_tac "b=b div n*n + b mod n" ) - prefer 2 apply (simp add: mod_div_equality [symmetric]) + prefer 2 apply (simp add: div_mult_mod_eq [symmetric]) apply(subgoal_tac "a=a div n*n + a mod n") prefer 2 - apply(simp add: mod_div_equality [symmetric]) + apply(simp add: div_mult_mod_eq [symmetric]) apply(subgoal_tac "b - a \ b - c") prefer 2 apply arith apply(drule le_less_trans) diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Library/Code_Target_Int.thy Sun Oct 16 09:31:05 2016 +0200 @@ -115,7 +115,7 @@ j = k mod 2 in if j = 0 then l else l + 1)" proof - - from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp + from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp show ?thesis by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute) qed diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Library/Code_Target_Nat.thy --- a/src/HOL/Library/Code_Target_Nat.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Library/Code_Target_Nat.thy Sun Oct 16 09:31:05 2016 +0200 @@ -115,7 +115,7 @@ m' = 2 * of_nat m in if q = 0 then m' else m' + 1)" proof - - from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp + from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp show ?thesis by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric]) (simp add: * mult.commute of_nat_mult add.commute) diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1302,13 +1302,13 @@ proof (cases "f div g * g = 0") assume "f div g * g \ 0" hence [simp]: "f div g \ 0" "g \ 0" by auto - from mod_div_equality[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps) + from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps) also from assms have "subdegree ... = subdegree f" by (intro subdegree_diff_eq1) simp_all finally show ?thesis . next assume zero: "f div g * g = 0" - from mod_div_equality[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps) + from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps) also note zero finally show ?thesis by simp qed diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1038,7 +1038,7 @@ thus "is_unit (unit_factor_field_poly p)" by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff) qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult - euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le) + euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) lemma field_poly_irreducible_imp_prime: assumes "irreducible (p :: 'a :: field poly)" @@ -1356,7 +1356,7 @@ "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" instance - by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le) + by standard (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) end diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Library/Stream.thy --- a/src/HOL/Library/Stream.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Library/Stream.thy Sun Oct 16 09:31:05 2016 +0200 @@ -336,7 +336,7 @@ lemma stake_cycle: "u \ [] \ stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u" - by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto + by (subst div_mult_mod_eq[of n "length u", symmetric], unfold stake_add[symmetric]) auto lemma sdrop_cycle: "u \ [] \ sdrop n (cycle u) = cycle (rotate (n mod length u) u)" by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric]) diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Nonstandard_Analysis/StarDef.thy --- a/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 16 09:31:05 2016 +0200 @@ -863,7 +863,7 @@ by (intro_classes; transfer) simp_all instance star :: (semiring_div) semiring_div - by (intro_classes; transfer) (simp_all add: mod_div_equality) + by (intro_classes; transfer) (simp_all add: div_mult_mod_eq) instance star :: (ring_no_zero_divisors) ring_no_zero_divisors .. instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200 @@ -27,7 +27,7 @@ begin lemma mod_0 [simp]: "0 mod a = 0" - using mod_div_equality [of 0 a] by simp + using div_mult_mod_eq [of 0 a] by simp lemma dvd_mod_iff: assumes "k dvd n" @@ -36,7 +36,7 @@ from assms have "(k dvd m mod n) \ (k dvd ((m div n) * n + m mod n))" by (simp add: dvd_add_right_iff) also have "(m div n) * n + m mod n = m" - using mod_div_equality [of m n] by simp + using div_mult_mod_eq [of m n] by simp finally show ?thesis . qed @@ -46,7 +46,7 @@ proof - have "b dvd ((a div b) * b)" by simp also have "(a div b) * b = a" - using mod_div_equality [of a b] by (simp add: assms) + using div_mult_mod_eq [of a b] by (simp add: assms) finally show ?thesis . qed @@ -72,7 +72,7 @@ obtains s and t where "a = s * b + t" and "euclidean_size t < euclidean_size b" proof - - from mod_div_equality [of a b] + from div_mult_mod_eq [of a b] have "a = a div b * b + a mod b" by simp with that and assms show ?thesis by (auto simp add: mod_size_less) qed @@ -507,7 +507,7 @@ (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps) also have "s' * a + t' * b = r'" by fact also have "s * a + t * b = r" by fact - also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r] + also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r] by (simp add: algebra_simps) finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" . qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality') diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Number_Theory/Pocklington.thy --- a/src/HOL/Number_Theory/Pocklington.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Number_Theory/Pocklington.thy Sun Oct 16 09:31:05 2016 +0200 @@ -227,7 +227,7 @@ {assume nm1: "(n - 1) mod m > 0" from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast let ?y = "a^ ((n - 1) div m * m)" - note mdeq = mod_div_equality[of "(n - 1)" m] + note mdeq = div_mult_mod_eq[of "(n - 1)" m] have yn: "coprime ?y n" by (metis an(1) coprime_exp gcd.commute) have "?y mod n = (a^m)^((n - 1) div m) mod n" @@ -239,7 +239,7 @@ finally have th3: "?y mod n = 1" . have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)" using an1[unfolded cong_nat_def onen] onen - mod_div_equality[of "(n - 1)" m, symmetric] + div_mult_mod_eq[of "(n - 1)" m, symmetric] by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def) have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)" by (metis cong_mult_rcancel_nat mult.commute th2 yn) @@ -362,7 +362,7 @@ by (metis cong_exp_nat ord power_one) from H have onz: "?o \ 0" by (simp add: ord_eq_0) hence op: "?o > 0" by simp - from mod_div_equality[of d "ord n a"] lh + from div_mult_mod_eq[of d "ord n a"] lh have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute) hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric]) @@ -618,7 +618,7 @@ {assume b0: "b = 0" from p(2) nqr have "(n - 1) mod p = 0" by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0) - with mod_div_equality[of "n - 1" p] + with div_mult_mod_eq[of "n - 1" p] have "(n - 1) div p * p= n - 1" by auto hence eq: "(a^((n - 1) div p))^p = a^(n - 1)" by (simp only: power_mult[symmetric]) @@ -720,7 +720,7 @@ unfolding arnb[symmetric] power_mod by (simp_all add: power_mult[symmetric] algebra_simps) from n have n0: "n > 0" by arith - from mod_div_equality[of "a^(n - 1)" n] + from div_mult_mod_eq[of "a^(n - 1)" n] mod_less_divisor[OF n0, of "a^(n - 1)"] have an1: "[a ^ (n - 1) = 1] (mod n)" by (metis bqn cong_nat_def mod_mod_trivial) diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Old_Number_Theory/Pocklington.thy --- a/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 09:31:05 2016 +0200 @@ -744,7 +744,7 @@ {assume nm1: "(n - 1) mod m > 0" from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast let ?y = "a^ ((n - 1) div m * m)" - note mdeq = mod_div_equality[of "(n - 1)" m] + note mdeq = div_mult_mod_eq[of "(n - 1)" m] from coprime_exp[OF an(1)[unfolded coprime_commute[of a n]], of "(n - 1) div m * m"] have yn: "coprime ?y n" by (simp add: coprime_commute) @@ -757,7 +757,7 @@ finally have th3: "?y mod n = 1" . have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)" using an1[unfolded modeq_def onen] onen - mod_div_equality[of "(n - 1)" m, symmetric] + div_mult_mod_eq[of "(n - 1)" m, symmetric] by (simp add:power_add[symmetric] modeq_def th3 del: One_nat_def) from cong_mult_lcancel[of ?y n "a^((n - 1) mod m)" 1, OF yn th2] have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)" . @@ -855,7 +855,7 @@ have eqo: "[(a^?o)^?q = 1] (mod n)" by (simp add: modeq_def power_Suc0) from H have onz: "?o \ 0" by (simp add: ord_eq_0) hence op: "?o > 0" by simp - from mod_div_equality[of d "ord n a"] lh + from div_mult_mod_eq[of d "ord n a"] lh have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: modeq_def mult.commute) hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" by (simp add: modeq_def power_mult[symmetric] power_add[symmetric]) @@ -1108,7 +1108,7 @@ {assume b0: "b = 0" from p(2) nqr have "(n - 1) mod p = 0" apply (simp only: dvd_eq_mod_eq_0[symmetric]) by (rule dvd_mult2, simp) - with mod_div_equality[of "n - 1" p] + with div_mult_mod_eq[of "n - 1" p] have "(n - 1) div p * p= n - 1" by auto hence eq: "(a^((n - 1) div p))^p = a^(n - 1)" by (simp only: power_mult[symmetric]) @@ -1196,7 +1196,7 @@ lemma mod_le: assumes n: "n \ (0::nat)" shows "m mod n \ m" proof- - from mod_div_equality[of m n] + from div_mult_mod_eq[of m n] have "\x. x + m mod n = m" by blast then show ?thesis by auto qed @@ -1214,7 +1214,7 @@ and psp: "list_all (\p. prime p \ coprime (a^(r *(q div p)) mod n - 1) n) ps" unfolding arnb[symmetric] power_mod by (simp_all add: power_mult[symmetric] algebra_simps) from n have n0: "n > 0" by arith - from mod_div_equality[of "a^(n - 1)" n] + from div_mult_mod_eq[of "a^(n - 1)" n] mod_less_divisor[OF n0, of "a^(n - 1)"] have an1: "[a ^ (n - 1) = 1] (mod n)" unfolding nat_mod bqn diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Presburger.thy Sun Oct 16 09:31:05 2016 +0200 @@ -420,8 +420,8 @@ declare mod_div_trivial [presburger] declare div_mod_equality2 [presburger] declare div_mod_equality [presburger] -declare mod_div_equality2 [presburger] -declare mod_div_equality [presburger] +declare mult_div_mod_eq [presburger] +declare div_mult_mod_eq [presburger] declare mod_mult_self1 [presburger] declare mod_mult_self2 [presburger] declare mod2_Suc_Suc[presburger] diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Rings.thy Sun Oct 16 09:31:05 2016 +0200 @@ -1290,7 +1290,7 @@ text \Arbitrary quotient and remainder partitions\ class semiring_modulo = comm_semiring_1_cancel + divide + modulo + - assumes mod_div_equality: "a div b * b + a mod b = a" + assumes div_mult_mod_eq: "a div b * b + a mod b = a" begin lemma mod_div_decomp: @@ -1298,35 +1298,35 @@ obtains q r where "q = a div b" and "r = a mod b" and "a = q * b + r" proof - - from mod_div_equality have "a = a div b * b + a mod b" by simp + from div_mult_mod_eq have "a = a div b * b + a mod b" by simp moreover have "a div b = a div b" .. moreover have "a mod b = a mod b" .. note that ultimately show thesis by blast qed -lemma mod_div_equality2: "b * (a div b) + a mod b = a" - using mod_div_equality [of a b] by (simp add: ac_simps) +lemma mult_div_mod_eq: "b * (a div b) + a mod b = a" + using div_mult_mod_eq [of a b] by (simp add: ac_simps) -lemma mod_div_equality3: "a mod b + a div b * b = a" - using mod_div_equality [of a b] by (simp add: ac_simps) +lemma mod_div_mult_eq: "a mod b + a div b * b = a" + using div_mult_mod_eq [of a b] by (simp add: ac_simps) -lemma mod_div_equality4: "a mod b + b * (a div b) = a" - using mod_div_equality [of a b] by (simp add: ac_simps) +lemma mod_mult_div_eq: "a mod b + b * (a div b) = a" + using div_mult_mod_eq [of a b] by (simp add: ac_simps) -lemma minus_div_eq_mod: "a - a div b * b = a mod b" - by (rule add_implies_diff [symmetric]) (fact mod_div_equality3) +lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b" + by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq) -lemma minus_div_eq_mod2: "a - b * (a div b) = a mod b" - by (rule add_implies_diff [symmetric]) (fact mod_div_equality4) +lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b" + by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq) -lemma minus_mod_eq_div: "a - a mod b = a div b * b" - by (rule add_implies_diff [symmetric]) (fact mod_div_equality) +lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b" + by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq) -lemma minus_mod_eq_div2: "a - a mod b = b * (a div b)" - by (rule add_implies_diff [symmetric]) (fact mod_div_equality2) +lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)" + by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq) end - + class ordered_semiring = semiring + ordered_comm_monoid_add + assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200 @@ -835,7 +835,7 @@ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]) val splits_ss = simpset_of (put_simpset comp_ss @{context} - addsimps [@{thm "mod_div_equality'"}] + addsimps [@{thm "div_mult_mod_eq'"}] |> fold Splitter.add_split [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Word/Bit_Representation.thy Sun Oct 16 09:31:05 2016 +0200 @@ -43,7 +43,7 @@ lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w" unfolding bin_rest_def bin_last_def Bit_def - using mod_div_equality [of w 2] + using div_mult_mod_eq [of w 2] by (cases "w mod 2 = 0", simp_all) lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x" diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Word/Word.thy Sun Oct 16 09:31:05 2016 +0200 @@ -2161,7 +2161,7 @@ apply (unfold word_less_nat_alt word_arith_nat_defs) apply (cut_tac y="unat b" in gt_or_eq_0) apply (erule disjE) - apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse) + apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse) apply simp done @@ -3867,7 +3867,7 @@ apply clarsimp apply (clarsimp simp add : nth_append size_rcat_lem) apply (simp (no_asm_use) only: mult_Suc [symmetric] - td_gal_lt_len less_Suc_eq_le mod_div_equality') + td_gal_lt_len less_Suc_eq_le div_mult_mod_eq') apply clarsimp done diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/ex/Transfer_Ex.thy --- a/src/HOL/ex/Transfer_Ex.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/ex/Transfer_Ex.thy Sun Oct 16 09:31:05 2016 +0200 @@ -16,7 +16,7 @@ by (fact ex1 [untransferred]) lemma ex2: "(a::nat) div b * b + a mod b = a" - by (rule mod_div_equality) + by (rule div_mult_mod_eq) lemma "0 \ (b::int) \ 0 \ (a::int) \ a div b * b + a mod b = a" by (fact ex2 [transferred]) diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/ex/Word_Type.thy --- a/src/HOL/ex/Word_Type.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/ex/Word_Type.thy Sun Oct 16 09:31:05 2016 +0200 @@ -33,7 +33,7 @@ where "b = a div 2" and "c = a mod 2" then have a: "a = b * 2 + c" and "c = 0 \ c = 1" - by (simp_all add: mod_div_equality parity) + by (simp_all add: div_mult_mod_eq parity) from \c = 0 \ c = 1\ have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c" proof