--- a/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 25 10:24:32 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 25 13:51:58 2007 +0200
@@ -328,10 +328,10 @@
a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
\begin{quotation}
- @{ML "(fn (t, thy) => Thm.add_def false
+ @{ML "(fn (t, thy) => Thm.add_def false
(\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
(Sign.declare_const []
- (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}.
+ (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}
\end{quotation}
With increasing numbers of applications, this code gets quite
@@ -339,12 +339,6 @@
written down in the opposite order as they actually ``happen''.
*}
-(*<*)
-ML {*
-val thy = Theory.copy @{theory}
-*}
-(*>*)
-
text {*
\noindent At this stage, Isabelle offers some combinators which allow
for more convenient notation, most notably reverse application:
@@ -422,18 +416,37 @@
\noindent This principles naturally lift to @{text lists} using
the @{ML fold} and @{ML fold_map} combinators.
The first lifts a single function
- @{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}
+ \[
+ \mbox{@{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}}
+ \]
such that
- @{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"};
- the second accumulates side results in a list by lifting
+ \[
+ \mbox{@{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"}}
+ \]
+ The second accumulates side results in a list by lifting
a single function
- @{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"}
+ \[
+ \mbox{@{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"}}
+ \]
such that
- @{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
- ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"};
-
- Example: FIXME
+ \[
+ \mbox{@{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv>"}} \\
+ ~~\mbox{@{text "y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \<dots> ||>> f x\<^isub>n ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"}}
+ \]
+
+ Example:
\begin{quotation}
+@{ML "let
+ val consts = [\"foo\", \"bar\"];
+in
+ thy
+ |> fold_map (fn const => Sign.declare_const []
+ (const, @{typ \"foo => foo\"}, NoSyn)) consts
+ |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
+ |-> (fn defs => fold_map (fn def =>
+ Thm.add_def false (\"\", def)) defs)
+end
+"}
\end{quotation}
*}
@@ -461,7 +474,20 @@
*}
text {*
- \noindent FIXME
+ \noindent These operators allow to ``query'' a context
+ in a series of context transformations:
+
+ \begin{quotation}
+@{ML "thy
+|> tap (fn _ => writeln \"now adding constant\")
+|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
+||>> `(fn thy => Sign.declared_const thy
+ (Sign.full_name thy \"foobar\"))
+|-> (fn (t, b) => if b then I
+ else Sign.declare_const []
+ (\"foobar\", @{typ \"foo => foo\"}, NoSyn) #> snd)
+"}
+ \end{quotation}
*}
section {* Options and partiality *}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 25 10:24:32 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 25 13:51:58 2007 +0200
@@ -384,10 +384,10 @@
a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
\begin{quotation}
- \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline%
+ \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline%
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
\verb| (Sign.declare_const []|\isasep\isanewline%
-\verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)|.
+\verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)|
\end{quotation}
With increasing numbers of applications, this code gets quite
@@ -396,19 +396,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
\begin{isamarkuptext}%
\noindent At this stage, Isabelle offers some combinators which allow
for more convenient notation, most notably reverse application:
@@ -516,17 +503,37 @@
\noindent This principles naturally lift to \isa{lists} using
the \verb|fold| and \verb|fold_map| combinators.
The first lifts a single function
- \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}
+ \[
+ \mbox{\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}}
+ \]
such that
- \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};
- the second accumulates side results in a list by lifting
+ \[
+ \mbox{\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}}
+ \]
+ The second accumulates side results in a list by lifting
a single function
- \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}
+ \[
+ \mbox{\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}}
+ \]
such that
- \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}};
+ \[
+ \mbox{\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}}} \\
+ ~~\mbox{\isa{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}}}
+ \]
+
+ Example:
+ \begin{quotation}
+\verb|let|\isasep\isanewline%
+\verb| val consts = ["foo", "bar"];|\isasep\isanewline%
+\verb|in|\isasep\isanewline%
+\verb| thy|\isasep\isanewline%
+\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
+\verb| (const, @{typ "foo => foo"}, NoSyn)) consts|\isasep\isanewline%
+\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
+\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
+\verb| Thm.add_def false ("", def)) defs)|\isasep\isanewline%
+\verb|end|\isasep\isanewline%
- Example: FIXME
- \begin{quotation}
\end{quotation}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -584,7 +591,20 @@
\endisadelimmlref
%
\begin{isamarkuptext}%
-\noindent FIXME%
+\noindent These operators allow to ``query'' a context
+ in a series of context transformations:
+
+ \begin{quotation}
+\verb|thy|\isasep\isanewline%
+\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
+\verb| (Sign.full_name thy "foobar"))|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
+\verb| else Sign.declare_const []|\isasep\isanewline%
+\verb| ("foobar", @{typ "foo => foo"}, NoSyn) #> snd)|\isasep\isanewline%
+
+ \end{quotation}%
\end{isamarkuptext}%
\isamarkuptrue%
%