author | wenzelm |
Mon, 22 Oct 2001 18:03:49 +0200 | |
changeset 11892 | 4a8834757140 |
parent 11732 | 139aaced13f4 |
child 11972 | 15da572c3c27 |
permissions | -rw-r--r-- |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/skip_proof.ML |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
8807 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
5 |
|
8539 | 6 |
Skipping proofs -- quick_and_dirty mode. |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
7 |
*) |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
8 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
9 |
signature SKIP_PROOF = |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
10 |
sig |
8539 | 11 |
val quick_and_dirty: bool ref |
11892 | 12 |
val make_thm: theory -> term -> thm |
13 |
val cheat_tac: theory -> tactic |
|
6984 | 14 |
val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
15 |
-> Proof.state -> Proof.state Seq.seq |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
16 |
val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
17 |
val setup: (theory -> theory) list |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
18 |
end; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
19 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
20 |
structure SkipProof: SKIP_PROOF = |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
21 |
struct |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
22 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
23 |
|
8539 | 24 |
(* quick_and_dirty *) |
25 |
||
26 |
(*if true then some packages will OMIT SOME PROOFS*) |
|
27 |
val quick_and_dirty = ref false; |
|
28 |
||
29 |
||
11892 | 30 |
(* oracle setup *) |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
31 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
32 |
val skip_proofN = "skip_proof"; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
33 |
|
11892 | 34 |
exception SkipProof of term; |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
35 |
|
11892 | 36 |
fun skip_proof (_, SkipProof t) = |
37 |
if ! quick_and_dirty then t |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
38 |
else error "Proofs may be skipped in quick_and_dirty mode only!"; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
39 |
|
11892 | 40 |
val setup = [Theory.add_oracle (skip_proofN, skip_proof)]; |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
41 |
|
11892 | 42 |
|
43 |
(* make_thm and cheat_tac *) |
|
44 |
||
45 |
fun make_thm thy t = |
|
46 |
(*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*) |
|
47 |
Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t); |
|
48 |
||
8539 | 49 |
fun cheat_tac thy st = |
11892 | 50 |
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st; |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
51 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
52 |
|
8539 | 53 |
(* "sorry" proof command *) |
54 |
||
55 |
fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt))); |
|
56 |
||
57 |
val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None); |
|
58 |
val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None); |
|
59 |
||
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
60 |
end; |
8539 | 61 |
|
62 |
||
63 |
val quick_and_dirty = SkipProof.quick_and_dirty; |