Re: [isabelle] Sublocale, subclass and execution.



It might be helpful to explain what permanent_interpretation does in terms a sublocale declaration and definitions.

Clemens


On 09 October, 2014 16:02 CEST, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Jose,
>
> > So, I did it using sublocales (see the attached file).
>
> you approach in principle is right.
>
> The complications you encounter are due to the fact that the code
> generator only accepts equations headed by logical constants (for
> purpose of simple foundation) but syntactical constants stemming from
> interpretations after definitions in locales are usually syntactic
> abbreviations.
>
> Find the solution in the attached theory.
>
> In short steps:
> * Import "~~/src/Tools/Permanent_Interpretation" (this will later allow
> to resolve the constant / abbreviation issue with minimal effort).
> * sublocale a ⊆ E is equivalent to context a begin … sublocale E … end
> * Substitute sublocale p: F by permanent_interpretation p?: F (logically
> equivalent, but note the subtle change in semantics of prefixes, see below)
> * Note that locale expressions support also named instantiation rather
> than positional one, which is superior in presence of many parameters
> (see below – this is not required, but makes more clear whats going on)
> * Currently we are at
>
> > permanent_interpretation field_is_euclidean_ring?: euclidean_ring
> >   where div = "λa b. if b = 0 then 0 else a/b"
> >     and mod = "λa b. if b = 0 then a else 0"
> >     and euclidean_size = "λi. if i = 0 then 0 else 1::nat"
> >     and normalisation_factor = id
>
> * Then add a »defining« clause
>
> > defining gcd_eucl = gcd_eucl
>
> which essentially makes an appropriate constant definition and provides
> a suitable mixin equation for the interpretation such that theorems are
> properly folded.
>
> That's it in the first instance.
>
> Note that the unexpected »real« type is due to an implicit coercion.
>
> I usually recommend to make interpretation prefixes mandatory (ie.
> dropping the »?«).
>
> Hope this helps,
> 	Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de








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