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