Re: [isabelle] question about locales and locale parameters
Thank you all for answering my question. It seems that this is a
Applying a rule (auto) in local context which takes you out from the
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.
I have figured out that avoiding unfolding "test.label none" to
"test.label (f x)", would let me
lemma second: "none = f x ==> f = label (f(x := i)) [x]";
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and