wenzelm@6888: (*  Title:      Pure/Isar/skip_proof.ML
wenzelm@6888:     ID:         $Id$
wenzelm@6888:     Author:     Markus Wenzel, TU Muenchen
wenzelm@6888: 
wenzelm@8539: Skipping proofs -- quick_and_dirty mode.
wenzelm@6888: *)
wenzelm@6888: 
wenzelm@6888: signature SKIP_PROOF =
wenzelm@6888: sig
wenzelm@11892:   val make_thm: theory -> term -> thm
wenzelm@11892:   val cheat_tac: theory -> tactic
wenzelm@20289:   val prove: Proof.context -> string list -> term list -> term ->
wenzelm@20289:     ({prems: thm list, context: Proof.context} -> tactic) -> thm
wenzelm@6888: end;
wenzelm@6888: 
wenzelm@6888: structure SkipProof: SKIP_PROOF =
wenzelm@6888: struct
wenzelm@6888: 
wenzelm@11892: (* oracle setup *)
wenzelm@6888: 
wenzelm@11892: exception SkipProof of term;
wenzelm@6888: 
wenzelm@17362: fun skip_proof (_, SkipProof prop) =
wenzelm@17362:   if ! quick_and_dirty then prop
wenzelm@12318:   else error "Proof may be skipped in quick_and_dirty mode only!";
wenzelm@6888: 
wenzelm@18708: val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
wenzelm@6888: 
wenzelm@11892: 
wenzelm@11972: (* basic cheating *)
wenzelm@11892: 
wenzelm@17362: fun make_thm thy prop =
wenzelm@17362:   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
wenzelm@11892: 
wenzelm@8539: fun cheat_tac thy st =
wenzelm@11892:   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888: 
wenzelm@20049: fun prove ctxt xs asms prop tac =
wenzelm@20049:   Goal.prove ctxt xs asms prop
wenzelm@20049:     (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac);
wenzelm@11972: 
wenzelm@6888: end;