--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Appendix.thy	Wed Oct 01 20:09:45 2008 -0400
@@ -0,0 +1,15 @@
+
+theory Appendix
+imports Main
+begin
+
+text {* \appendix *}
+
+chapter {* Recipes *}
+
+
+end
+  
+
+
+

--- a/CookBook/FirstSteps.thy	Wed Oct 01 15:40:20 2008 -0400
+++ b/CookBook/FirstSteps.thy	Wed Oct 01 20:09:45 2008 -0400
@@ -64,6 +64,8 @@
   then Isabelle's undo operation has no effect on the definition of 
   @{ML "foo"}. 
 
+  (FIXME: add comment about including whole ML-files) 
+
   During developments you might find it necessary to quickly inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
   the function @{ML "warning"}. For example 
@@ -75,8 +77,8 @@
 
 text {*
   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
-  PolyML provides a convenient, though quick-and-dirty, method for converting 
-  arbitrary values into strings, for example: 
+  PolyML provides a convenient, though again ``quick-and-dirty'', method for 
+  converting arbitrary values into strings, for example: 
 *}
 
 ML {*
@@ -88,8 +90,8 @@
   a function.
 *}
 
-text {* (FIXME: add comment about including ML-files) *}
-
+text {* (FIXME: add here or in the appendix a comment about tracing) *}
+text {* (FIXME: maybe a comment about redirecting the trace information) *}
 
 section {* Antiquotations *}
 
@@ -106,7 +108,7 @@
 text {* 
   where @{text "@{theory}"} is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory CookBook). 
-  The name of this theory can be extrated using the function @{ML "Context.theory_name"}. 
+  The name of this theory can be extracted using the function @{ML "Context.theory_name"}. 
   So the code above returns the string @{ML "\"CookBook\""}.
 
   Note, however, that antiquotations are statically scoped, that is the value is
@@ -135,7 +137,7 @@
 
 text {*
   In the course of this introduction, we will learn more about 
-  these antoquotations: they greatly simplify Isabelle programming since one
+  these antiquotations: they greatly simplify Isabelle programming since one
   can directly access all kinds of logical elements from ML.
 
 *}
@@ -151,8 +153,8 @@
 
 text {*
   This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
-  representation of this term. This internal represenation corresponds to the 
-  datatype defined in @{ML_file "Pure/term.ML"}.
+  representation of this term. This internal representation corresponds to the 
+  datatype @{ML_text "term"}.
   
   The internal representation of terms uses the usual de-Bruijn index mechanism where bound 
   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
@@ -161,14 +163,16 @@
   kept at abstractions for printing purposes, and so should be treated only as comments. 
 
   \begin{readmore}
-  Terms are described in detail in \ichcite{ch:logic}. Their
+  Terms are described in detail in \isccite{sec:terms}. Their
   definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
   \end{readmore}
 
-  Sometimes the internal representation can be surprisingly different
+  Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user level, because the layers of
   parsing/type checking/pretty printing can be quite elaborate. 
+*}
 
+text {*
   \begin{exercise}
   Look at the internal term representation of the following terms, and
   find out why they are represented like this.
@@ -181,43 +185,45 @@
 
   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 @{ML "print_depth 50"} to set the limit to a value high enough.
+  can use the following ML funtion to set the limit to a value high 
+  enough:
   \end{exercise}
+*}
+ML {* print_depth 50 *} 
 
-  The anti-quotation @{text "@prop"} constructs terms of proposition type, 
-  inserting the invisible @{text "Trueprop"} coercion when necessary. 
+text {*
+  
+  The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
+  inserting the invisible @{text "Trueprop"} coercions whenever necessary. 
   Consider for example
 
 *}
 
-ML {* @{term "P x"} *}
+ML {* @{term "P x"} ; @{prop "P x"} *}
 
-ML {* @{prop "P x"} *}
-
-text {* and *}
+text {* which needs the coercion and *}
 
 
-ML {* @{term "P x \<Longrightarrow> Q x"} *}
+ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
-ML {* @{prop "P x \<Longrightarrow> Q x"} *}
+text {* which does not. *}
 
-section {* Construting Terms Manually *} 
+section {* Constructing Terms Manually *} 
 
 text {*
 
   While antiquotations are very convenient for constructing terms, they can
-  only construct fixed terms. However, one often needs to construct terms dynamially. 
-  For example in order to write the function that returns the implication 
-  @{term "\<And>x. P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments, one can 
-  only write
+  only construct fixed terms. Unfortunately, one often needs to construct terms 
+  dynamically. For example, a function that returns the implication 
+  @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as input terms 
+  can only be written as
 *}
 
 
 ML {*
-  fun make_PQ_imp P Q =
+  fun make_imp P Q =
   let
-    val nat = HOLogic.natT
-    val x = Free ("x", nat)
+    val x = @{term "x::nat"}
   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
                                     HOLogic.mk_Trueprop (Q $ x)))
   end
@@ -226,45 +232,52 @@
 text {*
 
   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
-  an antiquotation. 
+  an antiquotation, like   
+*}
+
+ML {*
+  fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
 *}
 
 text {*
 
-   The internal names of constants like @{term "zero"} or @{text "+"} are
-  often more complex than one first expects. Here, the extra prefixes
-  @{text zero_class} and @{text plus_class} are present because the
-  constants are defined within a type class. Guessing such internal
-  names can be extremely hard, which is why the system provides
-  another antiquotation: @{ML "@{const_name plus}"} gives just this
-  name. For example 
+  To see the difference apply @{text "@{term S}"} and 
+  @{text "@{term T}"} to the functions.
+  
+
+  One tricky point in constructing terms by hand is to obtain the fully qualified 
+  names for constants. For example the names for @{text "zero"} or @{text "+"} are
+  more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"} 
+  and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class} 
+  and @{ML_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 
+  Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} does the expansion 
+  automatically, for example:
 
 *}
 
-ML {* @{const_name plus} *}
-
-text {* produes the fully qualyfied name of the constant plus. *}
-
-
-
+ML {* @{const_name HOL.zero}; @{const_name  plus} *}
 
 text {*
 
-  There are many funtions in @{ML_file "Pure/logic.ML"} and
+  \begin{readmore}
+  There are many functions in @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
-  easier. Have a look ther and try to solve the following exercises:
+  easier.\end{readmore}
+
+  Have a look at these files and try to solve the following two exercises:
 
 *}
 
 text {*
 
-  \begin{exercise}
+  \begin{exercise}\label{fun:revsum}
   Write a function @{ML_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)
   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, and see if 
-  the result typechecks. 
+  associates to the left. Try your function on some examples. 
   \end{exercise}
 *}
 
@@ -298,10 +311,12 @@
 section {* Type checking *}
 
 text {* 
+  
+  (FIXME: Should we say something about types?)
+
   We can freely construct and manipulate terms, since they are just
   arbitrary unchecked trees. However, we eventually want to see if a
-  term is wellformed, or type checks, relative to a theory.
-
+  term is well-formed, or type checks, relative to a theory.
   Type checking is done via the function @{ML cterm_of}, which turns 
   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   Unlike @{ML_type term}s, which are just trees, @{ML_type
@@ -327,37 +342,38 @@
   end
 *}
 
+text {*
+  
+  \begin{exercise}
+  Check that the function defined in Exercise~\ref{fun:revsum} returns a
+  result that type checks.
+  \end{exercise}
+
+*}
+
 section {* Theorems *}
 
 text {*
   Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are
   abstract objects that can only be built by going through the kernel
-  interfaces, which means that all your proofs will be checked. The
-  basic rules of the Isabelle/Pure logical framework are defined in
-  @{ML_file "Pure/thm.ML"}. 
+  interfaces, which means that all your proofs will be checked. 
 
-  Using these rules, which are just ML functions, you can do simple
-  natural deduction proofs on the ML level. For example, the statement
+  To see theorems in ``action'', let us give a proof for the following statement
 *}
 
   lemma 
    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
    and     assm\<^isub>2: "P t"
-   shows "Q t"
-   (*<*)oops(*>*) 
+   shows "Q t" (*<*)oops(*>*) 
 
 text {*
-  can be proved in ML like 
-  this\footnote{Note that @{text "|>"} is just reverse
+  on the ML level:\footnote{Note that @{text "|>"} is just reverse
   application. This combinator, and several variants are defined in
-  @{ML_file "Pure/General/basics.ML"}}:
+  @{ML_file "Pure/General/basics.ML"}.}
 
 *}
 
-
-
 ML {*
-
 let
   val thy = @{theory}
 
@@ -375,13 +391,15 @@
   |> implies_intr assm2
   |> implies_intr assm1
 end
-
 *}
 
 text {*
-  For how the functions @{text "assume"}, @{text "forall_elim"} and so on work
-  see \ichcite{sec:thms}. (FIXME correct name)
 
+  \begin{readmore}
+  For how the functions @{text "assume"}, @{text "forall_elim"} etc work
+  see \isccite{sec:thms}. The basic functions for theorems are defined in
+  @{ML_file "Pure/thm.ML"}. 
+  \end{readmore}
 
 *}
 
@@ -389,20 +407,26 @@
 section {* Tactical Reasoning *}
 
 text {*
-  The goal-oriented tactical style is similar to the @{text apply}
-  style at the user level. Reasoning is centered around a \emph{goal},
-  which is modified in a sequence of proof steps until it is solved.
+  The goal-oriented tactical style reasoning of the ML level is similar 
+  to the @{text apply}-style at the user level, i.e.~the reasoning is centred 
+  around a \emph{goal}, which is modified in a sequence of proof steps 
+  until it is solved.
 
   A goal (or goal state) is a special @{ML_type thm}, which by
   convention is an implication of the form:
 
   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
 
-  Since the formula @{term C} could potentially be an implication, there is a
+  where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. 
+
+  Since the goal @{term C} can potentially be an implication, there is a
   @{text "#"} wrapped around it, which prevents that premises are 
   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
   prop"} is just the identity function and used as a syntactic marker. 
-  For more on this goals see \ichcite{sec:tactical-goals}. (FIXME name)
+  
+  \begin{readmore}
+  For more on goals see \isccite{sec:tactical-goals}. 
+  \end{readmore}
 
   Tactics are functions that map a goal state to a (lazy)
   sequence of successor states, hence the type of a tactic is
@@ -410,18 +434,18 @@
   
   \begin{readmore}
   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
-  sequences. However one rarly onstructs sequences manually, but uses
-  the predefined tactic combinators (tacticals) instead 
-  (see @{ML_file "Pure/tctical.ML"}).
+  sequences. However in day-to-day Isabelle programming, one rarely 
+  constructs sequences explicitly, but uses the predefined tactic 
+  combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}). 
+  (FIXME: Pointer to the old reference manual)
   \end{readmore}
 
-  Note, however, that tactics are expected to behave nicely and leave 
-  the final conclusion @{term C} intact (that is only work on the @{text "A\<^isub>i"} 
-  representing the subgoals to be proved) with the exception of possibly 
-  instantiating schematic variables. 
+  While tatics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
+  are expected to leave the conclusion @{term C} intact, with the 
+  exception of possibly instantiating schematic variables. 
  
-  To see how tactics work, let us transcribe a simple apply-style proof from the
-  tutorial \cite{isa-tutorial} into ML:
+  To see how tactics work, let us transcribe a simple @{text apply}-style 
+  proof from the tutorial \cite{isa-tutorial} into ML:
 *}
 
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -437,9 +461,9 @@
   
   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
   sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
-  additional variables @{text params} (the variables that are generalised once the
-  goal is proved); @{text "tac"} is a function that returns a tactic (FIXME see non-existing
-  explanation in the imp-manual). 
+  the variables @{text params} that will be generalised once the
+  goal is proved; @{text "tac"} is a function that returns a tactic having some funny 
+  input parameters (FIXME by possibly having an explanation in the implementation-manual). 
 
 *}
 

--- a/CookBook/NamedThms.thy	Wed Oct 01 15:40:20 2008 -0400
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-
-theory NamedThms
-imports Main
-begin
-
-
-chapter {* Recipes *}
-
-text_raw {* 
-
-\section*{Accumulate a list of theorems under a name} 
-*}
-
-text {*
-  \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules.
-
-  Users should be able to declare @{text foo}-rules in the theory,
-  which are then used by some method.
-
-  \paragraph{Solution:}
-
-  *}
-ML {*
-  structure FooRules = NamedThmsFun(
-    val name = "foo" 
-    val description = "Rules for foo"
-  );
-*}
-
-setup FooRules.setup
-
-text {*
-  This declares a context data slot where the theorems are stored,
-  an attribute @{attribute foo} (with the usual @{text add} and @{text del} options
-  to declare new rules, and the internal ML interface to retrieve and 
-  modify the facts.
-
-  Furthermore, the facts are made available under the dynamic fact name
-  @{text foo}:
-*}
-
-lemma rule1[foo]: "A" sorry
-lemma rule2[foo]: "B" sorry
-
-declare rule1[foo del]
-
-thm foo
-
-ML {* 
-  FooRules.get @{context};
-*}
-
-
-text {* 
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
-  \end{readmore}
- *}
-
-
-end
-  
-
-
-

--- a/CookBook/ROOT.ML	Wed Oct 01 15:40:20 2008 -0400
+++ b/CookBook/ROOT.ML	Wed Oct 01 20:09:45 2008 -0400
@@ -3,5 +3,7 @@
 use_thy "Intro";
 use_thy "FirstSteps";
 use_thy "Parsing";
-use_thy "NamedThms";
-use_thy "Transformation";
\ No newline at end of file
+
+use_thy "Appendix";
+use_thy "Recipes/NamedThms";
+use_thy "Recipes/Transformation";
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Wed Oct 01 20:09:45 2008 -0400
@@ -0,0 +1,61 @@
+
+theory NamedThms
+imports Main
+begin
+
+
+section {* Accumulate a List of Theorems under a Name *} 
+
+
+text {*
+  \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules.
+
+  Users should be able to declare @{text foo}-rules in the theory,
+  which are then used by some method.
+
+  \paragraph{Solution:}
+
+  *}
+ML {*
+  structure FooRules = NamedThmsFun(
+    val name = "foo" 
+    val description = "Rules for foo"
+  );
+*}
+
+setup FooRules.setup
+
+text {*
+  This declares a context data slot where the theorems are stored,
+  an attribute @{attribute foo} (with the usual @{text add} and @{text del} options
+  to declare new rules, and the internal ML interface to retrieve and 
+  modify the facts.
+
+  Furthermore, the facts are made available under the dynamic fact name
+  @{text foo}:
+*}
+
+lemma rule1[foo]: "A" sorry
+lemma rule2[foo]: "B" sorry
+
+declare rule1[foo del]
+
+thm foo
+
+ML {* 
+  FooRules.get @{context};
+*}
+
+
+text {* 
+  \begin{readmore}
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+  \end{readmore}
+ *}
+
+
+end
+  
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Transformation.thy	Wed Oct 01 20:09:45 2008 -0400
@@ -0,0 +1,15 @@
+
+theory Transformation
+imports Main
+begin
+
+
+section {* Ad-hoc Transformations of Theorems *}
+
+
+
+end
+  
+
+
+

--- a/CookBook/Transformation.thy	Wed Oct 01 15:40:20 2008 -0400
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-
-theory Transformation
-imports Main
-begin
-
-
-text_raw {* 
-
-\section*{Ad-hoc Transformation of Theorems} 
-*}
-
-
-
-end
-  
-
-
-

--- a/CookBook/document/root.tex	Wed Oct 01 15:40:20 2008 -0400
+++ b/CookBook/document/root.tex	Wed Oct 01 20:09:45 2008 -0400
@@ -9,8 +9,8 @@
 \usepackage{xr}
 \externaldocument[I-]{implementation}
 \newcommand{\impref}[1]{\ref{I-#1}}
-\newcommand{\ichcite}[1]{[Impl.\,Man., ch.~\impref{#1}]}
-\newcommand{\isccite}[1]{[Impl.\,Man., sec.~\impref{#1}]}
+\newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]}
+\newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]}
 
 \usepackage{pdfsetup}
 

Binary file cookbook.pdf has changed