Email Gateway (Aug 22 2022 at 17:23): Email Gateway (Aug 22 2022 at 17:23):From: Paulo Emílio de Vilhena <pevilhena2@gmail.com>
Dear all,
I'm working in HOL-Algebra and I would like to share a problem. The
formalism of algebraic structures proposed by this library is very
comprehensive, because it deals with sets of a certain type instead of all
the elements of a given type, and properties for operations are defined on
those sets. The problem is that to have these properties we need always to
prove that the elements which we talk about belong to this set. As a
consequence, a big part of almost all the proofs are results of the kind "a
: carrier G ==> b : carrier G ==> a + b : carrier G".
If membership to this set was seen as a type, many proofs of this library
could be shorten, so I wonder if there ism't a way to do this (at least
inside a proof). I know some tools to declare new types, but none of them
could solve this particular issue. I heard that locale typedefs could do
the job, but I didn't find any tutorial. Does anyone of you know how they
work or where could I find documentation for those?
Cheers,
Paulo.
Email Gateway (Aug 22 2022 at 17:30):From: Fabian Immler <immler@in.tum.de>
Dear Paulo,
I recently added another (somewhat larger) example [1] to HOL-Types_To_Sets to the development version.
So this will most likely be part of the upcoming Isabelle2018 release.
This example can be seen as one result of the discussions we had Spain:
It uses local typedef to go from the type-based linear algebra (Modules.thy, Vector_Spaces.thy) to explicit carrier sets.
Best regards,
Fabian
[1] http://isabelle.in.tum.de/repos/isabelle/file/f1f989b656bb/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
smime.p7s
Email Gateway (Aug 22 2022 at 17:31):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Paulo,
the problem that you run into, was the main motivation why we started
working on what is known under the name "local typedef". The local
typedef was added to Isabelle in 2017 and it still doesn't reach the
maturity of other parts of the system. This is also the reason why the
interface is a bit rudimentary, some steps must be done manually, and
there is no documentation in the traditional sense.
But the situation is not that hopeless that it might sound.
The sources of information are:
The extended JAR paper about local typedef, which was just
published a couple of days ago. The paper contains both theoretical
background and practical examples.
https://www21.in.tum.de/~kuncar/documents/types-to-sets-JAR2018.pdf
The examples from the paper as a proof text also exist in Isabelle
and can be found in src/HOL/Types_To_Sets/Examples.
There was a meeting of Isabelle powerusers in Spain the last year and
as far as I know the topic how to use local typedef for HOL-Algebra was
discussed there. Maybe some of the participants could tell us more
about the results.
This mailing list (or you could write privately to me).
Let me know if you need more help.
Best,
Ondřej
Last updated: Apr 26 2024 at 04:17 UTC