*To*: scott constable <sdconsta at syr.edu>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Makarius <makarius at sketis.net>*Date*: Sat, 8 Jul 2017 16:32:20 +0200*In-reply-to*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.1

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

**Follow-Ups**:**Re: [isabelle] Verify the legitimacy of a proof?***From:*scott constable

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

- Previous by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list