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