# HG changeset patch # User wenzelm # Date 1010168391 -3600 # Node ID 08eee994bf9965315b0ddd4275de85fc3e8c5fd9 # Parent fcff0c66b4f450842271725590f3a7d6db2299cd updated; diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Jan 04 19:19:51 2002 +0100 @@ -14,7 +14,7 @@ has as many subtrees as there are natural numbers. How can we possibly write down such a tree? Using functional notation! For example, the term \begin{isabelle}% -\ \ \ \ \ Br\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% +\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% \end{isabelle} of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose root is labeled with 0 and whose $i$th subtree is labeled with $i$ and diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Fri Jan 04 19:19:51 2002 +0100 @@ -2,6 +2,130 @@ \begin{isabellebody}% \def\isabellecontext{Documents}% \isamarkupfalse% +% +\isamarkupsection{Concrete syntax \label{sec:concrete-syntax}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure + for concrete syntax is that of general \emph{mixfix + annotations}\index{mixfix annotations|bold}. Associated with any + kind of name and type declaration, mixfixes give rise both to + grammar productions for the parser and output templates for the + pretty printer. + + In full generality, the whole affair of parser and pretty printer + configuration is rather subtle. Any syntax specifications given by + end-users need to interact properly with the existing setup of + Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further + details. It is particularly important to get the precedence of new + syntactic constructs right, avoiding ambiguities with existing + elements. + + \medskip Subsequently we introduce a few simple declaration forms + that already cover the most common situations fairly well.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Infixes% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Syntax annotations may be included wherever constants are declared + directly or indirectly, including \isacommand{consts}, + \isacommand{constdefs}, or \isacommand{datatype} (for the + constructor operations). Type-constructors may be annotated as + well, although this is less frequently encountered in practice + (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind). + + Infix declarations\index{infix annotations|bold} provide a useful + special case of mixfixes, where users need not care about the full + details of priorities, nesting, spacing, etc. The subsequent + example of the exclusive-or operation on boolean values illustrates + typical infix declarations.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline +\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +Any curried function with at least two arguments may be associated + with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to + the same expression internally. In partial applications with less + than two operands there is a special notation with \isa{op} prefix: + \isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; + combined with plain prefix application this turns \isa{xor\ A} + into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}. + + \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above declaration + refers to the bit of concrete syntax to represent the operator, + while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole + construct. + + As it happens, Isabelle/HOL already spends many popular combinations + of ASCII symbols for its own use, including both \isa{{\isacharplus}} and + \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present + \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current + arrangement of inner syntax may be inspected via + \commdx{print\protect\_syntax}, albeit its output is enormous. + + Operator precedence also needs some special considerations. The + admissible range is 0--1000. Very low or high priorities are + basically reserved for the meta-logic. Syntax of Isabelle/HOL + mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is + 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 + HOL forms, or use the mostly unused range 100--900. + + \medskip The keyword \isakeyword{infixl} specifies an operator that + is nested to the \emph{left}: in iterated applications the more + 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, + \isakeyword{infixr} refers to nesting to the \emph{right}, which + 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}}. + In contrast, a \emph{non-oriented} declaration via + \isakeyword{infix} would always demand explicit parentheses. + + Many binary operations observe the associative law, so the exact + grouping does not matter. Nevertheless, formal statements need be + given in a particular format, associativity needs to be treated + explicitly within the logic. Exclusive-or is happens to be + associative, as shown below.% +\end{isamarkuptext}% +\isamarkuptrue% +\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 +\ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptext}% +Such rules may be used in simplification to regroup nested + expressions as required. Note that the system would actually print + 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}} + (due to nesting to the left). We have preferred to give the fully + parenthesized form in the text for clarity.% +\end{isamarkuptext}% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkuptrue% +\isamarkuptrue% +\isamarkupfalse% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% +\isamarkupfalse% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% +\isamarkuptrue% \isamarkupfalse% \end{isabellebody}% %%% Local Variables: diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 04 19:19:51 2002 +0100 @@ -206,7 +206,7 @@ \indexbold{definitions!unfolding}% \end{isamarkuptxt}% \isamarkuptrue% -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptxt}% \noindent diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 04 19:19:51 2002 +0100 @@ -103,7 +103,7 @@ syntax with keywords like \isacommand{datatype} and \isacommand{end}. % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list). Embedded in this syntax are the types and formulae of HOL, whose syntax is -extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators. +extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators. To distinguish the two levels, everything HOL-specific (terms and types) should be enclosed in \texttt{"}\dots\texttt{"}. diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/Types/document/Pairs.tex --- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 04 19:19:51 2002 +0100 @@ -191,7 +191,7 @@ \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptxt}% \noindent diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/Types/document/Typedefs.tex --- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri Jan 04 19:19:51 2002 +0100 @@ -123,7 +123,7 @@ The situation is best summarized with the help of the following diagram, where squares denote types and the irregular region denotes a set: \begin{center} -\includegraphics[scale=.8]{Types/typedef} +\includegraphics[scale=.8]{typedef} \end{center} Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other: diff -r fcff0c66b4f4 -r 08eee994bf99 doc-src/TutorialI/tutorial.ind --- a/doc-src/TutorialI/tutorial.ind Fri Jan 04 19:19:29 2002 +0100 +++ b/doc-src/TutorialI/tutorial.ind Fri Jan 04 19:19:51 2002 +0100 @@ -21,9 +21,6 @@ \item \verb$^$\texttt{*}, \bold{201} \item \isasymAnd, \bold{12}, \bold{201} \item \ttAnd, \bold{201} - \item \isasymrightleftharpoons, 55 - \item \isasymrightharpoonup, 55 - \item \isasymleftharpoondown, 55 \item \emph {$\Rightarrow $}, \bold{5} \item \ttlbr, \bold{201} \item \ttrbr, \bold{201} @@ -283,6 +280,7 @@ \item inductive definitions, 119--137 \item \isacommand {inductive\_cases} (command), 123, 131 \item infinitely branching trees, 43 + \item infix annotations, \bold{54} \item \isacommand{infixr} (annotation), 10 \item \isa {inj_on_def} (theorem), \bold{102} \item injections, 102 @@ -326,6 +324,7 @@ \item LCF, 43 \item \isa {LEAST} (symbol), 23, 77 \item least number operator, \see{\protect\isa{LEAST}}{77} + \item Leibniz, Gottfried Wilhelm, 53 \item \isacommand {lemma} (command), 13 \item \isacommand {lemmas} (command), 85, 94 \item \isa {length} (symbol), 18 @@ -357,6 +356,7 @@ \item meta-logic, \bold{72} \item methods, \bold{16} \item \isa {min} (constant), 23, 24 + \item mixfix annotations, \bold{53} \item \isa {mod} (symbol), 23 \item \isa {mod_div_equality} (theorem), \bold{143} \item \isa {mod_mult_distrib} (theorem), \bold{143} @@ -419,6 +419,7 @@ \item \isacommand {prefer} (command), 16, 92 \item primitive recursion, \see{recursion, primitive}{1} \item \isacommand {primrec} (command), 10, 18, 38--43 + \item \isacommand {print\_syntax} (command), 54 \item product type, \see{pairs and tuples}{1} \item Proof General, \bold{7} \item proof state, 12 @@ -544,7 +545,6 @@ \item surjections, 102 \item \isa {sym} (theorem), \bold{86} \item syntax, 6, 11 - \item syntax translations, 55--56 \indexspace @@ -569,7 +569,6 @@ \item tracing the simplifier, \bold{33} \item \isa {trancl_trans} (theorem), \bold{105} \item transition systems, 109 - \item \isacommand {translations} (command), 55--56 \item tries, 44--46 \item \isa {True} (constant), 5 \item \isa {truncate} (constant), 155