equal
deleted
inserted
replaced
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 1 = Free("P", 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"*) |
|
24 fun mk_iff_oracle (sign, IffOracleExn n) = |
|
25 if n>0 andalso n mod 2 = 0 |
|
26 then Trueprop $ mk_iff n |
|
27 else raise IffOracleExn n; |
|