src/Doc/Tutorial/Documents/Documents.thy

 (*<*)
 theory Documents imports Main begin
 (*>*)
 
-section {* Concrete Syntax \label{sec:concrete-syntax} *}
-
-text {*
+section \<open>Concrete Syntax \label{sec:concrete-syntax}\<close>
+
+text \<open>
   The core concept of Isabelle's framework for concrete syntax is that
   of \bfindex{mixfix annotations}.  Associated with any kind of
   constant declaration, mixfixes affect both the grammar productions
   for the parser and output templates for the pretty printer.
 

   elements, it is particularly important to give new syntactic
   constructs the right precedence.
 
   Below we introduce a few simple syntax declaration
   forms that already cover many common situations fairly well.
-*}
-
-
-subsection {* Infix Annotations *}
-
-text {*
+\<close>
+
+
+subsection \<open>Infix Annotations\<close>
+
+text \<open>
   Syntax annotations may be included wherever constants are declared,
   such as \isacommand{definition} and \isacommand{primrec} --- and also
   \isacommand{datatype}, which declares constructor operations.
   Type-constructors may be annotated as well, although this is less
   frequently encountered in practice (the infix type @{text "\<times>"} comes
   to mind).
 
   Infix declarations\index{infix annotations} provide a useful special
   case of mixfixes.  The following example of the exclusive-or
   operation on boolean values illustrates typical infix declarations.
-*}
+\<close>
 
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
 where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 
-text {*
+text \<open>
   \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
   same expression internally.  Any curried function with at least two
   arguments may be given infix syntax.  For partial applications with
   fewer than two operands, the operator is enclosed in parentheses.
   For instance, @{text xor} without arguments is represented as

   the range of 10--100: the equality infix @{text "="} is centered at
   50; logical connectives (like @{text "\<or>"} and @{text "\<and>"}) are
   below 50; algebraic ones (like @{text "+"} and @{text "*"}) are
   above 50.  User syntax should strive to coexist with common HOL
   forms, or use the mostly unused range 100--900.
-*}
-
-
-subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Mathematical Symbols \label{sec:syntax-symbols}\<close>
+
+text \<open>
   Concrete syntax based on ASCII characters has inherent limitations.
   Mathematical notation demands a larger repertoire of glyphs.
   Several standards of extended character sets have been proposed over
   decades, but none has become universally available so far.  Isabelle
   has its own notion of \bfindex{symbols} as the smallest entities of

   \noindent is recognized as the term @{term "\<forall>\<alpha>\<^sub>1. \<alpha>\<^sub>1 = \<Pi>\<^sub>\<A>"} 
   by Isabelle.
 
   Replacing our previous definition of @{text xor} by the
   following specifies an Isabelle symbol for the new operator:
-*}
+\<close>
 
 (*<*)
 hide_const xor
-setup {* Sign.add_path "version1" *}
+setup \<open>Sign.add_path "version1"\<close>
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 (*<*)
-setup {* Sign.local_path *}
+setup \<open>Sign.local_path\<close>
 (*>*)
 
-text {*
+text \<open>
   It is possible to provide alternative syntax forms
   through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}.  By
   convention, the mode of ``$xsymbols$'' is enabled whenever
   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   consider the following hybrid declaration of @{text xor}:
-*}
+\<close>
 
 (*<*)
 hide_const xor
-setup {* Sign.add_path "version2" *}
+setup \<open>Sign.add_path "version2"\<close>
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
 where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 
 notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
 (*<*)
-setup {* Sign.local_path *}
+setup \<open>Sign.local_path\<close>
 (*>*)
 
-text {*\noindent
+text \<open>\noindent
 The \commdx{notation} command associates a mixfix
 annotation with a known constant.  The print mode specification,
 here @{text "(xsymbols)"}, is optional.
 
 We may now write @{text "A [+] B"} or @{text "A \<oplus> 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 *}
-
-text {*
+symbols displayed during proofs.\<close>
+
+
+subsection \<open>Prefix Annotations\<close>
+
+text \<open>
   Prefix syntax annotations\index{prefix annotation} are another form
   of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or
   priorities --- just some literal syntax.  The following example
   associates common symbols with the constructors of a datatype.
-*}
+\<close>
 
 datatype currency =
     Euro nat    ("\<euro>")
   | Pounds nat  ("\<pounds>")
   | Yen nat     ("\<yen>")
   | Dollar nat  ("$")
 
-text {*
+text \<open>
   \noindent Here the mixfix annotations on the rightmost column happen
   to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
   \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
   that a constructor like @{text Euro} actually is a function @{typ
   "nat \<Rightarrow> currency"}.  The expression @{text "Euro 10"} will be

   subject to our concrete syntax.  This rather simple form already
   achieves conformance with notational standards of the European
   Commission.
 
   Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
-*}
-
-
-subsection {* Abbreviations \label{sec:abbreviations} *}
-
-text{* Mixfix syntax annotations merely decorate particular constant
+\<close>
+
+
+subsection \<open>Abbreviations \label{sec:abbreviations}\<close>
+
+text\<open>Mixfix syntax annotations merely decorate particular constant
 application forms with concrete syntax, for instance replacing
 @{text "xor A B"} by @{text "A \<oplus> B"}.  Occasionally, the relationship
 between some piece of notation and its internal form is more
 complicated.  Here we need \emph{abbreviations}.
 

 simple mechanism for syntactic macros.
 
 A typical use of abbreviations is to introduce relational notation for
 membership in a set of pairs, replacing @{text "(x, y) \<in> sim"} by
 @{text "x \<approx> y"}. We assume that a constant @{text sim } of type
-@{typ"('a \<times> 'a) set"} has been introduced at this point. *}
+@{typ"('a \<times> 'a) set"} has been introduced at this point.\<close>
 (*<*)consts sim :: "('a \<times> 'a) set"(*>*)
 abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<approx>" 50)
 where "x \<approx> y  \<equiv>  (x, y) \<in> sim"
 
-text {* \noindent The given meta-equality is used as a rewrite rule
+text \<open>\noindent The given meta-equality is used as a rewrite rule
 after parsing (replacing \mbox{@{prop"x \<approx> y"}} by @{text"(x,y) \<in>
 sim"}) and before printing (turning @{text"(x,y) \<in> sim"} back into
 \mbox{@{prop"x \<approx> 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 \<noteq>} for negated equalities.  The following declaration
 stems from Isabelle/HOL itself:
-*}
+\<close>
 
 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)
 where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"
 
 notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
 
-text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it
+text \<open>\noindent The notation @{text \<noteq>} is introduced separately to restrict it
 to the \emph{xsymbols} mode.
 
 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

 definitions.
 
 Abbreviations are a simplified form of the general concept of
 \emph{syntax translations}; even heavier transformations may be
 written in ML @{cite "isabelle-isar-ref"}.
-*}
-
-
-section {* Document Preparation \label{sec:document-preparation} *}
-
-text {*
+\<close>
+
+
+section \<open>Document Preparation \label{sec:document-preparation}\<close>
+
+text \<open>
   Isabelle/Isar is centered around the concept of \bfindex{formal
   proof documents}\index{documents|bold}.  The outcome of a formal
   development effort is meant to be a human-readable record, presented
   as browsable PDF file or printed on paper.  The overall document
   structure follows traditional mathematical articles, with sections,

   reports on theory developments with little effort: many technical
   consistency checks are handled by the system.
 
   Here is an example to illustrate the idea of Isabelle document
   preparation.
-*}
-
-text_raw {* \begin{quotation} *}
-
-text {*
+\<close>
+
+text_raw \<open>\begin{quotation}\<close>
+
+text \<open>
   The following datatype definition of @{text "'a bintree"} models
   binary trees with nodes being decorated by elements of type @{typ
   'a}.
-*}
+\<close>
 
 datatype 'a bintree =
      Leaf | Branch 'a  "'a bintree"  "'a bintree"
 
-text {*
+text \<open>
   \noindent The datatype induction rule generated here is of the form
   @{thm [indent = 1, display] bintree.induct [no_vars]}
-*}
-
-text_raw {* \end{quotation} *}
-
-text {*
+\<close>
+
+text_raw \<open>\end{quotation}\<close>
+
+text \<open>
   \noindent The above document output has been produced as follows:
 
   \begin{ttbox}
   text {\ttlbrace}*
     The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}

   \noindent Here we have augmented the theory by formal comments
   (using \isakeyword{text} blocks), the informal parts may again refer
   to formal entities by means of ``antiquotations'' (such as
   \texttt{\at}\verb,{text "'a bintree"}, or
   \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
-*}
-
-
-subsection {* Isabelle Sessions *}
-
-text {*
+\<close>
+
+
+subsection \<open>Isabelle Sessions\<close>
+
+text \<open>
   In contrast to the highly interactive mode of Isabelle/Isar theory
   development, the document preparation stage essentially works in
   batch-mode.  An Isabelle \bfindex{session} consists of a collection
   of source files that may contribute to an output document.  Each
   session is derived from a single parent, usually an object-logic

 
   \medskip Any failure of the document preparation phase in an
   Isabelle batch session leaves the generated sources in their target
   location, identified by the accompanying error message.  This lets
   you trace {\LaTeX} problems with the generated files at hand.
-*}
-
-
-subsection {* Structure Markup *}
-
-text {*
+\<close>
+
+
+subsection \<open>Structure Markup\<close>
+
+text \<open>
   The large-scale structure of Isabelle documents follows existing
   {\LaTeX} conventions, with chapters, sections, subsubsections etc.
   The Isar language includes separate \bfindex{markup commands}, which
   do not affect the formal meaning of a theory (or proof), but result
   in corresponding {\LaTeX} elements.

 
   theorem main: \dots
 
   end
   \end{ttbox}
-*}
-
-
-subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Formal Comments and Antiquotations \label{sec:doc-prep-text}\<close>
+
+text \<open>
   Isabelle \bfindex{source comments}, which are of the form
   \verb,(,\verb,*,~@{text \<dots>}~\verb,*,\verb,),, essentially act like
   white space and do not really contribute to the content.  They
   mainly serve technical purposes to mark certain oddities in the raw
   input text.  In contrast, \bfindex{formal comments} are portions of

   syntax @{cite "isabelle-isar-ref"}; the common form is ``\verb,--,~$text$''
   where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple
   marginal comments may be given at the same time.  Here is a simple
   example:
-*}
+\<close>
 
 lemma "A --> A"
-  -- "a triviality of propositional logic"
-  -- "(should not really bother)"
-  by (rule impI) -- "implicit assumption step involved here"
-
-text {*
+  \<comment> "a triviality of propositional logic"
+  \<comment> "(should not really bother)"
+  by (rule impI) \<comment> "implicit assumption step involved here"
+
+text \<open>
   \noindent The above output has been produced as follows:
 
 \begin{verbatim}
   lemma "A --> A"
     -- "a triviality of propositional logic"

   (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
   mathematical notation in both the formal and informal parts of the
   document very easily, independently of the term language of
   Isabelle.  Manual {\LaTeX} code would leave more control over the
   typesetting, but is also slightly more tedious.
-*}
-
-
-subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Interpretation of Symbols \label{sec:doc-prep-symbols}\<close>
+
+text \<open>
   As has been pointed out before (\S\ref{sec:syntax-symbols}),
   Isabelle symbols are the smallest syntactic entities --- a
   straightforward generalization of ASCII characters.  While Isabelle
   does not impose any interpretation of the infinite collection of
   named symbols, {\LaTeX} documents use canonical glyphs for certain

   example, \verb,\isabellestyle{it}, uses the italics text style to
   mimic the general appearance of the {\LaTeX} math mode; double
   quotes are not printed at all.  The resulting quality of typesetting
   is quite good, so this should be the default style for work that
   gets distributed to a broader audience.
-*}
-
-
-subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Suppressing Output \label{sec:doc-prep-suppress}\<close>
+
+text \<open>
   By default, Isabelle's document system generates a {\LaTeX} file for
   each theory that gets loaded while running the session.  The
   generated \texttt{session.tex} will include all of these in order of
   appearance, which in turn gets included by the standard
   \texttt{root.tex}.  Certainly one may change the order or suppress

   using the predefined tags ``\emph{theory}'' (for theory begin and
   end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
   commands involving ML code).  Users may add their own tags using the
   \verb,%,\emph{tag} notation right after a command name.  In the
   subsequent example we hide a particularly irrelevant proof:
-*}
+\<close>
 
 lemma "x = x" by %invisible (simp)
 
-text {*
+text \<open>
   The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
   Tags observe the structure of proofs; adjacent commands with the
   same tag are joined into a single region.  The Isabelle document
   preparation system allows the user to specify how to interpret a
   tagged region, in order to keep, drop, or fold the corresponding

   \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
   before the type-setting phase, without affecting the formal checking
   of the theory, of course.  For example, we may hide parts of a proof
   that seem unfit for general public inspection.  The following
   ``fully automatic'' proof is actually a fake:
-*}
+\<close>
 
 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
 
-text {*
+text \<open>
   \noindent The real source of the proof has been as follows:
 
 \begin{verbatim}
   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
 \end{verbatim}

 
   \medskip Suppressing portions of printed text demands care.  You
   should not misrepresent the underlying theory development.  It is
   easy to invalidate the visible text by hiding references to
   questionable axioms, for example.
-*}
+\<close>
 
 (*<*)
 end
 (*>*)