1 (* Title: HOL/ex/Iff_Oracle.thy |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Author: Makarius |
|
4 *) |
|
5 |
|
6 section \<open>Example of Declaring an Oracle\<close> |
|
7 |
|
8 theory Iff_Oracle |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 subsection \<open>Oracle declaration\<close> |
|
13 |
|
14 text \<open> |
|
15 This oracle makes tautologies of the form \<^prop>\<open>P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P\<close>. |
|
16 The length is specified by an integer, which is checked to be even |
|
17 and positive. |
|
18 \<close> |
|
19 |
|
20 oracle iff_oracle = \<open> |
|
21 let |
|
22 fun mk_iff 1 = Var (("P", 0), \<^typ>\<open>bool\<close>) |
|
23 | mk_iff n = HOLogic.mk_eq (Var (("P", 0), \<^typ>\<open>bool\<close>), mk_iff (n - 1)); |
|
24 in |
|
25 fn (thy, n) => |
|
26 if n > 0 andalso n mod 2 = 0 |
|
27 then Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_iff n)) |
|
28 else raise Fail ("iff_oracle: " ^ string_of_int n) |
|
29 end |
|
30 \<close> |
|
31 |
|
32 |
|
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> |
|
37 |
|
38 ML \<open> |
|
39 \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]); |
|
40 \<close> |
|
41 |
|
42 text \<open>These oracle calls had better fail.\<close> |
|
43 |
|
44 ML \<open> |
|
45 (iff_oracle (\<^theory>, 5); error "Bad oracle") |
|
46 handle Fail _ => writeln "Oracle failed, as expected" |
|
47 \<close> |
|
48 |
|
49 ML \<open> |
|
50 (iff_oracle (\<^theory>, 1); error "Bad oracle") |
|
51 handle Fail _ => writeln "Oracle failed, as expected" |
|
52 \<close> |
|
53 |
|
54 |
|
55 subsection \<open>Oracle as proof method\<close> |
|
56 |
|
57 method_setup iff = |
|
58 \<open>Scan.lift Parse.nat >> (fn n => fn ctxt => |
|
59 SIMPLE_METHOD |
|
60 (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)]) |
|
61 handle Fail _ => no_tac))\<close> |
|
62 |
|
63 |
|
64 lemma "A \<longleftrightarrow> A" |
|
65 by (iff 2) |
|
66 |
|
67 lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A" |
|
68 by (iff 10) |
|
69 |
|
70 lemma "A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A \<longleftrightarrow> A" |
|
71 apply (iff 5)? |
|
72 oops |
|
73 |
|
74 lemma A |
|
75 apply (iff 1)? |
|
76 oops |
|
77 |
|
78 end |
|