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