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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and