1.1 --- a/src/HOL/Number_Theory/Cong.thy Sun Feb 09 17:47:23 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Cong.thy Sun Feb 09 19:10:12 2014 +0000
1.3 @@ -251,10 +251,7 @@
1.4 done
1.5
1.6 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
1.7 - apply (subst cong_eq_diff_cong_0_int)
1.8 - apply (unfold cong_int_def)
1.9 - apply (simp add: dvd_eq_mod_eq_0 [symmetric])
1.10 - done
1.11 + by (metis cong_int_def zmod_eq_dvd_iff)
1.12
1.13 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
1.14 by (simp add: cong_altdef_int)
1.15 @@ -270,18 +267,11 @@
1.16
1.17 lemma cong_mult_rcancel_int:
1.18 "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
1.19 - apply (subst (1 2) cong_altdef_int)
1.20 - apply (subst left_diff_distrib [symmetric])
1.21 - apply (rule coprime_dvd_mult_iff_int)
1.22 - apply (subst gcd_commute_int, assumption)
1.23 - done
1.24 + by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute)
1.25
1.26 lemma cong_mult_rcancel_nat:
1.27 - assumes "coprime k (m::nat)"
1.28 - shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
1.29 - apply (rule cong_mult_rcancel_int [transferred])
1.30 - using assms apply auto
1.31 - done
1.32 + "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
1.33 + by (metis cong_mult_rcancel_int [transferred])
1.34
1.35 lemma cong_mult_lcancel_nat:
1.36 "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
1.37 @@ -295,16 +285,12 @@
1.38 lemma coprime_cong_mult_int:
1.39 "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
1.40 \<Longrightarrow> [a = b] (mod m * n)"
1.41 - apply (simp only: cong_altdef_int)
1.42 - apply (erule (2) divides_mult_int)
1.43 - done
1.44 +by (metis divides_mult_int cong_altdef_int)
1.45
1.46 lemma coprime_cong_mult_nat:
1.47 assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
1.48 shows "[a = b] (mod m * n)"
1.49 - apply (rule coprime_cong_mult_int [transferred])
1.50 - using assms apply auto
1.51 - done
1.52 + by (metis assms coprime_cong_mult_int [transferred])
1.53
1.54 lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
1.55 a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
1.56 @@ -316,61 +302,46 @@
1.57
1.58 lemma cong_less_unique_nat:
1.59 "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
1.60 - apply auto
1.61 - apply (rule_tac x = "a mod m" in exI)
1.62 - apply (unfold cong_nat_def, auto)
1.63 - done
1.64 + by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
1.65
1.66 lemma cong_less_unique_int:
1.67 "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
1.68 - apply auto
1.69 - apply (rule_tac x = "a mod m" in exI)
1.70 - apply (unfold cong_int_def, auto)
1.71 - done
1.72 + by (auto simp: cong_int_def) (metis mod_mod_trivial pos_mod_conj)
1.73
1.74 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
1.75 - apply (auto simp add: cong_altdef_int dvd_def field_simps)
1.76 + apply (auto simp add: cong_altdef_int dvd_def)
1.77 apply (rule_tac [!] x = "-k" in exI, auto)
1.78 done
1.79
1.80 -lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
1.81 - (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
1.82 - apply (rule iffI)
1.83 - apply (cases "b <= a")
1.84 - apply (subst (asm) cong_altdef_nat, assumption)
1.85 - apply (unfold dvd_def, auto)
1.86 - apply (rule_tac x = k in exI)
1.87 - apply (rule_tac x = 0 in exI)
1.88 - apply (auto simp add: field_simps)
1.89 - apply (subst (asm) cong_sym_eq_nat)
1.90 - apply (subst (asm) cong_altdef_nat)
1.91 - apply force
1.92 - apply (unfold dvd_def, auto)
1.93 - apply (rule_tac x = 0 in exI)
1.94 - apply (rule_tac x = k in exI)
1.95 - apply (auto simp add: field_simps)
1.96 - apply (unfold cong_nat_def)
1.97 - apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
1.98 - apply (erule ssubst)back
1.99 - apply (erule subst)
1.100 - apply auto
1.101 - done
1.102 +lemma cong_iff_lin_nat:
1.103 + "([(a::nat) = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" (is "?lhs = ?rhs")
1.104 +proof (rule iffI)
1.105 + assume eqm: ?lhs
1.106 + show ?rhs
1.107 + proof (cases "b \<le> a")
1.108 + case True
1.109 + then show ?rhs using eqm
1.110 + by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult_commute)
1.111 + next
1.112 + case False
1.113 + then show ?rhs using eqm
1.114 + apply (subst (asm) cong_sym_eq_nat)
1.115 + apply (auto simp: cong_altdef_nat)
1.116 + apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
1.117 + done
1.118 + qed
1.119 +next
1.120 + assume ?rhs
1.121 + then show ?lhs
1.122 + by (metis cong_nat_def mod_mult_self2 nat_mult_commute)
1.123 +qed
1.124
1.125 lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.126 - apply (subst (asm) cong_iff_lin_int, auto)
1.127 - apply (subst add_commute)
1.128 - apply (subst (2) gcd_commute_int)
1.129 - apply (subst mult_commute)
1.130 - apply (subst gcd_add_mult_int)
1.131 - apply (rule gcd_commute_int)
1.132 - done
1.133 + by (metis cong_int_def gcd_red_int)
1.134
1.135 lemma cong_gcd_eq_nat:
1.136 - assumes "[(a::nat) = b] (mod m)"
1.137 - shows "gcd a m = gcd b m"
1.138 - apply (rule cong_gcd_eq_int [transferred])
1.139 - using assms apply auto
1.140 - done
1.141 + "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
1.142 + by (metis assms cong_gcd_eq_int [transferred])
1.143
1.144 lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.145 by (auto simp add: cong_gcd_eq_nat)
1.146 @@ -385,9 +356,7 @@
1.147 by (auto simp add: cong_int_def)
1.148
1.149 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
1.150 - apply (subst (1 2) cong_altdef_int)
1.151 - apply auto
1.152 - done
1.153 + by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
1.154
1.155 (*
1.156 lemma mod_dvd_mod_int:
1.157 @@ -460,18 +429,14 @@
1.158 by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
1.159
1.160 lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
1.161 - apply (simp add: cong_altdef_int)
1.162 - apply (subst dvd_minus_iff [symmetric])
1.163 - apply (simp add: field_simps)
1.164 - done
1.165 + by (metis cong_int_def minus_minus zminus_zmod)
1.166
1.167 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
1.168 by (auto simp add: cong_altdef_int)
1.169
1.170 lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
1.171 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
1.172 - apply (cases "b > 0")
1.173 - apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
1.174 + apply (cases "b > 0", simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
1.175 apply (subst (1 2) cong_modulus_neg_int)
1.176 apply (unfold cong_int_def)
1.177 apply (subgoal_tac "a * b = (-a * -b)")
1.178 @@ -482,11 +447,8 @@
1.179 done
1.180
1.181 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
1.182 - apply (cases "a = 0")
1.183 - apply force
1.184 - apply (subst (asm) cong_altdef_nat)
1.185 - apply auto
1.186 - done
1.187 + apply (cases "a = 0", force)
1.188 + by (metis cong_altdef_nat leI less_one)
1.189
1.190 lemma cong_0_1_nat': "[(0::nat) = Suc 0] (mod n) = (n = Suc 0)"
1.191 unfolding cong_nat_def by auto
1.192 @@ -503,40 +465,20 @@
1.193 apply auto [1]
1.194 apply (drule_tac x = "a - 1" in spec)
1.195 apply force
1.196 - apply (cases "a = 0")
1.197 - apply (metis add_is_0 cong_0_1_nat zero_neq_one)
1.198 + apply (cases "a = 0", simp add: cong_0_1_nat)
1.199 apply (rule iffI)
1.200 - apply (drule cong_to_1_nat)
1.201 - apply (unfold dvd_def)
1.202 - apply auto [1]
1.203 - apply (rule_tac x = k in exI)
1.204 - apply (auto simp add: field_simps) [1]
1.205 - apply (subst cong_altdef_nat)
1.206 - apply (auto simp add: dvd_def)
1.207 + apply (metis cong_to_1_nat dvd_def monoid_mult_class.mult.right_neutral mult_commute mult_eq_if)
1.208 + apply (metis cong_add_lcancel_0_nat cong_mult_self_nat)
1.209 done
1.210
1.211 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
1.212 - apply (subst cong_altdef_nat)
1.213 - apply assumption
1.214 - apply (unfold dvd_def, auto simp add: field_simps)
1.215 - apply (rule_tac x = k in exI)
1.216 - apply auto
1.217 - done
1.218 + by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def nat_mult_commute)
1.219
1.220 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
1.221 apply (cases "n = 0")
1.222 apply force
1.223 apply (frule bezout_nat [of a n], auto)
1.224 - apply (rule exI, erule ssubst)
1.225 - apply (rule cong_trans_nat)
1.226 - apply (rule cong_add_nat)
1.227 - apply (subst mult_commute)
1.228 - apply (rule cong_mult_self_nat)
1.229 - prefer 2
1.230 - apply simp
1.231 - apply (rule cong_refl_nat)
1.232 - apply (rule cong_refl_nat)
1.233 - done
1.234 + by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult_commute)
1.235
1.236 lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
1.237 apply (cases "n = 0")
1.238 @@ -545,18 +487,7 @@
1.239 apply (rule_tac x = "-1" in exI)
1.240 apply auto
1.241 apply (insert bezout_int [of a n], auto)
1.242 - apply (rule exI)
1.243 - apply (erule subst)
1.244 - apply (rule cong_trans_int)
1.245 - prefer 2
1.246 - apply (rule cong_add_int)
1.247 - apply (rule cong_refl_int)
1.248 - apply (rule cong_sym_int)
1.249 - apply (rule cong_mult_self_int)
1.250 - apply simp
1.251 - apply (subst mult_commute)
1.252 - apply (rule cong_refl_int)
1.253 - done
1.254 + by (metis cong_iff_lin_int mult_commute)
1.255
1.256 lemma cong_solve_dvd_nat:
1.257 assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
1.258 @@ -621,56 +552,34 @@
1.259 apply (subst coprime_iff_invertible_nat)
1.260 apply auto
1.261 apply (auto simp add: cong_nat_def)
1.262 - apply (rule_tac x = "x mod m" in exI)
1.263 apply (metis mod_less_divisor mod_mult_right_eq)
1.264 done
1.265
1.266 lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
1.267 (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
1.268 apply (subst coprime_iff_invertible_int)
1.269 - apply auto
1.270 apply (auto simp add: cong_int_def)
1.271 - apply (rule_tac x = "x mod m" in exI)
1.272 - apply (auto simp add: mod_mult_right_eq [symmetric])
1.273 + apply (metis mod_mult_right_eq pos_mod_conj)
1.274 done
1.275
1.276 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
1.277 [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.278 apply (cases "y \<le> x")
1.279 - apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
1.280 - apply (rule cong_sym_nat)
1.281 - apply (subst (asm) (1 2) cong_sym_eq_nat)
1.282 - apply (auto simp add: cong_altdef_nat lcm_least_nat)
1.283 + apply (metis cong_altdef_nat lcm_least_nat)
1.284 + apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
1.285 done
1.286
1.287 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
1.288 [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.289 by (auto simp add: cong_altdef_int lcm_least_int) [1]
1.290
1.291 -lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
1.292 - [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
1.293 - apply (frule (1) cong_cong_lcm_nat)
1.294 - back
1.295 - apply (simp add: lcm_nat_def)
1.296 - done
1.297 -
1.298 -lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
1.299 - [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
1.300 - apply (frule (1) cong_cong_lcm_int)
1.301 - back
1.302 - apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
1.303 - done
1.304 -
1.305 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
1.306 (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.307 (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
1.308 [x = y] (mod (PROD i:A. m i))"
1.309 apply (induct set: finite)
1.310 apply auto
1.311 - apply (rule cong_cong_coprime_nat)
1.312 - apply (subst gcd_commute_nat)
1.313 - apply (rule setprod_coprime_nat)
1.314 - apply auto
1.315 + apply (metis coprime_cong_mult_nat gcd_semilattice_nat.inf_commute setprod_coprime_nat)
1.316 done
1.317
1.318 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
1.319 @@ -679,10 +588,7 @@
1.320 [x = y] (mod (PROD i:A. m i))"
1.321 apply (induct set: finite)
1.322 apply auto
1.323 - apply (rule cong_cong_coprime_int)
1.324 - apply (subst gcd_commute_int)
1.325 - apply (rule setprod_coprime_int)
1.326 - apply auto
1.327 + apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
1.328 done
1.329
1.330 lemma binary_chinese_remainder_aux_nat:
1.331 @@ -929,10 +835,7 @@
1.332 [x = y] (mod (PROD i:A. m i))"
1.333 apply (induct set: finite)
1.334 apply auto
1.335 - apply (erule (1) coprime_cong_mult_nat)
1.336 - apply (subst gcd_commute_nat)
1.337 - apply (rule setprod_coprime_nat)
1.338 - apply auto
1.339 + apply (metis coprime_cong_mult_nat nat_mult_commute setprod_coprime_nat)
1.340 done
1.341
1.342 lemma chinese_remainder_unique_nat: