src/Pure/Isar/skip_proof.ML
author haftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 23086 12320f6e2523
parent 20289 ba7a7c56bed5
child 24502 8d5326f0098b
permissions -rw-r--r--
tuned Pure/General/name_space.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 signature SKIP_PROOF =
     9 sig
    10   val make_thm: theory -> term -> thm
    11   val cheat_tac: theory -> tactic
    12   val prove: Proof.context -> string list -> term list -> term ->
    13     ({prems: thm list, context: Proof.context} -> tactic) -> thm
    14 end;
    15 
    16 structure SkipProof: SKIP_PROOF =
    17 struct
    18 
    19 (* oracle setup *)
    20 
    21 exception SkipProof of term;
    22 
    23 fun skip_proof (_, SkipProof prop) =
    24   if ! quick_and_dirty then prop
    25   else error "Proof may be skipped in quick_and_dirty mode only!";
    26 
    27 val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
    28 
    29 
    30 (* basic cheating *)
    31 
    32 fun make_thm thy prop =
    33   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
    34 
    35 fun cheat_tac thy st =
    36   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    37 
    38 fun prove ctxt xs asms prop tac =
    39   Goal.prove ctxt xs asms prop
    40     (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac);
    41 
    42 end;