*To*: "C. Diekmann" <diekmann at in.tum.de>, scott constable <sdconsta at syr.edu>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Simon Wimmer <wimmersimon at gmail.com>*Date*: Sat, 08 Jul 2017 10:47:36 +0000*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAGbqCMxFwASJH4ympZ589fVua9-kX0qs4K-HAb1z5XgSPg2=Bw@mail.gmail.com>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <CAGbqCMxFwASJH4ympZ589fVua9-kX0qs4K-HAb1z5XgSPg2=Bw@mail.gmail.com>

Hi Scott, you can also check which oracles a theorem depends on from the ML level. A hack to look for the oracle that is used to implement sorry can look like this: theory Scratch imports Main keywords "check_sorry" :: diag begin ML â val get_oracles = Proofterm.all_oracles_of o Proofterm.strip_thm o Thm.proof_body_of val contains_sorry = exists (fn (a, _) => a = "Pure.skip_proof") o get_oracles fun report_sorry ctxt = if Context_Position.is_visible ctxt then Output.report [Markup.markup Markup.bad "Proof arises from sorry oracle!"] else (); fun check_sorry ctxt th = if contains_sorry th then report_sorry ctxt else () fun check_sorry_cmd thm_ref st = let val ctxt = Toplevel.context_of st val th = Proof_Context.get_fact_single ctxt thm_ref in check_sorry ctxt th end val _ = Outer_Syntax.command @{command_keyword check_sorry} "Check theorem for sorry" (Parse.thm >> (fn (th, _) => Toplevel.keep (check_sorry_cmd th))); â (* Usage: *) lemma one_add_1_eq_3: "1 + 1 = 3" sorry check_sorry HOL.refl check_sorry one_add_1_eq_3 Cheers, Simon On Fri, Jul 7, 2017 at 8:28 PM C. Diekmann <diekmann at in.tum.de> wrote: > > That is, I want to ensure that no lemma in the > > proof tree ended with "sorry", > > If you make a command line run with `isabelle build`, every use of `sorry` > is counted as cheating and makes the build fail (but only at the end of the > build, not at the time when the thy with the sorry is processed). > > This raises a new question: can I enable cheating (quick_and_dirty) mode in > a command line build? > > One question answered, one not answered, one new problem ;-) > > Cheers, > Cornelius >

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

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

**Re: [isabelle] Verify the legitimacy of a proof?***From:*C. Diekmann

- 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