*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Formalising matrix operations*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Mon, 09 Jan 2012 12:55:48 +1300*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 (X11; U; Linux x86_64; en-US; rv:1.9.2.24) Gecko/20111108 Thunderbird/3.1.16

On 05/01/12 05:10, Stefan Hetzl wrote: > 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 haven't checked this (partly because I usually use an old version of Isabelle --- 2009-2), but if there is a general injection function finplus1inj :: "'n -> 'n + 1" then I think you could get what you want by: definition dellastel :: "('a, 'n + 1) vec \<Rightarrow> ('a, 'n) vec" where "dellastel v = (\<chi> i. (v $ (finplus1inj i)))" So, does Isabelle have such an injection function in the general case? And would my suggestion work if Isabelle does have it? Tim <><

**Attachment:
signature.asc**

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

- Previous by Date: [isabelle] New AFP entry: Markov Models
- Next by Date: [isabelle] Elbe with Symbols
- Previous by Thread: Re: [isabelle] Formalising matrix operations
- Next by Thread: [isabelle] FUN verses PRIMREC
- 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