src/HOL/Old_Number_Theory/WilsonBij.thy
changeset 35048 82ab78fff970
parent 32960 69916a850301
child 38159 e9b4835a54ee
equal deleted inserted replaced
35047:1b2bae06c796 35048:82ab78fff970
    72   done
    72   done
    73 
    73 
    74 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    74 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    75   -- {* same as @{text WilsonRuss} *}
    75   -- {* same as @{text WilsonRuss} *}
    76   apply (unfold zcong_def)
    76   apply (unfold zcong_def)
    77   apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
    77   apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
    78   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    78   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    79    apply (simp add: mult_commute)
    79    apply (simp add: algebra_simps)
    80   apply (subst dvd_minus_iff)
    80   apply (subst dvd_minus_iff)
    81   apply (subst zdvd_reduce)
    81   apply (subst zdvd_reduce)
    82   apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
    82   apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
    83    apply (subst zdvd_reduce)
    83    apply (subst zdvd_reduce)
    84    apply auto
    84    apply auto