
diff -r d868e4f7905b -r fd773574cb81 doc-src/Ref/syntax.tex
--- a/doc-src/Ref/syntax.tex	Tue Jun 19 20:43:09 2012 +0200
+++ b/doc-src/Ref/syntax.tex	Tue Jun 19 20:51:15 2012 +0200
@@ -239,86 +239,12 @@
 \section{Macros: syntactic rewriting} \label{sec:macros}
 \index{macros|(}\index{rewriting!syntactic|(}
 
-Figure~\ref{fig:set_trans} defines a fragment of first-order logic and
-set theory.\footnote{This and the following theories are complete
-  working examples, though they specify only syntax, no axioms.  The
-  file {\tt ZF/ZF.thy} presents a full set theory definition,
-  including many macro rules.} Theory {\tt SetSyntax} declares
-constants for set comprehension ({\tt Collect}), replacement ({\tt
-  Replace}) and bounded universal quantification ({\tt Ball}).  Each
-of these binds some variables.  Without additional syntax we should
-have to write $\forall x \in A.  P$ as {\tt Ball(A,\%x.P)}, and
-similarly for the others.
-
-\begin{figure}
-\begin{ttbox}
-SetSyntax = Pure +
-types
-  i o
-arities
-  i, o :: logic
-consts
-  Trueprop      :: o => prop                ("_" 5)
-  Collect       :: [i, i => o] => i
-  Replace       :: [i, [i, i] => o] => i
-  Ball          :: [i, i => o] => o
-syntax
-  "{\at}Collect"    :: [idt, i, o] => i         ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
-  "{\at}Replace"    :: [idt, idt, i, o] => i    ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
-  "{\at}Ball"       :: [idt, i, o] => o         ("(3ALL _:_./ _)" 10)
-translations
-  "{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, \%x. P)"
-  "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
-  "ALL x:A. P"  == "Ball(A, \%x. P)"
-end
-\end{ttbox}
-\caption{Macro example: set theory}\label{fig:set_trans}
-\end{figure}
-
-The theory specifies a variable-binding syntax through additional productions
-that have mixfix declarations.  Each non-copy production must specify some
-constant, which is used for building \AST{}s. \index{constants!syntactic} The
-additional constants are decorated with {\tt\at} to stress their purely
-syntactic purpose; they may not occur within the final well-typed terms,
-being declared as {\tt syntax} rather than {\tt consts}.
-
-The translations cause the replacement of external forms by internal forms
-after parsing, and vice versa before printing of terms.  As a specification
-of the set theory notation, they should be largely self-explanatory.  The
-syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},
-appear implicitly in the macro rules via their mixfix forms.
-
-Macros can define variable-binding syntax because they operate on \AST{}s,
-which have no inbuilt notion of bound variable.  The macro variables {\tt
-  x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers,
-in this case bound variables.  The macro variables {\tt P} and~{\tt Q}
-range over formulae containing bound variable occurrences.
-
-Other applications of the macro system can be less straightforward, and
-there are peculiarities.  The rest of this section will describe in detail
-how Isabelle macros are preprocessed and applied.
-
-
 \subsection{Specifying macros}
 
-For theory~{\tt SetSyntax} of Fig.~\ref{fig:set_trans} these are
-\begin{ttbox}
-parse_rules:
-  ("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))
-  ("{\at}Replace" y x A Q)  ->  ("Replace" A ("_abs" x ("_abs" y Q)))
-  ("{\at}Ball" x A P)  ->  ("Ball" A ("_abs" x P))
-print_rules:
-  ("Collect" A ("_abs" x P))  ->  ("{\at}Collect" x A P)
-  ("Replace" A ("_abs" x ("_abs" y Q)))  ->  ("{\at}Replace" y x A Q)
-  ("Ball" A ("_abs" x P))  ->  ("{\at}Ball" x A P)
-\end{ttbox}
-
 \begin{warn}
-  Avoid choosing variable names that have previously been used as
-  constants, types or type classes; the {\tt consts} section in the output
-  of {\tt print_syntax} lists all such names.  If a macro rule works
-  incorrectly, inspect its internal form as shown above, recalling that
-  constants appear as quoted strings and variables without quotes.
+If a macro rule works incorrectly, inspect its internal form as
+shown above, recalling that constants appear as quoted strings and
+variables without quotes.
 \end{warn}
 
 \begin{warn}
@@ -392,22 +318,6 @@
 contain a messy mixture of {\tt Variable}s and {\tt Constant}s.  This is
 insignificant at macro level because matching treats them alike.
 
-Because of this behaviour, different kinds of atoms with the same name are
-indistinguishable, which may make some rules prone to misbehaviour.  Example:
-\begin{ttbox}
-types
-  Nil
-consts
-  Nil     :: 'a list
-syntax
-  "[]"    :: 'a list    ("[]")
-translations
-  "[]"    == "Nil"
-\end{ttbox}
-The term {\tt Nil} will be printed as {\tt []}, just as expected.
-The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
-expected!  Guess how type~{\tt Nil} is printed?
-
 Normalizing an \AST{} involves repeatedly applying macro rules until none are
 applicable.  Macro rules are chosen in order of appearance in the theory
 definitions.  You can watch the normalization of \AST{}s during parsing and
@@ -416,125 +326,6 @@
 normalization ({\tt pre}), redexes with results ({\tt rewrote}), the normal
 form finally reached ({\tt post}) and some statistics ({\tt normalize}).
 
-\subsection{Example: the syntax of finite sets}
-\index{examples!of macros}
-
-This example demonstrates the use of recursive macros to implement a
-convenient notation for finite sets.
-\begin{ttbox}
-FinSyntax = SetSyntax +
-types
-  is
-syntax
-  ""            :: i => is                  ("_")
-  "{\at}Enum"       :: [i, is] => is            ("_,/ _")
-consts
-  empty         :: i                        ("{\ttlbrace}{\ttrbrace}")
-  insert        :: [i, i] => i
-syntax
-  "{\at}Finset"     :: is => i                  ("{\ttlbrace}(_){\ttrbrace}")
-translations
-  "{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
-  "{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
-end
-\end{ttbox}
-Finite sets are internally built up by {\tt empty} and {\tt insert}.  The
-declarations above specify \verb|{x, y, z}| as the external representation
-of
-\begin{ttbox}
-insert(x, insert(y, insert(z, empty)))
-\end{ttbox}
-The nonterminal symbol~\ndx{is} stands for one or more objects of type~{\tt
-  i} separated by commas.  The mixfix declaration \hbox{\verb|"_,/ _"|}
-allows a line break after the comma for \rmindex{pretty printing}; if no
-line break is required then a space is printed instead.
-
-The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
-declaration.  Hence {\tt is} is not a logical type and may be used safely as
-a new nonterminal for custom syntax.  The nonterminal~{\tt is} can later be
-re-used for other enumerations of type~{\tt i} like lists or tuples.  If we
-had needed polymorphic enumerations, we could have used the predefined
-nonterminal symbol \ndx{args} and skipped this part altogether.
-
-Next follows {\tt empty}, which is already equipped with its syntax
-\verb|{}|, and {\tt insert} without concrete syntax.  The syntactic
-constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
-  i} enclosed in curly braces.  Remember that a pair of parentheses, as in
-\verb|"{(_)}"|, specifies a block of indentation for pretty printing.
-
-The translations may look strange at first.  Macro rules are best
-understood in their internal forms:
-\begin{ttbox}
-parse_rules:
-  ("{\at}Finset" ("{\at}Enum" x xs))  ->  ("insert" x ("{\at}Finset" xs))
-  ("{\at}Finset" x)  ->  ("insert" x "empty")
-print_rules:
-  ("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
-  ("insert" x "empty")  ->  ("{\at}Finset" x)
-\end{ttbox}
-This shows that \verb|{x,xs}| indeed matches any set enumeration of at least
-two elements, binding the first to {\tt x} and the rest to {\tt xs}.
-Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.
-The parse rules only work in the order given.
-
-\begin{warn}
-  The \AST{} rewriter cannot distinguish constants from variables and looks
-  only for names of atoms.  Thus the names of {\tt Constant}s occurring in
-  the (internal) left-hand side of translation rules should be regarded as
-  \rmindex{reserved words}.  Choose non-identifiers like {\tt\at Finset} or
-  sufficiently long and strange names.  If a bound variable's name gets
-  rewritten, the result will be incorrect; for example, the term
-\begin{ttbox}
-\%empty insert. insert(x, empty)
-\end{ttbox}
-\par\noindent is incorrectly printed as \verb|%empty insert. {x}|.
-\end{warn}
-
-
-\subsection{Example: a parse macro for dependent types}\label{prod_trans}
-\index{examples!of macros}
-
-As stated earlier, a macro rule may not introduce new {\tt Variable}s on
-the right-hand side.  Something like \verb|"K(B)" => "%x.B"| is illegal;
-if allowed, it could cause variable capture.  In such cases you usually
-must fall back on translation functions.  But a trick can make things
-readable in some cases: {\em calling\/} translation functions by parse
-macros:
-\begin{ttbox}
-ProdSyntax = SetSyntax +
-consts
-  Pi            :: [i, i => i] => i
-syntax
-  "{\at}PROD"       :: [idt, i, i] => i       ("(3PROD _:_./ _)" 10)
-  "{\at}->"         :: [i, i] => i            ("(_ ->/ _)" [51, 50] 50)
-\ttbreak
-translations
-  "PROD x:A. B" => "Pi(A, \%x. B)"
-  "A -> B"      => "Pi(A, _K(B))"
-end
-ML
-  val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
-\end{ttbox}
-
-Here {\tt Pi} is a logical constant for constructing general products.
-Two external forms exist: the general case {\tt PROD x:A.B} and the
-function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B}
-does not depend on~{\tt x}.
-
-The second parse macro introduces {\tt _K(B)}, which later becomes
-\verb|%x.B| due to a parse translation associated with \cdx{_K}.
-Unfortunately there is no such trick for printing, so we have to add a {\tt
-ML} section for the print translation \ttindex{dependent_tr'}.
-
-Recall that identifiers with a leading {\tt _} are allowed in translation
-rules, but not in ordinary terms.  Thus we can create \AST{}s containing
-names that are not directly expressible.
-
-The parse translation for {\tt _K} is already installed in Pure, and the
-function {\tt dependent_tr'} is exported by the syntax module for public use.
-See \S\ref{sec:tr_funs} below for more of the arcane lore of translation
-functions.  \index{macros|)}\index{rewriting!syntactic|)}
-
 
 \section{Translation functions} \label{sec:tr_funs}
 \index{translations|(}
@@ -630,79 +421,6 @@
 all logical constants and type constructors may invoke print translations.
 These, and macros, may introduce further constants.
 
-
-\subsection{Example: a print translation for dependent types}
-\index{examples!of translations}\indexbold{*dependent_tr'}
-
-Let us continue the dependent type example (page~\pageref{prod_trans}) by
-examining the parse translation for~\cdx{_K} and the print translation
-{\tt dependent_tr'}, which are both built-in.  By convention, parse
-translations have names ending with {\tt _tr} and print translations have
-names ending with {\tt _tr'}.  Search for such names in the Isabelle
-sources to locate more examples.
-
-Here is the parse translation for {\tt _K}:
-\begin{ttbox}
-fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t)
-  | k_tr ts = raise TERM ("k_tr", ts);
-\end{ttbox}
-If {\tt k_tr} is called with exactly one argument~$t$, it creates a new
-{\tt Abs} node with a body derived from $t$.  Since terms given to parse
-translations are not yet typed, the type of the bound variable in the new
-{\tt Abs} is simply {\tt dummyT}.  The function increments all {\tt Bound}
-nodes referring to outer abstractions by calling \ttindex{incr_boundvars},
-a basic term manipulation function defined in {\tt Pure/term.ML}.
-
-Here is the print translation for dependent types:
-\begin{ttbox}
-fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
-      if 0 mem (loose_bnos B) then
-        let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
-          list_comb
-            (Const (q,dummyT) $
-             Syntax.mark_boundT (x',{\thinspace}T) $ A $ B', ts)
-        end
-      else list_comb (Const (r, dummyT) $ A $ B, ts)
-  | dependent_tr' _ _ = raise Match;
-\end{ttbox}
-The argument {\tt (q,{\thinspace}r)} is supplied to the curried function {\tt
-  dependent_tr'} by a partial application during its installation.
-For example, we could set up print translations for both {\tt Pi} and
-{\tt Sigma} by including
-\begin{ttbox}\index{*ML section}
-val print_translation =
-  [("Pi",    dependent_tr' ("{\at}PROD", "{\at}->")),
-   ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))];
-\end{ttbox}
-within the {\tt ML} section.  The first of these transforms ${\tt
-  Pi}(A, \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
-$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not
-depend on~$x$.  It checks this using \ttindex{loose_bnos}, yet another
-function from {\tt Pure/term.ML}.  Note that $x'$ is a version of $x$
-renamed away from all names in $B$, and $B'$ is the body $B$ with {\tt
-  Bound} nodes referring to the {\tt Abs} node replaced by
-$\ttfct{Free} (x', \mtt{dummyT})$ (but marked as representing a bound
-variable).
-
-We must be careful with types here.  While types of {\tt Const}s are
-ignored, type constraints may be printed for some {\tt Free}s and
-{\tt Var}s if \ttindex{show_types} is set to {\tt true}.  Variables of type
-\ttindex{dummyT} are never printed with constraint, though.  The line
-\begin{ttbox}
-        let val (x', B') = Syntax.variant_abs' (x, dummyT, B);
-\end{ttbox}\index{*Syntax.variant_abs'}
-replaces bound variable occurrences in~$B$ by the free variable $x'$ with
-type {\tt dummyT}.  Only the binding occurrence of~$x'$ is given the
-correct type~{\tt T}, so this is the only place where a type
-constraint might appear.
-
-Also note that we are responsible to mark free identifiers that
-actually represent bound variables.  This is achieved by
-\ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above.
-Failing to do so may cause these names to be printed in the wrong
-style.  \index{translations|)} \index{syntax!transformations|)}
-
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "ref"




