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