# Re: [isabelle] Lifting variables in theorem

On Sun, 2 Feb 2014, Jeremy Dawson wrote:

`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").
`

`Yes, type thm has a back-reference to some background theory. This is its
``certificate in the sense of the LCF kernel. It is not a proper context.
``(Better forget functions like "the_context" that might still be in one of
``your ancient Isabelle versions.)
`

`In contrast, a proper context has type Proof.context, and is separate from
``type thm. When you work with formal entities (typ, term, thm) in
``Isabelle/ML, they implicitly "belong" to a ctxt: Proof.context. The
``context is required for all non-trivial operations: parsing, printing,
``advanced proof tools.
`

`If you don't have a proper context, that's bad, but there is no problem to
``get one. Just make your ML function depend on ctxt: Proof.context, and
``propagate the context you get from the Isabelle framework, e.g. in
``commands like 'method_setup'.
`

`(As usual I am speaking here of current Isabelle versions, lets say 5
``years back in time, but not 15 or 20.)
`

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

`So how about your Isabelle98-style ML tactic scripts in Isabelle2005 in
``this respect? Are they really proofs in any sense of the word? Can
``anybody read them today, lets say without struggling days or weeks to make
``Isabelle2005 run on current systems?
`

`The Proof.context was introduced shortly after Isabelle98 in order to
``support structured proofs in Isar. Later it turned out as generally
``useful concept, so after 2000 or so, more and more tools became
``context-aware. That made a big difference: before there was unsure
``tinkering with free and schematic variables by hand, never being sure if
``they could clash with other variables from the environment; afterwards
``things actually started working reliably.
`
Makarius

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