Re: [isabelle] question about locales and locale parameters



On Mon, Apr 19, 2010 at 1:40 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi> wrote:
> Hello Brian,
>
> The trick seems to work for the test theory, but it does not work
> for my real theory. Also using the global simplification rule does not
> work for me either because I have assumptions in the locale. I have
> succeeded to strip down the example for which the cong approach
> does not work. In the third and forth lemmas the definition label
> is expanded to test.label and the proofs fail.
...
> lemma third:
>  "tl a = [] ==>  f (hd a) = none
>      ==> f = label (f(hd a := i)) a";
>  apply auto;
>  sorry;
>
> lemma forth:
>  "? y ys . a = y # ys ==> f (hd a) = none
>      ==> f = label (f(hd a := i)) a";
>  apply auto;
>  sorry;

I see what is going on here. The congruence rule successfully prevents
the *simplifier* from rewriting "label" to "test.label", but with
lemmas "third" and "forth" it is not the simplifier that is causing
the problem. Try replacing "apply auto" with either "apply safe" or
"apply clarify", and you will get the same result.

This unhelpful behavior of "safe" (which is included as part of what
"auto" does) in the context of locales has been noted before on the
mailing list:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2007-February/msg00075.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2007-February/msg00076.html

Unfortunately, while it has been acknowledged as a problem, it seems
that nothing has been done about it.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.