Accessing first element of a matrix in Isabelle

Question

Accessing the “first” element of a matrix

I want to write a proof about a trivial case of the determinant of a matrix, where the matrix consists of just a single element (i.e., the cardinality of 'n is one).

Thus the determinant (or det A) is the single element in the matrix.

However, it is not clear to me how to reference the single element of the matrix. I tried A $ zero $ zero, which did not work.

My current way to demonstrate the problem is to write ∀a∈(UNIV :: 'n set). det A = A $ a $ a. It assumes that the cardinality of the numeral type is one.

What is the correct way to write this trivial proof about determinants?

Here is my current code:

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

---

UPDATE:

Unfortunately, this is part of a larger theorem which is already proven for the cardinality of 'n∷finite > 1. In this theorem the type of matrix A is fixed as A :: "('a::comm_ring_1)^'n∷finite^'n∷finite and the definition of the determinant is used in this larger theorem.

Therefore, I don't think I can change the type of my matrix A to ('a::comm_ring_1)^1^1) in oder to solve my larger theorem.

Answer 1

I feel that my previous answer is the better solution in general if it is possible to use, so I will leave it as-is. In your case where you are not able to use this approach, things get a little harder, unfortunately.

What you need to show is that:

• There can only be a single element in your type 'n, and thus every element is equal;

• Additionally, the definition of det also references permutations, so we need to show that there only exists a single function of type 'n ⇒ 'n, which happens to be equal to the function id.

With these in place, we can carry out the proof as follows:

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

Using A $ zero $ zero (or A $ 0 $ 0) wouldn't have worked, because the vectors are indexed from 1: A $ 0 $ 0 is undefined, which makes it hard to prove anything about.

Playing a little myself, I came up with the following lemma:

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

Instead of using a type 'a :: finite and assuming it has cardinality 1, I used the standard Isabelle 1 type which encodes both these facts into the type itself. (Similar types exist for all numerals, so you can write things like 'a ^ 23 ^ 72)

Incidentally, after typing in the lemma above, auto solve_direct quickly informed me that something already exists in the library stating the same result, a lemma named det_1.