--- 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}

--- 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

--- 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 {*

--- 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

--- 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) *}

Binary file cookbook.pdf has changed