[isabelle] Formalising matrix operations

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

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