*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] global_interpretation and code generation*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 22 Mar 2018 15:02:30 +0100*In-reply-to*: <1521724643.21440.14.camel@in.tum.de>*Organization*: TU Munich*References*: <1521724643.21440.14.camel@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

Hi Peter, > Suppose I have the following locale hierachy: > > A definition f = ... > A' = A + ... > B = A + ... definition h = ... f ... > > I (globally) interpret i10: A', and then B (using the i10- > interpretation for the A part). The proof obligations are as expected, > however, it will not generate code equations for functions in B that > use functions from A. > > If I build i10 stepwise, by first interpreting A and then A', > everything works fine. Is there a canonical way to obtain code > equations with global_interpretation? Does it include manually > providing interpretations for every super-locale, as worked in my case? > Is it documented somewhere? the rewrite morphisms stemming from mixin definitions are not propagated along an import hierarchy. Hence you have to spell it out explicitly. The standard pattern looks as follows: > global_interpretation B where n = "10" and m = "100" > rewrites "A.f 10 = f_impl" > defines h_impl = h > proof - > show "B 10 100" > by standard simp > then interpret B where n = "10" and m = "100" . > show "A.f 10 = f_impl" > by (simp add: f_impl_def) > qed Hope this helps, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] global_interpretation and code generation***From:*Peter Lammich

**References**:**[isabelle] global_interpretation and code generation***From:*Peter Lammich

- Previous by Date: [isabelle] global_interpretation and code generation
- Next by Date: Re: [isabelle] Cardinality for infinite sets
- Previous by Thread: [isabelle] global_interpretation and code generation
- Next by Thread: Re: [isabelle] global_interpretation and code generation
- Cl-isabelle-users March 2018 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