Email Gateway (Aug 18 2022 at 18:54): Email Gateway (Aug 18 2022 at 18:54):From: Stefan Hetzl <hetzl@logic.at>
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
Email Gateway (Aug 18 2022 at 18:54):From: Steven Obua <steven.obua@googlemail.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
Email Gateway (Aug 18 2022 at 18:54):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 18:55):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
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
<><
signature.asc
Last updated: Apr 19 2024 at 08:19 UTC