wenzelm@38159: (* Title: HOL/Old_Number_Theory/Euler.thy paulson@13871: Authors: Jeremy Avigad, David Gray, and Adam Kramer paulson@13871: *) paulson@13871: wenzelm@58889: section {* Euler's criterion *} paulson@13871: wenzelm@38159: theory Euler wenzelm@38159: imports Residues EvenOdd wenzelm@38159: begin paulson@13871: wenzelm@38159: definition MultInvPair :: "int => int => int => int set" wenzelm@38159: where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}" wenzelm@19670: wenzelm@38159: definition SetS :: "int => int => int set set" wenzelm@38159: where "SetS a p = MultInvPair a p ` SRStar p" paulson@13871: wenzelm@19670: wenzelm@19670: subsection {* Property for MultInvPair *} paulson@13871: wenzelm@19670: lemma MultInvPair_prop1a: wenzelm@19670: "[| zprime p; 2 < p; ~([a = 0](mod p)); wenzelm@19670: X \ (SetS a p); Y \ (SetS a p); wenzelm@19670: ~((X \ Y) = {}) |] ==> X = Y" paulson@13871: apply (auto simp add: SetS_def) wenzelm@16974: apply (drule StandardRes_SRStar_prop1a)+ defer 1 wenzelm@16974: apply (drule StandardRes_SRStar_prop1a)+ paulson@13871: apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym) wenzelm@20369: apply (drule notE, rule MultInv_zcong_prop1, auto)[] wenzelm@20369: apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[] wenzelm@20369: apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] wenzelm@20369: apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[] wenzelm@20369: apply (drule MultInv_zcong_prop1, auto)[] wenzelm@20369: apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] wenzelm@20369: apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] wenzelm@20369: apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[] wenzelm@19670: done paulson@13871: wenzelm@19670: lemma MultInvPair_prop1b: wenzelm@19670: "[| zprime p; 2 < p; ~([a = 0](mod p)); wenzelm@19670: X \ (SetS a p); Y \ (SetS a p); wenzelm@19670: X \ Y |] ==> X \ Y = {}" paulson@13871: apply (rule notnotD) paulson@13871: apply (rule notI) paulson@13871: apply (drule MultInvPair_prop1a, auto) wenzelm@19670: done paulson@13871: nipkow@16663: lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> paulson@13871: \X \ SetS a p. \Y \ SetS a p. X \ Y --> X\Y = {}" paulson@13871: by (auto simp add: MultInvPair_prop1b) paulson@13871: nipkow@16663: lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> wenzelm@16974: Union ( SetS a p) = SRStar p" paulson@13871: apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 paulson@13871: SRStar_mult_prop2) paulson@13871: apply (frule StandardRes_SRStar_prop3) paulson@13871: apply (rule bexI, auto) wenzelm@19670: done paulson@13871: wenzelm@41541: lemma MultInvPair_distinct: wenzelm@41541: assumes "zprime p" and "2 < p" and wenzelm@41541: "~([a = 0] (mod p))" and wenzelm@41541: "~([j = 0] (mod p))" and wenzelm@41541: "~(QuadRes p a)" wenzelm@41541: shows "~([j = a * MultInv p j] (mod p))" wenzelm@20369: proof wenzelm@16974: assume "[j = a * MultInv p j] (mod p)" wenzelm@16974: then have "[j * j = (a * MultInv p j) * j] (mod p)" paulson@13871: by (auto simp add: zcong_scalar) wenzelm@16974: then have a:"[j * j = a * (MultInv p j * j)] (mod p)" haftmann@57514: by (auto simp add: ac_simps) wenzelm@16974: have "[j * j = a] (mod p)" wenzelm@41541: proof - wenzelm@41541: from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)" wenzelm@41541: by (simp add: MultInv_prop2a) wenzelm@41541: from this and a show ?thesis wenzelm@41541: by (auto simp add: zcong_zmult_prop2) wenzelm@41541: qed wenzelm@53077: then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square) wenzelm@41541: with assms show False by (simp add: QuadRes_def) wenzelm@16974: qed paulson@13871: nipkow@16663: lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); paulson@13871: ~(QuadRes p a); ~([j = 0] (mod p)) |] ==> wenzelm@16974: card (MultInvPair a p j) = 2" paulson@13871: apply (auto simp add: MultInvPair_def) wenzelm@16974: apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))") paulson@13871: apply auto huffman@45480: apply (metis MultInvPair_distinct StandardRes_def aux) wenzelm@20369: done paulson@13871: wenzelm@19670: wenzelm@19670: subsection {* Properties of SetS *} paulson@13871: wenzelm@16974: lemma SetS_finite: "2 < p ==> finite (SetS a p)" nipkow@40786: by (auto simp add: SetS_def SRStar_finite [of p]) paulson@13871: wenzelm@16974: lemma SetS_elems_finite: "\X \ SetS a p. finite X" paulson@13871: by (auto simp add: SetS_def MultInvPair_def) paulson@13871: nipkow@16663: lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); paulson@13871: ~(QuadRes p a) |] ==> wenzelm@16974: \X \ SetS a p. card X = 2" paulson@13871: apply (auto simp add: SetS_def) paulson@13871: apply (frule StandardRes_SRStar_prop1a) paulson@13871: apply (rule MultInvPair_card_two, auto) wenzelm@19670: done paulson@13871: wenzelm@16974: lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))" wenzelm@41541: by (auto simp add: SetS_finite SetS_elems_finite) paulson@13871: paulson@13871: lemma card_setsum_aux: "[| finite S; \X \ S. finite (X::int set); wenzelm@16974: \X \ S. card X = n |] ==> setsum card S = setsum (%x. n) S" berghofe@22274: by (induct set: finite) auto paulson@13871: wenzelm@41541: lemma SetS_card: wenzelm@41541: assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" wenzelm@41541: shows "int(card(SetS a p)) = (p - 1) div 2" wenzelm@16974: proof - wenzelm@41541: have "(p - 1) = 2 * int(card(SetS a p))" wenzelm@16974: proof - wenzelm@16974: have "p - 1 = int(card(Union (SetS a p)))" wenzelm@41541: by (auto simp add: assms MultInvPair_prop2 SRStar_card) wenzelm@16974: also have "... = int (setsum card (SetS a p))" wenzelm@41541: by (auto simp add: assms SetS_finite SetS_elems_finite wenzelm@41541: MultInvPair_prop1c [of p a] card_Union_disjoint) wenzelm@16974: also have "... = int(setsum (%x.2) (SetS a p))" wenzelm@41541: using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite paulson@15047: card_setsum_aux simp del: setsum_constant) wenzelm@16974: also have "... = 2 * int(card( SetS a p))" wenzelm@41541: by (auto simp add: assms SetS_finite setsum_const2) wenzelm@16974: finally show ?thesis . wenzelm@16974: qed wenzelm@41541: then show ?thesis by auto wenzelm@16974: qed paulson@13871: nipkow@16663: lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); paulson@13871: ~(QuadRes p a); x \ (SetS a p) |] ==> wenzelm@16974: [\x = a] (mod p)" paulson@13871: apply (auto simp add: SetS_def MultInvPair_def) paulson@13871: apply (frule StandardRes_SRStar_prop1a) thomas@57492: apply hypsubst_thin wenzelm@16974: apply (subgoal_tac "StandardRes p x \ StandardRes p (a * MultInv p x)") paulson@13871: apply (auto simp add: StandardRes_prop2 MultInvPair_distinct) paulson@13871: apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in wenzelm@16974: StandardRes_prop4) wenzelm@16974: apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)") paulson@13871: apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and paulson@13871: b = "x * (a * MultInv p x)" and wenzelm@16974: c = "a * (x * MultInv p x)" in zcong_trans, force) paulson@13871: apply (frule_tac p = p and x = x in MultInv_prop2, auto) haftmann@57512: apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1) haftmann@57514: apply (auto simp add: ac_simps) wenzelm@19670: done paulson@13871: wenzelm@16974: lemma aux1: "[| 0 < x; (x::int) < a; x \ (a - 1) |] ==> x < a - 1" paulson@13871: by arith paulson@13871: wenzelm@16974: lemma aux2: "[| (a::int) < c; b < c |] ==> (a \ b | b \ a)" paulson@13871: by auto paulson@13871: krauss@35544: lemma d22set_induct_old: "(\a::int. 1 < a \ P (a - 1) \ P a) \ P x" krauss@35544: using d22set.induct by blast krauss@35544: wenzelm@18369: lemma SRStar_d22set_prop: "2 < p \ (SRStar p) = {1} \ (d22set (p - 1))" krauss@35544: apply (induct p rule: d22set_induct_old) wenzelm@18369: apply auto nipkow@16733: apply (simp add: SRStar_def d22set.simps) paulson@13871: apply (simp add: SRStar_def d22set.simps, clarify) paulson@13871: apply (frule aux1) paulson@13871: apply (frule aux2, auto) paulson@13871: apply (simp_all add: SRStar_def) paulson@13871: apply (simp add: d22set.simps) paulson@13871: apply (frule d22set_le) paulson@13871: apply (frule d22set_g_1, auto) wenzelm@18369: done paulson@13871: wenzelm@41541: lemma Union_SetS_setprod_prop1: wenzelm@41541: assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and wenzelm@41541: "~(QuadRes p a)" wenzelm@41541: shows "[\(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)" nipkow@15392: proof - wenzelm@41541: from assms have "[\(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)" paulson@13871: by (auto simp add: SetS_finite SetS_elems_finite haftmann@57418: MultInvPair_prop1c setprod.Union_disjoint) nipkow@15392: also have "[setprod (setprod (%x. x)) (SetS a p) = nipkow@15392: setprod (%x. a) (SetS a p)] (mod p)" wenzelm@18369: by (rule setprod_same_function_zcong) wenzelm@41541: (auto simp add: assms SetS_setprod_prop SetS_finite) nipkow@15392: also (zcong_trans) have "[setprod (%x. a) (SetS a p) = nipkow@15392: a^(card (SetS a p))] (mod p)" wenzelm@41541: by (auto simp add: assms SetS_finite setprod_constant) nipkow@15392: finally (zcong_trans) show ?thesis paulson@13871: apply (rule zcong_trans) nipkow@15392: apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto) nipkow@15392: apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force) wenzelm@41541: apply (auto simp add: assms SetS_card) wenzelm@18369: done nipkow@15392: qed paulson@13871: wenzelm@41541: lemma Union_SetS_setprod_prop2: wenzelm@41541: assumes "zprime p" and "2 < p" and "~([a = 0](mod p))" wenzelm@41541: shows "\(Union (SetS a p)) = zfact (p - 1)" wenzelm@16974: proof - wenzelm@41541: from assms have "\(Union (SetS a p)) = \(SRStar p)" paulson@13871: by (auto simp add: MultInvPair_prop2) nipkow@15392: also have "... = \({1} \ (d22set (p - 1)))" wenzelm@41541: by (auto simp add: assms SRStar_d22set_prop) nipkow@15392: also have "... = zfact(p - 1)" nipkow@15392: proof - wenzelm@18369: have "~(1 \ d22set (p - 1)) & finite( d22set (p - 1))" paulson@25760: by (metis d22set_fin d22set_g_1 linorder_neq_iff) wenzelm@18369: then have "\({1} \ (d22set (p - 1))) = \(d22set (p - 1))" wenzelm@18369: by auto wenzelm@18369: then show ?thesis wenzelm@18369: by (auto simp add: d22set_prod_zfact) wenzelm@16974: qed nipkow@15392: finally show ?thesis . wenzelm@16974: qed paulson@13871: nipkow@16663: lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> wenzelm@16974: [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)" paulson@13871: apply (frule Union_SetS_setprod_prop1) paulson@13871: apply (auto simp add: Union_SetS_setprod_prop2) wenzelm@18369: done paulson@13871: wenzelm@19670: text {* \medskip Prove the first part of Euler's Criterion: *} paulson@13871: nipkow@16663: lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); paulson@13871: ~(QuadRes p x) |] ==> wenzelm@16974: [x^(nat (((p) - 1) div 2)) = -1](mod p)" huffman@45480: by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop) paulson@13871: wenzelm@19670: text {* \medskip Prove another part of Euler Criterion: *} paulson@13871: wenzelm@16974: lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)" wenzelm@16974: proof - wenzelm@16974: assume "0 < p" wenzelm@16974: then have "a ^ (nat p) = a ^ (1 + (nat p - 1))" paulson@13871: by (auto simp add: diff_add_assoc) wenzelm@16974: also have "... = (a ^ 1) * a ^ (nat(p) - 1)" huffman@44766: by (simp only: power_add) wenzelm@16974: also have "... = a * a ^ (nat(p) - 1)" paulson@13871: by auto wenzelm@16974: finally show ?thesis . wenzelm@16974: qed paulson@13871: wenzelm@16974: lemma aux_2: "[| (2::int) < p; p \ zOdd |] ==> 0 < ((p - 1) div 2)" wenzelm@16974: proof - wenzelm@16974: assume "2 < p" and "p \ zOdd" wenzelm@16974: then have "(p - 1):zEven" paulson@13871: by (auto simp add: zEven_def zOdd_def) wenzelm@16974: then have aux_1: "2 * ((p - 1) div 2) = (p - 1)" paulson@13871: by (auto simp add: even_div_2_prop2) wenzelm@23373: with `2 < p` have "1 < (p - 1)" paulson@13871: by auto wenzelm@16974: then have " 1 < (2 * ((p - 1) div 2))" paulson@13871: by (auto simp add: aux_1) wenzelm@16974: then have "0 < (2 * ((p - 1) div 2)) div 2" paulson@13871: by auto paulson@13871: then show ?thesis by auto wenzelm@16974: qed paulson@13871: wenzelm@19670: lemma Euler_part2: wenzelm@19670: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)" paulson@13871: apply (frule zprime_zOdd_eq_grt_2) paulson@13871: apply (frule aux_2, auto) paulson@13871: apply (frule_tac a = a in aux_1, auto) paulson@13871: apply (frule zcong_zmult_prop1, auto) wenzelm@18369: done paulson@13871: wenzelm@19670: text {* \medskip Prove the final part of Euler's Criterion: *} paulson@13871: wenzelm@53077: lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)" nipkow@30042: by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans) paulson@13871: wenzelm@16974: lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))" paulson@13871: by (auto simp add: nat_mult_distrib) paulson@13871: nipkow@16663: lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> wenzelm@16974: [x^(nat (((p) - 1) div 2)) = 1](mod p)" paulson@13871: apply (subgoal_tac "p \ zOdd") paulson@13871: apply (auto simp add: QuadRes_def) paulson@25675: prefer 2 huffman@45480: apply (metis zprime_zOdd_eq_grt_2) paulson@13871: apply (frule aux__1, auto) wenzelm@16974: apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower) paulson@25675: apply (auto simp add: zpower_zpower) paulson@13871: apply (rule zcong_trans) wenzelm@16974: apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]) huffman@45480: apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2) wenzelm@18369: done paulson@13871: wenzelm@19670: wenzelm@19670: text {* \medskip Finally show Euler's Criterion: *} paulson@13871: nipkow@16663: theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) = wenzelm@16974: a^(nat (((p) - 1) div 2))] (mod p)" paulson@13871: apply (auto simp add: Legendre_def Euler_part2) wenzelm@20369: apply (frule Euler_part3, auto simp add: zcong_sym)[] wenzelm@20369: apply (frule Euler_part1, auto simp add: zcong_sym)[] wenzelm@18369: done paulson@13871: wenzelm@18369: end