# HG changeset patch
# User wenzelm
# Date 1121362094 -7200
# Node ID f220d1df0f4e68780a50aafeea7925a02d906274
# Parent  9ef92b7a22102341624eeb8c1437e89775671a4a
new type-safe interface;
added method example;

diff -r 9ef92b7a2210 -r f220d1df0f4e src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Thu Jul 14 19:28:13 2005 +0200
+++ b/src/FOL/ex/IffOracle.thy	Thu Jul 14 19:28:14 2005 +0200
@@ -4,45 +4,74 @@
     Copyright   1996  University of Cambridge
 *)
 
-header{*Example of Declaring an Oracle*}
+header {* Example of Declaring an Oracle *}
 
-theory IffOracle imports FOL begin
+theory IffOracle
+imports FOL
+begin
 
-text{*This oracle makes tautologies of the form "P <-> P <-> P <-> P".
-The length is specified by an integer, which is checked to be even and 
-positive.*}
+subsection {* Oracle declaration *}
+
+text {*
+  This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
+  The length is specified by an integer, which is checked to be even
+  and positive.
+*}
 
-ML
-{*
-local
+oracle iff_oracle (int) = {*
+  let
+    fun mk_iff 1 = Var (("P", 0), FOLogic.oT)
+      | mk_iff n = FOLogic.iff $ Var (("P", 0), FOLogic.oT) $ mk_iff (n - 1);
+  in
+    fn thy => fn n =>
+      if n > 0 andalso n mod 2 = 0
+      then FOLogic.mk_Trueprop (mk_iff n)
+      else raise Fail ("iff_oracle: " ^ string_of_int n)
+  end
+*}
 
-(* internal syntactic declarations *)
+
+subsection {* Oracle as low-level rule *}
 
-val oT = Type("o",[]);
+ML {* iff_oracle (the_context ()) 2 *}
+ML {* iff_oracle (the_context ()) 10 *}
+ML {* #der (Thm.rep_thm it) *}
+
+text {* These oracle calls had better fail *}
 
-val iff = Const("op <->", [oT,oT]--->oT);
+ML {*
+  (iff_oracle (the_context ()) 5; raise ERROR)
+    handle Fail _ => warning "Oracle failed, as expected"
+*}
 
-fun mk_iff 1 = Free("P", oT)
-  | mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1);
+ML {*
+  (iff_oracle (the_context ()) 1; raise ERROR)
+    handle Fail _ => warning "Oracle failed, as expected"
+*}
 
-val Trueprop = Const("Trueprop",oT-->propT);
+
+subsection {* Oracle as proof method *}
 
-in
+method_setup iff = {*
+  Method.simple_args Args.nat (fn n => fn ctxt =>
+    Method.SIMPLE_METHOD
+      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
+        handle Fail _ => no_tac))
+*} "iff oracle"
 
-(*new exception constructor for passing arguments to the oracle*)
-exception IffOracleExn of int;
+
+lemma "A <-> A"
+  by (iff 2)
 
-fun mk_iff_oracle (sign, IffOracleExn n) =
-  if n > 0 andalso n mod 2 = 0
-  then Trueprop $ mk_iff n
-  else raise IffOracleExn n;
+lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
+  by (iff 10)
+
+lemma "A <-> A <-> A <-> A <-> A"
+  apply (iff 5)?
+  oops
+
+lemma A
+  apply (iff 1)?
+  oops
 
 end
-*}
-
-oracle
-  iff = mk_iff_oracle
-
-end
-
-