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@8539:   val quick_and_dirty: bool ref
wenzelm@11892:   val make_thm: theory -> term -> thm
wenzelm@11892:   val cheat_tac: theory -> tactic
wenzelm@11972:   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
wenzelm@12148:   val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
wenzelm@12318:     (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@12318:   val global_skip_proof:
wenzelm@12318:     bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
wenzelm@6888: end;
wenzelm@6888: 
wenzelm@6888: structure SkipProof: SKIP_PROOF =
wenzelm@6888: struct
wenzelm@6888: 
wenzelm@6888: 
wenzelm@8539: (* quick_and_dirty *)
wenzelm@8539: 
wenzelm@8539: (*if true then some packages will OMIT SOME PROOFS*)
wenzelm@8539: val quick_and_dirty = ref false;
wenzelm@8539: 
wenzelm@8539: 
wenzelm@11892: (* oracle setup *)
wenzelm@6888: 
wenzelm@11892: exception SkipProof of term;
wenzelm@6888: 
wenzelm@11892: fun skip_proof (_, SkipProof t) =
wenzelm@11892:   if ! quick_and_dirty then t
wenzelm@12318:   else error "Proof may be skipped in quick_and_dirty mode only!";
wenzelm@6888: 
wenzelm@15831: val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
wenzelm@6888: 
wenzelm@11892: 
wenzelm@11972: (* basic cheating *)
wenzelm@11892: 
wenzelm@11892: fun make_thm thy t =
wenzelm@16842:   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
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@11972: fun prove thy xs asms prop tac =
wenzelm@16842:   Tactic.prove thy xs asms prop
wenzelm@11972:     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
wenzelm@11972: 
wenzelm@6888: 
wenzelm@8539: (* "sorry" proof command *)
wenzelm@8539: 
wenzelm@12318: fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
wenzelm@12318:     (cheat_tac (ProofContext.theory_of ctxt))));
wenzelm@8539: 
skalberg@15531: fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), NONE) x;
skalberg@15531: fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), NONE);
wenzelm@8539: 
wenzelm@6888: end;
wenzelm@8539: 
wenzelm@8539: 
wenzelm@8539: val quick_and_dirty = SkipProof.quick_and_dirty;