Re: [isabelle] global_interpretation and code generation



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
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.