# HG changeset patch # User nipkow # Date 1194524584 -3600 # Node ID 6eb185959aec8bf3d1a6576762d7cec0a38d5994 # Parent 93da87a1d2b366e5421ab396cdc716dad980206f updated to notation and abbreviation diff -r 93da87a1d2b3 -r 6eb185959aec doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Thu Nov 08 13:21:15 2007 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Thu Nov 08 13:23:04 2007 +0100 @@ -11,13 +11,13 @@ for the parser and output templates for the pretty printer. In full generality, parser and pretty printer configuration is a - subtle affair \cite{isabelle-ref}. Your syntax specifications need + subtle affair~\cite{isabelle-ref}. Your syntax specifications need to interact properly with the existing setup of Isabelle/Pure and Isabelle/HOL\@. To avoid creating ambiguities with existing elements, it is particularly important to give new syntactic constructs the right precedence. - \medskip Subsequently we introduce a few simple syntax declaration + Below we introduce a few simple syntax declaration forms that already cover many common situations fairly well. *} @@ -50,7 +50,7 @@ @{text "op [+]"}; together with ordinary function application, this turns @{text "xor A"} into @{text "op [+] A"}. - \medskip The keyword \isakeyword{infixl} seen above specifies an + The keyword \isakeyword{infixl} seen above specifies an infix operator that is nested to the \emph{left}: in iterated applications the more complex expression appears on the left-hand side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] @@ -134,7 +134,7 @@ by Isabelle. Note that @{text "\\<^isup>\"} is a single syntactic entity, not an exponentiation. - \medskip Replacing our previous definition of @{text xor} by the + Replacing our previous definition of @{text xor} by the following specifies an Isabelle symbol for the new operator: *} @@ -155,7 +155,7 @@ just type a named entity \verb,\,\verb,, by hand; the corresponding symbol will be displayed after further input. - \medskip More flexible is to provide alternative syntax forms + More flexible is to provide alternative syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}. By convention, the mode of ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or {\LaTeX} output is active. Now @@ -170,26 +170,20 @@ xor :: "bool \ bool \ bool" (infixl "[+]\" 60) "A [+]\ B \ (A \ \ B) \ (\ A \ B)" -syntax (xsymbols) - xor :: "bool \ bool \ bool" (infixl "\\" 60) +notation (xsymbols) xor (infixl "\\" 60) (*<*) local (*>*) -text {* - The \commdx{syntax} command introduced here acts like - \isakeyword{consts}, but without declaring a logical constant. The - print mode specification of \isakeyword{syntax}, here @{text - "(xsymbols)"}, is optional. Also note that its type merely serves - for syntactic purposes, and is \emph{not} checked for consistency - with the real constant. +text {*The \commdx{notation} command associates a mixfix +annotation with a logical constant. The print mode specification of +\isakeyword{syntax}, here @{text "(xsymbols)"}, is optional. - \medskip We may now write @{text "A [+] B"} or @{text "A \ B"} in - input, while output uses the nicer syntax of $xsymbols$ whenever - that print mode is active. Such an arrangement is particularly - useful for interactive development, where users may type ASCII text - and see mathematical symbols displayed during proofs. -*} +We may now write @{text "A [+] B"} or @{text "A \ B"} in input, while +output uses the nicer syntax of $xsymbols$ whenever that print mode is +active. Such an arrangement is particularly useful for interactive +development, where users may type ASCII text and see mathematical +symbols displayed during proofs. *} subsection {* Prefix Annotations *} @@ -223,64 +217,57 @@ *} -subsection {* Syntax Translations \label{sec:syntax-translations} *} +subsection {* Abbreviations \label{sec:abbreviations} *} -text{* - Mixfix syntax annotations merely decorate particular constant - application forms with concrete syntax, for instance replacing \ - @{text "xor A B"} by @{text "A \ B"}. Occasionally, the - relationship between some piece of notation and its internal form is - more complicated. Here we need \bfindex{syntax translations}. +text{* Mixfix syntax annotations merely decorate particular constant +application forms with concrete syntax, for instance replacing +@{text "xor A B"} by @{text "A \ B"}. Occasionally, the relationship +between some piece of notation and its internal form is more +complicated. Here we need \emph{abbreviations}. + +Command \commdx{abbreviation} introduces an uninterpreted notational +constant as an abbreviation for a complex term. Abbreviations are +unfolded upon parsing and re-introduced upon printing. This provides a +simple mechanism for syntactic macros. - Using the \isakeyword{syntax}\index{syntax (command)}, command we - introduce uninterpreted notational elements. Then - \commdx{translations} relate input forms to complex logical - expressions. This provides a simple mechanism for syntactic macros; - even heavier transformations may be written in ML - \cite{isabelle-ref}. +A typical use of abbreviations is to introduce relational notation for +membership in a set of pairs, replacing @{text "(x, y) \ sim"} by +@{text "x \ y"}. *} + +consts sim :: "('a \ 'a) set" + +abbreviation sim2 :: "'a \ 'a \ bool" (infix "\" 50) +where "x \ y \ (x, y) \ sim" - \medskip A typical use of syntax translations is to introduce - relational notation for membership in a set of pair, replacing \ - @{text "(x, y) \ sim"} by @{text "x \ y"}. +text {* \noindent The given meta-equality is used as a rewrite rule +after parsing (replacing \mbox{@{prop"x \ y"}} by @{text"(x,y) \ +sim"}) and before printing (turning @{text"(x,y) \ sim"} back into +\mbox{@{prop"x \ y"}}). The name of the dummy constant @{text "sim2"} +does not matter, as long as it is unique. + +Another common application of abbreviations is to +provide variant versions of fundamental relational expressions, such +as @{text \} for negated equalities. The following declaration +stems from Isabelle/HOL itself: *} -consts - sim :: "('a \ 'a) set" - -syntax - "_sim" :: "'a \ 'a \ bool" (infix "\" 50) -translations - "x \ y" \ "(x, y) \ sim" +abbreviation not_equal :: "'a \ 'a \ bool" (infixl "~=\" 50) +where "x ~=\ y \ \ (x = y)" -text {* - \noindent Here the name of the dummy constant @{text "_sim"} does - not matter, as long as it is not used elsewhere. Prefixing an - underscore is a common convention. The \isakeyword{translations} - declaration already uses concrete syntax on the left-hand side; - internally we relate a raw application @{text "_sim x y"} with - @{text "(x, y) \ sim"}. +notation (xsymbols) not_equal (infix "\\" 50) + +text {* \noindent The notation @{text \} is introduced separately to restrict it +to the \emph{xsymbols} mode. - \medskip Another common application of syntax translations is to - provide variant versions of fundamental relational expressions, such - as @{text \} for negated equalities. The following declaration - stems from Isabelle/HOL itself: -*} - -syntax "_not_equal" :: "'a \ 'a \ bool" (infixl "\\" 50) -translations "x \\ y" \ "\ (x = y)" + Abbreviations are appropriate when the defined concept is a +simple variation on an existing one. But because of the automatic +folding and unfolding of abbreviations, they do not scale up well to +large hierarchies of concepts. Abbreviations do not replace +definitions. -text {* - \noindent Normally one would introduce derived concepts like this - within the logic, using \isakeyword{consts} + \isakeyword{defs} - instead of \isakeyword{syntax} + \isakeyword{translations}. The - present formulation has the virtue that expressions are immediately - replaced by the ``definition'' upon parsing; the effect is reversed - upon printing. - - This sort of translation is appropriate when the defined concept is - a trivial variation on an existing one. On the other hand, syntax - translations do not scale up well to large hierarchies of concepts. - Translations do not replace definitions! +Abbreviations are a simplified form of the general concept of +\emph{syntax translations}; even heavier transformations may be +written in ML \cite{isabelle-ref}. *} @@ -643,6 +630,7 @@ \begin{tabular}{ll} \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ + \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\ \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\ diff -r 93da87a1d2b3 -r 6eb185959aec doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Thu Nov 08 13:21:15 2007 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Thu Nov 08 13:23:04 2007 +0100 @@ -26,13 +26,13 @@ for the parser and output templates for the pretty printer. In full generality, parser and pretty printer configuration is a - subtle affair \cite{isabelle-ref}. Your syntax specifications need + subtle affair~\cite{isabelle-ref}. Your syntax specifications need to interact properly with the existing setup of Isabelle/Pure and Isabelle/HOL\@. To avoid creating ambiguities with existing elements, it is particularly important to give new syntactic constructs the right precedence. - \medskip Subsequently we introduce a few simple syntax declaration + Below we introduce a few simple syntax declaration forms that already cover many common situations fairly well.% \end{isamarkuptext}% \isamarkuptrue% @@ -66,7 +66,7 @@ \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}. - \medskip The keyword \isakeyword{infixl} seen above specifies an + The keyword \isakeyword{infixl} seen above specifies an infix operator that is nested to the \emph{left}: in iterated applications the more complex expression appears on the left-hand side, and \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} means nesting to the @@ -149,7 +149,7 @@ by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single syntactic entity, not an exponentiation. - \medskip Replacing our previous definition of \isa{xor} by the + Replacing our previous definition of \isa{xor} by the following specifies an Isabelle symbol for the new operator:% \end{isamarkuptext}% \isamarkuptrue% @@ -176,7 +176,7 @@ just type a named entity \verb,\,\verb,, by hand; the corresponding symbol will be displayed after further input. - \medskip More flexible is to provide alternative syntax forms + More flexible is to provide alternative syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}. By convention, the mode of ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or {\LaTeX} output is active. Now @@ -201,21 +201,18 @@ \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline \ \ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline \isanewline -\isacommand{syntax}\isamarkupfalse% -\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline -\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}% +\isacommand{notation}\isamarkupfalse% +\ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}% \begin{isamarkuptext}% -The \commdx{syntax} command introduced here acts like - \isakeyword{consts}, but without declaring a logical constant. The - print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional. Also note that its type merely serves - for syntactic purposes, and is \emph{not} checked for consistency - with the real constant. +The \commdx{notation} command associates a mixfix +annotation with a logical constant. The print mode specification of +\isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional. - \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in - input, while output uses the nicer syntax of $xsymbols$ whenever - that print mode is active. Such an arrangement is particularly - useful for interactive development, where users may type ASCII text - and see mathematical symbols displayed during proofs.% +We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while +output uses the nicer syntax of $xsymbols$ whenever that print mode is +active. Such an arrangement is particularly useful for interactive +development, where users may type ASCII text and see mathematical +symbols displayed during proofs.% \end{isamarkuptext}% \isamarkuptrue% % @@ -251,69 +248,64 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}% +\isamarkupsubsection{Abbreviations \label{sec:abbreviations}% } \isamarkuptrue% % \begin{isamarkuptext}% Mixfix syntax annotations merely decorate particular constant - application forms with concrete syntax, for instance replacing \ - \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}. Occasionally, the - relationship between some piece of notation and its internal form is - more complicated. Here we need \bfindex{syntax translations}. +application forms with concrete syntax, for instance replacing +\isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}. Occasionally, the relationship +between some piece of notation and its internal form is more +complicated. Here we need \emph{abbreviations}. - Using the \isakeyword{syntax}\index{syntax (command)}, command we - introduce uninterpreted notational elements. Then - \commdx{translations} relate input forms to complex logical - expressions. This provides a simple mechanism for syntactic macros; - even heavier transformations may be written in ML - \cite{isabelle-ref}. +Command \commdx{abbreviation} introduces an uninterpreted notational +constant as an abbreviation for a complex term. Abbreviations are +unfolded upon parsing and re-introduced upon printing. This provides a +simple mechanism for syntactic macros. - \medskip A typical use of syntax translations is to introduce - relational notation for membership in a set of pair, replacing \ - \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.% +A typical use of abbreviations is to introduce relational notation for +membership in a set of pairs, replacing \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by +\isa{x\ {\isasymapprox}\ y}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isamarkupfalse% -\isanewline -\ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{syntax}\isamarkupfalse% +\ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline \isanewline -\ \ {\isachardoublequoteopen}{\isacharunderscore}sim{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymapprox}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline -\isacommand{translations}\isamarkupfalse% -\isanewline -\ \ {\isachardoublequoteopen}x\ {\isasymapprox}\ y{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequoteclose}% +\isacommand{abbreviation}\isamarkupfalse% +\ sim{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymapprox}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline +\isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymapprox}\ y\ \ {\isasymequiv}\ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequoteclose}% \begin{isamarkuptext}% -\noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does - not matter, as long as it is not used elsewhere. Prefixing an - underscore is a common convention. The \isakeyword{translations} - declaration already uses concrete syntax on the left-hand side; - internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with - \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}. +\noindent The given meta-equality is used as a rewrite rule +after parsing (replacing \mbox{\isa{x\ {\isasymapprox}\ y}} by \isa{{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ sim}) and before printing (turning \isa{{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ sim} back into +\mbox{\isa{x\ {\isasymapprox}\ y}}). The name of the dummy constant \isa{sim{\isadigit{2}}} +does not matter, as long as it is unique. - \medskip Another common application of syntax translations is to - provide variant versions of fundamental relational expressions, such - as \isa{{\isasymnoteq}} for negated equalities. The following declaration - stems from Isabelle/HOL itself:% +Another common application of abbreviations is to +provide variant versions of fundamental relational expressions, such +as \isa{{\isasymnoteq}} for negated equalities. The following declaration +stems from Isabelle/HOL itself:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{syntax}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymnoteq}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline -\isacommand{translations}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}% +\isacommand{abbreviation}\isamarkupfalse% +\ not{\isacharunderscore}equal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isachartilde}{\isacharequal}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline +\isakeyword{where}\ {\isachardoublequoteopen}x\ {\isachartilde}{\isacharequal}{\isasymignore}\ y\ \ {\isasymequiv}\ \ {\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{notation}\isamarkupfalse% +\ {\isacharparenleft}xsymbols{\isacharparenright}\ not{\isacharunderscore}equal\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymnoteq}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% \begin{isamarkuptext}% -\noindent Normally one would introduce derived concepts like this - within the logic, using \isakeyword{consts} + \isakeyword{defs} - instead of \isakeyword{syntax} + \isakeyword{translations}. The - present formulation has the virtue that expressions are immediately - replaced by the ``definition'' upon parsing; the effect is reversed - upon printing. +\noindent The notation \isa{{\isasymnoteq}} is introduced separately to restrict it +to the \emph{xsymbols} mode. - This sort of translation is appropriate when the defined concept is - a trivial variation on an existing one. On the other hand, syntax - translations do not scale up well to large hierarchies of concepts. - Translations do not replace definitions!% + Abbreviations are appropriate when the defined concept is a +simple variation on an existing one. But because of the automatic +folding and unfolding of abbreviations, they do not scale up well to +large hierarchies of concepts. Abbreviations do not replace +definitions. + +Abbreviations are a simplified form of the general concept of +\emph{syntax translations}; even heavier transformations may be +written in ML \cite{isabelle-ref}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -713,6 +705,7 @@ \begin{tabular}{ll} \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ + \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\ \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\