src/Pure/Isar/skip_proof.ML
author wenzelm
Thu Sep 25 20:34:20 2008 +0200 (2008-09-25 ago)
changeset 28365 6249297461cb
parent 28290 4cc2b6046258
child 28446 a01de3b3fa2e
permissions -rw-r--r--
added future_scheduler (from thy_info.ML);
prove: Goal.prove_promise if future_schedule;
wenzelm@6888
     1
(*  Title:      Pure/Isar/skip_proof.ML
wenzelm@6888
     2
    ID:         $Id$
wenzelm@6888
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6888
     4
wenzelm@8539
     5
Skipping proofs -- quick_and_dirty mode.
wenzelm@6888
     6
*)
wenzelm@6888
     7
wenzelm@28365
     8
val future_scheduler = ref false;
wenzelm@28365
     9
wenzelm@6888
    10
signature SKIP_PROOF =
wenzelm@6888
    11
sig
wenzelm@11892
    12
  val make_thm: theory -> term -> thm
wenzelm@11892
    13
  val cheat_tac: theory -> tactic
wenzelm@20289
    14
  val prove: Proof.context -> string list -> term list -> term ->
wenzelm@20289
    15
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
berghofe@26530
    16
  val prove_global: theory -> string list -> term list -> term ->
wenzelm@26711
    17
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
wenzelm@6888
    18
end;
wenzelm@6888
    19
wenzelm@6888
    20
structure SkipProof: SKIP_PROOF =
wenzelm@6888
    21
struct
wenzelm@6888
    22
wenzelm@11892
    23
(* oracle setup *)
wenzelm@6888
    24
wenzelm@28290
    25
val (_, skip_proof) = Context.>>> (Context.map_theory_result
wenzelm@28290
    26
  (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
wenzelm@28290
    27
    if ! quick_and_dirty then Thm.cterm_of thy prop
wenzelm@28290
    28
    else error "Proof may be skipped in quick_and_dirty mode only!")));
wenzelm@6888
    29
wenzelm@11892
    30
wenzelm@11972
    31
(* basic cheating *)
wenzelm@11892
    32
wenzelm@28290
    33
fun make_thm thy prop = skip_proof (thy, prop);
wenzelm@11892
    34
wenzelm@8539
    35
fun cheat_tac thy st =
wenzelm@11892
    36
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888
    37
wenzelm@20049
    38
fun prove ctxt xs asms prop tac =
wenzelm@28365
    39
  (if ! future_scheduler then Goal.prove_promise else Goal.prove) ctxt xs asms prop
wenzelm@28365
    40
    (fn args => fn st =>
wenzelm@28365
    41
      if ! quick_and_dirty
wenzelm@28365
    42
      then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
wenzelm@28365
    43
      else tac args st);
wenzelm@11972
    44
berghofe@26530
    45
fun prove_global thy xs asms prop tac =
wenzelm@26711
    46
  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
berghofe@26530
    47
wenzelm@6888
    48
end;