Email Gateway (Aug 22 2022 at 16:59): Email Gateway (Aug 22 2022 at 16:59):From: Peter Lammich <lammich@in.tum.de>
Hi.
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?
Email Gateway (Aug 22 2022 at 16:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 22 2022 at 17:00):From: Peter Lammich <lammich@in.tum.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
Last updated: Apr 26 2024 at 20:16 UTC