Re: [isabelle] Lifting variables in theorem
On 02/02/2014 05:27 AM, Makarius wrote:
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?
Whether they are proofs is a question which others might debate, and
have done so, at least since the proof of the four-colour theorem, if
not before. Whether they can be read today (without running them on an
Isabelle system) - with only the greatest of difficulty. They're to be
run on an appropriate system. Reading their source is more difficult
than a document in LaTex or HTML, easier than a document in PostScript
or PDF. And I can read (on the computer) documents dating from 2005 in
all of these formats without "struggling days or weeks to make [the 2005
versions of interpreters of those languages] run on current systems".
My whole point is that it should NOT be difficult for anyone to run
proofs today which were written in 2005 (or, indeed, much earlier).
And of course if I were to write out _all_ the steps of the proofs I've
done recently, whether in Isar, or any other language without (eg)
TRYALL (EVERY' [ ....]) there would be hundreds of thousands of lines of
code, so no-one would read it anyway, so I don't actually see what your
point is in asking whether anyone can read my proofs. Isar proofs
wouldn't (and, within reason, couldn't) be read either.
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.
I'm not clear what the problem is that you are describing but it doesn't
sound like anything I have issues with in my work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and