1.1 --- a/src/HOL/Number_Theory/Cong.thy Sat Sep 10 22:11:55 2011 +0200
1.2 +++ b/src/HOL/Number_Theory/Cong.thy Sat Sep 10 23:27:32 2011 +0200
1.3 @@ -14,7 +14,7 @@
1.4 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
1.5 extended gcd, lcm, primes to the integers. Amine Chaieb provided
1.6 another extension of the notions to the integers, and added a number
1.7 -of results to "Primes" and "GCD".
1.8 +of results to "Primes" and "GCD".
1.9
1.10 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
1.11 developed the congruence relations on the integers. The notion was
1.12 @@ -29,34 +29,33 @@
1.13 imports Primes
1.14 begin
1.15
1.16 -subsection {* Turn off One_nat_def *}
1.17 +subsection {* Turn off @{text One_nat_def} *}
1.18
1.19 -lemma induct'_nat [case_names zero plus1, induct type: nat]:
1.20 - "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
1.21 -by (erule nat_induct) (simp add:One_nat_def)
1.22 +lemma induct'_nat [case_names zero plus1, induct type: nat]:
1.23 + "P (0::nat) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 1)) \<Longrightarrow> P n"
1.24 + by (induct n) (simp_all add: One_nat_def)
1.25
1.26 -lemma cases_nat [case_names zero plus1, cases type: nat]:
1.27 - "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
1.28 -by(metis induct'_nat)
1.29 +lemma cases_nat [case_names zero plus1, cases type: nat]:
1.30 + "P (0::nat) \<Longrightarrow> (\<And>n. P (n + 1)) \<Longrightarrow> P n"
1.31 + by (rule induct'_nat)
1.32
1.33 lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
1.34 -by (simp add: One_nat_def)
1.35 + by (simp add: One_nat_def)
1.36
1.37 -lemma power_eq_one_eq_nat [simp]:
1.38 - "((x::nat)^m = 1) = (m = 0 | x = 1)"
1.39 -by (induct m, auto)
1.40 +lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
1.41 + by (induct m) auto
1.42
1.43 lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
1.44 - card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
1.45 -by (auto simp add: insert_absorb)
1.46 + card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
1.47 + by (auto simp add: insert_absorb)
1.48
1.49 lemma nat_1' [simp]: "nat 1 = 1"
1.50 -by simp
1.51 + by simp
1.52
1.53 (* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
1.54
1.55 declare nat_1 [simp del]
1.56 -declare add_2_eq_Suc [simp del]
1.57 +declare add_2_eq_Suc [simp del]
1.58 declare add_2_eq_Suc' [simp del]
1.59
1.60
1.61 @@ -66,31 +65,23 @@
1.62 subsection {* Main definitions *}
1.63
1.64 class cong =
1.65 -
1.66 -fixes
1.67 - cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
1.68 -
1.69 + fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
1.70 begin
1.71
1.72 -abbreviation
1.73 - notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
1.74 -where
1.75 - "notcong x y m == (~cong x y m)"
1.76 +abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
1.77 + where "notcong x y m \<equiv> \<not> cong x y m"
1.78
1.79 end
1.80
1.81 (* definitions for the natural numbers *)
1.82
1.83 instantiation nat :: cong
1.84 +begin
1.85
1.86 -begin
1.87 +definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
1.88 + where "cong_nat x y m = ((x mod m) = (y mod m))"
1.89
1.90 -definition
1.91 - cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
1.92 -where
1.93 - "cong_nat x y m = ((x mod m) = (y mod m))"
1.94 -
1.95 -instance proof qed
1.96 +instance ..
1.97
1.98 end
1.99
1.100 @@ -98,15 +89,12 @@
1.101 (* definitions for the integers *)
1.102
1.103 instantiation int :: cong
1.104 +begin
1.105
1.106 -begin
1.107 +definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
1.108 + where "cong_int x y m = ((x mod m) = (y mod m))"
1.109
1.110 -definition
1.111 - cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
1.112 -where
1.113 - "cong_int x y m = ((x mod m) = (y mod m))"
1.114 -
1.115 -instance proof qed
1.116 +instance ..
1.117
1.118 end
1.119
1.120 @@ -115,25 +103,25 @@
1.121
1.122
1.123 lemma transfer_nat_int_cong:
1.124 - "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
1.125 + "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
1.126 ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
1.127 - unfolding cong_int_def cong_nat_def
1.128 + unfolding cong_int_def cong_nat_def
1.129 apply (auto simp add: nat_mod_distrib [symmetric])
1.130 apply (subst (asm) eq_nat_nat_iff)
1.131 - apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
1.132 + apply (cases "m = 0", force, rule pos_mod_sign, force)+
1.133 apply assumption
1.134 -done
1.135 + done
1.136
1.137 -declare transfer_morphism_nat_int[transfer add return:
1.138 +declare transfer_morphism_nat_int[transfer add return:
1.139 transfer_nat_int_cong]
1.140
1.141 lemma transfer_int_nat_cong:
1.142 "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
1.143 apply (auto simp add: cong_int_def cong_nat_def)
1.144 apply (auto simp add: zmod_int [symmetric])
1.145 -done
1.146 + done
1.147
1.148 -declare transfer_morphism_int_nat[transfer add return:
1.149 +declare transfer_morphism_int_nat[transfer add return:
1.150 transfer_int_nat_cong]
1.151
1.152
1.153 @@ -141,52 +129,52 @@
1.154
1.155 (* was zcong_0, etc. *)
1.156 lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
1.157 - by (unfold cong_nat_def, auto)
1.158 + unfolding cong_nat_def by auto
1.159
1.160 lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
1.161 - by (unfold cong_int_def, auto)
1.162 + unfolding cong_int_def by auto
1.163
1.164 lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
1.165 - by (unfold cong_nat_def, auto)
1.166 + unfolding cong_nat_def by auto
1.167
1.168 lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
1.169 - by (unfold cong_nat_def, auto simp add: One_nat_def)
1.170 + unfolding cong_nat_def by (auto simp add: One_nat_def)
1.171
1.172 lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
1.173 - by (unfold cong_int_def, auto)
1.174 + unfolding cong_int_def by auto
1.175
1.176 lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
1.177 - by (unfold cong_nat_def, auto)
1.178 + unfolding cong_nat_def by auto
1.179
1.180 lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
1.181 - by (unfold cong_int_def, auto)
1.182 + unfolding cong_int_def by auto
1.183
1.184 lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
1.185 - by (unfold cong_nat_def, auto)
1.186 + unfolding cong_nat_def by auto
1.187
1.188 lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
1.189 - by (unfold cong_int_def, auto)
1.190 + unfolding cong_int_def by auto
1.191
1.192 lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
1.193 - by (unfold cong_nat_def, auto)
1.194 + unfolding cong_nat_def by auto
1.195
1.196 lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
1.197 - by (unfold cong_int_def, auto)
1.198 + unfolding cong_int_def by auto
1.199
1.200 lemma cong_trans_nat [trans]:
1.201 "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
1.202 - by (unfold cong_nat_def, auto)
1.203 + unfolding cong_nat_def by auto
1.204
1.205 lemma cong_trans_int [trans]:
1.206 "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
1.207 - by (unfold cong_int_def, auto)
1.208 + unfolding cong_int_def by auto
1.209
1.210 lemma cong_add_nat:
1.211 "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
1.212 apply (unfold cong_nat_def)
1.213 apply (subst (1 2) mod_add_eq)
1.214 apply simp
1.215 -done
1.216 + done
1.217
1.218 lemma cong_add_int:
1.219 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
1.220 @@ -194,21 +182,21 @@
1.221 apply (subst (1 2) mod_add_left_eq)
1.222 apply (subst (1 2) mod_add_right_eq)
1.223 apply simp
1.224 -done
1.225 + done
1.226
1.227 lemma cong_diff_int:
1.228 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
1.229 apply (unfold cong_int_def)
1.230 apply (subst (1 2) mod_diff_eq)
1.231 apply simp
1.232 -done
1.233 + done
1.234
1.235 lemma cong_diff_aux_int:
1.236 - "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
1.237 + "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
1.238 [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
1.239 apply (subst (1 2) tsub_eq)
1.240 apply (auto intro: cong_diff_int)
1.241 -done;
1.242 + done
1.243
1.244 lemma cong_diff_nat:
1.245 assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
1.246 @@ -221,7 +209,7 @@
1.247 apply (unfold cong_nat_def)
1.248 apply (subst (1 2) mod_mult_eq)
1.249 apply simp
1.250 -done
1.251 + done
1.252
1.253 lemma cong_mult_int:
1.254 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
1.255 @@ -230,73 +218,69 @@
1.256 apply (subst (1 2) mult_commute)
1.257 apply (subst (1 2) zmod_zmult1_eq)
1.258 apply simp
1.259 -done
1.260 + done
1.261
1.262 lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.263 - apply (induct k)
1.264 - apply (auto simp add: cong_mult_nat)
1.265 + by (induct k) (auto simp add: cong_mult_nat)
1.266 +
1.267 +lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.268 + by (induct k) (auto simp add: cong_mult_int)
1.269 +
1.270 +lemma cong_setsum_nat [rule_format]:
1.271 + "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.272 + [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
1.273 + apply (cases "finite A")
1.274 + apply (induct set: finite)
1.275 + apply (auto intro: cong_add_nat)
1.276 done
1.277
1.278 -lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.279 - apply (induct k)
1.280 - apply (auto simp add: cong_mult_int)
1.281 +lemma cong_setsum_int [rule_format]:
1.282 + "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.283 + [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
1.284 + apply (cases "finite A")
1.285 + apply (induct set: finite)
1.286 + apply (auto intro: cong_add_int)
1.287 done
1.288
1.289 -lemma cong_setsum_nat [rule_format]:
1.290 - "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.291 - [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
1.292 - apply (case_tac "finite A")
1.293 - apply (induct set: finite)
1.294 - apply (auto intro: cong_add_nat)
1.295 -done
1.296 -
1.297 -lemma cong_setsum_int [rule_format]:
1.298 - "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.299 - [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
1.300 - apply (case_tac "finite A")
1.301 - apply (induct set: finite)
1.302 - apply (auto intro: cong_add_int)
1.303 -done
1.304 -
1.305 -lemma cong_setprod_nat [rule_format]:
1.306 - "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.307 +lemma cong_setprod_nat [rule_format]:
1.308 + "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.309 [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
1.310 - apply (case_tac "finite A")
1.311 + apply (cases "finite A")
1.312 apply (induct set: finite)
1.313 apply (auto intro: cong_mult_nat)
1.314 -done
1.315 + done
1.316
1.317 -lemma cong_setprod_int [rule_format]:
1.318 - "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.319 +lemma cong_setprod_int [rule_format]:
1.320 + "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.321 [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
1.322 - apply (case_tac "finite A")
1.323 + apply (cases "finite A")
1.324 apply (induct set: finite)
1.325 apply (auto intro: cong_mult_int)
1.326 -done
1.327 + done
1.328
1.329 lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
1.330 - by (rule cong_mult_nat, simp_all)
1.331 + by (rule cong_mult_nat) simp_all
1.332
1.333 lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
1.334 - by (rule cong_mult_int, simp_all)
1.335 + by (rule cong_mult_int) simp_all
1.336
1.337 lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
1.338 - by (rule cong_mult_nat, simp_all)
1.339 + by (rule cong_mult_nat) simp_all
1.340
1.341 lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
1.342 - by (rule cong_mult_int, simp_all)
1.343 + by (rule cong_mult_int) simp_all
1.344
1.345 lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
1.346 - by (unfold cong_nat_def, auto)
1.347 + unfolding cong_nat_def by auto
1.348
1.349 lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
1.350 - by (unfold cong_int_def, auto)
1.351 + unfolding cong_int_def by auto
1.352
1.353 lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
1.354 apply (rule iffI)
1.355 apply (erule cong_diff_int [of a b m b b, simplified])
1.356 apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
1.357 -done
1.358 + done
1.359
1.360 lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
1.361 [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
1.362 @@ -307,29 +291,29 @@
1.363 shows "[a = b] (mod m) = [a - b = 0] (mod m)"
1.364 using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
1.365
1.366 -lemma cong_diff_cong_0'_nat:
1.367 - "[(x::nat) = y] (mod n) \<longleftrightarrow>
1.368 +lemma cong_diff_cong_0'_nat:
1.369 + "[(x::nat) = y] (mod n) \<longleftrightarrow>
1.370 (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
1.371 - apply (case_tac "y <= x")
1.372 + apply (cases "y <= x")
1.373 apply (frule cong_eq_diff_cong_0_nat [where m = n])
1.374 apply auto [1]
1.375 apply (subgoal_tac "x <= y")
1.376 apply (frule cong_eq_diff_cong_0_nat [where m = n])
1.377 apply (subst cong_sym_eq_nat)
1.378 apply auto
1.379 -done
1.380 + done
1.381
1.382 lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
1.383 apply (subst cong_eq_diff_cong_0_nat, assumption)
1.384 apply (unfold cong_nat_def)
1.385 apply (simp add: dvd_eq_mod_eq_0 [symmetric])
1.386 -done
1.387 + done
1.388
1.389 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
1.390 apply (subst cong_eq_diff_cong_0_int)
1.391 apply (unfold cong_int_def)
1.392 apply (simp add: dvd_eq_mod_eq_0 [symmetric])
1.393 -done
1.394 + done
1.395
1.396 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
1.397 by (simp add: cong_altdef_int)
1.398 @@ -342,29 +326,29 @@
1.399 (* any way around this? *)
1.400 apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
1.401 apply (auto simp add: field_simps)
1.402 -done
1.403 + done
1.404
1.405 lemma cong_mult_rcancel_int:
1.406 - "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
1.407 + "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
1.408 apply (subst (1 2) cong_altdef_int)
1.409 apply (subst left_diff_distrib [symmetric])
1.410 apply (rule coprime_dvd_mult_iff_int)
1.411 apply (subst gcd_commute_int, assumption)
1.412 -done
1.413 + done
1.414
1.415 lemma cong_mult_rcancel_nat:
1.416 assumes "coprime k (m::nat)"
1.417 shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
1.418 apply (rule cong_mult_rcancel_int [transferred])
1.419 using assms apply auto
1.420 -done
1.421 + done
1.422
1.423 lemma cong_mult_lcancel_nat:
1.424 - "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
1.425 + "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
1.426 by (simp add: mult_commute cong_mult_rcancel_nat)
1.427
1.428 lemma cong_mult_lcancel_int:
1.429 - "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
1.430 + "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
1.431 by (simp add: mult_commute cong_mult_rcancel_int)
1.432
1.433 (* was zcong_zgcd_zmult_zmod *)
1.434 @@ -395,7 +379,7 @@
1.435 apply auto
1.436 apply (rule_tac x = "a mod m" in exI)
1.437 apply (unfold cong_nat_def, auto)
1.438 -done
1.439 + done
1.440
1.441 lemma cong_less_unique_int:
1.442 "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
1.443 @@ -407,12 +391,12 @@
1.444 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
1.445 apply (auto simp add: cong_altdef_int dvd_def field_simps)
1.446 apply (rule_tac [!] x = "-k" in exI, auto)
1.447 -done
1.448 + done
1.449
1.450 -lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
1.451 +lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
1.452 (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
1.453 apply (rule iffI)
1.454 - apply (case_tac "b <= a")
1.455 + apply (cases "b <= a")
1.456 apply (subst (asm) cong_altdef_nat, assumption)
1.457 apply (unfold dvd_def, auto)
1.458 apply (rule_tac x = k in exI)
1.459 @@ -430,42 +414,40 @@
1.460 apply (erule ssubst)back
1.461 apply (erule subst)
1.462 apply auto
1.463 -done
1.464 + done
1.465
1.466 lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.467 apply (subst (asm) cong_iff_lin_int, auto)
1.468 - apply (subst add_commute)
1.469 + apply (subst add_commute)
1.470 apply (subst (2) gcd_commute_int)
1.471 apply (subst mult_commute)
1.472 apply (subst gcd_add_mult_int)
1.473 apply (rule gcd_commute_int)
1.474 done
1.475
1.476 -lemma cong_gcd_eq_nat:
1.477 +lemma cong_gcd_eq_nat:
1.478 assumes "[(a::nat) = b] (mod m)"
1.479 shows "gcd a m = gcd b m"
1.480 apply (rule cong_gcd_eq_int [transferred])
1.481 using assms apply auto
1.482 done
1.483
1.484 -lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
1.485 - coprime b m"
1.486 +lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.487 by (auto simp add: cong_gcd_eq_nat)
1.488
1.489 -lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
1.490 - coprime b m"
1.491 +lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.492 by (auto simp add: cong_gcd_eq_int)
1.493
1.494 -lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) =
1.495 - [a mod m = b mod m] (mod m)"
1.496 +lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
1.497 by (auto simp add: cong_nat_def)
1.498
1.499 -lemma cong_cong_mod_int: "[(a::int) = b] (mod m) =
1.500 - [a mod m = b mod m] (mod m)"
1.501 +lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
1.502 by (auto simp add: cong_int_def)
1.503
1.504 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
1.505 - by (subst (1 2) cong_altdef_int, auto)
1.506 + apply (subst (1 2) cong_altdef_int)
1.507 + apply auto
1.508 + done
1.509
1.510 lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
1.511 by auto
1.512 @@ -479,7 +461,7 @@
1.513 apply (unfold dvd_def, auto)
1.514 apply (rule mod_mod_cancel)
1.515 apply auto
1.516 -done
1.517 + done
1.518
1.519 lemma mod_dvd_mod:
1.520 assumes "0 < (m::nat)" and "m dvd b"
1.521 @@ -490,12 +472,12 @@
1.522 done
1.523 *)
1.524
1.525 -lemma cong_add_lcancel_nat:
1.526 - "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.527 +lemma cong_add_lcancel_nat:
1.528 + "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.529 by (simp add: cong_iff_lin_nat)
1.530
1.531 -lemma cong_add_lcancel_int:
1.532 - "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.533 +lemma cong_add_lcancel_int:
1.534 + "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.535 by (simp add: cong_iff_lin_int)
1.536
1.537 lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.538 @@ -504,43 +486,42 @@
1.539 lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.540 by (simp add: cong_iff_lin_int)
1.541
1.542 -lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.543 +lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.544 by (simp add: cong_iff_lin_nat)
1.545
1.546 -lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.547 +lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.548 by (simp add: cong_iff_lin_int)
1.549
1.550 -lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.551 +lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.552 by (simp add: cong_iff_lin_nat)
1.553
1.554 -lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.555 +lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.556 by (simp add: cong_iff_lin_int)
1.557
1.558 -lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.559 +lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.560 [x = y] (mod n)"
1.561 apply (auto simp add: cong_iff_lin_nat dvd_def)
1.562 apply (rule_tac x="k1 * k" in exI)
1.563 apply (rule_tac x="k2 * k" in exI)
1.564 apply (simp add: field_simps)
1.565 -done
1.566 + done
1.567
1.568 -lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.569 - [x = y] (mod n)"
1.570 +lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
1.571 by (auto simp add: cong_altdef_int dvd_def)
1.572
1.573 lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
1.574 - by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
1.575 + unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
1.576
1.577 lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
1.578 - by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
1.579 + unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
1.580
1.581 -lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.582 +lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.583 by (simp add: cong_nat_def)
1.584
1.585 -lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.586 +lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.587 by (simp add: cong_int_def)
1.588
1.589 -lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
1.590 +lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
1.591 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
1.592 by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
1.593
1.594 @@ -548,43 +529,43 @@
1.595 apply (simp add: cong_altdef_int)
1.596 apply (subst dvd_minus_iff [symmetric])
1.597 apply (simp add: field_simps)
1.598 -done
1.599 + done
1.600
1.601 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
1.602 by (auto simp add: cong_altdef_int)
1.603
1.604 -lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
1.605 +lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
1.606 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
1.607 - apply (case_tac "b > 0")
1.608 + apply (cases "b > 0")
1.609 apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
1.610 apply (subst (1 2) cong_modulus_neg_int)
1.611 apply (unfold cong_int_def)
1.612 apply (subgoal_tac "a * b = (-a * -b)")
1.613 apply (erule ssubst)
1.614 apply (subst zmod_zmult2_eq)
1.615 - apply (auto simp add: mod_add_left_eq)
1.616 -done
1.617 + apply (auto simp add: mod_add_left_eq)
1.618 + done
1.619
1.620 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
1.621 - apply (case_tac "a = 0")
1.622 + apply (cases "a = 0")
1.623 apply force
1.624 apply (subst (asm) cong_altdef_nat)
1.625 apply auto
1.626 -done
1.627 + done
1.628
1.629 lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
1.630 - by (unfold cong_nat_def, auto)
1.631 + unfolding cong_nat_def by auto
1.632
1.633 lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
1.634 - by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
1.635 + unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
1.636
1.637 -lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
1.638 +lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
1.639 a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
1.640 - apply (case_tac "n = 1")
1.641 + apply (cases "n = 1")
1.642 apply auto [1]
1.643 apply (drule_tac x = "a - 1" in spec)
1.644 apply force
1.645 - apply (case_tac "a = 0")
1.646 + apply (cases "a = 0")
1.647 apply (auto simp add: cong_0_1_nat) [1]
1.648 apply (rule iffI)
1.649 apply (drule cong_to_1_nat)
1.650 @@ -594,7 +575,7 @@
1.651 apply (auto simp add: field_simps) [1]
1.652 apply (subst cong_altdef_nat)
1.653 apply (auto simp add: dvd_def)
1.654 -done
1.655 + done
1.656
1.657 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
1.658 apply (subst cong_altdef_nat)
1.659 @@ -602,10 +583,10 @@
1.660 apply (unfold dvd_def, auto simp add: field_simps)
1.661 apply (rule_tac x = k in exI)
1.662 apply auto
1.663 -done
1.664 + done
1.665
1.666 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
1.667 - apply (case_tac "n = 0")
1.668 + apply (cases "n = 0")
1.669 apply force
1.670 apply (frule bezout_nat [of a n], auto)
1.671 apply (rule exI, erule ssubst)
1.672 @@ -617,11 +598,11 @@
1.673 apply simp
1.674 apply (rule cong_refl_nat)
1.675 apply (rule cong_refl_nat)
1.676 -done
1.677 + done
1.678
1.679 lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
1.680 - apply (case_tac "n = 0")
1.681 - apply (case_tac "a \<ge> 0")
1.682 + apply (cases "n = 0")
1.683 + apply (cases "a \<ge> 0")
1.684 apply auto
1.685 apply (rule_tac x = "-1" in exI)
1.686 apply auto
1.687 @@ -637,16 +618,15 @@
1.688 apply simp
1.689 apply (subst mult_commute)
1.690 apply (rule cong_refl_int)
1.691 -done
1.692 -
1.693 -lemma cong_solve_dvd_nat:
1.694 + done
1.695 +
1.696 +lemma cong_solve_dvd_nat:
1.697 assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
1.698 shows "EX x. [a * x = d] (mod n)"
1.699 proof -
1.700 - from cong_solve_nat [OF a] obtain x where
1.701 - "[a * x = gcd a n](mod n)"
1.702 + from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
1.703 by auto
1.704 - hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.705 + then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.706 by (elim cong_scalar2_nat)
1.707 also from b have "(d div gcd a n) * gcd a n = d"
1.708 by (rule dvd_div_mult_self)
1.709 @@ -656,14 +636,13 @@
1.710 by auto
1.711 qed
1.712
1.713 -lemma cong_solve_dvd_int:
1.714 +lemma cong_solve_dvd_int:
1.715 assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
1.716 shows "EX x. [a * x = d] (mod n)"
1.717 proof -
1.718 - from cong_solve_int [OF a] obtain x where
1.719 - "[a * x = gcd a n](mod n)"
1.720 + from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
1.721 by auto
1.722 - hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.723 + then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.724 by (elim cong_scalar2_int)
1.725 also from b have "(d div gcd a n) * gcd a n = d"
1.726 by (rule dvd_div_mult_self)
1.727 @@ -673,56 +652,52 @@
1.728 by auto
1.729 qed
1.730
1.731 -lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow>
1.732 - EX x. [a * x = 1] (mod n)"
1.733 - apply (case_tac "a = 0")
1.734 +lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
1.735 + apply (cases "a = 0")
1.736 apply force
1.737 apply (frule cong_solve_nat [of a n])
1.738 apply auto
1.739 -done
1.740 + done
1.741
1.742 -lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow>
1.743 - EX x. [a * x = 1] (mod n)"
1.744 - apply (case_tac "a = 0")
1.745 +lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
1.746 + apply (cases "a = 0")
1.747 apply auto
1.748 - apply (case_tac "n \<ge> 0")
1.749 + apply (cases "n \<ge> 0")
1.750 apply auto
1.751 apply (subst cong_int_def, auto)
1.752 apply (frule cong_solve_int [of a n])
1.753 apply auto
1.754 -done
1.755 + done
1.756
1.757 -lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m =
1.758 - (EX x. [a * x = 1] (mod m))"
1.759 +lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
1.760 apply (auto intro: cong_solve_coprime_nat)
1.761 apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
1.762 -done
1.763 + done
1.764
1.765 -lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m =
1.766 - (EX x. [a * x = 1] (mod m))"
1.767 +lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
1.768 apply (auto intro: cong_solve_coprime_int)
1.769 apply (unfold cong_int_def)
1.770 apply (auto intro: invertible_coprime_int)
1.771 -done
1.772 + done
1.773
1.774 -lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
1.775 +lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
1.776 (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
1.777 apply (subst coprime_iff_invertible_int)
1.778 apply auto
1.779 apply (auto simp add: cong_int_def)
1.780 apply (rule_tac x = "x mod m" in exI)
1.781 apply (auto simp add: mod_mult_right_eq [symmetric])
1.782 -done
1.783 + done
1.784
1.785
1.786 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
1.787 [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.788 - apply (case_tac "y \<le> x")
1.789 + apply (cases "y \<le> x")
1.790 apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
1.791 apply (rule cong_sym_nat)
1.792 apply (subst (asm) (1 2) cong_sym_eq_nat)
1.793 apply (auto simp add: cong_altdef_nat lcm_least_nat)
1.794 -done
1.795 + done
1.796
1.797 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
1.798 [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.799 @@ -730,15 +705,17 @@
1.800
1.801 lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
1.802 [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
1.803 - apply (frule (1) cong_cong_lcm_nat)back
1.804 + apply (frule (1) cong_cong_lcm_nat)
1.805 + back
1.806 apply (simp add: lcm_nat_def)
1.807 -done
1.808 + done
1.809
1.810 lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
1.811 [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
1.812 - apply (frule (1) cong_cong_lcm_int)back
1.813 + apply (frule (1) cong_cong_lcm_int)
1.814 + back
1.815 apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
1.816 -done
1.817 + done
1.818
1.819 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
1.820 (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.821 @@ -750,7 +727,7 @@
1.822 apply (subst gcd_commute_nat)
1.823 apply (rule setprod_coprime_nat)
1.824 apply auto
1.825 -done
1.826 + done
1.827
1.828 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
1.829 (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.830 @@ -762,20 +739,18 @@
1.831 apply (subst gcd_commute_int)
1.832 apply (rule setprod_coprime_int)
1.833 apply auto
1.834 -done
1.835 + done
1.836
1.837 -lemma binary_chinese_remainder_aux_nat:
1.838 +lemma binary_chinese_remainder_aux_nat:
1.839 assumes a: "coprime (m1::nat) m2"
1.840 shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
1.841 [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
1.842 proof -
1.843 - from cong_solve_coprime_nat [OF a]
1.844 - obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.845 + from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.846 by auto
1.847 - from a have b: "coprime m2 m1"
1.848 + from a have b: "coprime m2 m1"
1.849 by (subst gcd_commute_nat)
1.850 - from cong_solve_coprime_nat [OF b]
1.851 - obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.852 + from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.853 by auto
1.854 have "[m1 * x1 = 0] (mod m1)"
1.855 by (subst mult_commute, rule cong_mult_self_nat)
1.856 @@ -785,18 +760,16 @@
1.857 ultimately show ?thesis by blast
1.858 qed
1.859
1.860 -lemma binary_chinese_remainder_aux_int:
1.861 +lemma binary_chinese_remainder_aux_int:
1.862 assumes a: "coprime (m1::int) m2"
1.863 shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
1.864 [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
1.865 proof -
1.866 - from cong_solve_coprime_int [OF a]
1.867 - obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.868 + from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.869 by auto
1.870 - from a have b: "coprime m2 m1"
1.871 + from a have b: "coprime m2 m1"
1.872 by (subst gcd_commute_int)
1.873 - from cong_solve_coprime_int [OF b]
1.874 - obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.875 + from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.876 by auto
1.877 have "[m1 * x1 = 0] (mod m1)"
1.878 by (subst mult_commute, rule cong_mult_self_int)
1.879 @@ -811,8 +784,8 @@
1.880 shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
1.881 proof -
1.882 from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
1.883 - where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
1.884 - "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
1.885 + where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
1.886 + "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
1.887 by blast
1.888 let ?x = "u1 * b1 + u2 * b2"
1.889 have "[?x = u1 * 1 + u2 * 0] (mod m1)"
1.890 @@ -822,7 +795,7 @@
1.891 apply (rule cong_scalar2_nat)
1.892 apply (rule `[b2 = 0] (mod m1)`)
1.893 done
1.894 - hence "[?x = u1] (mod m1)" by simp
1.895 + then have "[?x = u1] (mod m1)" by simp
1.896 have "[?x = u1 * 0 + u2 * 1] (mod m2)"
1.897 apply (rule cong_add_nat)
1.898 apply (rule cong_scalar2_nat)
1.899 @@ -830,7 +803,7 @@
1.900 apply (rule cong_scalar2_nat)
1.901 apply (rule `[b2 = 1] (mod m2)`)
1.902 done
1.903 - hence "[?x = u2] (mod m2)" by simp
1.904 + then have "[?x = u2] (mod m2)" by simp
1.905 with `[?x = u1] (mod m1)` show ?thesis by blast
1.906 qed
1.907
1.908 @@ -850,7 +823,7 @@
1.909 apply (rule cong_scalar2_int)
1.910 apply (rule `[b2 = 0] (mod m1)`)
1.911 done
1.912 - hence "[?x = u1] (mod m1)" by simp
1.913 + then have "[?x = u1] (mod m1)" by simp
1.914 have "[?x = u1 * 0 + u2 * 1] (mod m2)"
1.915 apply (rule cong_add_int)
1.916 apply (rule cong_scalar2_int)
1.917 @@ -858,42 +831,42 @@
1.918 apply (rule cong_scalar2_int)
1.919 apply (rule `[b2 = 1] (mod m2)`)
1.920 done
1.921 - hence "[?x = u2] (mod m2)" by simp
1.922 + then have "[?x = u2] (mod m2)" by simp
1.923 with `[?x = u1] (mod m1)` show ?thesis by blast
1.924 qed
1.925
1.926 -lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
1.927 +lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
1.928 [x = y] (mod m)"
1.929 - apply (case_tac "y \<le> x")
1.930 + apply (cases "y \<le> x")
1.931 apply (simp add: cong_altdef_nat)
1.932 apply (erule dvd_mult_left)
1.933 apply (rule cong_sym_nat)
1.934 apply (subst (asm) cong_sym_eq_nat)
1.935 - apply (simp add: cong_altdef_nat)
1.936 + apply (simp add: cong_altdef_nat)
1.937 apply (erule dvd_mult_left)
1.938 -done
1.939 + done
1.940
1.941 -lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
1.942 +lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
1.943 [x = y] (mod m)"
1.944 - apply (simp add: cong_altdef_int)
1.945 + apply (simp add: cong_altdef_int)
1.946 apply (erule dvd_mult_left)
1.947 -done
1.948 + done
1.949
1.950 -lemma cong_less_modulus_unique_nat:
1.951 +lemma cong_less_modulus_unique_nat:
1.952 "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
1.953 by (simp add: cong_nat_def)
1.954
1.955 lemma binary_chinese_remainder_unique_nat:
1.956 - assumes a: "coprime (m1::nat) m2" and
1.957 - nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
1.958 + assumes a: "coprime (m1::nat) m2"
1.959 + and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
1.960 shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
1.961 proof -
1.962 - from binary_chinese_remainder_nat [OF a] obtain y where
1.963 + from binary_chinese_remainder_nat [OF a] obtain y where
1.964 "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
1.965 by blast
1.966 let ?x = "y mod (m1 * m2)"
1.967 from nz have less: "?x < m1 * m2"
1.968 - by auto
1.969 + by auto
1.970 have one: "[?x = u1] (mod m1)"
1.971 apply (rule cong_trans_nat)
1.972 prefer 2
1.973 @@ -911,9 +884,8 @@
1.974 apply (rule cong_mod_nat)
1.975 using nz apply auto
1.976 done
1.977 - have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
1.978 - z = ?x"
1.979 - proof (clarify)
1.980 + have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
1.981 + proof clarify
1.982 fix z
1.983 assume "z < m1 * m2"
1.984 assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)"
1.985 @@ -935,46 +907,43 @@
1.986 apply (intro cong_less_modulus_unique_nat)
1.987 apply (auto, erule cong_sym_nat)
1.988 done
1.989 - qed
1.990 - with less one two show ?thesis
1.991 - by auto
1.992 + qed
1.993 + with less one two show ?thesis by auto
1.994 qed
1.995
1.996 lemma chinese_remainder_aux_nat:
1.997 - fixes A :: "'a set" and
1.998 - m :: "'a \<Rightarrow> nat"
1.999 - assumes fin: "finite A" and
1.1000 - cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1001 - shows "EX b. (ALL i : A.
1.1002 - [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
1.1003 + fixes A :: "'a set"
1.1004 + and m :: "'a \<Rightarrow> nat"
1.1005 + assumes fin: "finite A"
1.1006 + and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1007 + shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
1.1008 proof (rule finite_set_choice, rule fin, rule ballI)
1.1009 fix i
1.1010 assume "i : A"
1.1011 with cop have "coprime (PROD j : A - {i}. m j) (m i)"
1.1012 by (intro setprod_coprime_nat, auto)
1.1013 - hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
1.1014 + then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
1.1015 by (elim cong_solve_coprime_nat)
1.1016 then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
1.1017 by auto
1.1018 - moreover have "[(PROD j : A - {i}. m j) * x = 0]
1.1019 + moreover have "[(PROD j : A - {i}. m j) * x = 0]
1.1020 (mod (PROD j : A - {i}. m j))"
1.1021 by (subst mult_commute, rule cong_mult_self_nat)
1.1022 - ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
1.1023 + ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
1.1024 (mod setprod m (A - {i}))"
1.1025 by blast
1.1026 qed
1.1027
1.1028 lemma chinese_remainder_nat:
1.1029 - fixes A :: "'a set" and
1.1030 - m :: "'a \<Rightarrow> nat" and
1.1031 - u :: "'a \<Rightarrow> nat"
1.1032 - assumes
1.1033 - fin: "finite A" and
1.1034 - cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1035 + fixes A :: "'a set"
1.1036 + and m :: "'a \<Rightarrow> nat"
1.1037 + and u :: "'a \<Rightarrow> nat"
1.1038 + assumes fin: "finite A"
1.1039 + and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1040 shows "EX x. (ALL i:A. [x = u i] (mod m i))"
1.1041 proof -
1.1042 from chinese_remainder_aux_nat [OF fin cop] obtain b where
1.1043 - bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
1.1044 + bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
1.1045 [b i = 0] (mod (PROD j : A - {i}. m j))"
1.1046 by blast
1.1047 let ?x = "SUM i:A. (u i) * (b i)"
1.1048 @@ -982,12 +951,12 @@
1.1049 proof (rule exI, clarify)
1.1050 fix i
1.1051 assume a: "i : A"
1.1052 - show "[?x = u i] (mod m i)"
1.1053 + show "[?x = u i] (mod m i)"
1.1054 proof -
1.1055 - from fin a have "?x = (SUM j:{i}. u j * b j) +
1.1056 + from fin a have "?x = (SUM j:{i}. u j * b j) +
1.1057 (SUM j:A-{i}. u j * b j)"
1.1058 by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
1.1059 - hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
1.1060 + then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
1.1061 by auto
1.1062 also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
1.1063 u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
1.1064 @@ -1010,35 +979,34 @@
1.1065 qed
1.1066 qed
1.1067
1.1068 -lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
1.1069 +lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
1.1070 (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.1071 (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
1.1072 - [x = y] (mod (PROD i:A. m i))"
1.1073 + [x = y] (mod (PROD i:A. m i))"
1.1074 apply (induct set: finite)
1.1075 apply auto
1.1076 apply (erule (1) coprime_cong_mult_nat)
1.1077 apply (subst gcd_commute_nat)
1.1078 apply (rule setprod_coprime_nat)
1.1079 apply auto
1.1080 -done
1.1081 + done
1.1082
1.1083 lemma chinese_remainder_unique_nat:
1.1084 - fixes A :: "'a set" and
1.1085 - m :: "'a \<Rightarrow> nat" and
1.1086 - u :: "'a \<Rightarrow> nat"
1.1087 - assumes
1.1088 - fin: "finite A" and
1.1089 - nz: "ALL i:A. m i \<noteq> 0" and
1.1090 - cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1091 + fixes A :: "'a set"
1.1092 + and m :: "'a \<Rightarrow> nat"
1.1093 + and u :: "'a \<Rightarrow> nat"
1.1094 + assumes fin: "finite A"
1.1095 + and nz: "ALL i:A. m i \<noteq> 0"
1.1096 + and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1097 shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
1.1098 proof -
1.1099 - from chinese_remainder_nat [OF fin cop] obtain y where
1.1100 - one: "(ALL i:A. [y = u i] (mod m i))"
1.1101 + from chinese_remainder_nat [OF fin cop]
1.1102 + obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
1.1103 by blast
1.1104 let ?x = "y mod (PROD i:A. m i)"
1.1105 from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
1.1106 by auto
1.1107 - hence less: "?x < (PROD i:A. m i)"
1.1108 + then have less: "?x < (PROD i:A. m i)"
1.1109 by auto
1.1110 have cong: "ALL i:A. [?x = u i] (mod m i)"
1.1111 apply auto
1.1112 @@ -1052,28 +1020,29 @@
1.1113 apply (rule fin)
1.1114 apply assumption
1.1115 done
1.1116 - have unique: "ALL z. z < (PROD i:A. m i) \<and>
1.1117 + have unique: "ALL z. z < (PROD i:A. m i) \<and>
1.1118 (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
1.1119 proof (clarify)
1.1120 fix z
1.1121 assume zless: "z < (PROD i:A. m i)"
1.1122 assume zcong: "(ALL i:A. [z = u i] (mod m i))"
1.1123 have "ALL i:A. [?x = z] (mod m i)"
1.1124 - apply clarify
1.1125 + apply clarify
1.1126 apply (rule cong_trans_nat)
1.1127 using cong apply (erule bspec)
1.1128 apply (rule cong_sym_nat)
1.1129 using zcong apply auto
1.1130 done
1.1131 with fin cop have "[?x = z] (mod (PROD i:A. m i))"
1.1132 - by (intro coprime_cong_prod_nat, auto)
1.1133 + apply (intro coprime_cong_prod_nat)
1.1134 + apply auto
1.1135 + done
1.1136 with zless less show "z = ?x"
1.1137 apply (intro cong_less_modulus_unique_nat)
1.1138 apply (auto, erule cong_sym_nat)
1.1139 done
1.1140 - qed
1.1141 - from less cong unique show ?thesis
1.1142 - by blast
1.1143 + qed
1.1144 + from less cong unique show ?thesis by blast
1.1145 qed
1.1146
1.1147 end