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

[Lukas Bulwahn]

Hi Andreas,


the following ML line should do the job of adding the congruence rule in 
your case:

setup {* Code_Preproc.map_pre (fn ss => ss addcongs [@{thm conj_cong}]) *}

Before we add yet another feature to the code generation setup in Isar, 
we would like to understand your scenario.
Does it occur naturally when setting up the code generator or is it a 
very special corner case in your specifications?


Lukas


On 05/29/2011 04:44 PM, Tobias Nipkow wrote:
> 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
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>