src/Pure/Isar/skip_proof.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19)
changeset 18708 4b3dadb4fe33
parent 17956 369e2af8ee45
child 20049 f48c4a3a34bc
permissions -rw-r--r--
setup: theory -> theory;
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@11972
    12
  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
wenzelm@6888
    13
end;
wenzelm@6888
    14
wenzelm@6888
    15
structure SkipProof: SKIP_PROOF =
wenzelm@6888
    16
struct
wenzelm@6888
    17
wenzelm@11892
    18
(* oracle setup *)
wenzelm@6888
    19
wenzelm@11892
    20
exception SkipProof of term;
wenzelm@6888
    21
wenzelm@17362
    22
fun skip_proof (_, SkipProof prop) =
wenzelm@17362
    23
  if ! quick_and_dirty then prop
wenzelm@12318
    24
  else error "Proof may be skipped in quick_and_dirty mode only!";
wenzelm@6888
    25
wenzelm@18708
    26
val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
wenzelm@6888
    27
wenzelm@11892
    28
wenzelm@11972
    29
(* basic cheating *)
wenzelm@11892
    30
wenzelm@17362
    31
fun make_thm thy prop =
wenzelm@17362
    32
  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
wenzelm@11892
    33
wenzelm@8539
    34
fun cheat_tac thy st =
wenzelm@11892
    35
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888
    36
wenzelm@11972
    37
fun prove thy xs asms prop tac =
wenzelm@17956
    38
  Goal.prove thy xs asms prop
wenzelm@11972
    39
    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
wenzelm@11972
    40
wenzelm@6888
    41
end;