*To*: "Florian Haftmann" <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Sublocale, subclass and execution.*From*: "Clemens Ballarin" <ballarin at in.tum.de>*Date*: Thu, 09 Oct 2014 22:04:06 +0200*Cc*: isabelle-users at cl.cam.ac.uk, Jose Divasón <jose.divasonm at unirioja.es>*In-reply-to*: <54369564.7040605@informatik.tu-muenchen.de>*User-agent*: SOGoMail 2.2.9a

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

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

**References**:**Re: [isabelle] Sublocale, subclass and execution.***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] The theory Option
- Next by Date: [isabelle] New AFP entry: Probability Density Functions
- Previous by Thread: Re: [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