# HG changeset patch
# User paulson
# Date 826022321 -3600
# Node ID 3f51f0945a3efaadb0213134c08c19f7241a8e85
# Parent  efbc887dfefb0dd8a1b4893da7c6e654fe70fe71
Example of declaring oracles

diff -r efbc887dfefb -r 3f51f0945a3e src/FOL/ex/IffOracle.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/IffOracle.ML	Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,13 @@
+(*  Title:      FOL/ex/IffOracle
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Example of how to use an oracle
+*)
+
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0);
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5);
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
+#der(rep_thm it);
+
diff -r efbc887dfefb -r 3f51f0945a3e src/FOL/ex/IffOracle.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/IffOracle.thy	Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,11 @@
+(*  Title:      FOL/ex/IffOracle
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Example of how to declare an oracle
+*)
+
+IffOracle = "declIffOracle" + FOL +
+oracle mk_iff_oracle
+end
diff -r efbc887dfefb -r 3f51f0945a3e src/FOL/ex/declIffOracle.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/declIffOracle.ML	Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,24 @@
+(*  Title:      FOL/ex/declIffOracle
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Example of how to declare an oracle
+*)
+
+
+(*New exception constructor for passing arguments to the oracle*)
+exception IffOracleExn of int;
+
+(*Internal syntactic declarations*)
+val oT = Type("o",[]);
+
+val iff = Const("op <->", [oT,oT]--->oT);
+
+fun mk_iff 0 = Const("True", oT)
+  | mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1);
+
+val Trueprop = Const("Trueprop",oT-->propT);
+
+(*Oracle makes tautologies of the form "P <-> P <-> P <-> P <-> True"*)
+fun mk_iff_oracle (sign, IffOracleExn n) = Trueprop $ mk_iff (2*n);
diff -r efbc887dfefb -r 3f51f0945a3e src/FOL/ex/declIffOracle.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/declIffOracle.thy	Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,1 @@
+declIffOracle = Pure