src/HOL/Old_Number_Theory/Euler.thy
changeset 44766 d4d33a4d7548
parent 41541 1fa4725c4656
child 45480 a39bb6d42ace
equal deleted inserted replaced
44765:d96550db3d77 44766:d4d33a4d7548
    65 proof
    65 proof
    66   assume "[j = a * MultInv p j] (mod p)"
    66   assume "[j = a * MultInv p j] (mod p)"
    67   then have "[j * j = (a * MultInv p j) * j] (mod p)"
    67   then have "[j * j = (a * MultInv p j) * j] (mod p)"
    68     by (auto simp add: zcong_scalar)
    68     by (auto simp add: zcong_scalar)
    69   then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
    69   then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
    70     by (auto simp add: zmult_ac)
    70     by (auto simp add: mult_ac)
    71   have "[j * j = a] (mod p)"
    71   have "[j * j = a] (mod p)"
    72   proof -
    72   proof -
    73     from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
    73     from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
    74       by (simp add: MultInv_prop2a)
    74       by (simp add: MultInv_prop2a)
    75     from this and a show ?thesis
    75     from this and a show ?thesis
   146   apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
   146   apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
   147                    b = "x * (a * MultInv p x)" and
   147                    b = "x * (a * MultInv p x)" and
   148                    c = "a * (x * MultInv p x)" in  zcong_trans, force)
   148                    c = "a * (x * MultInv p x)" in  zcong_trans, force)
   149   apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   149   apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   150 apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
   150 apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
   151   apply (auto simp add: zmult_ac)
   151   apply (auto simp add: mult_ac)
   152   done
   152   done
   153 
   153 
   154 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
   154 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
   155   by arith
   155   by arith
   156 
   156 
   235 proof -
   235 proof -
   236   assume "0 < p"
   236   assume "0 < p"
   237   then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
   237   then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
   238     by (auto simp add: diff_add_assoc)
   238     by (auto simp add: diff_add_assoc)
   239   also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
   239   also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
   240     by (simp only: zpower_zadd_distrib)
   240     by (simp only: power_add)
   241   also have "... = a * a ^ (nat(p) - 1)"
   241   also have "... = a * a ^ (nat(p) - 1)"
   242     by auto
   242     by auto
   243   finally show ?thesis .
   243   finally show ?thesis .
   244 qed
   244 qed
   245 
   245 
   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 zmult_1 aux__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)
   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