# HG changeset patch
# User haftmann
# Date 1171444037 -3600
# Node ID b9924abb8c66e937b555c20df890e5ff7804f973
# Parent  e5cddafe2629e8b4d1b0bea54aaae3a87e8511fa
continued

diff -r e5cddafe2629 -r b9924abb8c66 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Feb 14 10:06:17 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Feb 14 10:07:17 2007 +0100
@@ -110,7 +110,56 @@
   \end{mldecls}
 *}
 
-text FIXME
+(*<*)
+typedecl foo
+consts foo :: foo
+ML {*
+val dummy_const = ("bar", @{typ foo}, NoSyn)
+val dummy_def = ("bar", @{term foo})
+val thy = Theory.copy @{theory}
+*}
+(*>*)
+
+text {*
+  Many problems in functional programming can be thought of
+  as linear transformations, i.e.~a caluclation starts with a
+  particular value @{text "x \<Colon> foo"} which is then transformed
+  by application of a function @{text "f \<Colon> foo \<Rightarrow> foo"},
+  continued by an application of a function @{text "g \<Colon> foo \<Rightarrow> bar"},
+  and so on.  As a canoncial example, take primitive functions enriching
+  theories by constants and definitions:
+  @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory"}
+  and @{ML "Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory"}.
+  Written with naive application, an addition of a constant with
+  a corresponding definition would look like:
+  @{ML "Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)"}
+  With increasing numbers of applications, this code gets quite unreadable.
+  Using composition, at least the nesting of brackets may be reduced:
+  @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy"}
+  What remains unsatisfactory is that things are written down in the opposite order
+  as they actually ``happen''.
+*}
+
+(*<*)
+ML {*
+val thy = Theory.copy @{theory}
+*}
+(*>*)
+
+text {*
+  At this stage, Isabelle offers some combinators which allow for more convenient
+  notation, most notably reverse application:
+  @{ML "
+thy
+|> Sign.add_consts_i [dummy_const]
+|> Theory.add_defs_i false false [dummy_def]"}
+*}
+
+text {*
+  When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
+  the @{ML fold} combinator lifts a single function @{text "f \<Colon> 'a -> 'b -> 'b"}:
+  @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"}
+*}
 
 text %mlref {*
   \begin{mldecls}
@@ -122,6 +171,10 @@
   \end{mldecls}
 *}
 
+text {*
+  FIXME transformations involving side results
+*}
+
 text %mlref {*
   \begin{mldecls}
   @{index_ML "(op #>)": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
@@ -132,6 +185,10 @@
   \end{mldecls}
 *}
 
+text {*
+  FIXME higher-order variants
+*}
+
 text %mlref {*
   \begin{mldecls}
   @{index_ML "(op `)": "('b -> 'a) -> 'b -> 'a * 'b"} \\
diff -r e5cddafe2629 -r b9924abb8c66 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Feb 14 10:06:17 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Feb 14 10:07:17 2007 +0100
@@ -151,8 +151,67 @@
 %
 \endisadelimmlref
 %
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
 \begin{isamarkuptext}%
-FIXME%
+Many problems in functional programming can be thought of
+  as linear transformations, i.e.~a caluclation starts with a
+  particular value \isa{x\ {\isasymColon}\ foo} which is then transformed
+  by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo},
+  continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
+  and so on.  As a canoncial example, take primitive functions enriching
+  theories by constants and definitions:
+  \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory|
+  and \verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory|.
+  Written with naive application, an addition of a constant with
+  a corresponding definition would look like:
+  \verb|Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)|
+  With increasing numbers of applications, this code gets quite unreadable.
+  Using composition, at least the nesting of brackets may be reduced:
+  \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy|
+  What remains unsatisfactory is that things are written down in the opposite order
+  as they actually ``happen''.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+At this stage, Isabelle offers some combinators which allow for more convenient
+  notation, most notably reverse application:
+  \isasep\isanewline%
+\verb|thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\isasep\isanewline%
+\verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list},
+  the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
+  \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -173,6 +232,24 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+FIXME transformations involving side results%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{(op \#$>$)}\verb|(op #>): ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
@@ -184,6 +261,24 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+FIXME higher-order variants%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{(op `)}\verb|(op `): ('b -> 'a) -> 'b -> 'a * 'b| \\
diff -r e5cddafe2629 -r b9924abb8c66 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Feb 14 10:06:17 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Feb 14 10:07:17 2007 +0100
@@ -435,7 +435,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Primitive connectives and rules%
+\isamarkupsubsection{Primitive connectives and rules \label{sec:prim_rules}%
 }
 \isamarkuptrue%
 %
diff -r e5cddafe2629 -r b9924abb8c66 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Feb 14 10:06:17 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Feb 14 10:07:17 2007 +0100
@@ -434,7 +434,7 @@
   notion of equality/equivalence @{text "\<equiv>"}.
 *}
 
-subsection {* Primitive connectives and rules *}
+subsection {* Primitive connectives and rules \label{sec:prim_rules} *}
 
 text {*
   The theory @{text "Pure"} contains constant declarations for the