Re: [isabelle] global_interpretation and code generation
that worked for me, with the only change that (in Isabelle2017) the
"rewrites" section must come AFTER the "defines" section.
Thanks a lot,
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
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and