Re: [isabelle] Formalising matrix operations



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
Description: OpenPGP digital signature



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