1 (* Title: Pure/Isar/skip_proof.ML |
1 (* Title: Pure/Isar/skip_proof.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Skip subproofs (for quick_and_dirty mode only). |
5 Skipping proofs -- quick_and_dirty mode. |
6 *) |
6 *) |
7 |
7 |
8 signature SKIP_PROOF = |
8 signature SKIP_PROOF = |
9 sig |
9 sig |
|
10 val quick_and_dirty: bool ref |
10 val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) |
11 val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) |
11 -> Proof.state -> Proof.state Seq.seq |
12 -> Proof.state -> Proof.state Seq.seq |
12 val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} |
13 val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} |
|
14 val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm |
13 val setup: (theory -> theory) list |
15 val setup: (theory -> theory) list |
14 end; |
16 end; |
15 |
17 |
16 structure SkipProof: SKIP_PROOF = |
18 structure SkipProof: SKIP_PROOF = |
17 struct |
19 struct |
18 |
20 |
19 |
21 |
20 (* oracle *) |
22 (* quick_and_dirty *) |
|
23 |
|
24 (*if true then some packages will OMIT SOME PROOFS*) |
|
25 val quick_and_dirty = ref false; |
|
26 |
|
27 |
|
28 (* cheat_tac *) |
21 |
29 |
22 val skip_proofN = "skip_proof"; |
30 val skip_proofN = "skip_proof"; |
23 |
31 |
24 exception SkipProof; |
32 exception SkipProof; |
25 val any_prop = Var (("A", 0), propT); |
33 val any_prop = Var (("A", 0), propT); |
27 fun any_thm (_, SkipProof) = |
35 fun any_thm (_, SkipProof) = |
28 if ! quick_and_dirty then any_prop |
36 if ! quick_and_dirty then any_prop |
29 else error "Proofs may be skipped in quick_and_dirty mode only!"; |
37 else error "Proofs may be skipped in quick_and_dirty mode only!"; |
30 |
38 |
31 |
39 |
32 (* proof command *) |
40 (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*) |
33 |
41 fun cheat_tac thy st = |
34 fun cheat_meth ctxt = |
42 ALLGOALS (Tactic.rtac (Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof))) st; |
35 let |
|
36 val thy = ProofContext.theory_of ctxt; |
|
37 (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*) |
|
38 val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof); |
|
39 in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end; |
|
40 |
|
41 val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth, None); |
|
42 val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth, None); |
|
43 |
43 |
44 |
44 |
45 (* proof command *) |
45 (* "sorry" proof command *) |
|
46 |
|
47 fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt))); |
|
48 |
|
49 val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None); |
|
50 val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None); |
|
51 |
|
52 |
|
53 (* conditional prove_goalw_cterm *) |
|
54 |
|
55 fun prove_goalw_cterm thy rews ct tacs = |
|
56 Goals.prove_goalw_cterm rews ct |
|
57 (if ! quick_and_dirty then (K [cheat_tac thy]) else tacs); |
46 |
58 |
47 |
59 |
48 (* theory setup *) |
60 (* theory setup *) |
49 |
61 |
50 val setup = [Theory.add_oracle (skip_proofN, any_thm)]; |
62 val setup = [Theory.add_oracle (skip_proofN, any_thm)]; |
51 |
63 |
52 |
64 |
53 end; |
65 end; |
|
66 |
|
67 |
|
68 val quick_and_dirty = SkipProof.quick_and_dirty; |