src/Pure/skip_proof.ML
author wenzelm
Fri Oct 07 21:16:48 2016 +0200 (2016-10-07)
changeset 64092 95469c544b82
parent 61527 d05f3d86a758
child 64556 851ae0e7b09c
permissions -rw-r--r--
accept obscure timezone used in 2011;
     1 (*  Title:      Pure/skip_proof.ML
     2     Author:     Makarius
     3 
     4 Skip proof via oracle invocation.
     5 *)
     6 
     7 signature SKIP_PROOF =
     8 sig
     9   val report: Proof.context -> unit
    10   val make_thm_cterm: cterm -> thm
    11   val make_thm: theory -> term -> thm
    12   val cheat_tac: Proof.context -> int -> tactic
    13 end;
    14 
    15 structure Skip_Proof: SKIP_PROOF =
    16 struct
    17 
    18 (* report *)
    19 
    20 fun report ctxt =
    21   if Context_Position.is_visible ctxt then
    22     Output.report [Markup.markup Markup.bad "Skipped proof"]
    23   else ();
    24 
    25 
    26 (* oracle setup *)
    27 
    28 val (_, make_thm_cterm) =
    29   Context.>>>
    30     (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I)));
    31 
    32 fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
    33 
    34 
    35 (* cheat_tac *)
    36 
    37 fun cheat_tac ctxt i st =
    38   resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
    39 
    40 end;