author | wenzelm |
Wed, 27 Mar 2013 14:19:18 +0100 | |
changeset 51551 | 88d1d19fb74f |
parent 46045 | src/Pure/Isar/skip_proof.ML@332cb37cfcee |
child 51552 | c713c9505f68 |
permissions | -rw-r--r-- |
51551 | 1 |
(* Title: Pure/skip_proof.ML |
2 |
Author: Makarius |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
3 |
|
51551 | 4 |
Skip proof via oracle invocation. |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
5 |
*) |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
6 |
|
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
7 |
signature SKIP_PROOF = |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
8 |
sig |
51551 | 9 |
val report: Proof.context -> unit |
42409 | 10 |
val make_thm_cterm: cterm -> thm |
11892 | 11 |
val make_thm: theory -> term -> thm |
12 |
val cheat_tac: theory -> tactic |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
13 |
end; |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
14 |
|
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32966
diff
changeset
|
15 |
structure Skip_Proof: SKIP_PROOF = |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
16 |
struct |
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
17 |
|
51551 | 18 |
(* report *) |
19 |
||
20 |
fun report ctxt = |
|
21 |
Context_Position.if_visible ctxt Output.report |
|
22 |
(Markup.markup Markup.bad "Skipped proof"); |
|
23 |
||
24 |
||
11892 | 25 |
(* oracle setup *) |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
26 |
|
42409 | 27 |
val (_, make_thm_cterm) = |
28 |
Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I))); |
|
29 |
||
30 |
fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop); |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
31 |
|
11892 | 32 |
|
51551 | 33 |
(* cheat_tac *) |
11892 | 34 |
|
8539 | 35 |
fun cheat_tac thy st = |
51551 | 36 |
ALLGOALS (rtac (make_thm thy (Var (("A", 0), propT)))) st; |
26530 | 37 |
|
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset
|
38 |
end; |