src/HOL/Number_Theory/Cong.thy
 changeset 44872 a98ef45122f3 parent 41959 b460124855b8 child 47163 248376f8881d
```     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.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.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 -
1.85 -begin
1.86 +begin
1.87
1.88 -definition
1.89 -  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
1.90 -where
1.91 -  "cong_nat x y m = ((x mod m) = (y mod m))"
1.92 +definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
1.93 +  where "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 -
1.105 -begin
1.106 +begin
1.107
1.108 -definition
1.109 -  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
1.110 -where
1.111 -  "cong_int x y m = ((x mod m) = (y mod m))"
1.112 +definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
1.113 +  where "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.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.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.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.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 -
1.261 -lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.262 -  apply (induct k)
1.263 -  apply (auto simp add: cong_mult_nat)
1.264 -  done
1.265 -
1.266 -lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.267 -  apply (induct k)
1.268 -  apply (auto simp add: cong_mult_int)
1.269    done
1.270
1.271 -lemma cong_setsum_nat [rule_format]:
1.272 -    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.273 +lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.274 +  by (induct k) (auto simp add: cong_mult_nat)
1.275 +
1.276 +lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
1.277 +  by (induct k) (auto simp add: cong_mult_int)
1.278 +
1.279 +lemma cong_setsum_nat [rule_format]:
1.280 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.281        [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
1.282 -  apply (case_tac "finite A")
1.283 +  apply (cases "finite A")
1.284    apply (induct set: finite)
1.286 -done
1.287 +  done
1.288
1.289  lemma cong_setsum_int [rule_format]:
1.290 -    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.291 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.292        [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
1.293 -  apply (case_tac "finite A")
1.294 +  apply (cases "finite A")
1.295    apply (induct set: finite)
1.297 -done
1.298 +  done
1.299
1.300 -lemma cong_setprod_nat [rule_format]:
1.301 -    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.302 +lemma cong_setprod_nat [rule_format]:
1.303 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
1.304        [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
1.305 -  apply (case_tac "finite A")
1.306 +  apply (cases "finite A")
1.307    apply (induct set: finite)
1.308    apply (auto intro: cong_mult_nat)
1.309 -done
1.310 +  done
1.311
1.312 -lemma cong_setprod_int [rule_format]:
1.313 -    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.314 +lemma cong_setprod_int [rule_format]:
1.315 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
1.316        [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
1.317 -  apply (case_tac "finite A")
1.318 +  apply (cases "finite A")
1.319    apply (induct set: finite)
1.320    apply (auto intro: cong_mult_int)
1.321 -done
1.322 +  done
1.323
1.324  lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
1.325 -  by (rule cong_mult_nat, simp_all)
1.326 +  by (rule cong_mult_nat) simp_all
1.327
1.328  lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
1.329 -  by (rule cong_mult_int, simp_all)
1.330 +  by (rule cong_mult_int) simp_all
1.331
1.332  lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
1.333 -  by (rule cong_mult_nat, simp_all)
1.334 +  by (rule cong_mult_nat) simp_all
1.335
1.336  lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
1.337 -  by (rule cong_mult_int, simp_all)
1.338 +  by (rule cong_mult_int) simp_all
1.339
1.340  lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
1.341 -  by (unfold cong_nat_def, auto)
1.342 +  unfolding cong_nat_def by auto
1.343
1.344  lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
1.345 -  by (unfold cong_int_def, auto)
1.346 +  unfolding cong_int_def by auto
1.347
1.348  lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
1.349    apply (rule iffI)
1.350    apply (erule cong_diff_int [of a b m b b, simplified])
1.351    apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
1.352 -done
1.353 +  done
1.354
1.355  lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
1.356      [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
1.357 @@ -307,29 +291,29 @@
1.358    shows "[a = b] (mod m) = [a - b = 0] (mod m)"
1.359    using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
1.360
1.361 -lemma cong_diff_cong_0'_nat:
1.362 -  "[(x::nat) = y] (mod n) \<longleftrightarrow>
1.363 +lemma cong_diff_cong_0'_nat:
1.364 +  "[(x::nat) = y] (mod n) \<longleftrightarrow>
1.365      (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
1.366 -  apply (case_tac "y <= x")
1.367 +  apply (cases "y <= x")
1.368    apply (frule cong_eq_diff_cong_0_nat [where m = n])
1.369    apply auto [1]
1.370    apply (subgoal_tac "x <= y")
1.371    apply (frule cong_eq_diff_cong_0_nat [where m = n])
1.372    apply (subst cong_sym_eq_nat)
1.373    apply auto
1.374 -done
1.375 +  done
1.376
1.377  lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
1.378    apply (subst cong_eq_diff_cong_0_nat, assumption)
1.379    apply (unfold cong_nat_def)
1.380    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
1.381 -done
1.382 +  done
1.383
1.384  lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
1.385    apply (subst cong_eq_diff_cong_0_int)
1.386    apply (unfold cong_int_def)
1.387    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
1.388 -done
1.389 +  done
1.390
1.391  lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
1.393 @@ -342,29 +326,29 @@
1.394    (* any way around this? *)
1.395    apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
1.396    apply (auto simp add: field_simps)
1.397 -done
1.398 +  done
1.399
1.400  lemma cong_mult_rcancel_int:
1.401 -  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
1.402 +    "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
1.403    apply (subst (1 2) cong_altdef_int)
1.404    apply (subst left_diff_distrib [symmetric])
1.405    apply (rule coprime_dvd_mult_iff_int)
1.406    apply (subst gcd_commute_int, assumption)
1.407 -done
1.408 +  done
1.409
1.410  lemma cong_mult_rcancel_nat:
1.411    assumes  "coprime k (m::nat)"
1.412    shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
1.413    apply (rule cong_mult_rcancel_int [transferred])
1.414    using assms apply auto
1.415 -done
1.416 +  done
1.417
1.418  lemma cong_mult_lcancel_nat:
1.419 -  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
1.420 +    "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
1.421    by (simp add: mult_commute cong_mult_rcancel_nat)
1.422
1.423  lemma cong_mult_lcancel_int:
1.424 -  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
1.425 +    "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
1.426    by (simp add: mult_commute cong_mult_rcancel_int)
1.427
1.428  (* was zcong_zgcd_zmult_zmod *)
1.429 @@ -395,7 +379,7 @@
1.430    apply auto
1.431    apply (rule_tac x = "a mod m" in exI)
1.432    apply (unfold cong_nat_def, auto)
1.433 -done
1.434 +  done
1.435
1.436  lemma cong_less_unique_int:
1.437      "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
1.438 @@ -407,12 +391,12 @@
1.439  lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
1.440    apply (auto simp add: cong_altdef_int dvd_def field_simps)
1.441    apply (rule_tac [!] x = "-k" in exI, auto)
1.442 -done
1.443 +  done
1.444
1.445 -lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
1.446 +lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
1.447      (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
1.448    apply (rule iffI)
1.449 -  apply (case_tac "b <= a")
1.450 +  apply (cases "b <= a")
1.451    apply (subst (asm) cong_altdef_nat, assumption)
1.452    apply (unfold dvd_def, auto)
1.453    apply (rule_tac x = k in exI)
1.454 @@ -430,42 +414,40 @@
1.455    apply (erule ssubst)back
1.456    apply (erule subst)
1.457    apply auto
1.458 -done
1.459 +  done
1.460
1.461  lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.462    apply (subst (asm) cong_iff_lin_int, auto)
1.465    apply (subst (2) gcd_commute_int)
1.466    apply (subst mult_commute)
1.468    apply (rule gcd_commute_int)
1.469    done
1.470
1.471 -lemma cong_gcd_eq_nat:
1.472 +lemma cong_gcd_eq_nat:
1.473    assumes "[(a::nat) = b] (mod m)"
1.474    shows "gcd a m = gcd b m"
1.475    apply (rule cong_gcd_eq_int [transferred])
1.476    using assms apply auto
1.477    done
1.478
1.479 -lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
1.480 -    coprime b m"
1.481 +lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.482    by (auto simp add: cong_gcd_eq_nat)
1.483
1.484 -lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
1.485 -    coprime b m"
1.486 +lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.487    by (auto simp add: cong_gcd_eq_int)
1.488
1.489 -lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) =
1.490 -    [a mod m = b mod m] (mod m)"
1.491 +lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
1.492    by (auto simp add: cong_nat_def)
1.493
1.494 -lemma cong_cong_mod_int: "[(a::int) = b] (mod m) =
1.495 -    [a mod m = b mod m] (mod m)"
1.496 +lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
1.497    by (auto simp add: cong_int_def)
1.498
1.499  lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
1.500 -  by (subst (1 2) cong_altdef_int, auto)
1.501 +  apply (subst (1 2) cong_altdef_int)
1.502 +  apply auto
1.503 +  done
1.504
1.505  lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
1.506    by auto
1.507 @@ -479,7 +461,7 @@
1.508    apply (unfold dvd_def, auto)
1.509    apply (rule mod_mod_cancel)
1.510    apply auto
1.511 -done
1.512 +  done
1.513
1.514  lemma mod_dvd_mod:
1.515    assumes "0 < (m::nat)" and "m dvd b"
1.516 @@ -490,12 +472,12 @@
1.517    done
1.518  *)
1.519
1.521 -    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.523 +    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.525
1.527 -    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.529 +    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.531
1.532  lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.533 @@ -504,43 +486,42 @@
1.534  lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.536
1.537 -lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.538 +lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.540
1.541 -lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.542 +lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.544
1.545 -lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.546 +lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.548
1.549 -lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.550 +lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.552
1.553 -lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.554 +lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.555      [x = y] (mod n)"
1.556    apply (auto simp add: cong_iff_lin_nat dvd_def)
1.557    apply (rule_tac x="k1 * k" in exI)
1.558    apply (rule_tac x="k2 * k" in exI)
1.560 -done
1.561 +  done
1.562
1.563 -lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
1.564 -    [x = y] (mod n)"
1.565 +lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
1.566    by (auto simp add: cong_altdef_int dvd_def)
1.567
1.568  lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
1.569 -  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
1.570 +  unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
1.571
1.572  lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
1.573 -  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
1.574 +  unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
1.575
1.576 -lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.577 +lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.579
1.580 -lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.581 +lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
1.583
1.584 -lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
1.585 +lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
1.586      \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
1.588
1.589 @@ -548,43 +529,43 @@
1.591    apply (subst dvd_minus_iff [symmetric])
1.593 -done
1.594 +  done
1.595
1.596  lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
1.597    by (auto simp add: cong_altdef_int)
1.598
1.599 -lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
1.600 +lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
1.601      \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
1.602 -  apply (case_tac "b > 0")
1.603 +  apply (cases "b > 0")
1.605    apply (subst (1 2) cong_modulus_neg_int)
1.606    apply (unfold cong_int_def)
1.607    apply (subgoal_tac "a * b = (-a * -b)")
1.608    apply (erule ssubst)
1.609    apply (subst zmod_zmult2_eq)
1.611 -done
1.613 +  done
1.614
1.615  lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
1.616 -  apply (case_tac "a = 0")
1.617 +  apply (cases "a = 0")
1.618    apply force
1.619    apply (subst (asm) cong_altdef_nat)
1.620    apply auto
1.621 -done
1.622 +  done
1.623
1.624  lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
1.625 -  by (unfold cong_nat_def, auto)
1.626 +  unfolding cong_nat_def by auto
1.627
1.628  lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
1.629 -  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
1.630 +  unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
1.631
1.632 -lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
1.633 +lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
1.634      a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
1.635 -  apply (case_tac "n = 1")
1.636 +  apply (cases "n = 1")
1.637    apply auto [1]
1.638    apply (drule_tac x = "a - 1" in spec)
1.639    apply force
1.640 -  apply (case_tac "a = 0")
1.641 +  apply (cases "a = 0")
1.642    apply (auto simp add: cong_0_1_nat) [1]
1.643    apply (rule iffI)
1.644    apply (drule cong_to_1_nat)
1.645 @@ -594,7 +575,7 @@
1.646    apply (auto simp add: field_simps) [1]
1.647    apply (subst cong_altdef_nat)
1.648    apply (auto simp add: dvd_def)
1.649 -done
1.650 +  done
1.651
1.652  lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
1.653    apply (subst cong_altdef_nat)
1.654 @@ -602,10 +583,10 @@
1.655    apply (unfold dvd_def, auto simp add: field_simps)
1.656    apply (rule_tac x = k in exI)
1.657    apply auto
1.658 -done
1.659 +  done
1.660
1.661  lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
1.662 -  apply (case_tac "n = 0")
1.663 +  apply (cases "n = 0")
1.664    apply force
1.665    apply (frule bezout_nat [of a n], auto)
1.666    apply (rule exI, erule ssubst)
1.667 @@ -617,11 +598,11 @@
1.668    apply simp
1.669    apply (rule cong_refl_nat)
1.670    apply (rule cong_refl_nat)
1.671 -done
1.672 +  done
1.673
1.674  lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
1.675 -  apply (case_tac "n = 0")
1.676 -  apply (case_tac "a \<ge> 0")
1.677 +  apply (cases "n = 0")
1.678 +  apply (cases "a \<ge> 0")
1.679    apply auto
1.680    apply (rule_tac x = "-1" in exI)
1.681    apply auto
1.682 @@ -637,16 +618,15 @@
1.683    apply simp
1.684    apply (subst mult_commute)
1.685    apply (rule cong_refl_int)
1.686 -done
1.687 -
1.688 -lemma cong_solve_dvd_nat:
1.689 +  done
1.690 +
1.691 +lemma cong_solve_dvd_nat:
1.692    assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
1.693    shows "EX x. [a * x = d] (mod n)"
1.694  proof -
1.695 -  from cong_solve_nat [OF a] obtain x where
1.696 -      "[a * x = gcd a n](mod n)"
1.697 +  from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
1.698      by auto
1.699 -  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.700 +  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.701      by (elim cong_scalar2_nat)
1.702    also from b have "(d div gcd a n) * gcd a n = d"
1.703      by (rule dvd_div_mult_self)
1.704 @@ -656,14 +636,13 @@
1.705      by auto
1.706  qed
1.707
1.708 -lemma cong_solve_dvd_int:
1.709 +lemma cong_solve_dvd_int:
1.710    assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
1.711    shows "EX x. [a * x = d] (mod n)"
1.712  proof -
1.713 -  from cong_solve_int [OF a] obtain x where
1.714 -      "[a * x = gcd a n](mod n)"
1.715 +  from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
1.716      by auto
1.717 -  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.718 +  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
1.719      by (elim cong_scalar2_int)
1.720    also from b have "(d div gcd a n) * gcd a n = d"
1.721      by (rule dvd_div_mult_self)
1.722 @@ -673,56 +652,52 @@
1.723      by auto
1.724  qed
1.725
1.726 -lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow>
1.727 -    EX x. [a * x = 1] (mod n)"
1.728 -  apply (case_tac "a = 0")
1.729 +lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
1.730 +  apply (cases "a = 0")
1.731    apply force
1.732    apply (frule cong_solve_nat [of a n])
1.733    apply auto
1.734 -done
1.735 +  done
1.736
1.737 -lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow>
1.738 -    EX x. [a * x = 1] (mod n)"
1.739 -  apply (case_tac "a = 0")
1.740 +lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
1.741 +  apply (cases "a = 0")
1.742    apply auto
1.743 -  apply (case_tac "n \<ge> 0")
1.744 +  apply (cases "n \<ge> 0")
1.745    apply auto
1.746    apply (subst cong_int_def, auto)
1.747    apply (frule cong_solve_int [of a n])
1.748    apply auto
1.749 -done
1.750 +  done
1.751
1.752 -lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m =
1.753 -    (EX x. [a * x = 1] (mod m))"
1.754 +lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
1.755    apply (auto intro: cong_solve_coprime_nat)
1.756    apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
1.757 -done
1.758 +  done
1.759
1.760 -lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m =
1.761 -    (EX x. [a * x = 1] (mod m))"
1.762 +lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
1.763    apply (auto intro: cong_solve_coprime_int)
1.764    apply (unfold cong_int_def)
1.765    apply (auto intro: invertible_coprime_int)
1.766 -done
1.767 +  done
1.768
1.769 -lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
1.770 +lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
1.771      (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
1.772    apply (subst coprime_iff_invertible_int)
1.773    apply auto
1.774    apply (auto simp add: cong_int_def)
1.775    apply (rule_tac x = "x mod m" in exI)
1.776    apply (auto simp add: mod_mult_right_eq [symmetric])
1.777 -done
1.778 +  done
1.779
1.780
1.781  lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
1.782      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.783 -  apply (case_tac "y \<le> x")
1.784 +  apply (cases "y \<le> x")
1.785    apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
1.786    apply (rule cong_sym_nat)
1.787    apply (subst (asm) (1 2) cong_sym_eq_nat)
1.788    apply (auto simp add: cong_altdef_nat lcm_least_nat)
1.789 -done
1.790 +  done
1.791
1.792  lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
1.793      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.794 @@ -730,15 +705,17 @@
1.795
1.796  lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
1.797      [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
1.798 -  apply (frule (1) cong_cong_lcm_nat)back
1.799 +  apply (frule (1) cong_cong_lcm_nat)
1.800 +  back
1.802 -done
1.803 +  done
1.804
1.805  lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
1.806      [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
1.807 -  apply (frule (1) cong_cong_lcm_int)back
1.808 +  apply (frule (1) cong_cong_lcm_int)
1.809 +  back
1.810    apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
1.811 -done
1.812 +  done
1.813
1.814  lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
1.815      (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.816 @@ -750,7 +727,7 @@
1.817    apply (subst gcd_commute_nat)
1.818    apply (rule setprod_coprime_nat)
1.819    apply auto
1.820 -done
1.821 +  done
1.822
1.823  lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
1.824      (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.825 @@ -762,20 +739,18 @@
1.826    apply (subst gcd_commute_int)
1.827    apply (rule setprod_coprime_int)
1.828    apply auto
1.829 -done
1.830 +  done
1.831
1.832 -lemma binary_chinese_remainder_aux_nat:
1.833 +lemma binary_chinese_remainder_aux_nat:
1.834    assumes a: "coprime (m1::nat) m2"
1.835    shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
1.836      [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
1.837  proof -
1.838 -  from cong_solve_coprime_nat [OF a]
1.839 -      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.840 +  from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.841      by auto
1.842 -  from a have b: "coprime m2 m1"
1.843 +  from a have b: "coprime m2 m1"
1.844      by (subst gcd_commute_nat)
1.845 -  from cong_solve_coprime_nat [OF b]
1.846 -      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.847 +  from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.848      by auto
1.849    have "[m1 * x1 = 0] (mod m1)"
1.850      by (subst mult_commute, rule cong_mult_self_nat)
1.851 @@ -785,18 +760,16 @@
1.852    ultimately show ?thesis by blast
1.853  qed
1.854
1.855 -lemma binary_chinese_remainder_aux_int:
1.856 +lemma binary_chinese_remainder_aux_int:
1.857    assumes a: "coprime (m1::int) m2"
1.858    shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
1.859      [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
1.860  proof -
1.861 -  from cong_solve_coprime_int [OF a]
1.862 -      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.863 +  from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
1.864      by auto
1.865 -  from a have b: "coprime m2 m1"
1.866 +  from a have b: "coprime m2 m1"
1.867      by (subst gcd_commute_int)
1.868 -  from cong_solve_coprime_int [OF b]
1.869 -      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.870 +  from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
1.871      by auto
1.872    have "[m1 * x1 = 0] (mod m1)"
1.873      by (subst mult_commute, rule cong_mult_self_int)
1.874 @@ -811,8 +784,8 @@
1.875    shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
1.876  proof -
1.877    from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
1.878 -    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
1.879 -          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
1.880 +      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
1.881 +            "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
1.882      by blast
1.883    let ?x = "u1 * b1 + u2 * b2"
1.884    have "[?x = u1 * 1 + u2 * 0] (mod m1)"
1.885 @@ -822,7 +795,7 @@
1.886      apply (rule cong_scalar2_nat)
1.887      apply (rule `[b2 = 0] (mod m1)`)
1.888      done
1.889 -  hence "[?x = u1] (mod m1)" by simp
1.890 +  then have "[?x = u1] (mod m1)" by simp
1.891    have "[?x = u1 * 0 + u2 * 1] (mod m2)"
1.893      apply (rule cong_scalar2_nat)
1.894 @@ -830,7 +803,7 @@
1.895      apply (rule cong_scalar2_nat)
1.896      apply (rule `[b2 = 1] (mod m2)`)
1.897      done
1.898 -  hence "[?x = u2] (mod m2)" by simp
1.899 +  then have "[?x = u2] (mod m2)" by simp
1.900    with `[?x = u1] (mod m1)` show ?thesis by blast
1.901  qed
1.902
1.903 @@ -850,7 +823,7 @@
1.904      apply (rule cong_scalar2_int)
1.905      apply (rule `[b2 = 0] (mod m1)`)
1.906      done
1.907 -  hence "[?x = u1] (mod m1)" by simp
1.908 +  then have "[?x = u1] (mod m1)" by simp
1.909    have "[?x = u1 * 0 + u2 * 1] (mod m2)"
1.911      apply (rule cong_scalar2_int)
1.912 @@ -858,42 +831,42 @@
1.913      apply (rule cong_scalar2_int)
1.914      apply (rule `[b2 = 1] (mod m2)`)
1.915      done
1.916 -  hence "[?x = u2] (mod m2)" by simp
1.917 +  then have "[?x = u2] (mod m2)" by simp
1.918    with `[?x = u1] (mod m1)` show ?thesis by blast
1.919  qed
1.920
1.921 -lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
1.922 +lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
1.923      [x = y] (mod m)"
1.924 -  apply (case_tac "y \<le> x")
1.925 +  apply (cases "y \<le> x")
1.927    apply (erule dvd_mult_left)
1.928    apply (rule cong_sym_nat)
1.929    apply (subst (asm) cong_sym_eq_nat)
1.930 -  apply (simp add: cong_altdef_nat)
1.931 +  apply (simp add: cong_altdef_nat)
1.932    apply (erule dvd_mult_left)
1.933 -done
1.934 +  done
1.935
1.936 -lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
1.937 +lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
1.938      [x = y] (mod m)"
1.939 -  apply (simp add: cong_altdef_int)
1.940 +  apply (simp add: cong_altdef_int)
1.941    apply (erule dvd_mult_left)
1.942 -done
1.943 +  done
1.944
1.945 -lemma cong_less_modulus_unique_nat:
1.946 +lemma cong_less_modulus_unique_nat:
1.947      "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
1.949
1.950  lemma binary_chinese_remainder_unique_nat:
1.951 -  assumes a: "coprime (m1::nat) m2" and
1.952 -         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
1.953 +  assumes a: "coprime (m1::nat) m2"
1.954 +    and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
1.955    shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
1.956  proof -
1.957 -  from binary_chinese_remainder_nat [OF a] obtain y where
1.958 +  from binary_chinese_remainder_nat [OF a] obtain y where
1.959        "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
1.960      by blast
1.961    let ?x = "y mod (m1 * m2)"
1.962    from nz have less: "?x < m1 * m2"
1.963 -    by auto
1.964 +    by auto
1.965    have one: "[?x = u1] (mod m1)"
1.966      apply (rule cong_trans_nat)
1.967      prefer 2
1.968 @@ -911,9 +884,8 @@
1.969      apply (rule cong_mod_nat)
1.970      using nz apply auto
1.971      done
1.972 -  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
1.973 -      z = ?x"
1.974 -  proof (clarify)
1.975 +  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
1.976 +  proof clarify
1.977      fix z
1.978      assume "z < m1 * m2"
1.979      assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
1.980 @@ -935,46 +907,43 @@
1.981        apply (intro cong_less_modulus_unique_nat)
1.982        apply (auto, erule cong_sym_nat)
1.983        done
1.984 -  qed
1.985 -  with less one two show ?thesis
1.986 -    by auto
1.987 +  qed
1.988 +  with less one two show ?thesis by auto
1.989   qed
1.990
1.991  lemma chinese_remainder_aux_nat:
1.992 -  fixes A :: "'a set" and
1.993 -        m :: "'a \<Rightarrow> nat"
1.994 -  assumes fin: "finite A" and
1.995 -          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.996 -  shows "EX b. (ALL i : A.
1.997 -      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
1.998 +  fixes A :: "'a set"
1.999 +    and m :: "'a \<Rightarrow> nat"
1.1000 +  assumes fin: "finite A"
1.1001 +    and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1002 +  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
1.1003  proof (rule finite_set_choice, rule fin, rule ballI)
1.1004    fix i
1.1005    assume "i : A"
1.1006    with cop have "coprime (PROD j : A - {i}. m j) (m i)"
1.1007      by (intro setprod_coprime_nat, auto)
1.1008 -  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
1.1009 +  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
1.1010      by (elim cong_solve_coprime_nat)
1.1011    then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
1.1012      by auto
1.1013 -  moreover have "[(PROD j : A - {i}. m j) * x = 0]
1.1014 +  moreover have "[(PROD j : A - {i}. m j) * x = 0]
1.1015      (mod (PROD j : A - {i}. m j))"
1.1016      by (subst mult_commute, rule cong_mult_self_nat)
1.1017 -  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
1.1018 +  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
1.1019        (mod setprod m (A - {i}))"
1.1020      by blast
1.1021  qed
1.1022
1.1023  lemma chinese_remainder_nat:
1.1024 -  fixes A :: "'a set" and
1.1025 -        m :: "'a \<Rightarrow> nat" and
1.1026 -        u :: "'a \<Rightarrow> nat"
1.1027 -  assumes
1.1028 -        fin: "finite A" and
1.1029 -        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1030 +  fixes A :: "'a set"
1.1031 +    and m :: "'a \<Rightarrow> nat"
1.1032 +    and u :: "'a \<Rightarrow> nat"
1.1033 +  assumes fin: "finite A"
1.1034 +    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1035    shows "EX x. (ALL i:A. [x = u i] (mod m i))"
1.1036  proof -
1.1037    from chinese_remainder_aux_nat [OF fin cop] obtain b where
1.1038 -    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
1.1039 +    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
1.1040        [b i = 0] (mod (PROD j : A - {i}. m j))"
1.1041      by blast
1.1042    let ?x = "SUM i:A. (u i) * (b i)"
1.1043 @@ -982,12 +951,12 @@
1.1044    proof (rule exI, clarify)
1.1045      fix i
1.1046      assume a: "i : A"
1.1047 -    show "[?x = u i] (mod m i)"
1.1048 +    show "[?x = u i] (mod m i)"
1.1049      proof -
1.1050 -      from fin a have "?x = (SUM j:{i}. u j * b j) +
1.1051 +      from fin a have "?x = (SUM j:{i}. u j * b j) +
1.1052            (SUM j:A-{i}. u j * b j)"
1.1053          by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
1.1054 -      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
1.1055 +      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
1.1056          by auto
1.1057        also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
1.1058                    u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
1.1059 @@ -1010,35 +979,34 @@
1.1060    qed
1.1061  qed
1.1062
1.1063 -lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
1.1064 +lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
1.1065      (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
1.1066        (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
1.1067 -         [x = y] (mod (PROD i:A. m i))"
1.1068 +         [x = y] (mod (PROD i:A. m i))"
1.1069    apply (induct set: finite)
1.1070    apply auto
1.1071    apply (erule (1) coprime_cong_mult_nat)
1.1072    apply (subst gcd_commute_nat)
1.1073    apply (rule setprod_coprime_nat)
1.1074    apply auto
1.1075 -done
1.1076 +  done
1.1077
1.1078  lemma chinese_remainder_unique_nat:
1.1079 -  fixes A :: "'a set" and
1.1080 -        m :: "'a \<Rightarrow> nat" and
1.1081 -        u :: "'a \<Rightarrow> nat"
1.1082 -  assumes
1.1083 -        fin: "finite A" and
1.1084 -         nz: "ALL i:A. m i \<noteq> 0" and
1.1085 -        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1086 +  fixes A :: "'a set"
1.1087 +    and m :: "'a \<Rightarrow> nat"
1.1088 +    and u :: "'a \<Rightarrow> nat"
1.1089 +  assumes fin: "finite A"
1.1090 +    and nz: "ALL i:A. m i \<noteq> 0"
1.1091 +    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.1092    shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
1.1093  proof -
1.1094 -  from chinese_remainder_nat [OF fin cop] obtain y where
1.1095 -      one: "(ALL i:A. [y = u i] (mod m i))"
1.1096 +  from chinese_remainder_nat [OF fin cop]
1.1097 +  obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
1.1098      by blast
1.1099    let ?x = "y mod (PROD i:A. m i)"
1.1100    from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
1.1101      by auto
1.1102 -  hence less: "?x < (PROD i:A. m i)"
1.1103 +  then have less: "?x < (PROD i:A. m i)"
1.1104      by auto
1.1105    have cong: "ALL i:A. [?x = u i] (mod m i)"
1.1106      apply auto
1.1107 @@ -1052,28 +1020,29 @@
1.1108      apply (rule fin)
1.1109      apply assumption
1.1110      done
1.1111 -  have unique: "ALL z. z < (PROD i:A. m i) \<and>
1.1112 +  have unique: "ALL z. z < (PROD i:A. m i) \<and>
1.1113        (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
1.1114    proof (clarify)
1.1115      fix z
1.1116      assume zless: "z < (PROD i:A. m i)"
1.1117      assume zcong: "(ALL i:A. [z = u i] (mod m i))"
1.1118      have "ALL i:A. [?x = z] (mod m i)"
1.1119 -      apply clarify
1.1120 +      apply clarify
1.1121        apply (rule cong_trans_nat)
1.1122        using cong apply (erule bspec)
1.1123        apply (rule cong_sym_nat)
1.1124        using zcong apply auto
1.1125        done
1.1126      with fin cop have "[?x = z] (mod (PROD i:A. m i))"
1.1127 -      by (intro coprime_cong_prod_nat, auto)
1.1128 +      apply (intro coprime_cong_prod_nat)
1.1129 +      apply auto
1.1130 +      done
1.1131      with zless less show "z = ?x"
1.1132        apply (intro cong_less_modulus_unique_nat)
1.1133        apply (auto, erule cong_sym_nat)
1.1134        done
1.1135 -  qed
1.1136 -  from less cong unique show ?thesis
1.1137 -    by blast
1.1138 +  qed
1.1139 +  from less cong unique show ?thesis by blast
1.1140  qed
1.1141
1.1142  end
```