1.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Jan 04 19:19:29 2002 +0100
1.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Jan 04 19:19:51 2002 +0100
1.3 @@ -14,7 +14,7 @@
1.4 has as many subtrees as there are natural numbers. How can we possibly
1.5 write down such a tree? Using functional notation! For example, the term
1.6 \begin{isabelle}%
1.7 -\ \ \ \ \ Br\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
1.8 +\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
1.9 \end{isabelle}
1.10 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
1.11 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Fri Jan 04 19:19:29 2002 +0100
2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Fri Jan 04 19:19:51 2002 +0100
2.3 @@ -2,6 +2,130 @@
2.4 \begin{isabellebody}%
2.5 \def\isabellecontext{Documents}%
2.6 \isamarkupfalse%
2.7 +%
2.8 +\isamarkupsection{Concrete syntax \label{sec:concrete-syntax}%
2.9 +}
2.10 +\isamarkuptrue%
2.11 +%
2.12 +\begin{isamarkuptext}%
2.13 +Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure
2.14 + for concrete syntax is that of general \emph{mixfix
2.15 + annotations}\index{mixfix annotations|bold}. Associated with any
2.16 + kind of name and type declaration, mixfixes give rise both to
2.17 + grammar productions for the parser and output templates for the
2.18 + pretty printer.
2.19 +
2.20 + In full generality, the whole affair of parser and pretty printer
2.21 + configuration is rather subtle. Any syntax specifications given by
2.22 + end-users need to interact properly with the existing setup of
2.23 + Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further
2.24 + details. It is particularly important to get the precedence of new
2.25 + syntactic constructs right, avoiding ambiguities with existing
2.26 + elements.
2.27 +
2.28 + \medskip Subsequently we introduce a few simple declaration forms
2.29 + that already cover the most common situations fairly well.%
2.30 +\end{isamarkuptext}%
2.31 +\isamarkuptrue%
2.32 +%
2.33 +\isamarkupsubsection{Infixes%
2.34 +}
2.35 +\isamarkuptrue%
2.36 +%
2.37 +\begin{isamarkuptext}%
2.38 +Syntax annotations may be included wherever constants are declared
2.39 + directly or indirectly, including \isacommand{consts},
2.40 + \isacommand{constdefs}, or \isacommand{datatype} (for the
2.41 + constructor operations). Type-constructors may be annotated as
2.42 + well, although this is less frequently encountered in practice
2.43 + (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
2.44 +
2.45 + Infix declarations\index{infix annotations|bold} provide a useful
2.46 + special case of mixfixes, where users need not care about the full
2.47 + details of priorities, nesting, spacing, etc. The subsequent
2.48 + example of the exclusive-or operation on boolean values illustrates
2.49 + typical infix declarations.%
2.50 +\end{isamarkuptext}%
2.51 +\isamarkuptrue%
2.52 +\isacommand{constdefs}\isanewline
2.53 +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
2.54 +\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.55 +%
2.56 +\begin{isamarkuptext}%
2.57 +Any curried function with at least two arguments may be associated
2.58 + with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to
2.59 + the same expression internally. In partial applications with less
2.60 + than two operands there is a special notation with \isa{op} prefix:
2.61 + \isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}};
2.62 + combined with plain prefix application this turns \isa{xor\ A}
2.63 + into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
2.64 +
2.65 + \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above declaration
2.66 + refers to the bit of concrete syntax to represent the operator,
2.67 + while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole
2.68 + construct.
2.69 +
2.70 + As it happens, Isabelle/HOL already spends many popular combinations
2.71 + of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
2.72 + \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present
2.73 + \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current
2.74 + arrangement of inner syntax may be inspected via
2.75 + \commdx{print\protect\_syntax}, albeit its output is enormous.
2.76 +
2.77 + Operator precedence also needs some special considerations. The
2.78 + admissible range is 0--1000. Very low or high priorities are
2.79 + basically reserved for the meta-logic. Syntax of Isabelle/HOL
2.80 + mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
2.81 + centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common
2.82 + HOL forms, or use the mostly unused range 100--900.
2.83 +
2.84 + \medskip The keyword \isakeyword{infixl} specifies an operator that
2.85 + is nested to the \emph{left}: in iterated applications the more
2.86 + complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly,
2.87 + \isakeyword{infixr} refers to nesting to the \emph{right}, which
2.88 + would turn \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} into \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.
2.89 + In contrast, a \emph{non-oriented} declaration via
2.90 + \isakeyword{infix} would always demand explicit parentheses.
2.91 +
2.92 + Many binary operations observe the associative law, so the exact
2.93 + grouping does not matter. Nevertheless, formal statements need be
2.94 + given in a particular format, associativity needs to be treated
2.95 + explicitly within the logic. Exclusive-or is happens to be
2.96 + associative, as shown below.%
2.97 +\end{isamarkuptext}%
2.98 +\isamarkuptrue%
2.99 +\isacommand{lemma}\ xor{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}{\isachardoublequote}\isanewline
2.100 +\ \ \isamarkupfalse%
2.101 +\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
2.102 +%
2.103 +\begin{isamarkuptext}%
2.104 +Such rules may be used in simplification to regroup nested
2.105 + expressions as required. Note that the system would actually print
2.106 + the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}
2.107 + (due to nesting to the left). We have preferred to give the fully
2.108 + parenthesized form in the text for clarity.%
2.109 +\end{isamarkuptext}%
2.110 +\isamarkuptrue%
2.111 +\isamarkuptrue%
2.112 +\isamarkuptrue%
2.113 +\isamarkupfalse%
2.114 +\isamarkupfalse%
2.115 +\isamarkupfalse%
2.116 +\isamarkupfalse%
2.117 +\isamarkuptrue%
2.118 +\isamarkuptrue%
2.119 +\isamarkupfalse%
2.120 +\isamarkuptrue%
2.121 +\isamarkuptrue%
2.122 +\isamarkuptrue%
2.123 +\isamarkupfalse%
2.124 +\isamarkuptrue%
2.125 +\isamarkuptrue%
2.126 +\isamarkuptrue%
2.127 +\isamarkuptrue%
2.128 +\isamarkuptrue%
2.129 +\isamarkuptrue%
2.130 +\isamarkuptrue%
2.131 \isamarkupfalse%
2.132 \end{isabellebody}%
2.133 %%% Local Variables:
3.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 04 19:19:29 2002 +0100
3.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 04 19:19:51 2002 +0100
3.3 @@ -206,7 +206,7 @@
3.4 \indexbold{definitions!unfolding}%
3.5 \end{isamarkuptxt}%
3.6 \isamarkuptrue%
3.7 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
3.8 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
3.9 %
3.10 \begin{isamarkuptxt}%
3.11 \noindent
4.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 04 19:19:29 2002 +0100
4.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 04 19:19:51 2002 +0100
4.3 @@ -103,7 +103,7 @@
4.4 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
4.5 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
4.6 Embedded in this syntax are the types and formulae of HOL, whose syntax is
4.7 -extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
4.8 +extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.
4.9 To distinguish the two levels, everything
4.10 HOL-specific (terms and types) should be enclosed in
4.11 \texttt{"}\dots\texttt{"}.
5.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 04 19:19:29 2002 +0100
5.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 04 19:19:51 2002 +0100
5.3 @@ -191,7 +191,7 @@
5.4 \isamarkupfalse%
5.5 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
5.6 \isamarkupfalse%
5.7 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
5.8 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
5.9 %
5.10 \begin{isamarkuptxt}%
5.11 \noindent
6.1 --- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri Jan 04 19:19:29 2002 +0100
6.2 +++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri Jan 04 19:19:51 2002 +0100
6.3 @@ -123,7 +123,7 @@
6.4 The situation is best summarized with the help of the following diagram,
6.5 where squares denote types and the irregular region denotes a set:
6.6 \begin{center}
6.7 -\includegraphics[scale=.8]{Types/typedef}
6.8 +\includegraphics[scale=.8]{typedef}
6.9 \end{center}
6.10 Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
6.11 surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
7.1 --- a/doc-src/TutorialI/tutorial.ind Fri Jan 04 19:19:29 2002 +0100
7.2 +++ b/doc-src/TutorialI/tutorial.ind Fri Jan 04 19:19:51 2002 +0100
7.3 @@ -21,9 +21,6 @@
7.4 \item \verb$^$\texttt{*}, \bold{201}
7.5 \item \isasymAnd, \bold{12}, \bold{201}
7.6 \item \ttAnd, \bold{201}
7.7 - \item \isasymrightleftharpoons, 55
7.8 - \item \isasymrightharpoonup, 55
7.9 - \item \isasymleftharpoondown, 55
7.10 \item \emph {$\Rightarrow $}, \bold{5}
7.11 \item \ttlbr, \bold{201}
7.12 \item \ttrbr, \bold{201}
7.13 @@ -283,6 +280,7 @@
7.14 \item inductive definitions, 119--137
7.15 \item \isacommand {inductive\_cases} (command), 123, 131
7.16 \item infinitely branching trees, 43
7.17 + \item infix annotations, \bold{54}
7.18 \item \isacommand{infixr} (annotation), 10
7.19 \item \isa {inj_on_def} (theorem), \bold{102}
7.20 \item injections, 102
7.21 @@ -326,6 +324,7 @@
7.22 \item LCF, 43
7.23 \item \isa {LEAST} (symbol), 23, 77
7.24 \item least number operator, \see{\protect\isa{LEAST}}{77}
7.25 + \item Leibniz, Gottfried Wilhelm, 53
7.26 \item \isacommand {lemma} (command), 13
7.27 \item \isacommand {lemmas} (command), 85, 94
7.28 \item \isa {length} (symbol), 18
7.29 @@ -357,6 +356,7 @@
7.30 \item meta-logic, \bold{72}
7.31 \item methods, \bold{16}
7.32 \item \isa {min} (constant), 23, 24
7.33 + \item mixfix annotations, \bold{53}
7.34 \item \isa {mod} (symbol), 23
7.35 \item \isa {mod_div_equality} (theorem), \bold{143}
7.36 \item \isa {mod_mult_distrib} (theorem), \bold{143}
7.37 @@ -419,6 +419,7 @@
7.38 \item \isacommand {prefer} (command), 16, 92
7.39 \item primitive recursion, \see{recursion, primitive}{1}
7.40 \item \isacommand {primrec} (command), 10, 18, 38--43
7.41 + \item \isacommand {print\_syntax} (command), 54
7.42 \item product type, \see{pairs and tuples}{1}
7.43 \item Proof General, \bold{7}
7.44 \item proof state, 12
7.45 @@ -544,7 +545,6 @@
7.46 \item surjections, 102
7.47 \item \isa {sym} (theorem), \bold{86}
7.48 \item syntax, 6, 11
7.49 - \item syntax translations, 55--56
7.50
7.51 \indexspace
7.52
7.53 @@ -569,7 +569,6 @@
7.54 \item tracing the simplifier, \bold{33}
7.55 \item \isa {trancl_trans} (theorem), \bold{105}
7.56 \item transition systems, 109
7.57 - \item \isacommand {translations} (command), 55--56
7.58 \item tries, 44--46
7.59 \item \isa {True} (constant), 5
7.60 \item \isa {truncate} (constant), 155