author haftmann Wed Feb 14 10:07:17 2007 +0100 (2007-02-14) changeset 22322 b9924abb8c66 parent 22321 e5cddafe2629 child 22323 b8c227d8ca91
continued
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Feb 14 10:06:17 2007 +0100
1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Feb 14 10:07:17 2007 +0100
1.3 @@ -110,7 +110,56 @@
1.4    \end{mldecls}
1.5  *}
1.6
1.7 -text FIXME
1.8 +(*<*)
1.9 +typedecl foo
1.10 +consts foo :: foo
1.11 +ML {*
1.12 +val dummy_const = ("bar", @{typ foo}, NoSyn)
1.13 +val dummy_def = ("bar", @{term foo})
1.14 +val thy = Theory.copy @{theory}
1.15 +*}
1.16 +(*>*)
1.17 +
1.18 +text {*
1.19 +  Many problems in functional programming can be thought of
1.20 +  as linear transformations, i.e.~a caluclation starts with a
1.21 +  particular value @{text "x \<Colon> foo"} which is then transformed
1.22 +  by application of a function @{text "f \<Colon> foo \<Rightarrow> foo"},
1.23 +  continued by an application of a function @{text "g \<Colon> foo \<Rightarrow> bar"},
1.24 +  and so on.  As a canoncial example, take primitive functions enriching
1.25 +  theories by constants and definitions:
1.26 +  @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory"}
1.27 +  and @{ML "Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory"}.
1.28 +  Written with naive application, an addition of a constant with
1.29 +  a corresponding definition would look like:
1.31 +  With increasing numbers of applications, this code gets quite unreadable.
1.32 +  Using composition, at least the nesting of brackets may be reduced:
1.34 +  What remains unsatisfactory is that things are written down in the opposite order
1.35 +  as they actually happen''.
1.36 +*}
1.37 +
1.38 +(*<*)
1.39 +ML {*
1.40 +val thy = Theory.copy @{theory}
1.41 +*}
1.42 +(*>*)
1.43 +
1.44 +text {*
1.45 +  At this stage, Isabelle offers some combinators which allow for more convenient
1.46 +  notation, most notably reverse application:
1.47 +  @{ML "
1.48 +thy
1.50 +|> Theory.add_defs_i false false [dummy_def]"}
1.51 +*}
1.52 +
1.53 +text {*
1.54 +  When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
1.55 +  the @{ML fold} combinator lifts a single function @{text "f \<Colon> 'a -> 'b -> 'b"}:
1.56 +  @{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"}
1.57 +*}
1.58
1.59  text %mlref {*
1.60    \begin{mldecls}
1.61 @@ -122,6 +171,10 @@
1.62    \end{mldecls}
1.63  *}
1.64
1.65 +text {*
1.66 +  FIXME transformations involving side results
1.67 +*}
1.68 +
1.69  text %mlref {*
1.70    \begin{mldecls}
1.71    @{index_ML "(op #>)": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
1.72 @@ -132,6 +185,10 @@
1.73    \end{mldecls}
1.74  *}
1.75
1.76 +text {*
1.77 +  FIXME higher-order variants
1.78 +*}
1.79 +
1.80  text %mlref {*
1.81    \begin{mldecls}
1.82    @{index_ML "(op )": "('b -> 'a) -> 'b -> 'a * 'b"} \\

     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Feb 14 10:06:17 2007 +0100
2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Feb 14 10:07:17 2007 +0100
2.3 @@ -151,8 +151,67 @@
2.4  %
2.6  %
2.8 +%
2.10 +%
2.11 +\isatagML
2.12 +%
2.13 +\endisatagML
2.14 +{\isafoldML}%
2.15 +%
2.17 +%
2.19 +%
2.20  \begin{isamarkuptext}%
2.21 -FIXME%
2.22 +Many problems in functional programming can be thought of
2.23 +  as linear transformations, i.e.~a caluclation starts with a
2.24 +  particular value \isa{x\ {\isasymColon}\ foo} which is then transformed
2.25 +  by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo},
2.26 +  continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
2.27 +  and so on.  As a canoncial example, take primitive functions enriching
2.28 +  theories by constants and definitions:
2.29 +  \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory|
2.30 +  and \verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory|.
2.31 +  Written with naive application, an addition of a constant with
2.32 +  a corresponding definition would look like:
2.34 +  With increasing numbers of applications, this code gets quite unreadable.
2.35 +  Using composition, at least the nesting of brackets may be reduced:
2.37 +  What remains unsatisfactory is that things are written down in the opposite order
2.38 +  as they actually happen''.%
2.39 +\end{isamarkuptext}%
2.40 +\isamarkuptrue%
2.41 +%
2.43 +%
2.45 +%
2.46 +\isatagML
2.47 +%
2.48 +\endisatagML
2.49 +{\isafoldML}%
2.50 +%
2.52 +%
2.54 +%
2.55 +\begin{isamarkuptext}%
2.56 +At this stage, Isabelle offers some combinators which allow for more convenient
2.57 +  notation, most notably reverse application:
2.58 +  \isasep\isanewline%
2.59 +\verb|thy|\isasep\isanewline%
2.61 +\verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|%
2.62 +\end{isamarkuptext}%
2.63 +\isamarkuptrue%
2.64 +%
2.65 +\begin{isamarkuptext}%
2.66 +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},
2.67 +  the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
2.68 +  \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}%
2.69  \end{isamarkuptext}%
2.70  \isamarkuptrue%
2.71  %
2.72 @@ -173,6 +232,24 @@
2.73  \end{isamarkuptext}%
2.74  \isamarkuptrue%
2.75  %
2.76 +\endisatagmlref
2.77 +{\isafoldmlref}%
2.78 +%
2.80 +%
2.82 +%
2.83 +\begin{isamarkuptext}%
2.84 +FIXME transformations involving side results%
2.85 +\end{isamarkuptext}%
2.86 +\isamarkuptrue%
2.87 +%
2.89 +%
2.91 +%
2.92 +\isatagmlref
2.93 +%
2.94  \begin{isamarkuptext}%
2.95  \begin{mldecls}
2.96    \indexml{(op \#$>$)}\verb|(op #>): ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
2.97 @@ -184,6 +261,24 @@
2.98  \end{isamarkuptext}%
2.99  \isamarkuptrue%
2.100  %
2.101 +\endisatagmlref
2.102 +{\isafoldmlref}%
2.103 +%
2.105 +%
2.107 +%
2.108 +\begin{isamarkuptext}%
2.109 +FIXME higher-order variants%
2.110 +\end{isamarkuptext}%
2.111 +\isamarkuptrue%
2.112 +%
2.114 +%
2.116 +%
2.117 +\isatagmlref
2.118 +%
2.119  \begin{isamarkuptext}%
2.120  \begin{mldecls}
2.121    \indexml{(op )}\verb|(op ): ('b -> 'a) -> 'b -> 'a * 'b| \\

     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Feb 14 10:06:17 2007 +0100
3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Feb 14 10:07:17 2007 +0100
3.3 @@ -435,7 +435,7 @@
3.4  \end{isamarkuptext}%
3.5  \isamarkuptrue%
3.6  %
3.7 -\isamarkupsubsection{Primitive connectives and rules%
3.8 +\isamarkupsubsection{Primitive connectives and rules \label{sec:prim_rules}%
3.9  }
3.10  \isamarkuptrue%
3.11  %

     4.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Feb 14 10:06:17 2007 +0100
4.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Feb 14 10:07:17 2007 +0100
4.3 @@ -434,7 +434,7 @@
4.4    notion of equality/equivalence @{text "\<equiv>"}.
4.5  *}
4.6
4.7 -subsection {* Primitive connectives and rules *}
4.8 +subsection {* Primitive connectives and rules \label{sec:prim_rules} *}
4.9
4.10  text {*
4.11    The theory @{text "Pure"} contains constant declarations for the
`