src/HOL/Number_Theory/Gauss.thy
author nipkow
Sat Apr 12 17:26:27 2014 +0200 (2014-04-12)
changeset 56544 b60d5d119489
parent 55730 97ff9276e12d
child 57418 6ab1c7cb0b8d
permissions -rw-r--r--
made mult_pos_pos a simp rule
     1 (*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     2 
     3 Ported by lcp but unfinished
     4 *)
     5 
     6 header {* Gauss' Lemma *}
     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 {* Basic properties of p *}
    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 auto presburger
    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_def) (metis p_eq2)
    61 
    62 
    63 subsection {* Basic Properties of the Gauss Sets *}
    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 a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
   113     have "[x = y](mod p)"
   114       by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
   115                 cong_mult_self_int gcd_int.commute prime_imp_coprime_int)
   116     with cong_less_imp_eq_int [of x y p] p_minus_one_l
   117         order_le_less_trans [of x "(int p - 1) div 2" p]
   118         order_le_less_trans [of y "(int p - 1) div 2" p] 
   119     have "x = y"
   120       by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
   121     } note xy = this
   122   show ?thesis
   123     apply (insert p_ge_2 p_a_relprime p_minus_one_l)
   124     apply (auto simp add: B_def)
   125     apply (rule ResSet_image)
   126     apply (auto simp add: A_res)
   127     apply (auto simp add: A_def xy)
   128     done
   129   qed
   130 
   131 lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
   132 proof -
   133 { fix x fix y
   134   assume a: "x * a mod p = y * a mod p"
   135   assume b: "0 < x"
   136   assume c: "x \<le> (int p - 1) div 2"
   137   assume d: "0 < y"
   138   assume e: "y \<le> (int p - 1) div 2"
   139   assume f: "x \<noteq> y"
   140   from a have "[x * a = y * a](mod p)" 
   141     by (metis cong_int_def)
   142   with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
   143   have "[x = y](mod p)" 
   144     by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int)
   145   with cong_less_imp_eq_int [of x y p] p_minus_one_l
   146     order_le_less_trans [of x "(int p - 1) div 2" p]
   147     order_le_less_trans [of y "(int p - 1) div 2" p] 
   148   have "x = y"
   149     by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
   150   then have False
   151     by (simp add: f)}
   152   then show ?thesis
   153     by (auto simp add: B_def inj_on_def A_def) metis
   154 qed
   155 
   156 lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
   157   apply (auto simp add: E_def C_def B_def A_def)
   158   apply (rule_tac g = "(op - (int p))" in inj_on_inverseI)
   159   apply auto
   160   done
   161 
   162 lemma nonzero_mod_p:
   163   fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
   164 by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int 
   165      inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int)
   166 
   167 lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
   168   by (rule nonzero_mod_p) (auto simp add: A_def)
   169 
   170 lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x"
   171   by (auto simp add: A_def)
   172 
   173 lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
   174   by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
   175 
   176 lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
   177   using a_nonzero by (auto simp add: B_def A_greater_zero)
   178 
   179 lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
   180 proof (auto simp add: C_def)
   181   fix x :: int
   182   assume a1: "x \<in> B"
   183   have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith
   184   have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp
   185   thus "0 < x mod int p" using a1 f2 
   186     by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
   187 qed
   188 
   189 lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}"
   190   apply (auto simp add: F_def E_def C_def)
   191   apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj)
   192   apply (auto intro: p_odd_int)
   193   done
   194 
   195 lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   196   by (auto simp add: D_def C_greater_zero)
   197 
   198 lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}"
   199   by (auto simp add: F_def E_def D_def C_def B_def A_def)
   200 
   201 lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}"
   202   by (auto simp add: D_def C_def B_def A_def)
   203 
   204 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
   205   using p_prime A_ncong_p [OF assms]
   206   by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
   207 
   208 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
   209   by (metis DEADID.map_id all_A_relprime setprod_coprime_int)
   210 
   211 
   212 subsection {* Relationships Between Gauss Sets *}
   213 
   214 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
   215   by (auto simp add: ResSet_def inj_on_def cong_int_def)
   216 
   217 lemma B_card_eq_A: "card B = card A"
   218   using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   219 
   220 lemma B_card_eq: "card B = nat ((int p - 1) div 2)"
   221   by (simp add: B_card_eq_A A_card_eq)
   222 
   223 lemma F_card_eq_E: "card F = card E"
   224   using finite_E 
   225   by (simp add: F_def inj_on_pminusx_E card_image)
   226 
   227 lemma C_card_eq_B: "card C = card B"
   228 proof -
   229   have "inj_on (\<lambda>x. x mod p) B"
   230     by (metis SR_B_inj) 
   231   then show ?thesis
   232     by (metis C_def card_image)
   233 qed
   234 
   235 lemma D_E_disj: "D \<inter> E = {}"
   236   by (auto simp add: D_def E_def)
   237 
   238 lemma C_card_eq_D_plus_E: "card C = card D + card E"
   239   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   240 
   241 lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   242   by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod_Un_disjoint sup_commute)
   243 
   244 lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   245   apply (auto simp add: C_def)
   246   apply (insert finite_B SR_B_inj)
   247   apply (frule_tac f = "\<lambda>x. x mod int p" in setprod_reindex_id [symmetric], auto)
   248   apply (rule cong_setprod_int)
   249   apply (auto simp add: cong_int_def)
   250   done
   251 
   252 lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   253   apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset])
   254   apply (auto simp add: A_def)
   255   done
   256 
   257 lemma F_D_disj: "(F \<inter> D) = {}"
   258 proof (auto simp add: F_eq D_eq)
   259   fix y::int and z::int
   260   assume "p - (y*a) mod p = (z*a) mod p"
   261   then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
   262     by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
   263   moreover have "[y * a = (y*a) mod p] (mod p)"
   264     by (metis cong_int_def mod_mod_trivial)
   265   ultimately have "[a * (y + z) = 0] (mod p)"
   266     by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1))
   267   with p_prime a_nonzero p_a_relprime
   268   have a: "[y + z = 0] (mod p)"
   269     by (metis cong_prime_prod_zero_int)
   270   assume b: "y \<in> A" and c: "z \<in> A"
   271   with A_def have "0 < y + z"
   272     by auto
   273   moreover from b c p_eq2 A_def have "y + z < p"
   274     by auto
   275   ultimately show False
   276     by (metis a nonzero_mod_p)
   277 qed
   278 
   279 lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   280 proof -
   281   have "card (F \<union> D) = card E + card D"
   282     by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E)
   283   then have "card (F \<union> D) = card C"
   284     by (simp add: C_card_eq_D_plus_E)
   285   then show "card (F \<union> D) = nat ((p - 1) div 2)"
   286     by (simp add: C_card_eq_B B_card_eq)
   287 qed
   288 
   289 lemma F_Un_D_eq_A: "F \<union> D = A"
   290   using finite_A F_Un_D_subset A_card_eq F_Un_D_card 
   291   by (auto simp add: card_seteq)
   292 
   293 lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
   294   by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod_Un_disjoint)
   295 
   296 lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   297 proof -
   298   have FE: "setprod id F = setprod (op - p) E"
   299     apply (auto simp add: F_def)
   300     apply (insert finite_E inj_on_pminusx_E)
   301     apply (frule setprod_reindex_id, auto)
   302     done
   303   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
   304     by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
   305   then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)"
   306     using finite_E p_ge_2
   307           cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
   308     by auto
   309   then have two: "[setprod id F = setprod (uminus) E](mod p)"
   310     by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1)
   311   have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   312     using finite_E by (induct set: finite) auto
   313   with two show ?thesis
   314     by simp
   315 qed
   316 
   317 
   318 subsection {* Gauss' Lemma *}
   319 
   320 lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   321 by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one)
   322 
   323 theorem pre_gauss_lemma:
   324   "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   325 proof -
   326   have "[setprod id A = setprod id F * setprod id D](mod p)"
   327     by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
   328   then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
   329     apply (rule cong_trans_int)
   330     apply (metis cong_scalar_int prod_F_zcong)
   331     done
   332   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   333     by (metis C_prod_eq_D_times_E mult_commute mult_left_commute)
   334   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   335     by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
   336   then have "[setprod id A = ((-1)^(card E) *
   337     (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)"
   338     by (simp add: B_def)
   339   then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
   340     (mod p)"
   341     by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
   342   moreover have "setprod (\<lambda>x. x * a) A =
   343     setprod (\<lambda>x. a) A * setprod id A"
   344     using finite_A by (induct set: finite) auto
   345   ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A *
   346     setprod id A))] (mod p)"
   347     by simp
   348   then have "[setprod id A = ((-1)^(card E) * a^(card A) *
   349       setprod id A)](mod p)"
   350     apply (rule cong_trans_int)
   351     apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc)
   352     done
   353   then have a: "[setprod id A * (-1)^(card E) =
   354       ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   355     by (rule cong_scalar_int)
   356   then have "[setprod id A * (-1)^(card E) = setprod id A *
   357       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   358     apply (rule cong_trans_int)
   359     apply (simp add: a mult_commute mult_left_commute)
   360     done
   361   then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
   362     apply (rule cong_trans_int)
   363     apply (simp add: aux cong del:setprod_cong)
   364     done
   365   with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   366     by (metis cong_mult_lcancel_int)
   367   then show ?thesis
   368     by (simp add: A_card_eq cong_sym_int)
   369 qed
   370 
   371 (*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's
   372 quite a mess and should better be completely redone.
   373 
   374 theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   375 proof -
   376   from Euler_Criterion p_prime p_ge_2 have
   377       "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   378     by auto
   379   moreover note pre_gauss_lemma
   380   ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
   381     by (rule cong_trans_int)
   382   moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
   383     by (auto simp add: Legendre_def)
   384   moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
   385     by (rule neg_one_power)
   386   ultimately show ?thesis
   387     by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym)
   388 qed
   389 *)
   390 
   391 end
   392 
   393 end