Re: [isabelle] question about locales and locale parameters



Hello,

Thank you all for answering my question. It seems that this is a delicate issue. Applying a rule (auto) in local context which takes you out from the local context,
although well motivated by the implementation, seem strange to the new user
which may not be aware of the internals. On the other hand if auto changes
the goal into a global goal, why the global simplification rules are not
used here. If auto would use these simplification rules (test.label.simps),
then this goal will be solved automatically. Moreover, I suppose
(test.label.simps) are always applicable when (label.simps) are
applicable, and using (test.label.simps) in auto would always
yield better results. If the final result contains "test.label none"
then the abbreviation would replace it back by label.

Another way I would imagine is that you would not allow results
which take you out of the local theory. Whenever you get out
of the locale you stop the proof and search for alternatives.
After all that is what you want with a locale.


  lemma second: "none = f x ==> f = label (f(x := i)) [x]";
    apply auto;

the matter is: internally, "label" (in test) is represented as
"test.label none".  Therefore the assumption "none = f x" rewrites this
to "test.label (f x)" (c.f. also
http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf).  You could call
this a misbehaviour of the simplifier.

Once "test.label none" has been unfolded to "test.label (f x)", the
local theorems (in test) are not applicable any more.  The global
foundational theorems test.label.simps etc. could be used;  however I do
recommend to avoid that unfolding from the very beginning.
I have figured out that avoiding unfolding "test.label none" to "test.label (f x)", would let me
progress with the prof. However, as I already mentioned, this is not a good
option in my case because this problem occurs in a context where the goal has many components, and auto solves all except the one from this example. It would be much easier for me to use the global rule instead of splitting the goal little by little and make
sure the unfolding "test.label none" to "test.label (f x)" does not occur.

Best regards,

Viorel





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