Re: [isabelle] Verify the legitimacy of a proof?

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

theory Scratch
  imports Main
  keywords "check_sorry" :: diag

ML â
val get_oracles = Proofterm.all_oracles_of o Proofterm.strip_thm o

val contains_sorry = exists (fn (a, _) => a = "Pure.skip_proof") o

fun report_sorry ctxt =
  if Context_Position.is_visible ctxt then [Markup.markup Markup.bad "Proof arises from sorry
  else ();

fun check_sorry ctxt th =
    if contains_sorry th then report_sorry ctxt else ()

fun check_sorry_cmd thm_ref st =
    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
    (Parse.thm >> (fn (th, _) => Toplevel.keep (check_sorry_cmd th)));

(* Usage: *)
lemma one_add_1_eq_3:
  "1 + 1 = 3"

check_sorry HOL.refl
check_sorry one_add_1_eq_3


On Fri, Jul 7, 2017 at 8:28 PM C. Diekmann <diekmann at> 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

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