author | wenzelm |
Fri, 01 Dec 2000 19:42:05 +0100 | |
changeset 10567 | e7c9900cca4d |
parent 8807 | 0046be1769f9 |
child 11732 | 139aaced13f4 |
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 |
6984 | 12 |
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
|
13 |
-> Proof.state -> Proof.state Seq.seq |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
14 |
val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} |
8539 | 15 |
val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
16 |
val setup: (theory -> theory) list |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
17 |
end; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
18 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
19 |
structure SkipProof: SKIP_PROOF = |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
20 |
struct |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
21 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
22 |
|
8539 | 23 |
(* quick_and_dirty *) |
24 |
||
25 |
(*if true then some packages will OMIT SOME PROOFS*) |
|
26 |
val quick_and_dirty = ref false; |
|
27 |
||
28 |
||
29 |
(* cheat_tac *) |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
30 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
31 |
val skip_proofN = "skip_proof"; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
32 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
33 |
exception SkipProof; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
34 |
val any_prop = Var (("A", 0), propT); |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
35 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
36 |
fun any_thm (_, SkipProof) = |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
37 |
if ! quick_and_dirty then any_prop |
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 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
40 |
|
8539 | 41 |
(*too bad -- dynamic scoping of the oracle, cannot even qualify the name*) |
42 |
fun cheat_tac thy st = |
|
43 |
ALLGOALS (Tactic.rtac (Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof))) st; |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
44 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
45 |
|
8539 | 46 |
(* "sorry" proof command *) |
47 |
||
48 |
fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt))); |
|
49 |
||
50 |
val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None); |
|
51 |
val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None); |
|
52 |
||
53 |
||
54 |
(* conditional prove_goalw_cterm *) |
|
55 |
||
56 |
fun prove_goalw_cterm thy rews ct tacs = |
|
57 |
Goals.prove_goalw_cterm rews ct |
|
58 |
(if ! quick_and_dirty then (K [cheat_tac thy]) else tacs); |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
59 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
60 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
61 |
(* theory setup *) |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
62 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
63 |
val setup = [Theory.add_oracle (skip_proofN, any_thm)]; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
64 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
65 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
66 |
end; |
8539 | 67 |
|
68 |
||
69 |
val quick_and_dirty = SkipProof.quick_and_dirty; |