--- a/CookBook/Recipes/Sat.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,122 +0,0 @@
-
-theory Sat
-imports Main "../Base"
-begin
-
-section {* SAT Solvers\label{rec:sat} *}
-
-text {*
-  {\bf Problem:}
-  You like to use a SAT solver to find out whether
-  an Isabelle formula is satisfiable or not.\smallskip
-
-  {\bf Solution:} Isabelle contains a general interface for 
-  a number of external SAT solvers (including ZChaff and Minisat)
-  and also contains a simple internal SAT solver that
-  is based on the DPLL algorithm.\smallskip
-
-  The SAT solvers expect a propositional formula as input and produce
-  a result indicating that the formula is either satisfiable, unsatisfiable or
-  unknown. The type of the propositional formula is  
-  @{ML_type "PropLogic.prop_formula"} with the usual constructors such 
-  as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on.
-
-  The function  @{ML  PropLogic.prop_formula_of_term} translates an Isabelle 
-  term into a propositional formula. Let
-  us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. 
-  The function will return a propositional formula and a table. Suppose 
-*}
-
-ML{*val (pform, table) = 
-       PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
-
-text {*
-  then the resulting propositional formula @{ML pform} is 
-  
-  @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 
-  
-
-  where indices are assigned for the variables 
-  @{text "A"} and @{text "B"}, respectively. This assignment is recorded 
-  in the table that is given to the translation function and also returned 
-  (appropriately updated) in the result. In the case above the
-  input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
-
-  @{ML_response_fake [display,gray]
-  "Termtab.dest table"
-  "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
-
-  An index is also produced whenever the translation
-  function cannot find an appropriate propositional formula for a term. 
-  Attempting to translate @{term "\<forall>x::nat. P x"}
-*}
-
-ML{*val (pform', table') = 
-       PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
-
-text {*
-  returns @{ML "BoolVar 1" in PropLogic} for  @{ML pform'} and the table 
-  @{ML table'} is:
-
-  @{ML_response_fake [display,gray]
-  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
-  "(\<forall>x. P x, 1)"}
-  
-  We used some pretty printing scaffolding to see better what the output is.
- 
-  Having produced a propositional formula, you can now call the SAT solvers 
-  with the function @{ML "SatSolver.invoke_solver"}. For example
-
-  @{ML_response_fake [display,gray]
-  "SatSolver.invoke_solver \"dpll\" pform"
-  "SatSolver.SATISFIABLE assg"}
-
-  determines that the formula @{ML pform} is satisfiable. If we inspect
-  the returned function @{text assg}
-
-  @{ML_response [display,gray]
-"let
-  val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform
-in 
-  (assg 1, assg 2, assg 3)
-end"
-  "(SOME true, SOME true, NONE)"}
-
-  we obtain a possible assignment for the variables @{text "A"} and @{text "B"}
-  that makes the formula satisfiable. 
-
-  Note that we invoked the SAT solver with the string @{text [quotes] dpll}. 
-  This string specifies which SAT solver is invoked (in this case the internal
-  one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"}
-
-  @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}
-
-  several external SAT solvers will be tried (assuming they are installed). 
-  If no external SAT solver is installed, then the default is 
-  @{text [quotes] "dpll"}.
-
-  There are also two tactics that make use of SAT solvers. One 
-  is the tactic @{ML sat_tac in sat}. For example 
-*}
-
-lemma "True"
-apply(tactic {* sat.sat_tac 1 *})
-done
-
-text {*
-  However, for proving anything more exciting you have to use a SAT solver
-  that can produce a proof. The internal one is not usuable for this. 
-
-  \begin{readmore} 
-  The interface for the external SAT solvers is implemented
-  in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple
-  SAT solver based on the DPLL algorithm. The tactics for SAT solvers are
-  implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning
-  propositional formulas are implemented in @{ML_file
-  "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are
-  implemented in @{ML_file "Pure/General/table.ML"}.  
-  \end{readmore}
-*}
-
-
-end
\ No newline at end of file