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

[Lukas Bulwahn]

On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
> Hi Lukas,
>
> here is an example that I would have expected to work. However, 
> congruences seem to work other than I expected. Du you know what I am 
> missing here?
>
> theory Scratch imports Main begin
> definition test where "test xs = (last xs = 0)"
> definition test2 where "test2 xs = (xs ~= [] & test (rev xs))"
>
> (* Optimized implementation for test with context condition *)
> lemma test_rev: "xs ~= [] ==> test (rev xs) = (hd xs = 0)"
> unfolding test_def by(simp add: last_rev)
>
> declare conj_cong[cong] test_rev[simp]
> thm test2_def test2_def[simplified]
>
> lemma "test2 xs = (xs ~= [] & test (rev xs))"
> apply simp
> oops
>
> The [simplified] attribute does apply the test_rev equation, but the 
> simp method in the proof does. Apparently, the same issue prevents the 
> code preprocessor from optimizing the code for test:
>
The simplifier behaves differently when working with free variables or 
schematic variables.
Tobias can probably give a more precise answer how it behaves 
differently (and why).

I will change the code preprocessor, so that you get the intended behaviour.

It might be worth discussing if the simplified attribute should be 
changed to do the same thing.


Lukas


> lemmas [code_inline] = test_rev test_rev[folded List.null_def]
> setup {* Code_Preproc.map_pre (fn ss => ss addcongs [@{thm 
> conj_cong}]) *}
> code_thms test2
>
> test2 is still implemented in terms of "test (rev xs)"
>
> How can I unfold test_rev in test2_def?
>

> Andreas
>