src/Pure/Isar/skip_proof.ML
author wenzelm
Tue Apr 19 22:08:42 2011 +0200 (2011-04-19 ago)
changeset 42409 3e1e80df6a42
parent 42360 da8817d01e7c
child 46045 332cb37cfcee
permissions -rw-r--r--
added more elementary Skip_Proof.make_thm_cterm;
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@42409
    10
  val make_thm_cterm: cterm -> thm
wenzelm@11892
    11
  val make_thm: theory -> term -> thm
wenzelm@11892
    12
  val cheat_tac: theory -> tactic
wenzelm@20289
    13
  val prove: Proof.context -> string list -> term list -> term ->
wenzelm@20289
    14
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
berghofe@26530
    15
  val prove_global: theory -> string list -> term list -> term ->
wenzelm@26711
    16
    ({prems: thm list, context: Proof.context} -> tactic) -> thm
wenzelm@6888
    17
end;
wenzelm@6888
    18
wenzelm@32970
    19
structure Skip_Proof: SKIP_PROOF =
wenzelm@6888
    20
struct
wenzelm@6888
    21
wenzelm@11892
    22
(* oracle setup *)
wenzelm@6888
    23
wenzelm@42409
    24
val (_, make_thm_cterm) =
wenzelm@42409
    25
  Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
wenzelm@42409
    26
wenzelm@42409
    27
fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
wenzelm@6888
    28
wenzelm@11892
    29
wenzelm@11972
    30
(* basic cheating *)
wenzelm@11892
    31
wenzelm@8539
    32
fun cheat_tac thy st =
wenzelm@11892
    33
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
wenzelm@6888
    34
wenzelm@20049
    35
fun prove ctxt xs asms prop tac =
wenzelm@29448
    36
  (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
wenzelm@28365
    37
    (fn args => fn st =>
wenzelm@28365
    38
      if ! quick_and_dirty
wenzelm@42360
    39
      then cheat_tac (Proof_Context.theory_of ctxt) st
wenzelm@28365
    40
      else tac args st);
wenzelm@11972
    41
berghofe@26530
    42
fun prove_global thy xs asms prop tac =
wenzelm@42360
    43
  Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
berghofe@26530
    44
wenzelm@6888
    45
end;