various minor changes;
authorwenzelm
Mon Nov 22 11:27:04 1993 +0100 (1993-11-22)
changeset 135493308514ea8
parent 134 595fda4879b6
child 136 a9015b16a0e5
various minor changes;
doc-src/Logics/defining.tex
     1.1 --- a/doc-src/Logics/defining.tex	Mon Nov 22 09:20:28 1993 +0100
     1.2 +++ b/doc-src/Logics/defining.tex	Mon Nov 22 11:27:04 1993 +0100
     1.3 @@ -144,12 +144,14 @@
     1.4  $aprop$ &=& $id$ ~~$|$~~ $var$
     1.5      ~~$|$~~ $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
     1.6  $fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
     1.7 +    &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
     1.8 +    &$|$& $fun@{max_pri}$ {\tt::} $type$ \\
     1.9      &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\
    1.10  $idts$ &=& $idt$ ~~$|$~~ $idt@1$ $idts$ \\\\
    1.11  $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
    1.12      &$|$& $id$ \ttindex{::} $type$ & (0) \\\\
    1.13 -$type$ &=& $tfree$ ~~$|$~~ $tvar$ \\
    1.14 -     &$|$& $tfree$ {\tt::} $sort$ ~~$|$~~ $tvar$ {\tt::} $sort$ \\
    1.15 +$type$ &=& $tfree$ ~~$|$~~ $tvar$ ~~$|$~~ $tfree$ {\tt::} $sort$
    1.16 +  ~~$|$~~ $tvar$ {\tt::} $sort$ \\
    1.17       &$|$& $id$ ~~$|$~~ $type@{max_pri}$ $id$
    1.18                  ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
    1.19       &$|$& $type@1$ \ttindex{=>} $type$ & (0) \\
    1.20 @@ -180,7 +182,7 @@
    1.21  
    1.22    \item[$type$] Meta-types.
    1.23  
    1.24 -  \item[$idts$] a list of identifiers, possibly constrained by types. Note
    1.25 +  \item[$idts$] A list of identifiers, possibly constrained by types. Note
    1.26      that \verb|x :: nat y| is parsed as \verb|x :: (nat y)|, i.e.\ {\tt y}
    1.27      would be treated like a type constructor applied to {\tt nat}.
    1.28  \end{description}
    1.29 @@ -192,8 +194,8 @@
    1.30  minimal vocabulary: identifiers, variables, parentheses, and the lambda
    1.31  calculus. Logical types, i.e.\ those of class $logic$, are automatically
    1.32  equipped with this basic syntax. More precisely, for any type constructor
    1.33 -$ty$ with arity $(\dots)c$, where $c$ is a subclass of $logic$, the following
    1.34 -productions are added:
    1.35 +$ty$ with arity $(\vec{s})c$, where $c$ is a subclass of $logic$, the
    1.36 +following productions are added:
    1.37  \begin{center}
    1.38  \begin{tabular}{rclc}
    1.39  $ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
    1.40 @@ -284,8 +286,7 @@
    1.41  syntax, therefore being quite verbose. Its output is divided into labeled
    1.42  sections. The syntax proper is represented by {\tt lexicon}, {\tt roots} and
    1.43  {\tt prods}. The rest refers to the manifold facilities to apply syntactic
    1.44 -translations (macro expansion etc.). See \S\ref{sec:macros} and
    1.45 -\S\ref{sec:tr_funs} for more details on translations.
    1.46 +translations (macro expansion etc.).
    1.47  
    1.48  To simplify coping with the verbosity of {\tt Syntax.print_syntax}, there are
    1.49  \ttindex{Syntax.print_gram} to print the syntax proper only and
    1.50 @@ -333,14 +334,14 @@
    1.51  
    1.52        \item $root_of_type(\alpha) = \mtt{logic}$.
    1.53      \end{itemize}
    1.54 -    Thereby $\tau@1, \dots, \tau@n$ are types, $ty$ a type infix or ordinary
    1.55 -    type constructor and $\alpha$ a type variable or unknown. Note that only
    1.56 -    the outermost type constructor is taken into account.
    1.57 +    Thereby $\tau@1, \dots, \tau@n$ are types, $ty$ an infix or ordinary type
    1.58 +    constructor and $\alpha$ a type variable or unknown. Note that only the
    1.59 +    outermost type constructor is taken into account.
    1.60  
    1.61    \item[\ttindex{prods}]
    1.62      The list of productions describing the precedence grammar. Nonterminals
    1.63 -    $A@n$ are rendered in ASCII as {\tt $A$[$n$]}, literal tokens are quoted.
    1.64 -    Note that some productions have strings attached after an {\tt =>}. These
    1.65 +    $A@n$ are rendered in {\sc ascii} as {\tt $A$[$n$]}, literal tokens are
    1.66 +    quoted. Some productions have strings attached after an {\tt =>}. These
    1.67      strings later become the heads of parse trees, but they also play a vital
    1.68      role when terms are printed (see \S\ref{sec:asts}).
    1.69  
    1.70 @@ -439,7 +440,7 @@
    1.71  
    1.72  Note that {\tt ()} and {\tt (f)} are both illegal.
    1.73  
    1.74 -The resemblance of LISP's S-expressions is intentional, but notice the two
    1.75 +The resemblance of Lisp's S-expressions is intentional, but notice the two
    1.76  kinds of atomic symbols: $\Constant x$ and $\Variable x$. This distinction
    1.77  has some more obscure reasons and you can ignore it about half of the time.
    1.78  You should not take the names ``{\tt Constant}'' and ``{\tt Variable}'' too
    1.79 @@ -456,7 +457,7 @@
    1.80  higher-order: the {\tt "_abs"} does not yet bind the {\tt x} in any way,
    1.81  though later at the term level, {\tt ("_abs" x $t$)} will become an {\tt Abs}
    1.82  node and occurrences of {\tt x} in $t$ will be replaced by {\tt Bound}s. Even
    1.83 -if non constant heads of applications may seem unusual, asts should be
    1.84 +if non-constant heads of applications may seem unusual, asts should be
    1.85  regarded as first-order. Purists may think of ${\tt (} f~x@1~\ldots~x@n{\tt
    1.86  )}$ as a first-order application of some invisible $(n+1)$-ary constant.
    1.87  
    1.88 @@ -510,7 +511,7 @@
    1.89  order to provide some nice standard form of asts before macro expansion takes
    1.90  place. Hence the Pure syntax provides predefined parse ast
    1.91  translations\index{parse ast translation!of Pure} for ordinary applications,
    1.92 -type applications, nested abstraction, meta implication and function types.
    1.93 +type applications, nested abstractions, meta implications and function types.
    1.94  Their net effect on some representative input strings is shown in
    1.95  Figure~\ref{fig:parse_ast_tr}.
    1.96  
    1.97 @@ -609,7 +610,7 @@
    1.98      {\tt Constant}s, type variables as {\tt Variable}s and type applications
    1.99      as {\tt Appl}s with the head type constructor as first element.
   1.100      Additionally, if \ttindex{show_sorts} is set to {\tt true}, some type
   1.101 -    variables are decorated with an ast encoding their sort.
   1.102 +    variables are decorated with an ast encoding of their sort.
   1.103  \end{itemize}
   1.104  
   1.105  \medskip
   1.106 @@ -635,10 +636,9 @@
   1.107  $\Variable x$ is simply printed as $x$.
   1.108  
   1.109  Note that the system does {\em not\/} insert blanks automatically. They
   1.110 -should be part of the mixfix declaration (which provide the user interface
   1.111 -for defining syntax) if they are required to separate tokens. Mixfix
   1.112 -declarations may also contain pretty printing annotations. See
   1.113 -\S\ref{sec:mixfix} for details.
   1.114 +should be part of the mixfix declaration the production has been derived
   1.115 +from, if they are required to separate tokens. Mixfix declarations may also
   1.116 +contain pretty printing annotations.
   1.117  
   1.118  
   1.119  
   1.120 @@ -659,9 +659,8 @@
   1.121  mixfix\/} syntax. Each mixfix annotation defines a precedence grammar
   1.122  production and optionally associates a constant with it.
   1.123  
   1.124 -There is a general form of mixfix annotation exhibiting the full power of
   1.125 -extending a theory's syntax, and some shortcuts for common cases like infix
   1.126 -operators.
   1.127 +There is a general form of mixfix annotation and some shortcuts for common
   1.128 +cases like infix operators.
   1.129  
   1.130  The general \bfindex{mixfix declaration} as it may occur within the {\tt
   1.131  consts} section\index{consts section@{\tt consts} section} of a {\tt .thy}
   1.132 @@ -730,7 +729,7 @@
   1.133  \end{ttbox}
   1.134  Note that the {\tt arities} declaration causes {\tt exp} to be added to the
   1.135  syntax' roots. If you put the above text into a file {\tt exp.thy} and load
   1.136 -it via {\tt use_thy "exp"}, you can run some tests:
   1.137 +it via {\tt use_thy "EXP"}, you can run some tests:
   1.138  \begin{ttbox}
   1.139  val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
   1.140  read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
   1.141 @@ -816,8 +815,8 @@
   1.142  
   1.143  Thus, prefixing infixes with \ttindex{op} makes them behave like ordinary
   1.144  function symbols. Special characters occurring in $c$ have to be escaped as
   1.145 -in delimiters. Also note that the expanded forms above are illegal at the
   1.146 -user level because of duplicate declarations of constants.
   1.147 +in delimiters. Also note that the expanded forms above would be actually
   1.148 +illegal at the user level because of duplicate declarations of constants.
   1.149  
   1.150  
   1.151  \subsection{Binders}
   1.152 @@ -924,7 +923,7 @@
   1.153  cannot refer to such names directly, since they are not legal identifiers.
   1.154  
   1.155  The translations cause the replacement of external forms by internal forms
   1.156 -after parsing and before printing of terms.
   1.157 +after parsing, and vice versa before printing of terms.
   1.158  \end{example}
   1.159  
   1.160  This is only a very simple but common instance of a more powerful mechanism.
   1.161 @@ -950,12 +949,12 @@
   1.162  
   1.163  This specifies a \rmindex{parse rule} ({\tt =>}) a \rmindex{print rule} ({\tt
   1.164  <=}) or both ({\tt ==}). The two $string$s preceded by optional parenthesized
   1.165 -$root$s denote the left-hand and right-hand side of the rule as 'source
   1.166 +$root$s denote the left-hand and right-hand side of the rule as `source
   1.167  code', i.e.\ in the usual syntax of terms.
   1.168  
   1.169  Rules are internalized wrt.\ an intermediate signature that is obtained from
   1.170  the parent theories' ones by adding all material of all sections preceding
   1.171 -{\tt translations} in the {\tt .thy} file, especially new syntax defined in
   1.172 +{\tt translations} in the {\tt .thy} file. Especially, new syntax defined in
   1.173  {\tt consts} is already effective.
   1.174  
   1.175  Then part of the process that transforms input strings into terms is applied:
   1.176 @@ -971,8 +970,8 @@
   1.177  
   1.178  \medskip
   1.179  The result are two lists of translation rules in internal form, that is pairs
   1.180 -of asts. They can be viewed using {\tt Syntax.print_syntax}
   1.181 -(\ttindex{parse_rules} and \ttindex{print_rules}). For {\tt SET} of
   1.182 +of asts. They can be viewed using {\tt Syntax.print_syntax} (sections
   1.183 +\ttindex{parse_rules} and \ttindex{print_rules}). For {\tt SET} of
   1.184  Example~\ref{ex:set_trans} these are:
   1.185  \begin{ttbox}
   1.186  parse_rules:
   1.187 @@ -1001,7 +1000,7 @@
   1.188  In the course of parsing and printing terms, asts are generated as an
   1.189  intermediate form as pictured in Figure~\ref{fig:parse_print}. These asts are
   1.190  normalized wrt.\ the given lists of translation rules in a uniform manner. As
   1.191 -stated earlier, asts are supposed to be first-order 'terms'. The rewriting
   1.192 +stated earlier, asts are supposed to be first-order `terms'. The rewriting
   1.193  systems derived from {\tt translations} sections essentially resemble
   1.194  traditional first-order term rewriting systems. We first examine how a single
   1.195  rule is applied.
   1.196 @@ -1055,8 +1054,8 @@
   1.197  Having first-order matching in mind, the second case of $match$ may look a
   1.198  bit odd. But this is exactly the place, where {\tt Variable}s of non-rule
   1.199  asts behave like {\tt Constant}s. The deeper meaning of this is related with
   1.200 -asts being very 'primitive' in some sense, ignorant of the underlying
   1.201 -'semantics', not far removed from parse trees. At this level it is not yet
   1.202 +asts being very `primitive' in some sense, ignorant of the underlying
   1.203 +`semantics', not far removed from parse trees. At this level it is not yet
   1.204  known, which $id$s will become constants, bounds, frees, types or classes. As
   1.205  $ast_of_pt$ (see \S\ref{sec:asts}) shows, former parse tree heads appear in
   1.206  asts as {\tt Constant}s, while $id$s, $var$s, $tfree$s and $tvar$s become
   1.207 @@ -1100,7 +1099,7 @@
   1.208  always applies the first matching rule reducing an unspecified redex chosen
   1.209  first.
   1.210  
   1.211 -Thereby, 'first rule' is roughly speaking meant wrt.\ the appearance of the
   1.212 +Thereby, `first rule' is roughly speaking meant wrt.\ the appearance of the
   1.213  rules in the {\tt translations} sections. But this is more tricky than it
   1.214  seems: If a given theory is {\em extended}, new rules are simply appended to
   1.215  the end. But if theories are {\em merged}, it is not clear which list of
   1.216 @@ -1215,7 +1214,7 @@
   1.217  atoms.
   1.218  
   1.219  Thus the names of {\tt Constant}s occurring in the (internal) left-hand side
   1.220 -of translation rules should be regarded as 'reserved keywords'. It is good
   1.221 +of translation rules should be regarded as `reserved keywords'. It is good
   1.222  practice to choose non-identifiers here like {\tt\at Finset} or sufficiently
   1.223  long and strange names.
   1.224  \end{example}
   1.225 @@ -1251,10 +1250,11 @@
   1.226  introduced during ast rewriting, which later becomes \verb|%x.B| due to a
   1.227  parse translation associated with \ttindex{_K}. Note that a leading {\tt _}
   1.228  in $id$s is allowed in translation rules, but not in ordinary terms. This
   1.229 -special behaviour of the lexer is very useful for 'forging' asts containing
   1.230 -names that are not directly accessible normally. Unfortunately, there is no
   1.231 -such trick for printing, so we have to add a {\tt ML} section for the print
   1.232 -translation \ttindex{dependent_tr'}.
   1.233 +special behaviour of the lexer is very useful for `forging' asts containing
   1.234 +names that are not directly accessible normally.
   1.235 +
   1.236 +Unfortunately, there is no such trick for printing, so we have to add a {\tt
   1.237 +ML} section for the print translation \ttindex{dependent_tr'}.
   1.238  
   1.239  The parse translation for {\tt _K} is already installed in Pure, and {\tt
   1.240  dependent_tr'} is exported by the syntax module for public use. See
   1.241 @@ -1321,7 +1321,7 @@
   1.242  $(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation function $f$
   1.243  of appropriate kind exists for $c$, the result will be $f \mtt[ x@1, \ldots,
   1.244  x@n \mtt]$. Thereby, $x@1, \ldots, x@n$ (with $n \ge 0$) are asts for ast
   1.245 -translations and terms for term translations. A 'combination' at ast level is
   1.246 +translations and terms for term translations. A `combination' at ast level is
   1.247  of the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots, x@n}$, and at
   1.248  term level $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttrel{\$}
   1.249  x@1 \ttrel{\$} \dots \ttrel{\$} x@n$.
   1.250 @@ -1338,7 +1338,7 @@
   1.251    \item[Parse (ast) translations] are applied bottom-up, i.e.\ the arguments
   1.252      supplied ($x@1, \ldots, x@n$ above) are already in translated form.
   1.253      Additionally, they may not fail, exceptions are re-raised after printing
   1.254 -    of an error message.
   1.255 +    an error message.
   1.256  
   1.257    \item[Print (ast) translations] are applied top-down, i.e.\ supplied with
   1.258      arguments that are partly still in internal form. The result is again fed
   1.259 @@ -1421,12 +1421,11 @@
   1.260  
   1.261  We have to be more careful with types here. While types of {\tt Const}s are
   1.262  completely ignored, type constraints may be printed for some {\tt Free}s and
   1.263 -{\tt Var}s (only if \ttindex{show_types} is set to {\tt true}). Variables of
   1.264 -type \ttindex{dummyT} are never printed with constraint, though. Thus, a
   1.265 +{\tt Var}s (if \ttindex{show_types} is set to {\tt true}). Variables of type
   1.266 +\ttindex{dummyT} are never printed with constraint, though. Thus, a
   1.267  constraint of $x'$ may only appear at its binding place, since {\tt Free}s of
   1.268  $B'$ replacing the appropriate {\tt Bound}s of $B$ via \ttindex{variant_abs}
   1.269 -have all type {\tt dummyT}.
   1.270 -\end{example}
   1.271 +have all type {\tt dummyT}. \end{example}
   1.272  
   1.273  
   1.274  
   1.275 @@ -1454,7 +1453,7 @@
   1.276  \end{ttbox}
   1.277  The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible
   1.278  coercion function. Assuming this definition resides in a file {\tt base.thy},
   1.279 -you have to load it with the command {\tt use_thy "base"}.
   1.280 +you have to load it with the command {\tt use_thy "Base"}.
   1.281  
   1.282  One of the simplest nontrivial logics is {\em minimal logic\/} of
   1.283  implication. Its definition in Isabelle needs no advanced features but