Re: [isabelle] Sublocale, subclass and execution.
It might be helpful to explain what permanent_interpretation does in terms a sublocale declaration and definitions.
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
> 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,
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and