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

[Andreas Lochbihler]

Thanks Lukas and Florian.

I guess that it *is* a corner case in my specifications, because I have a 
conditional code equation that implements one constant x in terms of another y. 
However, I use x only in the equation of another constant z which tests for the 
precondition first. At the moment, I explicitly the code equation for z with x 
replaced by y. With congruence rules, that replacement would be automated.

Since this is rather special, I am also happy with the ML setup. However, I 
recommend that an ML example be added to the code generation tutorial.

Andreas

Lukas Bulwahn schrieb:
> 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 
>>
> 

-- 
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft