Re: [isabelle] Isabelle2009: Where's the [!] after lemmas that are not proven ?

On Wed, 22 Apr 2009, Peter Lammich wrote:

up to Isabelle2008, when quick-and-dirty mode was off and a lemma was "shown" with sorry, ProofGeneral showed a [!] after the lemma and all lemmas depending on it.

The "[!]" was a visual rendering of the old "oracle" flag within internal derivation objects. In Isabelle2009 there is now a more elaborate notion of "derivation status" that reflects how much of the formal proofs has actually been conducted. In particular, the standard mode of operation is already asynchronous in the sense that claims are immediately turned into theorems, and the actual proof is delivered later. (The main application at the moment is parallel proof checking in batch mode, but a more refined interface could also let the user edit proofs independently of toplevel specifications, for example.)

The thm status can be queried in ML like this:

  lemma a: A sorry

  ML {* Thm.status_of @{thm a} *}

  > val it = {failed = false, oracle = true, unfinished = false}

There is also a visual rendering as combinations of "?" and "!", but this is disabled in the toplevel goals, because it would be [?] (for "unfinished") most of the time. As long as the prover interface does not give any direct feedback on this information, you can query it manually via the plain 'thm' command:

  thm a

  > True  [!]


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