src/Pure/Isar/skip_proof.ML
author wenzelm
Thu Apr 17 22:22:21 2008 +0200 (2008-04-17 ago)
changeset 26711 3a478bfa1650
parent 26530 777f334ff652
child 28290 4cc2b6046258
permissions -rw-r--r--
prove_global: pass context;
     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 exception SkipProof of term;
    24 
    25 fun skip_proof (_, SkipProof prop) =
    26   if ! quick_and_dirty then prop
    27   else error "Proof may be skipped in quick_and_dirty mode only!";
    28 
    29 val _ = Context.>> (Context.map_theory
    30   (Theory.add_oracle ("skip_proof", skip_proof)));
    31 
    32 
    33 (* basic cheating *)
    34 
    35 fun make_thm thy prop =
    36   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
    37 
    38 fun cheat_tac thy st =
    39   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    40 
    41 fun prove ctxt xs asms prop tac =
    42   Goal.prove ctxt xs asms prop (fn args => fn st =>
    43     if ! quick_and_dirty
    44     then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
    45     else tac args st);
    46 
    47 fun prove_global thy xs asms prop tac =
    48   Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
    49 
    50 end;