src/HOL/NumberTheory/IntPrimes.thy
author wenzelm
Fri Oct 05 21:52:39 2001 +0200 (2001-10-05)
changeset 11701 3d51fbf81c17
parent 11049 7eef34adb852
child 11868 56db9f3a6b3e
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
     1 (*  Title:      HOL/NumberTheory/IntPrimes.thy
     2     ID:         $Id$
     3     Author:     Thomas M. Rasmussen
     4     Copyright   2000  University of Cambridge
     5 *)
     6 
     7 header {* Divisibility and prime numbers (on integers) *}
     8 
     9 theory IntPrimes = Primes:
    10 
    11 text {*
    12   The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
    13   congruences (all on the Integers).  Comparable to theory @{text
    14   Primes}, but @{text dvd} is included here as it is not present in
    15   main HOL.  Also includes extended GCD and congruences not present in
    16   @{text Primes}.
    17 *}
    18 
    19 
    20 subsection {* Definitions *}
    21 
    22 consts
    23   xzgcda :: "int * int * int * int * int * int * int * int => int * int * int"
    24   xzgcd :: "int => int => int * int * int"
    25   zprime :: "int set"
    26   zcong :: "int => int => int => bool"    ("(1[_ = _] '(mod _'))")
    27 
    28 recdef xzgcda
    29   "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
    30     :: int * int * int * int *int * int * int * int => nat)"
    31   "xzgcda (m, n, r', r, s', s, t', t) =
    32     (if r \<le> Numeral0 then (r', s', t')
    33      else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))"
    34   (hints simp: pos_mod_bound)
    35 
    36 constdefs
    37   zgcd :: "int * int => int"
    38   "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
    39 
    40 defs
    41   xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, Numeral1, Numeral0, Numeral0, Numeral1)"
    42   zprime_def: "zprime == {p. Numeral1 < p \<and> (\<forall>m. m dvd p --> m = Numeral1 \<or> m = p)}"
    43   zcong_def: "[a = b] (mod m) == m dvd (a - b)"
    44 
    45 
    46 lemma zabs_eq_iff:
    47     "(abs (z::int) = w) = (z = w \<and> Numeral0 <= z \<or> z = -w \<and> z < Numeral0)"
    48   apply (auto simp add: zabs_def)
    49   done
    50 
    51 
    52 text {* \medskip @{term gcd} lemmas *}
    53 
    54 lemma gcd_add1_eq: "gcd (m + k, k) = gcd (m + k, m)"
    55   apply (simp add: gcd_commute)
    56   done
    57 
    58 lemma gcd_diff2: "m \<le> n ==> gcd (n, n - m) = gcd (n, m)"
    59   apply (subgoal_tac "n = m + (n - m)")
    60    apply (erule ssubst, rule gcd_add1_eq)
    61   apply simp
    62   done
    63 
    64 
    65 subsection {* Divides relation *}
    66 
    67 lemma zdvd_0_right [iff]: "(m::int) dvd Numeral0"
    68   apply (unfold dvd_def)
    69   apply (blast intro: zmult_0_right [symmetric])
    70   done
    71 
    72 lemma zdvd_0_left [iff]: "(Numeral0 dvd (m::int)) = (m = Numeral0)"
    73   apply (unfold dvd_def)
    74   apply auto
    75   done
    76 
    77 lemma zdvd_1_left [iff]: "Numeral1 dvd (m::int)"
    78   apply (unfold dvd_def)
    79   apply simp
    80   done
    81 
    82 lemma zdvd_refl [simp]: "m dvd (m::int)"
    83   apply (unfold dvd_def)
    84   apply (blast intro: zmult_1_right [symmetric])
    85   done
    86 
    87 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
    88   apply (unfold dvd_def)
    89   apply (blast intro: zmult_assoc)
    90   done
    91 
    92 lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
    93   apply (unfold dvd_def)
    94   apply auto
    95    apply (rule_tac [!] x = "-k" in exI)
    96   apply auto
    97   done
    98 
    99 lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
   100   apply (unfold dvd_def)
   101   apply auto
   102    apply (rule_tac [!] x = "-k" in exI)
   103   apply auto
   104   done
   105 
   106 lemma zdvd_anti_sym:
   107     "Numeral0 < m ==> Numeral0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   108   apply (unfold dvd_def)
   109   apply auto
   110   apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
   111   done
   112 
   113 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
   114   apply (unfold dvd_def)
   115   apply (blast intro: zadd_zmult_distrib2 [symmetric])
   116   done
   117 
   118 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
   119   apply (unfold dvd_def)
   120   apply (blast intro: zdiff_zmult_distrib2 [symmetric])
   121   done
   122 
   123 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
   124   apply (subgoal_tac "m = n + (m - n)")
   125    apply (erule ssubst)
   126    apply (blast intro: zdvd_zadd)
   127   apply simp
   128   done
   129 
   130 lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   131   apply (unfold dvd_def)
   132   apply (blast intro: zmult_left_commute)
   133   done
   134 
   135 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
   136   apply (subst zmult_commute)
   137   apply (erule zdvd_zmult)
   138   done
   139 
   140 lemma [iff]: "(k::int) dvd m * k"
   141   apply (rule zdvd_zmult)
   142   apply (rule zdvd_refl)
   143   done
   144 
   145 lemma [iff]: "(k::int) dvd k * m"
   146   apply (rule zdvd_zmult2)
   147   apply (rule zdvd_refl)
   148   done
   149 
   150 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   151   apply (unfold dvd_def)
   152   apply (simp add: zmult_assoc)
   153   apply blast
   154   done
   155 
   156 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   157   apply (rule zdvd_zmultD2)
   158   apply (subst zmult_commute)
   159   apply assumption
   160   done
   161 
   162 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   163   apply (unfold dvd_def)
   164   apply clarify
   165   apply (rule_tac x = "k * ka" in exI)
   166   apply (simp add: zmult_ac)
   167   done
   168 
   169 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
   170   apply (rule iffI)
   171    apply (erule_tac [2] zdvd_zadd)
   172    apply (subgoal_tac "n = (n + k * m) - k * m")
   173     apply (erule ssubst)
   174     apply (erule zdvd_zdiff)
   175     apply simp_all
   176   done
   177 
   178 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   179   apply (unfold dvd_def)
   180   apply (auto simp add: zmod_zmult_zmult1)
   181   done
   182 
   183 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   184   apply (subgoal_tac "k dvd n * (m div n) + m mod n")
   185    apply (simp add: zmod_zdiv_equality [symmetric])
   186   apply (simp add: zdvd_zadd zdvd_zmult2)
   187   done
   188 
   189 lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = Numeral0)"
   190   apply (unfold dvd_def)
   191   apply auto
   192   done
   193 
   194 lemma zdvd_not_zless: "Numeral0 < m ==> m < n ==> \<not> n dvd (m::int)"
   195   apply (unfold dvd_def)
   196   apply auto
   197   apply (subgoal_tac "Numeral0 < n")
   198    prefer 2
   199    apply (blast intro: zless_trans)
   200   apply (simp add: int_0_less_mult_iff)
   201   apply (subgoal_tac "n * k < n * Numeral1")
   202    apply (drule zmult_zless_cancel1 [THEN iffD1])
   203    apply auto
   204   done
   205 
   206 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   207   apply (auto simp add: dvd_def nat_abs_mult_distrib)
   208   apply (auto simp add: nat_eq_iff zabs_eq_iff)
   209    apply (rule_tac [2] x = "-(int k)" in exI)
   210   apply (auto simp add: zmult_int [symmetric])
   211   done
   212 
   213 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   214   apply (auto simp add: dvd_def zabs_def zmult_int [symmetric])
   215     apply (rule_tac [3] x = "nat k" in exI)
   216     apply (rule_tac [2] x = "-(int k)" in exI)
   217     apply (rule_tac x = "nat (-k)" in exI)
   218     apply (cut_tac [3] k = m in int_less_0_conv)
   219     apply (cut_tac k = m in int_less_0_conv)
   220     apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
   221       nat_mult_distrib [symmetric] nat_eq_iff2)
   222   done
   223 
   224 lemma nat_dvd_iff: "(nat z dvd m) = (if Numeral0 \<le> z then (z dvd int m) else m = 0)"
   225   apply (auto simp add: dvd_def zmult_int [symmetric])
   226   apply (rule_tac x = "nat k" in exI)
   227   apply (cut_tac k = m in int_less_0_conv)
   228   apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
   229     nat_mult_distrib [symmetric] nat_eq_iff2)
   230   done
   231 
   232 lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   233   apply (auto simp add: dvd_def)
   234    apply (rule_tac [!] x = "-k" in exI)
   235    apply auto
   236   done
   237 
   238 lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   239   apply (auto simp add: dvd_def)
   240    apply (drule zminus_equation [THEN iffD1])
   241    apply (rule_tac [!] x = "-k" in exI)
   242    apply auto
   243   done
   244 
   245 
   246 subsection {* Euclid's Algorithm and GCD *}
   247 
   248 lemma zgcd_0 [simp]: "zgcd (m, Numeral0) = abs m"
   249   apply (simp add: zgcd_def zabs_def)
   250   done
   251 
   252 lemma zgcd_0_left [simp]: "zgcd (Numeral0, m) = abs m"
   253   apply (simp add: zgcd_def zabs_def)
   254   done
   255 
   256 lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)"
   257   apply (simp add: zgcd_def)
   258   done
   259 
   260 lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)"
   261   apply (simp add: zgcd_def)
   262   done
   263 
   264 lemma zgcd_non_0: "Numeral0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   265   apply (frule_tac b = n and a = m in pos_mod_sign)
   266   apply (simp add: zgcd_def zabs_def nat_mod_distrib)
   267   apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if)
   268   apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   269   apply (frule_tac a = m in pos_mod_bound)
   270   apply (simp add: nat_diff_distrib)
   271   apply (rule gcd_diff2)
   272   apply (simp add: nat_le_eq_zle)
   273   done
   274 
   275 lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
   276   apply (tactic {* zdiv_undefined_case_tac "n = Numeral0" 1 *})
   277   apply (auto simp add: linorder_neq_iff zgcd_non_0)
   278   apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0)
   279    apply auto
   280   done
   281 
   282 lemma zgcd_1 [simp]: "zgcd (m, Numeral1) = Numeral1"
   283   apply (simp add: zgcd_def zabs_def)
   284   done
   285 
   286 lemma zgcd_0_1_iff [simp]: "(zgcd (Numeral0, m) = Numeral1) = (abs m = Numeral1)"
   287   apply (simp add: zgcd_def zabs_def)
   288   done
   289 
   290 lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m"
   291   apply (simp add: zgcd_def zabs_def int_dvd_iff)
   292   done
   293 
   294 lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n"
   295   apply (simp add: zgcd_def zabs_def int_dvd_iff)
   296   done
   297 
   298 lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \<and> k dvd n)"
   299   apply (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff)
   300   done
   301 
   302 lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)"
   303   apply (simp add: zgcd_def gcd_commute)
   304   done
   305 
   306 lemma zgcd_1_left [simp]: "zgcd (Numeral1, m) = Numeral1"
   307   apply (simp add: zgcd_def gcd_1_left)
   308   done
   309 
   310 lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))"
   311   apply (simp add: zgcd_def gcd_assoc)
   312   done
   313 
   314 lemma zgcd_left_commute: "zgcd (k, zgcd (m, n)) = zgcd (m, zgcd (k, n))"
   315   apply (rule zgcd_commute [THEN trans])
   316   apply (rule zgcd_assoc [THEN trans])
   317   apply (rule zgcd_commute [THEN arg_cong])
   318   done
   319 
   320 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
   321   -- {* addition is an AC-operator *}
   322 
   323 lemma zgcd_zmult_distrib2: "Numeral0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
   324   apply (simp del: zmult_zminus_right
   325     add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
   326     zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
   327   done
   328 
   329 lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
   330   apply (simp add: zabs_def zgcd_zmult_distrib2)
   331   done
   332 
   333 lemma zgcd_self [simp]: "Numeral0 \<le> m ==> zgcd (m, m) = m"
   334   apply (cut_tac k = m and m = "Numeral1" and n = "Numeral1" in zgcd_zmult_distrib2)
   335    apply simp_all
   336   done
   337 
   338 lemma zgcd_zmult_eq_self [simp]: "Numeral0 \<le> k ==> zgcd (k, k * n) = k"
   339   apply (cut_tac k = k and m = "Numeral1" and n = n in zgcd_zmult_distrib2)
   340    apply simp_all
   341   done
   342 
   343 lemma zgcd_zmult_eq_self2 [simp]: "Numeral0 \<le> k ==> zgcd (k * n, k) = k"
   344   apply (cut_tac k = k and m = n and n = "Numeral1" in zgcd_zmult_distrib2)
   345    apply simp_all
   346   done
   347 
   348 lemma aux: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> Numeral0 \<le> m ==> k dvd m"
   349   apply (subgoal_tac "m = zgcd (m * n, m * k)")
   350    apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
   351    apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
   352   done
   353 
   354 lemma zrelprime_zdvd_zmult: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> k dvd m"
   355   apply (case_tac "Numeral0 \<le> m")
   356    apply (blast intro: aux)
   357   apply (subgoal_tac "k dvd -m")
   358    apply (rule_tac [2] aux)
   359      apply auto
   360   done
   361 
   362 lemma zprime_imp_zrelprime:
   363     "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = Numeral1"
   364   apply (unfold zprime_def)
   365   apply auto
   366   done
   367 
   368 lemma zless_zprime_imp_zrelprime:
   369     "p \<in> zprime ==> Numeral0 < n ==> n < p ==> zgcd (n, p) = Numeral1"
   370   apply (erule zprime_imp_zrelprime)
   371   apply (erule zdvd_not_zless)
   372   apply assumption
   373   done
   374 
   375 lemma zprime_zdvd_zmult:
   376     "Numeral0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   377   apply safe
   378   apply (rule zrelprime_zdvd_zmult)
   379    apply (rule zprime_imp_zrelprime)
   380     apply auto
   381   done
   382 
   383 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k, n) = zgcd (m, n)"
   384   apply (rule zgcd_eq [THEN trans])
   385   apply (simp add: zmod_zadd1_eq)
   386   apply (rule zgcd_eq [symmetric])
   387   done
   388 
   389 lemma zgcd_zdvd_zgcd_zmult: "zgcd (m, n) dvd zgcd (k * m, n)"
   390   apply (simp add: zgcd_greatest_iff)
   391   apply (blast intro: zdvd_trans)
   392   done
   393 
   394 lemma zgcd_zmult_zdvd_zgcd:
   395     "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) dvd zgcd (m, n)"
   396   apply (simp add: zgcd_greatest_iff)
   397   apply (rule_tac n = k in zrelprime_zdvd_zmult)
   398    prefer 2
   399    apply (simp add: zmult_commute)
   400   apply (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))")
   401    apply simp
   402   apply (simp (no_asm) add: zgcd_ac)
   403   done
   404 
   405 lemma zgcd_zmult_cancel: "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) = zgcd (m, n)"
   406   apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
   407   done
   408 
   409 lemma zgcd_zgcd_zmult:
   410     "zgcd (k, m) = Numeral1 ==> zgcd (n, m) = Numeral1 ==> zgcd (k * n, m) = Numeral1"
   411   apply (simp (no_asm_simp) add: zgcd_zmult_cancel)
   412   done
   413 
   414 lemma zdvd_iff_zgcd: "Numeral0 < m ==> (m dvd n) = (zgcd (n, m) = m)"
   415   apply safe
   416    apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans)
   417     apply (rule_tac [3] zgcd_zdvd1)
   418    apply simp_all
   419   apply (unfold dvd_def)
   420   apply auto
   421   done
   422 
   423 
   424 subsection {* Congruences *}
   425 
   426 lemma zcong_1 [simp]: "[a = b] (mod Numeral1)"
   427   apply (unfold zcong_def)
   428   apply auto
   429   done
   430 
   431 lemma zcong_refl [simp]: "[k = k] (mod m)"
   432   apply (unfold zcong_def)
   433   apply auto
   434   done
   435 
   436 lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
   437   apply (unfold zcong_def dvd_def)
   438   apply auto
   439    apply (rule_tac [!] x = "-k" in exI)
   440    apply auto
   441   done
   442 
   443 lemma zcong_zadd:
   444     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
   445   apply (unfold zcong_def)
   446   apply (rule_tac s = "(a - b) + (c - d)" in subst)
   447    apply (rule_tac [2] zdvd_zadd)
   448     apply auto
   449   done
   450 
   451 lemma zcong_zdiff:
   452     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)"
   453   apply (unfold zcong_def)
   454   apply (rule_tac s = "(a - b) - (c - d)" in subst)
   455    apply (rule_tac [2] zdvd_zdiff)
   456     apply auto
   457   done
   458 
   459 lemma zcong_trans:
   460     "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
   461   apply (unfold zcong_def dvd_def)
   462   apply auto
   463   apply (rule_tac x = "k + ka" in exI)
   464   apply (simp add: zadd_ac zadd_zmult_distrib2)
   465   done
   466 
   467 lemma zcong_zmult:
   468     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
   469   apply (rule_tac b = "b * c" in zcong_trans)
   470    apply (unfold zcong_def)
   471    apply (rule_tac s = "c * (a - b)" in subst)
   472     apply (rule_tac [3] s = "b * (c - d)" in subst)
   473      prefer 4
   474      apply (blast intro: zdvd_zmult)
   475     prefer 2
   476     apply (blast intro: zdvd_zmult)
   477    apply (simp_all add: zdiff_zmult_distrib2 zmult_commute)
   478   done
   479 
   480 lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
   481   apply (rule zcong_zmult)
   482   apply simp_all
   483   done
   484 
   485 lemma zcong_scalar2: "[a = b] (mod m) ==> [k * a = k * b] (mod m)"
   486   apply (rule zcong_zmult)
   487   apply simp_all
   488   done
   489 
   490 lemma zcong_zmult_self: "[a * m = b * m] (mod m)"
   491   apply (unfold zcong_def)
   492   apply (rule zdvd_zdiff)
   493    apply simp_all
   494   done
   495 
   496 lemma zcong_square:
   497   "p \<in> zprime ==> Numeral0 < a ==> [a * a = Numeral1] (mod p)
   498     ==> [a = Numeral1] (mod p) \<or> [a = p - Numeral1] (mod p)"
   499   apply (unfold zcong_def)
   500   apply (rule zprime_zdvd_zmult)
   501     apply (rule_tac [3] s = "a * a - Numeral1 + p * (Numeral1 - a)" in subst)
   502      prefer 4
   503      apply (simp add: zdvd_reduce)
   504     apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2)
   505   done
   506 
   507 lemma zcong_cancel:
   508   "Numeral0 \<le> m ==>
   509     zgcd (k, m) = Numeral1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
   510   apply safe
   511    prefer 2
   512    apply (blast intro: zcong_scalar)
   513   apply (case_tac "b < a")
   514    prefer 2
   515    apply (subst zcong_sym)
   516    apply (unfold zcong_def)
   517    apply (rule_tac [!] zrelprime_zdvd_zmult)
   518      apply (simp_all add: zdiff_zmult_distrib)
   519   apply (subgoal_tac "m dvd (-(a * k - b * k))")
   520    apply (simp add: zminus_zdiff_eq)
   521   apply (subst zdvd_zminus_iff)
   522   apply assumption
   523   done
   524 
   525 lemma zcong_cancel2:
   526   "Numeral0 \<le> m ==>
   527     zgcd (k, m) = Numeral1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
   528   apply (simp add: zmult_commute zcong_cancel)
   529   done
   530 
   531 lemma zcong_zgcd_zmult_zmod:
   532   "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = Numeral1
   533     ==> [a = b] (mod m * n)"
   534   apply (unfold zcong_def dvd_def)
   535   apply auto
   536   apply (subgoal_tac "m dvd n * ka")
   537    apply (subgoal_tac "m dvd ka")
   538     apply (case_tac [2] "Numeral0 \<le> ka")
   539      prefer 3
   540      apply (subst zdvd_zminus_iff [symmetric])
   541      apply (rule_tac n = n in zrelprime_zdvd_zmult)
   542       apply (simp add: zgcd_commute)
   543      apply (simp add: zmult_commute zdvd_zminus_iff)
   544     prefer 2
   545     apply (rule_tac n = n in zrelprime_zdvd_zmult)
   546      apply (simp add: zgcd_commute)
   547     apply (simp add: zmult_commute)
   548    apply (auto simp add: dvd_def)
   549   apply (blast intro: sym)
   550   done
   551 
   552 lemma zcong_zless_imp_eq:
   553   "Numeral0 \<le> a ==>
   554     a < m ==> Numeral0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
   555   apply (unfold zcong_def dvd_def)
   556   apply auto
   557   apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
   558   apply (cut_tac z = a and w = b in zless_linear)
   559   apply auto
   560    apply (subgoal_tac [2] "(a - b) mod m = a - b")
   561     apply (rule_tac [3] mod_pos_pos_trivial)
   562      apply auto
   563   apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)")
   564    apply (rule_tac [2] mod_pos_pos_trivial)
   565     apply auto
   566   done
   567 
   568 lemma zcong_square_zless:
   569   "p \<in> zprime ==> Numeral0 < a ==> a < p ==>
   570     [a * a = Numeral1] (mod p) ==> a = Numeral1 \<or> a = p - Numeral1"
   571   apply (cut_tac p = p and a = a in zcong_square)
   572      apply (simp add: zprime_def)
   573     apply (auto intro: zcong_zless_imp_eq)
   574   done
   575 
   576 lemma zcong_not:
   577     "Numeral0 < a ==> a < m ==> Numeral0 < b ==> b < a ==> \<not> [a = b] (mod m)"
   578   apply (unfold zcong_def)
   579   apply (rule zdvd_not_zless)
   580    apply auto
   581   done
   582 
   583 lemma zcong_zless_0:
   584     "Numeral0 \<le> a ==> a < m ==> [a = Numeral0] (mod m) ==> a = Numeral0"
   585   apply (unfold zcong_def dvd_def)
   586   apply auto
   587   apply (subgoal_tac "Numeral0 < m")
   588    apply (rotate_tac -1)
   589    apply (simp add: int_0_le_mult_iff)
   590    apply (subgoal_tac "m * k < m * Numeral1")
   591     apply (drule zmult_zless_cancel1 [THEN iffD1])
   592     apply (auto simp add: linorder_neq_iff)
   593   done
   594 
   595 lemma zcong_zless_unique:
   596     "Numeral0 < m ==> (\<exists>!b. Numeral0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   597   apply auto
   598    apply (subgoal_tac [2] "[b = y] (mod m)")
   599     apply (case_tac [2] "b = Numeral0")
   600      apply (case_tac [3] "y = Numeral0")
   601       apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le
   602         simp add: zcong_sym)
   603   apply (unfold zcong_def dvd_def)
   604   apply (rule_tac x = "a mod m" in exI)
   605   apply (auto simp add: pos_mod_sign pos_mod_bound)
   606   apply (rule_tac x = "-(a div m)" in exI)
   607   apply (cut_tac a = a and b = m in zmod_zdiv_equality)
   608   apply auto
   609   done
   610 
   611 lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
   612   apply (unfold zcong_def dvd_def)
   613   apply auto
   614    apply (rule_tac [!] x = "-k" in exI)
   615    apply auto
   616   done
   617 
   618 lemma zgcd_zcong_zgcd:
   619   "Numeral0 < m ==>
   620     zgcd (a, m) = Numeral1 ==> [a = b] (mod m) ==> zgcd (b, m) = Numeral1"
   621   apply (auto simp add: zcong_iff_lin)
   622   done
   623 
   624 lemma aux: "a = c ==> b = d ==> a - b = c - (d::int)"
   625   apply auto
   626   done
   627 
   628 lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   629   apply (rule_tac "s" = "(m * (a div m) + a mod m) - (m * (b div m) + b mod m)"
   630     in trans)
   631    prefer 2
   632    apply (simp add: zdiff_zmult_distrib2)
   633   apply (rule aux)
   634    apply (rule_tac [!] zmod_zdiv_equality)
   635   done
   636 
   637 lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   638   apply (unfold zcong_def)
   639   apply (rule_tac t = "a - b" in ssubst)
   640   apply (rule_tac "m" = "m" in aux)
   641   apply (rule trans)
   642    apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
   643   apply (simp add: zadd_commute)
   644   done
   645 
   646 lemma zcong_zmod_eq: "Numeral0 < m ==> [a = b] (mod m) = (a mod m = b mod m)"
   647   apply auto
   648    apply (rule_tac m = m in zcong_zless_imp_eq)
   649        prefer 5
   650        apply (subst zcong_zmod [symmetric])
   651        apply (simp_all add: pos_mod_bound pos_mod_sign)
   652   apply (unfold zcong_def dvd_def)
   653   apply (rule_tac x = "a div m - b div m" in exI)
   654   apply (rule_tac m1 = m in aux [THEN trans])
   655   apply auto
   656   done
   657 
   658 lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)"
   659   apply (auto simp add: zcong_def)
   660   done
   661 
   662 lemma zcong_zero [iff]: "[a = b] (mod Numeral0) = (a = b)"
   663   apply (auto simp add: zcong_def)
   664   done
   665 
   666 lemma "[a = b] (mod m) = (a mod m = b mod m)"
   667   apply (tactic {* zdiv_undefined_case_tac "m = Numeral0" 1 *})
   668   apply (case_tac "Numeral0 < m")
   669    apply (simp add: zcong_zmod_eq)
   670   apply (rule_tac t = m in zminus_zminus [THEN subst])
   671   apply (subst zcong_zminus)
   672   apply (subst zcong_zmod_eq)
   673    apply arith
   674   oops  -- {* FIXME: finish this proof? *}
   675 
   676 
   677 subsection {* Modulo *}
   678 
   679 lemma zmod_zdvd_zmod:
   680     "Numeral0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   681   apply (unfold dvd_def)
   682   apply auto
   683   apply (subst zcong_zmod_eq [symmetric])
   684    prefer 2
   685    apply (subst zcong_iff_lin)
   686    apply (rule_tac x = "k * (a div (m * k))" in exI)
   687    apply (subst zadd_commute)
   688    apply (subst zmult_assoc [symmetric])
   689    apply (rule_tac zmod_zdiv_equality)
   690   apply assumption
   691   done
   692 
   693 
   694 subsection {* Extended GCD *}
   695 
   696 declare xzgcda.simps [simp del]
   697 
   698 lemma aux1:
   699   "zgcd (r', r) = k --> Numeral0 < r -->
   700     (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
   701   apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   702     z = s and aa = t' and ab = t in xzgcda.induct)
   703   apply (subst zgcd_eq)
   704   apply (subst xzgcda.simps)
   705   apply auto
   706   apply (case_tac "r' mod r = Numeral0")
   707    prefer 2
   708    apply (frule_tac a = "r'" in pos_mod_sign)
   709    apply auto
   710    apply arith
   711   apply (rule exI)
   712   apply (rule exI)
   713   apply (subst xzgcda.simps)
   714   apply auto
   715   apply (simp add: zabs_def)
   716   done
   717 
   718 lemma aux2:
   719   "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> Numeral0 < r -->
   720     zgcd (r', r) = k"
   721   apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   722     z = s and aa = t' and ab = t in xzgcda.induct)
   723   apply (subst zgcd_eq)
   724   apply (subst xzgcda.simps)
   725   apply (auto simp add: linorder_not_le)
   726   apply (case_tac "r' mod r = Numeral0")
   727    prefer 2
   728    apply (frule_tac a = "r'" in pos_mod_sign)
   729    apply auto
   730    apply arith
   731   apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   732   apply (subst xzgcda.simps)
   733   apply auto
   734   apply (simp add: zabs_def)
   735   done
   736 
   737 lemma xzgcd_correct:
   738     "Numeral0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
   739   apply (unfold xzgcd_def)
   740   apply (rule iffI)
   741    apply (rule_tac [2] aux2 [THEN mp, THEN mp])
   742     apply (rule aux1 [THEN mp, THEN mp])
   743      apply auto
   744   done
   745 
   746 
   747 text {* \medskip @{term xzgcd} linear *}
   748 
   749 lemma aux:
   750   "(a - r * b) * m + (c - r * d) * (n::int) =
   751     (a * m + c * n) - r * (b * m + d * n)"
   752   apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
   753   done
   754 
   755 lemma aux:
   756   "r' = s' * m + t' * n ==> r = s * m + t * n
   757     ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
   758   apply (rule trans)
   759    apply (rule_tac [2] aux [symmetric])
   760   apply simp
   761   apply (subst eq_zdiff_eq)
   762   apply (rule trans [symmetric])
   763   apply (rule_tac b = "s * m + t * n" in zmod_zdiv_equality)
   764   apply (simp add: zmult_commute)
   765   done
   766 
   767 lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"
   768   by (rule iffD2 [OF order_less_le conjI])
   769 
   770 lemma xzgcda_linear [rule_format]:
   771   "Numeral0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) -->
   772     r' = s' * m + t' * n -->  r = s * m + t * n --> rn = sn * m + tn * n"
   773   apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   774     z = s and aa = t' and ab = t in xzgcda.induct)
   775   apply (subst xzgcda.simps)
   776   apply (simp (no_asm))
   777   apply (rule impI)+
   778   apply (case_tac "r' mod r = Numeral0")
   779    apply (simp add: xzgcda.simps)
   780    apply clarify
   781   apply (subgoal_tac "Numeral0 < r' mod r")
   782    apply (rule_tac [2] order_le_neq_implies_less)
   783    apply (rule_tac [2] pos_mod_sign)
   784     apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
   785       s = s and t' = t' and t = t in aux)
   786       apply auto
   787   done
   788 
   789 lemma xzgcd_linear:
   790     "Numeral0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n"
   791   apply (unfold xzgcd_def)
   792   apply (erule xzgcda_linear)
   793     apply assumption
   794    apply auto
   795   done
   796 
   797 lemma zgcd_ex_linear:
   798     "Numeral0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)"
   799   apply (simp add: xzgcd_correct)
   800   apply safe
   801   apply (rule exI)+
   802   apply (erule xzgcd_linear)
   803   apply auto
   804   done
   805 
   806 lemma zcong_lineq_ex:
   807     "Numeral0 < n ==> zgcd (a, n) = Numeral1 ==> \<exists>x. [a * x = Numeral1] (mod n)"
   808   apply (cut_tac m = a and n = n and k = "Numeral1" in zgcd_ex_linear)
   809     apply safe
   810   apply (rule_tac x = s in exI)
   811   apply (rule_tac b = "s * a + t * n" in zcong_trans)
   812    prefer 2
   813    apply simp
   814   apply (unfold zcong_def)
   815   apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff)
   816   done
   817 
   818 lemma zcong_lineq_unique:
   819   "Numeral0 < n ==>
   820     zgcd (a, n) = Numeral1 ==> \<exists>!x. Numeral0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
   821   apply auto
   822    apply (rule_tac [2] zcong_zless_imp_eq)
   823        apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *})
   824          apply (rule_tac [8] zcong_trans)
   825           apply (simp_all (no_asm_simp))
   826    prefer 2
   827    apply (simp add: zcong_sym)
   828   apply (cut_tac a = a and n = n in zcong_lineq_ex)
   829     apply auto
   830   apply (rule_tac x = "x * b mod n" in exI)
   831   apply safe
   832     apply (simp_all (no_asm_simp) add: pos_mod_bound pos_mod_sign)
   833   apply (subst zcong_zmod)
   834   apply (subst zmod_zmult1_eq [symmetric])
   835   apply (subst zcong_zmod [symmetric])
   836   apply (subgoal_tac "[a * x * b = Numeral1 * b] (mod n)")
   837    apply (rule_tac [2] zcong_zmult)
   838     apply (simp_all add: zmult_assoc)
   839   done
   840 
   841 end