Re: [isabelle] Verify the legitimacy of a proof?
On 07/07/17 18:37, scott constable wrote:
> Let's suppose I have some lemma
> lemma ComplexProperty: "something interesting"
> whose proof cites numerous other lemmas in other .thy files, possibly
> written by other persons with malicious intentions. Is there a command in
> Isabelle which I could use to determine the legitimacy of the entire proof
> tree of ComplexProperty? That is, I want to ensure that no lemma in the
> proof tree ended with "sorry", or if any axioms were used, I want to know
> which ones, etc.
Back to the very start. This is how I usually do it:
* Everything needs to work cleanly with "isabelle build" in batch
mode, with default options (no quick_and_dirty).
* Superficial inspection of syntax. The substring "axiomatization"
points to most ways to use axioms in practice (but very obscure
* Inspection if add-on Isabelle/ML setup is used (normally not
required at all).
* Inspection of definitions, statements, proofs (preferably in
structured Isar). Does it all "make sense", "look reasonable" etc.?
The latter is often the main problem: definitions that are not what one
would expect or like to see, or proofs that don't expose the reasoning
In that sense, I would say that a "legitimate" proof needs to be one
that is nicely structured and presented, based on clear definitions.
Extra points for proofs that are checked reasonably fast.
This archive was generated by a fusion of
Pipermail (Mailman edition) and