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?

Hi Makarius,

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.

Jeremy

    Makarius






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