--- 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"} \\
--- 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| \\
--- 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%
%
--- 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