src/Pure/Isar/skip_proof.ML
author wenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14 ago)
changeset 16842 5979c46853d1
parent 15831 aa58e4ec3a1f
child 17114 8638a0a0a668
permissions -rw-r--r--
tuned;
     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 quick_and_dirty: bool ref
    11   val make_thm: theory -> term -> thm
    12   val cheat_tac: theory -> tactic
    13   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    14   val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
    15     (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
    16   val global_skip_proof:
    17     bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
    18 end;
    19 
    20 structure SkipProof: SKIP_PROOF =
    21 struct
    22 
    23 
    24 (* quick_and_dirty *)
    25 
    26 (*if true then some packages will OMIT SOME PROOFS*)
    27 val quick_and_dirty = ref false;
    28 
    29 
    30 (* oracle setup *)
    31 
    32 exception SkipProof of term;
    33 
    34 fun skip_proof (_, SkipProof t) =
    35   if ! quick_and_dirty then t
    36   else error "Proof may be skipped in quick_and_dirty mode only!";
    37 
    38 val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
    39 
    40 
    41 (* basic cheating *)
    42 
    43 fun make_thm thy t =
    44   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
    45 
    46 fun cheat_tac thy st =
    47   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    48 
    49 fun prove thy xs asms prop tac =
    50   Tactic.prove thy xs asms prop
    51     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
    52 
    53 
    54 (* "sorry" proof command *)
    55 
    56 fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
    57     (cheat_tac (ProofContext.theory_of ctxt))));
    58 
    59 fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), NONE) x;
    60 fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), NONE);
    61 
    62 end;
    63 
    64 
    65 val quick_and_dirty = SkipProof.quick_and_dirty;