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