diff -r fbc17f1e746b -r 930df4604b36 doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Sun Jan 06 16:51:04 2002 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Sun Jan 06 16:51:48 2002 +0100 @@ -106,7 +106,7 @@ *} -subsection {* Mathematical Symbols \label{sec:thy-present-symbols} *} +subsection {* Mathematical Symbols *} text {* Concrete syntax based on plain ASCII characters has its inherent @@ -137,7 +137,7 @@ interpretation is left to further front-end tools. For example, the \verb,\,\verb,, symbol of Isabelle is really displayed as $\forall$ --- both by the user-interface of Proof~General + X-Symbol - and the Isabelle document processor (see \S\ref{FIXME}). + and the Isabelle document processor (see \S\ref{sec:document-prep}). A list of standard Isabelle symbols is given in \cite[appendix~A]{isabelle-sys}. Users may introduce their own @@ -241,66 +241,99 @@ | Dollar nat ("$") text {* - Here the degenerate mixfix annotations on the rightmost column - happen to consist of a single Isabelle symbol each: + \noindent Here the degenerate mixfix annotations on the rightmost + column happen to consist of a single Isabelle symbol each: \verb,\,\verb,,, \verb,\,\verb,,, - \verb,\,\verb,,, \verb,$,. + \verb,\,\verb,,, and \verb,$,. Recall that a constructor like @{text Euro} actually is a function @{typ "nat \ currency"}. An expression like @{text "Euro 10"} will - be printed as @{term "\ 10"}. Only the head of the application is - subject to our concrete syntax; this simple form already achieves + be printed as @{term "\ 10"}; only the head of the application is + subject to our concrete syntax. This simple form already achieves conformance with notational standards of the European Commission. \medskip Certainly, the same idea of prefix syntax also works for - \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we - might introduce a (slightly unrealistic) function to calculate an - abstract currency value, by cases on the datatype constructors and - fixed exchange rates. The funny symbol used here is that of - \verb,\,. + \isakeyword{consts}, \isakeyword{constdefs} etc. The slightly + unusual syntax declaration below decorates the existing @{typ + currency} type with the international currency symbol @{text \} + (\verb,\,\verb,,). +*} + +syntax + currency :: type ("\") + +text {* + \noindent Here @{typ type} refers to the builtin syntactic category + of Isabelle types. We could now write down funny things like @{text + "\ :: nat \ \"}, for example. +*} + + +subsection {* Syntax Translations \label{sec:syntax-translations} *} + +text{* + Mixfix syntax annotations work well for those situations, where a + constant application forms needs to be decorated by concrete syntax. + Just reconsider @{text "xor A B"} versus @{text "A \ B"} covered + before. Occasionally, the relationship between some piece of + notation and its internal form is slightly more involved. + + Here the concept of \bfindex{syntax translations} enters the scene. + Using the raw \isakeyword{syntax}\index{syntax (command)} command we + introduce uninterpreted notational elements, while + \commdx{translations} relates the input forms with certain logical + expressions. This essentially provides a simple mechanism for for + syntactic macros; even heavier transformations may be programmed in + ML \cite{isabelle-ref}. + + \medskip A typical example of syntax translations is to decorate an + relational expression (i.e.\ set membership of tuples) with nice + symbolic notation, such as @{text "(x, y) \ sim"} versus @{text "x \ + y"}. *} consts - currency :: "currency \ nat" ("\") - + sim :: "('a \ 'a) set" -subsection {* Syntax Translations \label{sec:def-translations} *} - -text{* - FIXME +syntax + "_sim" :: "'a \ 'a \ bool" (infix "\" 50) +translations + "x \ y" \ "(x, y) \ sim" -\index{syntax translations|(}% -\index{translations@\isacommand {translations} (command)|(} -Isabelle offers an additional definitional facility, -\textbf{syntax translations}. -They resemble macros: upon parsing, the defined concept is immediately -replaced by its definition. This effect is reversed upon printing. For example, -the symbol @{text"\"} is defined via a syntax translation: +text {* + \noindent Here the name of the dummy constant @{text "_sim"} does + not really matter, as long as it is not used otherwise. 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"}. + + \medskip Another useful 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: *} -translations "x \ y" \ "\(x = y)" - -text{*\index{$IsaEqTrans@\isasymrightleftharpoons} -\noindent -Internally, @{text"\"} never appears. +syntax "_not_equal" :: "'a \ 'a \ bool" (infixl "\\" 50) +translations "x \\ y" \ "\ (x = y)" -In addition to @{text"\"} there are -@{text"\"}\index{$IsaEqTrans1@\isasymrightharpoonup} -and @{text"\"}\index{$IsaEqTrans2@\isasymleftharpoondown} -for uni-directional translations, which only affect -parsing or printing. This tutorial will not cover the details of -translations. We have mentioned the concept merely because it -crops up occasionally; a number of HOL's built-in constructs are defined -via translations. Translations are preferable to definitions when the new -concept is a trivial variation on an existing one. For example, we -don't need to derive new theorems about @{text"\"}, since existing theorems -about @{text"="} still apply.% -\index{syntax translations|)}% -\index{translations@\isacommand {translations} (command)|)} +text {* + \noindent Normally one would introduce derived concepts like this + within the logic, using \isakeyword{consts} and \isakeyword{defs} + instead of \isakeyword{syntax} and \isakeyword{translations}. The + present formulation has the virtue that expressions are immediately + replaced by its ``definition'' upon parsing; the effect is reversed + upon printing. Internally, @{text"\"} never appears. + + Simulating definitions via translations is adequate for very basic + variations of fundamental logical concepts, when the new + representation is a trivial variation on an existing one. On the + other hand, syntax translations do not scale up well to large + hierarchies of concepts built on each other. *} -section {* Document Preparation *} +section {* Document Preparation \label{sec:document-prep} *} text {* Isabelle/Isar is centered around a certain notion of \bfindex{formal @@ -424,8 +457,6 @@ subsubsection {* Sections *} text {* - FIXME \verb,\label, within sections; - The large-scale structure of Isabelle documents closely follows {\LaTeX} convention, with chapters, sections, subsubsections etc. The formal Isar language includes separate structure \bfindex{markup @@ -524,6 +555,8 @@ text {* Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,), + FIXME + *} @@ -587,8 +620,44 @@ \medskip - Ignoring portions of printed text like this demands some special - care. FIXME + Text may be suppressed at a very fine grain; thus we may even drop + vital parts of the formal text, preventing that things have been + simpler than in reality. For example, the following ``fully + automatic'' proof is actually a fake: +*} + +lemma "x \ (0::int) \ 0 < x * x" + by (auto(*<*)simp add: int_less_le(*>*)) + +text {* + \noindent Here the real source of the proof has been as follows: + +\begin{verbatim} + by (auto(*<*)simp add: int_less_le(*>*)) +\end{verbatim} %(* + + \medskip Ignoring portions of printed text generally demands some + care by the user. First of all, the writer is responsible not to + obfuscate the underlying formal development in an unduly manner. It + is fairly easy to scramble the remaining visible text by referring + to questionable formal items (strange definitions, arbitrary axioms + etc.) that have been hidden from sight. + + Some minor technical subtleties of the + \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), + elements need to be observed as well, as the system performs little + sanity checks here. Arguments of markup commands and formal + comments must not be hidden, otherwise presentation fails. Open and + close parentheses need to be inserted carefully; it is fairly easy + to hide just the wrong parts, especially after rearranging the + sources. + + \medskip Authentic reports of formal theories, say as part of a + library, should usually refrain from suppressing parts of the text + at all. Other users may need the full information for their own + derivative work. If a particular formalization works out as too + ugly for general public coverage, it is often better to think of a + better way in the first place. *} (*<*)