*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Mon, 3 Feb 2014 02:15:51 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1402011914460.25155@lxbroy10.informatik.tu-muenchen.de>*References*: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se> <52EC64E4.30405@anu.edu.au> <alpine.LNX.2.00.1402011236190.15165@lxbroy10.informatik.tu-muenchen.de> <52ED0D37.1070908@anu.edu.au> <alpine.LNX.2.00.1402011914460.25155@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130110 Thunderbird/17.0.2

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 theoremin Isabelle2005 is associated with a global background context (type"theory") and not a local proof context (type "Proof.context") (Itake it that this is the same thing as a "proper context").Yes, type thm has a back-reference to some background theory. This isits certificate in the sense of the LCF kernel. It is not a propercontext. (Better forget functions like "the_context" that might stillbe in one of your ancient Isabelle versions.)In contrast, a proper context has type Proof.context, and is separatefrom type thm. When you work with formal entities (typ, term, thm) inIsabelle/ML, they implicitly "belong" to a ctxt: Proof.context. Thecontext 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 noproblem to get one. Just make your ML function depend on ctxt:Proof.context, and propagate the context you get from the Isabelleframework, e.g. in commands like 'method_setup'.(As usual I am speaking here of current Isabelle versions, lets say 5years back in time, but not 15 or 20.)More importantly you seem to regard things from the 1990-ies asreally ancient. While that may be so in the context of computerhardware, it's not so in the context of mathematical proofs. The penand 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 Isabelle2005in this respect? Are they really proofs in any sense of the word?Can anybody read them today, lets say without struggling days or weeksto make Isabelle2005 run on current systems?

Hi Makarius,

The Proof.context was introduced shortly after Isabelle98 in order tosupport structured proofs in Isar. Later it turned out as generallyuseful concept, so after 2000 or so, more and more tools becamecontext-aware. That made a big difference: before there was unsuretinkering with free and schematic variables by hand, never being sureif they could clash with other variables from the environment;afterwards things actually started working reliably.

Jeremy

Makarius

**Follow-Ups**:**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**References**:**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

- Previous by Date: Re: [isabelle] Lifting variables in theorem
- Next by Date: [isabelle] Large bodies of knowledge
- Previous by Thread: Re: [isabelle] Lifting variables in theorem
- Next by Thread: Re: [isabelle] Lifting variables in theorem
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list