[isabelle-dev] Declaration depending on user proofs

[Makarius]

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.


 	Makarius