Re: [isabelle] Formalising matrix operations



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
> 






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