*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] global_interpretation and code generation*From*: Peter Lammich <lammich at in.tum.de>*Date*: Thu, 22 Mar 2018 17:34:43 +0100*In-reply-to*: <e9afb449-f54f-c511-bb95-2c6a8ab92081@informatik.tu-muenchen.de>*References*: <1521724643.21440.14.camel@in.tum.de> <e9afb449-f54f-c511-bb95-2c6a8ab92081@informatik.tu-muenchen.de>

Hi Florian, that worked for me, with the only change that (in Isabelle2017) the "rewrites" section must come AFTER the "defines" section. Thanks a lot, Peter On Do, 2018-03-22 at 15:02 +0100, Florian Haftmann wrote: > 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 >

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

**Re: [isabelle] global_interpretation and code generation***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Cardinality for infinite sets
- Next by Date: Re: [isabelle] Cardinality for infinite sets
- Previous by Thread: Re: [isabelle] global_interpretation and code generation
- Next by Thread: [isabelle] Deadline Extension: ICMS'18 Session on Software for Mathematical Reasoning and Applications
- 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