--- a/CookBook/Recipes/ExternalSolver.thy	Fri Jan 30 08:24:48 2009 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Fri Jan 30 16:58:31 2009 +0100
@@ -1,161 +1,211 @@
 theory ExternalSolver
 imports "../Base"
+uses ("external_solver.ML")
 begin
 
-section {* Using an External Solver\label{rec:external} *} 
+
+section {* Executing an External Application *}
 
 text {*
   {\bf Problem:}
-  You want to use an external solver, because the solver might be more efficient 
-  for deciding a certain class of formulae than Isabelle tactics.
+  You want to use an external application.
+  \smallskip
+
+  {\bf Solution:} The function @{ML system_out} might be the right thing for
+  you.
   \smallskip
 
-  {\bf Solution:} The easiest way to do this is by implementing an oracle.
-  We will also construct proofs inside Isabelle by using the results produced 
-  by the oracle.
+  This function executes an external command as if printed in a shell. It
+  returns the output of the program and its return value.
+
+  For example, consider running an ordinary shell commands:
+
+  @{ML_response [display,gray] 
+    "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+
+  Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
+  on Page~\pageref{rec:timeout}), i.e. external applications are killed
+  properly. For example, the following expression takes only approximately
+  one second:
+
+  @{ML_response [display,gray] 
+    "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
+     handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+*}
+
+text {*
+  The function @{ML system_out} can also be used for more reasonable
+  applications, e.g. coupling external solvers with Isabelle. In that case,
+  one has to make sure that Isabelle can find the particular executable.
+  One way to ensure this is by adding a Bash-like variable binding into
+  one of Isabelle's settings file (prefer the user settings file usually to
+  be found at @{text "$HOME/.isabelle/etc/settings"}).
+  
+  For example, assume you want to use the application @{text foo} which
+  is here supposed to be located at @{text "/usr/local/bin/"}.
+  The following line has to be added to one of Isabelle's settings file:
+
+  @{text "FOO=/usr/local/bin/foo"}
+
+  In Isabelle, this application may now be executed by
+
+  @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}
+*}
+
+
+
+
+
+
+section {* Writing an Oracle\label{rec:external} *} 
+
+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 is given in 
-  @{ML_file "FOL/ex/IffOracle"}.
-  (TODO: add more references to the code)
+  for section 3.11]. A simple example, which we will slightly extend here,
+  is given in @{ML_file "FOL/ex/IffOracle"}. The raw interface for adding
+  oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm"}.
   \end{readmore}
 
-  For our explanation here, we will use the @{text metis} prover for proving
-  propositional formulae. The general method will be roughly as follows: 
-  Given a goal @{text G}, we transform it into the syntactical respresentation 
-  of @{text "metis"}, build the CNF of the negated formula and then let metis search 
-  for a refutation. @{text Metis} will either return the proved goal or raise 
-  an exception meaning 
-  that it was unable to prove the goal (FIXME: is this so?).
+  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"
 
-  The translation function from Isabelle propositions into formulae of 
-  @{text metis} is as follows:
+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 trans t =
-  (case t of
-    @{term Trueprop} $ t => trans t
-  | @{term True} => Metis.Formula.True
-  | @{term False} => Metis.Formula.False
-  | @{term Not} $ t => Metis.Formula.Not (trans t)
-  | @{term "op &"} $ t1 $ t2 => Metis.Formula.And (trans t1, trans t2)
-  | @{term "op |"} $ t1 $ t2 => Metis.Formula.Or (trans t1, trans t2)
-  | @{term "op -->"} $ t1 $ t2 => Metis.Formula.Imp (trans t1, trans t2)
-  | @{term "op = :: bool => bool => bool"} $ t1 $ t2 => 
-                                     Metis.Formula.Iff (trans t1, trans t2)
-  | Free (n, @{typ bool}) => Metis.Formula.Atom (n, [])
-  | _ => error "inacceptable term")*}
-
-
-text {* 
-  An example is as follows:
-
-@{ML_response [display,gray] "trans @{prop \"A \<and> B\"}" 
-"Metis.Formula.And 
-        (Metis.Formula.Atom (\"A\", []), Metis.Formula.Atom (\"B\", []))"}
-
-
-  The next function computes the conjunctive-normal-form.
+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 %linenumbers{*fun make_cnfs fm =
-       fm |> Metis.Formula.Not
-          |> Metis.Normalize.cnf
-          |> map Metis.Formula.stripConj
-          |> map (map Metis.Formula.stripDisj)
-          |> map (map (map Metis.Literal.fromFormula))
-          |> map (map Metis.LiteralSet.fromList)
-          |> map (map Metis.Thm.axiom)*}
+  @{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 {* 
-  (FIXME: Is there a deep reason why Metis.Normalize.cnf returns a list?)
-
-  (FIXME: What does Line 8 do?)
+  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.
 
-  (FIXME: Can this code be improved?)
-
-
-  Setting up the resolution.
+  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:
 *}
 
-ML{*fun refute cls =
- let val result = 
-        Metis.Resolution.loop             
-          (Metis.Resolution.new Metis.Resolution.default cls)
- in
-   (case result of
-      Metis.Resolution.Contradiction _ => true
-    | Metis.Resolution.Satisfiable _ => false)
- end*}
+oracle iff_oracle = {* fn ct =>
+  if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct)))
+  then ct
+  else error "Proof failed."*}
 
-text {* 
-  Stringing the functions together.
+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{*fun solve f = List.all refute (make_cnfs f)*}
+ML{*val iff_oracle_tac =
+  CSUBGOAL (fn (goal, i) => 
+    (case try iff_oracle goal of
+      NONE => no_tac
+    | SOME thm => rtac thm i))*}
 
-text {* Setting up the oracle*}
+text {*
+  and create a new method solely based on this tactic:
+*}
 
-ML{*fun prop_dp (thy, t) = 
-        if solve (trans t) then (Thm.cterm_of thy t) 
-        else error "Proof failed."*}
+method_setup iff_oracle = {*
+   Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)
+*} "Oracle-based decision procedure for chains of equivalences"
+
+text {*
+  (FIXME: what does @{ML "Method.SIMPLE_METHOD'"} do? ... what do you mean?)
 
-oracle prop_oracle = prop_dp
+  Finally, we can test our oracle to prove some theorems:
+*}
 
-text {* (FIXME: What does oracle do?) *}
+lemma "p = (p::bool)"
+   by iff_oracle
+
+lemma "p = (q = p) = q"
+   by iff_oracle
 
 
-ML{*fun prop_oracle_tac ctxt = 
-  SUBGOAL (fn (goal, i) => 
-    (case (try prop_oracle (ProofContext.theory_of ctxt, goal)) of
-      SOME thm => rtac thm i
-    | NONE => no_tac))*}
-
 text {*
-  (FIXME: The oracle returns a @{text cterm}. How is it possible
-  that I can apply this cterm with @{ML rtac}?)
-*}
-
-method_setup prop_oracle = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (prop_oracle_tac ctxt))
-*} "Oracle-based decision procedure for propositional logic"
-
-text {* (FIXME What does @{ML Method.SIMPLE_METHOD'} do?) *}
-
-lemma test: "p \<or> \<not>p"
-  by prop_oracle
-
-text {* (FIXME: say something about what the proof of the oracle is)
-
-  @{ML_response_fake [display,gray] "Thm.proof_of @{thm test}" "???"}
-
+(FIXME: say something about what the proof of the oracle is ... what do you mean?)
 *} 
 
 
-
-lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p"
-  by prop_oracle
-
-lemma "\<forall>x::nat. x \<ge> 0"
-  sorry
-
-text {*
-  (FIXME: proof reconstruction)
-*}
-
-
-
-text {*
-  For communication with external programs, there are the primitives
-  @{ML_text system} and @{ML_text system_out}, the latter of which captures
-  the invoked program's output. For simplicity, here, we will use metis, an
-  external solver included in the Isabelle destribution. Since it is written
-  in ML, we can call it directly without the detour of invoking an external
-  program.
-*}
-
-
 end
\ No newline at end of file

--- a/CookBook/Recipes/TimeLimit.thy	Fri Jan 30 08:24:48 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Fri Jan 30 16:58:31 2009 +0100
@@ -2,7 +2,7 @@
 imports "../Base"
 begin
 
-section {* Restricting the Runtime of a Function *} 
+section {* Restricting the Runtime of a Function\label{rec:timeout} *} 
 
 text {*
   {\bf Problem:}
@@ -30,7 +30,7 @@
 
 @{ML_response [display,gray]
 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
-  handle TimeOut => ~1"
+  handle TimeLimit.TimeOut => ~1"
 "~1"}
 
   where @{ML_text TimeOut} is the exception raised when the time limit

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/external_solver.ML	Fri Jan 30 16:58:31 2009 +0100
@@ -0,0 +1,56 @@
+signature IFF_SOLVER =
+sig
+  val decide : string -> bool
+end
+
+
+structure IffSolver : IFF_SOLVER =
+struct
+
+exception FAIL
+
+datatype formula = Atom of string | Iff of formula * formula
+
+fun scan s =
+  let
+
+    fun push yss = [] :: yss 
+
+    fun add x (ys :: yss) = (x :: ys) :: yss
+      | add _ _ = raise FAIL
+
+    fun pop ([a, b] :: yss) = add (Iff (b, a)) yss
+      | pop _ = raise FAIL
+
+    fun formula [] acc = acc
+      | formula ("(" :: xs) acc = formula xs (push acc)
+      | formula (")" :: xs) acc = formula xs (pop acc)
+      | formula ("<=>" :: xs) acc = formula xs acc
+      | formula (x :: xs) acc = formula xs (add (Atom x) acc)
+
+    val tokens = String.tokens (fn c => c = #" ") s
+  in
+    (case formula tokens [[]] of
+      [[f]] => f
+    | _ => raise FAIL)
+  end
+
+
+fun decide s =
+  let
+    fun fold_atoms f (Atom n) = f s
+      | fold_atoms f (Iff (p, q)) = fold_atoms f p #> fold_atoms f q
+
+    fun collect s tab =
+      (case Symtab.lookup tab s of
+        NONE => Symtab.update (s, false) tab
+      | SOME v => Symtab.update (s, not v) tab)
+
+    fun check tab = Symtab.fold (fn (_, v) => fn b => b andalso v) tab true
+  in 
+    (case try scan s of
+      NONE => false
+    | SOME f => check (fold_atoms collect f Symtab.empty))
+  end
+
+end

Binary file cookbook.pdf has changed