src/HOL/Number_Theory/Cong.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (19 months ago)
changeset 66817 0b12755ccbb2
parent 66453 cc19f7ca2ed6
child 66837 6ba663ff2b1c
permissions -rw-r--r--
euclidean rings need no normalization
     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   apply (auto simp add: cong_altdef_int dvd_def)
   322   apply (rule_tac [!] x = "-k" in exI, auto)
   323   done
   324 
   325 lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   326   (is "?lhs = ?rhs")
   327   for a b :: nat
   328 proof
   329   assume ?lhs
   330   show ?rhs
   331   proof (cases "b \<le> a")
   332     case True
   333     with \<open>?lhs\<close> show ?rhs
   334       by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute)
   335   next
   336     case False
   337     with \<open>?lhs\<close> show ?rhs
   338       apply (subst (asm) cong_sym_eq_nat)
   339       apply (auto simp: cong_altdef_nat)
   340       apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
   341       done
   342   qed
   343 next
   344   assume ?rhs
   345   then show ?lhs
   346     by (metis cong_nat_def mod_mult_self2 mult.commute)
   347 qed
   348 
   349 lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   350   for a b :: int
   351   by (metis cong_int_def gcd_red_int)
   352 
   353 lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   354   for a b :: nat
   355   by (metis cong_gcd_eq_int [transferred])
   356 
   357 lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   358   for a b :: nat
   359   by (auto simp add: cong_gcd_eq_nat)
   360 
   361 lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   362   for a b :: int
   363   by (auto simp add: cong_gcd_eq_int)
   364 
   365 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   366   for a b :: nat
   367   by (auto simp add: cong_nat_def)
   368 
   369 lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   370   for a b :: int
   371   by (auto simp add: cong_int_def)
   372 
   373 lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
   374   for a b :: int
   375   by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
   376 
   377 (*
   378 lemma mod_dvd_mod_int:
   379     "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
   380   apply (unfold dvd_def, auto)
   381   apply (rule mod_mod_cancel)
   382   apply auto
   383   done
   384 
   385 lemma mod_dvd_mod:
   386   assumes "0 < (m::nat)" and "m dvd b"
   387   shows "(a mod b mod m) = (a mod m)"
   388 
   389   apply (rule mod_dvd_mod_int [transferred])
   390   using assms apply auto
   391   done
   392 *)
   393 
   394 lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   395   for a x y :: nat
   396   by (simp add: cong_iff_lin_nat)
   397 
   398 lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   399   for a x y :: int
   400   by (simp add: cong_iff_lin_int)
   401 
   402 lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   403   for a x y :: nat
   404   by (simp add: cong_iff_lin_nat)
   405 
   406 lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   407   for a x y :: int
   408   by (simp add: cong_iff_lin_int)
   409 
   410 lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   411   for a x :: nat
   412   by (simp add: cong_iff_lin_nat)
   413 
   414 lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   415   for a x :: int
   416   by (simp add: cong_iff_lin_int)
   417 
   418 lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   419   for a x :: nat
   420   by (simp add: cong_iff_lin_nat)
   421 
   422 lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   423   for a x :: int
   424   by (simp add: cong_iff_lin_int)
   425 
   426 lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   427   for x y :: nat
   428   apply (auto simp add: cong_iff_lin_nat dvd_def)
   429   apply (rule_tac x= "k1 * k" in exI)
   430   apply (rule_tac x= "k2 * k" in exI)
   431   apply (simp add: field_simps)
   432   done
   433 
   434 lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   435   for x y :: int
   436   by (auto simp add: cong_altdef_int dvd_def)
   437 
   438 lemma cong_dvd_eq_nat: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   439   for x y :: nat
   440   by (auto simp: cong_nat_def dvd_eq_mod_eq_0)
   441 
   442 lemma cong_dvd_eq_int: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   443   for x y :: int
   444   by (auto simp: cong_int_def dvd_eq_mod_eq_0)
   445 
   446 lemma cong_mod_nat: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
   447   for a n :: nat
   448   by (simp add: cong_nat_def)
   449 
   450 lemma cong_mod_int: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
   451   for a n :: int
   452   by (simp add: cong_int_def)
   453 
   454 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)"
   455   for a b :: nat
   456   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   457 
   458 lemma neg_cong_int: "[a = b] (mod m) \<longleftrightarrow> [- a = - b] (mod m)"
   459   for a b :: int
   460   by (metis cong_int_def minus_minus mod_minus_cong)
   461 
   462 lemma cong_modulus_neg_int: "[a = b] (mod m) \<longleftrightarrow> [a = b] (mod - m)"
   463   for a b :: int
   464   by (auto simp add: cong_altdef_int)
   465 
   466 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)"
   467   for a b :: int
   468 proof (cases "b > 0")
   469   case True
   470   then show ?thesis
   471     by (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   472 next
   473   case False
   474   then show ?thesis
   475     apply (subst (1 2) cong_modulus_neg_int)
   476     apply (unfold cong_int_def)
   477     apply (subgoal_tac "a * b = (- a * - b)")
   478      apply (erule ssubst)
   479      apply (subst zmod_zmult2_eq)
   480       apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
   481      apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
   482     done
   483 qed
   484 
   485 lemma cong_to_1_nat:
   486   fixes a :: nat
   487   assumes "[a = 1] (mod n)"
   488   shows "n dvd (a - 1)"
   489 proof (cases "a = 0")
   490   case True
   491   then show ?thesis by force
   492 next
   493   case False
   494   with assms show ?thesis by (metis cong_altdef_nat leI less_one)
   495 qed
   496 
   497 lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0"
   498   by (auto simp: cong_nat_def)
   499 
   500 lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1"
   501   for n :: nat
   502   by (auto simp: cong_nat_def)
   503 
   504 lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1"
   505   for n :: int
   506   by (auto simp: cong_int_def zmult_eq_1_iff)
   507 
   508 lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
   509   for a :: nat
   510   by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat
   511       dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
   512 
   513 lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   514   for x y :: nat
   515   by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
   516 
   517 lemma cong_solve_nat:
   518   fixes a :: nat
   519   assumes "a \<noteq> 0"
   520   shows "\<exists>x. [a * x = gcd a n] (mod n)"
   521 proof (cases "n = 0")
   522   case True
   523   then show ?thesis by force
   524 next
   525   case False
   526   then show ?thesis
   527     using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>]
   528     by auto (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
   529 qed
   530 
   531 lemma cong_solve_int: "a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
   532   for a :: int
   533   apply (cases "n = 0")
   534    apply (cases "a \<ge> 0")
   535     apply auto
   536    apply (rule_tac x = "-1" in exI)
   537    apply auto
   538   apply (insert bezout_int [of a n], auto)
   539   apply (metis cong_iff_lin_int mult.commute)
   540   done
   541 
   542 lemma cong_solve_dvd_nat:
   543   fixes a :: nat
   544   assumes a: "a \<noteq> 0" and b: "gcd a n dvd d"
   545   shows "\<exists>x. [a * x = d] (mod n)"
   546 proof -
   547   from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
   548     by auto
   549   then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
   550     by (elim cong_scalar2_nat)
   551   also from b have "(d div gcd a n) * gcd a n = d"
   552     by (rule dvd_div_mult_self)
   553   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   554     by auto
   555   finally show ?thesis
   556     by auto
   557 qed
   558 
   559 lemma cong_solve_dvd_int:
   560   assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
   561   shows "\<exists>x. [a * x = d] (mod n)"
   562 proof -
   563   from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
   564     by auto
   565   then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
   566     by (elim cong_scalar2_int)
   567   also from b have "(d div gcd a n) * gcd a n = d"
   568     by (rule dvd_div_mult_self)
   569   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   570     by auto
   571   finally show ?thesis
   572     by auto
   573 qed
   574 
   575 lemma cong_solve_coprime_nat:
   576   fixes a :: nat
   577   assumes "coprime a n"
   578   shows "\<exists>x. [a * x = 1] (mod n)"
   579 proof (cases "a = 0")
   580   case True
   581   with assms show ?thesis by force
   582 next
   583   case False
   584   with assms show ?thesis by (metis cong_solve_nat)
   585 qed
   586 
   587 lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
   588   apply (cases "a = 0")
   589    apply auto
   590    apply (cases "n \<ge> 0")
   591     apply auto
   592   apply (metis cong_solve_int)
   593   done
   594 
   595 lemma coprime_iff_invertible_nat:
   596   "m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))"
   597   by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0)
   598 
   599 lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   600   for m :: int
   601   apply (auto intro: cong_solve_coprime_int)
   602   apply (metis cong_int_def coprime_mul_eq gcd_1_int gcd.commute gcd_red_int)
   603   done
   604 
   605 lemma coprime_iff_invertible'_nat:
   606   "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
   607   apply (subst coprime_iff_invertible_nat)
   608    apply auto
   609   apply (auto simp add: cong_nat_def)
   610   apply (metis mod_less_divisor mod_mult_right_eq)
   611   done
   612 
   613 lemma coprime_iff_invertible'_int:
   614   "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
   615   for m :: int
   616   apply (subst coprime_iff_invertible_int)
   617    apply (auto simp add: cong_int_def)
   618   apply (metis mod_mult_right_eq pos_mod_conj)
   619   done
   620 
   621 lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   622   for x y :: nat
   623   apply (cases "y \<le> x")
   624   apply (metis cong_altdef_nat lcm_least)
   625   apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear)
   626   done
   627 
   628 lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   629   for x y :: int
   630   by (auto simp add: cong_altdef_int lcm_least)
   631 
   632 lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
   633     (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   634     (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   635       [x = y] (mod (\<Prod>i\<in>A. m i))"
   636   apply (induct set: finite)
   637   apply auto
   638   apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   639   done
   640 
   641 lemma cong_cong_prod_coprime_int [rule_format]: "finite A \<Longrightarrow>
   642     (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   643     (\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
   644       [x = y] (mod (\<Prod>i\<in>A. m i))"
   645   apply (induct set: finite)
   646   apply auto
   647   apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
   648   done
   649 
   650 lemma binary_chinese_remainder_aux_nat:
   651   fixes m1 m2 :: nat
   652   assumes a: "coprime m1 m2"
   653   shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   654 proof -
   655   from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
   656     by auto
   657   from a have b: "coprime m2 m1"
   658     by (subst gcd.commute)
   659   from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
   660     by auto
   661   have "[m1 * x1 = 0] (mod m1)"
   662     by (subst mult.commute) (rule cong_mult_self_nat)
   663   moreover have "[m2 * x2 = 0] (mod m2)"
   664     by (subst mult.commute) (rule cong_mult_self_nat)
   665   ultimately show ?thesis
   666     using 1 2 by blast
   667 qed
   668 
   669 lemma binary_chinese_remainder_aux_int:
   670   fixes m1 m2 :: int
   671   assumes a: "coprime m1 m2"
   672   shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   673 proof -
   674   from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
   675     by auto
   676   from a have b: "coprime m2 m1"
   677     by (subst gcd.commute)
   678   from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
   679     by auto
   680   have "[m1 * x1 = 0] (mod m1)"
   681     by (subst mult.commute) (rule cong_mult_self_int)
   682   moreover have "[m2 * x2 = 0] (mod m2)"
   683     by (subst mult.commute) (rule cong_mult_self_int)
   684   ultimately show ?thesis
   685     using 1 2 by blast
   686 qed
   687 
   688 lemma binary_chinese_remainder_nat:
   689   fixes m1 m2 :: nat
   690   assumes a: "coprime m1 m2"
   691   shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   692 proof -
   693   from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
   694     where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
   695       and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   696     by blast
   697   let ?x = "u1 * b1 + u2 * b2"
   698   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   699     apply (rule cong_add_nat)
   700      apply (rule cong_scalar2_nat)
   701      apply (rule \<open>[b1 = 1] (mod m1)\<close>)
   702     apply (rule cong_scalar2_nat)
   703     apply (rule \<open>[b2 = 0] (mod m1)\<close>)
   704     done
   705   then have "[?x = u1] (mod m1)" by simp
   706   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   707     apply (rule cong_add_nat)
   708      apply (rule cong_scalar2_nat)
   709      apply (rule \<open>[b1 = 0] (mod m2)\<close>)
   710     apply (rule cong_scalar2_nat)
   711     apply (rule \<open>[b2 = 1] (mod m2)\<close>)
   712     done
   713   then have "[?x = u2] (mod m2)"
   714     by simp
   715   with \<open>[?x = u1] (mod m1)\<close> show ?thesis
   716     by blast
   717 qed
   718 
   719 lemma binary_chinese_remainder_int:
   720   fixes m1 m2 :: int
   721   assumes a: "coprime m1 m2"
   722   shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   723 proof -
   724   from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
   725     where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
   726       and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   727     by blast
   728   let ?x = "u1 * b1 + u2 * b2"
   729   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   730     apply (rule cong_add_int)
   731      apply (rule cong_scalar2_int)
   732      apply (rule \<open>[b1 = 1] (mod m1)\<close>)
   733     apply (rule cong_scalar2_int)
   734     apply (rule \<open>[b2 = 0] (mod m1)\<close>)
   735     done
   736   then have "[?x = u1] (mod m1)" by simp
   737   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   738     apply (rule cong_add_int)
   739      apply (rule cong_scalar2_int)
   740      apply (rule \<open>[b1 = 0] (mod m2)\<close>)
   741     apply (rule cong_scalar2_int)
   742     apply (rule \<open>[b2 = 1] (mod m2)\<close>)
   743     done
   744   then have "[?x = u2] (mod m2)" by simp
   745   with \<open>[?x = u1] (mod m1)\<close> show ?thesis
   746     by blast
   747 qed
   748 
   749 lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
   750   for x y :: nat
   751   apply (cases "y \<le> x")
   752    apply (simp add: cong_altdef_nat)
   753    apply (erule dvd_mult_left)
   754   apply (rule cong_sym_nat)
   755   apply (subst (asm) cong_sym_eq_nat)
   756   apply (simp add: cong_altdef_nat)
   757   apply (erule dvd_mult_left)
   758   done
   759 
   760 lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
   761   for x y :: int
   762   apply (simp add: cong_altdef_int)
   763   apply (erule dvd_mult_left)
   764   done
   765 
   766 lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   767   for x y :: nat
   768   by (simp add: cong_nat_def)
   769 
   770 lemma binary_chinese_remainder_unique_nat:
   771   fixes m1 m2 :: nat
   772   assumes a: "coprime m1 m2"
   773     and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   774   shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   775 proof -
   776   from binary_chinese_remainder_nat [OF a] obtain y
   777     where "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
   778     by blast
   779   let ?x = "y mod (m1 * m2)"
   780   from nz have less: "?x < m1 * m2"
   781     by auto
   782   have 1: "[?x = u1] (mod m1)"
   783     apply (rule cong_trans_nat)
   784      prefer 2
   785      apply (rule \<open>[y = u1] (mod m1)\<close>)
   786     apply (rule cong_modulus_mult_nat)
   787     apply (rule cong_mod_nat)
   788     using nz apply auto
   789     done
   790   have 2: "[?x = u2] (mod m2)"
   791     apply (rule cong_trans_nat)
   792      prefer 2
   793      apply (rule \<open>[y = u2] (mod m2)\<close>)
   794     apply (subst mult.commute)
   795     apply (rule cong_modulus_mult_nat)
   796     apply (rule cong_mod_nat)
   797     using nz apply auto
   798     done
   799   have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
   800   proof clarify
   801     fix z
   802     assume "z < m1 * m2"
   803     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
   804     have "[?x = z] (mod m1)"
   805       apply (rule cong_trans_nat)
   806        apply (rule \<open>[?x = u1] (mod m1)\<close>)
   807       apply (rule cong_sym_nat)
   808       apply (rule \<open>[z = u1] (mod m1)\<close>)
   809       done
   810     moreover have "[?x = z] (mod m2)"
   811       apply (rule cong_trans_nat)
   812        apply (rule \<open>[?x = u2] (mod m2)\<close>)
   813       apply (rule cong_sym_nat)
   814       apply (rule \<open>[z = u2] (mod m2)\<close>)
   815       done
   816     ultimately have "[?x = z] (mod m1 * m2)"
   817       by (auto intro: coprime_cong_mult_nat a)
   818     with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
   819       apply (intro cong_less_modulus_unique_nat)
   820         apply (auto, erule cong_sym_nat)
   821       done
   822   qed
   823   with less 1 2 show ?thesis by auto
   824  qed
   825 
   826 lemma chinese_remainder_aux_nat:
   827   fixes A :: "'a set"
   828     and m :: "'a \<Rightarrow> nat"
   829   assumes fin: "finite A"
   830     and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   831   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)))"
   832 proof (rule finite_set_choice, rule fin, rule ballI)
   833   fix i
   834   assume "i \<in> A"
   835   with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
   836     by (intro prod_coprime) auto
   837   then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
   838     by (elim cong_solve_coprime_nat)
   839   then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
   840     by auto
   841   moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   842     by (subst mult.commute, rule cong_mult_self_nat)
   843   ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
   844     by blast
   845 qed
   846 
   847 lemma chinese_remainder_nat:
   848   fixes A :: "'a set"
   849     and m :: "'a \<Rightarrow> nat"
   850     and u :: "'a \<Rightarrow> nat"
   851   assumes fin: "finite A"
   852     and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)"
   853   shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)"
   854 proof -
   855   from chinese_remainder_aux_nat [OF fin cop]
   856   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))"
   857     by blast
   858   let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
   859   show ?thesis
   860   proof (rule exI, clarify)
   861     fix i
   862     assume a: "i \<in> A"
   863     show "[?x = u i] (mod m i)"
   864     proof -
   865       from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) + (\<Sum>j \<in> A - {i}. u j * b j)"
   866         by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong)
   867       then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)"
   868         by auto
   869       also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
   870                   u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
   871         apply (rule cong_add_nat)
   872          apply (rule cong_scalar2_nat)
   873         using b a apply blast
   874         apply (rule cong_sum_nat)
   875         apply (rule cong_scalar2_nat)
   876         using b apply auto
   877         apply (rule cong_dvd_modulus_nat)
   878          apply (drule (1) bspec)
   879          apply (erule conjE)
   880          apply assumption
   881         apply rule
   882         using fin a apply auto
   883         done
   884       finally show ?thesis
   885         by simp
   886     qed
   887   qed
   888 qed
   889 
   890 lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
   891     (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   892       (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   893          [x = y] (mod (\<Prod>i\<in>A. m i))"
   894   apply (induct set: finite)
   895   apply auto
   896   apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   897   done
   898 
   899 lemma chinese_remainder_unique_nat:
   900   fixes A :: "'a set"
   901     and m :: "'a \<Rightarrow> nat"
   902     and u :: "'a \<Rightarrow> nat"
   903   assumes fin: "finite A"
   904     and nz: "\<forall>i\<in>A. m i \<noteq> 0"
   905     and cop: "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)"
   906   shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
   907 proof -
   908   from chinese_remainder_nat [OF fin cop]
   909   obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))"
   910     by blast
   911   let ?x = "y mod (\<Prod>i\<in>A. m i)"
   912   from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0"
   913     by auto
   914   then have less: "?x < (\<Prod>i\<in>A. m i)"
   915     by auto
   916   have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)"
   917     apply auto
   918     apply (rule cong_trans_nat)
   919      prefer 2
   920     using one apply auto
   921     apply (rule cong_dvd_modulus_nat)
   922      apply (rule cong_mod_nat)
   923     using prodnz apply auto
   924     apply rule
   925      apply (rule fin)
   926     apply assumption
   927     done
   928   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"
   929   proof clarify
   930     fix z
   931     assume zless: "z < (\<Prod>i\<in>A. m i)"
   932     assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))"
   933     have "\<forall>i\<in>A. [?x = z] (mod m i)"
   934       apply clarify
   935       apply (rule cong_trans_nat)
   936       using cong apply (erule bspec)
   937       apply (rule cong_sym_nat)
   938       using zcong apply auto
   939       done
   940     with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
   941       apply (intro coprime_cong_prod_nat)
   942         apply auto
   943       done
   944     with zless less show "z = ?x"
   945       apply (intro cong_less_modulus_unique_nat)
   946         apply auto
   947       apply (erule cong_sym_nat)
   948       done
   949   qed
   950   from less cong unique show ?thesis
   951     by blast
   952 qed
   953 
   954 end