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
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
>



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