1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:31:25 2008 +0100
1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:32:36 2008 +0100
1.3 @@ -101,11 +101,13 @@
1.4 subsection}, and @{command subsubsection}] mark chapter and section
1.5 headings within the main theory body or local theory targets. The
1.6 corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"},
1.7 - @{verbatim "\\isamarkupsection"} etc.
1.8 + @{verbatim "\\isamarkupsection"}, @{verbatim
1.9 + "\\isamarkupsubsection"} etc.
1.10
1.11 \item [@{command sect}, @{command subsect}, and @{command
1.12 subsubsect}] mark section headings within proofs. The corresponding
1.13 - {\LaTeX} macros are @{verbatim "\\isamarkupsect"} etc.
1.14 + {\LaTeX} macros are @{verbatim "\\isamarkupsect"}, @{verbatim
1.15 + "\\isamarkupsubsect"} etc.
1.16
1.17 \item [@{command text} and @{command txt}] specify paragraphs of
1.18 plain text. This corresponds to a {\LaTeX} environment @{verbatim
1.19 @@ -121,19 +123,18 @@
1.20
1.21 Except for @{command "text_raw"} and @{command "txt_raw"}, the text
1.22 passed to any of the above markup commands may refer to formal
1.23 - entities via \emph{antiquotations}, see also \secref{sec:antiq}.
1.24 - These are interpreted in the present theory or proof context, or the
1.25 - named @{text "target"}.
1.26 + entities via \emph{document antiquotations}, see also
1.27 + \secref{sec:antiq}. These are interpreted in the present theory or
1.28 + proof context, or the named @{text "target"}.
1.29
1.30 \medskip The proof markup commands closely resemble those for theory
1.31 specifications, but have a different formal status and produce
1.32 - different {\LaTeX} macros (although the default definitions coincide
1.33 - for analogous commands such as @{command section} and @{command
1.34 - sect}).
1.35 + different {\LaTeX} macros. The default definitions coincide for
1.36 + analogous commands such as @{command section} and @{command sect}.
1.37 *}
1.38
1.39
1.40 -section {* Antiquotations \label{sec:antiq} *}
1.41 +section {* Document Antiquotations \label{sec:antiq} *}
1.42
1.43 text {*
1.44 \begin{matharray}{rcl}
1.45 @@ -158,18 +159,24 @@
1.46 @{antiquotation_def ML_struct} & : & \isarantiq \\
1.47 \end{matharray}
1.48
1.49 - The text body of formal comments (see also \secref{sec:comments})
1.50 - may contain antiquotations of logical entities, such as theorems,
1.51 - terms and types, which are to be presented in the final output
1.52 - produced by the Isabelle document preparation system.
1.53 + The overall content of an Isabelle/Isar theory may alternate between
1.54 + formal and informal text. The main body consists of formal
1.55 + specification and proof commands, interspersed with markup commands
1.56 + (\secref{sec:markup}) or document comments (\secref{sec:comments}).
1.57 + The argument of markup commands quotes informal text to be printed
1.58 + in the resulting document, but may again refer to formal entities
1.59 + via \emph{document antiquotations}.
1.60
1.61 - Thus embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
1.62 - within a text block would cause
1.63 - \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document. Also note that theorem
1.64 - antiquotations may involve attributes as well. For example,
1.65 - @{text "@{thm sym [no_vars]}"} would print the theorem's
1.66 - statement where all schematic variables have been replaced by fixed
1.67 - ones, which are easier to read.
1.68 + For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
1.69 + within a text block makes
1.70 + \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document.
1.71 +
1.72 + Antiquotations usually spare the author tedious typing of logical
1.73 + entities in full detail. Even more importantly, some degree of
1.74 + consistency-checking between the main body of formal text and its
1.75 + informal explanation is achieved, since terms and types appearing in
1.76 + antiquotations are checked within the current theory or proof
1.77 + context.
1.78
1.79 \begin{rail}
1.80 atsign lbrace antiquotation rbrace
1.81 @@ -203,7 +210,7 @@
1.82 \end{rail}
1.83
1.84 Note that the syntax of antiquotations may \emph{not} include source
1.85 - comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} or verbatim
1.86 + comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
1.87 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
1.88 "*"}@{verbatim "}"}.
1.89
1.90 @@ -213,17 +220,15 @@
1.91 guaranteed to refer to a valid ancestor theory in the current
1.92 context.
1.93
1.94 - \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems
1.95 - @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications
1.96 - may be included as well (see also \secref{sec:syn-att}); the
1.97 - @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would
1.98 - be particularly useful to suppress printing of schematic variables.
1.99 + \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
1.100 + Full fact expressions are allowed here, including attributes
1.101 + (\secref{sec:syn-att}).
1.102
1.103 \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
1.104 "\<phi>"}.
1.105
1.106 - \item [@{text "@{lemma \<phi> by m}"}] asserts a well-typed proposition @{text
1.107 - "\<phi>"} to be provable by method @{text m} and prints @{text "\<phi>"}.
1.108 + \item [@{text "@{lemma \<phi> by m}"}] proves a well-typed proposition
1.109 + @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
1.110
1.111 \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
1.112
1.113 @@ -247,45 +252,50 @@
1.114
1.115 \item [@{text "@{text s}"}] prints uninterpreted source text @{text
1.116 s}. This is particularly useful to print portions of text according
1.117 - to the Isabelle {\LaTeX} output style, without demanding
1.118 - well-formedness (e.g.\ small pieces of terms that should not be
1.119 - parsed or type-checked yet).
1.120 + to the Isabelle document style, without demanding well-formedness,
1.121 + e.g.\ small pieces of terms that should not be parsed or
1.122 + type-checked yet.
1.123
1.124 \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
1.125 state. This is mainly for support of tactic-emulation scripts
1.126 - within Isar --- presentation of goal states does not conform to
1.127 - actual human-readable proof documents.
1.128 + within Isar. Presentation of goal states does not conform to the
1.129 + idea of human-readable proof documents!
1.130
1.131 - Please do not include goal states into document output unless you
1.132 - really know what you are doing!
1.133 + When explaining proofs in detail it is usually better to spell out
1.134 + the reasoning via proper Isar proof commands, instead of peeking at
1.135 + the internal machine configuration.
1.136
1.137 \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
1.138 does not print the main goal.
1.139
1.140 - \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact)
1.141 - proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots>
1.142 - a\<^sub>n"}. Note that this requires proof terms to be switched on
1.143 - for the current object logic (see the ``Proof terms'' section of the
1.144 - Isabelle reference manual for information on how to do this).
1.145 + \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact) proof terms
1.146 + corresponding to the theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that this
1.147 + requires proof terms to be switched on for the current logic
1.148 + session.
1.149
1.150 \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
1.151 - "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
1.152 - i.e.\ also displays information omitted in the compact proof term,
1.153 - which is denoted by ``@{text _}'' placeholders there.
1.154 + "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but prints the full proof terms, i.e.\ also
1.155 + displays information omitted in the compact proof term, which is
1.156 + denoted by ``@{text _}'' placeholders there.
1.157
1.158 \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
1.159 "@{ML_struct s}"}] check text @{text s} as ML value, type, and
1.160 - structure, respectively. The source is displayed verbatim.
1.161 + structure, respectively. The source is printed verbatim.
1.162
1.163 \end{descr}
1.164 +*}
1.165
1.166 - \medskip The following standard styles for use with @{text
1.167 - thm_style} and @{text term_style} are available:
1.168 +
1.169 +subsubsection {* Styled antiquotations *}
1.170 +
1.171 +text {* Some antiquotations like @{text thm_style} and @{text
1.172 + term_style} admit an extra \emph{style} specification to modify the
1.173 + printed result. The following standard styles are available:
1.174
1.175 \begin{descr}
1.176
1.177 \item [@{text lhs}] extracts the first argument of any application
1.178 - form with at least two arguments -- typically meta-level or
1.179 + form with at least two arguments --- typically meta-level or
1.180 object-level equality, or any other binary relation.
1.181
1.182 \item [@{text rhs}] is like @{text lhs}, but extracts the second
1.183 @@ -299,10 +309,14 @@
1.184 Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
1.185
1.186 \end{descr}
1.187 +*}
1.188
1.189 - \medskip
1.190 - The following options are available to tune the output. Note that most of
1.191 - these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
1.192 +
1.193 +subsubsection {* General options *}
1.194 +
1.195 +text {* The following options are available to tune the printed output
1.196 + of antiquotations. Note that many of these coincide with global ML
1.197 + flags of the same names.
1.198
1.199 \begin{descr}
1.200
1.201 @@ -333,6 +347,9 @@
1.202 output as multi-line ``display material'', rather than a small piece
1.203 of text without line breaks (which is the default).
1.204
1.205 + In this mode the embedded entities are printed in the same style as
1.206 + the main theory text.
1.207 +
1.208 \item[@{text "break = bool"}] controls line breaks in non-display
1.209 material.
1.210
1.211 @@ -347,29 +364,35 @@
1.212 \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
1.213 margin or indentation for pretty printing of display material.
1.214
1.215 - \item[@{text "source = bool"}] prints the source text of the
1.216 - antiquotation arguments, rather than the actual value. Note that
1.217 - this does not affect well-formedness checks of @{antiquotation
1.218 - "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation
1.219 - "text"} antiquotation admits arbitrary output).
1.220 -
1.221 \item[@{text "goals_limit = nat"}] determines the maximum number of
1.222 - goals to be printed.
1.223 + goals to be printed (for goal-based antiquotation).
1.224
1.225 \item[@{text "locale = name"}] specifies an alternative locale
1.226 context used for evaluating and printing the subsequent argument.
1.227
1.228 + \item[@{text "source = bool"}] prints the original source text of
1.229 + the antiquotation arguments, rather than its internal
1.230 + representation. Note that formal checking of @{antiquotation
1.231 + "thm"}, @{antiquotation "term"}, etc. is still enabled; use the
1.232 + @{antiquotation "text"} antiquotation for unchecked output.
1.233 +
1.234 + Regular @{text "term"} and @{text "typ"} antiquotations with @{text
1.235 + "source = false"} involve a full round-trip from the original source
1.236 + to an internalized logical entity back to a source form, according
1.237 + to the syntax of the current context. Thus the printed output is
1.238 + not under direct control of the author, it may even fluctuate a bit
1.239 + as the underlying theory is changed later on.
1.240 +
1.241 + In contrast, @{text "source = true"} admits direct printing of the
1.242 + given source text, with the desirable well-formedness check in the
1.243 + background, but without modification of the printed text.
1.244 +
1.245 \end{descr}
1.246
1.247 For boolean flags, ``@{text "name = true"}'' may be abbreviated as
1.248 ``@{text name}''. All of the above flags are disabled by default,
1.249 - unless changed from ML.
1.250 -
1.251 - \medskip Note that antiquotations do not only spare the author from
1.252 - tedious typing of logical entities, but also achieve some degree of
1.253 - consistency-checking of informal explanations with formal
1.254 - developments: well-formedness of terms and types with respect to the
1.255 - current theory or proof context is ensured here.
1.256 + unless changed from ML, say in the @{verbatim "ROOT.ML"} of the
1.257 + logic session.
1.258 *}
1.259
1.260