--- a/CookBook/Recipes/ExternalSolver.thy	Mon Jan 26 12:28:43 2009 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Mon Jan 26 12:29:01 2009 +0000
@@ -6,13 +6,13 @@
 
 text {*
   {\bf Problem:}
-  You want to use an external solver, say, because it is more efficient in
-  deciding particular formulas than any Isabelle tactic.
+  You want to use an external solver, because the solver might be more efficient 
+  for deciding a certain class of formulae than Isabelle tactics.
   \smallskip
 
-  {\bf Solution:} The easiest way to do this is writing an oracle.
-  To yield results checked by Isabelle's kernel, one can reconstruct the
-  proofs.
+  {\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.
   \smallskip
 
   \begin{readmore}
@@ -22,26 +22,18 @@
   (TODO: add more references to the code)
   \end{readmore}
 
-  The general layout will be as follows. Given a goal G, we transform it into
-  the syntactical respresentation of the external solver, and invoke the
-  solver. The solver's result is then used inside the oracle to either return
-  the proved goal or raise an exception meaning that the solver was unable to
-  prove the goal.
+  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 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 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.
-
-  We will restrict ourselves to proving formulas of propositional logic, a
-  task metis is very good at.
+  The translation function from Isabelle propositions into formulae of 
+  @{text metis} is as follows:
   *}
 
-
-ML {*
-fun trans t =
+ML{*fun trans t =
   (case t of
     @{term Trueprop} $ t => trans t
   | @{term True} => Metis.Formula.True
@@ -51,62 +43,114 @@
   | @{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)
+                                     Metis.Formula.Iff (trans t1, trans t2)
   | Free (n, @{typ bool}) => Metis.Formula.Atom (n, [])
-  | _ => error "inacceptable term")
+  | _ => 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 solve f =
-  let
-    open Metis
-    fun fromLiterals fms = LiteralSet.fromList (map Literal.fromFormula fms)
-    fun fromClause fm = fromLiterals (Formula.stripDisj fm)
-    fun fromCnf fm = map fromClause (Formula.stripConj fm)
+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)*}
 
-    val mk_cnfs = map fromCnf o Normalize.cnf o Formula.Not
-    fun refute cls =
-      let val res = Resolution.new Resolution.default (map Thm.axiom cls)
-      in
-        (case Resolution.loop res of
-          Resolution.Contradiction _ => true
-        | Resolution.Satisfiable _ => false)
-      end
-  in List.all refute (mk_cnfs f) end
+text {* 
+  (FIXME: Is there a deep reason why Metis.Normalize.cnf returns a list?)
+
+  (FIXME: What does Line 8 do?)
+
+  (FIXME: Can this code improved?)
+
+
+  Setting up the resolution.
 *}
 
+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*}
 
-ML {*
-fun prop_dp (thy, t) = if solve (trans t) then Thm.cterm_of thy t 
-  else error "Proof failed."
+text {* 
+  Stringing the functions together.
 *}
 
+ML{*fun solve f = List.all refute (make_cnfs f)*}
+
+text {* Setting up the oracle*}
+
+ML{*fun prop_dp (thy, t) = 
+        if solve (trans t) then (Thm.cterm_of thy t) 
+        else error "Proof failed."*}
+
 oracle prop_oracle = prop_dp
 
-ML {*
-fun prop_oracle_tac ctxt = 
+text {* (FIXME: What does oracle this do?) *}
+
+
+ML{*fun prop_oracle_tac ctxt = 
   SUBGOAL (fn (goal, i) => 
-    (case try prop_oracle (ProofContext.theory_of ctxt, goal) of
+    (case (try prop_oracle (ProofContext.theory_of ctxt, goal)) of
       SOME thm => rtac thm i
-    | NONE => no_tac))
+    | 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"
 
-lemma "p \<or> \<not>p"
+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 {* Thm.proof_of @{thm test} *} 
+
 lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p"
   by prop_oracle
 
 lemma "\<forall>x::nat. x \<ge> 0"
   sorry
 
+text {*
+  (FIXME: proof reconstruction)
+*}
 
-(* TODO: 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