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.