TWiki> PG Web>IsabellePGPlans (revision 1)EditAttach

Plans for extending Proof General support in Isabelle

These notes are based on discussions of DavidAspinall and MakariusWenzel at MKM2006.

Extending Isabelle with "Proof Obligations"


  • sorry <id> to save current state
  • resume <id> to restore an earlier (or later?) saved state

This allows the interface to fill in subproofs by generating identifiers and issuing "sorry" behind the scenes. In the editor it might be displayed as a red ellipsis.

Claim: this should work cleanly on Isar because sub-proofs are really independent.

Record of saved states seems to become part of proof state?

Proof construction wizards with templates/outline

Idea: Isabelle can output templates which are filled in in the Interface.

E.g. print induct displays template with sorry (proof obligations) in subproofs.

So in fact we already always have complete proofs.

Cf. Agda-style interface

This should be combined with PG-Win opcmd

Here we would like to have more kinds of holes: holes for terms, facts, etc. Maybe special identifiers here: syntactically legal but nonsense (DUMMY term, type, _/nothing fact, etc).

Of course: holes need to be marked up for interface.

Suggestion: just find these by regexps, BUT then the interface cannot know the types of the holes (unless separate regexps for each type, etc). BETTER seems if system can add PGIP markup for holes, so we can know them (and not care about their text content):

      <hole objtype="term">   </hole>

Parsing proof scripts with meta-information

We'd like to get some intentional information from commands within proof scripts, especially:

  • names of identifiers that are bound
  • names of identifiers that are referenced

Is it possible to have a lightweight execution which does not execute proofs but does calculate name bindings, etc?

Alternatively (or as an interim), we should provide this information during normal processing, when Proof General can cache it (conceptually or actually, adding it to the PGIP markup of the source text).

** Idea of continuous

Printing proof scripts

If we had real parse trees for Isar scripts, then we could generate, manipulate and print them to make Isar source texts.


  • Larry wants this for constructing scripts containing proofs generated automatically by resolution provers.
  • Lucas wants this for proof planning. Note that the planning refinement involves a potentially expensive undo-redo cycle where we change the outline "proof sketch". Seems possible to support this wholly in the interface, though.
  • David probably needs this for forms of refactoring and proof patterns (similar to Bundy/Dixon's plans to investigate planning in-the-large)

Question: how can we support this kind of thing without having canonical ways of generating texts? (Possibly: the opcmd mechanism of the interface)

Annotations in inner syntax

Would be highly desirable to have a way of passing annotations to the print engine. Annotations are typically used to refer back to abstract syntax.

Alternative/additionally: if we can manipulate that abstract syntax directly via a special "raw term" print mode parser, we may recover a robust input syntax. This could be used by the interface to construct terms to send to Isabelle, e.g. to make instantiations or to search for matching theorems. However the "raw term" mode probably wouldn't be desirable for inclusion in source scripts.

Cf Matita design for bidirectional transformations between view and source. They describe "three formats": content level [semantics], presentation level [MathML], interchange level [XML].

Edit | Attach | Print version | History: r4 < r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 21 Aug 2006 - 16:35:54 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies