访问Isabelle中矩阵的第一个元素

Question

访问矩阵的“第一”元素

我想要写一个关于矩阵行列式的平凡情形的证明，其中矩阵只包含一个元素(即'n的基数是1)。

因此行列式(或det A)是矩阵中的单个元素。

然而，我不清楚如何引用矩阵中的单一元素。我试过A $ zero $ zero，但没有用。

我目前演示这个问题的方法是编写∀a∈(UNIV :: 'n set). det A = A $ a $ a。它假定数字类型的基数为1。

写这个关于决定因素的琐碎证明的正确方法是什么？

以下是我的当前代码：

theory Notepad
imports
  Main
  "~~/src/HOL/Library/Polynomial"
  "~~/src/HOL/Algebra/Ring"
  "~~/src/HOL/Library/Numeral_Type"
  "~~/src/HOL/Library/Permutations"
  "~~/src/HOL/Multivariate_Analysis/Determinants"
  "~~/src/HOL/Multivariate_Analysis/L2_Norm"
  "~~/src/HOL/Library/Numeral_Type"
begin


lemma det_one_element_matrix:
fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
assumes "card(UNIV :: 'n set) = 1"
shows "∀a∈(UNIV :: 'n set). det A = A $ a $ a"
proof-

  (*sledgehammer proof of 1, 2 and ?thesis *)
  have 1: "∀a∈(UNIV :: 'n set). UNIV = {a}"   
  by (metis (full_types) Set.set_insert UNIV_I assms card_1_exists ex_in_conv)

  have 2:
  "det A = (∏i∈UNIV. A $ i $ i)" 
  by (metis (mono_tags, lifting) "1" UNIV_I det_diagonal singletonD)

  from 1 2 show ?thesis by (metis setprod_singleton)

qed

更新：

不幸的是，这是一个更大的定理的一部分，这个定理已经证明了'n∷finite > 1的基数。在这个定理中，矩阵A的类型被固定为A :: "('a::comm_ring_1)^'n∷finite^'n∷finite，行列式的定义也在这个较大的定理中使用。

因此，我认为我不能把矩阵A的类型改变为('a::comm_ring_1)^1^1)，来解决我的更大的定理。

Answer 1

我认为，如果可以使用，我以前的答案一般是更好的解决办法，因此我将保留原样。在您无法使用这种方法的情况下，不幸的是，事情变得更加困难。

你需要展示的是：

• 类型'n中只能有一个元素，因此每个元素都是相等的；
• 此外，det的定义也引用了排列，因此我们需要证明只有一个类型为'n ⇒ 'n的函数，它恰好等于函数id。

有了这些证据，我们可以进行下列证明：

lemma det_one_element_matrix:
  fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
  assumes "card(UNIV :: 'n set) = 1"
  shows "det A = A $ x $ x"
proof-
  have 0: "⋀x y. (x :: 'n) = y"
    by (metis (full_types) UNIV_I assms card_1_exists)

  hence 1: "(UNIV :: 'n set) = {x}"
    by auto

  have 2: "(UNIV :: ('n ⇒ 'n) set) = {id}"
    by (auto intro!: ext simp: 0)

  thus ?thesis
    by (auto simp: det_def permutes_def 0 1 2 sign_id)
qed

Answer 2

使用A $ zero $ zero (或A $ 0 $ 0)是行不通的，因为向量是从1：A $ 0 $ 0中索引的，这使得很难证明任何关于。

我自己玩了一会儿，我想出了下面的引理：

lemma det_one_element_matrix:
   "det (A :: ('a::comm_ring_1)^1^1) = A $ 1 $ 1"
  by (clarsimp simp: det_def sign_def)

我没有使用类型'a :: finite并假设它具有基数1，而是使用了标准的Isabelle 1类型，它将这两个事实编码为类型本身。(所有数字都存在类似的类型，因此您可以编写类似于'a ^ 23 ^ 72的东西)

顺便说一句，在输入上述引理之后，auto solve_direct很快告诉我，库中已经存在一些东西，说明了相同的结果，一个名为det_1的引理。