Isabelle:矩阵的幂(A ^ n)? [英] Isabelle: Power of a matrix (A^n)?
问题描述
Cartesian_Euclidean_Space
中有一个矩阵乘法定义(在目录HOL/Multivariate_Analysis中):
There is a matrix multiplication definition in Cartesian_Euclidean_Space
(in directory HOL/Multivariate_Analysis"):
definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m ⇒ 'a ^'p^'n ⇒ 'a ^ 'p ^'m"
(infixl "**" 70)
where "m ** m' == (χ i j. setsum (λk. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
现在,平方矩阵将是A ** A
,A ^ 3将是A ** A ** A
.
Now the the squared matrix would be A ** A
and A^3 would be A ** A ** A
.
我找不到定义A^n
的幂函数(即A ** A ** ... ** A
n次).
I couldn't find a powerfunction, to define A^n
(i.e., A ** A ** ... ** A
n times).
库中是否有幂函数?需要手动定义吗?
Is there a power function in the library? Is a manual definition needed?
推荐答案
我在HOL/Power.thy
中找到了以下定义:
I have found the following definition in HOL/Power.thy
:
primrec power :: "'a ⇒ nat ⇒ 'a" (infixr "^" 80) where
power_0: "a ^ 0 = 1"
| power_Suc: "a ^ Suc n = a * a ^ n"
(按Control + Click进入相应的定义!所以我单击"^",我首先写了"1 ^ 1 = 1"作为引理.
(Control + Click gets you to the respecitve definition! So I clicked on "^", I just wrote "1 ^ 1 = 1" as a lemma first.
这是矩阵幂的定义.
(由于我只使用平方矩阵,这很好,但是更通用的^'n^'m
类型会很好.)
Here is the definition for the power of a matrice.
(As I only use square matrices this is fine, but a more general type of ^'n^'m
would be nice.)
primrec powerM :: "(('a::semiring_1) ^'n^'n) ⇒ nat ⇒ (('a::semiring_1) ^'n^'n)"
(infixr "^^^" 80) where
powerM_0: "A ^^^(0::nat) = mat 1"
| powerM_Suc: "A ^^^(Suc n) = A ** (powerM A n)"
这篇关于Isabelle:矩阵的幂(A ^ n)?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!