equal
deleted
inserted
replaced
251 |
251 |
252 fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where |
252 fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where |
253 "vector_power x 0 = 1" |
253 "vector_power x 0 = 1" |
254 | "vector_power x (Suc n) = x * vector_power x n" |
254 | "vector_power x (Suc n) = x * vector_power x n" |
255 |
255 |
256 instantiation "^" :: (recpower,type) recpower |
256 instance "^" :: (recpower,type) recpower .. |
257 begin |
|
258 definition vec_power_def: "op ^ \<equiv> vector_power" |
|
259 instance |
|
260 apply (intro_classes) by (simp_all add: vec_power_def) |
|
261 end |
|
262 |
257 |
263 instance "^" :: (semiring,type) semiring |
258 instance "^" :: (semiring,type) semiring |
264 apply (intro_classes) by (vector ring_simps)+ |
259 apply (intro_classes) by (vector ring_simps)+ |
265 |
260 |
266 instance "^" :: (semiring_0,type) semiring_0 |
261 instance "^" :: (semiring_0,type) semiring_0 |