# [isabelle] Assumptions of auxiliary context in other contexts

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Assumptions of auxiliary context in other contexts
*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>
*Date*: Wed, 06 Jun 2012 13:10:49 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

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 ..
end
thm L
end

`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" ..
end
thm L
end
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?
`
Andreas
--
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
http://pp.info.uni-karlsruhe.de

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