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

[Andreas Lochbihler]

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:

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

-- 
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