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