src/Pure/Isar/skip_proof.ML
author wenzelm
Fri Aug 31 18:46:37 2007 +0200 (2007-08-31 ago)
changeset 24502 8d5326f0098b
parent 20289 ba7a7c56bed5
child 26435 bdce320cd426
permissions -rw-r--r--
prove: setmp quick_and_dirty (avoids race condition);
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@6888
     8
signature SKIP_PROOF =
wenzelm@6888
     9
sig
wenzelm@11892
    10
  val make_thm: theory -> term -> thm
wenzelm@11892
    11
  val cheat_tac: theory -> tactic
wenzelm@20289
    12
  val prove: Proof.context -> string list -> term list -> term ->
wenzelm@20289
    13
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
wenzelm@6888
    14
end;
wenzelm@6888
    15
wenzelm@6888
    16
structure SkipProof: SKIP_PROOF =
wenzelm@6888
    17
struct
wenzelm@6888
    18
wenzelm@11892
    19
(* oracle setup *)
wenzelm@6888
    20
wenzelm@11892
    21
exception SkipProof of term;
wenzelm@6888
    22
wenzelm@17362
    23
fun skip_proof (_, SkipProof prop) =
wenzelm@17362
    24
  if ! quick_and_dirty then prop
wenzelm@12318
    25
  else error "Proof may be skipped in quick_and_dirty mode only!";
wenzelm@6888
    26
wenzelm@18708
    27
val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
wenzelm@6888
    28
wenzelm@11892
    29
wenzelm@11972
    30
(* basic cheating *)
wenzelm@11892
    31
wenzelm@17362
    32
fun make_thm thy prop =
wenzelm@17362
    33
  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof 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@24502
    39
  Goal.prove ctxt xs asms prop (fn args => fn st =>
wenzelm@24502
    40
    if ! quick_and_dirty
wenzelm@24502
    41
    then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
wenzelm@24502
    42
    else tac args st);
wenzelm@11972
    43
wenzelm@6888
    44
end;