src/HOL/Old_Number_Theory/Euler.thy
author paulson <lp15@cam.ac.uk>
Fri Nov 13 12:27:13 2015 +0000 (2015-11-13)
changeset 61649 268d88ec9087
parent 61382 efac889fccbc
child 61952 546958347e05
permissions -rw-r--r--
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
     1 (*  Title:      HOL/Old_Number_Theory/Euler.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 section \<open>Euler's criterion\<close>
     6 
     7 theory Euler
     8 imports Residues EvenOdd
     9 begin
    10 
    11 definition MultInvPair :: "int => int => int => int set"
    12   where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
    13 
    14 definition SetS :: "int => int => int set set"
    15   where "SetS a p = MultInvPair a p ` SRStar p"
    16 
    17 
    18 subsection \<open>Property for MultInvPair\<close>
    19 
    20 lemma MultInvPair_prop1a:
    21   "[| zprime p; 2 < p; ~([a = 0](mod p));
    22       X \<in> (SetS a p); Y \<in> (SetS a p);
    23       ~((X \<inter> Y) = {}) |] ==> X = Y"
    24   apply (auto simp add: SetS_def)
    25   apply (drule StandardRes_SRStar_prop1a)+ defer 1
    26   apply (drule StandardRes_SRStar_prop1a)+
    27   apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
    28   apply (drule notE, rule MultInv_zcong_prop1, auto)[]
    29   apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    30   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    31   apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
    32   apply (drule MultInv_zcong_prop1, auto)[]
    33   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    34   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
    35   apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
    36   done
    37 
    38 lemma MultInvPair_prop1b:
    39   "[| zprime p; 2 < p; ~([a = 0](mod p));
    40       X \<in> (SetS a p); Y \<in> (SetS a p);
    41       X \<noteq> Y |] ==> X \<inter> Y = {}"
    42   apply (rule notnotD)
    43   apply (rule notI)
    44   apply (drule MultInvPair_prop1a, auto)
    45   done
    46 
    47 lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
    48     \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
    49   by (auto simp add: MultInvPair_prop1b)
    50 
    51 lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
    52                           Union ( SetS a p) = SRStar p"
    53   apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
    54     SRStar_mult_prop2)
    55   apply (frule StandardRes_SRStar_prop3)
    56   apply (rule bexI, auto)
    57   done
    58 
    59 lemma MultInvPair_distinct:
    60   assumes "zprime p" and "2 < p" and
    61     "~([a = 0] (mod p))" and
    62     "~([j = 0] (mod p))" and
    63     "~(QuadRes p a)"
    64   shows "~([j = a * MultInv p j] (mod p))"
    65 proof
    66   assume "[j = a * MultInv p j] (mod p)"
    67   then have "[j * j = (a * MultInv p j) * j] (mod p)"
    68     by (auto simp add: zcong_scalar)
    69   then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
    70     by (auto simp add: ac_simps)
    71   have "[j * j = a] (mod p)"
    72   proof -
    73     from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
    74       by (simp add: MultInv_prop2a)
    75     from this and a show ?thesis
    76       by (auto simp add: zcong_zmult_prop2)
    77   qed
    78   then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square)
    79   with assms show False by (simp add: QuadRes_def)
    80 qed
    81 
    82 lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
    83                                 ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
    84                              card (MultInvPair a p j) = 2"
    85   apply (auto simp add: MultInvPair_def)
    86   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
    87   apply auto
    88   apply (metis MultInvPair_distinct StandardRes_def aux)
    89   done
    90 
    91 
    92 subsection \<open>Properties of SetS\<close>
    93 
    94 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
    95   by (auto simp add: SetS_def SRStar_finite [of p])
    96 
    97 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
    98   by (auto simp add: SetS_def MultInvPair_def)
    99 
   100 lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
   101                         ~(QuadRes p a) |]  ==>
   102                         \<forall>X \<in> SetS a p. card X = 2"
   103   apply (auto simp add: SetS_def)
   104   apply (frule StandardRes_SRStar_prop1a)
   105   apply (rule MultInvPair_card_two, auto)
   106   done
   107 
   108 lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
   109   by (auto simp add: SetS_finite SetS_elems_finite)
   110 
   111 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
   112     \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
   113   by (induct set: finite) auto
   114 
   115 lemma SetS_card:
   116   assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
   117   shows "int(card(SetS a p)) = (p - 1) div 2"
   118 proof -
   119   have "(p - 1) = 2 * int(card(SetS a p))"
   120   proof -
   121     have "p - 1 = int(card(Union (SetS a p)))"
   122       by (auto simp add: assms MultInvPair_prop2 SRStar_card)
   123     also have "... = int (setsum card (SetS a p))"
   124       by (auto simp add: assms SetS_finite SetS_elems_finite
   125         MultInvPair_prop1c [of p a] card_Union_disjoint)
   126     also have "... = int(setsum (%x.2) (SetS a p))"
   127       using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
   128         card_setsum_aux simp del: setsum_constant)
   129     also have "... = 2 * int(card( SetS a p))"
   130       by (auto simp add: assms SetS_finite setsum_const2)
   131     finally show ?thesis .
   132   qed
   133   then show ?thesis by auto
   134 qed
   135 
   136 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
   137                               ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
   138                           [\<Prod>x = a] (mod p)"
   139   apply (auto simp add: SetS_def MultInvPair_def)
   140   apply (frule StandardRes_SRStar_prop1a)
   141   apply hypsubst_thin
   142   apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
   143   apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
   144   apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
   145     StandardRes_prop4)
   146   apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")
   147   apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
   148                    b = "x * (a * MultInv p x)" and
   149                    c = "a * (x * MultInv p x)" in  zcong_trans, force)
   150   apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   151 apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
   152   apply (auto simp add: ac_simps)
   153   done
   154 
   155 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
   156   by arith
   157 
   158 lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
   159   by auto
   160 
   161 lemma d22set_induct_old: "(\<And>a::int. 1 < a \<longrightarrow> P (a - 1) \<Longrightarrow> P a) \<Longrightarrow> P x"
   162 using d22set.induct by blast
   163 
   164 lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
   165   apply (induct p rule: d22set_induct_old)
   166   apply auto
   167   apply (simp add: SRStar_def d22set.simps)
   168   apply (simp add: SRStar_def d22set.simps, clarify)
   169   apply (frule aux1)
   170   apply (frule aux2, auto)
   171   apply (simp_all add: SRStar_def)
   172   apply (simp add: d22set.simps)
   173   apply (frule d22set_le)
   174   apply (frule d22set_g_1, auto)
   175   done
   176 
   177 lemma Union_SetS_setprod_prop1:
   178   assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
   179     "~(QuadRes p a)"
   180   shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
   181 proof -
   182   from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
   183     by (auto simp add: SetS_finite SetS_elems_finite
   184       MultInvPair_prop1c setprod.Union_disjoint)
   185   also have "[setprod (setprod (%x. x)) (SetS a p) = 
   186       setprod (%x. a) (SetS a p)] (mod p)"
   187     by (rule setprod_same_function_zcong)
   188       (auto simp add: assms SetS_setprod_prop SetS_finite)
   189   also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
   190       a^(card (SetS a p))] (mod p)"
   191     by (auto simp add: assms SetS_finite setprod_constant)
   192   finally (zcong_trans) show ?thesis
   193     apply (rule zcong_trans)
   194     apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
   195     apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
   196     apply (auto simp add: assms SetS_card)
   197     done
   198 qed
   199 
   200 lemma Union_SetS_setprod_prop2:
   201   assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
   202   shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
   203 proof -
   204   from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
   205     by (auto simp add: MultInvPair_prop2)
   206   also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
   207     by (auto simp add: assms SRStar_d22set_prop)
   208   also have "... = zfact(p - 1)"
   209   proof -
   210     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
   211       by (metis d22set_fin d22set_g_1 linorder_neq_iff)
   212     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
   213       by auto
   214     then show ?thesis
   215       by (auto simp add: d22set_prod_zfact)
   216   qed
   217   finally show ?thesis .
   218 qed
   219 
   220 lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
   221                    [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
   222   apply (frule Union_SetS_setprod_prop1) 
   223   apply (auto simp add: Union_SetS_setprod_prop2)
   224   done
   225 
   226 text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
   227 
   228 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   229     ~(QuadRes p x) |] ==> 
   230       [x^(nat (((p) - 1) div 2)) = -1](mod p)"
   231   by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
   232 
   233 text \<open>\medskip Prove another part of Euler Criterion:\<close>
   234 
   235 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
   236 proof -
   237   assume "0 < p"
   238   then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
   239     by (auto simp add: diff_add_assoc)
   240   also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
   241     by (simp only: power_add)
   242   also have "... = a * a ^ (nat(p) - 1)"
   243     by auto
   244   finally show ?thesis .
   245 qed
   246 
   247 lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"
   248 proof -
   249   assume "2 < p" and "p \<in> zOdd"
   250   then have "(p - 1):zEven"
   251     by (auto simp add: zEven_def zOdd_def)
   252   then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
   253     by (auto simp add: even_div_2_prop2)
   254   with \<open>2 < p\<close> have "1 < (p - 1)"
   255     by auto
   256   then have " 1 < (2 * ((p - 1) div 2))"
   257     by (auto simp add: aux_1)
   258   then have "0 < (2 * ((p - 1) div 2)) div 2"
   259     by auto
   260   then show ?thesis by auto
   261 qed
   262 
   263 lemma Euler_part2:
   264     "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
   265   apply (frule zprime_zOdd_eq_grt_2)
   266   apply (frule aux_2, auto)
   267   apply (frule_tac a = a in aux_1, auto)
   268   apply (frule zcong_zmult_prop1, auto)
   269   done
   270 
   271 text \<open>\medskip Prove the final part of Euler's Criterion:\<close>
   272 
   273 lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
   274   by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
   275 
   276 lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
   277   by (auto simp add: nat_mult_distrib)
   278 
   279 lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> 
   280                       [x^(nat (((p) - 1) div 2)) = 1](mod p)"
   281   apply (subgoal_tac "p \<in> zOdd")
   282   apply (auto simp add: QuadRes_def)
   283    prefer 2 
   284    apply (metis zprime_zOdd_eq_grt_2)
   285   apply (frule aux__1, auto)
   286   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
   287   apply (auto simp add: power_mult [symmetric]) 
   288   apply (rule zcong_trans)
   289   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
   290   apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
   291   done
   292 
   293 
   294 text \<open>\medskip Finally show Euler's Criterion:\<close>
   295 
   296 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
   297     a^(nat (((p) - 1) div 2))] (mod p)"
   298   apply (auto simp add: Legendre_def Euler_part2)
   299   apply (frule Euler_part3, auto simp add: zcong_sym)[]
   300   apply (frule Euler_part1, auto simp add: zcong_sym)[]
   301   done
   302 
   303 end