src/HOL/Old_Number_Theory/IntPrimes.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44766 d4d33a4d7548
child 47162 9d7d919b9fd8
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 zdvd_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 zdvd_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 add_ac)
   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 right_distrib 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 zmod_zmult1_eq mult_1 mult_assoc)
   411   done
   412 
   413 end