author | wenzelm |
Wed, 10 Oct 2012 15:21:26 +0200 | |
changeset 49754 | acafcac41690 |
parent 42814 | 5af15f1e2ef6 |
child 50126 | 3dec88149176 |
permissions | -rw-r--r-- |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
1 |
(* Title: HOL/ex/Iff_Oracle.thy |
1537 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
3 |
Author: Makarius |
1537 | 4 |
*) |
5 |
||
16832 | 6 |
header {* Example of Declaring an Oracle *} |
16063 | 7 |
|
29752 | 8 |
theory Iff_Oracle |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
9 |
imports Main |
16832 | 10 |
begin |
3817 | 11 |
|
16832 | 12 |
subsection {* Oracle declaration *} |
13 |
||
14 |
text {* |
|
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
15 |
This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}. |
16832 | 16 |
The length is specified by an integer, which is checked to be even |
17 |
and positive. |
|
18 |
*} |
|
3817 | 19 |
|
28290 | 20 |
oracle iff_oracle = {* |
16832 | 21 |
let |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
22 |
fun mk_iff 1 = Var (("P", 0), @{typ bool}) |
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
23 |
| mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1)); |
16832 | 24 |
in |
28290 | 25 |
fn (thy, n) => |
16832 | 26 |
if n > 0 andalso n mod 2 = 0 |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
27 |
then Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_iff n)) |
16832 | 28 |
else raise Fail ("iff_oracle: " ^ string_of_int n) |
29 |
end |
|
30 |
*} |
|
3817 | 31 |
|
16832 | 32 |
|
33 |
subsection {* Oracle as low-level rule *} |
|
3817 | 34 |
|
28290 | 35 |
ML {* iff_oracle (@{theory}, 2) *} |
36 |
ML {* iff_oracle (@{theory}, 10) *} |
|
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
37 |
ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *} |
16832 | 38 |
|
21863 | 39 |
text {* These oracle calls had better fail. *} |
3817 | 40 |
|
16832 | 41 |
ML {* |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
42 |
(iff_oracle (@{theory}, 5); error "Bad oracle") |
23153 | 43 |
handle Fail _ => warning "Oracle failed, as expected" |
16832 | 44 |
*} |
3817 | 45 |
|
16832 | 46 |
ML {* |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
36960
diff
changeset
|
47 |
(iff_oracle (@{theory}, 1); error "Bad oracle") |
23153 | 48 |
handle Fail _ => warning "Oracle failed, as expected" |
16832 | 49 |
*} |
3817 | 50 |
|
16832 | 51 |
|
52 |
subsection {* Oracle as proof method *} |
|
3817 | 53 |
|
16832 | 54 |
method_setup iff = {* |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
30719
diff
changeset
|
55 |
Scan.lift Parse.nat >> (fn n => fn ctxt => |
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
29752
diff
changeset
|
56 |
SIMPLE_METHOD |
42361 | 57 |
(HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n))) |
16832 | 58 |
handle Fail _ => no_tac)) |
42814 | 59 |
*} |
3817 | 60 |
|
16832 | 61 |
|
62 |
lemma "A <-> A" |
|
63 |
by (iff 2) |
|
3817 | 64 |
|
16832 | 65 |
lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A" |
66 |
by (iff 10) |
|
67 |
||
68 |
lemma "A <-> A <-> A <-> A <-> A" |
|
69 |
apply (iff 5)? |
|
70 |
oops |
|
71 |
||
72 |
lemma A |
|
73 |
apply (iff 1)? |
|
74 |
oops |
|
3817 | 75 |
|
16063 | 76 |
end |