[isabelle-dev] Declaration depending on user proofs
makarius at sketis.net
Tue Nov 2 15:11:21 CET 2010
On Thu, 7 Oct 2010, Lukas Bulwahn wrote:
> The code_pred command for the invocation of the predicate compiler could
> also fit under this umbrella.
> So the syntax would change from "code_pred" to "prove code_pred" which
> is actually better, because then users are not surprised that the
> command sets up some goal state (in most cases the empty goal) for the
> user to prove.
This scheme would be outside of Isar traditions for several reasons, such
as the naming of toplevel commands (nouns, not verbs).
BTW, the very idea of an empty goal state shown to the user belongs to the
PG interaction model. It is easy to imagine an Isar prover IDE that fills
such holes seemlessly according to the formal structure of the text. The
traditional mismatch of PG interaction and Isar structure may soon be
overcome in the new document model.
More information about the isabelle-dev