--- a/CookBook/Intro.thy	Mon Mar 16 03:02:56 2009 +0100
+++ b/CookBook/Intro.thy	Tue Mar 17 01:56:29 2009 +0100
@@ -135,6 +135,8 @@
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.
 
+  \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
+
   \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
   chapter and also contributed the material on @{text NamedThmsFun}.
   \end{itemize}

--- a/CookBook/Package/Ind_Code.thy	Mon Mar 16 03:02:56 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Tue Mar 17 01:56:29 2009 +0100
@@ -229,7 +229,7 @@
   For example we can use it to instantiate an assumption:
 *}
 
-lemma "\<forall>x1 x2 x3. P (x1::nat) (x2::nat) (x3::nat) \<Longrightarrow> True"
+lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
 apply (tactic {* 
   let 
     val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}]
@@ -249,7 +249,7 @@
   as follows
 *}
 
-ML{*fun induction_tac defs prems insts =
+ML %linenosgray{*fun induction_tac defs prems insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
           K (rewrite_goals_tac defs),
@@ -280,17 +280,24 @@
 
   While the generic proof for the induction principle is relatively simple, 
   it is a bit harder to set up the goals just from the given introduction 
-  rules. For this we have to construct
+  rules. For this we have to construct for each predicate @{text "pred"}
 
   @{text [display] 
-  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}
+  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}
+
+  where the given predicates @{text preds} are replaced by new distinct 
+  ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to
+  new variables @{text "\<^raw:$zs$>"}. 
 
-  where the given predicates are replaced by new ones written
-  as @{text "\<^raw:$Ps$>"}, and also generate new variables 
-  @{text "\<^raw:$zs$>"}.
+  The function below expects that the rules are already appropriately
+  replaced. The argument @{text "mrules"} stands for these modified
+  introduction rules; @{text cnewpreds} are the certified terms coresponding
+  to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for
+  which we prove the introduction principle; @{text "newpred"} is its
+  replacement and @{text "tys"} are the types of its argument.
 *}
 
-ML %linenosgray{* fun prove_induction lthy defs rules cnewpreds ((pred, newpred), tys)  =
+ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys)  =
 let
   val zs = replicate (length tys) "z"
   val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -298,14 +305,32 @@
   
   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
   val goal = Logic.list_implies 
-         (rules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
+         (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
   Goal.prove lthy' [] [prem] goal
   (fn {prems, ...} => induction_tac defs prems cnewpreds)
   |> singleton (ProofContext.export lthy' lthy)
 end *}
 
-text {* *}
+text {* 
+  In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type 
+  list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)
+  variables. These variables are free in the new theory @{text "lthy'"}. In Line 5
+  we just construct the terms corresponding to the variables. The term variables are
+  applied to the predicate in Line 7 (this is the first premise 
+  @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9
+  we first the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add
+  the (modified) introduction rules as premises.
+
+  In Line 11 we set up the goal to be proved; call the induction tactic in
+  Line 13. This returns a theorem. However, it is a theorem proved inside
+  the local theory @{text "lthy'"} where the variables @{text "\<^raw:$zs$>"} are
+  fixed, but free. By exporting this theorem from @{text "lthy'"} (which does contain
+  the  @{text "\<^raw:$zs$>"} as free) to @{text "lthy"} (which does not), we
+  obtain the desired quantifications @{text "\<And>\<^raw:$zs$>"}.
+
+  So it is left to produce the modified rules and 
+*}
 
 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
 let

--- a/CookBook/Recipes/Sat.thy	Mon Mar 16 03:02:56 2009 +0100
+++ b/CookBook/Recipes/Sat.thy	Tue Mar 17 01:56:29 2009 +0100
@@ -1,15 +1,112 @@
 
 theory Sat
-imports Main
+imports Main "../Base"
 begin
 
+section {* SAT Solver\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 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.
+
+  There is the function  @{ML  PropLogic.prop_formula_of_term}, which
+  translates an Isabelle term into a propositional formula. Let
+  us illustrate this function with translating the term @{term "A \<and> \<not>A \<or> B"}. 
+  Suppose the ML-value
+*}
+
+ML{*val (form, tab) = 
+       PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
+
+text {*
+  then the resulting propositional formula @{ML form} is 
+  @{ML "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 
+  where indices are assigned  for the propositional 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 and the output table is
+
+  @{ML_response_fake [display,gray]
+  "Termtab.dest tab"
+  "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
+
+  A propositional variable is also introduced whenever the translation
+  function cannot find an appropriate propositional formula for a term. 
+  Given the ML-value
+*}
+
+ML{*val (form', tab') = 
+       PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
+
+text {*
+  @{ML form'} is now the propositional variable @{ML "BoolVar 1" in PropLogic} 
+  and the table @{ML tab'} is
+
+  @{ML_response_fake [display,gray]
+  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest tab')"
+  "(\<forall>x. P x, 1)"}
+  
+  Having produced a propositional formula, you can call the SAT solvers 
+  with the function @{ML "SatSolver.invoke_solver"}. 
+  For example
+
+  @{ML_response_fake [display,gray]
+  "SatSolver.invoke_solver \"dpll\" form"
+  "SatSolver.SATISFIABLE ass"}
+
+  determines that the formula @{ML form} is satisfiable. If we inspect
+  the returned function @{text ass}
+
+  @{ML_response [display,gray]
+"let
+  val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form
+in 
+  (ass 1, ass 2, ass 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. 
+
+  If we instead invoke the SAT solver with the string @{text [quotes] "auto"}
+
+  @{ML [display,gray] "SatSolver.invoke_solver \"auto\" form"}
+
+  several external SAT solvers will be tried (if they are installed) and
+  the default is the internal SAT solver @{text [quotes] "dpll"}.
+
+  There are also two tactics that make use of the SAT solvers. One 
+  is the tactic @{ML sat_tac in sat}. For example 
+*}
+
+lemma "True"
+apply(tactic {* sat.sat_tac 1 *})
+done
+
+text {*
+  \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"}. Tables used in the translation function are
+  implemented in @{ML_file "Pure/General/table.ML"}.  
+  \end{readmore}
+*}
+
 
-section {* SAT Solver *}
-
-
-
-end
-  
-
-
-
+end
\ No newline at end of file

Binary file cookbook.pdf has changed