src/Pure/Isar/skip_proof.ML
author wenzelm
Mon Mar 20 18:48:12 2000 +0100 (2000-03-20 ago)
changeset 8539 3cbe48a112f7
parent 6984 26d43e26ea61
child 8807 0046be1769f9
permissions -rw-r--r--
added prove_goalw_cterm;
quick_and_dirty moved here;
     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 local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    12     -> Proof.state -> Proof.state Seq.seq
    13   val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    14   val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm
    15   val setup: (theory -> theory) list
    16 end;
    17 
    18 structure SkipProof: SKIP_PROOF =
    19 struct
    20 
    21 
    22 (* quick_and_dirty *)
    23 
    24 (*if true then some packages will OMIT SOME PROOFS*)
    25 val quick_and_dirty = ref false;
    26 
    27 
    28 (* cheat_tac *)
    29 
    30 val skip_proofN = "skip_proof";
    31 
    32 exception SkipProof;
    33 val any_prop = Var (("A", 0), propT);
    34 
    35 fun any_thm (_, SkipProof) =
    36   if ! quick_and_dirty then any_prop
    37   else error "Proofs may be skipped in quick_and_dirty mode only!";
    38 
    39 
    40 (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
    41 fun cheat_tac thy st =
    42   ALLGOALS (Tactic.rtac (Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof))) st;
    43 
    44 
    45 (* "sorry" proof command *)
    46 
    47 fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt)));
    48 
    49 val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None);
    50 val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None);
    51 
    52 
    53 (* conditional prove_goalw_cterm *)
    54 
    55 fun prove_goalw_cterm thy rews ct tacs =
    56   Goals.prove_goalw_cterm rews ct
    57     (if ! quick_and_dirty then (K [cheat_tac thy]) else tacs);
    58 
    59 
    60 (* theory setup *)
    61 
    62 val setup = [Theory.add_oracle (skip_proofN, any_thm)];
    63 
    64 
    65 end;
    66 
    67 
    68 val quick_and_dirty = SkipProof.quick_and_dirty;