[isabelle] Assumptions of auxiliary context in other contexts

Hi all,

I want to nest an auxiliary context inside another local context to factor out a bunch of assumptions. The assumptions should refer to fixed parameters of the surrounding context, like in the following example:

locale l = fixes n :: nat begin
context assumes n: "n ~= 0" begin
lemma L: True ..
thm L

Unfortunately, thm L refers to "(!!n. n ~= 0) ==> True" instead of "n ~= 0 ==> True", i.e., the assumption n generalises over n instead of taking it as a fixed parameter. Consequently, L's assumption is unprovable and therefore L unusable.

How can I refer to the fixed parameter n of the surrounding context in the assumption n?

I tried the following:

locale l = fixes n :: nat begin
definition n' where "n' = n"
context assumes n: "n' ~= 0" begin
lemma L: "True" ..
thm L

But thm L still contains the unprovable assumption: "(!!n. L.n' n = 0) ==> True"

By the way: The Isar/Ref manual mentions that unnamed contexts may be nested within other targets and mentions locales, type classes etc. as examples. May I also nest unnamed contexts inside unnamed contexts? Isabelle2012 does not complain, if I do so, but is this officially supported?


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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