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