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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
