--- a/src/HOL/Library/Commutative_Ring.thy Thu Sep 21 19:06:16 2006 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy Fri Sep 22 13:04:30 2006 +0200
@@ -266,7 +266,6 @@
lemma pow_ci: "Ipol ls (pow (p, n)) = Ipol ls p ^ n"
proof (induct n arbitrary: p rule: nat_less_induct)
case (1 k)
- have two: "2 = Suc (Suc 0)" by simp
show ?case
proof (cases k)
case 0
@@ -295,14 +294,14 @@
next
case (Suc w)
with `odd l` have "even w" by simp
- from two have two_times: "2 * (w div 2) = w"
- by (simp only: even_nat_div_two_times_two [OF `even w`])
+ have two_times: "2 * (w div 2) = w"
+ by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
have "Ipol ls p * Ipol ls p = Ipol ls p ^ Suc (Suc 0)"
by (simp add: power_Suc)
- from this and two [symmetric] have "Ipol ls p * Ipol ls p = Ipol ls p ^ 2"
- by simp
+ then have "Ipol ls p * Ipol ls p = Ipol ls p ^ 2"
+ by (simp add: numerals)
with Suc show ?thesis
- by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
+ by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci)
qed
} with 1 Suc `odd l` show ?thesis by simp
qed
@@ -326,4 +325,6 @@
use "comm_ring.ML"
setup CommRing.setup
+thm mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]
+
end