src/Pure/Isar/skip_proof.ML
author wenzelm
Sun Feb 07 19:33:34 2010 +0100 (2010-02-07 ago)
changeset 35021 c839a4c670c6
parent 32970 fbd2bb2489a8
child 36610 bafd82950e24
permissions -rw-r--r--
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm@6888
     1
(*  Title:      Pure/Isar/skip_proof.ML
wenzelm@6888
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6888
     3
wenzelm@32970
     4
Skipping proofs -- via oracle (in quick and dirty mode) or by forking
wenzelm@32970
     5
(parallel mode).
wenzelm@6888
     6
*)
wenzelm@6888
     7
wenzelm@6888
     8
signature SKIP_PROOF =
wenzelm@6888
     9
sig
wenzelm@11892
    10
  val make_thm: theory -> term -> thm
wenzelm@11892
    11
  val cheat_tac: theory -> tactic
wenzelm@20289
    12
  val prove: Proof.context -> string list -> term list -> term ->
wenzelm@20289
    13
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
berghofe@26530
    14
  val prove_global: theory -> string list -> term list -> term ->
wenzelm@26711
    15
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
wenzelm@6888
    16
end;
wenzelm@6888
    17
wenzelm@32970
    18
structure Skip_Proof: SKIP_PROOF =
wenzelm@6888
    19
struct
wenzelm@6888
    20
wenzelm@11892
    21
(* oracle setup *)
wenzelm@6888
    22
wenzelm@28290
    23
val (_, skip_proof) = Context.>>> (Context.map_theory_result
wenzelm@32970
    24
  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
wenzelm@6888
    25
wenzelm@11892
    26
wenzelm@11972
    27
(* basic cheating *)
wenzelm@11892
    28
wenzelm@28290
    29
fun make_thm thy prop = skip_proof (thy, prop);
wenzelm@11892
    30
wenzelm@8539
    31
fun cheat_tac thy st =
wenzelm@11892
    32
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888
    33
wenzelm@20049
    34
fun prove ctxt xs asms prop tac =
wenzelm@29448
    35
  (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
wenzelm@28365
    36
    (fn args => fn st =>
wenzelm@28365
    37
      if ! quick_and_dirty
wenzelm@32970
    38
      then cheat_tac (ProofContext.theory_of ctxt) st
wenzelm@28365
    39
      else tac args st);
wenzelm@11972
    40
berghofe@26530
    41
fun prove_global thy xs asms prop tac =
wenzelm@35021
    42
  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
berghofe@26530
    43
wenzelm@6888
    44
end;