--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Feb 21 09:58:45 2009 +0100
@@ -28,11 +28,9 @@
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
@@ -70,9 +68,8 @@
val (t,np,nh) = prepare_for_linz q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
- addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,
- nat_mod_add_right_eq, int_mod_add_eq,
- int_mod_add_right_eq, int_mod_add_left_eq,
+ addsimps [refl,nat_mod_add_eq, mod_add_left_eq,
+ mod_add_right_eq, int_mod_add_eq,
nat_div_add_eq, int_div_add_eq,
@{thm mod_self}, @{thm "zmod_self"},
@{thm mod_by_0}, @{thm div_by_0},
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat Feb 21 09:58:45 2009 +0100
@@ -32,11 +32,9 @@
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Feb 21 09:58:45 2009 +0100
@@ -47,11 +47,9 @@
val imp_le_cong = @{thm "imp_le_cong"};
val conj_le_cong = @{thm "conj_le_cong"};
val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
-val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
-val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
+val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
+val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
-val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
-val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
--- a/src/HOL/Groebner_Basis.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Groebner_Basis.thy Sat Feb 21 09:58:45 2009 +0100
@@ -454,8 +454,8 @@
declare zdiv_minus1_right[algebra]
declare mod_div_trivial[algebra]
declare mod_mod_trivial[algebra]
-declare zmod_zmult_self1[algebra]
-declare zmod_zmult_self2[algebra]
+declare mod_mult_self2_is_0[algebra]
+declare mod_mult_self1_is_0[algebra]
declare zmod_eq_0_iff[algebra]
declare zdvd_0_left[algebra]
declare zdvd1_eq[algebra]
--- a/src/HOL/IntDiv.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/IntDiv.thy Sat Feb 21 09:58:45 2009 +0100
@@ -747,41 +747,12 @@
show ?thesis by simp
qed
-lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (rule div_add_self1) (* already declared [simp] *)
-
-lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (rule div_add_self2) (* already declared [simp] *)
-
-lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (rule div_mult_self1_is_id) (* already declared [simp] *)
-
-lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
-by (rule mod_mult_self2_is_0) (* already declared [simp] *)
-
-lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
-by (rule mod_mult_self1_is_0) (* already declared [simp] *)
-
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
(* REVISIT: should this be generalized to all semiring_div types? *)
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
-lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-by (rule mod_add_left_eq)
-
-lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-by (rule mod_add_right_eq)
-
-lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
-by (rule mod_add_self1) (* already declared [simp] *)
-
-lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
-by (rule mod_add_self2) (* already declared [simp] *)
-
-lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
-by (rule mod_diff_eq)
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
@@ -896,9 +867,6 @@
apply (auto simp add: mult_commute)
done
-lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
-by (rule mod_mod_cancel)
-
subsection {*Splitting Rules for div and mod*}
@@ -1350,8 +1318,8 @@
by (rule mod_diff_right_eq [symmetric])
lemmas zmod_simps =
- IntDiv.zmod_zadd_left_eq [symmetric]
- IntDiv.zmod_zadd_right_eq [symmetric]
+ mod_add_left_eq [symmetric]
+ mod_add_right_eq [symmetric]
IntDiv.zmod_zmult1_eq [symmetric]
mod_mult_left_eq [symmetric]
IntDiv.zpower_zmod
@@ -1426,14 +1394,14 @@
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: zmod_zdiff1_eq[symmetric])
+ hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
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: zmod_zadd_left_eq)
+ thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
qed
lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
--- a/src/HOL/Library/Float.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Library/Float.thy Sat Feb 21 09:58:45 2009 +0100
@@ -795,7 +795,7 @@
have "x \<noteq> y"
proof (rule ccontr)
assume "\<not> x \<noteq> y" hence "x = y" by auto
- have "?X mod y = 0" unfolding `x = y` using zmod_zmult_self2 by auto
+ have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
thus False using False by auto
qed
hence "x < y" using `x \<le> y` by auto
--- a/src/HOL/NumberTheory/Chinese.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/NumberTheory/Chinese.thy Sat Feb 21 09:58:45 2009 +0100
@@ -103,7 +103,7 @@
apply (rule trans)
apply (rule mod_add_eq)
apply simp
- apply (rule zmod_zadd_right_eq [symmetric])
+ apply (rule mod_add_right_eq [symmetric])
done
lemma funsum_zero [rule_format (no_asm)]:
@@ -238,20 +238,20 @@
apply safe
apply (tactic {* stac (thm "zcong_zmod") 3 *})
apply (tactic {* stac (thm "mod_mult_eq") 3 *})
- apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
- apply (tactic {* stac (thm "x_sol_lin") 5 *})
- apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
- apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
- apply (subgoal_tac [7]
+ apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
+ apply (tactic {* stac (thm "x_sol_lin") 4 *})
+ apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
+ apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
+ apply (subgoal_tac [6]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
- prefer 7
+ prefer 6
apply (simp add: zmult_ac)
apply (unfold xilin_sol_def)
- apply (tactic {* asm_simp_tac @{simpset} 7 *})
- apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
- apply (rule_tac [7] unique_xi_sol)
- apply (rule_tac [4] funprod_zdvd)
+ apply (tactic {* asm_simp_tac @{simpset} 6 *})
+ apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
+ apply (rule_tac [6] unique_xi_sol)
+ apply (rule_tac [3] funprod_zdvd)
apply (unfold m_cond_def)
apply (rule funprod_pos [THEN pos_mod_sign])
apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
--- a/src/HOL/NumberTheory/Gauss.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/NumberTheory/Gauss.thy Sat Feb 21 09:58:45 2009 +0100
@@ -64,14 +64,14 @@
qed
lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
- using zdiv_zmult_self2 [of 2 "p - 1"] by auto
+ using div_mult_self1_is_id [of 2 "p - 1"] by auto
lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
apply (frule odd_minus_one_even)
apply (simp add: zEven_def)
apply (subgoal_tac "2 \<noteq> 0")
- apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
+ apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
apply (auto simp add: even_div_2_prop2)
done
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/NumberTheory/IntPrimes.thy Sat Feb 21 09:58:45 2009 +0100
@@ -217,7 +217,7 @@
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
apply (unfold zcong_def dvd_def, auto)
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
- apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff zmod_zadd_right_eq)
+ apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq)
done
lemma zcong_square_zless:
@@ -237,7 +237,7 @@
lemma zcong_zless_0:
"0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
apply (unfold zcong_def dvd_def, auto)
- apply (metis div_pos_pos_trivial linorder_not_less zdiv_zmult_self2 zle_refl zle_trans)
+ apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id zle_refl zle_trans)
done
lemma zcong_zless_unique:
@@ -302,7 +302,7 @@
lemma zmod_zdvd_zmod:
"0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
- by (rule zmod_zmod_cancel)
+ by (rule mod_mod_cancel)
subsection {* Extended GCD *}
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Sat Feb 21 09:58:45 2009 +0100
@@ -322,7 +322,7 @@
by (rule zdiv_mono1) (insert p_g_2, auto)
then show "b \<le> (q * a) div p"
apply (subgoal_tac "p \<noteq> 0")
- apply (frule zdiv_zmult_self2, force)
+ apply (frule div_mult_self1_is_id, force)
apply (insert p_g_2, auto)
done
qed
@@ -356,7 +356,7 @@
by (rule zdiv_mono1) (insert q_g_2, auto)
then show "a \<le> (p * b) div q"
apply (subgoal_tac "q \<noteq> 0")
- apply (frule zdiv_zmult_self2, force)
+ apply (frule div_mult_self1_is_id, force)
apply (insert q_g_2, auto)
done
qed
--- a/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Tools/Qelim/presburger.ML Sat Feb 21 09:58:45 2009 +0100
@@ -124,8 +124,7 @@
@ map (symmetric o mk_meta_eq)
[@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
- @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
- @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
+ @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
--- a/src/HOL/Word/BinGeneral.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Word/BinGeneral.thy Sat Feb 21 09:58:45 2009 +0100
@@ -433,7 +433,7 @@
"!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
apply (induct n)
apply clarsimp
- apply (subst zmod_zadd_left_eq)
+ apply (subst mod_add_left_eq)
apply (simp add: bin_last_mod)
apply (simp add: number_of_eq)
apply clarsimp
@@ -767,23 +767,23 @@
lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
lemmas brdmod1s' [symmetric] =
- zmod_zadd_left_eq zmod_zadd_right_eq
+ mod_add_left_eq mod_add_right_eq
zmod_zsub_left_eq zmod_zsub_right_eq
zmod_zmult1_eq zmod_zmult1_eq_rev
lemmas brdmods' [symmetric] =
zpower_zmod' [symmetric]
- trans [OF zmod_zadd_left_eq zmod_zadd_right_eq]
+ trans [OF mod_add_left_eq mod_add_right_eq]
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
zmod_uminus' [symmetric]
- zmod_zadd_left_eq [where b = "1"]
+ mod_add_left_eq [where b = "1::int"]
zmod_zsub_left_eq [where b = "1"]
lemmas bintr_arith1s =
- brdmod1s' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
+ brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
lemmas bintr_ariths =
- brdmods' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
+ brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard]
--- a/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Word/Num_Lemmas.thy Sat Feb 21 09:58:45 2009 +0100
@@ -127,12 +127,12 @@
lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
apply (unfold diff_int_def)
- apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]])
- apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])
+ apply (rule trans [OF _ mod_add_right_eq [symmetric]])
+ apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
done
lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
- by (rule zmod_zadd_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
+ by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
lemma zmod_zsub_self [simp]:
"((b :: int) - a) mod a = b mod a"
@@ -146,8 +146,8 @@
done
lemmas rdmods [symmetric] = zmod_uminus [symmetric]
- zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq
- zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
+ zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
+ mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
lemma mod_plus_right:
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
@@ -169,7 +169,8 @@
lemmas push_mods = push_mods' [THEN eq_reflection, standard]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
lemmas mod_simps =
- zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection]
+ 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:
--- a/src/HOL/Word/WordGenLib.thy Fri Feb 20 16:07:20 2009 -0800
+++ b/src/HOL/Word/WordGenLib.thy Sat Feb 21 09:58:45 2009 +0100
@@ -273,7 +273,7 @@
have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
show ?thesis
apply (subst x)
- apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2)
+ apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
apply simp
done
qed