src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 61694 6571c78c9667
parent 61649 268d88ec9087
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -29,7 +29,7 @@
     1.4  text \<open>\medskip @{term [source] inv}\<close>
     1.5  
     1.6  lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
     1.7 -  by (subst int_int_eq [symmetric]) auto
     1.8 +  by simp
     1.9  
    1.10  lemma inv_is_inv:
    1.11      "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
    1.12 @@ -38,10 +38,7 @@
    1.13    apply (subst mod_mult_right_eq [symmetric])
    1.14    apply (subst zcong_zmod [symmetric])
    1.15    apply (subst power_Suc [symmetric])
    1.16 -  apply (subst inv_is_inv_aux)
    1.17 -   apply (erule_tac [2] Little_Fermat)
    1.18 -   apply (erule_tac [2] zdvd_not_zless)
    1.19 -   apply (unfold zprime_def, auto)
    1.20 +  using Little_Fermat inv_is_inv_aux zdvd_not_zless apply auto
    1.21    done
    1.22  
    1.23  lemma inv_distinct:
    1.24 @@ -116,8 +113,7 @@
    1.25  
    1.26  lemma inv_inv_aux: "5 \<le> p ==>
    1.27      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
    1.28 -  apply (subst int_int_eq [symmetric])
    1.29 -  apply (simp add: of_nat_mult)
    1.30 +  apply (subst of_nat_eq_iff [where 'a = int, symmetric])
    1.31    apply (simp add: left_diff_distrib right_diff_distrib)
    1.32    done
    1.33