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