equal
deleted
inserted
replaced
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_cterm: cterm -> thm |
|
11 val make_thm: theory -> term -> thm |
|
12 val cheat_tac: theory -> tactic |
|
13 val prove: Proof.context -> string list -> term list -> term -> |
|
14 ({prems: thm list, context: Proof.context} -> tactic) -> thm |
|
15 val prove_global: theory -> string list -> term list -> term -> |
|
16 ({prems: thm list, context: Proof.context} -> tactic) -> thm |
|
17 end; |
|
18 |
|
19 structure Skip_Proof: SKIP_PROOF = |
|
20 struct |
|
21 |
|
22 (* oracle setup *) |
|
23 |
|
24 val (_, make_thm_cterm) = |
|
25 Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I))); |
|
26 |
|
27 fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop); |
|
28 |
|
29 |
|
30 (* basic cheating *) |
|
31 |
|
32 fun cheat_tac thy st = |
|
33 ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st; |
|
34 |
|
35 fun prove ctxt xs asms prop tac = |
|
36 if ! quick_and_dirty then |
|
37 Goal.prove ctxt xs asms prop (fn _ => cheat_tac (Proof_Context.theory_of ctxt)) |
|
38 else (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop tac; |
|
39 |
|
40 fun prove_global thy xs asms prop tac = |
|
41 Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac); |
|
42 |
|
43 end; |
|