
diff -r 8fda6b452f28 -r 6dfe6975bda0 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Mon Jan 26 16:09:02 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Jan 27 05:41:14 2009 +0000
@@ -510,10 +510,10 @@
 section {* Combinators\label{sec:combinators} *}
 
 text {*
-  Perhaps one of the most puzzling aspect for a beginner when reading  
-  existing Isabelle code special purpose combinators. At first they 
-  seem to obstruct the comprehension of the code, but after getting familiar 
-  with them they actually ease the understanding and also the programming.
+  For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
+  the combinators. At first they seem to greatly obstruct the
+  comprehension of the code, but after getting familiar with them, they
+  actually ease the understanding and also the programming.
 
   \begin{readmore}
   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
@@ -525,15 +525,16 @@
 
 ML{*fun I x = x*}
 
-text {* Another combinator is @{ML K}, defined as *}
+text {* Another simple combinator is @{ML K}, defined as *}
 
 ML{*fun K x = fn _ => x*}
 
 text {*
   It ``wraps'' a function around the argument @{text "x"}. However, this 
-  function ignores its argument. 
+  function ignores its argument. So @{ML K} defines a constant function 
+  returning @{text x}.
 
-  The next combinator is reverse application, @{ML "(op |>)"}, defined as 
+  The next combinator is reverse application, @{ML "|>"}, defined as 
 *}
 
 ML{*fun x |> f = f x*}
@@ -554,7 +555,8 @@
   the first component of the pair (Line 4) and finally incrementing the first 
   component by 4 (Line 5). This kind of cascading manipulations of values is quite
   common when dealing with theories (for example by adding a definition, followed by
-  lemmas and so on). Writing the function @{ML inc_by_five} using the reverse
+  lemmas and so on). It should also be familiar to anyone who has used Haskell's
+  do-notation. Writing the function @{ML inc_by_five} using the reverse
   application is much clearer than writing
 *}
 
@@ -575,9 +577,13 @@
    in y4 end*}
 
 text {* 
+  Another reason why the let-bindings in the code above are better to be
+  avoided: it is more than easy to get the intermediate values wrong!
+
+
   (FIXME: give a real world example involving theories)
 
-  Similarly, the combinator @{ML "(op #>)"} is the reverse function 
+  Similarly, the combinator @{ML "#>"} is the reverse function 
   composition. It can be used to define functions as follows
 *}
 
@@ -588,33 +594,30 @@
 
 text {* 
   which is the function composed of first the increment-by-one function and then
-  increment-by-two, followed by increment-by-three. Applying 6 to this function 
-  yields
-
-  @{ML_response [display,gray] "inc_by_six 6" "12"}
-
-  as expected.
+  increment-by-two, followed by increment-by-three. 
 
-  The remaining combinators add convenience for the ``waterfall method''
-  of writing functions. The combinator @{ML tap} allows one to get 
-  hold of an intermediate result (to do some side-calculations for instance). 
-  The function *}
+  The remaining combinators described in this section add convenience for the
+  ``waterfall method'' of writing functions. The combinator @{ML tap} allows
+  one to get hold of an intermediate result (to do some side-calculations for
+  instance). The function
 
-ML{*fun inc_by_three x =
+ *}
+
+ML %linenumbers{*fun inc_by_three x =
      x |> (fn x => x + 1)
        |> tap (fn x => tracing (makestring x))
        |> (fn x => x + 2)*}
 
 text {* increments the argument first by one and then by two. In the middle,
   however, it uses @{ML tap} for printing the ``plus-one'' intermediate 
-  result inside the tracing buffer.
+  result inside the tracing buffer (Line 3). The function @{ML tap} can only
+  be used for side-calculations, because any value that is computed cannot
+  be merged back into the ``main waterfall''. To do this, the next combinator
+  can be used.
 
-  The combinator @{ML "(op `)"} is similar, but applies a function to the value
-  and returns the result together with the original value (as pair). For example
-  the following function takes @{text x} as argument, and then first 
-  increments @{text x}, but also keeps @{text x}. The intermediate result is 
-  therefore the pair @{ML "(x + 1,x)" for x}. The function then increments the 
-  right-hand component of the pair.
+  The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
+  and returns the result together with the value (as a pair). For example
+  the function 
 *}
 
 ML{*fun inc_as_pair x =
@@ -622,7 +625,13 @@
        |> (fn (x, y) => (x, y + 1))*}
 
 text {*
-  The combinators @{ML "(op |>>)"} and @{ML "(op ||>)"} are defined for 
+  takes @{text x} as argument, and then first 
+  increments @{text x}, but also keeps @{text x}. The intermediate result is 
+  therefore the pair @{ML "(x + 1, x)" for x}. The function then increments the 
+  right-hand component of the pair. So finally the result will be 
+  @{ML "(x + 1, x + 1)" for x}.
+
+  The combinators @{ML "|>>"} and @{ML "||>"} are defined for 
   functions manipulating pairs. The first applies the function to
   the first component of the pair, defined as:
 *}
@@ -636,6 +645,35 @@
 ML{*fun (x, y) ||> f = (x, f y)*}
 
 text {*
+  With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+  This combinator is defined as
+*}
+
+ML{*fun (x, y) |-> f = f x y*}
+
+text {* and can be used to write the following version of the @{text double} function *}
+
+ML{*fun double x =
+      x |>  (fn x => (x, x))
+        |-> (fn x => fn y => x + y)*}
+
+text {*
+  Recall that @{ML "|>"} is the reverse function applications. The related 
+  reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"},
+  @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
+  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. In this
+  way, the function @{text double} can also be written as
+*}
+
+ML{*val double =
+            (fn x => (x, x))
+        #-> (fn x => fn y => x + y)*}
+  
+
+text {*
+  
+
+
   (FIXME: find a good exercise for combinators)
 *}
 




