Email Gateway (Aug 18 2022 at 13:25): Email Gateway (Aug 18 2022 at 13:25):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
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.
This does not occur in Isabelle2009, there I cannot see whether my
statements depend on some unproven lemmas or not.
How can I enable this feature also in version 2009 ?
Best,
Peter
Email Gateway (Aug 18 2022 at 13:26):From: Makarius <makarius@sketis.net>
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 [!]
Makarius
Last updated: May 03 2024 at 04:19 UTC