matrix - 伊莎贝尔:莱布尼茨公式的问题

Question

据我了解，Isabelle 中的矩阵本质上是任意维度的函数。在此设置中，定义平方矩阵(n x n 矩阵)并不容易。此外，在纸上校样中，可以在校样中使用平方的尺寸“n”。但我该如何在伊莎贝尔做到这一点呢？

莱布尼茨公式:

我的纸质证明:

这是我的伊莎贝尔证明的相关摘录:

(* tested with Isabelle2013-2 (and also Isabelle2013-1) *)
theory Notepad
imports
  Main
  "~~/src/HOL/Library/Polynomial"
  "~~/src/HOL/Multivariate_Analysis/Determinants"
begin

notepad
begin
  fix C :: "('a::comm_ring_1 poly)^'n∷finite^'n∷finite"

  (* Definition Determinant (from the HOL Library, shown for reference
     see: "~~/src/HOL/Multivariate_Analysis/Determinants") *)
 have "det C =
      setsum (λp. of_int (sign p) * 
             setprod (λi. C$i$p i) (UNIV :: 'n set))
             {p. p permutes (UNIV :: 'n set)}" unfolding det_def by simp 

  (* assumtions *)
  have 1: "∀ i j. degree (C $ i $ j) ≤ 1" sorry (* from assumtions, not shown *)
  have 2: "∀ i. degree (C $ i $ i) = 1" sorry (* from assumtions, not shown *)

  (* don't have "n", that is the dimension of the squared matrix *)
  have "∀p∈{p. p permutes (UNIV :: 'n set)}. degree (setprod (λi. C$i$p i) (UNIV :: 'n set)) ≤ n" sorry (* no n! *)
end

遇到这种情况我能做什么？

<小时/>

更新:

Your type for C, a restricted version of ('a ^ 'n ^ 'n), appears to be a custom type of > yours, because I get an error when trying to use it, even after importing > Polynomial.thy. But maybe it's defined in some other HOL theory.

不幸的是，我没有在代码示例中编写包含内容，请参阅更新的示例。但它不是自定义类型，导入“Polynomial.thy”和“Determinants”就足够了。 (我测试了 Isabelle 版本 2013-1 和 2013-2。)

If you're using a custom definition of a matrix, there's a good chance you're on your own, for the most part.

我不相信我正在使用矩阵的自定义定义。库Determinants (~~/src/HOL/Multivariate_Analysis/Determinants) 具有以下行列式定义:
定义 det::"'a::comm_ring_1^'n^'n ⇒ 'a"其中 ...。因此，该库使用矩阵的概念作为向量的向量。如果我的环是多项式，那么在我看来应该不会有什么不同。

Regardless, for a type such as ('a ^ 'n ^ 'n), it seems to me, you should be able to write a function to return a value for the size of the matrix. So if (p ^ n ^ n) is a matrix, where n is a set, then maybe the cardinality of n is the n you want in your question.

这让我走上了正确的道路。我目前的猜测是以下定义很有帮助:

definition card_diagonal :: "('a::zero poly)^'n^'n ⇒ nat" where "card_diagonal A = card { (A $ i $ i) | i . True }"

card 定义在 Finite_Set 中。

Answer 1

在我看来，这个问题的本质是如何从给定的 n x n 矩阵 A 中获取整数 n。这里的困难在于这个整数是用 A 的类型编码的。尽管如此，我似乎很清楚 n 实际上是问题的一个参数。尽管我们可以想象以某种方式在内部存储维度的矩阵表示，但从数学的角度来看，通过陈述“让 n 为正整数”来开始整个开发是很自然的。