Re: [isabelle] values from locales



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


On 07/11/13 11:41, Walther Neuper wrote:
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.




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