*To*: hetzl at logic.at*Subject*: Re: [isabelle] Formalising matrix operations*From*: Steven Obua <steven.obua at googlemail.com>*Date*: Thu, 5 Jan 2012 09:33:49 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAChLSoBZmtv5_M=YTTi_WkEbbG+TFZ+ubqHEfk33qSFSWHb8PA@mail.gmail.com>*References*: <CAChLSoBZmtv5_M=YTTi_WkEbbG+TFZ+ubqHEfk33qSFSWHb8PA@mail.gmail.com>

Hi Stefan, I am not familiar with the Multivariate_Analysis package, but with the trick of representing matrix dimensions by types. This trick becomes pretty ugly in exactly this situation of mapping between matrices of variable dimensions. Nevertheless, a (n ugly) way of achieving your goal would proceed along the following lines: There is probably some sort of "size" function already defined, for example size : 'a -> nat, that returns the number of elements of type 'a. Then you turn the concrete dimensions in the type of the function you want to define into type variables, like this: definition del :: "nat -> ('a, 'n) vec -> ('a, 'm) vec" where "del row v = let n = size (arbitrary : 'n), m = size (arbitrary : 'm), in if (row < n && m + 1 = n) then .... else arbitrary end end" Cheers, Steven On 04.01.2012, at 16:10, Stefan Hetzl wrote: > 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 >

**References**:**[isabelle] Formalising matrix operations***From:*Stefan Hetzl

- Previous by Date: Re: [isabelle] L4.verified C-to-Isabelle parser release
- Next by Date: Re: [isabelle] Formalising matrix operations
- Previous by Thread: [isabelle] Formalising matrix operations
- Next by Thread: Re: [isabelle] Formalising matrix operations
- Cl-isabelle-users January 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list