On 05/30/2011 06:03 PM, Lukas Bulwahn wrote:
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.
Changeset 027ed67f5d98 enables rewriting with the declared congruence rules.
In the example above, the negation still causes problems (in your
setup), but it works if you define some predicate for "xs ~= []" hiding
the negation.
Getting the setup for the code preprocessing simplifier right is of
course an exercise for its users.
It might be worth discussing if the simplified attribute should be
changed to do the same thing.
After an offline discussion with Tobias, I experimented to do the same
with the simplified attribute resulting in the following changeset:
--- a/src/Pure/simplifier.ML Tue May 31 18:29:00 2011 +0200
+++ b/src/Pure/simplifier.ML Tue May 31 18:32:58 2011 +0200
@@ -321,8 +321,8 @@
val simplified = conv_mode -- Attrib.thms >>
(fn (f, ths) => Thm.rule_attribute (fn context =>
- f ((if null ths then I else Raw_Simplifier.clear_ss)
- (simpset_of (Context.proof_of context)) addsimps ths)));
+ singleton (Variable.trade (fn ctxt => map (f ((if null ths then I
else Raw_Simplifier.clear_ss)
+ (simpset_of ctxt) addsimps ths))) (Context.proof_of context))));
end;
Unfortunately, the provided function Variable.trade renames schematic
variables (even if not necessary), making its behaviour too unexpected
for the users and causing problems with many applications in the
distribution (cf.
http://isabelle.in.tum.de/testboard/Isabelle/rev/330c709f0df9).
A Variable.trade function that at least tries to keep the same schematic
variables (in the obvious cases) would be nice for this setting. But as
long as such a function is not provided, modifying the simplified
attribute leads to problems that are not worth the benefits.
Lukas
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
