--- a/NEWS Sat Dec 17 15:22:14 2016 +0100
+++ b/NEWS Sat Dec 17 15:22:14 2016 +0100
@@ -6,6 +6,24 @@
New in this Isabelle version
----------------------------
+*** HOL ***
+
+* Swapped orientation of congruence rules mod_add_left_eq,
+mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
+mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
+mod_diff_eq. INCOMPATIBILITY.
+
+* Generalized some facts:
+ zminus_zmod ~> mod_minus_eq
+ zdiff_zmod_left ~> mod_diff_left_eq
+ zdiff_zmod_right ~> mod_diff_right_eq
+ zmod_eq_dvd_iff ~> mod_eq_dvd_iff
+INCOMPATIBILITY.
+
+* Named collection mod_simps covers various congruence rules
+concerning mod, replacing former zmod_simps.
+INCOMPATIBILITY.
+
* (Co)datatype package:
- The 'size_gen_o_map' lemma is no longer generated for datatypes
with type class annotations. As a result, the tactic that derives
@@ -74,7 +92,6 @@
* Solve direct: option "solve_direct_strict_warnings" gives explicit
warnings for lemma statements with trivial proofs.
-
*** Prover IDE -- Isabelle/Scala/jEdit ***
* More aggressive flushing of machine-generated input, according to
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sat Dec 17 15:22:14 2016 +0100
@@ -3206,7 +3206,7 @@
using of_int_eq_iff apply fastforce
by (metis of_int_add of_int_mult of_int_of_nat_eq)
also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
- by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
+ by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
also have "... \<longleftrightarrow> j mod n = k mod n"
by (metis of_nat_eq_iff zmod_int)
finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 17 15:22:14 2016 +0100
@@ -45,8 +45,8 @@
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
- mod_add_right_eq [symmetric]
+ addsimps @{thms refl mod_add_eq mod_add_left_eq
+ mod_add_right_eq
div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
mod_self
div_by_0 mod_by_0 div_0 mod_0
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Dec 17 15:22:14 2016 +0100
@@ -31,8 +31,6 @@
@{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_add_eq = @{thm "mod_add_eq"} RS sym;
-
fun prepare_for_mir q fm =
let
val ps = Logic.strip_params fm
@@ -71,7 +69,7 @@
val (t,np,nh) = prepare_for_mir q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = put_simpset HOL_basic_ss ctxt
- addsimps [refl, mod_add_eq,
+ addsimps [refl, @{thm mod_add_eq},
@{thm mod_self},
@{thm div_0}, @{thm mod_0},
@{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
--- a/src/HOL/Divides.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Divides.thy Sat Dec 17 15:22:14 2016 +0100
@@ -189,97 +189,6 @@
finally show ?thesis .
qed
-text \<open>Addition respects modular equivalence.\<close>
-
-lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
- "(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: 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"
- by (rule mod_mult_self1)
- finally show ?thesis .
-qed
-
-lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
- "(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: 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"
- by (rule mod_mult_self1)
- finally show ?thesis .
-qed
-
-lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close>
- "(a + b) mod c = (a mod c + b mod c) mod c"
-by (rule trans [OF mod_add_left_eq mod_add_right_eq])
-
-lemma mod_add_cong:
- assumes "a mod c = a' mod c"
- assumes "b mod c = b' mod c"
- shows "(a + b) mod c = (a' + b') mod c"
-proof -
- have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
- unfolding assms ..
- thus ?thesis
- by (simp only: mod_add_eq [symmetric])
-qed
-
-text \<open>Multiplication respects modular equivalence.\<close>
-
-lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
- "(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: 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"
- by (rule mod_mult_self1)
- finally show ?thesis .
-qed
-
-lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
- "(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: 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"
- by (rule mod_mult_self1)
- finally show ?thesis .
-qed
-
-lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close>
- "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
-by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
-
-lemma mod_mult_cong:
- assumes "a mod c = a' mod c"
- assumes "b mod c = b' mod c"
- shows "(a * b) mod c = (a' * b') mod c"
-proof -
- have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
- unfolding assms ..
- thus ?thesis
- by (simp only: mod_mult_eq [symmetric])
-qed
-
-text \<open>Exponentiation respects modular equivalence.\<close>
-
-lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
-apply (induct n, simp_all)
-apply (rule mod_mult_right_eq [THEN trans])
-apply (simp (no_asm_simp))
-apply (rule mod_mult_eq [symmetric])
-done
-
lemma mod_mod_cancel:
assumes "c dvd b"
shows "a mod b mod c = a mod c"
@@ -331,6 +240,121 @@
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
unfolding dvd_def by (auto simp add: mod_mult_mult1)
+named_theorems mod_simps
+
+text \<open>Addition respects modular equivalence.\<close>
+
+lemma mod_add_left_eq [mod_simps]:
+ "(a mod c + b) mod c = (a + b) mod c"
+proof -
+ have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+ 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"
+ by (rule mod_mult_self1)
+ finally show ?thesis
+ by (rule sym)
+qed
+
+lemma mod_add_right_eq [mod_simps]:
+ "(a + b mod c) mod c = (a + b) mod c"
+ using mod_add_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_add_eq:
+ "(a mod c + b mod c) mod c = (a + b) mod c"
+ by (simp add: mod_add_left_eq mod_add_right_eq)
+
+lemma mod_sum_eq [mod_simps]:
+ "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
+proof (induct A rule: infinite_finite_induct)
+ case (insert i A)
+ then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
+ = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
+ by simp
+ also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
+ by (simp add: mod_simps)
+ also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
+ by (simp add: insert.hyps)
+ finally show ?case
+ by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_add_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a + b) mod c = (a' + b') mod c"
+proof -
+ have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+ unfolding assms ..
+ then show ?thesis
+ by (simp add: mod_add_eq)
+qed
+
+text \<open>Multiplication respects modular equivalence.\<close>
+
+lemma mod_mult_left_eq [mod_simps]:
+ "((a mod c) * b) mod c = (a * b) mod c"
+proof -
+ have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+ 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"
+ by (rule mod_mult_self1)
+ finally show ?thesis
+ by (rule sym)
+qed
+
+lemma mod_mult_right_eq [mod_simps]:
+ "(a * (b mod c)) mod c = (a * b) mod c"
+ using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_mult_eq:
+ "((a mod c) * (b mod c)) mod c = (a * b) mod c"
+ by (simp add: mod_mult_left_eq mod_mult_right_eq)
+
+lemma mod_prod_eq [mod_simps]:
+ "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
+proof (induct A rule: infinite_finite_induct)
+ case (insert i A)
+ then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
+ = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
+ by simp
+ also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
+ by (simp add: mod_simps)
+ also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
+ by (simp add: insert.hyps)
+ finally show ?case
+ by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_mult_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a * b) mod c = (a' * b') mod c"
+proof -
+ have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+ unfolding assms ..
+ then show ?thesis
+ by (simp add: mod_mult_eq)
+qed
+
+text \<open>Exponentiation respects modular equivalence.\<close>
+
+lemma power_mod [mod_simps]:
+ "((a mod b) ^ n) mod b = (a ^ n) mod b"
+proof (induct n)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
+ by (simp add: mod_mult_right_eq)
+ with Suc show ?case
+ by (simp add: mod_mult_left_eq mod_mult_right_eq)
+qed
+
end
class ring_div = comm_ring_1 + semiring_div
@@ -338,9 +362,28 @@
subclass idom_divide ..
+lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
+ using div_mult_mult1 [of "- 1" a b] by simp
+
+lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
+ using mod_mult_mult1 [of "- 1" a b] by simp
+
+lemma div_minus_right: "a div (- b) = (- a) div b"
+ using div_minus_minus [of "- a" b] by simp
+
+lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
+ using mod_minus_minus [of "- a" b] by simp
+
+lemma div_minus1_right [simp]: "a div (- 1) = - a"
+ using div_minus_right [of a 1] by simp
+
+lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
+ using mod_minus_right [of a 1] by simp
+
text \<open>Negation respects modular equivalence.\<close>
-lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
+lemma mod_minus_eq [mod_simps]:
+ "(- (a mod b)) mod b = (- a) mod b"
proof -
have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
by (simp only: div_mult_mod_eq)
@@ -348,7 +391,8 @@
by (simp add: ac_simps)
also have "\<dots> = (- (a mod b)) mod b"
by (rule mod_mult_self1)
- finally show ?thesis .
+ finally show ?thesis
+ by (rule sym)
qed
lemma mod_minus_cong:
@@ -357,51 +401,37 @@
proof -
have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
unfolding assms ..
- thus ?thesis
- by (simp only: mod_minus_eq [symmetric])
+ then show ?thesis
+ by (simp add: mod_minus_eq)
qed
text \<open>Subtraction respects modular equivalence.\<close>
-lemma mod_diff_left_eq:
- "(a - b) mod c = (a mod c - b) mod c"
- using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
-
-lemma mod_diff_right_eq:
- "(a - b) mod c = (a - b mod c) mod c"
- using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
+lemma mod_diff_left_eq [mod_simps]:
+ "(a mod c - b) mod c = (a - b) mod c"
+ using mod_add_cong [of a c "a mod c" "- b" "- b"]
+ by simp
+
+lemma mod_diff_right_eq [mod_simps]:
+ "(a - b mod c) mod c = (a - b) mod c"
+ using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+ by simp
lemma mod_diff_eq:
- "(a - b) mod c = (a mod c - b mod c) mod c"
- using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
+ "(a mod c - b mod c) mod c = (a - b) mod c"
+ using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+ by simp
lemma mod_diff_cong:
assumes "a mod c = a' mod c"
assumes "b mod c = b' mod c"
shows "(a - b) mod c = (a' - b') mod c"
- using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
-
-lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
- using div_mult_mult1 [of "- 1" a b]
- unfolding neg_equal_0_iff_equal by simp
-
-lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
- using mod_mult_mult1 [of "- 1" a b] by simp
-
-lemma div_minus_right: "a div (-b) = (-a) div b"
- using div_minus_minus [of "-a" b] by simp
-
-lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
- using mod_minus_minus [of "-a" b] by simp
-
-lemma div_minus1_right [simp]: "a div (-1) = -a"
- using div_minus_right [of a 1] by simp
-
-lemma mod_minus1_right [simp]: "a mod (-1) = 0"
- using mod_minus_right [of a 1] by simp
+ using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
+ by simp
lemma minus_mod_self2 [simp]:
"(a - b) mod b = a mod b"
+ using mod_diff_right_eq [of a b b]
by (simp add: mod_diff_right_eq)
lemma minus_mod_self1 [simp]:
@@ -455,18 +485,21 @@
assume "a mod 2 = 1"
moreover assume "b mod 2 = 1"
ultimately show "(a + b) mod 2 = 0"
- using mod_add_eq [of a b 2] by simp
+ using mod_add_eq [of a 2 b] by simp
next
fix a b
assume "(a * b) mod 2 = 0"
+ then have "(a mod 2) * (b mod 2) mod 2 = 0"
+ by (simp add: mod_mult_eq)
then have "(a mod 2) * (b mod 2) = 0"
- by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
+ by (cases "a mod 2 = 0") simp_all
then show "a mod 2 = 0 \<or> b mod 2 = 0"
by (rule divisors_zero)
next
fix a
assume "a mod 2 = 1"
- then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [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
@@ -1052,6 +1085,24 @@
let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
+lemma mod_Suc_eq [mod_simps]:
+ "Suc (m mod n) mod n = Suc m mod n"
+proof -
+ have "(m mod n + 1) mod n = (m + 1) mod n"
+ by (simp only: mod_simps)
+ then show ?thesis
+ by simp
+qed
+
+lemma mod_Suc_Suc_eq [mod_simps]:
+ "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
+proof -
+ have "(m mod n + 2) mod n = (m + 2) mod n"
+ by (simp only: mod_simps)
+ then show ?thesis
+ by simp
+qed
+
subsubsection \<open>Quotient\<close>
@@ -1860,12 +1911,12 @@
apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
done
-lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
+lemma zmod_zminus1_not_zero:
fixes k l :: int
shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
by (simp add: mod_eq_0_iff_dvd)
-lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
+lemma zmod_zminus2_not_zero:
fixes k l :: int
shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
by (simp add: mod_eq_0_iff_dvd)
@@ -2094,7 +2145,7 @@
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
apply (erule_tac P="P x y" for x y in rev_mp)
- apply (subst mod_add_eq)
+ apply (subst mod_add_eq [symmetric])
apply (subst zdiv_zadd1_eq)
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
txt\<open>converse direction\<close>
@@ -2107,7 +2158,7 @@
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
apply (erule_tac P="P x y" for x y in rev_mp)
- apply (subst mod_add_eq)
+ apply (subst mod_add_eq [symmetric])
apply (subst zdiv_zadd1_eq)
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
txt\<open>converse direction\<close>
@@ -2427,24 +2478,6 @@
apply simp_all
done
-text \<open>by Brian Huffman\<close>
-lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
-by (rule mod_minus_eq [symmetric])
-
-lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
-by (rule mod_diff_left_eq [symmetric])
-
-lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
-by (rule mod_diff_right_eq [symmetric])
-
-lemmas zmod_simps =
- mod_add_left_eq [symmetric]
- mod_add_right_eq [symmetric]
- mod_mult_right_eq[symmetric]
- mod_mult_left_eq [symmetric]
- power_mod
- zminus_zmod zdiff_zmod_left zdiff_zmod_right
-
text \<open>Distributive laws for function \<open>nat\<close>.\<close>
lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
@@ -2504,28 +2537,29 @@
apply (rule Divides.div_less_dividend, simp_all)
done
-lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
+lemma (in ring_div) mod_eq_dvd_iff:
+ "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
proof
- assume H: "x mod n = y mod n"
- hence "x mod n - y mod n = 0" by simp
- hence "(x mod n - y mod n) mod n = 0" by simp
- hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
- thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
+ assume ?P
+ then have "(a mod c - b mod c) mod c = 0"
+ by simp
+ then show ?Q
+ by (simp add: dvd_eq_mod_eq_0 mod_simps)
next
- assume H: "n dvd x - y"
- then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
- hence "x = n*k + y" by simp
- hence "x mod n = (n*k + y) mod n" by simp
- thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
+ assume ?Q
+ then obtain d where d: "a - b = c * d" ..
+ then have "a = c * d + b"
+ by (simp add: algebra_simps)
+ then show ?P by simp
qed
-lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
+lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
shows "\<exists>q. x = y + n * q"
proof-
from xy have th: "int x - int y = int (x - y)" by simp
from xyn have "int x mod int n = int y mod int n"
by (simp add: zmod_int [symmetric])
- hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
+ hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
hence "n dvd x - y" by (simp add: th zdvd_int)
then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
qed
--- a/src/HOL/Groebner_Basis.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Groebner_Basis.thy Sat Dec 17 15:22:14 2016 +0100
@@ -72,7 +72,7 @@
declare zmod_eq_0_iff[algebra]
declare dvd_0_left_iff[algebra]
declare zdvd1_eq[algebra]
-declare zmod_eq_dvd_iff[algebra]
+declare mod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
context semiring_parity
--- a/src/HOL/IMP/Abs_Int1_parity.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Sat Dec 17 15:22:14 2016 +0100
@@ -112,7 +112,8 @@
case 3 show ?case by auto
next
case (4 _ a1 _ a2) thus ?case
- by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
+ by (induction a1 a2 rule: plus_parity.induct)
+ (auto simp add: mod_add_eq [symmetric])
qed
text{* In case 4 we needed to refer to particular variables.
--- a/src/HOL/Library/Numeral_Type.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Dec 17 15:22:14 2016 +0100
@@ -133,7 +133,7 @@
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps zmod_simps field_simps)
+apply (simp_all add: Rep_simps mod_simps field_simps)
done
end
@@ -147,12 +147,12 @@
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
apply (induct k)
apply (simp add: zero_def)
-apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
+apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
done
lemma of_int_eq: "of_int z = Abs (z mod n)"
apply (cases z rule: int_diff_cases)
-apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
+apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
done
lemma Rep_numeral:
--- a/src/HOL/Library/Omega_Words_Fun.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Library/Omega_Words_Fun.thy Sat Dec 17 15:22:14 2016 +0100
@@ -626,7 +626,7 @@
by (auto simp add: set_conv_nth)
\<comment> "the following bound is terrible, but it simplifies the proof"
from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
- by (simp add: mod_add_left_eq)
+ by (simp add: mod_add_left_eq [symmetric])
moreover
\<comment> "why is the following so hard to prove??"
have "\<forall>m. m < (Suc m)*(length w) + k"
--- a/src/HOL/Number_Theory/Cong.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Sat Dec 17 15:22:14 2016 +0100
@@ -251,7 +251,7 @@
done
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
- by (metis cong_int_def zmod_eq_dvd_iff)
+ by (metis cong_int_def mod_eq_dvd_iff)
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
by (simp add: cong_altdef_int)
@@ -429,7 +429,7 @@
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
- by (metis cong_int_def minus_minus zminus_zmod)
+ by (metis cong_int_def minus_minus mod_minus_cong)
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
by (auto simp add: cong_altdef_int)
--- a/src/HOL/Number_Theory/Pocklington.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy Sat Dec 17 15:22:14 2016 +0100
@@ -369,7 +369,7 @@
hence th: "[a^?r = 1] (mod n)"
using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
apply (simp add: cong_nat_def del: One_nat_def)
- by (simp add: mod_mult_left_eq[symmetric])
+ by (metis mod_mult_left_eq nat_mult_1)
{assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
moreover
{assume r: "?r \<noteq> 0"
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sat Dec 17 15:22:14 2016 +0100
@@ -167,7 +167,7 @@
fix a b
assume a: "P_1 res a" "P_1 res b"
hence "int p * int q dvd a - b"
- using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int zmod_eq_dvd_iff[of a _ b]
+ using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b]
unfolding P_1_def by force
hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
}
@@ -187,7 +187,7 @@
assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
hence "int p * int q dvd x - y"
using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"]
- zmod_eq_dvd_iff[of x _ y] by auto
+ mod_eq_dvd_iff[of x _ y] by auto
hence "x = y"
using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
}
--- a/src/HOL/Number_Theory/Residues.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Sat Dec 17 15:22:14 2016 +0100
@@ -40,7 +40,7 @@
apply (insert m_gt_one)
apply (rule abelian_groupI)
apply (unfold R_def residue_ring_def)
- apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
+ apply (auto simp add: mod_add_right_eq ac_simps)
apply (case_tac "x = 0")
apply force
apply (subgoal_tac "(x + (m - x)) mod m = 0")
@@ -55,7 +55,7 @@
apply auto
apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
apply (erule ssubst)
- apply (subst mod_mult_right_eq [symmetric])+
+ apply (subst mod_mult_right_eq)+
apply (simp_all only: ac_simps)
done
@@ -64,9 +64,9 @@
apply (rule abelian_group)
apply (rule comm_monoid)
apply (unfold R_def residue_ring_def, auto)
- apply (subst mod_add_eq [symmetric])
+ apply (subst mod_add_eq)
apply (subst mult.commute)
- apply (subst mod_mult_right_eq [symmetric])
+ apply (subst mod_mult_right_eq)
apply (simp add: field_simps)
done
@@ -116,9 +116,9 @@
apply auto
apply (rule the_equality)
apply auto
- apply (subst mod_add_right_eq [symmetric])
+ apply (subst mod_add_right_eq)
apply auto
- apply (subst mod_add_left_eq [symmetric])
+ apply (subst mod_add_left_eq)
apply auto
apply (subgoal_tac "y mod m = - x mod m")
apply simp
@@ -143,13 +143,11 @@
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
unfolding R_def residue_ring_def
- apply auto
- apply presburger
- done
+ by (auto simp add: mod_simps)
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
unfolding R_def residue_ring_def
- by auto (metis mod_mult_eq)
+ by (auto simp add: mod_simps)
lemma zero_cong: "\<zero> = 0"
unfolding R_def residue_ring_def by auto
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Dec 17 15:22:14 2016 +0100
@@ -456,7 +456,7 @@
unfolding round_def
unfolding steps_to_steps'
unfolding H1[symmetric]
- by (simp add: uint_word_ariths(1) rdmods
+ by (simp add: uint_word_ariths(1) mod_simps
uint_word_of_int_id)
qed
--- a/src/HOL/SPARK/Manual/Proc1.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/SPARK/Manual/Proc1.thy Sat Dec 17 15:22:14 2016 +0100
@@ -5,10 +5,10 @@
spark_open "loop_invariant/proc1"
spark_vc procedure_proc1_5
- by (simp add: ring_distribs pull_mods)
+ by (simp add: ring_distribs mod_simps)
spark_vc procedure_proc1_8
- by (simp add: ring_distribs pull_mods)
+ by (simp add: ring_distribs mod_simps)
spark_end
--- a/src/HOL/SPARK/Manual/Proc2.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/SPARK/Manual/Proc2.thy Sat Dec 17 15:22:14 2016 +0100
@@ -5,7 +5,7 @@
spark_open "loop_invariant/proc2"
spark_vc procedure_proc2_7
- by (simp add: ring_distribs pull_mods)
+ by (simp add: ring_distribs mod_simps)
spark_end
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Sat Dec 17 15:22:14 2016 +0100
@@ -824,8 +824,8 @@
val div_mod_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
addsimps @{thms simp_thms
- mod_eq_0_iff_dvd mod_add_left_eq [symmetric] mod_add_right_eq [symmetric]
- mod_add_eq [symmetric] div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+ mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq
+ mod_add_eq div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
mod_self mod_by_0 div_by_0
div_0 mod_0 div_by_1 mod_by_1
div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
--- a/src/HOL/Word/Bit_Representation.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Sat Dec 17 15:22:14 2016 +0100
@@ -308,17 +308,12 @@
lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
apply (induct n arbitrary: w)
- apply simp
- apply (subst mod_add_left_eq)
- apply (simp add: bin_last_def)
- apply arith
- apply (simp add: bin_last_def bin_rest_def Bit_def)
- apply (clarsimp simp: mod_mult_mult1 [symmetric]
- mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
- apply (rule trans [symmetric, OF _ emep1])
- apply auto
+ apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE)
+ apply (smt pos_zmod_mult_2 zle2p)
+ apply (simp add: mult_mod_right)
done
+
subsection "Simplifications for (s)bintrunc"
lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
@@ -647,28 +642,6 @@
"x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
-lemmas zmod_uminus' = zminus_zmod [where m=c] for c
-lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
-
-lemmas brdmod1s' [symmetric] =
- mod_add_left_eq mod_add_right_eq
- mod_diff_left_eq mod_diff_right_eq
- mod_mult_left_eq mod_mult_right_eq
-
-lemmas brdmods' [symmetric] =
- zpower_zmod' [symmetric]
- trans [OF mod_add_left_eq mod_add_right_eq]
- trans [OF mod_diff_left_eq mod_diff_right_eq]
- trans [OF mod_mult_right_eq mod_mult_left_eq]
- zmod_uminus' [symmetric]
- mod_add_left_eq [where b = "1::int"]
- mod_diff_left_eq [where b = "1::int"]
-
-lemmas bintr_arith1s =
- brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
-lemmas bintr_ariths =
- brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
-
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
lemma bintr_ge0: "0 \<le> bintrunc n w"
--- a/src/HOL/Word/Bits_Int.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Bits_Int.thy Sat Dec 17 15:22:14 2016 +0100
@@ -643,14 +643,14 @@
lemma mod_BIT:
"bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
proof -
- have "bin mod 2 ^ n < 2 ^ n" by simp
- then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
- then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
- by (rule mult_left_mono) simp
- then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
- then show ?thesis
- by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
- mod_pos_pos_trivial)
+ have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
+ by (simp add: mod_mult_mult1)
+ also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
+ by (simp add: ac_simps p1mod22k')
+ also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
+ by (simp only: mod_simps)
+ finally show ?thesis
+ by (auto simp add: Bit_def)
qed
lemma AND_mod:
--- a/src/HOL/Word/Misc_Numeric.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy Sat Dec 17 15:22:14 2016 +0100
@@ -8,6 +8,10 @@
imports Main
begin
+lemma one_mod_exp_eq_one [simp]:
+ "1 mod (2 * 2 ^ n) = (1::int)"
+ by (smt mod_pos_pos_trivial zero_less_power)
+
lemma mod_2_neq_1_eq_eq_0:
fixes k :: int
shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
--- a/src/HOL/Word/Word.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Word.thy Sat Dec 17 15:22:14 2016 +0100
@@ -282,10 +282,10 @@
subsection \<open>Arithmetic operations\<close>
lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
- by (metis bintr_ariths(6))
+ by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
- by (metis bintr_ariths(7))
+ by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
begin
@@ -295,16 +295,16 @@
lift_definition one_word :: "'a word" is "1" .
lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op +"
- by (metis bintr_ariths(2))
+ by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op -"
- by (metis bintr_ariths(3))
+ by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
- by (metis bintr_ariths(5))
+ by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"
- by (metis bintr_ariths(4))
+ by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
definition
word_div_def: "a div b = word_of_int (uint a div uint b)"
@@ -332,9 +332,6 @@
unfolding word_succ_def word_pred_def zero_word_def one_word_def
by simp_all
-lemmas arths =
- bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]
-
lemma wi_homs:
shows
wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
@@ -1340,10 +1337,11 @@
and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
- by (simp_all add: uint_word_arith_bintrs
- [THEN uint_sint [symmetric, THEN trans],
- unfolded uint_sint bintr_arith1s bintr_ariths
- len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
+ apply (simp_all only: word_sbin.inverse_norm [symmetric])
+ apply (simp_all add: wi_hom_syms)
+ apply transfer apply simp
+ apply transfer apply simp
+ done
lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
@@ -1443,7 +1441,7 @@
with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
by auto
then show ?thesis
- by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
+ by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
qed
lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
@@ -2699,7 +2697,7 @@
lemma nth_w2p:
"((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
unfolding test_bit_2p [symmetric] word_of_int [symmetric]
- by (simp add: of_int_power)
+ by simp
lemma uint_2p:
"(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
@@ -2723,16 +2721,7 @@
done
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
- apply (unfold word_arith_power_alt)
- apply (case_tac "len_of TYPE ('a)")
- apply clarsimp
- apply (case_tac "nat")
- apply (rule word_ubin.norm_eq_iff [THEN iffD1])
- apply (rule box_equals)
- apply (rule_tac [2] bintr_ariths (1))+
- apply simp
- apply simp
- done
+ by (induct n) (simp_all add: wi_hom_syms)
lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)"
apply (rule xtr3)
@@ -3244,6 +3233,9 @@
lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
+lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
+ by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
+
lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
unfolding word_numeral_alt by (rule and_mask_wi)
@@ -3342,12 +3334,12 @@
"word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
"word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
- by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
+ by (auto simp add: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
lemma mask_power_eq:
"(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
using word_of_int_Ex [where x=x]
- by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
+ by (auto simp add: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
subsubsection \<open>Revcast\<close>
@@ -4242,7 +4234,7 @@
apply (simp add: word_size nat_mod_distrib)
apply (rule of_nat_eq_0_iff [THEN iffD1])
apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
- using mod_mod_trivial zmod_eq_dvd_iff
+ using mod_mod_trivial mod_eq_dvd_iff
apply blast
done
@@ -4579,9 +4571,9 @@
shows "(x + y) mod b = z' mod b'"
proof -
from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
- by (simp add: mod_add_eq[symmetric])
+ by (simp add: mod_add_eq)
also have "\<dots> = (x' + y') mod b'"
- by (simp add: mod_add_eq[symmetric])
+ by (simp add: mod_add_eq)
finally show ?thesis by (simp add: 4)
qed
@@ -4591,11 +4583,8 @@
and 3: "y mod b' = y' mod b'"
and 4: "x' - y' = z'"
shows "(x - y) mod b = z' mod b'"
- using assms
- apply (subst mod_diff_left_eq)
- apply (subst mod_diff_right_eq)
- apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
- done
+ using 1 2 3 4 [symmetric]
+ by (auto intro: mod_diff_cong)
lemma word_induct_less:
"\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
--- a/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 17 15:22:14 2016 +0100
@@ -201,10 +201,6 @@
lemmas push_mods = push_mods' [THEN eq_reflection]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
-lemmas mod_simps =
- mod_mult_self2_is_0 [THEN eq_reflection]
- mod_mult_self1_is_0 [THEN eq_reflection]
- mod_mod_trivial [THEN eq_reflection]
lemma nat_mod_eq:
"!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"
--- a/src/HOL/ex/Word_Type.thy Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/ex/Word_Type.thy Sat Dec 17 15:22:14 2016 +0100
@@ -57,7 +57,7 @@
lemma bitrunc_plus:
"bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
- by (simp add: bitrunc_eq_mod mod_add_eq [symmetric])
+ by (simp add: bitrunc_eq_mod mod_add_eq)
lemma bitrunc_of_1_eq_0_iff [simp]:
"bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
@@ -74,12 +74,12 @@
lemma bitrunc_uminus:
fixes k :: int
shows "bitrunc n (- (bitrunc n k)) = bitrunc n (- k)"
- by (simp add: bitrunc_eq_mod mod_minus_eq [symmetric])
+ by (simp add: bitrunc_eq_mod mod_minus_eq)
lemma bitrunc_minus:
fixes k l :: int
shows "bitrunc n (bitrunc n k - bitrunc n l) = bitrunc n (k - l)"
- by (simp add: bitrunc_eq_mod mod_diff_eq [symmetric])
+ by (simp add: bitrunc_eq_mod mod_diff_eq)
lemma bitrunc_nonnegative [simp]:
fixes k :: int
@@ -279,7 +279,7 @@
lemma of_int_signed [simp]:
"of_int (signed a) = a"
- by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod zdiff_zmod_left)
+ by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod mod_simps)
subsubsection \<open>Properties\<close>