diff -r 3d3d6038bdaa -r a16b18fd6299 doc-src/IsarImplementation/Thy/ML_old.thy
--- a/doc-src/IsarImplementation/Thy/ML_old.thy	Fri Oct 22 20:43:48 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,321 +0,0 @@
-theory ML_old
-imports Base
-begin
-
-chapter {* Advanced ML programming *}
-
-section {* Style *}
-
-text {*
-  Like any style guide, also this one should not be interpreted dogmatically, but
-  with care and discernment.  It consists of a collection of
-  recommendations which have been turned out useful over long years of
-  Isabelle system development and are supposed to support writing of readable
-  and managable code.  Special cases encourage derivations,
-  as far as you know what you are doing.
-  \footnote{This style guide is loosely based on
-  \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}}
-
-  \begin{description}
-
-    \item[fundamental law of programming]
-      Whenever writing code, keep in mind: A program is
-      written once, modified ten times, and read
-      hundred times.  So simplify its writing,
-      always keep future modifications in mind,
-      and never jeopardize readability.  Every second you hesitate
-      to spend on making your code more clear you will
-      have to spend ten times understanding what you have
-      written later on.
-
-    \item[white space matters]
-      Treat white space in your code as if it determines
-      the meaning of code.
-
-      \begin{itemize}
-
-        \item The space bar is the easiest key to find on the keyboard,
-          press it as often as necessary. @{verbatim "2 + 2"} is better
-          than @{verbatim "2+2"}, likewise @{verbatim "f (x, y)"} is
-          better than @{verbatim "f(x,y)"}.
-
-        \item Restrict your lines to 80 characters.  This will allow
-          you to keep the beginning of a line in view while watching
-          its end.\footnote{To acknowledge the lax practice of
-          text editing these days, we tolerate as much as 100
-          characters per line, but anything beyond 120 is not
-          considered proper source text.}
-
-        \item Ban tabulators; they are a context-sensitive formatting
-          feature and likely to confuse anyone not using your favorite
-          editor.\footnote{Some modern programming language even
-          forbid tabulators altogether according to the formal syntax
-          definition.}
-
-        \item Get rid of trailing whitespace.  Instead, do not
-          suppress a trailing newline at the end of your files.
-
-        \item Choose a generally accepted style of indentation,
-          then use it systematically throughout the whole
-          application.  An indentation of two spaces is appropriate.
-          Avoid dangling indentation.
-
-      \end{itemize}
-
-    \item[cut-and-paste succeeds over copy-and-paste]
-       \emph{Never} copy-and-paste code when programming.  If you
-        need the same piece of code twice, introduce a
-        reasonable auxiliary function (if there is no
-        such function, very likely you got something wrong).
-        Any copy-and-paste will turn out to be painful 
-        when something has to be changed later on.
-
-    \item[comments]
-      are a device which requires careful thinking before using
-      it.  The best comment for your code should be the code itself.
-      Prefer efforts to write clear, understandable code
-      over efforts to explain nasty code.
-
-    \item[functional programming is based on functions]
-      Model things as abstract as appropriate.  Avoid unnecessarrily
-      concrete datatype  representations.  For example, consider a function
-      taking some table data structure as argument and performing
-      lookups on it.  Instead of taking a table, it could likewise
-      take just a lookup function.  Accustom
-      your way of coding to the level of expressiveness a functional
-      programming language is giving onto you.
-
-    \item[tuples]
-      are often in the way.  When there is no striking argument
-      to tuple function arguments, just write your function curried.
-
-    \item[telling names]
-      Any name should tell its purpose as exactly as possible, while
-      keeping its length to the absolutely necessary minimum.  Always
-      give the same name to function arguments which have the same
-      meaning. Separate words by underscores (@{verbatim
-      int_of_string}, not @{verbatim intOfString}).\footnote{Some
-      recent tools for Emacs include special precautions to cope with
-      bumpy names in @{text "camelCase"}, e.g.\ for improved on-screen
-      readability.  It is easier to abstain from using such names in the
-      first place.}
-
-  \end{description}
-*}
-
-
-chapter {* Basic library functions *}
-
-text {*
-  Beyond the proposal of the SML/NJ basis library, Isabelle comes
-  with its own library, from which selected parts are given here.
-  These should encourage a study of the Isabelle sources,
-  in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.
-*}
-
-section {* Linear transformations \label{sec:ML-linear-trans} *}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
-  \end{mldecls}
-*}
-
-(*<*)
-typedecl foo
-consts foo :: foo
-ML {*
-val thy = Theory.copy @{theory}
-*}
-(*>*)
-
-text {*
-  \noindent Many problems in functional programming can be thought of
-  as linear transformations, i.e.~a caluclation starts with a
-  particular value @{ML_text "x : foo"} which is then transformed
-  by application of a function @{ML_text "f : foo -> foo"},
-  continued by an application of a function @{ML_text "g : foo -> bar"},
-  and so on.  As a canoncial example, take functions enriching
-  a theory by constant declararion and primitive definitions:
-
-  \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: (binding * typ) * mixfix
-  -> theory -> term * theory"} \\
-  @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory"}
-  \end{mldecls}
-
-  \noindent Written with naive application, an addition of constant
-  @{term bar} with type @{typ "foo \<Rightarrow> foo"} and
-  a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
-
-  \smallskip\begin{mldecls}
-  @{ML "(fn (t, thy) => Thm.add_def false false
-  (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
-    (Sign.declare_const
-      ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
-  \end{mldecls}
-
-  \noindent With increasing numbers of applications, this code gets quite
-  unreadable.  Further, it is unintuitive that things are
-  written down in the opposite order as they actually ``happen''.
-*}
-
-text {*
-  \noindent At this stage, Isabelle offers some combinators which allow
-  for more convenient notation, most notably reverse application:
-
-  \smallskip\begin{mldecls}
-@{ML "thy
-|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-|> (fn (t, thy) => thy
-|> Thm.add_def false false
-     (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
-  \end{mldecls}
-*}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML "op |-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
-  @{index_ML "op |>> ": "('a * 'c) * ('a -> 'b) -> 'b * 'c"} \\
-  @{index_ML "op ||> ": "('c * 'a) * ('a -> 'b) -> 'c * 'b"} \\
-  @{index_ML "op ||>> ": "('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b"} \\
-  \end{mldecls}
-*}
-
-text {*
-  \noindent Usually, functions involving theory updates also return
-  side results; to use these conveniently, yet another
-  set of combinators is at hand, most notably @{ML "op |->"}
-  which allows curried access to side results:
-
-  \smallskip\begin{mldecls}
-@{ML "thy
-|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-|-> (fn t => Thm.add_def false false
-      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
-"}
-  \end{mldecls}
-
-  \noindent @{ML "op |>>"} allows for processing side results on their own:
-
-  \smallskip\begin{mldecls}
-@{ML "thy
-|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
-|-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
-"}
-  \end{mldecls}
-
-  \noindent Orthogonally, @{ML "op ||>"} applies a transformation
-  in the presence of side results which are left unchanged:
-
-  \smallskip\begin{mldecls}
-@{ML "thy
-|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||> Sign.add_path \"foobar\"
-|-> (fn t => Thm.add_def false false
-      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
-||> Sign.restore_naming thy
-"}
-  \end{mldecls}
-
-  \noindent @{ML "op ||>>"} accumulates side results:
-
-  \smallskip\begin{mldecls}
-@{ML "thy
-|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> Sign.declare_const ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
-|-> (fn (t1, t2) => Thm.add_def false false
-      (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
-"}
-  \end{mldecls}
-*}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
-  @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
-  \end{mldecls}
-*}
-
-text {*
-  \noindent This principles naturally lift to \emph{lists} using
-  the @{ML fold} and @{ML fold_map} combinators.
-  The first lifts a single function
-  \begin{quote}\footnotesize
-    @{ML_text "f : 'a -> 'b -> 'b"} to @{ML_text "'a list -> 'b -> 'b"}
-  \end{quote}
-  such that
-  \begin{quote}\footnotesize
-    @{ML_text "y |> fold f [x1, x2, ..., x_n]"} \\
-    \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 |> f x2 |> ... |> f x_n"}
-  \end{quote}
-  \noindent The second accumulates side results in a list by lifting
-  a single function
-  \begin{quote}\footnotesize
-    @{ML_text "f : 'a -> 'b -> 'c * 'b"} to @{ML_text "'a list -> 'b -> 'c list * 'b"}
-  \end{quote}
-  such that
-  \begin{quote}\footnotesize
-    @{ML_text "y |> fold_map f [x1, x2, ..., x_n]"} \\
-    \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 ||>> f x2 ||>> ... ||>> f x_n"} \\
-    \hspace*{6ex}@{ML_text "||> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])"}
-  \end{quote}
-  
-  \noindent Example:
-
-  \smallskip\begin{mldecls}
-@{ML "let
-  val consts = [\"foo\", \"bar\"];
-in
-  thy
-  |> fold_map (fn const => Sign.declare_const
-       ((Binding.name 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 false (Binding.empty, def)) defs)
-end"}
-  \end{mldecls}
-*}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML "op #> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
-  @{index_ML "op #-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
-  @{index_ML "op #>> ": "('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b"} \\
-  @{index_ML "op ##> ": "('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd"} \\
-  @{index_ML "op ##>> ": "('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd"} \\
-  \end{mldecls}
-*}
-
-text {*
-  \noindent All those linear combinators also exist in higher-order
-  variants which do not expect a value on the left hand side
-  but a function.
-*}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML "op ` ": "('b -> 'a) -> 'b -> 'a * 'b"} \\
-  @{index_ML tap: "('b -> 'a) -> 'b -> 'b"} \\
-  \end{mldecls}
-*}
-
-text {*
-  \noindent These operators allow to ``query'' a context
-  in a series of context transformations:
-
-  \smallskip\begin{mldecls}
-@{ML "thy
-|> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> `(fn thy => Sign.declared_const thy
-         (Sign.full_name thy (Binding.name \"foobar\")))
-|-> (fn (t, b) => if b then I
-       else Sign.declare_const
-         ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
-"}
-  \end{mldecls}
-*}
-
-end
\ No newline at end of file