author | wenzelm |
Wed, 25 Mar 2009 17:23:44 +0100 | |
changeset 30719 | 21c20c7d1932 |
parent 30549 | d2d7874648bd |
child 36960 | 01594f816e3a |
permissions | -rw-r--r-- |
29752 | 1 |
(* Title: FOL/ex/Iff_Oracle.thy |
1537 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1996 University of Cambridge |
|
4 |
*) |
|
5 |
||
16832 | 6 |
header {* Example of Declaring an Oracle *} |
16063 | 7 |
|
29752 | 8 |
theory Iff_Oracle |
16832 | 9 |
imports FOL |
10 |
begin |
|
3817 | 11 |
|
16832 | 12 |
subsection {* Oracle declaration *} |
13 |
||
14 |
text {* |
|
15 |
This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}. |
|
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 |
23153 | 22 |
fun mk_iff 1 = Var (("P", 0), @{typ o}) |
23 |
| mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1); |
|
16832 | 24 |
in |
28290 | 25 |
fn (thy, n) => |
16832 | 26 |
if n > 0 andalso n mod 2 = 0 |
28290 | 27 |
then Thm.cterm_of thy (FOLogic.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) *} |
|
30719
21c20c7d1932
use more informative Thm.proof_body_of for oracle demo;
wenzelm
parents:
30549
diff
changeset
|
37 |
ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *} |
16832 | 38 |
|
21863 | 39 |
text {* These oracle calls had better fail. *} |
3817 | 40 |
|
16832 | 41 |
ML {* |
28290 | 42 |
(iff_oracle (@{theory}, 5); error "?") |
23153 | 43 |
handle Fail _ => warning "Oracle failed, as expected" |
16832 | 44 |
*} |
3817 | 45 |
|
16832 | 46 |
ML {* |
28290 | 47 |
(iff_oracle (@{theory}, 1); error "?") |
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 = {* |
30549 | 55 |
Scan.lift OuterParse.nat >> (fn n => fn ctxt => |
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
29752
diff
changeset
|
56 |
SIMPLE_METHOD |
28290 | 57 |
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) |
16832 | 58 |
handle Fail _ => no_tac)) |
59 |
*} "iff oracle" |
|
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 |