src/Pure/Isar/skip_proof.ML
author wenzelm
Tue Sep 13 22:19:47 2005 +0200 (2005-09-13 ago)
changeset 17362 c089fa02c1e5
parent 17114 8638a0a0a668
child 17476 315cb57e3dd7
permissions -rw-r--r--
load before proof.ML;
moved proof elements to proof.ML;
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@17362
     8
(*if true then some tools will OMIT some proofs*)
wenzelm@17362
     9
val quick_and_dirty = ref false;
wenzelm@17362
    10
wenzelm@6888
    11
signature SKIP_PROOF =
wenzelm@6888
    12
sig
wenzelm@11892
    13
  val make_thm: theory -> term -> thm
wenzelm@11892
    14
  val cheat_tac: theory -> tactic
wenzelm@11972
    15
  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
wenzelm@6888
    16
end;
wenzelm@6888
    17
wenzelm@6888
    18
structure SkipProof: SKIP_PROOF =
wenzelm@6888
    19
struct
wenzelm@6888
    20
wenzelm@11892
    21
(* oracle setup *)
wenzelm@6888
    22
wenzelm@11892
    23
exception SkipProof of term;
wenzelm@6888
    24
wenzelm@17362
    25
fun skip_proof (_, SkipProof prop) =
wenzelm@17362
    26
  if ! quick_and_dirty then prop
wenzelm@12318
    27
  else error "Proof may be skipped in quick_and_dirty mode only!";
wenzelm@6888
    28
wenzelm@15831
    29
val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
wenzelm@6888
    30
wenzelm@11892
    31
wenzelm@11972
    32
(* basic cheating *)
wenzelm@11892
    33
wenzelm@17362
    34
fun make_thm thy prop =
wenzelm@17362
    35
  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
wenzelm@11892
    36
wenzelm@8539
    37
fun cheat_tac thy st =
wenzelm@11892
    38
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888
    39
wenzelm@11972
    40
fun prove thy xs asms prop tac =
wenzelm@16842
    41
  Tactic.prove thy xs asms prop
wenzelm@11972
    42
    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
wenzelm@11972
    43
wenzelm@6888
    44
end;