Re: [isabelle] Lifting variables in theorem
On 02/01/2014 10:50 PM, Makarius wrote:
On Sat, 1 Feb 2014, Jeremy Dawson wrote:
I don't know about recent versions of Isabelle, but in Isabelle2005
the function Drule.standard does this (plus some other useful things).
I see subsequent emails in the thread talk about contexts - again I
don't know about subsequent versions of Isabelle, but in Isabelle
2005 contexts (as I understand the way the word is used nowadays) are
not part of a theorem.
No, Isabelle2005 has the same notion of global background context
(type "theory") and local proof context (type "Proof.context"), it
also has locales and other applications of local context routinely
available. The thing that is part of the thm is merely a certificate
of the background theory, not a proper context. (It is merely a
historical accident that the certificate also contains the full
background theory content, not just its identification stamp.)
Drule.standard was already disruptive to local situations in
Isabelle2005, but many more tools were not properly localized, so it
did not stand out particularly.
Starting with Isabelle2007, old things were systematically removed
under the label of "localization". That is a long story and still not
finished, but the system is continously converging to a fully local
context displiciple for all proof tools and definitional packages.
The jump from Isabelle2005 to Isabelle2007 (with 25 months distance)
also marks the point where really ancient things from the 1990-ies
were removed. This is the deeper reason why you are yourself still
stuck with it, since it is possible to pretend that it is Isabelle98.
Consequently we have every few months a thread on this mailing list to
uncover features of historic Isabelle versions that hardly anybody
Although you say "No", you seem to be agreeing with me that a theorem in
Isabelle2005 is associated with a global background context (type
"theory") and not a local proof context (type "Proof.context") (I take
it that this is the same thing as a "proper context").
More importantly you seem to regard things from the 1990-ies as really
ancient. While that may be so in the context of computer hardware, it's
not so in the context of mathematical proofs. The pen and paper
mathematical proofs I did in the 1970s are still 100% useful today, and
that's the way I want it to be.
This archive was generated by a fusion of
Pipermail (Mailman edition) and