author | ballarin |
Mon, 01 Dec 2008 13:43:32 +0100 | |
changeset 28927 | 7e631979922f |
parent 28316 | b17d863a050f |
permissions | -rw-r--r-- |
3817 | 1 |
(* Title: FOL/ex/IffOracle.thy |
1537 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
*) |
|
6 |
||
16832 | 7 |
header {* Example of Declaring an Oracle *} |
16063 | 8 |
|
16832 | 9 |
theory IffOracle |
10 |
imports FOL |
|
11 |
begin |
|
3817 | 12 |
|
16832 | 13 |
subsection {* Oracle declaration *} |
14 |
||
15 |
text {* |
|
16 |
This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}. |
|
17 |
The length is specified by an integer, which is checked to be even |
|
18 |
and positive. |
|
19 |
*} |
|
3817 | 20 |
|
28290 | 21 |
oracle iff_oracle = {* |
16832 | 22 |
let |
23153 | 23 |
fun mk_iff 1 = Var (("P", 0), @{typ o}) |
24 |
| mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1); |
|
16832 | 25 |
in |
28290 | 26 |
fn (thy, n) => |
16832 | 27 |
if n > 0 andalso n mod 2 = 0 |
28290 | 28 |
then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n)) |
16832 | 29 |
else raise Fail ("iff_oracle: " ^ string_of_int n) |
30 |
end |
|
31 |
*} |
|
3817 | 32 |
|
16832 | 33 |
|
34 |
subsection {* Oracle as low-level rule *} |
|
3817 | 35 |
|
28290 | 36 |
ML {* iff_oracle (@{theory}, 2) *} |
37 |
ML {* iff_oracle (@{theory}, 10) *} |
|
28316
b17d863a050f
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset
|
38 |
ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *} |
16832 | 39 |
|
21863 | 40 |
text {* These oracle calls had better fail. *} |
3817 | 41 |
|
16832 | 42 |
ML {* |
28290 | 43 |
(iff_oracle (@{theory}, 5); error "?") |
23153 | 44 |
handle Fail _ => warning "Oracle failed, as expected" |
16832 | 45 |
*} |
3817 | 46 |
|
16832 | 47 |
ML {* |
28290 | 48 |
(iff_oracle (@{theory}, 1); error "?") |
23153 | 49 |
handle Fail _ => warning "Oracle failed, as expected" |
16832 | 50 |
*} |
3817 | 51 |
|
16832 | 52 |
|
53 |
subsection {* Oracle as proof method *} |
|
3817 | 54 |
|
16832 | 55 |
method_setup iff = {* |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
25946
diff
changeset
|
56 |
Method.simple_args OuterParse.nat (fn n => fn ctxt => |
16832 | 57 |
Method.SIMPLE_METHOD |
28290 | 58 |
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) |
16832 | 59 |
handle Fail _ => no_tac)) |
60 |
*} "iff oracle" |
|
3817 | 61 |
|
16832 | 62 |
|
63 |
lemma "A <-> A" |
|
64 |
by (iff 2) |
|
3817 | 65 |
|
16832 | 66 |
lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A" |
67 |
by (iff 10) |
|
68 |
||
69 |
lemma "A <-> A <-> A <-> A <-> A" |
|
70 |
apply (iff 5)? |
|
71 |
oops |
|
72 |
||
73 |
lemma A |
|
74 |
apply (iff 1)? |
|
75 |
oops |
|
3817 | 76 |
|
16063 | 77 |
end |