
diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Recipes/Oracle.thy
--- a/CookBook/Recipes/Oracle.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,155 +0,0 @@
-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




