diff -r e968745986f1 -r cfcc1f6f21df doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Thu Mar 07 12:03:43 2002 +0100 +++ b/doc-src/IsarRef/syntax.tex Thu Mar 07 19:04:00 2002 +0100 @@ -1,5 +1,5 @@ -\chapter{Syntax primitives} +\chapter{Syntax Primitives} The rather generic framework of Isabelle/Isar syntax emerges from three main syntactic categories: \emph{commands} of the top-level Isar engine (covering @@ -40,7 +40,7 @@ particularly useful in interactive shell sessions to make clear where the current command is intended to end. Otherwise, the interpreter loop will continue to issue a secondary prompt ``\verb,#,'' until an end-of-command is -clearly indicated from the input syntax, e.g.\ encounter of the next command +clearly recognized from the input syntax, e.g.\ encounter of the next command keyword. Advanced interfaces such as Proof~General \cite{proofgeneral} do not require @@ -92,12 +92,11 @@ symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots \end{matharray} -The syntax of \railtoken{string} admits any characters, including newlines; -``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by -a backslash. Note that ML-style control characters are \emph{not} supported. -The body of \railtoken{verbatim} may consist of any text not containing -``\verb|*}|''; this allows handsome inclusion of quotes without further -escapes. +The syntax of $string$ admits any characters, including newlines; ``\verb|"|'' +(double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash. +Note that ML-style control characters are \emph{not} supported. The body of +$verbatim$ may consist of any text not containing ``\verb|*}|''; this allows +convenient inclusion of quotes without further escapes. Comments take the form \texttt{(*~\dots~*)} and may in principle be nested, just as in ML. Note that these are \emph{source} comments only, which are @@ -109,7 +108,8 @@ Proof~General does not handle nested comments properly; it is also unable to keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite their rather different meaning. These are inherent problems of Emacs - legacy. + legacy. Users should not be overly aggressive about nesting or alternating + these delimiters. \end{warn} \medskip @@ -209,8 +209,8 @@ level. Basically, any such entity has to be quoted to turn it into a single token (the parsing and type-checking is performed internally later). For convenience, a slightly more liberal convention is adopted: quotes may be -omitted for any type or term that is already \emph{atomic} at the outer level. -For example, one may just write \texttt{x} instead of \texttt{"x"}. Note that +omitted for any type or term that is already atomic at the outer level. For +example, one may just write \texttt{x} instead of \texttt{"x"}. Note that symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well, provided these have not been superseded by commands or other keywords already (e.g.\ \texttt{=} or \texttt{+}). @@ -338,9 +338,9 @@ Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}, the former requires an actual singleton result. Any of these theorem specifications may include lists of attributes both on the left and right hand -sides; attributes are applied to any immediately preceding theorem. If names -are omitted, the theorems are not stored within the theorem database of the -theory or proof context; any given attributes are still applied, though. +sides; attributes are applied to any immediately preceding fact. If names are +omitted, the theorems are not stored within the theorem database of the theory +or proof context; any given attributes are still applied, though. \indexouternonterm{thmdecl}\indexouternonterm{axmdecl} \indexouternonterm{thmdef}\indexouternonterm{thmrefs} @@ -365,9 +365,9 @@ Wherever explicit propositions (or term fragments) occur in a proof text, casual binding of schematic term variables may be given specified via patterns -of the form $\ISS{p@1\;\dots}{p@n}$. There are separate versions available -for \railqtoken{term}s and \railqtoken{prop}s. The latter provides a -$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule. +of the form ``$\ISS{p@1\;\dots}{p@n}$''. There are separate versions +available for \railqtoken{term}s and \railqtoken{prop}s. The latter provides +a $\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule. \indexouternonterm{termpat}\indexouternonterm{proppat} \begin{rail} @@ -380,8 +380,8 @@ Declarations of local variables $x :: \tau$ and logical propositions $a : \phi$ represent different views on the same principle of introducing a local scope. In practice, one may usually omit the typing of $vars$ (due to -type-inference), and the naming of propositions (due to implicit chaining of -emerging facts). In any case, Isar proof elements usually admit to introduce +type-inference), and the naming of propositions (due to implicit references of +current facts). In any case, Isar proof elements usually admit to introduce multiple such items simultaneously. \indexouternonterm{vars}\indexouternonterm{props} @@ -419,8 +419,8 @@ preparation system (see also \S\ref{sec:document-prep}). Thus embedding of -\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a -text block would cause +``\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}}'' +within a text block would cause \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x} to appear in the final {\LaTeX} document. Also note that theorem antiquotations may involve attributes as well. For example, @@ -453,25 +453,32 @@ \texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|. \begin{descr} + \item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute specifications may be included as well (see also \S\ref{sec:syn-att}); the $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly useful to suppress printing of schematic variables. + \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$. + \item [$\at\{term~t\}$] prints a well-typed term $t$. + \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$. + \item [$\at\{text~s\}$] prints uninterpreted source text $s$. This is particularly useful to print portions of text according to the Isabelle {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces - of terms that cannot be parsed or type-checked yet). + of terms that should not be parsed or type-checked yet). + \item [$\at\{goals\}$] prints the current \emph{dynamic} goal state. This is - only for support of tactic-emulation scripts within Isar --- presentation of - goal states does not conform to actual human-readable proof documents. - + mainly for support of tactic-emulation scripts within Isar --- presentation + of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing! + \item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not print the main goal. + \end{descr} \medskip @@ -507,9 +514,10 @@ the above flags are disabled by default, unless changed from ML. \medskip Note that antiquotations do not only spare the author from tedious -typing, but also achieve some degree of consistency-checking of informal -explanations with formal developments, since well-formedness of terms and -types with respect to the current theory or proof context can be ensured. +typing of logical entities, but also achieve some degree of +consistency-checking of informal explanations with formal developments: +well-formedness of terms and types with respect to the current theory or proof +context is ensured here. %%% Local Variables: %%% mode: latex