--- a/doc-src/TutorialI/Documents/Documents.thy Fri Jan 04 19:20:42 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Fri Jan 04 19:21:15 2002 +0100
@@ -2,6 +2,213 @@
theory Documents = Main:
(*>*)
+section {* Concrete syntax \label{sec:concrete-syntax} *}
+
+text {*
+ Concerning Isabelle's ``inner'' language of simply-typed @{text
+ \<lambda>}-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.
+*}
+
+
+subsection {* Infixes *}
+
+text {*
+ 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
+ (@{text "*"} and @{text "+"} 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.
+*}
+
+constdefs
+ xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
+ "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
+
+text {*
+ Any curried function with at least two arguments may be associated
+ with infix syntax: @{text "xor A B"} and @{text "A [+] B"} refer to
+ the same expression internally. In partial applications with less
+ than two operands there is a special notation with \isa{op} prefix:
+ @{text xor} without arguments is represented as @{text "op [+]"};
+ combined with plain prefix application this turns @{text "xor A"}
+ into @{text "op [+] A"}.
+
+ \medskip The string @{text [source] "[+]"} in the above declaration
+ refers to the bit of concrete syntax to represent the operator,
+ while the number @{text 60} 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 @{text "+"} and
+ @{text "++"}. Slightly more awkward combinations like the present
+ @{text "[+]"} 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 @{text "="} is
+ centered at 50, logical connectives (like @{text "\<or>"} and @{text
+ "\<and>"}) are below 50, and algebraic ones (like @{text "+"} and @{text
+ "*"}) 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: @{term "A [+] B
+ [+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly,
+ \isakeyword{infixr} refers to nesting to the \emph{right}, which
+ would turn @{term "A [+] B [+] C"} into @{text "A [+] (B [+] C)"}.
+ 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.
+*}
+
+lemma xor_assoc: "(A [+] B) [+] C = A [+] (B [+] C)"
+ by (auto simp add: xor_def)
+
+text {*
+ Such rules may be used in simplification to regroup nested
+ expressions as required. Note that the system would actually print
+ the above statement as @{term "A [+] B [+] C = A [+] (B [+] C)"}
+ (due to nesting to the left). We have preferred to give the fully
+ parenthesized form in the text for clarity.
+*}
+
+(*<*)(*FIXME*)
+subsection {* Mathematical symbols \label{sec:thy-present-symbols} *}
+
+text {*
+ The limitations of the ASCII character set pose a serious
+ limitations for representing mathematical notation. Even worse
+ many handsome combinations have already been used up by HOL
+ itself. Luckily, Isabelle supports infinitely many \emph{named
+ symbols}. FIXME
+
+*}
+
+(*<*)
+hide const xor
+ML_setup {* Context.>> (Theory.add_path "1") *}
+(*>*)
+constdefs
+ xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
+ "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
+
+(*<*)
+local
+(*>*)
+
+
+subsection {* Prefixes *}
+
+text {*
+ Prefix declarations are an even more degenerate form of mixfix
+ annotation, which allow a arbitrary symbolic token to be used for FIXME
+*}
+
+datatype currency =
+ Euro nat ("\<euro>")
+ | Pounds nat ("\<pounds>")
+ | Yen nat ("\<yen>")
+ | Dollar nat ("$")
+
+text {*
+ FIXME The predefined Isabelle symbols used above are \verb,\<euro>,,
+ \verb,\<pounds>,, \verb,\<yen>,, and \verb,\<dollar>,.
+
+ The above syntax annotation makes \verb,\<euro>, stand for the
+ datatype constructor constant @{text Euro}, which happens to be a
+ function @{typ "nat \<Rightarrow> currency"}. Using plain application syntax
+ we may write @{text "Euro 10"} as @{term "\<euro> 10"}. So we already
+ achieve a decent syntactic representation without having to consider
+ arguments and precedences of general mixfix annotations -- prefixes
+ are already sufficient.
+*}
+
+
+subsection {* Syntax translations \label{sec:def-translations} *}
+
+text{*
+ FIXME
+
+\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"\<noteq>"} is defined via a syntax translation:
+*}
+
+translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
+
+text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
+\noindent
+Internally, @{text"\<noteq>"} never appears.
+
+In addition to @{text"\<rightleftharpoons>"} there are
+@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and @{text"\<leftharpoondown>"}\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"\<noteq>"}, since existing theorems
+about @{text"="} still apply.%
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}
+*}
+
+
+section {* Document preparation *}
+
+subsection {* Batch-mode sessions *}
+
+subsection {* {\LaTeX} macros *}
+
+subsubsection {* Structure markup *}
+
+subsubsection {* Symbols and characters *}
+
+text {*
+ FIXME
+
+
+*}
+
(*<*)
end
(*>*)
+(*>*)