Re: [isabelle] question about locales and locale parameters



Hello Brian,

Thank you for your answer. I have succeeded with one theorem, but
I am struggling with the next one now.  It is quite difficult to get it
to work. I have many parameters in the theories, and many definitions
depending on one or more parameters. As you already said, and also
discovered by myself while trying to prove the results, even safe
and clarify expand the definitions in the undesired way. What is
even worse is that these apply to all sub-goals, not only to the first one.
Is there  a way of applying a rule (auto, safe, clarify, unfold) only
to the first goal (the same way as simp works)?

Best regards,

Viorel

On 4/19/2010 5:27 PM, Brian Huffman wrote:
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.