Re: [isabelle] question about locales and locale parameters



Hello Viorel,

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 label constant.

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

[...]

 f = test.label (f x) (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.

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.
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.

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.

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.
Instead of using auto, you could first tell the simplifier not to use the assumptions, which leaves the local version intact.

apply(simp (no_asm_use))

In a second step, use again the simplifier to solve the remaining goal.

Hope this helps,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.