src/Pure/Isar/skip_proof.ML
author wenzelm
Mon Jul 12 22:28:56 1999 +0200 (1999-07-12 ago)
changeset 6984 26d43e26ea61
parent 6935 a3f3f4128cab
child 8539 3cbe48a112f7
permissions -rw-r--r--
local qed; print rule;
     1 (*  Title:      Pure/Isar/skip_proof.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Skip subproofs (for quick_and_dirty mode only).
     6 *)
     7 
     8 signature SKIP_PROOF =
     9 sig
    10   val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    11     -> Proof.state -> Proof.state Seq.seq
    12   val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    13   val setup: (theory -> theory) list
    14 end;
    15 
    16 structure SkipProof: SKIP_PROOF =
    17 struct
    18 
    19 
    20 (* oracle *)
    21 
    22 val skip_proofN = "skip_proof";
    23 
    24 exception SkipProof;
    25 val any_prop = Var (("A", 0), propT);
    26 
    27 fun any_thm (_, SkipProof) =
    28   if ! quick_and_dirty then any_prop
    29   else error "Proofs may be skipped in quick_and_dirty mode only!";
    30 
    31 
    32 (* proof command *)
    33 
    34 fun cheat_meth ctxt =
    35   let
    36     val thy = ProofContext.theory_of ctxt;
    37     (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
    38     val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
    39   in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
    40 
    41 val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth, None);
    42 val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth, None);
    43 
    44 
    45 (* proof command *)
    46 
    47 
    48 (* theory setup *)
    49 
    50 val setup = [Theory.add_oracle (skip_proofN, any_thm)];
    51 
    52 
    53 end;