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

Tobias Nipkow nipkow at in.tum.de
Sun May 29 16:44:42 CEST 2011

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?


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

More information about the isabelle-dev mailing list