--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,112 @@
+theory ExternalSolver
+imports "../Base"
+begin
+
+section {* Using an External Solver *} 
+
+text {*
+  {\bf Problem:}
+  You want to use an external solver, say, because it is more efficient in
+  deciding particular formulas than any Isabelle tactic.
+  \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.
+  \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)
+  \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 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.
+  *}
+
+
+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")
+*}
+
+
+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)
+
+    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
+*}
+
+
+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 = 
+  SUBGOAL (fn (goal, i) => 
+    (case try prop_oracle (ProofContext.theory_of ctxt, goal) of
+      SOME thm => rtac thm i
+    | NONE => no_tac))
+*}
+
+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"
+  by prop_oracle
+
+lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p"
+  by prop_oracle
+
+lemma "\<forall>x::nat. x \<ge> 0"
+  sorry
+
+
+(* TODO: proof reconstruction *)
+
+
+end
\ No newline at end of file