src/HOL/Old_Number_Theory/Int2.thy
author wenzelm
Fri Aug 06 12:37:00 2010 +0200 (2010-08-06)
changeset 38159 e9b4835a54ee
parent 32479 521cc9bf2958
child 41541 1fa4725c4656
permissions -rw-r--r--
modernized specifications;
tuned headers;
     1 (*  Title:      HOL/Old_Number_Theory/Int2.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 header {*Integers: Divisibility and Congruences*}
     6 
     7 theory Int2
     8 imports Finite2 WilsonRuss
     9 begin
    10 
    11 definition MultInv :: "int => int => int"
    12   where "MultInv p x = x ^ nat (p - 2)"
    13 
    14 
    15 subsection {* Useful lemmas about dvd and powers *}
    16 
    17 lemma zpower_zdvd_prop1:
    18   "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
    19   by (induct n) (auto simp add: dvd_mult2 [of p y])
    20 
    21 lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
    22 proof -
    23   assume "n dvd m"
    24   then have "~(0 < m & m < n)"
    25     using zdvd_not_zless [of m n] by auto
    26   then show ?thesis by auto
    27 qed
    28 
    29 lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==>
    30     (p dvd m) | (p dvd n)"
    31   apply (cases "0 \<le> m")
    32   apply (simp add: zprime_zdvd_zmult)
    33   apply (insert zprime_zdvd_zmult [of "-m" p n])
    34   apply auto
    35   done
    36 
    37 lemma zpower_zdvd_prop2:
    38     "zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y"
    39   apply (induct n)
    40    apply simp
    41   apply (frule zprime_zdvd_zmult_better)
    42    apply simp
    43   apply (force simp del:dvd_mult)
    44   done
    45 
    46 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
    47 proof -
    48   assume "0 < z" then have modth: "x mod z \<ge> 0" by simp
    49   have "(x div z) * z \<le> (x div z) * z" by simp
    50   then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
    51   also have "\<dots> = x"
    52     by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
    53   also assume  "x < y * z"
    54   finally show ?thesis
    55     by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
    56 qed
    57 
    58 lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"
    59 proof -
    60   assume "0 < z" and "x < (y * z) + z"
    61   then have "x < (y + 1) * z" by (auto simp add: int_distrib)
    62   then have "x div z < y + 1"
    63     apply -
    64     apply (rule_tac y = "y + 1" in div_prop1)
    65     apply (auto simp add: prems)
    66     done
    67   then show ?thesis by auto
    68 qed
    69 
    70 lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"
    71 proof-
    72   assume "0 < y"
    73   from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
    74   moreover have "0 \<le> x mod y"
    75     by (auto simp add: prems pos_mod_sign)
    76   ultimately show ?thesis
    77     by arith
    78 qed
    79 
    80 
    81 subsection {* Useful properties of congruences *}
    82 
    83 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
    84   by (auto simp add: zcong_def)
    85 
    86 lemma zcong_id: "[m = 0] (mod m)"
    87   by (auto simp add: zcong_def)
    88 
    89 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
    90   by (auto simp add: zcong_refl zcong_zadd)
    91 
    92 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
    93   by (induct z) (auto simp add: zcong_zmult)
    94 
    95 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
    96     [a = d](mod m)"
    97   apply (erule zcong_trans)
    98   apply simp
    99   done
   100 
   101 lemma aux1: "a - b = (c::int) ==> a = c + b"
   102   by auto
   103 
   104 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
   105     [c = b * d] (mod m))"
   106   apply (auto simp add: zcong_def dvd_def)
   107   apply (rule_tac x = "ka + k * d" in exI)
   108   apply (drule aux1)+
   109   apply (auto simp add: int_distrib)
   110   apply (rule_tac x = "ka - k * d" in exI)
   111   apply (drule aux1)+
   112   apply (auto simp add: int_distrib)
   113   done
   114 
   115 lemma zcong_zmult_prop2: "[a = b](mod m) ==>
   116     ([c = d * a](mod m) = [c = d * b] (mod m))"
   117   by (auto simp add: zmult_ac zcong_zmult_prop1)
   118 
   119 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
   120     ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
   121   apply (auto simp add: zcong_def)
   122   apply (drule zprime_zdvd_zmult_better, auto)
   123   done
   124 
   125 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
   126     x < m; y < m |] ==> x = y"
   127   by (metis zcong_not zcong_sym zless_linear)
   128 
   129 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
   130     ~([x = 1] (mod p))"
   131 proof
   132   assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
   133   then have "[1 = -1] (mod p)"
   134     apply (auto simp add: zcong_sym)
   135     apply (drule zcong_trans, auto)
   136     done
   137   then have "[1 + 1 = -1 + 1] (mod p)"
   138     by (simp only: zcong_shift)
   139   then have "[2 = 0] (mod p)"
   140     by auto
   141   then have "p dvd 2"
   142     by (auto simp add: dvd_def zcong_def)
   143   with prems show False
   144     by (auto simp add: zdvd_not_zless)
   145 qed
   146 
   147 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"
   148   by (auto simp add: zcong_def)
   149 
   150 lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==>
   151     [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"
   152   by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
   153 
   154 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
   155   ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"
   156   apply auto
   157   apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
   158   apply auto
   159   done
   160 
   161 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"
   162   by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
   163 
   164 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"
   165   apply (drule order_le_imp_less_or_eq, auto)
   166   apply (frule_tac m = m in zcong_not_zero)
   167   apply auto
   168   done
   169 
   170 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |]
   171     ==> zgcd (setprod id A) y = 1"
   172   by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
   173 
   174 
   175 subsection {* Some properties of MultInv *}
   176 
   177 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
   178     [(MultInv p x) = (MultInv p y)] (mod p)"
   179   by (auto simp add: MultInv_def zcong_zpower)
   180 
   181 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   182   [(x * (MultInv p x)) = 1] (mod p)"
   183 proof (simp add: MultInv_def zcong_eq_zdvd_prop)
   184   assume "2 < p" and "zprime p" and "~ p dvd x"
   185   have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
   186     by auto
   187   also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
   188     by (simp only: nat_add_distrib)
   189   also have "p - 2 + 1 = p - 1" by arith
   190   finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
   191     by (rule ssubst, auto)
   192   also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
   193     by (auto simp add: Little_Fermat)
   194   finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
   195 qed
   196 
   197 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   198     [(MultInv p x) * x = 1] (mod p)"
   199   by (auto simp add: MultInv_prop2 zmult_ac)
   200 
   201 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
   202   by (simp add: nat_diff_distrib)
   203 
   204 lemma aux_2: "2 < p ==> 0 < nat (p - 2)"
   205   by auto
   206 
   207 lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   208     ~([MultInv p x = 0](mod p))"
   209   apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   210   apply (drule aux_2)
   211   apply (drule zpower_zdvd_prop2, auto)
   212   done
   213 
   214 lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
   215     [(MultInv p (MultInv p x)) = (x * (MultInv p x) *
   216       (MultInv p (MultInv p x)))] (mod p)"
   217   apply (drule MultInv_prop2, auto)
   218   apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto)
   219   apply (auto simp add: zcong_sym)
   220   done
   221 
   222 lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
   223     [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)"
   224   apply (frule MultInv_prop3, auto)
   225   apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   226   apply (drule MultInv_prop2, auto)
   227   apply (drule_tac k = x in zcong_scalar2, auto)
   228   apply (auto simp add: zmult_ac)
   229   done
   230 
   231 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   232     [(MultInv p (MultInv p x)) = x] (mod p)"
   233   apply (frule aux__1, auto)
   234   apply (drule aux__2, auto)
   235   apply (drule zcong_trans, auto)
   236   done
   237 
   238 lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p));
   239     ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==>
   240     [x = y] (mod p)"
   241   apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
   242     m = p and k = x in zcong_scalar)
   243   apply (insert MultInv_prop2 [of p x], simp)
   244   apply (auto simp only: zcong_sym [of "MultInv p x * x"])
   245   apply (auto simp add:  zmult_ac)
   246   apply (drule zcong_trans, auto)
   247   apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
   248   apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
   249   apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   250   apply (auto simp add: zcong_sym)
   251   done
   252 
   253 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>
   254     [a * MultInv p j = a * MultInv p k] (mod p)"
   255   by (drule MultInv_prop1, auto simp add: zcong_scalar2)
   256 
   257 lemma aux___1: "[j = a * MultInv p k] (mod p) ==>
   258     [j * k = a * MultInv p k * k] (mod p)"
   259   by (auto simp add: zcong_scalar)
   260 
   261 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p));
   262     [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   263   apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
   264     [of "MultInv p k * k" 1 p "j * k" a])
   265   apply (auto simp add: zmult_ac)
   266   done
   267 
   268 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
   269      (MultInv p j) * a] (mod p)"
   270   by (auto simp add: zmult_assoc zcong_scalar2)
   271 
   272 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
   273     [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   274        ==> [k = a * (MultInv p j)] (mod p)"
   275   apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
   276     [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   277   apply (auto simp add: zmult_ac zcong_sym)
   278   done
   279 
   280 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
   281     ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==>
   282     [k = a * MultInv p j] (mod p)"
   283   apply (drule aux___1)
   284   apply (frule aux___2, auto)
   285   by (drule aux___3, drule aux___4, auto)
   286 
   287 lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p));
   288     ~([k = 0](mod p)); ~([j = 0](mod p));
   289     [a * MultInv p j = a * MultInv p k] (mod p) |] ==>
   290       [j = k] (mod p)"
   291   apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   292   apply (frule zprime_imp_zrelprime, auto)
   293   apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
   294   apply (drule MultInv_prop5, auto)
   295   done
   296 
   297 end