# HG changeset patch # User Christian Urban # Date 1237251389 -3600 # Node ID 9c25418db6f0273d316ce25d4c81385e9d814399 # Parent 75381fa516cdbec89ff4f26c4f5005016d7bcc08 added a recipy about SAT solvers diff -r 75381fa516cd -r 9c25418db6f0 CookBook/Intro.thy --- 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} diff -r 75381fa516cd -r 9c25418db6f0 CookBook/Package/Ind_Code.thy --- 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 "\x1 x2 x3. P (x1::nat) (x2::nat) (x3::nat) \ True" +lemma "\(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \ 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] - "\\<^raw:$zs$>. pred \<^raw:$zs$> \ rules[preds := \<^raw:$Ps$>] \ \<^raw:$P$> \<^raw:$zs$>"} + "\\<^raw:$zs$>. pred \<^raw:$zs$> \ rules[preds := \<^raw:$Ps$>] \ \<^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 "\\<^raw:$zs$>"}. + + So it is left to produce the modified rules and +*} ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = let diff -r 75381fa516cd -r 9c25418db6f0 CookBook/Recipes/Sat.thy --- 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 \ \A \ B"}. + Suppose the ML-value +*} + +ML{*val (form, tab) = + PropLogic.prop_formula_of_term @{term "A \ \A \ 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 "\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')" + "(\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 diff -r 75381fa516cd -r 9c25418db6f0 cookbook.pdf Binary file cookbook.pdf has changed