# Re: [isabelle] Formalising matrix operations

```Dear Stefan,

I took the liberty of forwarding your email to John Harrison, whose HOL
light library our Multivariate_Analysis is based on. I have attched his
answer and trust you will find it useful ;-)

Tobias

Am 04/01/2012 17:10, schrieb Stefan Hetzl:
> Dear all,
>
> I am working on a formalisation of the Cayley-Hamilton theorem in
> Isabelle/HOL. I was planning to base it on the formalisation of
> matrices which is available in HOL/Multivariate_Analysis as it
> includes a number of useful properties of determinants.
>
> I would like to formalise operations that delete a single row and/or a
> single column from a matrix. Taking into account the fact the matrices
> of Multivariante_Analysis are vectors of vectors of elements and that
> it is easy to define permutations of elements of a vector, the task
> can be boiled down to defining an operation which deletes the last
> element of a vector.
>
> I have run into a problem there: a vector is defined as a mapping from
> a type 'b of class finite to a type 'a. Based on
> HOL/Library/Numeral_Type one can define something like
>
> definition dellastel32 :: "('a, 3) vec \<Rightarrow> ('a, 2) vec"
>   where "dellastel32 v = (\<chi> i. if i = 1 then (v \$ 1) else (v \$ 2))"
>
> for every finite vector length. However, I do not see what to do for
> the general case.
>
> I am grateful for any help or pointer you can provide.
>
>
> Best regards,
>
> Stefan Hetzl
```
--- Begin Message ---
• To: Tobias Nipkow <nipkow at in.tum.de>
• Subject: Re: Fwd: [isabelle] Formalising matrix operations
• From: "john.r.harrison" <johnh at ecsmtp.pdx.intel.com>
• Date: Thu, 05 Jan 2012 19:40:32 -0800
• Cc: John Harrison <johnh at ecsmtp.pdx.intel.com>
• Delivered-to: nipkow@mailbroy.informatik.tu-muenchen.de
• Delivered-to: tobias.nipkow@informatik.tu-muenchen.de
• In-reply-to: Your message of "Thu, 05 Jan 2012 09:12:16 +0100." <4F055B60.4000806@in.tum.de>
```Hi Tobias,

Happy New Year, by the way!

I did a proof of Cayley-Hamilton for a bit of fun sometime last year
and came across exactly the same issue.

One could perfectly well define a type constructor ('a)delete or
something that would give you a type one element smaller than 'a.
It would be basically straightforward, but mildly tedious, and
I'm not sure how generally useful it would be.

I chose the simpler solution of defining cofactors in a slightly
non-standard but equivalent way. Instead of deleting the i'th row
and j'th column I jammed a 1 in the (i,j) position and otherwise
0s in those rows and columns:

let cofactor = new_definition
`(cofactor:real^N^N->real^N^N) A =
lambda i j. det((lambda k l. if k = i /\ l = j then &1
else if k = i \/ l = j then &0
else A\$k\$l):real^N^N)`;;

This stays in the cosy NxN world, and if anything it's slightly
simpler to work with than the usual definition because you don't
have the additional (-1)^{i+j} factor. For more details see