*To*: Jose Divasón <jose.divasonm at unirioja.es>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Sublocale, subclass and execution.*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 09 Oct 2014 16:02:12 +0200*In-reply-to*: <CA+MUZ5ta51MyoA+JK0gzZEdLCZmP1PvWqp7aU1eKGFpCtkMuDA@mail.gmail.com>*Organization*: TU Munich*References*: <CA+MUZ5ta51MyoA+JK0gzZEdLCZmP1PvWqp7aU1eKGFpCtkMuDA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.1.2

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

**Attachment:
Foo.thy**

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Sublocale, subclass and execution.***From:*Clemens Ballarin

**Re: [isabelle] Sublocale, subclass and execution.***From:*Jose Divasón

**References**:**[isabelle] Sublocale, subclass and execution.***From:*Jose Divasón

- Previous by Date: [isabelle] Sublocale, subclass and execution.
- Next by Date: Re: [isabelle] The theory Option
- Previous by Thread: [isabelle] Sublocale, subclass and execution.
- Next by Thread: Re: [isabelle] Sublocale, subclass and execution.
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list