src/HOL/Number_Theory/Cong.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 41959 b460124855b8
child 44872 a98ef45122f3
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     1 (*  Title:      HOL/Number_Theory/Cong.thy
     2     Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     3                 Thomas M. Rasmussen, Jeremy Avigad
     4 
     5 Defines congruence (notation: [x = y] (mod z)) for natural numbers and
     6 integers.
     7 
     8 This file combines and revises a number of prior developments.
     9 
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    11 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    12 gcd, lcm, and prime for the natural numbers.
    13 
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    16 another extension of the notions to the integers, and added a number
    17 of results to "Primes" and "GCD". 
    18 
    19 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
    20 developed the congruence relations on the integers. The notion was
    21 extended to the natural numbers by Chaieb. Jeremy Avigad combined
    22 these, revised and tidied them, made the development uniform for the
    23 natural numbers and the integers, and added a number of new theorems.
    24 *)
    25 
    26 header {* Congruence *}
    27 
    28 theory Cong
    29 imports Primes
    30 begin
    31 
    32 subsection {* Turn off One_nat_def *}
    33 
    34 lemma induct'_nat [case_names zero plus1, induct type: nat]: 
    35     "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
    36 by (erule nat_induct) (simp add:One_nat_def)
    37 
    38 lemma cases_nat [case_names zero plus1, cases type: nat]: 
    39     "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
    40 by(metis induct'_nat)
    41 
    42 lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
    43 by (simp add: One_nat_def)
    44 
    45 lemma power_eq_one_eq_nat [simp]: 
    46   "((x::nat)^m = 1) = (m = 0 | x = 1)"
    47 by (induct m, auto)
    48 
    49 lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
    50   card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
    51 by (auto simp add: insert_absorb)
    52 
    53 lemma nat_1' [simp]: "nat 1 = 1"
    54 by simp
    55 
    56 (* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
    57 
    58 declare nat_1 [simp del]
    59 declare add_2_eq_Suc [simp del] 
    60 declare add_2_eq_Suc' [simp del]
    61 
    62 
    63 declare mod_pos_pos_trivial [simp]
    64 
    65 
    66 subsection {* Main definitions *}
    67 
    68 class cong =
    69 
    70 fixes 
    71   cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
    72 
    73 begin
    74 
    75 abbreviation
    76   notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
    77 where
    78   "notcong x y m == (~cong x y m)" 
    79 
    80 end
    81 
    82 (* definitions for the natural numbers *)
    83 
    84 instantiation nat :: cong
    85 
    86 begin 
    87 
    88 definition 
    89   cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    90 where 
    91   "cong_nat x y m = ((x mod m) = (y mod m))"
    92 
    93 instance proof qed
    94 
    95 end
    96 
    97 
    98 (* definitions for the integers *)
    99 
   100 instantiation int :: cong
   101 
   102 begin 
   103 
   104 definition 
   105   cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
   106 where 
   107   "cong_int x y m = ((x mod m) = (y mod m))"
   108 
   109 instance proof qed
   110 
   111 end
   112 
   113 
   114 subsection {* Set up Transfer *}
   115 
   116 
   117 lemma transfer_nat_int_cong:
   118   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
   119     ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
   120   unfolding cong_int_def cong_nat_def 
   121   apply (auto simp add: nat_mod_distrib [symmetric])
   122   apply (subst (asm) eq_nat_nat_iff)
   123   apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
   124   apply assumption
   125 done
   126 
   127 declare transfer_morphism_nat_int[transfer add return: 
   128     transfer_nat_int_cong]
   129 
   130 lemma transfer_int_nat_cong:
   131   "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
   132   apply (auto simp add: cong_int_def cong_nat_def)
   133   apply (auto simp add: zmod_int [symmetric])
   134 done
   135 
   136 declare transfer_morphism_int_nat[transfer add return: 
   137     transfer_int_nat_cong]
   138 
   139 
   140 subsection {* Congruence *}
   141 
   142 (* was zcong_0, etc. *)
   143 lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
   144   by (unfold cong_nat_def, auto)
   145 
   146 lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
   147   by (unfold cong_int_def, auto)
   148 
   149 lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
   150   by (unfold cong_nat_def, auto)
   151 
   152 lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
   153   by (unfold cong_nat_def, auto simp add: One_nat_def)
   154 
   155 lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
   156   by (unfold cong_int_def, auto)
   157 
   158 lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
   159   by (unfold cong_nat_def, auto)
   160 
   161 lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
   162   by (unfold cong_int_def, auto)
   163 
   164 lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   165   by (unfold cong_nat_def, auto)
   166 
   167 lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   168   by (unfold cong_int_def, auto)
   169 
   170 lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
   171   by (unfold cong_nat_def, auto)
   172 
   173 lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
   174   by (unfold cong_int_def, auto)
   175 
   176 lemma cong_trans_nat [trans]:
   177     "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   178   by (unfold cong_nat_def, auto)
   179 
   180 lemma cong_trans_int [trans]:
   181     "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   182   by (unfold cong_int_def, auto)
   183 
   184 lemma cong_add_nat:
   185     "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   186   apply (unfold cong_nat_def)
   187   apply (subst (1 2) mod_add_eq)
   188   apply simp
   189 done
   190 
   191 lemma cong_add_int:
   192     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   193   apply (unfold cong_int_def)
   194   apply (subst (1 2) mod_add_left_eq)
   195   apply (subst (1 2) mod_add_right_eq)
   196   apply simp
   197 done
   198 
   199 lemma cong_diff_int:
   200     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
   201   apply (unfold cong_int_def)
   202   apply (subst (1 2) mod_diff_eq)
   203   apply simp
   204 done
   205 
   206 lemma cong_diff_aux_int:
   207   "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
   208       [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
   209   apply (subst (1 2) tsub_eq)
   210   apply (auto intro: cong_diff_int)
   211 done;
   212 
   213 lemma cong_diff_nat:
   214   assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
   215     "[c = d] (mod m)"
   216   shows "[a - c = b - d] (mod m)"
   217   using assms by (rule cong_diff_aux_int [transferred]);
   218 
   219 lemma cong_mult_nat:
   220     "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   221   apply (unfold cong_nat_def)
   222   apply (subst (1 2) mod_mult_eq)
   223   apply simp
   224 done
   225 
   226 lemma cong_mult_int:
   227     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   228   apply (unfold cong_int_def)
   229   apply (subst (1 2) zmod_zmult1_eq)
   230   apply (subst (1 2) mult_commute)
   231   apply (subst (1 2) zmod_zmult1_eq)
   232   apply simp
   233 done
   234 
   235 lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   236   apply (induct k)
   237   apply (auto simp add: cong_mult_nat)
   238   done
   239 
   240 lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   241   apply (induct k)
   242   apply (auto simp add: cong_mult_int)
   243   done
   244 
   245 lemma cong_setsum_nat [rule_format]: 
   246     "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
   247       [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
   248   apply (case_tac "finite A")
   249   apply (induct set: finite)
   250   apply (auto intro: cong_add_nat)
   251 done
   252 
   253 lemma cong_setsum_int [rule_format]:
   254     "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
   255       [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
   256   apply (case_tac "finite A")
   257   apply (induct set: finite)
   258   apply (auto intro: cong_add_int)
   259 done
   260 
   261 lemma cong_setprod_nat [rule_format]: 
   262     "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
   263       [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
   264   apply (case_tac "finite A")
   265   apply (induct set: finite)
   266   apply (auto intro: cong_mult_nat)
   267 done
   268 
   269 lemma cong_setprod_int [rule_format]: 
   270     "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
   271       [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
   272   apply (case_tac "finite A")
   273   apply (induct set: finite)
   274   apply (auto intro: cong_mult_int)
   275 done
   276 
   277 lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   278   by (rule cong_mult_nat, simp_all)
   279 
   280 lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   281   by (rule cong_mult_int, simp_all)
   282 
   283 lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   284   by (rule cong_mult_nat, simp_all)
   285 
   286 lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   287   by (rule cong_mult_int, simp_all)
   288 
   289 lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
   290   by (unfold cong_nat_def, auto)
   291 
   292 lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
   293   by (unfold cong_int_def, auto)
   294 
   295 lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
   296   apply (rule iffI)
   297   apply (erule cong_diff_int [of a b m b b, simplified])
   298   apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
   299 done
   300 
   301 lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
   302     [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
   303   by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
   304 
   305 lemma cong_eq_diff_cong_0_nat:
   306   assumes "(a::nat) >= b"
   307   shows "[a = b] (mod m) = [a - b = 0] (mod m)"
   308   using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
   309 
   310 lemma cong_diff_cong_0'_nat: 
   311   "[(x::nat) = y] (mod n) \<longleftrightarrow> 
   312     (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
   313   apply (case_tac "y <= x")
   314   apply (frule cong_eq_diff_cong_0_nat [where m = n])
   315   apply auto [1]
   316   apply (subgoal_tac "x <= y")
   317   apply (frule cong_eq_diff_cong_0_nat [where m = n])
   318   apply (subst cong_sym_eq_nat)
   319   apply auto
   320 done
   321 
   322 lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
   323   apply (subst cong_eq_diff_cong_0_nat, assumption)
   324   apply (unfold cong_nat_def)
   325   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   326 done
   327 
   328 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
   329   apply (subst cong_eq_diff_cong_0_int)
   330   apply (unfold cong_int_def)
   331   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   332 done
   333 
   334 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   335   by (simp add: cong_altdef_int)
   336 
   337 lemma cong_square_int:
   338    "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
   339     \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   340   apply (simp only: cong_altdef_int)
   341   apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
   342   (* any way around this? *)
   343   apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   344   apply (auto simp add: field_simps)
   345 done
   346 
   347 lemma cong_mult_rcancel_int:
   348   "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   349   apply (subst (1 2) cong_altdef_int)
   350   apply (subst left_diff_distrib [symmetric])
   351   apply (rule coprime_dvd_mult_iff_int)
   352   apply (subst gcd_commute_int, assumption)
   353 done
   354 
   355 lemma cong_mult_rcancel_nat:
   356   assumes  "coprime k (m::nat)"
   357   shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
   358   apply (rule cong_mult_rcancel_int [transferred])
   359   using assms apply auto
   360 done
   361 
   362 lemma cong_mult_lcancel_nat:
   363   "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
   364   by (simp add: mult_commute cong_mult_rcancel_nat)
   365 
   366 lemma cong_mult_lcancel_int:
   367   "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
   368   by (simp add: mult_commute cong_mult_rcancel_int)
   369 
   370 (* was zcong_zgcd_zmult_zmod *)
   371 lemma coprime_cong_mult_int:
   372   "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
   373     \<Longrightarrow> [a = b] (mod m * n)"
   374   apply (simp only: cong_altdef_int)
   375   apply (erule (2) divides_mult_int)
   376   done
   377 
   378 lemma coprime_cong_mult_nat:
   379   assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
   380   shows "[a = b] (mod m * n)"
   381   apply (rule coprime_cong_mult_int [transferred])
   382   using assms apply auto
   383   done
   384 
   385 lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
   386     a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   387   by (auto simp add: cong_nat_def)
   388 
   389 lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
   390     a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   391   by (auto simp add: cong_int_def)
   392 
   393 lemma cong_less_unique_nat:
   394     "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   395   apply auto
   396   apply (rule_tac x = "a mod m" in exI)
   397   apply (unfold cong_nat_def, auto)
   398 done
   399 
   400 lemma cong_less_unique_int:
   401     "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   402   apply auto
   403   apply (rule_tac x = "a mod m" in exI)
   404   apply (unfold cong_int_def, auto)
   405   done
   406 
   407 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   408   apply (auto simp add: cong_altdef_int dvd_def field_simps)
   409   apply (rule_tac [!] x = "-k" in exI, auto)
   410 done
   411 
   412 lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
   413     (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   414   apply (rule iffI)
   415   apply (case_tac "b <= a")
   416   apply (subst (asm) cong_altdef_nat, assumption)
   417   apply (unfold dvd_def, auto)
   418   apply (rule_tac x = k in exI)
   419   apply (rule_tac x = 0 in exI)
   420   apply (auto simp add: field_simps)
   421   apply (subst (asm) cong_sym_eq_nat)
   422   apply (subst (asm) cong_altdef_nat)
   423   apply force
   424   apply (unfold dvd_def, auto)
   425   apply (rule_tac x = 0 in exI)
   426   apply (rule_tac x = k in exI)
   427   apply (auto simp add: field_simps)
   428   apply (unfold cong_nat_def)
   429   apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
   430   apply (erule ssubst)back
   431   apply (erule subst)
   432   apply auto
   433 done
   434 
   435 lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   436   apply (subst (asm) cong_iff_lin_int, auto)
   437   apply (subst add_commute) 
   438   apply (subst (2) gcd_commute_int)
   439   apply (subst mult_commute)
   440   apply (subst gcd_add_mult_int)
   441   apply (rule gcd_commute_int)
   442   done
   443 
   444 lemma cong_gcd_eq_nat: 
   445   assumes "[(a::nat) = b] (mod m)"
   446   shows "gcd a m = gcd b m"
   447   apply (rule cong_gcd_eq_int [transferred])
   448   using assms apply auto
   449   done
   450 
   451 lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
   452     coprime b m"
   453   by (auto simp add: cong_gcd_eq_nat)
   454 
   455 lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
   456     coprime b m"
   457   by (auto simp add: cong_gcd_eq_int)
   458 
   459 lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = 
   460     [a mod m = b mod m] (mod m)"
   461   by (auto simp add: cong_nat_def)
   462 
   463 lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = 
   464     [a mod m = b mod m] (mod m)"
   465   by (auto simp add: cong_int_def)
   466 
   467 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
   468   by (subst (1 2) cong_altdef_int, auto)
   469 
   470 lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
   471   by auto
   472 
   473 lemma cong_zero_int: "[(a::int) = b] (mod 0) = (a = b)"
   474   by auto
   475 
   476 (*
   477 lemma mod_dvd_mod_int:
   478     "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
   479   apply (unfold dvd_def, auto)
   480   apply (rule mod_mod_cancel)
   481   apply auto
   482 done
   483 
   484 lemma mod_dvd_mod:
   485   assumes "0 < (m::nat)" and "m dvd b"
   486   shows "(a mod b mod m) = (a mod m)"
   487 
   488   apply (rule mod_dvd_mod_int [transferred])
   489   using assms apply auto
   490   done
   491 *)
   492 
   493 lemma cong_add_lcancel_nat: 
   494     "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
   495   by (simp add: cong_iff_lin_nat)
   496 
   497 lemma cong_add_lcancel_int: 
   498     "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
   499   by (simp add: cong_iff_lin_int)
   500 
   501 lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   502   by (simp add: cong_iff_lin_nat)
   503 
   504 lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   505   by (simp add: cong_iff_lin_int)
   506 
   507 lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   508   by (simp add: cong_iff_lin_nat)
   509 
   510 lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   511   by (simp add: cong_iff_lin_int)
   512 
   513 lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   514   by (simp add: cong_iff_lin_nat)
   515 
   516 lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   517   by (simp add: cong_iff_lin_int)
   518 
   519 lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   520     [x = y] (mod n)"
   521   apply (auto simp add: cong_iff_lin_nat dvd_def)
   522   apply (rule_tac x="k1 * k" in exI)
   523   apply (rule_tac x="k2 * k" in exI)
   524   apply (simp add: field_simps)
   525 done
   526 
   527 lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   528     [x = y] (mod n)"
   529   by (auto simp add: cong_altdef_int dvd_def)
   530 
   531 lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   532   by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
   533 
   534 lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   535   by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
   536 
   537 lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
   538   by (simp add: cong_nat_def)
   539 
   540 lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
   541   by (simp add: cong_int_def)
   542 
   543 lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
   544     \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   545   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   546 
   547 lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   548   apply (simp add: cong_altdef_int)
   549   apply (subst dvd_minus_iff [symmetric])
   550   apply (simp add: field_simps)
   551 done
   552 
   553 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   554   by (auto simp add: cong_altdef_int)
   555 
   556 lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
   557     \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   558   apply (case_tac "b > 0")
   559   apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   560   apply (subst (1 2) cong_modulus_neg_int)
   561   apply (unfold cong_int_def)
   562   apply (subgoal_tac "a * b = (-a * -b)")
   563   apply (erule ssubst)
   564   apply (subst zmod_zmult2_eq)
   565   apply (auto simp add: mod_add_left_eq) 
   566 done
   567 
   568 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
   569   apply (case_tac "a = 0")
   570   apply force
   571   apply (subst (asm) cong_altdef_nat)
   572   apply auto
   573 done
   574 
   575 lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
   576   by (unfold cong_nat_def, auto)
   577 
   578 lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
   579   by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
   580 
   581 lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
   582     a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
   583   apply (case_tac "n = 1")
   584   apply auto [1]
   585   apply (drule_tac x = "a - 1" in spec)
   586   apply force
   587   apply (case_tac "a = 0")
   588   apply (auto simp add: cong_0_1_nat) [1]
   589   apply (rule iffI)
   590   apply (drule cong_to_1_nat)
   591   apply (unfold dvd_def)
   592   apply auto [1]
   593   apply (rule_tac x = k in exI)
   594   apply (auto simp add: field_simps) [1]
   595   apply (subst cong_altdef_nat)
   596   apply (auto simp add: dvd_def)
   597 done
   598 
   599 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   600   apply (subst cong_altdef_nat)
   601   apply assumption
   602   apply (unfold dvd_def, auto simp add: field_simps)
   603   apply (rule_tac x = k in exI)
   604   apply auto
   605 done
   606 
   607 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   608   apply (case_tac "n = 0")
   609   apply force
   610   apply (frule bezout_nat [of a n], auto)
   611   apply (rule exI, erule ssubst)
   612   apply (rule cong_trans_nat)
   613   apply (rule cong_add_nat)
   614   apply (subst mult_commute)
   615   apply (rule cong_mult_self_nat)
   616   prefer 2
   617   apply simp
   618   apply (rule cong_refl_nat)
   619   apply (rule cong_refl_nat)
   620 done
   621 
   622 lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   623   apply (case_tac "n = 0")
   624   apply (case_tac "a \<ge> 0")
   625   apply auto
   626   apply (rule_tac x = "-1" in exI)
   627   apply auto
   628   apply (insert bezout_int [of a n], auto)
   629   apply (rule exI)
   630   apply (erule subst)
   631   apply (rule cong_trans_int)
   632   prefer 2
   633   apply (rule cong_add_int)
   634   apply (rule cong_refl_int)
   635   apply (rule cong_sym_int)
   636   apply (rule cong_mult_self_int)
   637   apply simp
   638   apply (subst mult_commute)
   639   apply (rule cong_refl_int)
   640 done
   641   
   642 lemma cong_solve_dvd_nat: 
   643   assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
   644   shows "EX x. [a * x = d] (mod n)"
   645 proof -
   646   from cong_solve_nat [OF a] obtain x where 
   647       "[a * x = gcd a n](mod n)"
   648     by auto
   649   hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
   650     by (elim cong_scalar2_nat)
   651   also from b have "(d div gcd a n) * gcd a n = d"
   652     by (rule dvd_div_mult_self)
   653   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   654     by auto
   655   finally show ?thesis
   656     by auto
   657 qed
   658 
   659 lemma cong_solve_dvd_int: 
   660   assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
   661   shows "EX x. [a * x = d] (mod n)"
   662 proof -
   663   from cong_solve_int [OF a] obtain x where 
   664       "[a * x = gcd a n](mod n)"
   665     by auto
   666   hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
   667     by (elim cong_scalar2_int)
   668   also from b have "(d div gcd a n) * gcd a n = d"
   669     by (rule dvd_div_mult_self)
   670   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   671     by auto
   672   finally show ?thesis
   673     by auto
   674 qed
   675 
   676 lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> 
   677     EX x. [a * x = 1] (mod n)"
   678   apply (case_tac "a = 0")
   679   apply force
   680   apply (frule cong_solve_nat [of a n])
   681   apply auto
   682 done
   683 
   684 lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> 
   685     EX x. [a * x = 1] (mod n)"
   686   apply (case_tac "a = 0")
   687   apply auto
   688   apply (case_tac "n \<ge> 0")
   689   apply auto
   690   apply (subst cong_int_def, auto)
   691   apply (frule cong_solve_int [of a n])
   692   apply auto
   693 done
   694 
   695 lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = 
   696     (EX x. [a * x = 1] (mod m))"
   697   apply (auto intro: cong_solve_coprime_nat)
   698   apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
   699 done
   700 
   701 lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = 
   702     (EX x. [a * x = 1] (mod m))"
   703   apply (auto intro: cong_solve_coprime_int)
   704   apply (unfold cong_int_def)
   705   apply (auto intro: invertible_coprime_int)
   706 done
   707 
   708 lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = 
   709     (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
   710   apply (subst coprime_iff_invertible_int)
   711   apply auto
   712   apply (auto simp add: cong_int_def)
   713   apply (rule_tac x = "x mod m" in exI)
   714   apply (auto simp add: mod_mult_right_eq [symmetric])
   715 done
   716 
   717 
   718 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
   719     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   720   apply (case_tac "y \<le> x")
   721   apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
   722   apply (rule cong_sym_nat)
   723   apply (subst (asm) (1 2) cong_sym_eq_nat)
   724   apply (auto simp add: cong_altdef_nat lcm_least_nat)
   725 done
   726 
   727 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
   728     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   729   by (auto simp add: cong_altdef_int lcm_least_int) [1]
   730 
   731 lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
   732     [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
   733   apply (frule (1) cong_cong_lcm_nat)back
   734   apply (simp add: lcm_nat_def)
   735 done
   736 
   737 lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
   738     [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
   739   apply (frule (1) cong_cong_lcm_int)back
   740   apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
   741 done
   742 
   743 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
   744     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   745     (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   746       [x = y] (mod (PROD i:A. m i))"
   747   apply (induct set: finite)
   748   apply auto
   749   apply (rule cong_cong_coprime_nat)
   750   apply (subst gcd_commute_nat)
   751   apply (rule setprod_coprime_nat)
   752   apply auto
   753 done
   754 
   755 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
   756     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   757     (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
   758       [x = y] (mod (PROD i:A. m i))"
   759   apply (induct set: finite)
   760   apply auto
   761   apply (rule cong_cong_coprime_int)
   762   apply (subst gcd_commute_int)
   763   apply (rule setprod_coprime_int)
   764   apply auto
   765 done
   766 
   767 lemma binary_chinese_remainder_aux_nat: 
   768   assumes a: "coprime (m1::nat) m2"
   769   shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   770     [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   771 proof -
   772   from cong_solve_coprime_nat [OF a]
   773       obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   774     by auto
   775   from a have b: "coprime m2 m1" 
   776     by (subst gcd_commute_nat)
   777   from cong_solve_coprime_nat [OF b]
   778       obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   779     by auto
   780   have "[m1 * x1 = 0] (mod m1)"
   781     by (subst mult_commute, rule cong_mult_self_nat)
   782   moreover have "[m2 * x2 = 0] (mod m2)"
   783     by (subst mult_commute, rule cong_mult_self_nat)
   784   moreover note one two
   785   ultimately show ?thesis by blast
   786 qed
   787 
   788 lemma binary_chinese_remainder_aux_int: 
   789   assumes a: "coprime (m1::int) m2"
   790   shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   791     [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   792 proof -
   793   from cong_solve_coprime_int [OF a]
   794       obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   795     by auto
   796   from a have b: "coprime m2 m1" 
   797     by (subst gcd_commute_int)
   798   from cong_solve_coprime_int [OF b]
   799       obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   800     by auto
   801   have "[m1 * x1 = 0] (mod m1)"
   802     by (subst mult_commute, rule cong_mult_self_int)
   803   moreover have "[m2 * x2 = 0] (mod m2)"
   804     by (subst mult_commute, rule cong_mult_self_int)
   805   moreover note one two
   806   ultimately show ?thesis by blast
   807 qed
   808 
   809 lemma binary_chinese_remainder_nat:
   810   assumes a: "coprime (m1::nat) m2"
   811   shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   812 proof -
   813   from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
   814     where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   815           "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   816     by blast
   817   let ?x = "u1 * b1 + u2 * b2"
   818   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   819     apply (rule cong_add_nat)
   820     apply (rule cong_scalar2_nat)
   821     apply (rule `[b1 = 1] (mod m1)`)
   822     apply (rule cong_scalar2_nat)
   823     apply (rule `[b2 = 0] (mod m1)`)
   824     done
   825   hence "[?x = u1] (mod m1)" by simp
   826   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   827     apply (rule cong_add_nat)
   828     apply (rule cong_scalar2_nat)
   829     apply (rule `[b1 = 0] (mod m2)`)
   830     apply (rule cong_scalar2_nat)
   831     apply (rule `[b2 = 1] (mod m2)`)
   832     done
   833   hence "[?x = u2] (mod m2)" by simp
   834   with `[?x = u1] (mod m1)` show ?thesis by blast
   835 qed
   836 
   837 lemma binary_chinese_remainder_int:
   838   assumes a: "coprime (m1::int) m2"
   839   shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   840 proof -
   841   from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
   842     where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   843           "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   844     by blast
   845   let ?x = "u1 * b1 + u2 * b2"
   846   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   847     apply (rule cong_add_int)
   848     apply (rule cong_scalar2_int)
   849     apply (rule `[b1 = 1] (mod m1)`)
   850     apply (rule cong_scalar2_int)
   851     apply (rule `[b2 = 0] (mod m1)`)
   852     done
   853   hence "[?x = u1] (mod m1)" by simp
   854   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   855     apply (rule cong_add_int)
   856     apply (rule cong_scalar2_int)
   857     apply (rule `[b1 = 0] (mod m2)`)
   858     apply (rule cong_scalar2_int)
   859     apply (rule `[b2 = 1] (mod m2)`)
   860     done
   861   hence "[?x = u2] (mod m2)" by simp
   862   with `[?x = u1] (mod m1)` show ?thesis by blast
   863 qed
   864 
   865 lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
   866     [x = y] (mod m)"
   867   apply (case_tac "y \<le> x")
   868   apply (simp add: cong_altdef_nat)
   869   apply (erule dvd_mult_left)
   870   apply (rule cong_sym_nat)
   871   apply (subst (asm) cong_sym_eq_nat)
   872   apply (simp add: cong_altdef_nat) 
   873   apply (erule dvd_mult_left)
   874 done
   875 
   876 lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
   877     [x = y] (mod m)"
   878   apply (simp add: cong_altdef_int) 
   879   apply (erule dvd_mult_left)
   880 done
   881 
   882 lemma cong_less_modulus_unique_nat: 
   883     "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   884   by (simp add: cong_nat_def)
   885 
   886 lemma binary_chinese_remainder_unique_nat:
   887   assumes a: "coprime (m1::nat) m2" and
   888          nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   889   shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   890 proof -
   891   from binary_chinese_remainder_nat [OF a] obtain y where 
   892       "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
   893     by blast
   894   let ?x = "y mod (m1 * m2)"
   895   from nz have less: "?x < m1 * m2"
   896     by auto   
   897   have one: "[?x = u1] (mod m1)"
   898     apply (rule cong_trans_nat)
   899     prefer 2
   900     apply (rule `[y = u1] (mod m1)`)
   901     apply (rule cong_modulus_mult_nat)
   902     apply (rule cong_mod_nat)
   903     using nz apply auto
   904     done
   905   have two: "[?x = u2] (mod m2)"
   906     apply (rule cong_trans_nat)
   907     prefer 2
   908     apply (rule `[y = u2] (mod m2)`)
   909     apply (subst mult_commute)
   910     apply (rule cong_modulus_mult_nat)
   911     apply (rule cong_mod_nat)
   912     using nz apply auto
   913     done
   914   have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
   915       z = ?x"
   916   proof (clarify)
   917     fix z
   918     assume "z < m1 * m2"
   919     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
   920     have "[?x = z] (mod m1)"
   921       apply (rule cong_trans_nat)
   922       apply (rule `[?x = u1] (mod m1)`)
   923       apply (rule cong_sym_nat)
   924       apply (rule `[z = u1] (mod m1)`)
   925       done
   926     moreover have "[?x = z] (mod m2)"
   927       apply (rule cong_trans_nat)
   928       apply (rule `[?x = u2] (mod m2)`)
   929       apply (rule cong_sym_nat)
   930       apply (rule `[z = u2] (mod m2)`)
   931       done
   932     ultimately have "[?x = z] (mod m1 * m2)"
   933       by (auto intro: coprime_cong_mult_nat a)
   934     with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
   935       apply (intro cong_less_modulus_unique_nat)
   936       apply (auto, erule cong_sym_nat)
   937       done
   938   qed  
   939   with less one two show ?thesis
   940     by auto
   941  qed
   942 
   943 lemma chinese_remainder_aux_nat:
   944   fixes A :: "'a set" and
   945         m :: "'a \<Rightarrow> nat"
   946   assumes fin: "finite A" and
   947           cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   948   shows "EX b. (ALL i : A. 
   949       [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
   950 proof (rule finite_set_choice, rule fin, rule ballI)
   951   fix i
   952   assume "i : A"
   953   with cop have "coprime (PROD j : A - {i}. m j) (m i)"
   954     by (intro setprod_coprime_nat, auto)
   955   hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   956     by (elim cong_solve_coprime_nat)
   957   then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   958     by auto
   959   moreover have "[(PROD j : A - {i}. m j) * x = 0] 
   960     (mod (PROD j : A - {i}. m j))"
   961     by (subst mult_commute, rule cong_mult_self_nat)
   962   ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
   963       (mod setprod m (A - {i}))"
   964     by blast
   965 qed
   966 
   967 lemma chinese_remainder_nat:
   968   fixes A :: "'a set" and
   969         m :: "'a \<Rightarrow> nat" and
   970         u :: "'a \<Rightarrow> nat"
   971   assumes 
   972         fin: "finite A" and
   973         cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   974   shows "EX x. (ALL i:A. [x = u i] (mod m i))"
   975 proof -
   976   from chinese_remainder_aux_nat [OF fin cop] obtain b where
   977     bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
   978       [b i = 0] (mod (PROD j : A - {i}. m j))"
   979     by blast
   980   let ?x = "SUM i:A. (u i) * (b i)"
   981   show "?thesis"
   982   proof (rule exI, clarify)
   983     fix i
   984     assume a: "i : A"
   985     show "[?x = u i] (mod m i)" 
   986     proof -
   987       from fin a have "?x = (SUM j:{i}. u j * b j) + 
   988           (SUM j:A-{i}. u j * b j)"
   989         by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
   990       hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
   991         by auto
   992       also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
   993                   u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
   994         apply (rule cong_add_nat)
   995         apply (rule cong_scalar2_nat)
   996         using bprop a apply blast
   997         apply (rule cong_setsum_nat)
   998         apply (rule cong_scalar2_nat)
   999         using bprop apply auto
  1000         apply (rule cong_dvd_modulus_nat)
  1001         apply (drule (1) bspec)
  1002         apply (erule conjE)
  1003         apply assumption
  1004         apply (rule dvd_setprod)
  1005         using fin a apply auto
  1006         done
  1007       finally show ?thesis
  1008         by simp
  1009     qed
  1010   qed
  1011 qed
  1012 
  1013 lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> 
  1014     (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
  1015       (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
  1016          [x = y] (mod (PROD i:A. m i))" 
  1017   apply (induct set: finite)
  1018   apply auto
  1019   apply (erule (1) coprime_cong_mult_nat)
  1020   apply (subst gcd_commute_nat)
  1021   apply (rule setprod_coprime_nat)
  1022   apply auto
  1023 done
  1024 
  1025 lemma chinese_remainder_unique_nat:
  1026   fixes A :: "'a set" and
  1027         m :: "'a \<Rightarrow> nat" and
  1028         u :: "'a \<Rightarrow> nat"
  1029   assumes 
  1030         fin: "finite A" and
  1031          nz: "ALL i:A. m i \<noteq> 0" and
  1032         cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
  1033   shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
  1034 proof -
  1035   from chinese_remainder_nat [OF fin cop] obtain y where
  1036       one: "(ALL i:A. [y = u i] (mod m i))" 
  1037     by blast
  1038   let ?x = "y mod (PROD i:A. m i)"
  1039   from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
  1040     by auto
  1041   hence less: "?x < (PROD i:A. m i)"
  1042     by auto
  1043   have cong: "ALL i:A. [?x = u i] (mod m i)"
  1044     apply auto
  1045     apply (rule cong_trans_nat)
  1046     prefer 2
  1047     using one apply auto
  1048     apply (rule cong_dvd_modulus_nat)
  1049     apply (rule cong_mod_nat)
  1050     using prodnz apply auto
  1051     apply (rule dvd_setprod)
  1052     apply (rule fin)
  1053     apply assumption
  1054     done
  1055   have unique: "ALL z. z < (PROD i:A. m i) \<and> 
  1056       (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
  1057   proof (clarify)
  1058     fix z
  1059     assume zless: "z < (PROD i:A. m i)"
  1060     assume zcong: "(ALL i:A. [z = u i] (mod m i))"
  1061     have "ALL i:A. [?x = z] (mod m i)"
  1062       apply clarify     
  1063       apply (rule cong_trans_nat)
  1064       using cong apply (erule bspec)
  1065       apply (rule cong_sym_nat)
  1066       using zcong apply auto
  1067       done
  1068     with fin cop have "[?x = z] (mod (PROD i:A. m i))"
  1069       by (intro coprime_cong_prod_nat, auto)
  1070     with zless less show "z = ?x"
  1071       apply (intro cong_less_modulus_unique_nat)
  1072       apply (auto, erule cong_sym_nat)
  1073       done
  1074   qed 
  1075   from less cong unique show ?thesis
  1076     by blast  
  1077 qed
  1078 
  1079 end