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;
     1 (*  Title:      Pure/Isar/skip_proof.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Skipping proofs -- quick_and_dirty mode.
     6 *)
     7 
     8 (*if true then some tools will OMIT some proofs*)
     9 val quick_and_dirty = ref false;
    10 
    11 signature SKIP_PROOF =
    12 sig
    13   val make_thm: theory -> term -> thm
    14   val cheat_tac: theory -> tactic
    15   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    16 end;
    17 
    18 structure SkipProof: SKIP_PROOF =
    19 struct
    20 
    21 (* oracle setup *)
    22 
    23 exception SkipProof of term;
    24 
    25 fun skip_proof (_, SkipProof prop) =
    26   if ! quick_and_dirty then prop
    27   else error "Proof may be skipped in quick_and_dirty mode only!";
    28 
    29 val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
    30 
    31 
    32 (* basic cheating *)
    33 
    34 fun make_thm thy prop =
    35   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
    36 
    37 fun cheat_tac thy st =
    38   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    39 
    40 fun prove thy xs asms prop tac =
    41   Tactic.prove thy xs asms prop
    42     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
    43 
    44 end;