*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Formalising matrix operations*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 06 Jan 2012 09:22:51 +0100*Cc*: John Harrison <johnh at ichips.intel.com>*In-reply-to*: <CAChLSoBZmtv5_M=YTTi_WkEbbG+TFZ+ubqHEfk33qSFSWHb8PA@mail.gmail.com>*References*: <CAChLSoBZmtv5_M=YTTi_WkEbbG+TFZ+ubqHEfk33qSFSWHb8PA@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0

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 operationsFrom: "john.r.harrison" <johnh at ecsmtp.pdx.intel.com>Date: Thu, 05 Jan 2012 19:40:32 -0800Cc: John Harrison <johnh at ecsmtp.pdx.intel.com>Delivered-to: nipkow@mailbroy.informatik.tu-muenchen.deDelivered-to: tobias.nipkow@informatik.tu-muenchen.deIn-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 http://code.google.com/p/hol-light/source/browse/trunk/Multivariate/determinants.ml John.

---End Message---

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

- Previous by Date: Re: [isabelle] Formalising matrix operations
- Next by Date: Re: [isabelle] chaining facts into the terminal method after "qed"
- Previous by Thread: Re: [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