author | paulson |
Wed, 02 Apr 1997 15:19:40 +0200 | |
changeset 2867 | 0aa5a3cd4550 |
parent 1847 | 58ab3b74a344 |
permissions | -rw-r--r-- |
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 |
||
1847
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
18 |
fun mk_iff 1 = Free("P", oT) |
1537 | 19 |
| mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1); |
20 |
||
21 |
val Trueprop = Const("Trueprop",oT-->propT); |
|
22 |
||
1847
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
23 |
(*Oracle makes tautologies of the form "P <-> P <-> P <-> P"*) |
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
24 |
fun mk_iff_oracle (sign, IffOracleExn n) = |
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
25 |
if n>0 andalso n mod 2 = 0 |
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
26 |
then Trueprop $ mk_iff n |
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
27 |
else raise IffOracleExn n; |