|
1537
|
1 |
(* Title: FOL/ex/declIffOracle
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1996 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Example of how to declare an oracle
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
|
|
|
10 |
(*New exception constructor for passing arguments to the oracle*)
|
|
|
11 |
exception IffOracleExn of int;
|
|
|
12 |
|
|
|
13 |
(*Internal syntactic declarations*)
|
|
|
14 |
val oT = Type("o",[]);
|
|
|
15 |
|
|
|
16 |
val iff = Const("op <->", [oT,oT]--->oT);
|
|
|
17 |
|
|
|
18 |
fun mk_iff 0 = Const("True", oT)
|
|
|
19 |
| mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1);
|
|
|
20 |
|
|
|
21 |
val Trueprop = Const("Trueprop",oT-->propT);
|
|
|
22 |
|
|
|
23 |
(*Oracle makes tautologies of the form "P <-> P <-> P <-> P <-> True"*)
|
|
|
24 |
fun mk_iff_oracle (sign, IffOracleExn n) = Trueprop $ mk_iff (2*n);
|