src/Pure/skip_proof.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59498 50b60f501b05
child 59621 291934bac95e
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 (*  Title:      Pure/skip_proof.ML
     2     Author:     Makarius
     3 
     4 Skip proof via oracle invocation.
     5 *)
     6 
     7 val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
     8 val quick_and_dirty = Config.bool quick_and_dirty_raw;
     9 
    10 signature SKIP_PROOF =
    11 sig
    12   val report: Proof.context -> unit
    13   val make_thm_cterm: cterm -> thm
    14   val make_thm: theory -> term -> thm
    15   val cheat_tac: Proof.context -> int -> tactic
    16 end;
    17 
    18 structure Skip_Proof: SKIP_PROOF =
    19 struct
    20 
    21 (* report *)
    22 
    23 fun report ctxt =
    24   if Context_Position.is_visible ctxt then
    25     Output.report [Markup.markup Markup.bad "Skipped proof"]
    26   else ();
    27 
    28 
    29 (* oracle setup *)
    30 
    31 val (_, make_thm_cterm) =
    32   Context.>>>
    33     (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I)));
    34 
    35 fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
    36 
    37 
    38 (* cheat_tac *)
    39 
    40 fun cheat_tac ctxt i st =
    41   resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
    42 
    43 end;