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 ---
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

  http://code.google.com/p/hol-light/source/browse/trunk/Multivariate/determinants.ml

John.

--- End Message ---


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.