Re: [isabelle] Renaming on code-export

Hi Andreas,

thanks for the explanation. I was using this kind of lifting already to
get code generation for locale interpretations work properly. But for
whatever reason I did not see that it is also applicable here. (And this
'lifting from locales' is also just renaming ...)

- René

Am 07.01.2013 15:07, schrieb andreas.lochbihler at
> Hi Rene,
> the code generator provides no means to specify how a constant be named
> in the generated code, so you have to introduce another constant with
> the desired name and do the necessary setup yourself. Your attempt
> already pursued the right direction, but it was not complete. You must
> also transfer foo's code equation to bar:
> lemmas [code] =  foo.simps[folded bar_def] (* if foo is defined with
> primrec or fun *)
>  foo_def[folded bar_def] (* if foo is defined with definition *)
>  xxx[folded bar_def] (* if xxx is your custom code equation for foo *)
> Here's how this works:
> 1. code_unfold on an equation "lhs = rhs" tells the code generator to
> replace any lhs instance on the right-hand side of any other code
> equation with the appropriate rhs. Thus, it rewrites usages of foo to
> usages of bar.
> 2. The above addition declares foo's code equation for bar, hence bar
> becomes implemented the same way as foo would.
> Afterwards, you can even remove foo's code equations from the code
> generator setup, if you wished to do so.
> Hope this helps,
> Andreas
> Quoting René Neumann <rene.neumann at>:
>> Hi,
>> in my theories I have a fun foo, but I'd like to have it called 'bar' in
>> my SML code (in usage and definition). Is this possible in general
>> (without having to add a function bar to Isabelle with the same content
>> as foo)?
>> I tried:
>> definition "bar = foo"
>> lemma [code_unfold]: "foo = bar" by (simp add: bar_def)
>> but this did not work out as expected.
>> Thanks,
>> René

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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