src/Pure/Isar/skip_proof.ML
author wenzelm
Fri Dec 12 12:14:02 2008 +0100 (2008-12-12 ago)
changeset 29088 95a239a5e055
parent 28552 f8719bcc5006
child 29435 a5f84ac14609
permissions -rw-r--r--
future proofs: more robust check via Future.enabled;
     1 (*  Title:      Pure/Isar/skip_proof.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Skipping proofs -- quick_and_dirty mode.
     6 *)
     7 
     8 signature SKIP_PROOF =
     9 sig
    10   val make_thm: theory -> term -> thm
    11   val cheat_tac: theory -> tactic
    12   val prove: Proof.context -> string list -> term list -> term ->
    13     ({prems: thm list, context: Proof.context} -> tactic) -> thm
    14   val prove_global: theory -> string list -> term list -> term ->
    15     ({prems: thm list, context: Proof.context} -> tactic) -> thm
    16 end;
    17 
    18 structure SkipProof: SKIP_PROOF =
    19 struct
    20 
    21 (* oracle setup *)
    22 
    23 val (_, skip_proof) = Context.>>> (Context.map_theory_result
    24   (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
    25     if ! quick_and_dirty then Thm.cterm_of thy prop
    26     else error "Proof may be skipped in quick_and_dirty mode only!")));
    27 
    28 
    29 (* basic cheating *)
    30 
    31 fun make_thm thy prop = skip_proof (thy, prop);
    32 
    33 fun cheat_tac thy st =
    34   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    35 
    36 fun prove ctxt xs asms prop tac =
    37   (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
    38     (fn args => fn st =>
    39       if ! quick_and_dirty
    40       then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
    41       else tac args st);
    42 
    43 fun prove_global thy xs asms prop tac =
    44   Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
    45 
    46 end;