# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1237341831 -3600 # Node ID c7f04a008c9c1d7a35c770df88a2cf6648204024 # Parent 8bb4eaa2ec928c01cc888264e34aac7bd9a2dfa7 some polishing diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Appendix.thy --- a/CookBook/Appendix.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/Appendix.thy Wed Mar 18 03:03:51 2009 +0100 @@ -10,7 +10,7 @@ chapter {* Recipes *} text {* - Possible further topics: + Possible topics: \begin{itemize} \item translations/print translations; @@ -18,7 +18,8 @@ \item user space type systems (in the form that already exists) - \item unification and typing algorithms + \item unification and typing algorithms + (@{ML_file "Pure/pattern.ML"} implements HOPU) \item useful datastructures: discrimination nets, association lists \end{itemize} diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/FirstSteps.thy Wed Mar 18 03:03:51 2009 +0100 @@ -261,8 +261,8 @@ |> (curry list_comb) pred *} text {* - This code extracts the argument types of the given - predicate and then generate for each type a distinct variable; finally it + This code extracts the argument types of a given + predicate and then generates for each argument type a distinct variable; finally it applies the generated variables to the predicate. For example @{ML_response_fake [display,gray] @@ -271,17 +271,17 @@ |> warning" "P z za zb"} - You can read this off this behaviour from how @{ML apply_fresh_args} is + You can read off this behaviour from how @{ML apply_fresh_args} is coded: in Line 2, the function @{ML fastype_of} calculates the type of the - predicate; in Line 3, @{ML binder_types} produces the list of argument - types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each - type with the string @{text "z"}; the + predicate; @{ML binder_types} in the next line produces the list of argument + types (in the case above the list @{text "[nat, int, unit]"}); Line 4 + pairs up each type with the string @{text "z"}; the function @{ML variant_frees in Variable} generates for each @{text "z"} a - unique name avoiding @{text pred}; the list of name-type pairs is turned - into a list of variable terms in Line 6, which in the last line are applied + unique name avoiding the given @{text pred}; the list of name-type pairs is turned + into a list of variable terms in Line 6, which in the last line is applied by the function @{ML list_comb} to the predicate. We have to use the function @{ML curry}, because @{ML list_comb} expects the predicate and the - argument list as a pair. + variables list as a pair. The combinator @{ML "#>"} is the reverse function composition. It can be used to define the following function @@ -443,9 +443,9 @@ text {* The function @{ML dest_ss in MetaSimplifier} returns a record containing all - information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored - in the current simpset. This simpset can be referred to using the antiquotation - @{text "@{simpset}"}. + information stored in the simpset. We are only interested in the names of the + simp-rules. So now you can feed in the current simpset into this function. + The simpset can be referred to using the antiquotation @{text "@{simpset}"}. @{ML_response_fake [display,gray] "get_thm_names_from_ss @{simpset}" @@ -596,7 +596,7 @@ Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} - (FIXME: handy functions for constructing terms @{ML list_comb}, @{ML lambda}) + (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}) Although types of terms can often be inferred, there are many diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/Package/Ind_Code.thy Wed Mar 18 03:03:51 2009 +0100 @@ -55,7 +55,7 @@ text {* It returns the definition (as a theorem) and the local theory in which this definition has - been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the + been made. In Line 4, @{ML internalK in Thm} is a flag attached to the theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). These flags just classify theorems and have no significant meaning, except for tools that, for example, find theorems in the theorem database. We also @@ -72,7 +72,7 @@ end *} text {* - which makes the difinition @{prop "MyTrue \<equiv> True"} and then prints it out. + which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. Since we are testing the function inside \isacommand{local\_setup}, i.e.~make changes to the ambient theory, we can query the definition using the usual command \isacommand{thm}: @@ -82,17 +82,20 @@ @{text "> MyTrue \<equiv> True"} \end{isabelle} - The next two functions construct the terms we need for the definitions, namely - terms of the form + The next two functions construct the terms we need for the definitions for + our \isacommand{simple\_inductive} command. These + terms are of the form @{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> pred \<^raw:$zs$>"} The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur - in the @{text orules} and also be distinct from @{text "preds"}. + in the @{text orules} and also be distinct from the @{text "preds"}. - The first function constructs the term for one particular predicate @{text - "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is - determined by the number of argument types of @{text "arg_tys"}. + The first function constructs the term for one particular predicate, say + @{text "pred"}; the number of arguments of this predicate is + determined by the number of argument types of @{text "arg_tys"}. + So it takes these two parameters as arguments. The other arguments are + all the @{text "preds"} and the @{text "orules"}. *} ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) = @@ -112,11 +115,13 @@ end*} text {* - The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"}. For this - it pairs every argument type with the string @{text [quotes] "z"} (Line 7); - then generates variants for all these strings so that they are unique - w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the - corresponding variable terms for the unique strings. + The function in Line 3 is just a helper function for constructing universal + quantifications. The code in Lines 5 to 9 produces the fresh @{text + "\<^raw:$zs$>"}. For this it pairs every argument type with the string + @{text [quotes] "z"} (Line 7); then generates variants for all these strings + so that they are unique w.r.t.~to the @{text "orules"} and the predicates; + in Line 9 it generates the corresponding variable terms for the unique + strings. The unique free variables are applied to the predicate (Line 11) using the function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in @@ -132,7 +137,7 @@ val orules = [@{prop "even 0"}, @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"}, @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] - val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] + val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}, @{term "z::nat"}] val pred = @{term "even::nat\<Rightarrow>bool"} val arg_tys = [@{typ "nat"}] val def = defs_aux lthy orules preds (pred, arg_tys) @@ -141,15 +146,18 @@ end *} text {* - It constructs the left-hand side for the definition of @{term "even"}. So we obtain + It constructs the left-hand side for the definition of @{text "even"}. So we obtain as printout the term @{text [display] "\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"} - The main function for the definitions now has to just iterate - the function @{ML defs_aux} over all predicates. + The main function for the definitions now has to just iterate the function + @{ML defs_aux} over all predicates. The argument @{text "preds"} is again + the the list of predicates as @{ML_type term}s; the argument @{text + "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is + the list of argument-type-lists for each predicate. *} ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = @@ -162,19 +170,16 @@ end*} text {* - The argument @{text "preds"} is again the the list of predicates as - @{ML_type term}s; - the argument @{text "prednames"} is the list of names of the predicates; - @{text "arg_tyss"} is the list of argument-type-lists for each predicate. - - The user give the introduction rules using meta-implications and meta-quantifications. - In line 4 we transform the introduction rules into the object logic (definitions - cannot use them). To do the transformation we have to - obtain the theory behind the local theory (Line 3); with this theory - we can use the function @{ML ObjectLogic.atomize_term} to make the - transformation (Line 4). The call to @{ML defs_aux} in Line 5 produces all - left-hand sides of the definitions. The actual definitions are then made in Line 7. - As the result we obtain a list of theorems and a local theory. + The user will state the introduction rules using meta-implications and + meta-quanti\-fications. In Line 4, we transform these introduction rules into + the object logic (since definitions cannot be stated with + meta-connectives). To do this transformation we have to obtain the theory + behind the local theory (Line 3); with this theory we can use the function + @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call + to @{ML defs_aux} in Line 5 produces all left-hand sides of the + definitions. The actual definitions are then made in Line 7. The result + of the function is a list of theorems and a local theory. + A testcase for this function is *} @@ -194,6 +199,9 @@ end *} text {* + where we feed into the functions all parameters corresponding to + the @{text even}-@{text odd} example. The definitions we obtain + are: \begin{isabelle} \isacommand{thm}~@{text "even_def odd_def"}\\ @@ -201,18 +209,16 @@ "> even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) > \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z, > odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) -> \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"} +> \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"} \end{isabelle} - This completes the code concerning the definitions. Next comes the code for - the induction principles. - - Let us now turn to the induction principles. Recall that the proof of the - induction principle for @{term "even"} was: + This completes the code for making the definitions. Next we deal with + the induction principles. Recall that the proof of the induction principle + for @{text "even"} was: *} -lemma +lemma man_ind_principle: assumes prems: "even n" shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" apply(atomize (full)) @@ -224,32 +230,35 @@ done text {* - We have to implement code that constructs the induction principle and then - a tactic that automatically proves it. + The code for such induction principles has to accomplish two tasks: + constructing the induction principles from the given introduction + rules and then automatically generating a proof of them using a tactic. The tactic will use the following helper function for instantiating universal - quantifiers. This function instantiates the @{text "?x"} in the theorem - @{thm spec} with a given @{ML_type cterm}. + quantifiers. *} ML{*fun inst_spec ctrm = Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*} text {* - For example we can use it in the following proof to instantiate the - three quantifiers in the assumption. We use the tactic + This helper function instantiates the @{text "?x"} in the theorem + @{thm spec} with a given @{ML_type cterm}. Together with the tactic *} ML{*fun inst_spec_tac ctrms = EVERY' (map (dtac o inst_spec) ctrms)*} text {* - and then apply use it with the @{ML_type cterm}s @{text "y1\<dots>y3"}. - *} + we can use @{ML inst_spec} in the following proof to instantiate the + three quantifiers in the assumption. +*} -lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True" +lemma + fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" + shows "\<forall>x y z. P x y z \<Longrightarrow> True" apply (tactic {* - inst_spec_tac [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *}) + inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *}) txt {* We obtain the goal state @@ -271,8 +280,11 @@ assume_tac]*} text {* - We only have to give it as arguments the premises and the instantiations. - A testcase for the tactic is + We only have to give it as arguments the definitions, the premise + (like @{text "even n"}) + and the instantiations. Compare this with the manual proof given for the + lemma @{thm [source] man_ind_principle}. + A testcase for this tactic is the function *} ML{*fun test_tac prems = @@ -284,7 +296,7 @@ end*} text {* - which indeed proves the induction principle. + which indeed proves the induction principle: *} lemma @@ -294,22 +306,23 @@ done text {* - While the generic proof for the induction principle is relatively simple, - it is a bit harder to construct the goals from just the introduction - rules the user states. In general we have to construct for each predicate + While the tactic for the induction principle is relatively simple, + it is a bit harder to construct the goals from the introduction + rules the user provides. In general we have to construct for each predicate @{text "pred"} a goal of the form @{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 in the introduction - rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}. - We also need to generate fresh arguments for the predicate @{text "pred"} and - the @{text "\<^raw:$P$>"} in the conclusion of the induction principle. + rules by new distinct variables written @{text "\<^raw:$Ps$>"}. + We also need to generate fresh arguments for the predicate @{text "pred"} in + the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve + that in two steps. - The function below expects that the rules are already appropriately - substitued. The argument @{text "srules"} stands for these substituted - introduction rules; @{text cnewpreds} are the certified terms coresponding + The function below expects that the introduction rules are already appropriately + substituted. The argument @{text "srules"} stands for these substituted + 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 argument types of this predicate. @@ -331,64 +344,102 @@ end *} text {* - In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the + In Line 3 we produce names @{text "\<^raw:$zs$>"} for each type in the argument type list. Line 4 makes these names unique and declares them as \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In Line 5 we just construct the terms corresponding to these variables. The term variables are applied to the predicate in Line 7 (this corresponds to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9, we first construct the term @{text "\<^raw:$P$>\<^raw:$zs$>"} - and then add the (modified) introduction rules as premises. In case that - no introduction rules are given, the conclusion of this implications needs + and then add the (substituded) introduction rules as premises. In case that + no introduction rules are given, the conclusion of this implication needs to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal mechanism will fail. - In Line 11 we set up the goal to be proved; then call the tactic for proving the - induction principle. This tactic expects the (certified) predicates with which - the introduction rules have been substituted. This will return 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 contains the @{text "\<^raw:$zs$>"} - as free) to @{text "lthy"} (which does not), we obtain the desired quantifications - @{text "\<And>\<^raw:$zs$>"}. + In Line 11 we set up the goal to be proved; in the next line call the tactic + for proving the induction principle. This tactic expects definitions, the + premise and the (certified) predicates with which the introduction rules + have been substituted. This will return 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 contains the @{text "\<^raw:$zs$>"} as free) to @{text + "lthy"} (which does not), we obtain the desired quantifications @{text + "\<And>\<^raw:$zs$>"}. - Now it is left to produce the new predicated with which the introduction + (FIXME testcase) + + + Now it is left to produce the new predicates with which the introduction rules are substituted. *} -ML %linenosgray{*fun inductions rules defs preds tyss lthy = +ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy = let val Ps = replicate (length preds) "P" val (newprednames, lthy') = Variable.variant_fixes Ps lthy val thy = ProofContext.theory_of lthy' - val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss + val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss val newpreds = map Free (newprednames ~~ tyss') val cnewpreds = map (cterm_of thy) newpreds - val rules' = map (subst_free (preds ~~ newpreds)) rules + val srules = map (subst_free (preds ~~ newpreds)) rules in - map (prove_induction lthy' defs rules' cnewpreds) - (preds ~~ newpreds ~~ tyss) + map (prove_induction lthy' defs srules cnewpreds) + (preds ~~ newpreds ~~ arg_tyss) |> ProofContext.export lthy' lthy end*} -ML {* - let - val rules = [@{prop "even (0::nat)"}, - @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, - @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] - val defs = [@{thm even_def}, @{thm odd_def}] - val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] - val tyss = [[@{typ "nat"}], [@{typ "nat"}]] - in - inductions rules defs preds tyss @{context} - end +text {* + In Line 3 we generate a string @{text [quotes] "P"} for each predicate. + In Line 4, we use the same trick as in the previous function, that is making the + @{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in + the new local theory @{text "lthy'"}. From the local theory we extract + the ambient theory in Line 6. We need this theory in order to certify + the new predicates. In Line 8 we calculate the types of these new predicates + using the argument types. Next we turn them into terms and subsequently + certify them. We can now produce the substituted introduction rules + (Line 11). Line 14 and 15 just iterate the proofs for all predicates. + From this we obtain a list of theorems. Finally we need to export the + fixed variables @{text "\<^raw:$Ps$>"} to obtain the correct quantification + (Line 16). + + A testcase for this function is +*} + +local_setup %gray {* fn lthy => +let + val rules = [@{prop "even (0::nat)"}, + @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, + @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] + val defs = [@{thm even_def}, @{thm odd_def}] + val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] + val tyss = [[@{typ "nat"}], [@{typ "nat"}]] + val ind_thms = inductions rules defs preds tyss lthy +in + warning (str_of_thms lthy ind_thms); lthy +end *} -subsection {* Introduction Rules *} +text {* + which prints out + +@{text [display] +"> even z \<Longrightarrow> +> P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> P z, +> odd z \<Longrightarrow> +> P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> Pa z"} + + + This completes the code for the induction principles. Finally we can + prove the introduction rules. + +*} + +ML {* ObjectLogic.rulify *} + ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} @@ -422,7 +473,7 @@ fun introductions_tac defs rules preds i ctxt = EVERY1 [ObjectLogic.rulify_tac, K (rewrite_goals_tac defs), - REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), + REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), subproof1 rules preds i ctxt]*} lemma evenS: @@ -491,7 +542,6 @@ end*} ML{*val spec_parser = - OuterParse.opt_target -- OuterParse.fixes -- Scan.optional (OuterParse.$$$ "where" |-- @@ -501,10 +551,9 @@ ML{*val specification = spec_parser >> - (fn ((loc, pred_specs), rule_specs) => - Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*} + (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*} -ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" +ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates" OuterKeyword.thy_decl specification*} text {* diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Recipes/Sat.thy --- a/CookBook/Recipes/Sat.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/Recipes/Sat.thy Wed Mar 18 03:03:51 2009 +0100 @@ -16,79 +16,86 @@ 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 + 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. - 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 + 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 (form, tab) = +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 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 + 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 and the output table is + input table is empty (i.e.~@{ML Termtab.empty}) and the output table is @{ML_response_fake [display,gray] - "Termtab.dest tab" + "Termtab.dest table" "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} - A propositional variable is also introduced whenever the translation + An index is also produced whenever the translation function cannot find an appropriate propositional formula for a term. - Given the ML-value + Attempting to translate @{term "\<forall>x::nat. P x"} *} -ML{*val (form', tab') = +ML{*val (pform', table') = 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 + 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 tab')" + "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" "(\<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 + 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\" form" - "SatSolver.SATISFIABLE ass"} + "SatSolver.invoke_solver \"dpll\" pform" + "SatSolver.SATISFIABLE assg"} - determines that the formula @{ML form} is satisfiable. If we inspect - the returned function @{text ass} + determines that the formula @{ML pform} is satisfiable. If we inspect + the returned function @{text assg} @{ML_response [display,gray] "let - val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form + val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform in - (ass 1, ass 2, ass 3) + (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. - If we instead invoke the SAT solver with the string @{text [quotes] "auto"} + 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\" form"} + @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"} - several external SAT solvers will be tried (if they are installed) and - the default is the internal SAT solver @{text [quotes] "dpll"}. + 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 the SAT solvers. One + There are also two tactics that make use of SAT solvers. One is the tactic @{ML sat_tac in sat}. For example *} @@ -97,6 +104,9 @@ done text {* + However, for prove 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 diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Tactical.thy --- a/CookBook/Tactical.thy Tue Mar 17 17:32:12 2009 +0100 +++ b/CookBook/Tactical.thy Wed Mar 18 03:03:51 2009 +0100 @@ -2068,7 +2068,10 @@ *} - +text {* + (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term} + are of any use/efficient) +*} section {* Structured Proofs (TBD) *} diff -r 8bb4eaa2ec92 -r c7f04a008c9c cookbook.pdf Binary file cookbook.pdf has changed