--- 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.
--- 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<n \<Longrightarrow> (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
--- 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
--- 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]}
--- 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.
--- 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}
--- 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')
--- 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 \<le> m \<longleftrightarrow> real n \<le> real m"
"n < m \<longleftrightarrow> real n < real m"
"n \<in> {m .. l} \<longleftrightarrow> real n \<in> {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"
--- 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 =
--- 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'"},
--- 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 \<open>@{const divide} and @{const modulo}\<close>
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 \<noteq> 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
"\<dots> = (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 "\<dots> = a div b"
- by (simp only: mod_div_equality3)
+ by (simp only: mod_div_mult_eq)
also have "\<dots> = 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 "\<dots> = 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 \<open>Addition respects modular equivalence.\<close>
@@ -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 "\<dots> = (a mod c + b + a div c * c) mod c"
by (simp only: ac_simps)
also have "\<dots> = (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 "\<dots> = (a + b mod c + b div c * c) mod c"
by (simp only: ac_simps)
also have "\<dots> = (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 "\<dots> = (a mod c * b + a div c * b * c) mod c"
by (simp only: algebra_simps)
also have "\<dots> = (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 "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
by (simp only: algebra_simps)
also have "\<dots> = (a * (b mod c)) mod c"
@@ -287,7 +287,7 @@
also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
by (simp only: ac_simps)
also have "\<dots> = 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 "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
by (simp add: ac_simps)
also have "\<dots> = (- (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 \<or> 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 "\<exists>b. a = b + 1" ..
qed
@@ -528,7 +528,7 @@
lemma odd_two_times_div_two_succ [simp]:
"odd a \<Longrightarrow> 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 \<le> 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 \<le> 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 \<Longrightarrow> m mod n \<le> (n::nat)"
apply (drule mod_less_divisor [where m = m])
@@ -1279,7 +1279,7 @@
assumes "m mod d = r"
shows "\<exists>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 \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
@@ -1812,7 +1812,7 @@
text\<open>Basic laws about division and remainder\<close>
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 \<open>Proving @{term "a div (b * c) = (a div b) div c"}\<close>
@@ -2282,7 +2282,7 @@
shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
proof -
have "i mod k = i \<longleftrightarrow> 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
--- 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
--- 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: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> 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 \<le> b - c")
prefer 2 apply arith
apply(drule le_less_trans)
--- 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
--- 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)
--- 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 \<noteq> 0"
hence [simp]: "f div g \<noteq> 0" "g \<noteq> 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
--- 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
--- 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 \<noteq> [] \<Longrightarrow>
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 \<noteq> [] \<Longrightarrow> 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])
--- 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 ..
--- 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) \<longleftrightarrow> (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')
--- 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 \<noteq> 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)
--- 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 \<noteq> 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 \<noteq> (0::nat)" shows "m mod n \<le> m"
proof-
- from mod_div_equality[of m n]
+ from div_mult_mod_eq[of m n]
have "\<exists>x. x + m mod n = m" by blast
then show ?thesis by auto
qed
@@ -1214,7 +1214,7 @@
and psp: "list_all (\<lambda>p. prime p \<and> 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
--- 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]
--- 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 \<open>Arbitrary quotient and remainder partitions\<close>
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 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
--- 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"}])
--- 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"
--- 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
--- 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 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
by (fact ex2 [transferred])
--- 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 \<or> c = 1"
- by (simp_all add: mod_div_equality parity)
+ by (simp_all add: div_mult_mod_eq parity)
from \<open>c = 0 \<or> c = 1\<close>
have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
proof