doc-src/TutorialI/Documents/Documents.thy
author wenzelm
Sun Oct 09 15:46:06 2011 +0200 (2011-10-09 ago)
changeset 45106 3498077f2012
parent 38765 5aa8e5e770a8
child 47822 34b44d28fc4b
permissions -rw-r--r--
updated ISABELLE_HOME_USER;
wenzelm@11647
     1
(*<*)
haftmann@16417
     2
theory Documents imports Main begin
wenzelm@11647
     3
(*>*)
wenzelm@11647
     4
wenzelm@12648
     5
section {* Concrete Syntax \label{sec:concrete-syntax} *}
wenzelm@12629
     6
wenzelm@12629
     7
text {*
wenzelm@12766
     8
  The core concept of Isabelle's framework for concrete syntax is that
wenzelm@12766
     9
  of \bfindex{mixfix annotations}.  Associated with any kind of
wenzelm@12766
    10
  constant declaration, mixfixes affect both the grammar productions
wenzelm@12766
    11
  for the parser and output templates for the pretty printer.
wenzelm@12629
    12
wenzelm@12743
    13
  In full generality, parser and pretty printer configuration is a
nipkow@25338
    14
  subtle affair~\cite{isabelle-ref}.  Your syntax specifications need
wenzelm@12766
    15
  to interact properly with the existing setup of Isabelle/Pure and
wenzelm@12766
    16
  Isabelle/HOL\@.  To avoid creating ambiguities with existing
wenzelm@12766
    17
  elements, it is particularly important to give new syntactic
paulson@12764
    18
  constructs the right precedence.
wenzelm@12629
    19
nipkow@25338
    20
  Below we introduce a few simple syntax declaration
wenzelm@12743
    21
  forms that already cover many common situations fairly well.
wenzelm@12629
    22
*}
wenzelm@12629
    23
wenzelm@12629
    24
wenzelm@12648
    25
subsection {* Infix Annotations *}
wenzelm@12629
    26
wenzelm@12629
    27
text {*
paulson@12764
    28
  Syntax annotations may be included wherever constants are declared,
nipkow@27015
    29
  such as \isacommand{definition} and \isacommand{primrec} --- and also
wenzelm@12766
    30
  \isacommand{datatype}, which declares constructor operations.
wenzelm@12766
    31
  Type-constructors may be annotated as well, although this is less
wenzelm@12766
    32
  frequently encountered in practice (the infix type @{text "\<times>"} comes
wenzelm@12766
    33
  to mind).
wenzelm@12629
    34
wenzelm@12645
    35
  Infix declarations\index{infix annotations} provide a useful special
wenzelm@12766
    36
  case of mixfixes.  The following example of the exclusive-or
wenzelm@12766
    37
  operation on boolean values illustrates typical infix declarations.
wenzelm@12629
    38
*}
wenzelm@12629
    39
nipkow@27015
    40
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
nipkow@27015
    41
where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
wenzelm@12629
    42
wenzelm@12629
    43
text {*
wenzelm@12653
    44
  \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
wenzelm@12653
    45
  same expression internally.  Any curried function with at least two
wenzelm@12766
    46
  arguments may be given infix syntax.  For partial applications with
wenzelm@12766
    47
  fewer than two operands, there is a notation using the prefix~@{text
wenzelm@12766
    48
  op}.  For instance, @{text xor} without arguments is represented as
wenzelm@12766
    49
  @{text "op [+]"}; together with ordinary function application, this
wenzelm@12653
    50
  turns @{text "xor A"} into @{text "op [+] A"}.
wenzelm@12629
    51
nipkow@25338
    52
  The keyword \isakeyword{infixl} seen above specifies an
wenzelm@12746
    53
  infix operator that is nested to the \emph{left}: in iterated
wenzelm@12746
    54
  applications the more complex expression appears on the left-hand
wenzelm@12766
    55
  side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]
wenzelm@12766
    56
  C"}.  Similarly, \isakeyword{infixr} means nesting to the
wenzelm@12746
    57
  \emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B
wenzelm@12766
    58
  [+] C)"}.  A \emph{non-oriented} declaration via \isakeyword{infix}
wenzelm@12766
    59
  would render @{term "A [+] B [+] C"} illegal, but demand explicit
wenzelm@12766
    60
  parentheses to indicate the intended grouping.
wenzelm@12743
    61
wenzelm@12746
    62
  The string @{text [source] "[+]"} in our annotation refers to the
wenzelm@12746
    63
  concrete syntax to represent the operator (a literal token), while
paulson@12764
    64
  the number @{text 60} determines the precedence of the construct:
wenzelm@12766
    65
  the syntactic priorities of the arguments and result.  Isabelle/HOL
wenzelm@12766
    66
  already uses up many popular combinations of ASCII symbols for its
wenzelm@12766
    67
  own use, including both @{text "+"} and @{text "++"}.  Longer
wenzelm@12766
    68
  character combinations are more likely to be still available for
wenzelm@12766
    69
  user extensions, such as our~@{text "[+]"}.
wenzelm@12629
    70
wenzelm@12766
    71
  Operator precedences have a range of 0--1000.  Very low or high
wenzelm@12766
    72
  priorities are reserved for the meta-logic.  HOL syntax mainly uses
wenzelm@12766
    73
  the range of 10--100: the equality infix @{text "="} is centered at
wenzelm@12766
    74
  50; logical connectives (like @{text "\<or>"} and @{text "\<and>"}) are
wenzelm@12766
    75
  below 50; algebraic ones (like @{text "+"} and @{text "*"}) are
wenzelm@12766
    76
  above 50.  User syntax should strive to coexist with common HOL
wenzelm@12766
    77
  forms, or use the mostly unused range 100--900.
wenzelm@12629
    78
*}
wenzelm@12629
    79
wenzelm@12635
    80
wenzelm@12659
    81
subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
wenzelm@12629
    82
wenzelm@12629
    83
text {*
wenzelm@12766
    84
  Concrete syntax based on ASCII characters has inherent limitations.
wenzelm@12766
    85
  Mathematical notation demands a larger repertoire of glyphs.
wenzelm@12766
    86
  Several standards of extended character sets have been proposed over
wenzelm@12766
    87
  decades, but none has become universally available so far.  Isabelle
wenzelm@12766
    88
  has its own notion of \bfindex{symbols} as the smallest entities of
wenzelm@12766
    89
  source text, without referring to internal encodings.  There are
wenzelm@12766
    90
  three kinds of such ``generalized characters'':
wenzelm@12635
    91
wenzelm@12635
    92
  \begin{enumerate}
wenzelm@12635
    93
wenzelm@12653
    94
  \item 7-bit ASCII characters
wenzelm@12635
    95
wenzelm@12653
    96
  \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
wenzelm@12629
    97
wenzelm@12653
    98
  \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
wenzelm@12635
    99
wenzelm@12635
   100
  \end{enumerate}
wenzelm@12635
   101
kleing@14486
   102
  Here $ident$ is any sequence of letters. 
kleing@14486
   103
  This results in an infinite store of symbols, whose
wenzelm@12766
   104
  interpretation is left to further front-end tools.  For example, the
wenzelm@12766
   105
  user-interface of Proof~General + X-Symbol and the Isabelle document
wenzelm@12766
   106
  processor (see \S\ref{sec:document-preparation}) display the
wenzelm@12766
   107
  \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
wenzelm@12635
   108
wenzelm@12635
   109
  A list of standard Isabelle symbols is given in
wenzelm@28838
   110
  \cite{isabelle-isar-ref}.  You may introduce your own
wenzelm@12635
   111
  interpretation of further symbols by configuring the appropriate
wenzelm@12653
   112
  front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
wenzelm@12653
   113
  macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
wenzelm@12653
   114
  few predefined control symbols, such as \verb,\,\verb,<^sub>, and
wenzelm@12635
   115
  \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
paulson@12764
   116
  printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
wenzelm@12670
   117
  output as @{text "A\<^sup>\<star>"}.
wenzelm@12635
   118
wenzelm@17183
   119
  A number of symbols are considered letters by the Isabelle lexer and
wenzelm@17183
   120
  can be used as part of identifiers. These are the greek letters
wenzelm@17183
   121
  @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}
wenzelm@17183
   122
  (\verb+\+\verb+<beta>+), etc. (excluding @{text "\<lambda>"}),
wenzelm@17183
   123
  special letters like @{text "\<A>"} (\verb+\+\verb+<A>+) and @{text
wenzelm@17183
   124
  "\<AA>"} (\verb+\+\verb+<AA>+), and the control symbols
wenzelm@17183
   125
  \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
wenzelm@17183
   126
  sub and super scripts. This means that the input
kleing@14486
   127
kleing@14486
   128
  \medskip
wenzelm@17183
   129
  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
kleing@14486
   130
kleing@14486
   131
  \medskip
kleing@14486
   132
  \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"} 
wenzelm@17183
   133
  by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single
wenzelm@17183
   134
  syntactic entity, not an exponentiation.
kleing@14486
   135
nipkow@25338
   136
  Replacing our previous definition of @{text xor} by the
wenzelm@17183
   137
  following specifies an Isabelle symbol for the new operator:
wenzelm@12629
   138
*}
wenzelm@12629
   139
wenzelm@12629
   140
(*<*)
wenzelm@36176
   141
hide_const xor
wenzelm@26698
   142
setup {* Sign.add_path "version1" *}
wenzelm@12629
   143
(*>*)
nipkow@27015
   144
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
nipkow@27015
   145
where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
wenzelm@12635
   146
(*<*)
wenzelm@38765
   147
setup {* Sign.local_path *}
wenzelm@12635
   148
(*>*)
wenzelm@12629
   149
wenzelm@12635
   150
text {*
wenzelm@12653
   151
  \noindent The X-Symbol package within Proof~General provides several
wenzelm@12653
   152
  input methods to enter @{text \<oplus>} in the text.  If all fails one may
wenzelm@12766
   153
  just type a named entity \verb,\,\verb,<oplus>, by hand; the
wenzelm@12766
   154
  corresponding symbol will be displayed after further input.
wenzelm@12635
   155
nipkow@25338
   156
  More flexible is to provide alternative syntax forms
wenzelm@12766
   157
  through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
wenzelm@12766
   158
  convention, the mode of ``$xsymbols$'' is enabled whenever
wenzelm@12766
   159
  Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
wenzelm@12766
   160
  consider the following hybrid declaration of @{text xor}:
wenzelm@12635
   161
*}
wenzelm@12635
   162
wenzelm@12635
   163
(*<*)
wenzelm@36176
   164
hide_const xor
wenzelm@26698
   165
setup {* Sign.add_path "version2" *}
wenzelm@12635
   166
(*>*)
nipkow@27015
   167
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
nipkow@27015
   168
where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
wenzelm@12635
   169
nipkow@25338
   170
notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
wenzelm@12629
   171
(*<*)
wenzelm@38765
   172
setup {* Sign.local_path *}
wenzelm@12629
   173
(*>*)
wenzelm@12629
   174
nipkow@27015
   175
text {*\noindent
nipkow@27015
   176
The \commdx{notation} command associates a mixfix
nipkow@27015
   177
annotation with a known constant.  The print mode specification,
nipkow@27015
   178
here @{text "(xsymbols)"}, is optional.
wenzelm@12635
   179
nipkow@25338
   180
We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in input, while
nipkow@25338
   181
output uses the nicer syntax of $xsymbols$ whenever that print mode is
nipkow@25338
   182
active.  Such an arrangement is particularly useful for interactive
nipkow@25338
   183
development, where users may type ASCII text and see mathematical
nipkow@25338
   184
symbols displayed during proofs.  *}
wenzelm@12635
   185
wenzelm@12629
   186
wenzelm@12648
   187
subsection {* Prefix Annotations *}
wenzelm@12629
   188
wenzelm@12629
   189
text {*
wenzelm@12766
   190
  Prefix syntax annotations\index{prefix annotation} are another form
wenzelm@12766
   191
  of mixfixes \cite{isabelle-ref}, without any template arguments or
wenzelm@12766
   192
  priorities --- just some literal syntax.  The following example
wenzelm@12766
   193
  associates common symbols with the constructors of a datatype.
wenzelm@12629
   194
*}
wenzelm@12629
   195
wenzelm@12629
   196
datatype currency =
wenzelm@12629
   197
    Euro nat    ("\<euro>")
wenzelm@12629
   198
  | Pounds nat  ("\<pounds>")
wenzelm@12629
   199
  | Yen nat     ("\<yen>")
wenzelm@12629
   200
  | Dollar nat  ("$")
wenzelm@12629
   201
wenzelm@12629
   202
text {*
wenzelm@12653
   203
  \noindent Here the mixfix annotations on the rightmost column happen
wenzelm@12653
   204
  to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
wenzelm@12653
   205
  \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
wenzelm@12653
   206
  that a constructor like @{text Euro} actually is a function @{typ
wenzelm@12746
   207
  "nat \<Rightarrow> currency"}.  The expression @{text "Euro 10"} will be
wenzelm@12653
   208
  printed as @{term "\<euro> 10"}; only the head of the application is
wenzelm@12743
   209
  subject to our concrete syntax.  This rather simple form already
wenzelm@12743
   210
  achieves conformance with notational standards of the European
wenzelm@12743
   211
  Commission.
wenzelm@12629
   212
nipkow@27015
   213
  Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
wenzelm@12651
   214
*}
wenzelm@12651
   215
wenzelm@12651
   216
nipkow@25338
   217
subsection {* Abbreviations \label{sec:abbreviations} *}
wenzelm@12651
   218
nipkow@25338
   219
text{* Mixfix syntax annotations merely decorate particular constant
nipkow@25338
   220
application forms with concrete syntax, for instance replacing
nipkow@25338
   221
@{text "xor A B"} by @{text "A \<oplus> B"}.  Occasionally, the relationship
nipkow@25338
   222
between some piece of notation and its internal form is more
nipkow@25338
   223
complicated.  Here we need \emph{abbreviations}.
nipkow@25338
   224
nipkow@25338
   225
Command \commdx{abbreviation} introduces an uninterpreted notational
nipkow@25338
   226
constant as an abbreviation for a complex term. Abbreviations are
nipkow@25338
   227
unfolded upon parsing and re-introduced upon printing. This provides a
nipkow@25338
   228
simple mechanism for syntactic macros.
wenzelm@12651
   229
nipkow@25338
   230
A typical use of abbreviations is to introduce relational notation for
nipkow@25338
   231
membership in a set of pairs, replacing @{text "(x, y) \<in> sim"} by
nipkow@27015
   232
@{text "x \<approx> y"}. We assume that a constant @{text sim } of type
nipkow@27015
   233
@{typ"('a \<times> 'a) set"} has been introduced at this point. *}
nipkow@27015
   234
(*<*)consts sim :: "('a \<times> 'a) set"(*>*)
nipkow@25338
   235
abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<approx>" 50)
nipkow@25338
   236
where "x \<approx> y  \<equiv>  (x, y) \<in> sim"
wenzelm@12651
   237
nipkow@25338
   238
text {* \noindent The given meta-equality is used as a rewrite rule
nipkow@25338
   239
after parsing (replacing \mbox{@{prop"x \<approx> y"}} by @{text"(x,y) \<in>
nipkow@25338
   240
sim"}) and before printing (turning @{text"(x,y) \<in> sim"} back into
nipkow@25338
   241
\mbox{@{prop"x \<approx> y"}}). The name of the dummy constant @{text "sim2"}
nipkow@25338
   242
does not matter, as long as it is unique.
nipkow@25338
   243
nipkow@25338
   244
Another common application of abbreviations is to
nipkow@25338
   245
provide variant versions of fundamental relational expressions, such
nipkow@25338
   246
as @{text \<noteq>} for negated equalities.  The following declaration
nipkow@25338
   247
stems from Isabelle/HOL itself:
wenzelm@12635
   248
*}
wenzelm@12635
   249
nipkow@25338
   250
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)
nipkow@25338
   251
where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"
wenzelm@12629
   252
nipkow@25338
   253
notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
nipkow@25338
   254
nipkow@25338
   255
text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it
nipkow@25338
   256
to the \emph{xsymbols} mode.
wenzelm@12651
   257
nipkow@27015
   258
Abbreviations are appropriate when the defined concept is a
nipkow@25338
   259
simple variation on an existing one.  But because of the automatic
nipkow@25338
   260
folding and unfolding of abbreviations, they do not scale up well to
nipkow@25338
   261
large hierarchies of concepts. Abbreviations do not replace
nipkow@25338
   262
definitions.
wenzelm@12629
   263
nipkow@25338
   264
Abbreviations are a simplified form of the general concept of
nipkow@25338
   265
\emph{syntax translations}; even heavier transformations may be
nipkow@25338
   266
written in ML \cite{isabelle-ref}.
wenzelm@12629
   267
*}
wenzelm@12629
   268
wenzelm@12629
   269
wenzelm@12653
   270
section {* Document Preparation \label{sec:document-preparation} *}
wenzelm@12629
   271
wenzelm@12645
   272
text {*
wenzelm@12653
   273
  Isabelle/Isar is centered around the concept of \bfindex{formal
wenzelm@12766
   274
  proof documents}\index{documents|bold}.  The outcome of a formal
wenzelm@12766
   275
  development effort is meant to be a human-readable record, presented
wenzelm@12766
   276
  as browsable PDF file or printed on paper.  The overall document
wenzelm@12766
   277
  structure follows traditional mathematical articles, with sections,
wenzelm@12766
   278
  intermediate explanations, definitions, theorems and proofs.
wenzelm@12629
   279
wenzelm@12645
   280
  \medskip The Isabelle document preparation system essentially acts
wenzelm@12670
   281
  as a front-end to {\LaTeX}.  After checking specifications and
wenzelm@12670
   282
  proofs formally, the theory sources are turned into typesetting
wenzelm@12766
   283
  instructions in a schematic manner.  This lets you write authentic
wenzelm@12766
   284
  reports on theory developments with little effort: many technical
wenzelm@12766
   285
  consistency checks are handled by the system.
wenzelm@12744
   286
wenzelm@12744
   287
  Here is an example to illustrate the idea of Isabelle document
wenzelm@12744
   288
  preparation.
wenzelm@12746
   289
*}
wenzelm@12744
   290
wenzelm@12746
   291
text_raw {* \begin{quotation} *}
wenzelm@12746
   292
wenzelm@12746
   293
text {*
wenzelm@12746
   294
  The following datatype definition of @{text "'a bintree"} models
wenzelm@12746
   295
  binary trees with nodes being decorated by elements of type @{typ
wenzelm@12746
   296
  'a}.
wenzelm@12744
   297
*}
wenzelm@12744
   298
wenzelm@12744
   299
datatype 'a bintree =
wenzelm@12746
   300
     Leaf | Branch 'a  "'a bintree"  "'a bintree"
wenzelm@12744
   301
wenzelm@12744
   302
text {*
wenzelm@12744
   303
  \noindent The datatype induction rule generated here is of the form
wenzelm@12746
   304
  @{thm [indent = 1, display] bintree.induct [no_vars]}
wenzelm@12746
   305
*}
wenzelm@12744
   306
wenzelm@12746
   307
text_raw {* \end{quotation} *}
wenzelm@12746
   308
wenzelm@12746
   309
text {*
wenzelm@12766
   310
  \noindent The above document output has been produced as follows:
wenzelm@12744
   311
wenzelm@12744
   312
  \begin{ttbox}
wenzelm@12744
   313
  text {\ttlbrace}*
wenzelm@12744
   314
    The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
wenzelm@12744
   315
    models binary trees with nodes being decorated by elements
wenzelm@12744
   316
    of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
wenzelm@12744
   317
  *{\ttrbrace}
wenzelm@12744
   318
wenzelm@12744
   319
  datatype 'a bintree =
wenzelm@12744
   320
    Leaf | Branch 'a  "'a bintree"  "'a bintree"
wenzelm@12766
   321
  \end{ttbox}
wenzelm@12766
   322
  \begin{ttbox}
wenzelm@12744
   323
  text {\ttlbrace}*
wenzelm@12744
   324
    {\ttback}noindent The datatype induction rule generated here is
wenzelm@12744
   325
    of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
wenzelm@12744
   326
  *{\ttrbrace}
wenzelm@12766
   327
  \end{ttbox}\vspace{-\medskipamount}
wenzelm@12744
   328
wenzelm@12746
   329
  \noindent Here we have augmented the theory by formal comments
wenzelm@12766
   330
  (using \isakeyword{text} blocks), the informal parts may again refer
wenzelm@12766
   331
  to formal entities by means of ``antiquotations'' (such as
wenzelm@12744
   332
  \texttt{\at}\verb,{text "'a bintree"}, or
wenzelm@12746
   333
  \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
wenzelm@12645
   334
*}
wenzelm@12645
   335
wenzelm@12645
   336
wenzelm@12648
   337
subsection {* Isabelle Sessions *}
wenzelm@12629
   338
wenzelm@12629
   339
text {*
wenzelm@12653
   340
  In contrast to the highly interactive mode of Isabelle/Isar theory
wenzelm@12653
   341
  development, the document preparation stage essentially works in
wenzelm@12670
   342
  batch-mode.  An Isabelle \bfindex{session} consists of a collection
wenzelm@12766
   343
  of source files that may contribute to an output document.  Each
wenzelm@12766
   344
  session is derived from a single parent, usually an object-logic
wenzelm@12766
   345
  image like \texttt{HOL}.  This results in an overall tree structure,
wenzelm@12766
   346
  which is reflected by the output location in the file system
wenzelm@45106
   347
  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
wenzelm@12645
   348
wenzelm@12683
   349
  \medskip The easiest way to manage Isabelle sessions is via
wenzelm@28504
   350
  \texttt{isabelle mkdir} (generates an initial session source setup)
wenzelm@28504
   351
  and \texttt{isabelle make} (run sessions controlled by
wenzelm@12683
   352
  \texttt{IsaMakefile}).  For example, a new session
wenzelm@12683
   353
  \texttt{MySession} derived from \texttt{HOL} may be produced as
wenzelm@12683
   354
  follows:
wenzelm@12683
   355
wenzelm@12683
   356
\begin{verbatim}
wenzelm@28504
   357
  isabelle mkdir HOL MySession
wenzelm@28504
   358
  isabelle make
wenzelm@12683
   359
\end{verbatim}
wenzelm@12683
   360
wenzelm@28504
   361
  The \texttt{isabelle make} job also informs about the file-system
wenzelm@12685
   362
  location of the ultimate results.  The above dry run should be able
wenzelm@12685
   363
  to produce some \texttt{document.pdf} (with dummy title, empty table
wenzelm@12743
   364
  of contents etc.).  Any failure at this stage usually indicates
wenzelm@17183
   365
  technical problems of the {\LaTeX} installation.
wenzelm@12683
   366
wenzelm@12683
   367
  \medskip The detailed arrangement of the session sources is as
wenzelm@12746
   368
  follows.
wenzelm@12645
   369
wenzelm@12645
   370
  \begin{itemize}
wenzelm@12645
   371
wenzelm@12670
   372
  \item Directory \texttt{MySession} holds the required theory files
wenzelm@12670
   373
  $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
wenzelm@12645
   374
wenzelm@12645
   375
  \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
wenzelm@12645
   376
  for loading all wanted theories, usually just
wenzelm@12665
   377
  ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
wenzelm@12670
   378
  dependency graph.
wenzelm@12645
   379
wenzelm@12645
   380
  \item Directory \texttt{MySession/document} contains everything
wenzelm@12653
   381
  required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
wenzelm@12653
   382
  provided initially.
wenzelm@12645
   383
wenzelm@12653
   384
  The latter file holds appropriate {\LaTeX} code to commence a
wenzelm@12653
   385
  document (\verb,\documentclass, etc.), and to include the generated
wenzelm@12743
   386
  files $T@i$\texttt{.tex} for each theory.  Isabelle will generate a
wenzelm@12743
   387
  file \texttt{session.tex} holding {\LaTeX} commands to include all
wenzelm@12746
   388
  generated theory output files in topologically sorted order, so
wenzelm@12746
   389
  \verb,\input{session}, in the body of \texttt{root.tex} does the job
wenzelm@12746
   390
  in most situations.
wenzelm@12653
   391
wenzelm@12681
   392
  \item \texttt{IsaMakefile} holds appropriate dependencies and
wenzelm@12681
   393
  invocations of Isabelle tools to control the batch job.  In fact,
wenzelm@12746
   394
  several sessions may be managed by the same \texttt{IsaMakefile}.
paulson@12764
   395
  See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
paulson@12764
   396
  for further details, especially on
wenzelm@28504
   397
  \texttt{isabelle usedir} and \texttt{isabelle make}.
wenzelm@12645
   398
wenzelm@12645
   399
  \end{itemize}
wenzelm@12645
   400
wenzelm@12685
   401
  One may now start to populate the directory \texttt{MySession}, and
wenzelm@12766
   402
  the file \texttt{MySession/ROOT.ML} accordingly.  The file
wenzelm@12766
   403
  \texttt{MySession/document/root.tex} should also be adapted at some
wenzelm@12685
   404
  point; the default version is mostly self-explanatory.  Note that
wenzelm@12685
   405
  \verb,\isabellestyle, enables fine-tuning of the general appearance
wenzelm@12685
   406
  of characters and mathematical symbols (see also
wenzelm@12685
   407
  \S\ref{sec:doc-prep-symbols}).
wenzelm@12653
   408
wenzelm@12685
   409
  Especially observe the included {\LaTeX} packages \texttt{isabelle}
wenzelm@12685
   410
  (mandatory), \texttt{isabellesym} (required for mathematical
wenzelm@12743
   411
  symbols), and the final \texttt{pdfsetup} (provides sane defaults
paulson@12764
   412
  for \texttt{hyperref}, including URL markup).  All three are
wenzelm@12743
   413
  distributed with Isabelle. Further packages may be required in
paulson@12764
   414
  particular applications, say for unusual mathematical symbols.
wenzelm@12645
   415
wenzelm@12746
   416
  \medskip Any additional files for the {\LaTeX} stage go into the
wenzelm@12746
   417
  \texttt{MySession/document} directory as well.  In particular,
wenzelm@12766
   418
  adding a file named \texttt{root.bib} causes an automatic run of
wenzelm@12766
   419
  \texttt{bibtex} to process a bibliographic database; see also
wenzelm@28504
   420
  \texttt{isabelle document} \cite{isabelle-sys}.
wenzelm@12645
   421
wenzelm@12653
   422
  \medskip Any failure of the document preparation phase in an
wenzelm@12670
   423
  Isabelle batch session leaves the generated sources in their target
wenzelm@12766
   424
  location, identified by the accompanying error message.  This lets
wenzelm@12766
   425
  you trace {\LaTeX} problems with the generated files at hand.
wenzelm@12645
   426
*}
wenzelm@12645
   427
wenzelm@12645
   428
wenzelm@12648
   429
subsection {* Structure Markup *}
wenzelm@12645
   430
wenzelm@12653
   431
text {*
wenzelm@12653
   432
  The large-scale structure of Isabelle documents follows existing
wenzelm@12653
   433
  {\LaTeX} conventions, with chapters, sections, subsubsections etc.
wenzelm@12653
   434
  The Isar language includes separate \bfindex{markup commands}, which
wenzelm@12681
   435
  do not affect the formal meaning of a theory (or proof), but result
wenzelm@12665
   436
  in corresponding {\LaTeX} elements.
wenzelm@12645
   437
wenzelm@12665
   438
  There are separate markup commands depending on the textual context:
wenzelm@12665
   439
  in header position (just before \isakeyword{theory}), within the
wenzelm@12665
   440
  theory body, or within a proof.  The header needs to be treated
wenzelm@12665
   441
  specially here, since ordinary theory and proof commands may only
wenzelm@12665
   442
  occur \emph{after} the initial \isakeyword{theory} specification.
wenzelm@12645
   443
wenzelm@12665
   444
  \medskip
wenzelm@12645
   445
wenzelm@12645
   446
  \begin{tabular}{llll}
wenzelm@12645
   447
  header & theory & proof & default meaning \\\hline
wenzelm@12645
   448
    & \commdx{chapter} & & \verb,\chapter, \\
wenzelm@12645
   449
  \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
wenzelm@12645
   450
    & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
wenzelm@12645
   451
    & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
wenzelm@12645
   452
  \end{tabular}
wenzelm@12645
   453
wenzelm@12645
   454
  \medskip
wenzelm@12645
   455
wenzelm@12645
   456
  From the Isabelle perspective, each markup command takes a single
wenzelm@12746
   457
  $text$ argument (delimited by \verb,",~@{text \<dots>}~\verb,", or
wenzelm@12746
   458
  \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},).  After stripping any
wenzelm@12645
   459
  surrounding white space, the argument is passed to a {\LaTeX} macro
wenzelm@12766
   460
  \verb,\isamarkupXYZ, for command \isakeyword{XYZ}.  These macros are
wenzelm@12766
   461
  defined in \verb,isabelle.sty, according to the meaning given in the
wenzelm@12766
   462
  rightmost column above.
wenzelm@12645
   463
wenzelm@12645
   464
  \medskip The following source fragment illustrates structure markup
wenzelm@12653
   465
  of a theory.  Note that {\LaTeX} labels may be included inside of
wenzelm@12653
   466
  section headings as well.
wenzelm@12645
   467
wenzelm@12645
   468
  \begin{ttbox}
wenzelm@12645
   469
  header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
wenzelm@12645
   470
nipkow@15136
   471
  theory Foo_Bar
nipkow@15141
   472
  imports Main
nipkow@15136
   473
  begin
wenzelm@12645
   474
wenzelm@12645
   475
  subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
wenzelm@12645
   476
nipkow@27027
   477
  definition foo :: \dots
wenzelm@12648
   478
nipkow@27027
   479
  definition bar :: \dots
wenzelm@12648
   480
wenzelm@12645
   481
  subsection {\ttlbrace}* Derived rules *{\ttrbrace}
wenzelm@12645
   482
wenzelm@12645
   483
  lemma fooI: \dots
wenzelm@12645
   484
  lemma fooE: \dots
wenzelm@12645
   485
wenzelm@12648
   486
  subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
wenzelm@12645
   487
wenzelm@12645
   488
  theorem main: \dots
wenzelm@12645
   489
wenzelm@12645
   490
  end
wenzelm@12766
   491
  \end{ttbox}\vspace{-\medskipamount}
wenzelm@12645
   492
wenzelm@12766
   493
  You may occasionally want to change the meaning of markup commands,
wenzelm@12766
   494
  say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
wenzelm@12766
   495
  \verb,\isamarkupheader, is a good candidate for some tuning.  We
wenzelm@12766
   496
  could move it up in the hierarchy to become \verb,\chapter,.
wenzelm@12645
   497
wenzelm@12645
   498
\begin{verbatim}
wenzelm@12645
   499
  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
wenzelm@12645
   500
\end{verbatim}
wenzelm@12645
   501
wenzelm@12766
   502
  \noindent Now we must change the document class given in
wenzelm@12766
   503
  \texttt{root.tex} to something that supports chapters.  A suitable
wenzelm@12766
   504
  command is \verb,\documentclass{report},.
wenzelm@12645
   505
wenzelm@12648
   506
  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
wenzelm@12648
   507
  hold the name of the current theory context.  This is particularly
wenzelm@12653
   508
  useful for document headings:
wenzelm@12645
   509
wenzelm@12645
   510
\begin{verbatim}
wenzelm@12653
   511
  \renewcommand{\isamarkupheader}[1]
wenzelm@12645
   512
  {\chapter{#1}\markright{THEORY~\isabellecontext}}
wenzelm@12645
   513
\end{verbatim}
wenzelm@12645
   514
wenzelm@12645
   515
  \noindent Make sure to include something like
wenzelm@12648
   516
  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
paulson@12764
   517
  should have more than two pages to show the effect.
wenzelm@12645
   518
*}
wenzelm@12645
   519
wenzelm@12645
   520
wenzelm@12744
   521
subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}
wenzelm@12645
   522
wenzelm@12645
   523
text {*
wenzelm@12744
   524
  Isabelle \bfindex{source comments}, which are of the form
wenzelm@12746
   525
  \verb,(,\verb,*,~@{text \<dots>}~\verb,*,\verb,),, essentially act like
wenzelm@12746
   526
  white space and do not really contribute to the content.  They
wenzelm@12746
   527
  mainly serve technical purposes to mark certain oddities in the raw
wenzelm@12746
   528
  input text.  In contrast, \bfindex{formal comments} are portions of
wenzelm@12746
   529
  text that are associated with formal Isabelle/Isar commands
wenzelm@12681
   530
  (\bfindex{marginal comments}), or as standalone paragraphs within a
wenzelm@12665
   531
  theory or proof context (\bfindex{text blocks}).
wenzelm@12659
   532
wenzelm@12659
   533
  \medskip Marginal comments are part of each command's concrete
wenzelm@12670
   534
  syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
wenzelm@12746
   535
  where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
wenzelm@12746
   536
  \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple
wenzelm@12670
   537
  marginal comments may be given at the same time.  Here is a simple
wenzelm@12670
   538
  example:
wenzelm@12665
   539
*}
wenzelm@12665
   540
wenzelm@12665
   541
lemma "A --> A"
wenzelm@12665
   542
  -- "a triviality of propositional logic"
wenzelm@12665
   543
  -- "(should not really bother)"
wenzelm@12665
   544
  by (rule impI) -- "implicit assumption step involved here"
wenzelm@12665
   545
wenzelm@12665
   546
text {*
wenzelm@12665
   547
  \noindent The above output has been produced as follows:
wenzelm@12659
   548
wenzelm@12659
   549
\begin{verbatim}
wenzelm@12659
   550
  lemma "A --> A"
wenzelm@12659
   551
    -- "a triviality of propositional logic"
wenzelm@12659
   552
    -- "(should not really bother)"
wenzelm@12659
   553
    by (rule impI) -- "implicit assumption step involved here"
wenzelm@12659
   554
\end{verbatim}
wenzelm@12659
   555
wenzelm@12670
   556
  From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
wenzelm@12670
   557
  command, associated with the macro \verb,\isamarkupcmt, (taking a
wenzelm@12670
   558
  single argument).
wenzelm@12659
   559
wenzelm@12665
   560
  \medskip Text blocks are introduced by the commands \bfindex{text}
wenzelm@12665
   561
  and \bfindex{txt}, for theory and proof contexts, respectively.
wenzelm@12665
   562
  Each takes again a single $text$ argument, which is interpreted as a
wenzelm@12665
   563
  free-form paragraph in {\LaTeX} (surrounded by some additional
wenzelm@12670
   564
  vertical space).  This behavior may be changed by redefining the
wenzelm@12670
   565
  {\LaTeX} environments of \verb,isamarkuptext, or
wenzelm@12670
   566
  \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
wenzelm@12670
   567
  text style of the body is determined by \verb,\isastyletext, and
wenzelm@12670
   568
  \verb,\isastyletxt,; the default setup uses a smaller font within
wenzelm@12746
   569
  proofs.  This may be changed as follows:
wenzelm@12746
   570
wenzelm@12746
   571
\begin{verbatim}
wenzelm@12746
   572
  \renewcommand{\isastyletxt}{\isastyletext}
wenzelm@12746
   573
\end{verbatim}
wenzelm@12659
   574
wenzelm@12766
   575
  \medskip The $text$ part of Isabelle markup commands essentially
wenzelm@12766
   576
  inserts \emph{quoted material} into a formal text, mainly for
wenzelm@12766
   577
  instruction of the reader.  An \bfindex{antiquotation} is again a
wenzelm@12766
   578
  formal object embedded into such an informal portion.  The
wenzelm@12766
   579
  interpretation of antiquotations is limited to some well-formedness
wenzelm@12766
   580
  checks, with the result being pretty printed to the resulting
wenzelm@12766
   581
  document.  Quoted text blocks together with antiquotations provide
wenzelm@12766
   582
  an attractive means of referring to formal entities, with good
wenzelm@12766
   583
  confidence in getting the technical details right (especially syntax
wenzelm@12766
   584
  and types).
wenzelm@12659
   585
wenzelm@12665
   586
  The general syntax of antiquotations is as follows:
wenzelm@12659
   587
  \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
wenzelm@12659
   588
  \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
wenzelm@12665
   589
  for a comma-separated list of options consisting of a $name$ or
wenzelm@12766
   590
  \texttt{$name$=$value$} each.  The syntax of $arguments$ depends on
wenzelm@12766
   591
  the kind of antiquotation, it generally follows the same conventions
wenzelm@12766
   592
  for types, terms, or theorems as in the formal part of a theory.
wenzelm@12645
   593
wenzelm@12766
   594
  \medskip This sentence demonstrates quotations and antiquotations:
wenzelm@12766
   595
  @{term "%x y. x"} is a well-typed term.
wenzelm@12659
   596
paulson@12764
   597
  \medskip\noindent The output above was produced as follows:
wenzelm@12659
   598
  \begin{ttbox}
wenzelm@12659
   599
text {\ttlbrace}*
paulson@12764
   600
  This sentence demonstrates quotations and antiquotations:
wenzelm@12659
   601
  {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
wenzelm@12659
   602
*{\ttrbrace}
wenzelm@12766
   603
  \end{ttbox}\vspace{-\medskipamount}
wenzelm@12659
   604
paulson@12764
   605
  The notational change from the ASCII character~\verb,%, to the
wenzelm@12766
   606
  symbol~@{text \<lambda>} reveals that Isabelle printed this term, after
wenzelm@12766
   607
  parsing and type-checking.  Document preparation enables symbolic
wenzelm@12766
   608
  output by default.
wenzelm@12659
   609
nipkow@16523
   610
  \medskip The next example includes an option to show the type of all
nipkow@16523
   611
  variables.  The antiquotation
wenzelm@12766
   612
  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
wenzelm@12766
   613
  output @{term [show_types] "%x y. x"}.  Type inference has figured
wenzelm@12766
   614
  out the most general typings in the present theory context.  Terms
wenzelm@12766
   615
  may acquire different typings due to constraints imposed by their
wenzelm@12766
   616
  environment; within a proof, for example, variables are given the
wenzelm@12766
   617
  same types as they have in the main goal statement.
wenzelm@12659
   618
paulson@12764
   619
  \medskip Several further kinds of antiquotations and options are
nipkow@30649
   620
  available \cite{isabelle-isar-ref}.  Here are a few commonly used
wenzelm@12670
   621
  combinations:
wenzelm@12659
   622
wenzelm@12659
   623
  \medskip
wenzelm@12651
   624
wenzelm@12659
   625
  \begin{tabular}{ll}
wenzelm@12659
   626
  \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
nipkow@25338
   627
  \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
wenzelm@12659
   628
  \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
wenzelm@12659
   629
  \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
wenzelm@12665
   630
  \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
wenzelm@12659
   631
  \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
wenzelm@12659
   632
  \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
wenzelm@12659
   633
  \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
wenzelm@12746
   634
  \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
wenzelm@12659
   635
  \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
wenzelm@12659
   636
  \end{tabular}
wenzelm@12659
   637
wenzelm@12659
   638
  \medskip
wenzelm@12659
   639
wenzelm@12665
   640
  Note that \attrdx{no_vars} given above is \emph{not} an
wenzelm@12665
   641
  antiquotation option, but an attribute of the theorem argument given
wenzelm@12665
   642
  here.  This might be useful with a diagnostic command like
wenzelm@12665
   643
  \isakeyword{thm}, too.
wenzelm@12659
   644
wenzelm@12665
   645
  \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
wenzelm@12659
   646
  particularly interesting.  Embedding uninterpreted text within an
wenzelm@12665
   647
  informal body might appear useless at first sight.  Here the key
wenzelm@12665
   648
  virtue is that the string $s$ is processed as Isabelle output,
wenzelm@12665
   649
  interpreting Isabelle symbols appropriately.
wenzelm@12659
   650
wenzelm@12665
   651
  For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces @{text
wenzelm@12665
   652
  "\<forall>\<exists>"}, according to the standard interpretation of these symbol
wenzelm@12665
   653
  (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
wenzelm@12659
   654
  mathematical notation in both the formal and informal parts of the
wenzelm@12766
   655
  document very easily, independently of the term language of
wenzelm@12766
   656
  Isabelle.  Manual {\LaTeX} code would leave more control over the
wenzelm@12766
   657
  typesetting, but is also slightly more tedious.
wenzelm@12645
   658
*}
wenzelm@12645
   659
wenzelm@12645
   660
wenzelm@12674
   661
subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
wenzelm@12645
   662
wenzelm@12645
   663
text {*
wenzelm@12665
   664
  As has been pointed out before (\S\ref{sec:syntax-symbols}),
wenzelm@12670
   665
  Isabelle symbols are the smallest syntactic entities --- a
wenzelm@12681
   666
  straightforward generalization of ASCII characters.  While Isabelle
wenzelm@12665
   667
  does not impose any interpretation of the infinite collection of
paulson@12764
   668
  named symbols, {\LaTeX} documents use canonical glyphs for certain
wenzelm@28838
   669
  standard symbols \cite{isabelle-isar-ref}.
wenzelm@12659
   670
wenzelm@12766
   671
  The {\LaTeX} code produced from Isabelle text follows a simple
wenzelm@12766
   672
  scheme.  You can tune the final appearance by redefining certain
wenzelm@12766
   673
  macros, say in \texttt{root.tex} of the document.
wenzelm@12670
   674
wenzelm@12670
   675
  \begin{enumerate}
wenzelm@12659
   676
wenzelm@12670
   677
  \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
wenzelm@12746
   678
  \texttt{a\dots z} are output directly, digits are passed as an
wenzelm@12670
   679
  argument to the \verb,\isadigit, macro, other characters are
wenzelm@12670
   680
  replaced by specifically named macros of the form
wenzelm@12665
   681
  \verb,\isacharXYZ,.
wenzelm@12659
   682
wenzelm@12766
   683
  \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
wenzelm@12766
   684
  \verb,{\isasymXYZ},; note the additional braces.
wenzelm@12659
   685
wenzelm@12766
   686
  \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
wenzelm@12766
   687
  \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
wenzelm@12766
   688
  control macro is defined accordingly.
wenzelm@12670
   689
wenzelm@12659
   690
  \end{enumerate}
wenzelm@12665
   691
paulson@12764
   692
  You may occasionally wish to give new {\LaTeX} interpretations of
paulson@12764
   693
  named symbols.  This merely requires an appropriate definition of
wenzelm@12766
   694
  \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
wenzelm@12746
   695
  \texttt{isabelle.sty} for working examples).  Control symbols are
wenzelm@12746
   696
  slightly more difficult to get right, though.
wenzelm@12665
   697
wenzelm@12665
   698
  \medskip The \verb,\isabellestyle, macro provides a high-level
wenzelm@12665
   699
  interface to tune the general appearance of individual symbols.  For
wenzelm@12670
   700
  example, \verb,\isabellestyle{it}, uses the italics text style to
wenzelm@12670
   701
  mimic the general appearance of the {\LaTeX} math mode; double
wenzelm@12743
   702
  quotes are not printed at all.  The resulting quality of typesetting
wenzelm@12743
   703
  is quite good, so this should be the default style for work that
wenzelm@12743
   704
  gets distributed to a broader audience.
wenzelm@12645
   705
*}
wenzelm@12645
   706
wenzelm@12645
   707
wenzelm@12653
   708
subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
wenzelm@12645
   709
wenzelm@12645
   710
text {*
wenzelm@12748
   711
  By default, Isabelle's document system generates a {\LaTeX} file for
wenzelm@12748
   712
  each theory that gets loaded while running the session.  The
wenzelm@12748
   713
  generated \texttt{session.tex} will include all of these in order of
wenzelm@12748
   714
  appearance, which in turn gets included by the standard
wenzelm@12743
   715
  \texttt{root.tex}.  Certainly one may change the order or suppress
wenzelm@12746
   716
  unwanted theories by ignoring \texttt{session.tex} and load
wenzelm@12746
   717
  individual files directly in \texttt{root.tex}.  On the other hand,
wenzelm@12746
   718
  such an arrangement requires additional maintenance whenever the
wenzelm@12746
   719
  collection of theories changes.
wenzelm@12648
   720
wenzelm@12648
   721
  Alternatively, one may tune the theory loading process in
wenzelm@12653
   722
  \texttt{ROOT.ML} itself: traversal of the theory dependency graph
wenzelm@12670
   723
  may be fine-tuned by adding \verb,use_thy, invocations, although
wenzelm@12670
   724
  topological sorting still has to be observed.  Moreover, the ML
wenzelm@12670
   725
  operator \verb,no_document, temporarily disables document generation
wenzelm@12766
   726
  while executing a theory loader command.  Its usage is like this:
wenzelm@12648
   727
wenzelm@12648
   728
\begin{verbatim}
wenzelm@12665
   729
  no_document use_thy "T";
wenzelm@12648
   730
\end{verbatim}
wenzelm@12645
   731
wenzelm@17183
   732
  \medskip Theory output may be suppressed more selectively, either
wenzelm@17183
   733
  via \bfindex{tagged command regions} or \bfindex{ignored material}.
wenzelm@12648
   734
wenzelm@17183
   735
  Tagged command regions works by annotating commands with named tags,
wenzelm@17183
   736
  which correspond to certain {\LaTeX} markup that tells how to treat
wenzelm@17183
   737
  particular parts of a document when doing the actual type-setting.
wenzelm@17183
   738
  By default, certain Isabelle/Isar commands are implicitly marked up
wenzelm@17183
   739
  using the predefined tags ``\emph{theory}'' (for theory begin and
wenzelm@17183
   740
  end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
wenzelm@17183
   741
  commands involving ML code).  Users may add their own tags using the
wenzelm@17183
   742
  \verb,%,\emph{tag} notation right after a command name.  In the
wenzelm@17183
   743
  subsequent example we hide a particularly irrelevant proof:
wenzelm@17183
   744
*}
wenzelm@12648
   745
wenzelm@17183
   746
lemma "x = x" by %invisible (simp)
wenzelm@12648
   747
wenzelm@17183
   748
text {*
wenzelm@17183
   749
  The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
wenzelm@17183
   750
  Tags observe the structure of proofs; adjacent commands with the
wenzelm@17183
   751
  same tag are joined into a single region.  The Isabelle document
wenzelm@17183
   752
  preparation system allows the user to specify how to interpret a
wenzelm@17183
   753
  tagged region, in order to keep, drop, or fold the corresponding
wenzelm@17183
   754
  parts of the document.  See the \emph{Isabelle System Manual}
wenzelm@17183
   755
  \cite{isabelle-sys} for further details, especially on
wenzelm@28504
   756
  \texttt{isabelle usedir} and \texttt{isabelle document}.
wenzelm@12648
   757
wenzelm@17183
   758
  Ignored material is specified by delimiting the original formal
wenzelm@17183
   759
  source with special source comments
wenzelm@17183
   760
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
wenzelm@17183
   761
  \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
wenzelm@17183
   762
  before the type-setting phase, without affecting the formal checking
wenzelm@17183
   763
  of the theory, of course.  For example, we may hide parts of a proof
wenzelm@17183
   764
  that seem unfit for general public inspection.  The following
wenzelm@17183
   765
  ``fully automatic'' proof is actually a fake:
wenzelm@12651
   766
*}
wenzelm@12651
   767
wenzelm@12651
   768
lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
paulson@14353
   769
  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
wenzelm@12651
   770
wenzelm@12651
   771
text {*
wenzelm@17183
   772
  \noindent The real source of the proof has been as follows:
wenzelm@12651
   773
wenzelm@12651
   774
\begin{verbatim}
paulson@14353
   775
  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
wenzelm@12659
   776
\end{verbatim}
wenzelm@12659
   777
%(*
wenzelm@12651
   778
wenzelm@12766
   779
  \medskip Suppressing portions of printed text demands care.  You
wenzelm@12766
   780
  should not misrepresent the underlying theory development.  It is
wenzelm@12766
   781
  easy to invalidate the visible text by hiding references to
wenzelm@17183
   782
  questionable axioms, for example.
wenzelm@12629
   783
*}
wenzelm@12629
   784
wenzelm@11647
   785
(*<*)
wenzelm@11647
   786
end
wenzelm@11647
   787
(*>*)