Email Gateway (Aug 19 2022 at 12:46): Email Gateway (Aug 19 2022 at 12:46):From: Walther Neuper <wneuper@ist.tugraz.at>
While studying /doc/locales.pdf, /doc/isar-ref.pdf and and code in
Vector_Space.thy I got stuck with evaluating definitions occurring
within locale:
locale lll =
fixes fff :: "int ⇒ int ⇒ int"
assumes ccc: "fff a b = fff b a"
begin
lemma aaa [code]: "fff a b = a + b"
sorry
value "fff 1 2" --{*"fff 1 2" :: "int" --- EXPECT "3" HERE *}
end
Question:
What am I missing in order to get
value "fff 1 2" --{"3" :: "int"}
Thanks for patience with this question,
Walther
PS: For pointers into ~~/doc I'd particularly grateful.
Locale_Value.thy
Email Gateway (Aug 19 2022 at 12:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Walter,
The code generator has not (yet) been localized, so it does not work well with locales. In
particular, you cannot declare code equations for fixed parameters. More precisely, the
declaration aaa[code] comes in effect whenever you interpret your locale. Only then, your
delcaration aaa [code] (with fff instantiated to some term t as specified in the
interpretation) executes, i.e., you get the same as if you write
lemma [code]: "t a b = a + b"
Inside the locale, however, [code] does not have any effect. Unfortunately, I do not know
of any documentation about this. In [1, Sect. 2.2], I discuss some limitations of the code
generator with locales, but this does not cover your case.
Hope this helps,
Andreas
[1] http://www.infsec.ethz.ch/people/andreloc/publications/lochbihler11itp.pdf
Email Gateway (Aug 19 2022 at 12:47):From: Walther Neuper <wneuper@ist.tugraz.at>
On 11/07/2013 12:07 PM, Andreas Lochbihler wrote:
Hope this helps,
it does, thank you very much !
Andreas
Walther
Last updated: Apr 16 2024 at 12:28 UTC