--- a/src/HOL/Library/Euclidean_Space.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Apr 29 14:20:26 2009 +0200
@@ -253,8 +253,6 @@
"vector_power x 0 = 1"
| "vector_power x (Suc n) = x * vector_power x n"
-instance "^" :: (recpower,type) recpower ..
-
instance "^" :: (semiring,type) semiring
apply (intro_classes) by (vector ring_simps)+
@@ -2757,7 +2755,7 @@
(* Geometric progression. *)
(* ------------------------------------------------------------------------- *)
-lemma sum_gp_basic: "((1::'a::{field, recpower}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
(is "?lhs = ?rhs")
proof-
{assume x1: "x = 1" hence ?thesis by simp}
@@ -2775,7 +2773,7 @@
qed
lemma sum_gp_multiplied: assumes mn: "m <= n"
- shows "((1::'a::{field, recpower}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+ shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
(is "?lhs = ?rhs")
proof-
let ?S = "{0..(n - m)}"
@@ -2792,7 +2790,7 @@
by (simp add: ring_simps power_add[symmetric])
qed
-lemma sum_gp: "setsum (op ^ (x::'a::{field, recpower})) {m .. n} =
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
(if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
else (x^ m - x^ (Suc n)) / (1 - x))"
proof-
@@ -2808,7 +2806,7 @@
ultimately show ?thesis by metis
qed
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field,recpower})) {m .. m+n} =
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
(if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
unfolding sum_gp[of x m "m + n"] power_Suc
by (simp add: ring_simps power_add)