diff -r df09e49b19bf -r 733614e236a3 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Sep 17 19:20:37 2008 -0400
+++ b/CookBook/FirstSteps.thy	Tue Sep 30 03:30:40 2008 -0400
@@ -64,9 +64,9 @@
   then Isabelle's undo operation has no effect on the definition of 
   @{ML "foo"}. 
 
-  During coding you might find it necessary to quickly inspect some data
+  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 
-  @{ML "warning"}. For example
+  the function @{ML "warning"}. For example
 *}
 
 ML {*
@@ -130,26 +130,22 @@
 section {* Terms *}
 
 text {*
-  Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \<dots>}"} 
-  antiquotation:
+  One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
+  @{text "@{term \<dots>}"}:
 *}
 
 ML {* @{term "(a::nat) + b = c"} *}
 
 text {*
   This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
-  representation of this term. This internal represenation is just a 
+  representation of this term. This internal represenation corresponds to the 
   datatype defined in @{ML_file "Pure/term.ML"}.
   
-  The internal representation of terms uses the usual deBruin indices mechanism: bound 
-  variables are represented by the constructor @{ML Bound} whose argument refers to
+  The internal representation of terms uses the usual de-Bruijn indices mechanism where bound 
+  variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
   binds the corresponding variable. However, the names of bound variables are 
-  kept at abstractions for printing purposes, and so should be treated just as comments. 
-  See \ichcite{ch:logic} for more details.
-
-  (FIXME: Alex why is the reference bolow given. It somehow does not read
-  with what is written above.)
+  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
@@ -174,45 +170,6 @@
   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.
   \end{exercise}
-
-  \begin{exercise}
-  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"}
-  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}.
-  Note that @{text "+"} associates to the left.
-  Try your function on some examples, and see if the result typechecks.
-  \end{exercise}
-*}
-
-text {* FIXME: check possible solution *}
-
-ML {* 
-  exception FORM_ERROR 
-
-  fun rev_sum term =
-    case term of
-       @{term "op +"} $ (Free (x,t1)) $ (Free (y,t2)) => 
-                   @{term "op +"} $ (Free (y,t2)) $ (Free (x,t1))
-    |  @{term "op +"} $ left $ (Free (x,t)) => 
-                   @{term "op +"} $ (Free (x,t)) $ (rev_sum left)
-    |  _ => raise FORM_ERROR
-*}
-
-
-text {*
-  \begin{exercise}
-  Write a function which takes two terms representing natural numbers
-  in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
-  number representing their sum.
-  \end{exercise}
-
-  \begin{exercise}
-  Look at the functions defined in @{ML_file "Pure/logic.ML"} and
-  @{ML_file "HOL/hologic.ML"} and see if they can make your life
-  easier.
-  \end{exercise}
-
-  (FIXME what is coming next should fit with the main flow)
 *}
 
 ML {*
@@ -239,6 +196,77 @@
 
 
 
+section {* Possible Section on Construting Explicitly Terms *} 
+
+text {*
+
+  There is a disadvantage of using the @{text "@{term \<dots>}"} antiquotation
+  directly in order to construct terms. 
+*}
+
+ML {*
+
+  val nat = HOLogic.natT
+  val x = Free ("x", nat)
+  val t = Free ("t", nat)
+  val P = Free ("P", nat --> HOLogic.boolT)
+  val Q = Free ("Q", nat --> HOLogic.boolT)
+
+  val A1 = Logic.all x 
+           (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
+                              HOLogic.mk_Trueprop (Q $ x)))
+           
+
+  val A2 = HOLogic.mk_Trueprop (P $ t)
+
+*}
+
+text {*
+
+  \begin{exercise}
+  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. (FIXME: clash with the type-checking section later)
+  \end{exercise}
+*}
+
+ML {* 
+  fun rev_sum t =
+  let
+   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = 
+                                                      u' :: dest_sum u
+     | dest_sum u = [u]
+   in
+     foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
+   end;
+*}
+
+text {*
+  \begin{exercise}
+  Write a function which takes two terms representing natural numbers
+  in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
+  number representing their sum.
+  \end{exercise}
+
+*}
+
+ML {*
+  fun make_sum t1 t2 =
+      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
+*}
+
+
+text {*
+  \begin{exercise}
+  Look at the functions defined in @{ML_file "Pure/logic.ML"} and
+  @{ML_file "HOL/hologic.ML"} and see if they can make your life
+  easier.
+  \end{exercise}
+*}
+
 
 section {* Type checking *}
 
@@ -288,38 +316,9 @@
   application. This combinator, and several variants are defined in
   @{ML_file "Pure/General/basics.ML"}}:
 
-
-  (FIXME: Alex why did you not use antiquotations for this?)
 *}
 
-ML {*
-let
-  val thy = @{theory}
-  val nat = HOLogic.natT
-  val x = Free ("x", nat)
-  val t = Free ("t", nat)
-  val P = Free ("P", nat --> HOLogic.boolT)
-  val Q = Free ("Q", nat --> HOLogic.boolT)
 
-  val A1 = Logic.all x 
-           (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
-                              HOLogic.mk_Trueprop (Q $ x)))
-           |> cterm_of thy
-
-  val A2 = HOLogic.mk_Trueprop (P $ t)
-           |> cterm_of thy
-
-  val Pt_implies_Qt = 
-        assume A1
-        |> forall_elim (cterm_of thy t)
-
-  val Qt = implies_elim Pt_implies_Qt (assume A2)
-in
-  Qt 
-  |> implies_intr A2
-  |> implies_intr A1
-end
-*}
 
 ML {*
 
@@ -344,7 +343,7 @@
 *}
 
 text {*
-  FIXME Explain this program more carefully
+  FIXME Explain this program more carefully (@{ML_text assume},  @{ML_text "forall_elim"} \ldots)
 *}
 
 
@@ -409,6 +408,9 @@
   Tactics that affect only a certain subgoal, take a subgoal number as
   an integer parameter. Here we always work on the first subgoal,
   following exactly the @{text "apply"} script.
+
+  (Fixme: would it make sense to explain THEN' here)
+
 *}