Re: [isabelle] question about locales and locale parameters
the definition of label in your locale test produces only one global
constant called test.label that takes all locale parameters on which the
definition depends (in your case "none") as extra parameters.
When you are inside the context of the locale, you merely see
abbreviations of the global constants with the parameters instantiated
to the fixed locale parameters, i.e. there is no local version of the
lemma second: "none = f x ==> f = label (f(x := i)) [x]";
Here, the simplifier rewrites "none" to "f x", so the local abbreviation
"label == test.label none" no longer applies.
This is why you see the global constant. Unfortunately, auto also
removes the equation "none = f x" from the assumptions because it thinks
that it would not be needed any more.
f = test.label (f x) (f(x := i)) [x]
Just like with the constants, there are local and global versions of the
theorem. For label, label.simps refers to the local version where none
is fixed as parameter. Since your goal involves the global version of
label after auto has been applied, you must also use the global version
test.label.simps for reasoning.
2. Even if they are treated as variable in second lemma I would expect
that the definition label can still be applied to test.label (f x) (f(x
:= i)) [x]
with (f x) instead on none. If that would be the case, then second lemma
should be discharged automatically.
Fortunately, your locale does not assume anything. Hence, the global
version of the defining theorem are not guarded by any locale predicate
and you can use them freely for reasoning.
Instead of using auto, you could first tell the simplifier not to use
the assumptions, which leaves the local version intact.
4. How do I prove f = test.label (f x) (f(x := i)) [x] ? I can prove
second lemma using by (case_tac "f x = none", auto) but the statement
" f = test.label (f x) (f(x := i)) [x]" occurs in a much more involved
result, and I cannot control how the simplifications are done before
getting this "unprovable" goal.
In a second step, use again the simplifier to solve the remaining goal.
Hope this helps,
Karlsruher Institut für Technologie
Adenauerring 20a, Gebäude 50.41, Raum 023
Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales
Großforschungszentrum in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and