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


    Makarius
Hi Makarius,

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.

Jeremy







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