[isabelle-dev] [isabelle] Congruence rules for the code preprocessor

[Tobias Nipkow]

Does the current attribute mechanism support selective attributes such 
as [code_inline cong], maybe along the lines of [simp del]? If it does, 
I assume it would be easy to add that information in the place that 
Florian pointed to?

Tobias

Am 28/05/2011 14:45, schrieb Florian Haftmann:
> Hi Andreas,
>
>> the code generator tutorial mentions that "the simpset for the code
>> preprocessor can apply the full generality of the Isabelle simplifier".
>> But how can I add anything else other than unfold theorems? The
>> attributes code_unfold and code_inline do not accept declarations like
>>
>> declare conj_cong[code_inline cong]
>>
>> Is there a way in Isar to declare congruence rules to the preprocessor?
>
> no, this can only be done on the ML level, cf.
> http://isabelle.in.tum.de/reports/Isabelle/file/0f9534b7ea75/src/Tools/Code/code_preproc.ML#l10.
>
> Maybe it would be worth thinking about transfering all simpset
> declaration attributes also to code_inline.
>
> Hope this helps,
> 	Florian
>