author | wenzelm |
Wed, 26 Oct 2016 15:14:17 +0200 | |
changeset 64406 | 492de9062cd2 |
parent 60754 | 02924903a6fd |
child 69597 | ff784d5a5bfb |
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 |
||
59030 | 6 |
section \<open>Example of Declaring an Oracle\<close> |
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 |
|
59030 | 12 |
subsection \<open>Oracle declaration\<close> |
16832 | 13 |
|
59030 | 14 |
text \<open> |
15 |
This oracle makes tautologies of the form @{prop "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"}. |
|
16832 | 16 |
The length is specified by an integer, which is checked to be even |
17 |
and positive. |
|
59030 | 18 |
\<close> |
3817 | 19 |
|
59030 | 20 |
oracle iff_oracle = \<open> |
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 |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59030
diff
changeset
|
27 |
then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n)) |
16832 | 28 |
else raise Fail ("iff_oracle: " ^ string_of_int n) |
29 |
end |
|
59030 | 30 |
\<close> |
3817 | 31 |
|
16832 | 32 |
|
59030 | 33 |
subsection \<open>Oracle as low-level rule\<close> |
34 |
||
35 |
ML \<open>iff_oracle (@{theory}, 2)\<close> |
|
36 |
ML \<open>iff_oracle (@{theory}, 10)\<close> |
|
3817 | 37 |
|
59030 | 38 |
ML \<open> |
39 |
Thm.peek_status (iff_oracle (@{theory}, 10)); |
|
40 |
@{assert} (#oracle it); |
|
41 |
\<close> |
|
3817 | 42 |
|
59030 | 43 |
text \<open>These oracle calls had better fail.\<close> |
3817 | 44 |
|
59030 | 45 |
ML \<open> |
46 |
(iff_oracle (@{theory}, 5); error "Bad oracle") |
|
47 |
handle Fail _ => writeln "Oracle failed, as expected" |
|
48 |
\<close> |
|
49 |
||
50 |
ML \<open> |
|
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
|
51 |
(iff_oracle (@{theory}, 1); error "Bad oracle") |
59030 | 52 |
handle Fail _ => writeln "Oracle failed, as expected" |
53 |
\<close> |
|
3817 | 54 |
|
16832 | 55 |
|
59030 | 56 |
subsection \<open>Oracle as proof method\<close> |
3817 | 57 |
|
59030 | 58 |
method_setup iff = |
59 |
\<open>Scan.lift Parse.nat >> (fn n => fn ctxt => |
|
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
29752
diff
changeset
|
60 |
SIMPLE_METHOD |
60754 | 61 |
(HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)]) |
59030 | 62 |
handle Fail _ => no_tac))\<close> |
3817 | 63 |
|
16832 | 64 |
|
59030 | 65 |
lemma "A \<longleftrightarrow> A" |
16832 | 66 |
by (iff 2) |
3817 | 67 |
|
59030 | 68 |
lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A" |
16832 | 69 |
by (iff 10) |
70 |
||
59030 | 71 |
lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A" |
16832 | 72 |
apply (iff 5)? |
73 |
oops |
|
74 |
||
75 |
lemma A |
|
76 |
apply (iff 1)? |
|
77 |
oops |
|
3817 | 78 |
|
16063 | 79 |
end |