*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Sat, 8 Jul 2017 12:01:28 +0100*In-reply-to*: <CAASQnwOXcZsZJ4YyoTUDXxTeZHXbLoic=fhJ5XmmE9Gv9eWmvw@mail.gmail.com>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <CAGbqCMxFwASJH4ympZ589fVua9-kX0qs4K-HAb1z5XgSPg2=Bw@mail.gmail.com> <CAASQnwOXcZsZJ4YyoTUDXxTeZHXbLoic=fhJ5XmmE9Gv9eWmvw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

Unfortunately, it is very easy to circumvent this. I don't recall who found this originally, but you can hide the âtaintâ of a theorem by going through a type class instantiation: lemma one_add_1_eq_3: "(1::nat) + 1 = 3" sorry class foo = semiring_1 + assumes foo: "1 + 1 = 3" instance nat :: foo by intro_classes (rule one_add_1_eq_3) lemmas one_add_1_eq_3' = foo [where ?'a = nat] check_sorry one_add_1_eq_3' Cheers, Manuel On 2017-07-08 11:47, Simon Wimmer wrote: > 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:*Makarius

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

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

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Simon Wimmer

- 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