continued
authorhaftmann
Wed Feb 14 10:07:17 2007 +0100 (2007-02-14)
changeset 22322b9924abb8c66
parent 22321 e5cddafe2629
child 22323 b8c227d8ca91
continued
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/logic.thy
     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.30 +  @{ML "Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)"}
    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.33 +  @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy"}
    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.49 +|> Sign.add_consts_i [dummy_const]
    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.5  \endisadelimmlref
     2.6  %
     2.7 +\isadelimML
     2.8 +%
     2.9 +\endisadelimML
    2.10 +%
    2.11 +\isatagML
    2.12 +%
    2.13 +\endisatagML
    2.14 +{\isafoldML}%
    2.15 +%
    2.16 +\isadelimML
    2.17 +%
    2.18 +\endisadelimML
    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.33 +  \verb|Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)|
    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.36 +  \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy|
    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.42 +\isadelimML
    2.43 +%
    2.44 +\endisadelimML
    2.45 +%
    2.46 +\isatagML
    2.47 +%
    2.48 +\endisatagML
    2.49 +{\isafoldML}%
    2.50 +%
    2.51 +\isadelimML
    2.52 +%
    2.53 +\endisadelimML
    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.60 +\verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\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.79 +\isadelimmlref
    2.80 +%
    2.81 +\endisadelimmlref
    2.82 +%
    2.83 +\begin{isamarkuptext}%
    2.84 +FIXME transformations involving side results%
    2.85 +\end{isamarkuptext}%
    2.86 +\isamarkuptrue%
    2.87 +%
    2.88 +\isadelimmlref
    2.89 +%
    2.90 +\endisadelimmlref
    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.104 +\isadelimmlref
   2.105 +%
   2.106 +\endisadelimmlref
   2.107 +%
   2.108 +\begin{isamarkuptext}%
   2.109 +FIXME higher-order variants%
   2.110 +\end{isamarkuptext}%
   2.111 +\isamarkuptrue%
   2.112 +%
   2.113 +\isadelimmlref
   2.114 +%
   2.115 +\endisadelimmlref
   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