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

[Lukas Bulwahn]

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