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
```