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"
> ...
> done
> 
> 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
possibilities remain).

  * 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
properly.


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.


	Makarius




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