--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/Oracle.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,155 @@
+theory Oracle
+imports "../Base"
+uses ("external_solver.ML")
+begin
+
+section {* Writing an Oracle\label{rec:oracle} *} 
+
+text {*
+  {\bf Problem:}
+  You want to use a fast, new decision procedure not based one Isabelle's
+  tactics, and you do not care whether it is sound.
+  \smallskip
+
+  {\bf Solution:} Isabelle provides the oracle mechanisms to bypass the
+  inference kernel. Note that theorems proven by an oracle carry a special
+  mark to inform the user of their potential incorrectness.
+  \smallskip
+
+  \begin{readmore}
+  A short introduction to oracles can be found in [isar-ref: no suitable label
+  for section 3.11]. A simple example, which we will slightly extend here,
+  is given in @{ML_file "FOL/ex/Iff_Oracle.thy"}. The raw interface for adding
+  oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}.
+  \end{readmore}
+
+  For our explanation here, we restrict ourselves to decide propositional
+  formulae which consist only of equivalences between propositional variables,
+  i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology.
+
+  Assume, that we have a decision procedure for such formulae, implemented
+  in ML. Since we do not care how it works, we will use it here as an
+  ``external solver'':
+*}
+
+use "external_solver.ML"
+
+text {*
+  We do, however, know that the solver provides a function
+  @{ML IffSolver.decide}.
+  It takes a string representation of a formula and returns either
+  @{ML true} if the formula is a tautology or
+  @{ML false} otherwise. The input syntax is specified as follows:
+
+  formula $::=$ atom $\mid$ \verb|(| formula \verb|<=>| formula \verb|)|
+
+  and all token are separated by at least one space.
+
+  (FIXME: is there a better way for describing the syntax?)
+ 
+  We will proceed in the following way. We start by translating a HOL formula
+  into the string representation expected by the solver. The solver's result
+  is then used to build an oracle, which we will subsequently use as a core
+  for an Isar method to be able to apply the oracle in proving theorems.
+
+  Let us start with the translation function from Isabelle propositions into
+  the solver's string representation. To increase efficiency while building
+  the string, we use functions from the @{text Buffer} module.
+  *}
+
+ML {*fun translate t =
+  let
+    fun trans t =
+      (case t of
+        @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>
+          Buffer.add " (" #>
+          trans t #>
+          Buffer.add "<=>" #> 
+          trans u #>
+          Buffer.add ") "
+      | Free (n, @{typ bool}) =>
+         Buffer.add " " #> 
+         Buffer.add n #>
+         Buffer.add " "
+      | _ => error "inacceptable term")
+  in Buffer.content (trans t Buffer.empty) end
+*}
+
+text {*
+  Here is the string representation of the term @{term "p = (q = p)"}:
+
+  @{ML_response 
+    "translate @{term \"p = (q = p)\"}" 
+    "\" ( p <=> ( q <=> p ) ) \""}
+
+  Let us check, what the solver returns when given a tautology:
+
+  @{ML_response 
+    "IffSolver.decide (translate @{term \"p = (q = p) = q\"})"
+    "true"}
+
+  And here is what it returns for a formula which is not valid:
+
+  @{ML_response 
+    "IffSolver.decide (translate @{term \"p = (q = p)\"})" 
+    "false"}
+*}
+
+text {* 
+  Now, we combine these functions into an oracle. In general, an oracle may
+  be given any input, but it has to return a certified proposition (a
+  special term which is type-checked), out of which Isabelle's inference
+  kernel ``magically'' makes a theorem.
+
+  Here, we take the proposition to be show as input. Note that we have
+  to first extract the term which is then passed to the translation and
+  decision procedure. If the solver finds this term to be valid, we return
+  the given proposition unchanged to be turned then into a theorem:
+*}
+
+oracle iff_oracle = {* fn ct =>
+  if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct)))
+  then ct
+  else error "Proof failed."*}
+
+text {*
+  Here is what we get when applying the oracle:
+
+  @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
+
+  (FIXME: is there a better way to present the theorem?)
+
+  To be able to use our oracle for Isar proofs, we wrap it into a tactic:
+*}
+
+ML{*val iff_oracle_tac =
+  CSUBGOAL (fn (goal, i) => 
+    (case try iff_oracle goal of
+      NONE => no_tac
+    | SOME thm => rtac thm i))*}
+
+text {*
+  and create a new method solely based on this tactic:
+*}
+
+method_setup iff_oracle = {*
+   Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))
+*} "Oracle-based decision procedure for chains of equivalences"
+
+text {*
+  Finally, we can test our oracle to prove some theorems:
+*}
+
+lemma "p = (p::bool)"
+   by iff_oracle
+
+lemma "p = (q = p) = q"
+   by iff_oracle
+
+
+text {*
+(FIXME: say something about what the proof of the oracle is ... what do you mean?)
+*} 
+
+
+end
\ No newline at end of file