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