src/HOL/Old_Number_Theory/Euler.thy
 changeset 45480 a39bb6d42ace parent 44766 d4d33a4d7548 child 53077 a1b3784f8129
equal inserted replaced
45477:11d9c2768729 45480:a39bb6d42ace
`    83                                 ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> `
`    83                                 ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> `
`    84                              card (MultInvPair a p j) = 2"`
`    84                              card (MultInvPair a p j) = 2"`
`    85   apply (auto simp add: MultInvPair_def)`
`    85   apply (auto simp add: MultInvPair_def)`
`    86   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")`
`    86   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")`
`    87   apply auto`
`    87   apply auto`
`    88   apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one)`
`    88   apply (metis MultInvPair_distinct StandardRes_def aux)`
`    89   done`
`    89   done`
`    90 `
`    90 `
`    91 `
`    91 `
`    92 subsection {* Properties of SetS *}`
`    92 subsection {* Properties of SetS *}`
`    93 `
`    93 `
`   225 text {* \medskip Prove the first part of Euler's Criterion: *}`
`   225 text {* \medskip Prove the first part of Euler's Criterion: *}`
`   226 `
`   226 `
`   227 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); `
`   227 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); `
`   228     ~(QuadRes p x) |] ==> `
`   228     ~(QuadRes p x) |] ==> `
`   229       [x^(nat (((p) - 1) div 2)) = -1](mod p)"`
`   229       [x^(nat (((p) - 1) div 2)) = -1](mod p)"`
`   230   by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop)`
`   230   by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)`
`   231 `
`   231 `
`   232 text {* \medskip Prove another part of Euler Criterion: *}`
`   232 text {* \medskip Prove another part of Euler Criterion: *}`
`   233 `
`   233 `
`   234 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"`
`   234 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"`
`   235 proof -`
`   235 proof -`
`   278 lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> `
`   278 lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> `
`   279                       [x^(nat (((p) - 1) div 2)) = 1](mod p)"`
`   279                       [x^(nat (((p) - 1) div 2)) = 1](mod p)"`
`   280   apply (subgoal_tac "p \<in> zOdd")`
`   280   apply (subgoal_tac "p \<in> zOdd")`
`   281   apply (auto simp add: QuadRes_def)`
`   281   apply (auto simp add: QuadRes_def)`
`   282    prefer 2 `
`   282    prefer 2 `
`   283    apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2)`
`   283    apply (metis zprime_zOdd_eq_grt_2)`
`   284   apply (frule aux__1, auto)`
`   284   apply (frule aux__1, auto)`
`   285   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)`
`   285   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)`
`   286   apply (auto simp add: zpower_zpower) `
`   286   apply (auto simp add: zpower_zpower) `
`   287   apply (rule zcong_trans)`
`   287   apply (rule zcong_trans)`
`   288   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])`
`   288   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])`
`   289   apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one mult_1 aux__2)`
`   289   apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)`
`   290   done`
`   290   done`
`   291 `
`   291 `
`   292 `
`   292 `
`   293 text {* \medskip Finally show Euler's Criterion: *}`
`   293 text {* \medskip Finally show Euler's Criterion: *}`
`   294 `
`   294 `