Re: [isabelle] Sublocale, subclass and execution.

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:

Attachment: Foo.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature

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