src/Pure/Isar/skip_proof.ML
author wenzelm
Thu Apr 21 22:02:06 2005 +0200 (2005-04-21 ago)
changeset 15801 d2f5ca3c048d
parent 15667 b7bdc1651198
child 15831 aa58e4ec3a1f
permissions -rw-r--r--
superceded by Pure.thy and CPure.thy;
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@8539
     5
Skipping proofs -- quick_and_dirty mode.
wenzelm@6888
     6
*)
wenzelm@6888
     7
wenzelm@6888
     8
signature SKIP_PROOF =
wenzelm@6888
     9
sig
wenzelm@8539
    10
  val quick_and_dirty: bool ref
wenzelm@11892
    11
  val make_thm: theory -> term -> thm
wenzelm@11892
    12
  val cheat_tac: theory -> tactic
wenzelm@11972
    13
  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
wenzelm@12148
    14
  val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
wenzelm@12318
    15
    (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@12318
    16
  val global_skip_proof:
wenzelm@12318
    17
    bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
wenzelm@6888
    18
end;
wenzelm@6888
    19
wenzelm@6888
    20
structure SkipProof: SKIP_PROOF =
wenzelm@6888
    21
struct
wenzelm@6888
    22
wenzelm@6888
    23
wenzelm@8539
    24
(* quick_and_dirty *)
wenzelm@8539
    25
wenzelm@8539
    26
(*if true then some packages will OMIT SOME PROOFS*)
wenzelm@8539
    27
val quick_and_dirty = ref false;
wenzelm@8539
    28
wenzelm@8539
    29
wenzelm@11892
    30
(* oracle setup *)
wenzelm@6888
    31
wenzelm@6888
    32
val skip_proofN = "skip_proof";
wenzelm@6888
    33
wenzelm@11892
    34
exception SkipProof of term;
wenzelm@6888
    35
wenzelm@11892
    36
fun skip_proof (_, SkipProof t) =
wenzelm@11892
    37
  if ! quick_and_dirty then t
wenzelm@12318
    38
  else error "Proof may be skipped in quick_and_dirty mode only!";
wenzelm@6888
    39
wenzelm@15801
    40
val _ = Context.add_setup
wenzelm@15801
    41
 [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
wenzelm@6888
    42
wenzelm@11892
    43
wenzelm@11972
    44
(* basic cheating *)
wenzelm@11892
    45
wenzelm@11892
    46
fun make_thm thy t =
wenzelm@15667
    47
  Thm.invoke_oracle_i thy skip_proofN (Theory.sign_of thy, SkipProof t);
wenzelm@11892
    48
wenzelm@8539
    49
fun cheat_tac thy st =
wenzelm@11892
    50
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888
    51
wenzelm@11972
    52
fun prove thy xs asms prop tac =
wenzelm@11972
    53
  Tactic.prove (Theory.sign_of thy) xs asms prop
wenzelm@11972
    54
    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
wenzelm@11972
    55
wenzelm@6888
    56
wenzelm@8539
    57
(* "sorry" proof command *)
wenzelm@8539
    58
wenzelm@12318
    59
fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
wenzelm@12318
    60
    (cheat_tac (ProofContext.theory_of ctxt))));
wenzelm@8539
    61
skalberg@15531
    62
fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), NONE) x;
skalberg@15531
    63
fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), NONE);
wenzelm@8539
    64
wenzelm@6888
    65
end;
wenzelm@8539
    66
wenzelm@8539
    67
wenzelm@8539
    68
val quick_and_dirty = SkipProof.quick_and_dirty;