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