continued
authorhaftmann
Tue Oct 23 10:53:15 2007 +0200 (2007-10-23)
changeset 251519374a0df240c
parent 25150 9d8893e9f381
child 25152 bfde2f8c0f63
continued
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/isabelle.sty
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 22 21:32:12 2007 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 23 10:53:15 2007 +0200
     1.3 @@ -296,8 +296,6 @@
     1.4  text %mlref {*
     1.5    \begin{mldecls}
     1.6    @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
     1.7 -  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
     1.8 -  @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
     1.9    \end{mldecls}
    1.10  *}
    1.11  
    1.12 @@ -305,8 +303,6 @@
    1.13  typedecl foo
    1.14  consts foo :: foo
    1.15  ML {*
    1.16 -val dummy_const = ("bar", @{typ foo}, NoSyn)
    1.17 -val dummy_def = ("bar", @{term foo})
    1.18  val thy = Theory.copy @{theory}
    1.19  *}
    1.20  (*>*)
    1.21 @@ -317,22 +313,30 @@
    1.22    particular value @{text "x \<Colon> foo"} which is then transformed
    1.23    by application of a function @{text "f \<Colon> foo \<Rightarrow> foo"},
    1.24    continued by an application of a function @{text "g \<Colon> foo \<Rightarrow> bar"},
    1.25 -  and so on.  As a canoncial example, take primitive functions enriching
    1.26 -  theories by constants and definitions:
    1.27 -  @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory
    1.28 --> theory"}
    1.29 -  and @{ML "Theory.add_defs_i: bool -> bool
    1.30 --> (bstring * term) list -> theory -> theory"}.
    1.31 -  Written with naive application, an addition of a constant with
    1.32 -  a corresponding definition would look like:
    1.33 -  @{ML "Theory.add_defs_i false false [dummy_def]
    1.34 -  (Sign.add_consts_i [dummy_const] thy)"}.
    1.35 -  With increasing numbers of applications, this code gets quite unreadable.
    1.36 -  Using composition, at least the nesting of brackets may be reduced:
    1.37 -  @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i
    1.38 -  [dummy_const]) thy"}.
    1.39 -  What remains unsatisfactory is that things are written down in the opposite order
    1.40 -  as they actually ``happen''.
    1.41 +  and so on.  As a canoncial example, take functions enriching
    1.42 +  a theory by constant declararion and primitive definitions:
    1.43 +
    1.44 +  \begin{quotation}
    1.45 +    @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
    1.46 +       -> theory -> term * theory"}
    1.47 +
    1.48 +    @{ML "Thm.add_def: bool -> bstring * term -> theory -> thm * theory"}
    1.49 +  \end{quotation}
    1.50 +
    1.51 +  Written with naive application, an addition of constant
    1.52 +  @{text bar} with type @{typ "foo \<Rightarrow> foo"} and
    1.53 +  a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
    1.54 +
    1.55 +  \begin{quotation}
    1.56 +  @{ML "(fn (t, thy) => Thm.add_def false
    1.57 +  (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
    1.58 +    (Sign.declare_const []
    1.59 +      (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}.
    1.60 +  \end{quotation}
    1.61 +
    1.62 +  With increasing numbers of applications, this code gets quite
    1.63 +  unreadable.  Further, it is unintuitive that things are
    1.64 +  written down in the opposite order as they actually ``happen''.
    1.65  *}
    1.66  
    1.67  (*<*)
    1.68 @@ -342,18 +346,15 @@
    1.69  (*>*)
    1.70  
    1.71  text {*
    1.72 -  At this stage, Isabelle offers some combinators which allow for more convenient
    1.73 -  notation, most notably reverse application:
    1.74 -  @{ML "
    1.75 -thy
    1.76 -|> Sign.add_consts_i [dummy_const]
    1.77 -|> Theory.add_defs_i false false [dummy_def]"}
    1.78 -*}
    1.79 -
    1.80 -text {*
    1.81 -  \noindent When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
    1.82 -  the @{ML fold} combinator lifts a single function @{text "f \<Colon> 'a -> 'b -> 'b"}:
    1.83 -  @{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.84 +  \noindent At this stage, Isabelle offers some combinators which allow
    1.85 +  for more convenient notation, most notably reverse application:
    1.86 +  \begin{quotation}
    1.87 +@{ML "thy
    1.88 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
    1.89 +|> (fn (t, thy) => thy
    1.90 +|> Thm.add_def false
    1.91 +     (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
    1.92 +  \end{quotation}
    1.93  *}
    1.94  
    1.95  text %mlref {*
    1.96 @@ -362,12 +363,78 @@
    1.97    @{index_ML "op |>> ": "('a * 'c) * ('a -> 'b) -> 'b * 'c"} \\
    1.98    @{index_ML "op ||> ": "('c * 'a) * ('a -> 'b) -> 'c * 'b"} \\
    1.99    @{index_ML "op ||>> ": "('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b"} \\
   1.100 +  \end{mldecls}
   1.101 +*}
   1.102 +
   1.103 +text {*
   1.104 +  \noindent Usually, functions involving theory updates also return
   1.105 +  side results; to use these conveniently, yet another
   1.106 +  set of combinators is at hand, most notably @{ML "op |->"}
   1.107 +  which allows curried access to side results:
   1.108 +  \begin{quotation}
   1.109 +@{ML "thy
   1.110 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
   1.111 +|-> (fn t => Thm.add_def false
   1.112 +      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
   1.113 +"}
   1.114 +  \end{quotation}
   1.115 +
   1.116 +  \noindent @{ML "op |>>"} allows for processing side results on their own:
   1.117 +  \begin{quotation}
   1.118 +@{ML "thy
   1.119 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
   1.120 +|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
   1.121 +|-> (fn def => Thm.add_def false (\"bar_def\", def))
   1.122 +"}
   1.123 +  \end{quotation}
   1.124 +
   1.125 +  \noindent Orthogonally, @{ML "op ||>"} applies a transformation
   1.126 +  in the presence of side results which are left unchanged:
   1.127 +  \begin{quotation}
   1.128 +@{ML "thy
   1.129 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
   1.130 +||> Sign.add_path \"foobar\"
   1.131 +|-> (fn t => Thm.add_def false
   1.132 +      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
   1.133 +||> Sign.restore_naming thy
   1.134 +"}
   1.135 +  \end{quotation}
   1.136 +
   1.137 +  \noindent @{index_ML "op ||>>"} accumulates side results:
   1.138 +  \begin{quotation}
   1.139 +@{ML "thy
   1.140 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
   1.141 +||>> Sign.declare_const [] (\"foobar\", @{typ \"foo => foo\"}, NoSyn)
   1.142 +|-> (fn (t1, t2) => Thm.add_def false
   1.143 +      (\"bar_def\", Logic.mk_equals (t1, t2)))
   1.144 +"}
   1.145 +  \end{quotation}
   1.146 +*}
   1.147 +
   1.148 +text %mlref {*
   1.149 +  \begin{mldecls}
   1.150 +  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   1.151    @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   1.152    \end{mldecls}
   1.153  *}
   1.154  
   1.155  text {*
   1.156 -  \noindent FIXME transformations involving side results
   1.157 +  \noindent This principles naturally lift to @{text lists} using
   1.158 +  the @{ML fold} and @{ML fold_map} combinators.
   1.159 +  The first lifts a single function
   1.160 +  @{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}
   1.161 +  such that
   1.162 +  @{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.163 +  the second accumulates side results in a list by lifting
   1.164 +  a single function
   1.165 +  @{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"}
   1.166 +  such that
   1.167 +  @{text "y |> fold_map 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.168 +    ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"};
   1.169 +
   1.170 +  Example: FIXME
   1.171 +  \begin{quotation}
   1.172 +  \end{quotation}
   1.173  *}
   1.174  
   1.175  text %mlref {*
   1.176 @@ -438,7 +505,7 @@
   1.177  
   1.178  text {*
   1.179    Lists are often used as set-like data structures -- set-like in
   1.180 -  then sense that they support notion of @{ML member}-ship,
   1.181 +  the sense that they support a notion of @{ML member}-ship,
   1.182    @{ML insert}-ing and @{ML remove}-ing, but are order-sensitive.
   1.183    This is convenient when implementing a history-like mechanism:
   1.184    @{ML insert} adds an element \emph{to the front} of a list,
     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Oct 22 21:32:12 2007 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Oct 23 10:53:15 2007 +0200
     2.3 @@ -339,8 +339,6 @@
     2.4  \begin{isamarkuptext}%
     2.5  \begin{mldecls}
     2.6    \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
     2.7 -  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
     2.8 -  \indexml{fold-rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
     2.9    \end{mldecls}%
    2.10  \end{isamarkuptext}%
    2.11  \isamarkuptrue%
    2.12 @@ -371,22 +369,30 @@
    2.13    particular value \isa{x\ {\isasymColon}\ foo} which is then transformed
    2.14    by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo},
    2.15    continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
    2.16 -  and so on.  As a canoncial example, take primitive functions enriching
    2.17 -  theories by constants and definitions:
    2.18 -  \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline%
    2.19 -\verb|-> theory|
    2.20 -  and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline%
    2.21 -\verb|-> (bstring * term) list -> theory -> theory|.
    2.22 -  Written with naive application, an addition of a constant with
    2.23 -  a corresponding definition would look like:
    2.24 -  \verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline%
    2.25 -\verb|  (Sign.add_consts_i [dummy_const] thy)|.
    2.26 -  With increasing numbers of applications, this code gets quite unreadable.
    2.27 -  Using composition, at least the nesting of brackets may be reduced:
    2.28 -  \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline%
    2.29 -\verb|  [dummy_const]) thy|.
    2.30 -  What remains unsatisfactory is that things are written down in the opposite order
    2.31 -  as they actually ``happen''.%
    2.32 +  and so on.  As a canoncial example, take functions enriching
    2.33 +  a theory by constant declararion and primitive definitions:
    2.34 +
    2.35 +  \begin{quotation}
    2.36 +    \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline%
    2.37 +\verb|       -> theory -> term * theory|
    2.38 +
    2.39 +    \verb|Thm.add_def: bool -> bstring * term -> theory -> thm * theory|
    2.40 +  \end{quotation}
    2.41 +
    2.42 +  Written with naive application, an addition of constant
    2.43 +  \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
    2.44 +  a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
    2.45 +
    2.46 +  \begin{quotation}
    2.47 +  \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline%
    2.48 +\verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
    2.49 +\verb|    (Sign.declare_const []|\isasep\isanewline%
    2.50 +\verb|      ("bar", @{typ "foo => foo"}, NoSyn) thy)|.
    2.51 +  \end{quotation}
    2.52 +
    2.53 +  With increasing numbers of applications, this code gets quite
    2.54 +  unreadable.  Further, it is unintuitive that things are
    2.55 +  written down in the opposite order as they actually ``happen''.%
    2.56  \end{isamarkuptext}%
    2.57  \isamarkuptrue%
    2.58  %
    2.59 @@ -404,19 +410,15 @@
    2.60  \endisadelimML
    2.61  %
    2.62  \begin{isamarkuptext}%
    2.63 -At this stage, Isabelle offers some combinators which allow for more convenient
    2.64 -  notation, most notably reverse application:
    2.65 -  \isasep\isanewline%
    2.66 +\noindent At this stage, Isabelle offers some combinators which allow
    2.67 +  for more convenient notation, most notably reverse application:
    2.68 +  \begin{quotation}
    2.69  \verb|thy|\isasep\isanewline%
    2.70 -\verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\isasep\isanewline%
    2.71 -\verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|%
    2.72 -\end{isamarkuptext}%
    2.73 -\isamarkuptrue%
    2.74 -%
    2.75 -\begin{isamarkuptext}%
    2.76 -\noindent 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.77 -  the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
    2.78 -  \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.79 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
    2.80 +\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
    2.81 +\verb||\verb,|,\verb|> Thm.add_def false|\isasep\isanewline%
    2.82 +\verb|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
    2.83 +  \end{quotation}%
    2.84  \end{isamarkuptext}%
    2.85  \isamarkuptrue%
    2.86  %
    2.87 @@ -432,6 +434,72 @@
    2.88    \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
    2.89    \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
    2.90    \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
    2.91 +  \end{mldecls}%
    2.92 +\end{isamarkuptext}%
    2.93 +\isamarkuptrue%
    2.94 +%
    2.95 +\endisatagmlref
    2.96 +{\isafoldmlref}%
    2.97 +%
    2.98 +\isadelimmlref
    2.99 +%
   2.100 +\endisadelimmlref
   2.101 +%
   2.102 +\begin{isamarkuptext}%
   2.103 +\noindent Usually, functions involving theory updates also return
   2.104 +  side results; to use these conveniently, yet another
   2.105 +  set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
   2.106 +  which allows curried access to side results:
   2.107 +  \begin{quotation}
   2.108 +\verb|thy|\isasep\isanewline%
   2.109 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
   2.110 +\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
   2.111 +\verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
   2.112 +
   2.113 +  \end{quotation}
   2.114 +
   2.115 +  \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
   2.116 +  \begin{quotation}
   2.117 +\verb|thy|\isasep\isanewline%
   2.118 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
   2.119 +\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
   2.120 +\verb||\verb,|,\verb|-> (fn def => Thm.add_def false ("bar_def", def))|\isasep\isanewline%
   2.121 +
   2.122 +  \end{quotation}
   2.123 +
   2.124 +  \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
   2.125 +  in the presence of side results which are left unchanged:
   2.126 +  \begin{quotation}
   2.127 +\verb|thy|\isasep\isanewline%
   2.128 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
   2.129 +\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
   2.130 +\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
   2.131 +\verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
   2.132 +\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
   2.133 +
   2.134 +  \end{quotation}
   2.135 +
   2.136 +  \noindent \indexml{op ||$>$$>$}\verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
   2.137 +  \begin{quotation}
   2.138 +\verb|thy|\isasep\isanewline%
   2.139 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
   2.140 +\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
   2.141 +\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false|\isasep\isanewline%
   2.142 +\verb|      ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
   2.143 +
   2.144 +  \end{quotation}%
   2.145 +\end{isamarkuptext}%
   2.146 +\isamarkuptrue%
   2.147 +%
   2.148 +\isadelimmlref
   2.149 +%
   2.150 +\endisadelimmlref
   2.151 +%
   2.152 +\isatagmlref
   2.153 +%
   2.154 +\begin{isamarkuptext}%
   2.155 +\begin{mldecls}
   2.156 +  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
   2.157    \indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
   2.158    \end{mldecls}%
   2.159  \end{isamarkuptext}%
   2.160 @@ -445,7 +513,21 @@
   2.161  \endisadelimmlref
   2.162  %
   2.163  \begin{isamarkuptext}%
   2.164 -\noindent FIXME transformations involving side results%
   2.165 +\noindent This principles naturally lift to \isa{lists} using
   2.166 +  the \verb|fold| and \verb|fold_map| combinators.
   2.167 +  The first lifts a single function
   2.168 +  \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}
   2.169 +  such that
   2.170 +  \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.171 +  the second accumulates side results in a list by lifting
   2.172 +  a single function
   2.173 +  \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b}
   2.174 +  such that
   2.175 +  \isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ 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}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}};
   2.176 +
   2.177 +  Example: FIXME
   2.178 +  \begin{quotation}
   2.179 +  \end{quotation}%
   2.180  \end{isamarkuptext}%
   2.181  \isamarkuptrue%
   2.182  %
   2.183 @@ -568,7 +650,7 @@
   2.184  %
   2.185  \begin{isamarkuptext}%
   2.186  Lists are often used as set-like data structures -- set-like in
   2.187 -  then sense that they support notion of \verb|member|-ship,
   2.188 +  the sense that they support a notion of \verb|member|-ship,
   2.189    \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
   2.190    This is convenient when implementing a history-like mechanism:
   2.191    \verb|insert| adds an element \emph{to the front} of a list,
     3.1 --- a/doc-src/IsarImplementation/Thy/document/isabelle.sty	Mon Oct 22 21:32:12 2007 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty	Tue Oct 23 10:53:15 2007 +0200
     3.3 @@ -25,10 +25,10 @@
     3.4  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
     3.5  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     3.6  \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
     3.7 -\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
     3.8 -\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
     3.9 -\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
    3.10 -\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
    3.11 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
    3.12 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    3.13 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
    3.14 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
    3.15  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    3.16  \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
    3.17  \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}