src/HOL/Library/Euclidean_Space.thy

   apply (intro_classes) by vector
 
 fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where
   "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)+
 
 instance "^" :: (semiring_0,type) semiring_0

 
 (* ------------------------------------------------------------------------- *)
 (* 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}
   moreover
   {assume x1: "x\<noteq>1"

     then have ?thesis by (simp add: ring_simps) }
   ultimately show ?thesis by metis
 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)}"
   from mn have mn': "n - m \<ge> 0" by arith
   let ?f = "op + m"

   have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
   then show ?thesis unfolding sum_gp_basic using mn
     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-
   {assume nm: "n < m" hence ?thesis by simp}
   moreover

     ultimately have ?thesis by metis
   }
   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)