src/HOL/Number_Theory/Cong.thy
author haftmann
Thu Jul 02 10:06:47 2015 +0200 (2015-07-02)
changeset 60634 e3b6e516608b
parent 60526 fad653acf58f
child 60688 01488b559910
permissions -rw-r--r--
separate (semi)ring with normalization
     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 @{text One_nat_def}\<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     "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
   182       [(SUM x:A. f x) = (SUM x: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     "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
   190       [(SUM x:A. f x) = (SUM x: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     "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
   198       [(PROD x:A. f x) = (PROD x: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     "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
   206       [(PROD x:A. f x) = (PROD x: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_int gcd_int.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_int 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 assms 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: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
   531   apply (auto intro: cong_solve_coprime_nat simp: One_nat_def)
   532   apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
   533   apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
   534       gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
   535   done
   536 
   537 lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
   538   apply (auto intro: cong_solve_coprime_int)
   539   apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int)
   540   done
   541 
   542 lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
   543     (EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))"
   544   apply (subst coprime_iff_invertible_nat)
   545   apply auto
   546   apply (auto simp add: cong_nat_def)
   547   apply (metis mod_less_divisor mod_mult_right_eq)
   548   done
   549 
   550 lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
   551     (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
   552   apply (subst coprime_iff_invertible_int)
   553   apply (auto simp add: cong_int_def)
   554   apply (metis mod_mult_right_eq pos_mod_conj)
   555   done
   556 
   557 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
   558     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   559   apply (cases "y \<le> x")
   560   apply (metis cong_altdef_nat lcm_least_nat)
   561   apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
   562   done
   563 
   564 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
   565     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   566   by (auto simp add: cong_altdef_int lcm_least_int) [1]
   567 
   568 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
   569     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   570     (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   571       [x = y] (mod (PROD i:A. m i))"
   572   apply (induct set: finite)
   573   apply auto
   574   apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
   575   done
   576 
   577 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
   578     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   579     (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
   580       [x = y] (mod (PROD i:A. m i))"
   581   apply (induct set: finite)
   582   apply auto
   583   apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
   584   done
   585 
   586 lemma binary_chinese_remainder_aux_nat:
   587   assumes a: "coprime (m1::nat) m2"
   588   shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   589     [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   590 proof -
   591   from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   592     by auto
   593   from a have b: "coprime m2 m1"
   594     by (subst gcd_commute_nat)
   595   from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   596     by auto
   597   have "[m1 * x1 = 0] (mod m1)"
   598     by (subst mult.commute, rule cong_mult_self_nat)
   599   moreover have "[m2 * x2 = 0] (mod m2)"
   600     by (subst mult.commute, rule cong_mult_self_nat)
   601   moreover note one two
   602   ultimately show ?thesis by blast
   603 qed
   604 
   605 lemma binary_chinese_remainder_aux_int:
   606   assumes a: "coprime (m1::int) m2"
   607   shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   608     [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   609 proof -
   610   from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   611     by auto
   612   from a have b: "coprime m2 m1"
   613     by (subst gcd_commute_int)
   614   from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   615     by auto
   616   have "[m1 * x1 = 0] (mod m1)"
   617     by (subst mult.commute, rule cong_mult_self_int)
   618   moreover have "[m2 * x2 = 0] (mod m2)"
   619     by (subst mult.commute, rule cong_mult_self_int)
   620   moreover note one two
   621   ultimately show ?thesis by blast
   622 qed
   623 
   624 lemma binary_chinese_remainder_nat:
   625   assumes a: "coprime (m1::nat) m2"
   626   shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   627 proof -
   628   from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
   629       where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   630             "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   631     by blast
   632   let ?x = "u1 * b1 + u2 * b2"
   633   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   634     apply (rule cong_add_nat)
   635     apply (rule cong_scalar2_nat)
   636     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
   637     apply (rule cong_scalar2_nat)
   638     apply (rule \<open>[b2 = 0] (mod m1)\<close>)
   639     done
   640   then have "[?x = u1] (mod m1)" by simp
   641   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   642     apply (rule cong_add_nat)
   643     apply (rule cong_scalar2_nat)
   644     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
   645     apply (rule cong_scalar2_nat)
   646     apply (rule \<open>[b2 = 1] (mod m2)\<close>)
   647     done
   648   then have "[?x = u2] (mod m2)" by simp
   649   with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
   650 qed
   651 
   652 lemma binary_chinese_remainder_int:
   653   assumes a: "coprime (m1::int) m2"
   654   shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   655 proof -
   656   from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
   657     where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   658           "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   659     by blast
   660   let ?x = "u1 * b1 + u2 * b2"
   661   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   662     apply (rule cong_add_int)
   663     apply (rule cong_scalar2_int)
   664     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
   665     apply (rule cong_scalar2_int)
   666     apply (rule \<open>[b2 = 0] (mod m1)\<close>)
   667     done
   668   then have "[?x = u1] (mod m1)" by simp
   669   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   670     apply (rule cong_add_int)
   671     apply (rule cong_scalar2_int)
   672     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
   673     apply (rule cong_scalar2_int)
   674     apply (rule \<open>[b2 = 1] (mod m2)\<close>)
   675     done
   676   then have "[?x = u2] (mod m2)" by simp
   677   with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
   678 qed
   679 
   680 lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
   681     [x = y] (mod m)"
   682   apply (cases "y \<le> x")
   683   apply (simp add: cong_altdef_nat)
   684   apply (erule dvd_mult_left)
   685   apply (rule cong_sym_nat)
   686   apply (subst (asm) cong_sym_eq_nat)
   687   apply (simp add: cong_altdef_nat)
   688   apply (erule dvd_mult_left)
   689   done
   690 
   691 lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
   692     [x = y] (mod m)"
   693   apply (simp add: cong_altdef_int)
   694   apply (erule dvd_mult_left)
   695   done
   696 
   697 lemma cong_less_modulus_unique_nat:
   698     "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   699   by (simp add: cong_nat_def)
   700 
   701 lemma binary_chinese_remainder_unique_nat:
   702   assumes a: "coprime (m1::nat) m2"
   703     and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   704   shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   705 proof -
   706   from binary_chinese_remainder_nat [OF a] obtain y where
   707       "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
   708     by blast
   709   let ?x = "y mod (m1 * m2)"
   710   from nz have less: "?x < m1 * m2"
   711     by auto
   712   have one: "[?x = u1] (mod m1)"
   713     apply (rule cong_trans_nat)
   714     prefer 2
   715     apply (rule \<open>[y = u1] (mod m1)\<close>)
   716     apply (rule cong_modulus_mult_nat)
   717     apply (rule cong_mod_nat)
   718     using nz apply auto
   719     done
   720   have two: "[?x = u2] (mod m2)"
   721     apply (rule cong_trans_nat)
   722     prefer 2
   723     apply (rule \<open>[y = u2] (mod m2)\<close>)
   724     apply (subst mult.commute)
   725     apply (rule cong_modulus_mult_nat)
   726     apply (rule cong_mod_nat)
   727     using nz apply auto
   728     done
   729   have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
   730   proof clarify
   731     fix z
   732     assume "z < m1 * m2"
   733     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
   734     have "[?x = z] (mod m1)"
   735       apply (rule cong_trans_nat)
   736       apply (rule \<open>[?x = u1] (mod m1)\<close>)
   737       apply (rule cong_sym_nat)
   738       apply (rule \<open>[z = u1] (mod m1)\<close>)
   739       done
   740     moreover have "[?x = z] (mod m2)"
   741       apply (rule cong_trans_nat)
   742       apply (rule \<open>[?x = u2] (mod m2)\<close>)
   743       apply (rule cong_sym_nat)
   744       apply (rule \<open>[z = u2] (mod m2)\<close>)
   745       done
   746     ultimately have "[?x = z] (mod m1 * m2)"
   747       by (auto intro: coprime_cong_mult_nat a)
   748     with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
   749       apply (intro cong_less_modulus_unique_nat)
   750       apply (auto, erule cong_sym_nat)
   751       done
   752   qed
   753   with less one two show ?thesis by auto
   754  qed
   755 
   756 lemma chinese_remainder_aux_nat:
   757   fixes A :: "'a set"
   758     and m :: "'a \<Rightarrow> nat"
   759   assumes fin: "finite A"
   760     and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   761   shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
   762 proof (rule finite_set_choice, rule fin, rule ballI)
   763   fix i
   764   assume "i : A"
   765   with cop have "coprime (PROD j : A - {i}. m j) (m i)"
   766     by (intro setprod_coprime_nat, auto)
   767   then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   768     by (elim cong_solve_coprime_nat)
   769   then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   770     by auto
   771   moreover have "[(PROD j : A - {i}. m j) * x = 0]
   772     (mod (PROD j : A - {i}. m j))"
   773     by (subst mult.commute, rule cong_mult_self_nat)
   774   ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
   775       (mod setprod m (A - {i}))"
   776     by blast
   777 qed
   778 
   779 lemma chinese_remainder_nat:
   780   fixes A :: "'a set"
   781     and m :: "'a \<Rightarrow> nat"
   782     and u :: "'a \<Rightarrow> nat"
   783   assumes fin: "finite A"
   784     and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   785   shows "EX x. (ALL i:A. [x = u i] (mod m i))"
   786 proof -
   787   from chinese_remainder_aux_nat [OF fin cop] obtain b where
   788     bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
   789       [b i = 0] (mod (PROD j : A - {i}. m j))"
   790     by blast
   791   let ?x = "SUM i:A. (u i) * (b i)"
   792   show "?thesis"
   793   proof (rule exI, clarify)
   794     fix i
   795     assume a: "i : A"
   796     show "[?x = u i] (mod m i)"
   797     proof -
   798       from fin a have "?x = (SUM j:{i}. u j * b j) +
   799           (SUM j:A-{i}. u j * b j)"
   800         by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong)
   801       then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
   802         by auto
   803       also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
   804                   u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
   805         apply (rule cong_add_nat)
   806         apply (rule cong_scalar2_nat)
   807         using bprop a apply blast
   808         apply (rule cong_setsum_nat)
   809         apply (rule cong_scalar2_nat)
   810         using bprop apply auto
   811         apply (rule cong_dvd_modulus_nat)
   812         apply (drule (1) bspec)
   813         apply (erule conjE)
   814         apply assumption
   815         apply rule
   816         using fin a apply auto
   817         done
   818       finally show ?thesis
   819         by simp
   820     qed
   821   qed
   822 qed
   823 
   824 lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
   825     (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   826       (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   827          [x = y] (mod (PROD i:A. m i))"
   828   apply (induct set: finite)
   829   apply auto
   830   apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
   831   done
   832 
   833 lemma chinese_remainder_unique_nat:
   834   fixes A :: "'a set"
   835     and m :: "'a \<Rightarrow> nat"
   836     and u :: "'a \<Rightarrow> nat"
   837   assumes fin: "finite A"
   838     and nz: "ALL i:A. m i \<noteq> 0"
   839     and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   840   shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
   841 proof -
   842   from chinese_remainder_nat [OF fin cop]
   843   obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
   844     by blast
   845   let ?x = "y mod (PROD i:A. m i)"
   846   from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
   847     by auto
   848   then have less: "?x < (PROD i:A. m i)"
   849     by auto
   850   have cong: "ALL i:A. [?x = u i] (mod m i)"
   851     apply auto
   852     apply (rule cong_trans_nat)
   853     prefer 2
   854     using one apply auto
   855     apply (rule cong_dvd_modulus_nat)
   856     apply (rule cong_mod_nat)
   857     using prodnz apply auto
   858     apply rule
   859     apply (rule fin)
   860     apply assumption
   861     done
   862   have unique: "ALL z. z < (PROD i:A. m i) \<and>
   863       (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
   864   proof (clarify)
   865     fix z
   866     assume zless: "z < (PROD i:A. m i)"
   867     assume zcong: "(ALL i:A. [z = u i] (mod m i))"
   868     have "ALL i:A. [?x = z] (mod m i)"
   869       apply clarify
   870       apply (rule cong_trans_nat)
   871       using cong apply (erule bspec)
   872       apply (rule cong_sym_nat)
   873       using zcong apply auto
   874       done
   875     with fin cop have "[?x = z] (mod (PROD i:A. m i))"
   876       apply (intro coprime_cong_prod_nat)
   877       apply auto
   878       done
   879     with zless less show "z = ?x"
   880       apply (intro cong_less_modulus_unique_nat)
   881       apply (auto, erule cong_sym_nat)
   882       done
   883   qed
   884   from less cong unique show ?thesis by blast
   885 qed
   886 
   887 end