wneuper/isa: src/HOL/Old_Number_Theory/Euler.thy@0a54cfc9add3

     1 (*  Title:      HOL/Old_Number_Theory/Euler.thy

     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer

     3 *)

     5 header {* Euler's criterion *}

     7 theory Euler

     8 imports Residues EvenOdd

     9 begin

    11 definition MultInvPair :: "int => int => int => int set"

    12   where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"

    14 definition SetS :: "int => int => int set set"

    15   where "SetS a p = MultInvPair a p ` SRStar p"

    18 subsection {* Property for MultInvPair *}

    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

    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

    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)

    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

    59 lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));

    60                                 ~([j = 0] (mod p));

    61                                 ~(QuadRes p a) |]  ==>

    62                              ~([j = a * MultInv p j] (mod p))"

    63 proof

    64   assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and

    65     "~([j = 0] (mod p))" and "~(QuadRes p a)"

    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: zmult_ac)

    71   have "[j * j = a] (mod p)"

    72     proof -

    73       from prems have b: "[MultInv p j * j = 1] (mod p)"

    74         by (simp add: MultInv_prop2a)

    75       from b a show ?thesis

    76         by (auto simp add: zcong_zmult_prop2)

    77     qed

    78   then have "[j^2 = a] (mod p)"

    79     by (metis  number_of_is_id power2_eq_square succ_bin_simps)

    80   with prems show False

    81     by (simp add: QuadRes_def)

    82 qed

    84 lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p));

    85                                 ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==>

    86                              card (MultInvPair a p j) = 2"

    87   apply (auto simp add: MultInvPair_def)

    88   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")

    89   apply auto

    90   apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one)

    91   done

    94 subsection {* Properties of SetS *}

    96 lemma SetS_finite: "2 < p ==> finite (SetS a p)"

    97   by (auto simp add: SetS_def SRStar_finite [of p])

    99 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"

   100   by (auto simp add: SetS_def MultInvPair_def)

   102 lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p));

   103                         ~(QuadRes p a) |]  ==>

   104                         \<forall>X \<in> SetS a p. card X = 2"

   105   apply (auto simp add: SetS_def)

   106   apply (frule StandardRes_SRStar_prop1a)

   107   apply (rule MultInvPair_card_two, auto)

   108   done

   110 lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"

   111   by (auto simp add: SetS_finite SetS_elems_finite finite_Union)

   113 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);

   114     \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"

   115   by (induct set: finite) auto

   117 lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>

   118                   int(card(SetS a p)) = (p - 1) div 2"

   119 proof -

   120   assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"

   121   then have "(p - 1) = 2 * int(card(SetS a p))"

   122   proof -

   123     have "p - 1 = int(card(Union (SetS a p)))"

   124       by (auto simp add: prems MultInvPair_prop2 SRStar_card)

   125     also have "... = int (setsum card (SetS a p))"

   126       by (auto simp add: prems SetS_finite SetS_elems_finite

   127                          MultInvPair_prop1c [of p a] card_Union_disjoint)

   128     also have "... = int(setsum (%x.2) (SetS a p))"

   129       using prems

   130       by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite

   131         card_setsum_aux simp del: setsum_constant)

   132     also have "... = 2 * int(card( SetS a p))"

   133       by (auto simp add: prems SetS_finite setsum_const2)

   134     finally show ?thesis .

   135   qed

   136   from this show ?thesis

   137     by auto

   138 qed

   140 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));

   141                               ~(QuadRes p a); x \<in> (SetS a p) |] ==>

   142                           [\<Prod>x = a] (mod p)"

   143   apply (auto simp add: SetS_def MultInvPair_def)

   144   apply (frule StandardRes_SRStar_prop1a)

   145   apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")

   146   apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)

   147   apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in

   148     StandardRes_prop4)

   149   apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")

   150   apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and

   151                    b = "x * (a * MultInv p x)" and

   152                    c = "a * (x * MultInv p x)" in  zcong_trans, force)

   153   apply (frule_tac p = p and x = x in MultInv_prop2, auto)

   154 apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)

   155   apply (auto simp add: zmult_ac)

   156   done

   158 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"

   159   by arith

   161 lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"

   162   by auto

   164 lemma d22set_induct_old: "(\<And>a::int. 1 < a \<longrightarrow> P (a - 1) \<Longrightarrow> P a) \<Longrightarrow> P x"

   165 using d22set.induct by blast

   167 lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"

   168   apply (induct p rule: d22set_induct_old)

   169   apply auto

   170   apply (simp add: SRStar_def d22set.simps)

   171   apply (simp add: SRStar_def d22set.simps, clarify)

   172   apply (frule aux1)

   173   apply (frule aux2, auto)

   174   apply (simp_all add: SRStar_def)

   175   apply (simp add: d22set.simps)

   176   apply (frule d22set_le)

   177   apply (frule d22set_g_1, auto)

   178   done

   180 lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>

   181                                  [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"

   182 proof -

   183   assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"

   184   then have "[\<Prod>(Union (SetS a p)) =

   185       setprod (setprod (%x. x)) (SetS a p)] (mod p)"

   186     by (auto simp add: SetS_finite SetS_elems_finite

   187                        MultInvPair_prop1c setprod_Union_disjoint)

   188   also have "[setprod (setprod (%x. x)) (SetS a p) =

   189       setprod (%x. a) (SetS a p)] (mod p)"

   190     by (rule setprod_same_function_zcong)

   191       (auto simp add: prems SetS_setprod_prop SetS_finite)

   192   also (zcong_trans) have "[setprod (%x. a) (SetS a p) =

   193       a^(card (SetS a p))] (mod p)"

   194     by (auto simp add: prems SetS_finite setprod_constant)

   195   finally (zcong_trans) show ?thesis

   196     apply (rule zcong_trans)

   197     apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)

   198     apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)

   199     apply (auto simp add: prems SetS_card)

   200     done

   201 qed

   203 lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>

   204                                     \<Prod>(Union (SetS a p)) = zfact (p - 1)"

   205 proof -

   206   assume "zprime p" and "2 < p" and "~([a = 0](mod p))"

   207   then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"

   208     by (auto simp add: MultInvPair_prop2)

   209   also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"

   210     by (auto simp add: prems SRStar_d22set_prop)

   211   also have "... = zfact(p - 1)"

   212   proof -

   213     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"

   214       by (metis d22set_fin d22set_g_1 linorder_neq_iff)

   215     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"

   216       by auto

   217     then show ?thesis

   218       by (auto simp add: d22set_prod_zfact)

   219   qed

   220   finally show ?thesis .

   221 qed

   223 lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>

   224                    [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"

   225   apply (frule Union_SetS_setprod_prop1)

   226   apply (auto simp add: Union_SetS_setprod_prop2)

   227   done

   229 text {* \medskip Prove the first part of Euler's Criterion: *}

   231 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));

   232     ~(QuadRes p x) |] ==>

   233       [x^(nat (((p) - 1) div 2)) = -1](mod p)"

   234   by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop)

   236 text {* \medskip Prove another part of Euler Criterion: *}

   238 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"

   239 proof -

   240   assume "0 < p"

   241   then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"

   242     by (auto simp add: diff_add_assoc)

   243   also have "... = (a ^ 1) * a ^ (nat(p) - 1)"

   244     by (simp only: zpower_zadd_distrib)

   245   also have "... = a * a ^ (nat(p) - 1)"

   246     by auto

   247   finally show ?thesis .

   248 qed

   250 lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"

   251 proof -

   252   assume "2 < p" and "p \<in> zOdd"

   253   then have "(p - 1):zEven"

   254     by (auto simp add: zEven_def zOdd_def)

   255   then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"

   256     by (auto simp add: even_div_2_prop2)

   257   with `2 < p` have "1 < (p - 1)"

   258     by auto

   259   then have " 1 < (2 * ((p - 1) div 2))"

   260     by (auto simp add: aux_1)

   261   then have "0 < (2 * ((p - 1) div 2)) div 2"

   262     by auto

   263   then show ?thesis by auto

   264 qed

   266 lemma Euler_part2:

   267     "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"

   268   apply (frule zprime_zOdd_eq_grt_2)

   269   apply (frule aux_2, auto)

   270   apply (frule_tac a = a in aux_1, auto)

   271   apply (frule zcong_zmult_prop1, auto)

   272   done

   274 text {* \medskip Prove the final part of Euler's Criterion: *}

   276 lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"

   277   by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)

   279 lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"

   280   by (auto simp add: nat_mult_distrib)

   282 lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==>

   283                       [x^(nat (((p) - 1) div 2)) = 1](mod p)"

   284   apply (subgoal_tac "p \<in> zOdd")

   285   apply (auto simp add: QuadRes_def)

   286    prefer 2

   287    apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2)

   288   apply (frule aux__1, auto)

   289   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)

   290   apply (auto simp add: zpower_zpower)

   291   apply (rule zcong_trans)

   292   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])

   293   apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)

   294   done

   297 text {* \medskip Finally show Euler's Criterion: *}

   299 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =

   300     a^(nat (((p) - 1) div 2))] (mod p)"

   301   apply (auto simp add: Legendre_def Euler_part2)

   302   apply (frule Euler_part3, auto simp add: zcong_sym)[]

   303   apply (frule Euler_part1, auto simp add: zcong_sym)[]

   304   done

   306 end

author	nipkow
	Sun, 28 Nov 2010 15:20:51 +0100
changeset 41030	0a54cfc9add3
parent 38462	e9b4835a54ee
child 41789	1fa4725c4656
permissions	-rw-r--r--