doc-src/TutorialI/Documents/Documents.thy
author wenzelm
Tue, 08 Jan 2002 17:51:56 +0100
changeset 12673 90568836340a
parent 12672 f85386e8acdf
child 12674 106d62d106fc
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11647
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
     1
(*<*)
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
     2
theory Documents = Main:
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
     3
(*>*)
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
     4
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
     5
section {* Concrete Syntax \label{sec:concrete-syntax} *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
     6
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
     7
text {*
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
     8
  Concerning Isabelle's ``inner'' language of simply-typed @{text
12653
wenzelm
parents: 12651
diff changeset
     9
  \<lambda>}-calculus, the core concept of Isabelle's elaborate
wenzelm
parents: 12651
diff changeset
    10
  infrastructure for concrete syntax is that of general
wenzelm
parents: 12651
diff changeset
    11
  \bfindex{mixfix annotations}.  Associated with any kind of constant
wenzelm
parents: 12651
diff changeset
    12
  declaration, mixfixes affect both the grammar productions for the
wenzelm
parents: 12651
diff changeset
    13
  parser and output templates for the pretty printer.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    14
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    15
  In full generality, the whole affair of parser and pretty printer
12670
wenzelm
parents: 12665
diff changeset
    16
  configuration is rather subtle, see also \cite{isabelle-ref}.
wenzelm
parents: 12665
diff changeset
    17
  Syntax specifications given by end-users need to interact properly
12665
wenzelm
parents: 12659
diff changeset
    18
  with the existing setup of Isabelle/Pure and Isabelle/HOL.  It is
wenzelm
parents: 12659
diff changeset
    19
  particularly important to get the precedence of new syntactic
wenzelm
parents: 12659
diff changeset
    20
  constructs right, avoiding ambiguities with existing elements.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    21
12670
wenzelm
parents: 12665
diff changeset
    22
  \medskip Subsequently we introduce a few simple syntax declaration
wenzelm
parents: 12665
diff changeset
    23
  forms that already cover most common situations fairly well.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    24
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    25
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    26
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
    27
subsection {* Infix Annotations *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    28
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    29
text {*
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    30
  Syntax annotations may be included wherever constants are declared
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    31
  directly or indirectly, including \isacommand{consts},
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    32
  \isacommand{constdefs}, or \isacommand{datatype} (for the
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    33
  constructor operations).  Type-constructors may be annotated as
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    34
  well, although this is less frequently encountered in practice
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    35
  (@{text "*"} and @{text "+"} types may come to mind).
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    36
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
    37
  Infix declarations\index{infix annotations} provide a useful special
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
    38
  case of mixfixes, where users need not care about the full details
12665
wenzelm
parents: 12659
diff changeset
    39
  of priorities, nesting, spacing, etc.  The following example of the
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
    40
  exclusive-or operation on boolean values illustrates typical infix
12653
wenzelm
parents: 12651
diff changeset
    41
  declarations arising in practice.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    42
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    43
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    44
constdefs
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    45
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    46
  "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    47
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    48
text {*
12653
wenzelm
parents: 12651
diff changeset
    49
  \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
wenzelm
parents: 12651
diff changeset
    50
  same expression internally.  Any curried function with at least two
wenzelm
parents: 12651
diff changeset
    51
  arguments may be associated with infix syntax.  For partial
wenzelm
parents: 12651
diff changeset
    52
  applications with less than two operands there is a special notation
wenzelm
parents: 12651
diff changeset
    53
  with \isa{op} prefix: @{text xor} without arguments is represented
wenzelm
parents: 12651
diff changeset
    54
  as @{text "op [+]"}; together with plain prefix application this
wenzelm
parents: 12651
diff changeset
    55
  turns @{text "xor A"} into @{text "op [+] A"}.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    56
12653
wenzelm
parents: 12651
diff changeset
    57
  \medskip The string @{text [source] "[+]"} in the above annotation
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    58
  refers to the bit of concrete syntax to represent the operator,
12653
wenzelm
parents: 12651
diff changeset
    59
  while the number @{text 60} determines the precedence of the
wenzelm
parents: 12651
diff changeset
    60
  construct (i.e.\ the syntactic priorities of the arguments and
wenzelm
parents: 12651
diff changeset
    61
  result).
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    62
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    63
  As it happens, Isabelle/HOL already spends many popular combinations
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    64
  of ASCII symbols for its own use, including both @{text "+"} and
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    65
  @{text "++"}.  Slightly more awkward combinations like the present
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    66
  @{text "[+]"} tend to be available for user extensions.  The current
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    67
  arrangement of inner syntax may be inspected via
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    68
  \commdx{print\protect\_syntax}, albeit its output is enormous.
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    69
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    70
  Operator precedence also needs some special considerations.  The
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    71
  admissible range is 0--1000.  Very low or high priorities are
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    72
  basically reserved for the meta-logic.  Syntax of Isabelle/HOL
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    73
  mainly uses the range of 10--100: the equality infix @{text "="} is
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    74
  centered at 50, logical connectives (like @{text "\<or>"} and @{text
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    75
  "\<and>"}) are below 50, and algebraic ones (like @{text "+"} and @{text
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    76
  "*"}) above 50.  User syntax should strive to coexist with common
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    77
  HOL forms, or use the mostly unused range 100--900.
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    78
12670
wenzelm
parents: 12665
diff changeset
    79
  The keyword \isakeyword{infixl} specifies an infix operator that is
wenzelm
parents: 12665
diff changeset
    80
  nested to the \emph{left}: in iterated applications the more complex
12665
wenzelm
parents: 12659
diff changeset
    81
  expression appears on the left-hand side: @{term "A [+] B [+] C"}
wenzelm
parents: 12659
diff changeset
    82
  stands for @{text "(A [+] B) [+] C"}.  Similarly,
12653
wenzelm
parents: 12651
diff changeset
    83
  \isakeyword{infixr} specifies to nesting to the \emph{right},
wenzelm
parents: 12651
diff changeset
    84
  reading @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}.  In
wenzelm
parents: 12651
diff changeset
    85
  contrast, a \emph{non-oriented} declaration via \isakeyword{infix}
12670
wenzelm
parents: 12665
diff changeset
    86
  would render @{term "A [+] B [+] C"} illegal, but demand explicit
wenzelm
parents: 12665
diff changeset
    87
  parentheses to indicate the intended grouping.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    88
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    89
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
    90
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
    91
subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    92
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
    93
text {*
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
    94
  Concrete syntax based on plain ASCII characters has its inherent
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
    95
  limitations.  Rich mathematical notation demands a larger repertoire
12670
wenzelm
parents: 12665
diff changeset
    96
  of glyphs.  Several standards of extended character sets have been
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
    97
  proposed over decades, but none has become universally available so
12665
wenzelm
parents: 12659
diff changeset
    98
  far.  Isabelle supports a generic notion of \bfindex{symbols} as the
wenzelm
parents: 12659
diff changeset
    99
  smallest entities of source text, without referring to internal
wenzelm
parents: 12659
diff changeset
   100
  encodings.  There are three kinds of such ``generalized
wenzelm
parents: 12659
diff changeset
   101
  characters'':
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   102
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   103
  \begin{enumerate}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   104
12653
wenzelm
parents: 12651
diff changeset
   105
  \item 7-bit ASCII characters
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   106
12653
wenzelm
parents: 12651
diff changeset
   107
  \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   108
12653
wenzelm
parents: 12651
diff changeset
   109
  \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   110
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   111
  \end{enumerate}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   112
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   113
  Here $ident$ may be any identifier according to the usual Isabelle
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   114
  conventions.  This results in an infinite store of symbols, whose
12653
wenzelm
parents: 12651
diff changeset
   115
  interpretation is left to further front-end tools.  For example,
12670
wenzelm
parents: 12665
diff changeset
   116
  both the user-interface of Proof~General + X-Symbol and the Isabelle
wenzelm
parents: 12665
diff changeset
   117
  document processor (see \S\ref{sec:document-preparation}) display
wenzelm
parents: 12665
diff changeset
   118
  the \verb,\,\verb,<forall>, symbol really as @{text \<forall>}.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   119
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   120
  A list of standard Isabelle symbols is given in
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   121
  \cite[appendix~A]{isabelle-sys}.  Users may introduce their own
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   122
  interpretation of further symbols by configuring the appropriate
12653
wenzelm
parents: 12651
diff changeset
   123
  front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
wenzelm
parents: 12651
diff changeset
   124
  macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
wenzelm
parents: 12651
diff changeset
   125
  few predefined control symbols, such as \verb,\,\verb,<^sub>, and
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   126
  \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
12653
wenzelm
parents: 12651
diff changeset
   127
  (printable) symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
12670
wenzelm
parents: 12665
diff changeset
   128
  output as @{text "A\<^sup>\<star>"}.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   129
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   130
  \medskip The following version of our @{text xor} definition uses a
12670
wenzelm
parents: 12665
diff changeset
   131
  standard Isabelle symbol to achieve typographically more pleasing
wenzelm
parents: 12665
diff changeset
   132
  output than before.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   133
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   134
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   135
(*<*)
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   136
hide const xor
12665
wenzelm
parents: 12659
diff changeset
   137
ML_setup {* Context.>> (Theory.add_path "version1") *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   138
(*>*)
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   139
constdefs
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   140
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   141
  "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   142
(*<*)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   143
local
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   144
(*>*)
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   145
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   146
text {*
12653
wenzelm
parents: 12651
diff changeset
   147
  \noindent The X-Symbol package within Proof~General provides several
wenzelm
parents: 12651
diff changeset
   148
  input methods to enter @{text \<oplus>} in the text.  If all fails one may
12670
wenzelm
parents: 12665
diff changeset
   149
  just type a named entity \verb,\,\verb,<oplus>, by hand; the display
wenzelm
parents: 12665
diff changeset
   150
  will be adapted immediately after continuing input.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   151
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   152
  \medskip A slightly more refined scheme is to provide alternative
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   153
  syntax via the \bfindex{print mode} concept of Isabelle (see also
12653
wenzelm
parents: 12651
diff changeset
   154
  \cite{isabelle-ref}).  By convention, the mode of ``$xsymbols$'' is
wenzelm
parents: 12651
diff changeset
   155
  enabled whenever Proof~General's X-Symbol mode (or {\LaTeX} output)
12670
wenzelm
parents: 12665
diff changeset
   156
  is active.  Now consider the following hybrid declaration of @{text
12653
wenzelm
parents: 12651
diff changeset
   157
  xor}.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   158
*}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   159
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   160
(*<*)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   161
hide const xor
12665
wenzelm
parents: 12659
diff changeset
   162
ML_setup {* Context.>> (Theory.add_path "version2") *}
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   163
(*>*)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   164
constdefs
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   165
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   166
  "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   167
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   168
syntax (xsymbols)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   169
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>\<ignore>" 60)
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   170
(*<*)
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   171
local
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   172
(*>*)
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   173
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   174
text {*
12653
wenzelm
parents: 12651
diff changeset
   175
  The \commdx{syntax} command introduced here acts like
wenzelm
parents: 12651
diff changeset
   176
  \isakeyword{consts}, but without declaring a logical constant; an
wenzelm
parents: 12651
diff changeset
   177
  optional print mode specification may be given, too.  Note that the
12670
wenzelm
parents: 12665
diff changeset
   178
  type declaration given above merely serves for syntactic purposes,
12653
wenzelm
parents: 12651
diff changeset
   179
  and is not checked for consistency with the real constant.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   180
12672
wenzelm
parents: 12670
diff changeset
   181
  \medskip We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in
wenzelm
parents: 12670
diff changeset
   182
  input, while output uses the nicer syntax of $xsymbols$, provided
wenzelm
parents: 12670
diff changeset
   183
  that print mode is active.  Such an arrangement is particularly
wenzelm
parents: 12670
diff changeset
   184
  useful for interactive development, where users may type plain ASCII
wenzelm
parents: 12670
diff changeset
   185
  text, but gain improved visual feedback from the system.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   186
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   187
  \begin{warn}
12653
wenzelm
parents: 12651
diff changeset
   188
  Alternative syntax declarations are apt to result in varying
wenzelm
parents: 12651
diff changeset
   189
  occurrences of concrete syntax in the input sources.  Isabelle
wenzelm
parents: 12651
diff changeset
   190
  provides no systematic way to convert alternative syntax expressions
wenzelm
parents: 12651
diff changeset
   191
  back and forth; print modes only affect situations where formal
wenzelm
parents: 12651
diff changeset
   192
  entities are pretty printed by the Isabelle process (e.g.\ output of
wenzelm
parents: 12651
diff changeset
   193
  terms and types), but not the original theory text.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   194
  \end{warn}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   195
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   196
  \medskip The following variant makes the alternative @{text \<oplus>}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   197
  notation only available for output.  Thus we may enforce input
12653
wenzelm
parents: 12651
diff changeset
   198
  sources to refer to plain ASCII only, but effectively disable
12670
wenzelm
parents: 12665
diff changeset
   199
  cut-and-paste from output at the same time.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   200
*}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   201
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   202
syntax (xsymbols output)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   203
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>\<ignore>" 60)
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   204
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   205
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   206
subsection {* Prefix Annotations *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   207
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   208
text {*
12653
wenzelm
parents: 12651
diff changeset
   209
  Prefix syntax annotations\index{prefix annotation} are just another
12670
wenzelm
parents: 12665
diff changeset
   210
  degenerate form of mixfixes \cite{isabelle-ref}, without any
12653
wenzelm
parents: 12651
diff changeset
   211
  template arguments or priorities --- just some bits of literal
wenzelm
parents: 12651
diff changeset
   212
  syntax.  The following example illustrates this idea idea by
wenzelm
parents: 12651
diff changeset
   213
  associating common symbols with the constructors of a datatype.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   214
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   215
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   216
datatype currency =
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   217
    Euro nat    ("\<euro>")
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   218
  | Pounds nat  ("\<pounds>")
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   219
  | Yen nat     ("\<yen>")
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   220
  | Dollar nat  ("$")
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   221
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   222
text {*
12653
wenzelm
parents: 12651
diff changeset
   223
  \noindent Here the mixfix annotations on the rightmost column happen
wenzelm
parents: 12651
diff changeset
   224
  to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
wenzelm
parents: 12651
diff changeset
   225
  \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
wenzelm
parents: 12651
diff changeset
   226
  that a constructor like @{text Euro} actually is a function @{typ
wenzelm
parents: 12651
diff changeset
   227
  "nat \<Rightarrow> currency"}.  An expression like @{text "Euro 10"} will be
wenzelm
parents: 12651
diff changeset
   228
  printed as @{term "\<euro> 10"}; only the head of the application is
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   229
  subject to our concrete syntax.  This simple form already achieves
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   230
  conformance with notational standards of the European Commission.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   231
12665
wenzelm
parents: 12659
diff changeset
   232
  Prefix syntax also works for plain \isakeyword{consts} or
wenzelm
parents: 12659
diff changeset
   233
  \isakeyword{constdefs}, of course.
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   234
*}
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   235
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   236
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   237
subsection {* Syntax Translations \label{sec:syntax-translations} *}
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   238
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   239
text{*
12670
wenzelm
parents: 12665
diff changeset
   240
  Mixfix syntax annotations work well in those situations where
12653
wenzelm
parents: 12651
diff changeset
   241
  particular constant application forms need to be decorated by
wenzelm
parents: 12651
diff changeset
   242
  concrete syntax; just reconsider @{text "xor A B"} versus @{text "A
12670
wenzelm
parents: 12665
diff changeset
   243
  \<oplus> B"} covered before.  Occasionally the relationship between some
12653
wenzelm
parents: 12651
diff changeset
   244
  piece of notation and its internal form is slightly more involved.
wenzelm
parents: 12651
diff changeset
   245
  Here the concept of \bfindex{syntax translations} enters the scene.
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   246
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   247
  Using the raw \isakeyword{syntax}\index{syntax (command)} command we
12653
wenzelm
parents: 12651
diff changeset
   248
  may introduce uninterpreted notational elements, while
12670
wenzelm
parents: 12665
diff changeset
   249
  \commdx{translations} relates input forms with more complex logical
wenzelm
parents: 12665
diff changeset
   250
  expressions.  This essentially provides a simple mechanism for
wenzelm
parents: 12665
diff changeset
   251
  syntactic macros; even heavier transformations may be written in ML
wenzelm
parents: 12665
diff changeset
   252
  \cite{isabelle-ref}.
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   253
12653
wenzelm
parents: 12651
diff changeset
   254
  \medskip A typical example of syntax translations is to decorate
12673
wenzelm
parents: 12672
diff changeset
   255
  relational expressions (i.e.\ set-membership of tuples) with
wenzelm
parents: 12672
diff changeset
   256
  handsome symbolic notation, such as @{text "(x, y) \<in> sim"} versus
wenzelm
parents: 12672
diff changeset
   257
  @{text "x \<approx> y"}.
12635
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   258
*}
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   259
e2d44df29c94 more on concrete syntax;
wenzelm
parents: 12629
diff changeset
   260
consts
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   261
  sim :: "('a \<times> 'a) set"
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   262
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   263
syntax
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   264
  "_sim" :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infix "\<approx>" 50)
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   265
translations
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   266
  "x \<approx> y" \<rightleftharpoons> "(x, y) \<in> sim"
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   267
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   268
text {*
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   269
  \noindent Here the name of the dummy constant @{text "_sim"} does
12653
wenzelm
parents: 12651
diff changeset
   270
  not really matter, as long as it is not used elsewhere.  Prefixing
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   271
  an underscore is a common convention.  The \isakeyword{translations}
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   272
  declaration already uses concrete syntax on the left-hand side;
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   273
  internally we relate a raw application @{text "_sim x y"} with
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   274
  @{text "(x, y) \<in> sim"}.
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   275
12653
wenzelm
parents: 12651
diff changeset
   276
  \medskip Another common application of syntax translations is to
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   277
  provide variant versions of fundamental relational expressions, such
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   278
  as @{text \<noteq>} for negated equalities.  The following declaration
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   279
  stems from Isabelle/HOL itself:
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   280
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   281
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   282
syntax "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<noteq>\<ignore>" 50)
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   283
translations "x \<noteq>\<ignore> y" \<rightleftharpoons> "\<not> (x = y)"
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   284
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   285
text {*
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   286
  \noindent Normally one would introduce derived concepts like this
12653
wenzelm
parents: 12651
diff changeset
   287
  within the logic, using \isakeyword{consts} + \isakeyword{defs}
wenzelm
parents: 12651
diff changeset
   288
  instead of \isakeyword{syntax} + \isakeyword{translations}.  The
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   289
  present formulation has the virtue that expressions are immediately
12665
wenzelm
parents: 12659
diff changeset
   290
  replaced by the ``definition'' upon parsing; the effect is reversed
wenzelm
parents: 12659
diff changeset
   291
  upon printing.
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   292
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   293
  Simulating definitions via translations is adequate for very basic
12665
wenzelm
parents: 12659
diff changeset
   294
  principles, where a new representation is a trivial variation on an
wenzelm
parents: 12659
diff changeset
   295
  existing one.  On the other hand, syntax translations do not scale
wenzelm
parents: 12659
diff changeset
   296
  up well to large hierarchies of concepts built on each other.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   297
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   298
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   299
12653
wenzelm
parents: 12651
diff changeset
   300
section {* Document Preparation \label{sec:document-preparation} *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   301
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   302
text {*
12653
wenzelm
parents: 12651
diff changeset
   303
  Isabelle/Isar is centered around the concept of \bfindex{formal
12665
wenzelm
parents: 12659
diff changeset
   304
  proof documents}\index{documents|bold}.  The ultimate result of a
wenzelm
parents: 12659
diff changeset
   305
  formal development effort is meant to be a human-readable record,
wenzelm
parents: 12659
diff changeset
   306
  presented as browsable PDF file or printed on paper.  The overall
wenzelm
parents: 12659
diff changeset
   307
  document structure follows traditional mathematical articles, with
wenzelm
parents: 12659
diff changeset
   308
  sections, intermediate explanations, definitions, theorems and
wenzelm
parents: 12659
diff changeset
   309
  proofs.
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   310
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   311
  The Isar proof language \cite{Wenzel-PhD}, which is not covered in
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   312
  this book, admits to write formal proof texts that are acceptable
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   313
  both to the machine and human readers at the same time.  Thus
12653
wenzelm
parents: 12651
diff changeset
   314
  marginal comments and explanations may be kept at a minimum.  Even
wenzelm
parents: 12651
diff changeset
   315
  without proper coverage of human-readable proofs, Isabelle document
12665
wenzelm
parents: 12659
diff changeset
   316
  is very useful to produce formally derived texts.  Unstructured
wenzelm
parents: 12659
diff changeset
   317
  proof scripts given here may be just ignored by readers, or
wenzelm
parents: 12659
diff changeset
   318
  intentionally suppressed from the text by the writer (see also
wenzelm
parents: 12659
diff changeset
   319
  \S\ref{sec:doc-prep-suppress}).
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   320
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   321
  \medskip The Isabelle document preparation system essentially acts
12670
wenzelm
parents: 12665
diff changeset
   322
  as a front-end to {\LaTeX}.  After checking specifications and
wenzelm
parents: 12665
diff changeset
   323
  proofs formally, the theory sources are turned into typesetting
wenzelm
parents: 12665
diff changeset
   324
  instructions in a schematic manner.  This enables users to write
wenzelm
parents: 12665
diff changeset
   325
  authentic reports on theory developments with little effort, where
wenzelm
parents: 12665
diff changeset
   326
  most consistency checks are handled by the system.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   327
*}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   328
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   329
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   330
subsection {* Isabelle Sessions *}
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   331
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   332
text {*
12653
wenzelm
parents: 12651
diff changeset
   333
  In contrast to the highly interactive mode of Isabelle/Isar theory
wenzelm
parents: 12651
diff changeset
   334
  development, the document preparation stage essentially works in
12670
wenzelm
parents: 12665
diff changeset
   335
  batch-mode.  An Isabelle \bfindex{session} consists of a collection
wenzelm
parents: 12665
diff changeset
   336
  of theory source files that contribute to a single output document
wenzelm
parents: 12665
diff changeset
   337
  eventually.  Each session is derived from a single parent one,
wenzelm
parents: 12665
diff changeset
   338
  usually an object-logic image like \texttt{HOL}.  This results in an
wenzelm
parents: 12665
diff changeset
   339
  overall tree structure, which is reflected by the output location in
wenzelm
parents: 12665
diff changeset
   340
  the file system (usually rooted at \verb,~/isabelle/browser_info,).
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   341
12670
wenzelm
parents: 12665
diff changeset
   342
  \medskip Here is the canonical arrangement of sources of a session
wenzelm
parents: 12665
diff changeset
   343
  called \texttt{MySession}:
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   344
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   345
  \begin{itemize}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   346
12670
wenzelm
parents: 12665
diff changeset
   347
  \item Directory \texttt{MySession} holds the required theory files
wenzelm
parents: 12665
diff changeset
   348
  $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   349
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   350
  \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   351
  for loading all wanted theories, usually just
12665
wenzelm
parents: 12659
diff changeset
   352
  ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
12670
wenzelm
parents: 12665
diff changeset
   353
  dependency graph.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   354
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   355
  \item Directory \texttt{MySession/document} contains everything
12653
wenzelm
parents: 12651
diff changeset
   356
  required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
wenzelm
parents: 12651
diff changeset
   357
  provided initially.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   358
12653
wenzelm
parents: 12651
diff changeset
   359
  The latter file holds appropriate {\LaTeX} code to commence a
wenzelm
parents: 12651
diff changeset
   360
  document (\verb,\documentclass, etc.), and to include the generated
12665
wenzelm
parents: 12659
diff changeset
   361
  files $T@i$\texttt{.tex} for each theory.  The generated
12670
wenzelm
parents: 12665
diff changeset
   362
  \texttt{session.tex} will contain {\LaTeX} commands to include all
12672
wenzelm
parents: 12670
diff changeset
   363
  generated files in topologically sorted order, so
12670
wenzelm
parents: 12665
diff changeset
   364
  \verb,\input{session}, in \texttt{root.tex} does the job in most
12653
wenzelm
parents: 12651
diff changeset
   365
  situations.
wenzelm
parents: 12651
diff changeset
   366
12665
wenzelm
parents: 12659
diff changeset
   367
  \item \texttt{IsaMakefile} outside of the directory
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   368
  \texttt{MySession} holds appropriate dependencies and invocations of
12653
wenzelm
parents: 12651
diff changeset
   369
  Isabelle tools to control the batch job.  In fact, several sessions
wenzelm
parents: 12651
diff changeset
   370
  may be controlled by the same \texttt{IsaMakefile}.  See also
wenzelm
parents: 12651
diff changeset
   371
  \cite{isabelle-sys} for further details, especially on
wenzelm
parents: 12651
diff changeset
   372
  \texttt{isatool usedir} and \texttt{isatool make}.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   373
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   374
  \end{itemize}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   375
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   376
  With everything put in its proper place, \texttt{isatool make}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   377
  should be sufficient to process the Isabelle session completely,
12653
wenzelm
parents: 12651
diff changeset
   378
  with the generated document appearing in its proper place.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   379
12665
wenzelm
parents: 12659
diff changeset
   380
  \medskip In reality, users may want to have \texttt{isatool mkdir}
12653
wenzelm
parents: 12651
diff changeset
   381
  generate an initial working setup without further ado.  For example,
12670
wenzelm
parents: 12665
diff changeset
   382
  a new session \texttt{MySession} derived from \texttt{HOL} may be
12653
wenzelm
parents: 12651
diff changeset
   383
  produced as follows:
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   384
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   385
\begin{verbatim}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   386
  isatool mkdir HOL MySession
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   387
  isatool make
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   388
\end{verbatim}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   389
12653
wenzelm
parents: 12651
diff changeset
   390
  This processes the session with sensible default options, including
wenzelm
parents: 12651
diff changeset
   391
  verbose mode to tell the user where the ultimate results will
12670
wenzelm
parents: 12665
diff changeset
   392
  appear.  The above dry run should already be able to produce a
wenzelm
parents: 12665
diff changeset
   393
  single page of output (with a dummy title, empty table of contents
wenzelm
parents: 12665
diff changeset
   394
  etc.).  Any failure at that stage is likely to indicate technical
wenzelm
parents: 12665
diff changeset
   395
  problems with the user's {\LaTeX} installation.\footnote{Especially
wenzelm
parents: 12665
diff changeset
   396
  make sure that \texttt{pdflatex} is present; if all fails one may
wenzelm
parents: 12665
diff changeset
   397
  fall back on DVI output by changing \texttt{usedir} options in
wenzelm
parents: 12665
diff changeset
   398
  \texttt{IsaMakefile} \cite{isabelle-sys}.}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   399
12653
wenzelm
parents: 12651
diff changeset
   400
  \medskip One may now start to populate the directory
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   401
  \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   402
  accordingly.  \texttt{MySession/document/root.tex} should be also
12653
wenzelm
parents: 12651
diff changeset
   403
  adapted at some point; the default version is mostly
12670
wenzelm
parents: 12665
diff changeset
   404
  self-explanatory.  Note that \verb,\isabellestyle, enables
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   405
  fine-tuning of the general appearance of characters and mathematical
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   406
  symbols (see also \S\ref{sec:doc-prep-symbols}).
12653
wenzelm
parents: 12651
diff changeset
   407
12670
wenzelm
parents: 12665
diff changeset
   408
  Especially observe inclusion of the {\LaTeX} packages
12653
wenzelm
parents: 12651
diff changeset
   409
  \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
wenzelm
parents: 12651
diff changeset
   410
  for mathematical symbols), and the final \texttt{pdfsetup} (provides
wenzelm
parents: 12651
diff changeset
   411
  handsome defaults for \texttt{hyperref}, including URL markup).
12670
wenzelm
parents: 12665
diff changeset
   412
  Further packages may be required in particular applications, e.g.\
wenzelm
parents: 12665
diff changeset
   413
  for unusual Isabelle symbols.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   414
12672
wenzelm
parents: 12670
diff changeset
   415
  \medskip Additional files for the {\LaTeX} stage may be included in
wenzelm
parents: 12670
diff changeset
   416
  the directory \texttt{MySession/document}, too, such as {\TeX}
wenzelm
parents: 12670
diff changeset
   417
  sources or graphics).  In particular, adding \texttt{root.bib} here
12670
wenzelm
parents: 12665
diff changeset
   418
  (with that specific name) causes an automatic run of \texttt{bibtex}
wenzelm
parents: 12665
diff changeset
   419
  to process a bibliographic database; see also \texttt{isatool
wenzelm
parents: 12665
diff changeset
   420
  document} covered in \cite{isabelle-sys}.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   421
12653
wenzelm
parents: 12651
diff changeset
   422
  \medskip Any failure of the document preparation phase in an
12670
wenzelm
parents: 12665
diff changeset
   423
  Isabelle batch session leaves the generated sources in their target
wenzelm
parents: 12665
diff changeset
   424
  location (as pointed out by the accompanied error message).  This
wenzelm
parents: 12665
diff changeset
   425
  enables users to trace {\LaTeX} at the file positions of the
wenzelm
parents: 12665
diff changeset
   426
  generated material.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   427
*}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   428
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   429
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   430
subsection {* Structure Markup *}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   431
12653
wenzelm
parents: 12651
diff changeset
   432
text {*
wenzelm
parents: 12651
diff changeset
   433
  The large-scale structure of Isabelle documents follows existing
wenzelm
parents: 12651
diff changeset
   434
  {\LaTeX} conventions, with chapters, sections, subsubsections etc.
wenzelm
parents: 12651
diff changeset
   435
  The Isar language includes separate \bfindex{markup commands}, which
wenzelm
parents: 12651
diff changeset
   436
  do not effect the formal content of a theory (or proof), but result
12665
wenzelm
parents: 12659
diff changeset
   437
  in corresponding {\LaTeX} elements.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   438
12665
wenzelm
parents: 12659
diff changeset
   439
  There are separate markup commands depending on the textual context:
wenzelm
parents: 12659
diff changeset
   440
  in header position (just before \isakeyword{theory}), within the
wenzelm
parents: 12659
diff changeset
   441
  theory body, or within a proof.  The header needs to be treated
wenzelm
parents: 12659
diff changeset
   442
  specially here, since ordinary theory and proof commands may only
wenzelm
parents: 12659
diff changeset
   443
  occur \emph{after} the initial \isakeyword{theory} specification.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   444
12665
wenzelm
parents: 12659
diff changeset
   445
  \medskip
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   446
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   447
  \begin{tabular}{llll}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   448
  header & theory & proof & default meaning \\\hline
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   449
    & \commdx{chapter} & & \verb,\chapter, \\
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   450
  \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   451
    & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   452
    & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   453
  \end{tabular}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   454
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   455
  \medskip
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   456
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   457
  From the Isabelle perspective, each markup command takes a single
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   458
  $text$ argument (delimited by \verb,",\dots\verb,", or
12653
wenzelm
parents: 12651
diff changeset
   459
  \verb,{,\verb,*,~\dots~\verb,*,\verb,},).  After stripping any
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   460
  surrounding white space, the argument is passed to a {\LaTeX} macro
12653
wenzelm
parents: 12651
diff changeset
   461
  \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}.  These macros
wenzelm
parents: 12651
diff changeset
   462
  are defined in \verb,isabelle.sty, according to the meaning given in
wenzelm
parents: 12651
diff changeset
   463
  the rightmost column above.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   464
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   465
  \medskip The following source fragment illustrates structure markup
12653
wenzelm
parents: 12651
diff changeset
   466
  of a theory.  Note that {\LaTeX} labels may be included inside of
wenzelm
parents: 12651
diff changeset
   467
  section headings as well.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   468
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   469
  \begin{ttbox}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   470
  header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   471
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   472
  theory Foo_Bar = Main:
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   473
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   474
  subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   475
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   476
  consts
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   477
    foo :: \dots
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   478
    bar :: \dots
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   479
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   480
  defs \dots
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   481
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   482
  subsection {\ttlbrace}* Derived rules *{\ttrbrace}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   483
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   484
  lemma fooI: \dots
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   485
  lemma fooE: \dots
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   486
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   487
  subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   488
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   489
  theorem main: \dots
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   490
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   491
  end
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   492
  \end{ttbox}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   493
12653
wenzelm
parents: 12651
diff changeset
   494
  Users may occasionally want to change the meaning of markup
12665
wenzelm
parents: 12659
diff changeset
   495
  commands, say via \verb,\renewcommand, in \texttt{root.tex};
12670
wenzelm
parents: 12665
diff changeset
   496
  \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
12653
wenzelm
parents: 12651
diff changeset
   497
  moving it up in the hierarchy to become \verb,\chapter,.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   498
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   499
\begin{verbatim}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   500
  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   501
\end{verbatim}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   502
12653
wenzelm
parents: 12651
diff changeset
   503
  \noindent Certainly, this requires to change the default
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   504
  \verb,\documentclass{article}, in \texttt{root.tex} to something
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   505
  that supports the notion of chapters in the first place, e.g.\
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   506
  \verb,\documentclass{report},.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   507
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   508
  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   509
  hold the name of the current theory context.  This is particularly
12653
wenzelm
parents: 12651
diff changeset
   510
  useful for document headings:
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   511
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   512
\begin{verbatim}
12653
wenzelm
parents: 12651
diff changeset
   513
  \renewcommand{\isamarkupheader}[1]
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   514
  {\chapter{#1}\markright{THEORY~\isabellecontext}}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   515
\end{verbatim}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   516
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   517
  \noindent Make sure to include something like
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   518
  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   519
  should have more than 2 pages to show the effect.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   520
*}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   521
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   522
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   523
subsection {* Formal Comments and Antiquotations *}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   524
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   525
text {*
12665
wenzelm
parents: 12659
diff changeset
   526
  Isabelle source comments, which are of the form
wenzelm
parents: 12659
diff changeset
   527
  \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white
wenzelm
parents: 12659
diff changeset
   528
  space and do not really contribute to the content.  They mainly
wenzelm
parents: 12659
diff changeset
   529
  serve technical purposes to mark certain oddities in the raw input
wenzelm
parents: 12659
diff changeset
   530
  text.  In contrast, \bfindex{formal comments} are portions of text
wenzelm
parents: 12659
diff changeset
   531
  that are associated with formal Isabelle/Isar commands
wenzelm
parents: 12659
diff changeset
   532
  (\bfindex{marginal comments}), or as stanalone paragraphs within a
wenzelm
parents: 12659
diff changeset
   533
  theory or proof context (\bfindex{text blocks}).
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   534
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   535
  \medskip Marginal comments are part of each command's concrete
12670
wenzelm
parents: 12665
diff changeset
   536
  syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
12665
wenzelm
parents: 12659
diff changeset
   537
  where $text$ is delimited by \verb,",\dots\verb,", or
12670
wenzelm
parents: 12665
diff changeset
   538
  \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as before.  Multiple
wenzelm
parents: 12665
diff changeset
   539
  marginal comments may be given at the same time.  Here is a simple
wenzelm
parents: 12665
diff changeset
   540
  example:
12665
wenzelm
parents: 12659
diff changeset
   541
*}
wenzelm
parents: 12659
diff changeset
   542
wenzelm
parents: 12659
diff changeset
   543
lemma "A --> A"
wenzelm
parents: 12659
diff changeset
   544
  -- "a triviality of propositional logic"
wenzelm
parents: 12659
diff changeset
   545
  -- "(should not really bother)"
wenzelm
parents: 12659
diff changeset
   546
  by (rule impI) -- "implicit assumption step involved here"
wenzelm
parents: 12659
diff changeset
   547
wenzelm
parents: 12659
diff changeset
   548
text {*
wenzelm
parents: 12659
diff changeset
   549
  \noindent The above output has been produced as follows:
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   550
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   551
\begin{verbatim}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   552
  lemma "A --> A"
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   553
    -- "a triviality of propositional logic"
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   554
    -- "(should not really bother)"
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   555
    by (rule impI) -- "implicit assumption step involved here"
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   556
\end{verbatim}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   557
12670
wenzelm
parents: 12665
diff changeset
   558
  From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
wenzelm
parents: 12665
diff changeset
   559
  command, associated with the macro \verb,\isamarkupcmt, (taking a
wenzelm
parents: 12665
diff changeset
   560
  single argument).
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   561
12665
wenzelm
parents: 12659
diff changeset
   562
  \medskip Text blocks are introduced by the commands \bfindex{text}
wenzelm
parents: 12659
diff changeset
   563
  and \bfindex{txt}, for theory and proof contexts, respectively.
wenzelm
parents: 12659
diff changeset
   564
  Each takes again a single $text$ argument, which is interpreted as a
wenzelm
parents: 12659
diff changeset
   565
  free-form paragraph in {\LaTeX} (surrounded by some additional
12670
wenzelm
parents: 12665
diff changeset
   566
  vertical space).  This behavior may be changed by redefining the
wenzelm
parents: 12665
diff changeset
   567
  {\LaTeX} environments of \verb,isamarkuptext, or
wenzelm
parents: 12665
diff changeset
   568
  \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
wenzelm
parents: 12665
diff changeset
   569
  text style of the body is determined by \verb,\isastyletext, and
wenzelm
parents: 12665
diff changeset
   570
  \verb,\isastyletxt,; the default setup uses a smaller font within
wenzelm
parents: 12665
diff changeset
   571
  proofs.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   572
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   573
  \medskip The $text$ part of each of the various markup commands
12670
wenzelm
parents: 12665
diff changeset
   574
  considered so far essentially inserts \emph{quoted material} into a
wenzelm
parents: 12665
diff changeset
   575
  formal text, mainly for instruction of the reader.  An
wenzelm
parents: 12665
diff changeset
   576
  \bfindex{antiquotation} is again a formal object embedded into such
wenzelm
parents: 12665
diff changeset
   577
  an informal portion.  The interpretation of antiquotations is
wenzelm
parents: 12665
diff changeset
   578
  limited to some well-formedness checks, with the result being pretty
wenzelm
parents: 12665
diff changeset
   579
  printed to the resulting document.  So quoted text blocks together
wenzelm
parents: 12665
diff changeset
   580
  with antiquotations provide very handsome means to reference formal
wenzelm
parents: 12665
diff changeset
   581
  entities with good confidence in getting the technical details right
wenzelm
parents: 12665
diff changeset
   582
  (especially syntax and types).
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   583
12665
wenzelm
parents: 12659
diff changeset
   584
  The general syntax of antiquotations is as follows:
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   585
  \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   586
  \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
12665
wenzelm
parents: 12659
diff changeset
   587
  for a comma-separated list of options consisting of a $name$ or
12670
wenzelm
parents: 12665
diff changeset
   588
  \texttt{$name$=$value$}.  The syntax of $arguments$ depends on the
wenzelm
parents: 12665
diff changeset
   589
  kind of antiquotation, it generally follows the same conventions for
wenzelm
parents: 12665
diff changeset
   590
  types, terms, or theorems as in the formal part of a theory.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   591
12665
wenzelm
parents: 12659
diff changeset
   592
  \medskip Here is an example of the quotation-antiquotation
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   593
  technique: @{term "%x y. x"} is a well-typed term.
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   594
12665
wenzelm
parents: 12659
diff changeset
   595
  \medskip\noindent The above output has been produced as follows:
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   596
  \begin{ttbox}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   597
text {\ttlbrace}*
12665
wenzelm
parents: 12659
diff changeset
   598
  Here is an example of the quotation-antiquotation technique:
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   599
  {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   600
*{\ttrbrace}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   601
  \end{ttbox}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   602
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   603
  From the notational change of the ASCII character \verb,%, to the
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   604
  symbol @{text \<lambda>} we see that the term really got printed by the
12670
wenzelm
parents: 12665
diff changeset
   605
  system (after parsing and type-checking) --- document preparation
12665
wenzelm
parents: 12659
diff changeset
   606
  enables symbolic output by default.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   607
12665
wenzelm
parents: 12659
diff changeset
   608
  \medskip The next example includes an option to modify the
wenzelm
parents: 12659
diff changeset
   609
  \verb,show_types, flag of Isabelle:
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   610
  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces @{term
12670
wenzelm
parents: 12665
diff changeset
   611
  [show_types] "%x y. x"}.  Type-inference has figured out the most
wenzelm
parents: 12665
diff changeset
   612
  general typings in the present (theory) context.  Note that term
wenzelm
parents: 12665
diff changeset
   613
  fragments may acquire different typings due to constraints imposed
wenzelm
parents: 12665
diff changeset
   614
  by previous text (say within a proof), e.g.\ due to the main goal
wenzelm
parents: 12665
diff changeset
   615
  statement given beforehand.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   616
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   617
  \medskip Several further kinds of antiquotations (and options) are
12665
wenzelm
parents: 12659
diff changeset
   618
  available \cite{isabelle-sys}.  Here are a few commonly used
12670
wenzelm
parents: 12665
diff changeset
   619
  combinations:
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   620
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   621
  \medskip
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   622
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   623
  \begin{tabular}{ll}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   624
  \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   625
  \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   626
  \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
12665
wenzelm
parents: 12659
diff changeset
   627
  \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   628
  \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   629
  \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   630
  \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
12665
wenzelm
parents: 12659
diff changeset
   631
  \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check validity of fact $a$, print its name \\
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   632
  \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   633
  \end{tabular}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   634
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   635
  \medskip
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   636
12665
wenzelm
parents: 12659
diff changeset
   637
  Note that \attrdx{no_vars} given above is \emph{not} an
wenzelm
parents: 12659
diff changeset
   638
  antiquotation option, but an attribute of the theorem argument given
wenzelm
parents: 12659
diff changeset
   639
  here.  This might be useful with a diagnostic command like
wenzelm
parents: 12659
diff changeset
   640
  \isakeyword{thm}, too.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   641
12665
wenzelm
parents: 12659
diff changeset
   642
  \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   643
  particularly interesting.  Embedding uninterpreted text within an
12665
wenzelm
parents: 12659
diff changeset
   644
  informal body might appear useless at first sight.  Here the key
wenzelm
parents: 12659
diff changeset
   645
  virtue is that the string $s$ is processed as Isabelle output,
wenzelm
parents: 12659
diff changeset
   646
  interpreting Isabelle symbols appropriately.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   647
12665
wenzelm
parents: 12659
diff changeset
   648
  For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces @{text
wenzelm
parents: 12659
diff changeset
   649
  "\<forall>\<exists>"}, according to the standard interpretation of these symbol
wenzelm
parents: 12659
diff changeset
   650
  (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   651
  mathematical notation in both the formal and informal parts of the
12665
wenzelm
parents: 12659
diff changeset
   652
  document very easily.  Manual {\LaTeX} code would leave more control
wenzelm
parents: 12659
diff changeset
   653
  over the type-setting, but is also slightly more tedious.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   654
*}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   655
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   656
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   657
subsection {* Interpretation of symbols \label{sec:doc-prep-symbols} *}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   658
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   659
text {*
12665
wenzelm
parents: 12659
diff changeset
   660
  As has been pointed out before (\S\ref{sec:syntax-symbols}),
12670
wenzelm
parents: 12665
diff changeset
   661
  Isabelle symbols are the smallest syntactic entities --- a
12665
wenzelm
parents: 12659
diff changeset
   662
  straight-forward generalization of ASCII characters.  While Isabelle
wenzelm
parents: 12659
diff changeset
   663
  does not impose any interpretation of the infinite collection of
12670
wenzelm
parents: 12665
diff changeset
   664
  named symbols, {\LaTeX} documents show canonical glyphs for certain
wenzelm
parents: 12665
diff changeset
   665
  standard symbols \cite[appendix~A]{isabelle-sys}.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   666
12665
wenzelm
parents: 12659
diff changeset
   667
  The {\LaTeX} code produced from Isabelle text follows a relatively
12670
wenzelm
parents: 12665
diff changeset
   668
  simple scheme.  Users may wish to tune the final appearance by
wenzelm
parents: 12665
diff changeset
   669
  redefining certain macros, say in \texttt{root.tex} of the document.
wenzelm
parents: 12665
diff changeset
   670
wenzelm
parents: 12665
diff changeset
   671
  \begin{enumerate}
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   672
12670
wenzelm
parents: 12665
diff changeset
   673
  \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
wenzelm
parents: 12665
diff changeset
   674
  \texttt{a\dots z} are output verbatim, digits are passed as an
wenzelm
parents: 12665
diff changeset
   675
  argument to the \verb,\isadigit, macro, other characters are
wenzelm
parents: 12665
diff changeset
   676
  replaced by specifically named macros of the form
12665
wenzelm
parents: 12659
diff changeset
   677
  \verb,\isacharXYZ,.
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   678
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   679
  \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become
12670
wenzelm
parents: 12665
diff changeset
   680
  \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces).
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   681
12670
wenzelm
parents: 12665
diff changeset
   682
  \item Named control symbols: \verb,{\isasym,$XYZ$\verb,}, become
wenzelm
parents: 12665
diff changeset
   683
  \verb,\isactrl,$XYZ$ each; subsequent symbols may act as arguments
wenzelm
parents: 12665
diff changeset
   684
  if the corresponding macro is defined accordingly.
wenzelm
parents: 12665
diff changeset
   685
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   686
  \end{enumerate}
12665
wenzelm
parents: 12659
diff changeset
   687
12670
wenzelm
parents: 12665
diff changeset
   688
  Users may occasionally wish to give new {\LaTeX} interpretations of
wenzelm
parents: 12665
diff changeset
   689
  named symbols; this merely requires an appropriate definition of
wenzelm
parents: 12665
diff changeset
   690
  \verb,\,\verb,<,$XYZ$\verb,>, (see \texttt{isabelle.sty} for working
wenzelm
parents: 12665
diff changeset
   691
  examples).  Control symbols are slightly more difficult to get
wenzelm
parents: 12665
diff changeset
   692
  right, though.
12665
wenzelm
parents: 12659
diff changeset
   693
wenzelm
parents: 12659
diff changeset
   694
  \medskip The \verb,\isabellestyle, macro provides a high-level
wenzelm
parents: 12659
diff changeset
   695
  interface to tune the general appearance of individual symbols.  For
12670
wenzelm
parents: 12665
diff changeset
   696
  example, \verb,\isabellestyle{it}, uses the italics text style to
wenzelm
parents: 12665
diff changeset
   697
  mimic the general appearance of the {\LaTeX} math mode; double
wenzelm
parents: 12665
diff changeset
   698
  quotes are not printed at all.  The resulting quality of
wenzelm
parents: 12665
diff changeset
   699
  type-setting is quite good, so this should usually be the default
wenzelm
parents: 12665
diff changeset
   700
  style for real production work that gets distributed to a broader
wenzelm
parents: 12665
diff changeset
   701
  audience.
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   702
*}
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   703
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   704
12653
wenzelm
parents: 12651
diff changeset
   705
subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   706
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   707
text {*
12670
wenzelm
parents: 12665
diff changeset
   708
  By default, Isabelle's document system generates a {\LaTeX} source
wenzelm
parents: 12665
diff changeset
   709
  file for each theory that happens to get loaded while running the
wenzelm
parents: 12665
diff changeset
   710
  session.  The generated \texttt{session.tex} will include all of
wenzelm
parents: 12665
diff changeset
   711
  these in order of appearance, which in turn gets included by the
wenzelm
parents: 12665
diff changeset
   712
  standard \texttt{root.tex}.  Certainly one may change the order or
wenzelm
parents: 12665
diff changeset
   713
  suppress unwanted theories by ignoring \texttt{session.tex} and
12653
wenzelm
parents: 12651
diff changeset
   714
  include individual files in \texttt{root.tex} by hand.  On the other
wenzelm
parents: 12651
diff changeset
   715
  hand, such an arrangement requires additional maintenance chores
wenzelm
parents: 12651
diff changeset
   716
  whenever the collection of theories changes.
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   717
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   718
  Alternatively, one may tune the theory loading process in
12653
wenzelm
parents: 12651
diff changeset
   719
  \texttt{ROOT.ML} itself: traversal of the theory dependency graph
12670
wenzelm
parents: 12665
diff changeset
   720
  may be fine-tuned by adding \verb,use_thy, invocations, although
wenzelm
parents: 12665
diff changeset
   721
  topological sorting still has to be observed.  Moreover, the ML
wenzelm
parents: 12665
diff changeset
   722
  operator \verb,no_document, temporarily disables document generation
wenzelm
parents: 12665
diff changeset
   723
  while executing a theory loader command; its usage is like this:
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   724
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   725
\begin{verbatim}
12665
wenzelm
parents: 12659
diff changeset
   726
  no_document use_thy "T";
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   727
\end{verbatim}
12645
3af5de958a1a some text on document preparation;
wenzelm
parents: 12642
diff changeset
   728
12670
wenzelm
parents: 12665
diff changeset
   729
  \medskip Theory output may be also suppressed in smaller portions.
wenzelm
parents: 12665
diff changeset
   730
  For example, research articles, or slides usually do not include the
wenzelm
parents: 12665
diff changeset
   731
  formal content in full.  In order to delimit \bfindex{ignored
12653
wenzelm
parents: 12651
diff changeset
   732
  material} special source comments
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   733
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
12653
wenzelm
parents: 12651
diff changeset
   734
  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
wenzelm
parents: 12651
diff changeset
   735
  text.  Only the document preparation system is affected, the formal
12670
wenzelm
parents: 12665
diff changeset
   736
  checking the theory is performed unchanged.
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   737
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   738
  In the following example we suppress the slightly formalistic
12653
wenzelm
parents: 12651
diff changeset
   739
  \isakeyword{theory} + \isakeyword{end} surroundings a theory.
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   740
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   741
  \medskip
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   742
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   743
  \begin{tabular}{l}
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   744
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
12665
wenzelm
parents: 12659
diff changeset
   745
  \texttt{theory T = Main:} \\
12648
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   746
  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   747
  ~~$\vdots$ \\
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   748
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   749
  \texttt{end} \\
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   750
  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   751
  \end{tabular}
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   752
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   753
  \medskip
16d4b8c09086 some more text;
wenzelm
parents: 12645
diff changeset
   754
12670
wenzelm
parents: 12665
diff changeset
   755
  Text may be suppressed in a fine grained manner.  We may even drop
wenzelm
parents: 12665
diff changeset
   756
  vital parts of a formal proof, pretending that things have been
wenzelm
parents: 12665
diff changeset
   757
  simpler than in reality.  For example, the following ``fully
wenzelm
parents: 12665
diff changeset
   758
  automatic'' proof is actually a fake:
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   759
*}
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   760
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   761
lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   762
  by (auto(*<*)simp add: int_less_le(*>*))
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   763
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   764
text {*
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   765
  \noindent Here the real source of the proof has been as follows:
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   766
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   767
\begin{verbatim}
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   768
  by (auto(*<*)simp add: int_less_le(*>*))
12659
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   769
\end{verbatim}
2aa05eb15bd2 getting close to completion;
wenzelm
parents: 12653
diff changeset
   770
%(*
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   771
12653
wenzelm
parents: 12651
diff changeset
   772
  \medskip Ignoring portions of printed does demand some care by the
12670
wenzelm
parents: 12665
diff changeset
   773
  writer.  First of all, the writer is responsible not to obfuscate
wenzelm
parents: 12665
diff changeset
   774
  the underlying formal development in an unduly manner.  It is fairly
12653
wenzelm
parents: 12651
diff changeset
   775
  easy to invalidate the remaining visible text, e.g.\ by referencing
wenzelm
parents: 12651
diff changeset
   776
  questionable formal items (strange definitions, arbitrary axioms
wenzelm
parents: 12651
diff changeset
   777
  etc.) that have been hidden from sight beforehand.
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   778
12670
wenzelm
parents: 12665
diff changeset
   779
  Authentic reports of formal theories, say as part of a library,
wenzelm
parents: 12665
diff changeset
   780
  usually should refrain from suppressing parts of the text at all.
wenzelm
parents: 12665
diff changeset
   781
  Other users may need the full information for their own derivative
wenzelm
parents: 12665
diff changeset
   782
  work.  If a particular formalization appears inadequate for general
wenzelm
parents: 12665
diff changeset
   783
  public coverage, it is often more appropriate to think of a better
wenzelm
parents: 12665
diff changeset
   784
  way in the first place.
wenzelm
parents: 12665
diff changeset
   785
wenzelm
parents: 12665
diff changeset
   786
  \medskip Some technical subtleties of the
12665
wenzelm
parents: 12659
diff changeset
   787
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
12670
wenzelm
parents: 12665
diff changeset
   788
  elements need to be kept in mind, too --- the system performs little
wenzelm
parents: 12665
diff changeset
   789
  sanity checks here.  Arguments of markup commands and formal
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   790
  comments must not be hidden, otherwise presentation fails.  Open and
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   791
  close parentheses need to be inserted carefully; it is fairly easy
12653
wenzelm
parents: 12651
diff changeset
   792
  to hide the wrong parts, especially after rearranging the sources.
12651
930df4604b36 some more ...;
wenzelm
parents: 12648
diff changeset
   793
12629
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   794
*}
281aa36829d8 beginnings of concrete syntax;
wenzelm
parents: 11647
diff changeset
   795
11647
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
   796
(*<*)
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
   797
end
0538cb0f7999 initial setup for chapter on document preparation;
wenzelm
parents:
diff changeset
   798
(*>*)