Re: [isabelle] Locale typedef



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:
1. 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
2. The examples from the paper as a proof text also exist in Isabelle
and can be found in src/HOL/Types_To_Sets/Examples.
3. 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.
4. This mailing list (or you could write privately to me).
5. There are first pioneers using the local typedef in AFP. You could
find the theory files by grepping for "Types_To_Sets" in the AFP
sources.

Let me know if you need more help.

Best,
Ondřej 



On Mon, 4 Jun 2018 16:24:40 +0100
Paulo Emílio de Vilhena <pevilhena2 at gmail.com> wrote:

> 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.





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