src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 44766 d4d33a4d7548
parent 42793 88bee9f6eec7
child 44821 a92f65e174cf
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -80,7 +80,7 @@
     1.4  lemma inv_not_p_minus_1_aux:
     1.5      "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
     1.6    apply (unfold zcong_def)
     1.7 -  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
     1.8 +  apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
     1.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
    1.10     apply (simp add: algebra_simps)
    1.11    apply (subst dvd_minus_iff)
    1.12 @@ -123,13 +123,13 @@
    1.13      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
    1.14    apply (subst int_int_eq [symmetric])
    1.15    apply (simp add: zmult_int [symmetric])
    1.16 -  apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
    1.17 +  apply (simp add: left_diff_distrib right_diff_distrib)
    1.18    done
    1.19  
    1.20  lemma zcong_zpower_zmult:
    1.21      "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
    1.22    apply (induct z)
    1.23 -   apply (auto simp add: zpower_zadd_distrib)
    1.24 +   apply (auto simp add: power_add)
    1.25    apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
    1.26     apply (rule_tac [2] zcong_zmult, simp_all)
    1.27    done
    1.28 @@ -261,7 +261,7 @@
    1.29        apply (subgoal_tac [5]
    1.30          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
    1.31         prefer 5
    1.32 -       apply (simp add: zmult_assoc)
    1.33 +       apply (simp add: mult_assoc)
    1.34        apply (rule_tac [5] zcong_zmult)
    1.35         apply (rule_tac [5] inv_is_inv)
    1.36           apply (tactic "clarify_tac @{context} 4")