src/HOL/NumberTheory/WilsonRuss.thy
changeset 13524 604d0f3622d6
parent 13187 e5434b822a96
child 13788 fd03c4ab89d4
     1.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  text {* \medskip @{term [source] inv} *}
     1.6  
     1.7 -lemma aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
     1.8 +lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
     1.9    apply (subst int_int_eq [symmetric])
    1.10    apply auto
    1.11    done
    1.12 @@ -44,7 +44,7 @@
    1.13    apply (subst zmod_zmult1_eq [symmetric])
    1.14    apply (subst zcong_zmod [symmetric])
    1.15    apply (subst power_Suc [symmetric])
    1.16 -  apply (subst aux)
    1.17 +  apply (subst inv_is_inv_aux)
    1.18     apply (erule_tac [2] Little_Fermat)
    1.19     apply (erule_tac [2] zdvd_not_zless)
    1.20     apply (unfold zprime_def)
    1.21 @@ -89,7 +89,7 @@
    1.22            apply auto
    1.23    done
    1.24  
    1.25 -lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    1.26 +lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    1.27    apply (unfold zcong_def)
    1.28    apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
    1.29    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    1.30 @@ -106,7 +106,7 @@
    1.31    apply safe
    1.32    apply (cut_tac a = a and p = p in inv_is_inv)
    1.33       apply auto
    1.34 -  apply (simp add: aux)
    1.35 +  apply (simp add: inv_not_p_minus_1_aux)
    1.36    apply (subgoal_tac "a = p - 1")
    1.37     apply (rule_tac [2] zcong_zless_imp_eq)
    1.38         apply auto
    1.39 @@ -137,7 +137,7 @@
    1.40    apply (simp add: pos_mod_bound)
    1.41    done
    1.42  
    1.43 -lemma aux: "5 \<le> p ==>
    1.44 +lemma inv_inv_aux: "5 \<le> p ==>
    1.45      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
    1.46    apply (subst int_int_eq [symmetric])
    1.47    apply (simp add: zmult_int [symmetric])
    1.48 @@ -163,7 +163,7 @@
    1.49        apply (subst zcong_zmod)
    1.50        apply (subst mod_mod_trivial)
    1.51        apply (subst zcong_zmod [symmetric])
    1.52 -      apply (subst aux)
    1.53 +      apply (subst inv_inv_aux)
    1.54         apply (subgoal_tac [2]
    1.55  	 "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
    1.56          apply (rule_tac [3] zcong_zmult)