author haftmann Mon Feb 08 17:12:30 2010 +0100 (2010-02-08) changeset 35048 82ab78fff970 parent 35047 1b2bae06c796 child 35049 00f311c32444
tuned proofs
```     1.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Feb 08 17:12:27 2010 +0100
1.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Feb 08 17:12:30 2010 +0100
1.3 @@ -74,9 +74,9 @@
1.4  lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
1.5    -- {* same as @{text WilsonRuss} *}
1.6    apply (unfold zcong_def)
1.7 -  apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
1.8 +  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
1.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
1.10 -   apply (simp add: mult_commute)
1.11 +   apply (simp add: algebra_simps)
1.12    apply (subst dvd_minus_iff)
1.13    apply (subst zdvd_reduce)
1.14    apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
```
```     2.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Feb 08 17:12:27 2010 +0100
2.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Feb 08 17:12:30 2010 +0100
2.3 @@ -82,9 +82,9 @@
2.4  lemma inv_not_p_minus_1_aux:
2.5      "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
2.6    apply (unfold zcong_def)
2.7 -  apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
2.8 +  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
2.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
2.10 -   apply (simp add: mult_commute)
2.11 +   apply (simp add: algebra_simps)
2.12    apply (subst dvd_minus_iff)
2.13    apply (subst zdvd_reduce)
2.14    apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
```
```     3.1 --- a/src/HOL/Word/BinGeneral.thy	Mon Feb 08 17:12:27 2010 +0100
3.2 +++ b/src/HOL/Word/BinGeneral.thy	Mon Feb 08 17:12:30 2010 +0100
3.3 @@ -742,7 +742,7 @@
3.4
3.5  lemma sb_inc_lem':
3.6    "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
3.7 -  by (rule iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0])
3.8 +  by (rule sb_inc_lem) simp
3.9
3.10  lemma sbintrunc_inc:
3.11    "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
```