--- a/CookBook/FirstSteps.thy	Mon Feb 16 17:17:24 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Feb 17 02:12:19 2009 +0000
@@ -114,7 +114,9 @@
 
   You can print out error messages with the function @{ML error}; for example:
 
-  @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
+@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
+"Exception- ERROR \"foo\" raised
+At command \"ML\"."}
 
   Section~\ref{sec:printing} will give more information about printing 
   the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 
@@ -122,8 +124,6 @@
 *}
 
 
-
-
 section {* Antiquotations *}
 
 text {*
@@ -161,7 +161,7 @@
 
   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 
-  and simpsets:
+  and current simpsets:
 
   @{ML_response_fake [display,gray] 
 "let
@@ -171,7 +171,7 @@
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
   The code about simpsets extracts the theorem names stored in the
-  current simpset.  You can get hold of the current simpset with the antiquotation 
+  simpset.  You can get hold of the current simpset with the antiquotation 
   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   containing all information about the simpset. The rules of a simpset are
   stored in a \emph{discrimination net} (a data structure for fast
@@ -197,8 +197,8 @@
   packages. Antiquotations solve this problem, since they are ``linked''
   statically at compile-time.  However, this static linkage also limits their
   usefulness in cases where data needs to be build up dynamically. In the
-  course of this introduction, we will learn more about these antiquotations:
-  they greatly simplify Isabelle programming since one can directly access all
+  course of this introduction, you will learn more about these antiquotations:
+  they can simplify Isabelle programming since one can directly access all
   kinds of logical elements from th ML-level.
 
 *}
@@ -206,7 +206,7 @@
 section {* Terms and Types *}
 
 text {*
-  One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
+  One way to construct terms of Isabelle is by using the antiquotation 
   \mbox{@{text "@{term \<dots>}"}}. For example:
 
   @{ML_response [display,gray] 
@@ -245,8 +245,8 @@
 
   Hint: The third term is already quite big, and the pretty printer
   may omit parts of it by default. If you want to see all of it, you
-  can use the following ML-function to set the limit to a value high 
-  enough:
+  can use the following ML-function to set the printing depth to a higher 
+  value:
 
   @{ML [display,gray] "print_depth 50"}
   \end{exercise}
@@ -323,28 +323,6 @@
       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  (FIXME: expand the following point)
-
-  One tricky point in constructing terms by hand is to obtain the fully
-  qualified name for constants. For example the names for @{text "zero"} and
-  @{text "+"} are more complex than one first expects, namely
-
-
-  \begin{center}
-  @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. 
-  \end{center}
-  
-  The extra prefixes @{text zero_class} and @{text plus_class} are present
-  because these constants are defined within type classes; the prefix @{text
-  "HOL"} indicates in which theory they are defined. Guessing such internal
-  names can sometimes be quite hard. Therefore Isabelle provides the
-  antiquotation @{text "@{const_name \<dots>}"} which does the expansion
-  automatically, for example:
-
-  @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
-
-  (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
-
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
   when defining constants. For example the function returning a function 
@@ -359,21 +337,19 @@
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
-
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
   and types easier.\end{readmore}
 
   Have a look at these files and try to solve the following two exercises:
-
 *}
 
 text {*
 
   \begin{exercise}\label{fun:revsum}
   Write a function @{text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
+  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   associates to the left. Try your function on some examples. 
@@ -387,7 +363,7 @@
 
   A handy function for manipulating terms is @{ML map_types}: it takes a 
   function and applies it to every type in the term. You can, for example,
-  change every @{typ nat} in a term into an @{typ int} using the function
+  change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 
 ML{*fun nat_to_int t =
@@ -397,8 +373,7 @@
    | _ => t)*}
 
 text {*
-  an then apply it as follows:
-
+  An example as follows:
 
 @{ML_response_fake [display,gray] 
 "map_types nat_to_int @{term \"a = (1::nat)\"}" 
@@ -456,11 +431,109 @@
 
 *}
 
+section {* Constants *}
+
+text {*
+  There are a few subtle issues with constants. They usually crop up when
+  pattern matching terms or constructing term. While it is perfectly ok
+  to write the function @{text is_true} as follows
+*}
+
+ML{*fun is_true @{term True} = true
+  | is_true _ = false*}
+
+text {*
+  this does not work for picking out @{text "\<forall>"}-quantified terms. Because
+  the function 
+*}
+
+ML{*fun is_all (@{term All} $ _) = true
+  | is_all _ = false*}
+
+text {* 
+  will not correctly match: 
+
+  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+
+  The problem is that the @{text "@term"}-antiquotation in the pattern 
+  fixes the type of @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
+  an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
+  for this function is
+*}
+
+ML{*fun is_all (Const ("All", _) $ _) = true
+  | is_all _ = false*}
+
+text {* 
+  because now
+
+@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+
+  matches correctly.
+
+  However there is still a problem: consider the function that attempts to 
+  pick out a @{text "Nil"}-term:
+*}
+
+ML{*fun is_nil (Const ("Nil", _)) = true
+  | is_nil _ = false *}
+
+text {* 
+  Unfortunately, also this one does not return the expected result, since
+
+  @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
+
+  The problem is that on the ML-level the name of constants is not
+  immediately clear. If you look at
+
+  @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
+
+  the name of the constant depends on the theory in which the term constructor
+  @{text "Nil"} is defined and also in which datatype. Even worse, some
+  constants have an even more complex name involving type-classes. Consider 
+  for example
+
+  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
+  "(Const (\"HOL.zero_class.zero\", \<dots>), 
+ Const (\"HOL.times_class.times\", \<dots>))"}
+
+  While you could always use the complete name, for example 
+  @{ML "Const (\"List.list.Nil\", @{typ \"nat list\"})"}, for referring to or
+  matching against @{text "Nil"}, this would make the code rather brittle. 
+  The reason is that the theory and the name of the datatype can easily change. 
+  To make the code more robust it is better to use the antiquotation 
+  @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
+  variable parts of the constant's name. Therefore the functions for 
+  matching against constants should be written as follows.
+*}
+
+ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+  | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
+  | is_nil_or_all _ = false *}
+
+text {*
+  Having said this, you also frequently have to calculate what the
+  ``base''  name of a constant is. For this you can use the function 
+  @{ML Sign.base_name}. For example:
+  
+  (FIXME is there an example for that statement?)
+
+
+  @{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
+
+  (FIXME authentic syntax?)
+
+  \begin{readmore}
+  FIXME
+  \end{readmore}
+*}
+
+
 section {* Theorems *}
 
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
-  that can only be built by going through interfaces. As a consequence, every proof 
+  that can only be build by going through interfaces. As a consequence, every proof 
   in Isabelle is correct by construction. 
 
   (FIXME reference LCF-philosophy)
@@ -585,30 +658,6 @@
   commas (map (str_of_thm ctxt) thms)*}
 
 
-section {* Operations on Constants (Names) *}
-
-text {*
-
-@{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
-
-  authentic syntax?
-
-*}
-
-ML {* @{const_name lfp} *}
-
-text {*
-  constants in case-patterns?
-
-  In the meantime, lfp has been moved to the Inductive theory, so it is  
-  no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been  
-  used, we would have gotten an error for this. Another advantage of the  
-  antiquotation is that we can then just write @{text "@{const_name lfp}"} rather  
-  than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct  
-  name.
-  
-*}
-
 section {* Combinators\label{sec:combinators} *}
 
 text {*

--- a/CookBook/Intro.thy	Mon Feb 16 17:17:24 2009 +0000
+++ b/CookBook/Intro.thy	Tue Feb 17 02:12:19 2009 +0000
@@ -15,7 +15,7 @@
   against recent versions of Isabelle.  If something does not work, then
   please let us know. If you have comments, criticism or like to add to the
   tutorial, feel free---you are most welcome! The tutorial is meant to be 
-  gentle and comprehensive.
+  gentle and comprehensive. To achieve this we need your feedback.
 *}
 
 section {* Intended Audience and Prior Knowledge *}
@@ -94,10 +94,10 @@
 
   @{ML_response [display,gray] "3 + 4" "7"}
 
-  The usual user-level commands of Isabelle are written in bold, for 
-  example \isacommand{lemma}, \isacommand{foobar} and so on.  
-  We use @{text "$"} to indicate that a command  needs to be run 
-  in a Unix-shell, for example:
+  The user-level commands of Isabelle (i.e.~the non-ML code) are written
+  in bold, for example \isacommand{lemma}, \isacommand{apply},
+  \isacommand{foobar} and so on.  We use @{text "$"} to indicate that a
+  command needs to be run in a Unix-shell, for example:
 
   @{text [display] "$ ls -la"}
 
@@ -114,13 +114,15 @@
 
 text {*
   Financial support for this tutorial was provided by the German 
-  Research Council (DFG) under grant number URB 165/5-1.
+  Research Council (DFG) under grant number URB 165/5-1. The following
+  people contributed:
 
   \begin{itemize}
-  \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the 
-  \simpleinductive-package and the code for the @{text "chunk"}-antiquotation. He also wrote the first
-  version of the chapter describing the package and has be 
-  helpful \emph{beyond measure} with answering questions about Isabelle. 
+  \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
+  \simpleinductive-package and the code for the @{text
+  "chunk"}-antiquotation. He also wrote the first version of the chapter
+  describing the package and has been helpful \emph{beyond measure} with
+  answering questions about Isabelle.
 
   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.

--- a/CookBook/Parsing.thy	Mon Feb 16 17:17:24 2009 +0000
+++ b/CookBook/Parsing.thy	Tue Feb 17 02:12:19 2009 +0000
@@ -1,6 +1,5 @@
 theory Parsing
 imports Base "Package/Simple_Inductive_Package"
-
 begin
 
 

--- a/CookBook/ROOT.ML	Mon Feb 16 17:17:24 2009 +0000
+++ b/CookBook/ROOT.ML	Tue Feb 17 02:12:19 2009 +0000
@@ -1,13 +1,13 @@
 set quick_and_dirty;
 
 no_document use_thy "Base";
+no_document use_thy "Package/Simple_Inductive_Package";
 
 use_thy "Intro";
 use_thy "FirstSteps";
 use_thy "Parsing";
 use_thy "Tactical";
 
-no_document use_thy "Package/Simple_Inductive_Package";
 use_thy "Package/Ind_Intro";
 use_thy "Package/Ind_Examples";
 use_thy "Package/Ind_General_Scheme";

Binary file cookbook.pdf has changed