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,



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"
     lemma aaa [code]: "fff a b = a + b"
     value "fff 1 2" --{*"fff 1 2" :: "int"  --- EXPECT "3" HERE *}

What am I missing in order to get

     value "fff 1 2" --{*"3" :: "int"*}

Thanks for patience with this question,

PS: For pointers into ~~/doc I'd particularly grateful.

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