src/HOL/Old_Number_Theory/IntPrimes.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57514 bdc2c6b40bf2 child 58889 5b7a9633cfa8 permissions -rw-r--r--
simpler proof
```     1 (*  Title:      HOL/Old_Number_Theory/IntPrimes.thy
```
```     2     Author:     Thomas M. Rasmussen
```
```     3     Copyright   2000  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 header {* Divisibility and prime numbers (on integers) *}
```
```     7
```
```     8 theory IntPrimes
```
```     9 imports Primes
```
```    10 begin
```
```    11
```
```    12 text {*
```
```    13   The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
```
```    14   congruences (all on the Integers).  Comparable to theory @{text
```
```    15   Primes}, but @{text dvd} is included here as it is not present in
```
```    16   main HOL.  Also includes extended GCD and congruences not present in
```
```    17   @{text Primes}.
```
```    18 *}
```
```    19
```
```    20
```
```    21 subsection {* Definitions *}
```
```    22
```
```    23 fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
```
```    24 where
```
```    25   "xzgcda m n r' r s' s t' t =
```
```    26         (if r \<le> 0 then (r', s', t')
```
```    27          else xzgcda m n r (r' mod r)
```
```    28                       s (s' - (r' div r) * s)
```
```    29                       t (t' - (r' div r) * t))"
```
```    30
```
```    31 definition zprime :: "int \<Rightarrow> bool"
```
```    32   where "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
```
```    33
```
```    34 definition xzgcd :: "int => int => int * int * int"
```
```    35   where "xzgcd m n = xzgcda m n m n 1 0 0 1"
```
```    36
```
```    37 definition zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))")
```
```    38   where "[a = b] (mod m) = (m dvd (a - b))"
```
```    39
```
```    40
```
```    41 subsection {* Euclid's Algorithm and GCD *}
```
```    42
```
```    43
```
```    44 lemma zrelprime_zdvd_zmult_aux:
```
```    45      "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
```
```    46     by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs mult_1_right)
```
```    47
```
```    48 lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
```
```    49   apply (case_tac "0 \<le> m")
```
```    50    apply (blast intro: zrelprime_zdvd_zmult_aux)
```
```    51   apply (subgoal_tac "k dvd -m")
```
```    52    apply (rule_tac [2] zrelprime_zdvd_zmult_aux, auto)
```
```    53   done
```
```    54
```
```    55 lemma zgcd_geq_zero: "0 <= zgcd x y"
```
```    56   by (auto simp add: zgcd_def)
```
```    57
```
```    58 text{*This is merely a sanity check on zprime, since the previous version
```
```    59       denoted the empty set.*}
```
```    60 lemma "zprime 2"
```
```    61   apply (auto simp add: zprime_def)
```
```    62   apply (frule zdvd_imp_le, simp)
```
```    63   apply (auto simp add: order_le_less dvd_def)
```
```    64   done
```
```    65
```
```    66 lemma zprime_imp_zrelprime:
```
```    67     "zprime p ==> \<not> p dvd n ==> zgcd n p = 1"
```
```    68   apply (auto simp add: zprime_def)
```
```    69   apply (metis zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
```
```    70   done
```
```    71
```
```    72 lemma zless_zprime_imp_zrelprime:
```
```    73     "zprime p ==> 0 < n ==> n < p ==> zgcd n p = 1"
```
```    74   apply (erule zprime_imp_zrelprime)
```
```    75   apply (erule zdvd_not_zless, assumption)
```
```    76   done
```
```    77
```
```    78 lemma zprime_zdvd_zmult:
```
```    79     "0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
```
```    80   by (metis zgcd_zdvd1 zgcd_zdvd2 zgcd_pos zprime_def zrelprime_dvd_mult)
```
```    81
```
```    82 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
```
```    83   apply (rule zgcd_eq [THEN trans])
```
```    84   apply (simp add: mod_add_eq)
```
```    85   apply (rule zgcd_eq [symmetric])
```
```    86   done
```
```    87
```
```    88 lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
```
```    89 by (simp add: zgcd_greatest_iff)
```
```    90
```
```    91 lemma zgcd_zmult_zdvd_zgcd:
```
```    92     "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
```
```    93   apply (simp add: zgcd_greatest_iff)
```
```    94   apply (rule_tac n = k in zrelprime_zdvd_zmult)
```
```    95    prefer 2
```
```    96    apply (simp add: mult.commute)
```
```    97   apply (metis zgcd_1 zgcd_commute zgcd_left_commute)
```
```    98   done
```
```    99
```
```   100 lemma zgcd_zmult_cancel: "zgcd k n = 1 ==> zgcd (k * m) n = zgcd m n"
```
```   101   by (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
```
```   102
```
```   103 lemma zgcd_zgcd_zmult:
```
```   104     "zgcd k m = 1 ==> zgcd n m = 1 ==> zgcd (k * n) m = 1"
```
```   105   by (simp add: zgcd_zmult_cancel)
```
```   106
```
```   107 lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
```
```   108   by (metis abs_of_pos dvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
```
```   109
```
```   110
```
```   111
```
```   112 subsection {* Congruences *}
```
```   113
```
```   114 lemma zcong_1 [simp]: "[a = b] (mod 1)"
```
```   115   by (unfold zcong_def, auto)
```
```   116
```
```   117 lemma zcong_refl [simp]: "[k = k] (mod m)"
```
```   118   by (unfold zcong_def, auto)
```
```   119
```
```   120 lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
```
```   121   unfolding zcong_def minus_diff_eq [of a, symmetric] dvd_minus_iff ..
```
```   122
```
```   123 lemma zcong_zadd:
```
```   124     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
```
```   125   apply (unfold zcong_def)
```
```   126   apply (rule_tac s = "(a - b) + (c - d)" in subst)
```
```   127    apply (rule_tac [2] dvd_add, auto)
```
```   128   done
```
```   129
```
```   130 lemma zcong_zdiff:
```
```   131     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)"
```
```   132   apply (unfold zcong_def)
```
```   133   apply (rule_tac s = "(a - b) - (c - d)" in subst)
```
```   134    apply (rule_tac [2] dvd_diff, auto)
```
```   135   done
```
```   136
```
```   137 lemma zcong_trans:
```
```   138   "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
```
```   139 unfolding zcong_def by (auto elim!: dvdE simp add: algebra_simps)
```
```   140
```
```   141 lemma zcong_zmult:
```
```   142     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
```
```   143   apply (rule_tac b = "b * c" in zcong_trans)
```
```   144    apply (unfold zcong_def)
```
```   145   apply (metis right_diff_distrib dvd_mult mult.commute)
```
```   146   apply (metis right_diff_distrib dvd_mult)
```
```   147   done
```
```   148
```
```   149 lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
```
```   150   by (rule zcong_zmult, simp_all)
```
```   151
```
```   152 lemma zcong_scalar2: "[a = b] (mod m) ==> [k * a = k * b] (mod m)"
```
```   153   by (rule zcong_zmult, simp_all)
```
```   154
```
```   155 lemma zcong_zmult_self: "[a * m = b * m] (mod m)"
```
```   156   apply (unfold zcong_def)
```
```   157   apply (rule dvd_diff, simp_all)
```
```   158   done
```
```   159
```
```   160 lemma zcong_square:
```
```   161    "[| zprime p;  0 < a;  [a * a = 1] (mod p)|]
```
```   162     ==> [a = 1] (mod p) \<or> [a = p - 1] (mod p)"
```
```   163   apply (unfold zcong_def)
```
```   164   apply (rule zprime_zdvd_zmult)
```
```   165     apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst)
```
```   166      prefer 4
```
```   167      apply (simp add: zdvd_reduce)
```
```   168     apply (simp_all add: left_diff_distrib mult.commute right_diff_distrib)
```
```   169   done
```
```   170
```
```   171 lemma zcong_cancel:
```
```   172   "0 \<le> m ==>
```
```   173     zgcd k m = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
```
```   174   apply safe
```
```   175    prefer 2
```
```   176    apply (blast intro: zcong_scalar)
```
```   177   apply (case_tac "b < a")
```
```   178    prefer 2
```
```   179    apply (subst zcong_sym)
```
```   180    apply (unfold zcong_def)
```
```   181    apply (rule_tac [!] zrelprime_zdvd_zmult)
```
```   182      apply (simp_all add: left_diff_distrib)
```
```   183   apply (subgoal_tac "m dvd (-(a * k - b * k))")
```
```   184    apply simp
```
```   185   apply (subst dvd_minus_iff, assumption)
```
```   186   done
```
```   187
```
```   188 lemma zcong_cancel2:
```
```   189   "0 \<le> m ==>
```
```   190     zgcd k m = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
```
```   191   by (simp add: mult.commute zcong_cancel)
```
```   192
```
```   193 lemma zcong_zgcd_zmult_zmod:
```
```   194   "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
```
```   195     ==> [a = b] (mod m * n)"
```
```   196   apply (auto simp add: zcong_def dvd_def)
```
```   197   apply (subgoal_tac "m dvd n * ka")
```
```   198    apply (subgoal_tac "m dvd ka")
```
```   199     apply (case_tac [2] "0 \<le> ka")
```
```   200   apply (metis dvd_mult_div_cancel dvd_refl dvd_mult_left mult.commute zrelprime_zdvd_zmult)
```
```   201   apply (metis abs_dvd_iff abs_of_nonneg add_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs mult_1_right mult.commute)
```
```   202   apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff order_antisym linorder_linear order_refl mult.commute zrelprime_zdvd_zmult)
```
```   203   apply (metis dvd_triv_left)
```
```   204   done
```
```   205
```
```   206 lemma zcong_zless_imp_eq:
```
```   207   "0 \<le> a ==>
```
```   208     a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
```
```   209   apply (unfold zcong_def dvd_def, auto)
```
```   210   apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
```
```   211   apply (metis diff_add_cancel mod_pos_pos_trivial add_0 add.commute zmod_eq_0_iff mod_add_right_eq)
```
```   212   done
```
```   213
```
```   214 lemma zcong_square_zless:
```
```   215   "zprime p ==> 0 < a ==> a < p ==>
```
```   216     [a * a = 1] (mod p) ==> a = 1 \<or> a = p - 1"
```
```   217   apply (cut_tac p = p and a = a in zcong_square)
```
```   218      apply (simp add: zprime_def)
```
```   219     apply (auto intro: zcong_zless_imp_eq)
```
```   220   done
```
```   221
```
```   222 lemma zcong_not:
```
```   223     "0 < a ==> a < m ==> 0 < b ==> b < a ==> \<not> [a = b] (mod m)"
```
```   224   apply (unfold zcong_def)
```
```   225   apply (rule zdvd_not_zless, auto)
```
```   226   done
```
```   227
```
```   228 lemma zcong_zless_0:
```
```   229     "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
```
```   230   apply (unfold zcong_def dvd_def, auto)
```
```   231   apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
```
```   232   done
```
```   233
```
```   234 lemma zcong_zless_unique:
```
```   235     "0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
```
```   236   apply auto
```
```   237    prefer 2 apply (metis zcong_sym zcong_trans zcong_zless_imp_eq)
```
```   238   apply (unfold zcong_def dvd_def)
```
```   239   apply (rule_tac x = "a mod m" in exI, auto)
```
```   240   apply (metis zmult_div_cancel)
```
```   241   done
```
```   242
```
```   243 lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
```
```   244   unfolding zcong_def
```
```   245   apply (auto elim!: dvdE simp add: algebra_simps)
```
```   246   apply (rule_tac x = "-k" in exI) apply simp
```
```   247   done
```
```   248
```
```   249 lemma zgcd_zcong_zgcd:
```
```   250   "0 < m ==>
```
```   251     zgcd a m = 1 ==> [a = b] (mod m) ==> zgcd b m = 1"
```
```   252   by (auto simp add: zcong_iff_lin)
```
```   253
```
```   254 lemma zcong_zmod_aux:
```
```   255      "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
```
```   256   by(simp add: right_diff_distrib add_diff_eq eq_diff_eq ac_simps)
```
```   257
```
```   258 lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
```
```   259   apply (unfold zcong_def)
```
```   260   apply (rule_tac t = "a - b" in ssubst)
```
```   261   apply (rule_tac m = m in zcong_zmod_aux)
```
```   262   apply (rule trans)
```
```   263    apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
```
```   264   apply (simp add: add.commute)
```
```   265   done
```
```   266
```
```   267 lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)"
```
```   268   apply auto
```
```   269   apply (metis pos_mod_conj zcong_zless_imp_eq zcong_zmod)
```
```   270   apply (metis zcong_refl zcong_zmod)
```
```   271   done
```
```   272
```
```   273 lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)"
```
```   274   by (auto simp add: zcong_def)
```
```   275
```
```   276 lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)"
```
```   277   by (auto simp add: zcong_def)
```
```   278
```
```   279 lemma "[a = b] (mod m) = (a mod m = b mod m)"
```
```   280   apply (cases "m = 0", simp)
```
```   281   apply (simp add: linorder_neq_iff)
```
```   282   apply (erule disjE)
```
```   283    prefer 2 apply (simp add: zcong_zmod_eq)
```
```   284   txt{*Remainding case: @{term "m<0"}*}
```
```   285   apply (rule_tac t = m in minus_minus [THEN subst])
```
```   286   apply (subst zcong_zminus)
```
```   287   apply (subst zcong_zmod_eq, arith)
```
```   288   apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b])
```
```   289   apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
```
```   290   done
```
```   291
```
```   292 subsection {* Modulo *}
```
```   293
```
```   294 lemma zmod_zdvd_zmod:
```
```   295     "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
```
```   296   by (rule mod_mod_cancel)
```
```   297
```
```   298
```
```   299 subsection {* Extended GCD *}
```
```   300
```
```   301 declare xzgcda.simps [simp del]
```
```   302
```
```   303 lemma xzgcd_correct_aux1:
```
```   304   "zgcd r' r = k --> 0 < r -->
```
```   305     (\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn))"
```
```   306   apply (induct m n r' r s' s t' t rule: xzgcda.induct)
```
```   307   apply (subst zgcd_eq)
```
```   308   apply (subst xzgcda.simps, auto)
```
```   309   apply (case_tac "r' mod r = 0")
```
```   310    prefer 2
```
```   311    apply (frule_tac a = "r'" in pos_mod_sign, auto)
```
```   312   apply (rule exI)
```
```   313   apply (rule exI)
```
```   314   apply (subst xzgcda.simps, auto)
```
```   315   done
```
```   316
```
```   317 lemma xzgcd_correct_aux2:
```
```   318   "(\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn)) --> 0 < r -->
```
```   319     zgcd r' r = k"
```
```   320   apply (induct m n r' r s' s t' t rule: xzgcda.induct)
```
```   321   apply (subst zgcd_eq)
```
```   322   apply (subst xzgcda.simps)
```
```   323   apply (auto simp add: linorder_not_le)
```
```   324   apply (case_tac "r' mod r = 0")
```
```   325    prefer 2
```
```   326    apply (frule_tac a = "r'" in pos_mod_sign, auto)
```
```   327   apply (metis Pair_eq xzgcda.simps order_refl)
```
```   328   done
```
```   329
```
```   330 lemma xzgcd_correct:
```
```   331     "0 < n ==> (zgcd m n = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
```
```   332   apply (unfold xzgcd_def)
```
```   333   apply (rule iffI)
```
```   334    apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
```
```   335     apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp], auto)
```
```   336   done
```
```   337
```
```   338
```
```   339 text {* \medskip @{term xzgcd} linear *}
```
```   340
```
```   341 lemma xzgcda_linear_aux1:
```
```   342   "(a - r * b) * m + (c - r * d) * (n::int) =
```
```   343    (a * m + c * n) - r * (b * m + d * n)"
```
```   344   by (simp add: left_diff_distrib distrib_left mult.assoc)
```
```   345
```
```   346 lemma xzgcda_linear_aux2:
```
```   347   "r' = s' * m + t' * n ==> r = s * m + t * n
```
```   348     ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
```
```   349   apply (rule trans)
```
```   350    apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
```
```   351   apply (simp add: eq_diff_eq mult.commute)
```
```   352   done
```
```   353
```
```   354 lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"
```
```   355   by (rule iffD2 [OF order_less_le conjI])
```
```   356
```
```   357 lemma xzgcda_linear [rule_format]:
```
```   358   "0 < r --> xzgcda m n r' r s' s t' t = (rn, sn, tn) -->
```
```   359     r' = s' * m + t' * n -->  r = s * m + t * n --> rn = sn * m + tn * n"
```
```   360   apply (induct m n r' r s' s t' t rule: xzgcda.induct)
```
```   361   apply (subst xzgcda.simps)
```
```   362   apply (simp (no_asm))
```
```   363   apply (rule impI)+
```
```   364   apply (case_tac "r' mod r = 0")
```
```   365    apply (simp add: xzgcda.simps, clarify)
```
```   366   apply (subgoal_tac "0 < r' mod r")
```
```   367    apply (rule_tac [2] order_le_neq_implies_less)
```
```   368    apply (rule_tac [2] pos_mod_sign)
```
```   369     apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
```
```   370       s = s and t' = t' and t = t in xzgcda_linear_aux2, auto)
```
```   371   done
```
```   372
```
```   373 lemma xzgcd_linear:
```
```   374     "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n"
```
```   375   apply (unfold xzgcd_def)
```
```   376   apply (erule xzgcda_linear, assumption, auto)
```
```   377   done
```
```   378
```
```   379 lemma zgcd_ex_linear:
```
```   380     "0 < n ==> zgcd m n = k ==> (\<exists>s t. k = s * m + t * n)"
```
```   381   apply (simp add: xzgcd_correct, safe)
```
```   382   apply (rule exI)+
```
```   383   apply (erule xzgcd_linear, auto)
```
```   384   done
```
```   385
```
```   386 lemma zcong_lineq_ex:
```
```   387     "0 < n ==> zgcd a n = 1 ==> \<exists>x. [a * x = 1] (mod n)"
```
```   388   apply (cut_tac m = a and n = n and k = 1 in zgcd_ex_linear, safe)
```
```   389   apply (rule_tac x = s in exI)
```
```   390   apply (rule_tac b = "s * a + t * n" in zcong_trans)
```
```   391    prefer 2
```
```   392    apply simp
```
```   393   apply (unfold zcong_def)
```
```   394   apply (simp (no_asm) add: mult.commute)
```
```   395   done
```
```   396
```
```   397 lemma zcong_lineq_unique:
```
```   398   "0 < n ==>
```
```   399     zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
```
```   400   apply auto
```
```   401    apply (rule_tac [2] zcong_zless_imp_eq)
```
```   402        apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 6 *})
```
```   403          apply (rule_tac [8] zcong_trans)
```
```   404           apply (simp_all (no_asm_simp))
```
```   405    prefer 2
```
```   406    apply (simp add: zcong_sym)
```
```   407   apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
```
```   408   apply (rule_tac x = "x * b mod n" in exI, safe)
```
```   409     apply (simp_all (no_asm_simp))
```
```   410   apply (metis zcong_scalar zcong_zmod mod_mult_right_eq mult_1 mult.assoc)
```
```   411   done
```
```   412
```
```   413 end
```