src/HOL/Number_Theory/Gauss.thy
 author eberlm Thu Jul 21 10:06:04 2016 +0200 (2016-07-21) changeset 63534 523b488b15c9 parent 62429 25271ff79171 child 63566 e5abbdee461a permissions -rw-r--r--
Overhaul of prime/multiplicity/prime_factors
```     1 (*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
```
```     2
```
```     3 Ported by lcp but unfinished
```
```     4 *)
```
```     5
```
```     6 section \<open>Gauss' Lemma\<close>
```
```     7
```
```     8 theory Gauss
```
```     9 imports Residues
```
```    10 begin
```
```    11
```
```    12 lemma cong_prime_prod_zero_nat:
```
```    13   fixes a::nat
```
```    14   shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
```
```    15   by (auto simp add: cong_altdef_nat)
```
```    16
```
```    17 lemma cong_prime_prod_zero_int:
```
```    18   fixes a::int
```
```    19   shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
```
```    20   by (auto simp add: cong_altdef_int)
```
```    21
```
```    22
```
```    23 locale GAUSS =
```
```    24   fixes p :: "nat"
```
```    25   fixes a :: "int"
```
```    26
```
```    27   assumes p_prime: "prime p"
```
```    28   assumes p_ge_2: "2 < p"
```
```    29   assumes p_a_relprime: "[a \<noteq> 0](mod p)"
```
```    30   assumes a_nonzero:    "0 < a"
```
```    31 begin
```
```    32
```
```    33 definition "A = {0::int <.. ((int p - 1) div 2)}"
```
```    34 definition "B = (\<lambda>x. x * a) ` A"
```
```    35 definition "C = (\<lambda>x. x mod p) ` B"
```
```    36 definition "D = C \<inter> {.. (int p - 1) div 2}"
```
```    37 definition "E = C \<inter> {(int p - 1) div 2 <..}"
```
```    38 definition "F = (\<lambda>x. (int p - x)) ` E"
```
```    39
```
```    40
```
```    41 subsection \<open>Basic properties of p\<close>
```
```    42
```
```    43 lemma odd_p: "odd p"
```
```    44 by (metis p_prime p_ge_2 prime_odd_nat)
```
```    45
```
```    46 lemma p_minus_one_l: "(int p - 1) div 2 < p"
```
```    47 proof -
```
```    48   have "(p - 1) div 2 \<le> (p - 1) div 1"
```
```    49     by (metis div_by_1 div_le_dividend)
```
```    50   also have "\<dots> = p - 1" by simp
```
```    51   finally show ?thesis using p_ge_2 by arith
```
```    52 qed
```
```    53
```
```    54 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
```
```    55   using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]
```
```    56   by simp
```
```    57
```
```    58 lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
```
```    59   using odd_p p_ge_2
```
```    60   by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
```
```    61
```
```    62
```
```    63 subsection \<open>Basic Properties of the Gauss Sets\<close>
```
```    64
```
```    65 lemma finite_A: "finite (A)"
```
```    66 by (auto simp add: A_def)
```
```    67
```
```    68 lemma finite_B: "finite (B)"
```
```    69 by (auto simp add: B_def finite_A)
```
```    70
```
```    71 lemma finite_C: "finite (C)"
```
```    72 by (auto simp add: C_def finite_B)
```
```    73
```
```    74 lemma finite_D: "finite (D)"
```
```    75 by (auto simp add: D_def finite_C)
```
```    76
```
```    77 lemma finite_E: "finite (E)"
```
```    78 by (auto simp add: E_def finite_C)
```
```    79
```
```    80 lemma finite_F: "finite (F)"
```
```    81 by (auto simp add: F_def finite_E)
```
```    82
```
```    83 lemma C_eq: "C = D \<union> E"
```
```    84 by (auto simp add: C_def D_def E_def)
```
```    85
```
```    86 lemma A_card_eq: "card A = nat ((int p - 1) div 2)"
```
```    87   by (auto simp add: A_def)
```
```    88
```
```    89 lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A"
```
```    90   using a_nonzero by (simp add: A_def inj_on_def)
```
```    91
```
```    92 definition ResSet :: "int => int set => bool"
```
```    93   where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
```
```    94
```
```    95 lemma ResSet_image:
```
```    96   "\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow>
```
```    97     ResSet m (f ` A)"
```
```    98   by (auto simp add: ResSet_def)
```
```    99
```
```   100 lemma A_res: "ResSet p A"
```
```   101   using p_ge_2
```
```   102   by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int)
```
```   103
```
```   104 lemma B_res: "ResSet p B"
```
```   105 proof -
```
```   106   {fix x fix y
```
```   107     assume a: "[x * a = y * a] (mod p)"
```
```   108     assume b: "0 < x"
```
```   109     assume c: "x \<le> (int p - 1) div 2"
```
```   110     assume d: "0 < y"
```
```   111     assume e: "y \<le> (int p - 1) div 2"
```
```   112     from p_a_relprime have "\<not>p dvd a"
```
```   113       by (simp add: cong_altdef_int)
```
```   114     with p_prime have "coprime a (int p)"
```
```   115        by (subst gcd.commute, intro is_prime_imp_coprime) auto
```
```   116     with a cong_mult_rcancel_int [of a "int p" x y]
```
```   117       have "[x = y] (mod p)" by simp
```
```   118     with cong_less_imp_eq_int [of x y p] p_minus_one_l
```
```   119         order_le_less_trans [of x "(int p - 1) div 2" p]
```
```   120         order_le_less_trans [of y "(int p - 1) div 2" p]
```
```   121     have "x = y"
```
```   122       by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
```
```   123     } note xy = this
```
```   124   show ?thesis
```
```   125     apply (insert p_ge_2 p_a_relprime p_minus_one_l)
```
```   126     apply (auto simp add: B_def)
```
```   127     apply (rule ResSet_image)
```
```   128     apply (auto simp add: A_res)
```
```   129     apply (auto simp add: A_def xy)
```
```   130     done
```
```   131   qed
```
```   132
```
```   133 lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
```
```   134 proof -
```
```   135 { fix x fix y
```
```   136   assume a: "x * a mod p = y * a mod p"
```
```   137   assume b: "0 < x"
```
```   138   assume c: "x \<le> (int p - 1) div 2"
```
```   139   assume d: "0 < y"
```
```   140   assume e: "y \<le> (int p - 1) div 2"
```
```   141   assume f: "x \<noteq> y"
```
```   142   from a have a': "[x * a = y * a](mod p)"
```
```   143     by (metis cong_int_def)
```
```   144   from p_a_relprime have "\<not>p dvd a"
```
```   145     by (simp add: cong_altdef_int)
```
```   146   with p_prime have "coprime a (int p)"
```
```   147      by (subst gcd.commute, intro is_prime_imp_coprime) auto
```
```   148   with a' cong_mult_rcancel_int [of a "int p" x y]
```
```   149     have "[x = y] (mod p)" by simp
```
```   150   with cong_less_imp_eq_int [of x y p] p_minus_one_l
```
```   151     order_le_less_trans [of x "(int p - 1) div 2" p]
```
```   152     order_le_less_trans [of y "(int p - 1) div 2" p]
```
```   153   have "x = y"
```
```   154     by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
```
```   155   then have False
```
```   156     by (simp add: f)}
```
```   157   then show ?thesis
```
```   158     by (auto simp add: B_def inj_on_def A_def) metis
```
```   159 qed
```
```   160
```
```   161 lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
```
```   162   apply (auto simp add: E_def C_def B_def A_def)
```
```   163   apply (rule_tac g = "(op - (int p))" in inj_on_inverseI)
```
```   164   apply auto
```
```   165   done
```
```   166
```
```   167 lemma nonzero_mod_p:
```
```   168   fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
```
```   169   by (simp add: cong_int_def)
```
```   170
```
```   171 lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
```
```   172   by (rule nonzero_mod_p) (auto simp add: A_def)
```
```   173
```
```   174 lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x"
```
```   175   by (auto simp add: A_def)
```
```   176
```
```   177 lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
```
```   178   by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int)
```
```   179
```
```   180 lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
```
```   181   using a_nonzero by (auto simp add: B_def A_greater_zero)
```
```   182
```
```   183 lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
```
```   184 proof (auto simp add: C_def)
```
```   185   fix x :: int
```
```   186   assume a1: "x \<in> B"
```
```   187   have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith
```
```   188   have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp
```
```   189   thus "0 < x mod int p" using a1 f2
```
```   190     by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
```
```   191 qed
```
```   192
```
```   193 lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}"
```
```   194   apply (auto simp add: F_def E_def C_def)
```
```   195   apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj)
```
```   196   apply (auto intro: p_odd_int)
```
```   197   done
```
```   198
```
```   199 lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
```
```   200   by (auto simp add: D_def C_greater_zero)
```
```   201
```
```   202 lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}"
```
```   203   by (auto simp add: F_def E_def D_def C_def B_def A_def)
```
```   204
```
```   205 lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}"
```
```   206   by (auto simp add: D_def C_def B_def A_def)
```
```   207
```
```   208 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
```
```   209   using p_prime A_ncong_p [OF assms]
```
```   210   by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime)
```
```   211
```
```   212 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
```
```   213   by (metis id_def all_A_relprime setprod_coprime)
```
```   214
```
```   215
```
```   216 subsection \<open>Relationships Between Gauss Sets\<close>
```
```   217
```
```   218 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
```
```   219   by (auto simp add: ResSet_def inj_on_def cong_int_def)
```
```   220
```
```   221 lemma B_card_eq_A: "card B = card A"
```
```   222   using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
```
```   223
```
```   224 lemma B_card_eq: "card B = nat ((int p - 1) div 2)"
```
```   225   by (simp add: B_card_eq_A A_card_eq)
```
```   226
```
```   227 lemma F_card_eq_E: "card F = card E"
```
```   228   using finite_E
```
```   229   by (simp add: F_def inj_on_pminusx_E card_image)
```
```   230
```
```   231 lemma C_card_eq_B: "card C = card B"
```
```   232 proof -
```
```   233   have "inj_on (\<lambda>x. x mod p) B"
```
```   234     by (metis SR_B_inj)
```
```   235   then show ?thesis
```
```   236     by (metis C_def card_image)
```
```   237 qed
```
```   238
```
```   239 lemma D_E_disj: "D \<inter> E = {}"
```
```   240   by (auto simp add: D_def E_def)
```
```   241
```
```   242 lemma C_card_eq_D_plus_E: "card C = card D + card E"
```
```   243   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
```
```   244
```
```   245 lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
```
```   246   by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute)
```
```   247
```
```   248 lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
```
```   249   apply (auto simp add: C_def)
```
```   250   apply (insert finite_B SR_B_inj)
```
```   251   apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id])
```
```   252   apply auto
```
```   253   apply (rule cong_setprod_int)
```
```   254   apply (auto simp add: cong_int_def)
```
```   255   done
```
```   256
```
```   257 lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
```
```   258   apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset])
```
```   259   apply (auto simp add: A_def)
```
```   260   done
```
```   261
```
```   262 lemma F_D_disj: "(F \<inter> D) = {}"
```
```   263 proof (auto simp add: F_eq D_eq)
```
```   264   fix y::int and z::int
```
```   265   assume "p - (y*a) mod p = (z*a) mod p"
```
```   266   then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
```
```   267     by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
```
```   268   moreover have "[y * a = (y*a) mod p] (mod p)"
```
```   269     by (metis cong_int_def mod_mod_trivial)
```
```   270   ultimately have "[a * (y + z) = 0] (mod p)"
```
```   271     by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
```
```   272   with p_prime a_nonzero p_a_relprime
```
```   273   have a: "[y + z = 0] (mod p)"
```
```   274     by (auto dest!: cong_prime_prod_zero_int)
```
```   275   assume b: "y \<in> A" and c: "z \<in> A"
```
```   276   with A_def have "0 < y + z"
```
```   277     by auto
```
```   278   moreover from b c p_eq2 A_def have "y + z < p"
```
```   279     by auto
```
```   280   ultimately show False
```
```   281     by (metis a nonzero_mod_p)
```
```   282 qed
```
```   283
```
```   284 lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
```
```   285 proof -
```
```   286   have "card (F \<union> D) = card E + card D"
```
```   287     by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E)
```
```   288   then have "card (F \<union> D) = card C"
```
```   289     by (simp add: C_card_eq_D_plus_E)
```
```   290   then show "card (F \<union> D) = nat ((p - 1) div 2)"
```
```   291     by (simp add: C_card_eq_B B_card_eq)
```
```   292 qed
```
```   293
```
```   294 lemma F_Un_D_eq_A: "F \<union> D = A"
```
```   295   using finite_A F_Un_D_subset A_card_eq F_Un_D_card
```
```   296   by (auto simp add: card_seteq)
```
```   297
```
```   298 lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
```
```   299   by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint)
```
```   300
```
```   301 lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
```
```   302 proof -
```
```   303   have FE: "setprod id F = setprod (op - p) E"
```
```   304     apply (auto simp add: F_def)
```
```   305     apply (insert finite_E inj_on_pminusx_E)
```
```   306     apply (drule setprod.reindex, auto)
```
```   307     done
```
```   308   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
```
```   309     by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
```
```   310   then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)"
```
```   311     using finite_E p_ge_2
```
```   312           cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
```
```   313     by auto
```
```   314   then have two: "[setprod id F = setprod (uminus) E](mod p)"
```
```   315     by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1)
```
```   316   have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
```
```   317     using finite_E by (induct set: finite) auto
```
```   318   with two show ?thesis
```
```   319     by simp
```
```   320 qed
```
```   321
```
```   322
```
```   323 subsection \<open>Gauss' Lemma\<close>
```
```   324
```
```   325 lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
```
```   326 by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
```
```   327
```
```   328 theorem pre_gauss_lemma:
```
```   329   "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
```
```   330 proof -
```
```   331   have "[setprod id A = setprod id F * setprod id D](mod p)"
```
```   332     by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong)
```
```   333   then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
```
```   334     apply (rule cong_trans_int)
```
```   335     apply (metis cong_scalar_int prod_F_zcong)
```
```   336     done
```
```   337   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
```
```   338     by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
```
```   339   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
```
```   340     by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
```
```   341   then have "[setprod id A = ((-1)^(card E) *
```
```   342     (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)"
```
```   343     by (simp add: B_def)
```
```   344   then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
```
```   345     (mod p)"
```
```   346     by (simp add: inj_on_xa_A setprod.reindex)
```
```   347   moreover have "setprod (\<lambda>x. x * a) A =
```
```   348     setprod (\<lambda>x. a) A * setprod id A"
```
```   349     using finite_A by (induct set: finite) auto
```
```   350   ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A *
```
```   351     setprod id A))] (mod p)"
```
```   352     by simp
```
```   353   then have "[setprod id A = ((-1)^(card E) * a^(card A) *
```
```   354       setprod id A)](mod p)"
```
```   355     apply (rule cong_trans_int)
```
```   356     apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc)
```
```   357     done
```
```   358   then have a: "[setprod id A * (-1)^(card E) =
```
```   359       ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
```
```   360     by (rule cong_scalar_int)
```
```   361   then have "[setprod id A * (-1)^(card E) = setprod id A *
```
```   362       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
```
```   363     apply (rule cong_trans_int)
```
```   364     apply (simp add: a mult.commute mult.left_commute)
```
```   365     done
```
```   366   then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
```
```   367     apply (rule cong_trans_int)
```
```   368     apply (simp add: aux cong del:setprod.cong)
```
```   369     done
```
```   370   with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
```
```   371     by (metis cong_mult_lcancel_int)
```
```   372   then show ?thesis
```
```   373     by (simp add: A_card_eq cong_sym_int)
```
```   374 qed
```
```   375
```
```   376 (*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's
```
```   377 quite a mess and should better be completely redone.
```
```   378
```
```   379 theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
```
```   380 proof -
```
```   381   from Euler_Criterion p_prime p_ge_2 have
```
```   382       "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
```
```   383     by auto
```
```   384   moreover note pre_gauss_lemma
```
```   385   ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
```
```   386     by (rule cong_trans_int)
```
```   387   moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
```
```   388     by (auto simp add: Legendre_def)
```
```   389   moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
```
```   390     by (rule neg_one_power)
```
```   391   ultimately show ?thesis
```
```   392     by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym)
```
```   393 qed
```
```   394 *)
```
```   395
```
```   396 end
```
```   397
```
```   398 end
```