src/HOL/NumberTheory/Int2.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14981 e73f8140af78
child 15392 290bc97038c7
permissions -rw-r--r--
import -> imports
     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 = Finite2 + WilsonRuss:;
     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 [rule_format]: "((0 < n) & (p dvd y)) --> 
    24     p dvd ((y::int) ^ n)";
    25   by (induct_tac 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     apply (insert zdvd_not_zless [of m n])
    32     by (rule contrapos_pn, auto)
    33   then have "(~0 < m | ~m < n)"  by auto
    34   then show ?thesis by auto
    35 qed;
    36 
    37 lemma aux4: " -(m * n) = (-m) * (n::int)";
    38   by auto
    39 
    40 lemma zprime_zdvd_zmult_better: "[| p \<in> zprime;  p dvd (m * n) |] ==> 
    41     (p dvd m) | (p dvd n)";
    42   apply (case_tac "0 \<le> m")
    43   apply (simp add: zprime_zdvd_zmult)
    44   by (insert zprime_zdvd_zmult [of "-m" p n], auto)
    45 
    46 lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n) 
    47     --> 0 < n --> p dvd y";
    48   apply (induct_tac n, auto)
    49   apply (frule zprime_zdvd_zmult_better, auto)
    50 done
    51 
    52 lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y";
    53   by arith
    54 
    55 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
    56 proof -;
    57   assume "0 < z";
    58   then have "(x div z) * z \<le> (x div z) * z + x mod z";
    59   apply (rule_tac x = "x div z * z" in stupid)
    60   by (simp add: pos_mod_sign)
    61   also have "... = x";
    62     by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
    63   also assume  "x < y * z";
    64   finally show ?thesis;
    65     by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
    66 qed;
    67 
    68 lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";
    69 proof -;
    70   assume "0 < z" and "x < (y * z) + z";
    71   then have "x < (y + 1) * z" by (auto simp add: int_distrib)
    72   then have "x div z < y + 1";
    73     by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
    74   then show ?thesis by auto
    75 qed;
    76 
    77 lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)";
    78 proof-;
    79   assume "0 < y";
    80   from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
    81   moreover have "0 \<le> x mod y";
    82     by (auto simp add: prems pos_mod_sign)
    83   ultimately show ?thesis;
    84     by arith
    85 qed;
    86 
    87 (*****************************************************************)
    88 (*                                                               *)
    89 (* Useful properties of congruences                              *)
    90 (*                                                               *)
    91 (*****************************************************************)
    92 
    93 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
    94   by (auto simp add: zcong_def)
    95 
    96 lemma zcong_id: "[m = 0] (mod m)";
    97   by (auto simp add: zcong_def zdvd_0_right)
    98 
    99 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";
   100   by (auto simp add: zcong_refl zcong_zadd)
   101 
   102 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
   103   by (induct_tac z, auto simp add: zcong_zmult)
   104 
   105 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
   106     [a = d](mod m)";
   107   by (auto, rule_tac b = c in zcong_trans)
   108 
   109 lemma aux1: "a - b = (c::int) ==> a = c + b";
   110   by auto
   111 
   112 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
   113     [c = b * d] (mod m))";
   114   apply (auto simp add: zcong_def dvd_def)
   115   apply (rule_tac x = "ka + k * d" in exI)
   116   apply (drule aux1)+;
   117   apply (auto simp add: int_distrib)
   118   apply (rule_tac x = "ka - k * d" in exI)
   119   apply (drule aux1)+;
   120   apply (auto simp add: int_distrib)
   121 done
   122 
   123 lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
   124     ([c = d * a](mod m) = [c = d * b] (mod m))";
   125   by (auto simp add: zmult_ac zcong_zmult_prop1)
   126 
   127 lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p); 
   128     ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
   129   apply (auto simp add: zcong_def)
   130   apply (drule zprime_zdvd_zmult_better, auto)
   131 done
   132 
   133 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
   134     x < m; y < m |] ==> x = y";
   135   apply (simp add: zcong_zmod_eq)
   136   apply (subgoal_tac "(x mod m) = x");
   137   apply (subgoal_tac "(y mod m) = y");
   138   apply simp
   139   apply (rule_tac [1-2] mod_pos_pos_trivial)
   140 by auto
   141 
   142 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
   143     ~([x = 1] (mod p))";
   144 proof;
   145   assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
   146   then have "[1 = -1] (mod p)";
   147     apply (auto simp add: zcong_sym)
   148     apply (drule zcong_trans, auto)
   149   done
   150   then have "[1 + 1 = -1 + 1] (mod p)";
   151     by (simp only: zcong_shift)
   152   then have "[2 = 0] (mod p)";
   153     by auto
   154   then have "p dvd 2";
   155     by (auto simp add: dvd_def zcong_def)
   156   with prems show False;
   157     by (auto simp add: zdvd_not_zless)
   158 qed;
   159 
   160 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
   161   by (auto simp add: zcong_def)
   162 
   163 lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==> 
   164   [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
   165   by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
   166 
   167 lemma zcong_zprime_prod_zero_contra: "[| p \<in> zprime; 0 < a |] ==>
   168   ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
   169   apply auto 
   170   apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
   171 by auto
   172 
   173 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"; 
   174   by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
   175 
   176 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0";
   177   apply (drule order_le_imp_less_or_eq, auto)
   178 by (frule_tac m = m in zcong_not_zero, auto)
   179 
   180 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
   181     ==> zgcd (gsetprod id A,y) = 1";
   182   by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
   183 
   184 (*****************************************************************)
   185 (*                                                               *)
   186 (* Some properties of MultInv                                    *)
   187 (*                                                               *)
   188 (*****************************************************************)
   189 
   190 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
   191     [(MultInv p x) = (MultInv p y)] (mod p)";
   192   by (auto simp add: MultInv_def zcong_zpower)
   193 
   194 lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   195   [(x * (MultInv p x)) = 1] (mod p)";
   196 proof (simp add: MultInv_def zcong_eq_zdvd_prop);
   197   assume "2 < p" and "p \<in> zprime" and "~ p dvd x";
   198   have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
   199     by auto
   200   also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
   201     by (simp only: nat_add_distrib, auto)
   202   also have "p - 2 + 1 = p - 1" by arith
   203   finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
   204     by (rule ssubst, auto)
   205   also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
   206     by (auto simp add: Little_Fermat) 
   207   finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
   208 qed;
   209 
   210 lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   211     [(MultInv p x) * x = 1] (mod p)";
   212   by (auto simp add: MultInv_prop2 zmult_ac)
   213 
   214 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
   215   by (simp add: nat_diff_distrib)
   216 
   217 lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
   218   by auto
   219 
   220 lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   221     ~([MultInv p x = 0](mod p))";
   222   apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   223   apply (drule aux_2)
   224   apply (drule zpower_zdvd_prop2, auto)
   225 done
   226 
   227 lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==> 
   228     [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
   229       (MultInv p (MultInv p x)))] (mod p)";
   230   apply (drule MultInv_prop2, auto)
   231   apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
   232   apply (auto simp add: zcong_sym)
   233 done
   234 
   235 lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
   236     [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
   237   apply (frule MultInv_prop3, auto)
   238   apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   239   apply (drule MultInv_prop2, auto)
   240   apply (drule_tac k = x in zcong_scalar2, auto)
   241   apply (auto simp add: zmult_ac)
   242 done
   243 
   244 lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
   245     [(MultInv p (MultInv p x)) = x] (mod p)";
   246   apply (frule aux__1, auto)
   247   apply (drule aux__2, auto)
   248   apply (drule zcong_trans, auto)
   249 done
   250 
   251 lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
   252     ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
   253     [x = y] (mod p)";
   254   apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
   255     m = p and k = x in zcong_scalar)
   256   apply (insert MultInv_prop2 [of p x], simp)
   257   apply (auto simp only: zcong_sym [of "MultInv p x * x"])
   258   apply (auto simp add:  zmult_ac)
   259   apply (drule zcong_trans, auto)
   260   apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
   261   apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
   262   apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   263   apply (auto simp add: zcong_sym)
   264 done
   265 
   266 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
   267     [a * MultInv p j = a * MultInv p k] (mod p)";
   268   by (drule MultInv_prop1, auto simp add: zcong_scalar2)
   269 
   270 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
   271     [j * k = a * MultInv p k * k] (mod p)";
   272   by (auto simp add: zcong_scalar)
   273 
   274 lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p)); 
   275     [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
   276   apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
   277     [of "MultInv p k * k" 1 p "j * k" a])
   278   apply (auto simp add: zmult_ac)
   279 done
   280 
   281 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
   282      (MultInv p j) * a] (mod p)";
   283   by (auto simp add: zmult_assoc zcong_scalar2)
   284 
   285 lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p)); 
   286     [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   287        ==> [k = a * (MultInv p j)] (mod p)";
   288   apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
   289     [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   290   apply (auto simp add: zmult_ac zcong_sym)
   291 done
   292 
   293 lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p)); 
   294     ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
   295     [k = a * MultInv p j] (mod p)";
   296   apply (drule aux___1)
   297   apply (frule aux___2, auto)
   298   by (drule aux___3, drule aux___4, auto)
   299 
   300 lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p)); 
   301     ~([k = 0](mod p)); ~([j = 0](mod p));
   302     [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
   303       [j = k] (mod p)";
   304   apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   305   apply (frule zprime_imp_zrelprime, auto)
   306   apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
   307   apply (drule MultInv_prop5, auto)
   308 done
   309 
   310 end