Re: [isabelle] global_interpretation and code generation



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
Description: OpenPGP digital signature



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