1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/Thy/pure.thy Fri May 02 16:36:05 2008 +0200
1.3 @@ -0,0 +1,1792 @@
1.4 +(* $Id$ *)
1.5 +
1.6 +theory pure
1.7 +imports CPure
1.8 +begin
1.9 +
1.10 +chapter {* Basic language elements \label{ch:pure-syntax} *}
1.11 +
1.12 +text {*
1.13 + Subsequently, we introduce the main part of Pure theory and proof
1.14 + commands, together with fundamental proof methods and attributes.
1.15 + \Chref{ch:gen-tools} describes further Isar elements provided by
1.16 + generic tools and packages (such as the Simplifier) that are either
1.17 + part of Pure Isabelle or pre-installed in most object logics.
1.18 + \Chref{ch:logics} refers to object-logic specific elements (mainly
1.19 + for HOL and ZF).
1.20 +
1.21 + \medskip Isar commands may be either \emph{proper} document
1.22 + constructors, or \emph{improper commands}. Some proof methods and
1.23 + attributes introduced later are classified as improper as well.
1.24 + Improper Isar language elements, which are subsequently marked by
1.25 + ``@{text "\<^sup>*"}'', are often helpful when developing proof
1.26 + documents, while their use is discouraged for the final
1.27 + human-readable outcome. Typical examples are diagnostic commands
1.28 + that print terms or theorems according to the current context; other
1.29 + commands emulate old-style tactical theorem proving.
1.30 +*}
1.31 +
1.32 +
1.33 +section {* Theory commands *}
1.34 +
1.35 +subsection {* Defining theories \label{sec:begin-thy} *}
1.36 +
1.37 +text {*
1.38 + \begin{matharray}{rcl}
1.39 + @{command_def "header"} & : & \isarkeep{toplevel} \\
1.40 + @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
1.41 + @{command_def "end"} & : & \isartrans{theory}{toplevel} \\
1.42 + \end{matharray}
1.43 +
1.44 + Isabelle/Isar theories are defined via theory, which contain both
1.45 + specifications and proofs; occasionally definitional mechanisms also
1.46 + require some explicit proof.
1.47 +
1.48 + The first ``real'' command of any theory has to be @{command
1.49 + "theory"}, which starts a new theory based on the merge of existing
1.50 + ones. Just preceding the @{command "theory"} keyword, there may be
1.51 + an optional @{command "header"} declaration, which is relevant to
1.52 + document preparation only; it acts very much like a special
1.53 + pre-theory markup command (cf.\ \secref{sec:markup-thy} and
1.54 + \secref{sec:markup-thy}). The @{command "end"} command concludes a
1.55 + theory development; it has to be the very last command of any theory
1.56 + file loaded in batch-mode.
1.57 +
1.58 + \begin{rail}
1.59 + 'header' text
1.60 + ;
1.61 + 'theory' name 'imports' (name +) uses? 'begin'
1.62 + ;
1.63 +
1.64 + uses: 'uses' ((name | parname) +);
1.65 + \end{rail}
1.66 +
1.67 + \begin{descr}
1.68 +
1.69 + \item [@{command "header"}~@{text "text"}] provides plain text
1.70 + markup just preceding the formal beginning of a theory. In actual
1.71 + document preparation the corresponding {\LaTeX} macro @{verbatim
1.72 + "\\isamarkupheader"} may be redefined to produce chapter or section
1.73 + headings. See also \secref{sec:markup-thy} and
1.74 + \secref{sec:markup-prf} for further markup commands.
1.75 +
1.76 + \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
1.77 + B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
1.78 + merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
1.79 +
1.80 + Due to inclusion of several ancestors, the overall theory structure
1.81 + emerging in an Isabelle session forms a directed acyclic graph
1.82 + (DAG). Isabelle's theory loader ensures that the sources
1.83 + contributing to the development graph are always up-to-date.
1.84 + Changed files are automatically reloaded when processing theory
1.85 + headers.
1.86 +
1.87 + The optional @{keyword_def "uses"} specification declares additional
1.88 + dependencies on extra files (usually ML sources). Files will be
1.89 + loaded immediately (as ML), unless the name is put in parentheses,
1.90 + which merely documents the dependency to be resolved later in the
1.91 + text (typically via explicit @{command_ref "use"} in the body text,
1.92 + see \secref{sec:ML}).
1.93 +
1.94 + \item [@{command "end"}] concludes the current theory definition or
1.95 + context switch.
1.96 +
1.97 + \end{descr}
1.98 +*}
1.99 +
1.100 +
1.101 +subsection {* Markup commands \label{sec:markup-thy} *}
1.102 +
1.103 +text {*
1.104 + \begin{matharray}{rcl}
1.105 + @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
1.106 + @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
1.107 + @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
1.108 + @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
1.109 + @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
1.110 + @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\
1.111 + \end{matharray}
1.112 +
1.113 + Apart from formal comments (see \secref{sec:comments}), markup
1.114 + commands provide a structured way to insert text into the document
1.115 + generated from a theory (see \cite{isabelle-sys} for more
1.116 + information on Isabelle's document preparation tools).
1.117 +
1.118 + \begin{rail}
1.119 + ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
1.120 + ;
1.121 + 'text\_raw' text
1.122 + ;
1.123 + \end{rail}
1.124 +
1.125 + \begin{descr}
1.126 +
1.127 + \item [@{command "chapter"}, @{command "section"}, @{command
1.128 + "subsection"}, and @{command "subsubsection"}] mark chapter and
1.129 + section headings.
1.130 +
1.131 + \item [@{command "text"}] specifies paragraphs of plain text.
1.132 +
1.133 + \item [@{command "text_raw"}] inserts {\LaTeX} source into the
1.134 + output, without additional markup. Thus the full range of document
1.135 + manipulations becomes available.
1.136 +
1.137 + \end{descr}
1.138 +
1.139 + The @{text "text"} argument of these markup commands (except for
1.140 + @{command "text_raw"}) may contain references to formal entities
1.141 + (``antiquotations'', see also \secref{sec:antiq}). These are
1.142 + interpreted in the present theory context, or the named @{text
1.143 + "target"}.
1.144 +
1.145 + Any of these markup elements corresponds to a {\LaTeX} command with
1.146 + the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning
1.147 + commands this is a plain macro with a single argument, e.g.\
1.148 + @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
1.149 + @{command "chapter"}. The @{command "text"} markup results in a
1.150 + {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"}~@{text
1.151 + "\<dots>"}~@{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
1.152 + causes the text to be inserted directly into the {\LaTeX} source.
1.153 +
1.154 + \medskip Additional markup commands are available for proofs (see
1.155 + \secref{sec:markup-prf}). Also note that the @{command_ref
1.156 + "header"} declaration (see \secref{sec:begin-thy}) admits to insert
1.157 + section markup just preceding the actual theory definition.
1.158 +*}
1.159 +
1.160 +
1.161 +subsection {* Type classes and sorts \label{sec:classes} *}
1.162 +
1.163 +text {*
1.164 + \begin{matharray}{rcll}
1.165 + @{command_def "classes"} & : & \isartrans{theory}{theory} \\
1.166 + @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1.167 + @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
1.168 + @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\
1.169 + \end{matharray}
1.170 +
1.171 + \begin{rail}
1.172 + 'classes' (classdecl +)
1.173 + ;
1.174 + 'classrel' (nameref ('<' | subseteq) nameref + 'and')
1.175 + ;
1.176 + 'defaultsort' sort
1.177 + ;
1.178 + \end{rail}
1.179 +
1.180 + \begin{descr}
1.181 +
1.182 + \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
1.183 + declares class @{text c} to be a subclass of existing classes @{text
1.184 + "c\<^sub>1, \<dots>, c\<^sub>n"}. Cyclic class structures are not permitted.
1.185 +
1.186 + \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states
1.187 + subclass relations between existing classes @{text "c\<^sub>1"} and
1.188 + @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref
1.189 + "instance"} command (see \secref{sec:axclass}) provides a way to
1.190 + introduce proven class relations.
1.191 +
1.192 + \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the
1.193 + new default sort for any type variables given without sort
1.194 + constraints. Usually, the default sort would be only changed when
1.195 + defining a new object-logic.
1.196 +
1.197 + \item [@{command "class_deps"}] visualizes the subclass relation,
1.198 + using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
1.199 +
1.200 + \end{descr}
1.201 +*}
1.202 +
1.203 +
1.204 +subsection {* Primitive types and type abbreviations \label{sec:types-pure} *}
1.205 +
1.206 +text {*
1.207 + \begin{matharray}{rcll}
1.208 + @{command_def "types"} & : & \isartrans{theory}{theory} \\
1.209 + @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
1.210 + @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
1.211 + @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1.212 + \end{matharray}
1.213 +
1.214 + \begin{rail}
1.215 + 'types' (typespec '=' type infix? +)
1.216 + ;
1.217 + 'typedecl' typespec infix?
1.218 + ;
1.219 + 'nonterminals' (name +)
1.220 + ;
1.221 + 'arities' (nameref '::' arity +)
1.222 + ;
1.223 + \end{rail}
1.224 +
1.225 + \begin{descr}
1.226 +
1.227 + \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
1.228 + introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
1.229 + for existing type @{text "\<tau>"}. Unlike actual type definitions, as
1.230 + are available in Isabelle/HOL for example, type synonyms are just
1.231 + purely syntactic abbreviations without any logical significance.
1.232 + Internally, type synonyms are fully expanded.
1.233 +
1.234 + \item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]
1.235 + declares a new type constructor @{text t}, intended as an actual
1.236 + logical type (of the object-logic, if available).
1.237 +
1.238 + \item [@{command "nonterminals"}~@{text c}] declares type
1.239 + constructors @{text c} (without arguments) to act as purely
1.240 + syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
1.241 + syntax of terms or types.
1.242 +
1.243 + \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)
1.244 + s"}] augments Isabelle's order-sorted signature of types by new type
1.245 + constructor arities. This is done axiomatically! The @{command_ref
1.246 + "instance"} command (see \S\ref{sec:axclass}) provides a way to
1.247 + introduce proven type arities.
1.248 +
1.249 + \end{descr}
1.250 +*}
1.251 +
1.252 +
1.253 +subsection {* Primitive constants and definitions \label{sec:consts} *}
1.254 +
1.255 +text {*
1.256 + Definitions essentially express abbreviations within the logic. The
1.257 + simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
1.258 + c} is a newly declared constant. Isabelle also allows derived forms
1.259 + where the arguments of @{text c} appear on the left, abbreviating a
1.260 + prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
1.261 + written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
1.262 + definitions may be weakened by adding arbitrary pre-conditions:
1.263 + @{text "A \<Longrightarrow> c x y \<equiv> t"}.
1.264 +
1.265 + \medskip The built-in well-formedness conditions for definitional
1.266 + specifications are:
1.267 +
1.268 + \begin{itemize}
1.269 +
1.270 + \item Arguments (on the left-hand side) must be distinct variables.
1.271 +
1.272 + \item All variables on the right-hand side must also appear on the
1.273 + left-hand side.
1.274 +
1.275 + \item All type variables on the right-hand side must also appear on
1.276 + the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
1.277 + \<alpha> list)"} for example.
1.278 +
1.279 + \item The definition must not be recursive. Most object-logics
1.280 + provide definitional principles that can be used to express
1.281 + recursion safely.
1.282 +
1.283 + \end{itemize}
1.284 +
1.285 + Overloading means that a constant being declared as @{text "c :: \<alpha>
1.286 + decl"} may be defined separately on type instances @{text "c ::
1.287 + (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
1.288 + t}. The right-hand side may mention overloaded constants
1.289 + recursively at type instances corresponding to the immediate
1.290 + argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
1.291 + specification patterns impose global constraints on all occurrences,
1.292 + e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
1.293 + corresponding occurrences on some right-hand side need to be an
1.294 + instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1.295 +
1.296 + \begin{matharray}{rcl}
1.297 + @{command_def "consts"} & : & \isartrans{theory}{theory} \\
1.298 + @{command_def "defs"} & : & \isartrans{theory}{theory} \\
1.299 + @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
1.300 + \end{matharray}
1.301 +
1.302 + \begin{rail}
1.303 + 'consts' ((name '::' type mixfix?) +)
1.304 + ;
1.305 + 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1.306 + ;
1.307 + \end{rail}
1.308 +
1.309 + \begin{rail}
1.310 + 'constdefs' structs? (constdecl? constdef +)
1.311 + ;
1.312 +
1.313 + structs: '(' 'structure' (vars + 'and') ')'
1.314 + ;
1.315 + constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1.316 + ;
1.317 + constdef: thmdecl? prop
1.318 + ;
1.319 + \end{rail}
1.320 +
1.321 + \begin{descr}
1.322 +
1.323 + \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
1.324 + @{text c} to have any instance of type scheme @{text \<sigma>}. The
1.325 + optional mixfix annotations may attach concrete syntax to the
1.326 + constants declared.
1.327 +
1.328 + \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}
1.329 + as a definitional axiom for some existing constant.
1.330 +
1.331 + The @{text "(unchecked)"} option disables global dependency checks
1.332 + for this definition, which is occasionally useful for exotic
1.333 + overloading. It is at the discretion of the user to avoid malformed
1.334 + theory specifications!
1.335 +
1.336 + The @{text "(overloaded)"} option declares definitions to be
1.337 + potentially overloaded. Unless this option is given, a warning
1.338 + message would be issued for any definitional equation with a more
1.339 + special type than that of the corresponding constant declaration.
1.340 +
1.341 + \item [@{command "constdefs"}] provides a streamlined combination of
1.342 + constants declarations and definitions: type-inference takes care of
1.343 + the most general typing of the given specification (the optional
1.344 + type constraint may refer to type-inference dummies ``@{verbatim
1.345 + _}'' as usual). The resulting type declaration needs to agree with
1.346 + that of the specification; overloading is \emph{not} supported here!
1.347 +
1.348 + The constant name may be omitted altogether, if neither type nor
1.349 + syntax declarations are given. The canonical name of the
1.350 + definitional axiom for constant @{text c} will be @{text c_def},
1.351 + unless specified otherwise. Also note that the given list of
1.352 + specifications is processed in a strictly sequential manner, with
1.353 + type-checking being performed independently.
1.354 +
1.355 + An optional initial context of @{text "(structure)"} declarations
1.356 + admits use of indexed syntax, using the special symbol @{verbatim
1.357 + "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
1.358 + particularly useful with locales (see also \S\ref{sec:locale}).
1.359 +
1.360 + \end{descr}
1.361 +*}
1.362 +
1.363 +
1.364 +subsection {* Syntax and translations \label{sec:syn-trans} *}
1.365 +
1.366 +text {*
1.367 + \begin{matharray}{rcl}
1.368 + @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
1.369 + @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
1.370 + @{command_def "translations"} & : & \isartrans{theory}{theory} \\
1.371 + @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
1.372 + \end{matharray}
1.373 +
1.374 + \railalias{rightleftharpoons}{\isasymrightleftharpoons}
1.375 + \railterm{rightleftharpoons}
1.376 +
1.377 + \railalias{rightharpoonup}{\isasymrightharpoonup}
1.378 + \railterm{rightharpoonup}
1.379 +
1.380 + \railalias{leftharpoondown}{\isasymleftharpoondown}
1.381 + \railterm{leftharpoondown}
1.382 +
1.383 + \begin{rail}
1.384 + ('syntax' | 'no\_syntax') mode? (constdecl +)
1.385 + ;
1.386 + ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
1.387 + ;
1.388 +
1.389 + mode: ('(' ( name | 'output' | name 'output' ) ')')
1.390 + ;
1.391 + transpat: ('(' nameref ')')? string
1.392 + ;
1.393 + \end{rail}
1.394 +
1.395 + \begin{descr}
1.396 +
1.397 + \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to
1.398 + @{command "consts"}~@{text decls}, except that the actual logical
1.399 + signature extension is omitted. Thus the context free grammar of
1.400 + Isabelle's inner syntax may be augmented in arbitrary ways,
1.401 + independently of the logic. The @{text mode} argument refers to the
1.402 + print mode that the grammar rules belong; unless the @{keyword_ref
1.403 + "output"} indicator is given, all productions are added both to the
1.404 + input and output grammar.
1.405 +
1.406 + \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes
1.407 + grammar declarations (and translations) resulting from @{text
1.408 + decls}, which are interpreted in the same manner as for @{command
1.409 + "syntax"} above.
1.410 +
1.411 + \item [@{command "translations"}~@{text rules}] specifies syntactic
1.412 + translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
1.413 + parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
1.414 + Translation patterns may be prefixed by the syntactic category to be
1.415 + used for parsing; the default is @{text logic}.
1.416 +
1.417 + \item [@{command "no_translations"}~@{text rules}] removes syntactic
1.418 + translation rules, which are interpreted in the same manner as for
1.419 + @{command "translations"} above.
1.420 +
1.421 + \end{descr}
1.422 +*}
1.423 +
1.424 +
1.425 +subsection {* Axioms and theorems \label{sec:axms-thms} *}
1.426 +
1.427 +text {*
1.428 + \begin{matharray}{rcll}
1.429 + @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1.430 + @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
1.431 + @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\
1.432 + \end{matharray}
1.433 +
1.434 + \begin{rail}
1.435 + 'axioms' (axmdecl prop +)
1.436 + ;
1.437 + ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1.438 + ;
1.439 + \end{rail}
1.440 +
1.441 + \begin{descr}
1.442 +
1.443 + \item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary
1.444 + statements as axioms of the meta-logic. In fact, axioms are
1.445 + ``axiomatic theorems'', and may be referred later just as any other
1.446 + theorem.
1.447 +
1.448 + Axioms are usually only introduced when declaring new logical
1.449 + systems. Everyday work is typically done the hard way, with proper
1.450 + definitions and proven theorems.
1.451 +
1.452 + \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
1.453 + retrieves and stores existing facts in the theory context, or the
1.454 + specified target context (see also \secref{sec:target}). Typical
1.455 + applications would also involve attributes, to declare Simplifier
1.456 + rules, for example.
1.457 +
1.458 + \item [@{command "theorems"}] is essentially the same as @{command
1.459 + "lemmas"}, but marks the result as a different kind of facts.
1.460 +
1.461 + \end{descr}
1.462 +*}
1.463 +
1.464 +
1.465 +subsection {* Name spaces *}
1.466 +
1.467 +text {*
1.468 + \begin{matharray}{rcl}
1.469 + @{command_def "global"} & : & \isartrans{theory}{theory} \\
1.470 + @{command_def "local"} & : & \isartrans{theory}{theory} \\
1.471 + @{command_def "hide"} & : & \isartrans{theory}{theory} \\
1.472 + \end{matharray}
1.473 +
1.474 + \begin{rail}
1.475 + 'hide' ('(open)')? name (nameref + )
1.476 + ;
1.477 + \end{rail}
1.478 +
1.479 + Isabelle organizes any kind of name declarations (of types,
1.480 + constants, theorems etc.) by separate hierarchically structured name
1.481 + spaces. Normally the user does not have to control the behavior of
1.482 + name spaces by hand, yet the following commands provide some way to
1.483 + do so.
1.484 +
1.485 + \begin{descr}
1.486 +
1.487 + \item [@{command "global"} and @{command "local"}] change the
1.488 + current name declaration mode. Initially, theories start in
1.489 + @{command "local"} mode, causing all names to be automatically
1.490 + qualified by the theory name. Changing this to @{command "global"}
1.491 + causes all names to be declared without the theory prefix, until
1.492 + @{command "local"} is declared again.
1.493 +
1.494 + Note that global names are prone to get hidden accidently later,
1.495 + when qualified names of the same base name are introduced.
1.496 +
1.497 + \item [@{command "hide"}~@{text "space names"}] fully removes
1.498 + declarations from a given name space (which may be @{text "class"},
1.499 + @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
1.500 + "(open)"} option, only the base name is hidden. Global
1.501 + (unqualified) names may never be hidden.
1.502 +
1.503 + Note that hiding name space accesses has no impact on logical
1.504 + declarations -- they remain valid internally. Entities that are no
1.505 + longer accessible to the user are printed with the special qualifier
1.506 + ``@{text "??"}'' prefixed to the full internal name.
1.507 +
1.508 + \end{descr}
1.509 +*}
1.510 +
1.511 +
1.512 +subsection {* Incorporating ML code \label{sec:ML} *}
1.513 +
1.514 +text {*
1.515 + \begin{matharray}{rcl}
1.516 + @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
1.517 + @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
1.518 + @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
1.519 + @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
1.520 + @{command_def "setup"} & : & \isartrans{theory}{theory} \\
1.521 + @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
1.522 + \end{matharray}
1.523 +
1.524 + \begin{rail}
1.525 + 'use' name
1.526 + ;
1.527 + ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
1.528 + ;
1.529 + 'method\_setup' name '=' text text
1.530 + ;
1.531 + \end{rail}
1.532 +
1.533 + \begin{descr}
1.534 +
1.535 + \item [@{command "use"}~@{text "file"}] reads and executes ML
1.536 + commands from @{text "file"}. The current theory context is passed
1.537 + down to the ML toplevel and may be modified, using @{ML
1.538 + "Context.>>"} or derived ML commands. The file name is checked with
1.539 + the @{keyword_ref "uses"} dependency declaration given in the theory
1.540 + header (see also \secref{sec:begin-thy}).
1.541 +
1.542 + \item [@{command "ML"}~@{text "text"}] is similar to @{command
1.543 + "use"}, but executes ML commands directly from the given @{text
1.544 + "text"}.
1.545 +
1.546 + \item [@{command "ML_val"} and @{command "ML_command"}] are
1.547 + diagnostic versions of @{command "ML"}, which means that the context
1.548 + may not be updated. @{command "ML_val"} echos the bindings produced
1.549 + at the ML toplevel, but @{command "ML_command"} is silent.
1.550 +
1.551 + \item [@{command "setup"}~@{text "text"}] changes the current theory
1.552 + context by applying @{text "text"}, which refers to an ML expression
1.553 + of type @{ML_type "theory -> theory"}. This enables to initialize
1.554 + any object-logic specific tools and packages written in ML, for
1.555 + example.
1.556 +
1.557 + \item [@{command "method_setup"}~@{text "name = text description"}]
1.558 + defines a proof method in the current theory. The given @{text
1.559 + "text"} has to be an ML expression of type @{ML_type "Args.src ->
1.560 + Proof.context -> Proof.method"}. Parsing concrete method syntax
1.561 + from @{ML_type Args.src} input can be quite tedious in general. The
1.562 + following simple examples are for methods without any explicit
1.563 + arguments, or a list of theorems, respectively.
1.564 +
1.565 +%FIXME proper antiquotations
1.566 +{\footnotesize
1.567 +\begin{verbatim}
1.568 + Method.no_args (Method.METHOD (fn facts => foobar_tac))
1.569 + Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
1.570 + Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
1.571 + Method.thms_ctxt_args (fn thms => fn ctxt =>
1.572 + Method.METHOD (fn facts => foobar_tac))
1.573 +\end{verbatim}
1.574 +}
1.575 +
1.576 + Note that mere tactic emulations may ignore the @{text facts}
1.577 + parameter above. Proper proof methods would do something
1.578 + appropriate with the list of current facts, though. Single-rule
1.579 + methods usually do strict forward-chaining (e.g.\ by using @{ML
1.580 + Drule.multi_resolves}), while automatic ones just insert the facts
1.581 + using @{ML Method.insert_tac} before applying the main tactic.
1.582 +
1.583 + \end{descr}
1.584 +*}
1.585 +
1.586 +
1.587 +subsection {* Syntax translation functions *}
1.588 +
1.589 +text {*
1.590 + \begin{matharray}{rcl}
1.591 + @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
1.592 + @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
1.593 + @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
1.594 + @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
1.595 + @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
1.596 + @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
1.597 + \end{matharray}
1.598 +
1.599 + \begin{rail}
1.600 + ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
1.601 + 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
1.602 + ;
1.603 +
1.604 + 'token\_translation' text
1.605 + ;
1.606 + \end{rail}
1.607 +
1.608 + Syntax translation functions written in ML admit almost arbitrary
1.609 + manipulations of Isabelle's inner syntax. Any of the above commands
1.610 + have a single \railqtok{text} argument that refers to an ML
1.611 + expression of appropriate type, which are as follows by default:
1.612 +
1.613 +%FIXME proper antiquotations
1.614 +\begin{ttbox}
1.615 +val parse_ast_translation : (string * (ast list -> ast)) list
1.616 +val parse_translation : (string * (term list -> term)) list
1.617 +val print_translation : (string * (term list -> term)) list
1.618 +val typed_print_translation :
1.619 + (string * (bool -> typ -> term list -> term)) list
1.620 +val print_ast_translation : (string * (ast list -> ast)) list
1.621 +val token_translation :
1.622 + (string * string * (string -> string * real)) list
1.623 +\end{ttbox}
1.624 +
1.625 + If the @{text "(advanced)"} option is given, the corresponding
1.626 + translation functions may depend on the current theory or proof
1.627 + context. This allows to implement advanced syntax mechanisms, as
1.628 + translations functions may refer to specific theory declarations or
1.629 + auxiliary proof data.
1.630 +
1.631 + See also \cite[\S8]{isabelle-ref} for more information on the
1.632 + general concept of syntax transformations in Isabelle.
1.633 +
1.634 +%FIXME proper antiquotations
1.635 +\begin{ttbox}
1.636 +val parse_ast_translation:
1.637 + (string * (Context.generic -> ast list -> ast)) list
1.638 +val parse_translation:
1.639 + (string * (Context.generic -> term list -> term)) list
1.640 +val print_translation:
1.641 + (string * (Context.generic -> term list -> term)) list
1.642 +val typed_print_translation:
1.643 + (string * (Context.generic -> bool -> typ -> term list -> term)) list
1.644 +val print_ast_translation:
1.645 + (string * (Context.generic -> ast list -> ast)) list
1.646 +\end{ttbox}
1.647 +*}
1.648 +
1.649 +
1.650 +subsection {* Oracles *}
1.651 +
1.652 +text {*
1.653 + \begin{matharray}{rcl}
1.654 + @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
1.655 + \end{matharray}
1.656 +
1.657 + The oracle interface promotes a given ML function @{ML_text
1.658 + "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some type
1.659 + @{ML_text T} given by the user. This acts like an infinitary
1.660 + specification of axioms -- there is no internal check of the
1.661 + correctness of the results! The inference kernel records oracle
1.662 + invocations within the internal derivation object of theorems, and
1.663 + the pretty printer attaches ``@{text "[!]"}'' to indicate results
1.664 + that are not fully checked by Isabelle inferences.
1.665 +
1.666 + \begin{rail}
1.667 + 'oracle' name '(' type ')' '=' text
1.668 + ;
1.669 + \end{rail}
1.670 +
1.671 + \begin{descr}
1.672 +
1.673 + \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
1.674 + given ML expression @{text "text"} of type @{ML_text "{theory
1.675 + ->"}~@{text "type"}~@{ML_text "-> term"} into an ML function
1.676 + @{ML_text name} of type @{ML_text "{theory ->"}~@{text
1.677 + "type"}~@{ML_text "-> thm"}.
1.678 +
1.679 + \end{descr}
1.680 +*}
1.681 +
1.682 +
1.683 +section {* Proof commands *}
1.684 +
1.685 +text {*
1.686 + Proof commands perform transitions of Isar/VM machine
1.687 + configurations, which are block-structured, consisting of a stack of
1.688 + nodes with three main components: logical proof context, current
1.689 + facts, and open goals. Isar/VM transitions are \emph{typed}
1.690 + according to the following three different modes of operation:
1.691 +
1.692 + \begin{descr}
1.693 +
1.694 + \item [@{text "proof(prove)"}] means that a new goal has just been
1.695 + stated that is now to be \emph{proven}; the next command may refine
1.696 + it by some proof method, and enter a sub-proof to establish the
1.697 + actual result.
1.698 +
1.699 + \item [@{text "proof(state)"}] is like a nested theory mode: the
1.700 + context may be augmented by \emph{stating} additional assumptions,
1.701 + intermediate results etc.
1.702 +
1.703 + \item [@{text "proof(chain)"}] is intermediate between @{text
1.704 + "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
1.705 + the contents of the special ``@{fact_ref this}'' register) have been
1.706 + just picked up in order to be used when refining the goal claimed
1.707 + next.
1.708 +
1.709 + \end{descr}
1.710 +
1.711 + The proof mode indicator may be read as a verb telling the writer
1.712 + what kind of operation may be performed next. The corresponding
1.713 + typings of proof commands restricts the shape of well-formed proof
1.714 + texts to particular command sequences. So dynamic arrangements of
1.715 + commands eventually turn out as static texts of a certain structure.
1.716 + \Appref{ap:refcard} gives a simplified grammar of the overall
1.717 + (extensible) language emerging that way.
1.718 +*}
1.719 +
1.720 +
1.721 +subsection {* Markup commands \label{sec:markup-prf} *}
1.722 +
1.723 +text {*
1.724 + \begin{matharray}{rcl}
1.725 + @{command_def "sect"} & : & \isartrans{proof}{proof} \\
1.726 + @{command_def "subsect"} & : & \isartrans{proof}{proof} \\
1.727 + @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
1.728 + @{command_def "txt"} & : & \isartrans{proof}{proof} \\
1.729 + @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
1.730 + \end{matharray}
1.731 +
1.732 + These markup commands for proof mode closely correspond to the ones
1.733 + of theory mode (see \S\ref{sec:markup-thy}).
1.734 +
1.735 + \begin{rail}
1.736 + ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
1.737 + ;
1.738 + \end{rail}
1.739 +*}
1.740 +
1.741 +
1.742 +subsection {* Context elements \label{sec:proof-context} *}
1.743 +
1.744 +text {*
1.745 + \begin{matharray}{rcl}
1.746 + @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
1.747 + @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
1.748 + @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
1.749 + @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
1.750 + \end{matharray}
1.751 +
1.752 + The logical proof context consists of fixed variables and
1.753 + assumptions. The former closely correspond to Skolem constants, or
1.754 + meta-level universal quantification as provided by the Isabelle/Pure
1.755 + logical framework. Introducing some \emph{arbitrary, but fixed}
1.756 + variable via ``@{command "fix"}~@{text x} results in a local value
1.757 + that may be used in the subsequent proof as any other variable or
1.758 + constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
1.759 + the context will be universally closed wrt.\ @{text x} at the
1.760 + outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
1.761 + form using Isabelle's meta-variables).
1.762 +
1.763 + Similarly, introducing some assumption @{text \<chi>} has two effects.
1.764 + On the one hand, a local theorem is created that may be used as a
1.765 + fact in subsequent proof steps. On the other hand, any result
1.766 + @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
1.767 + the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
1.768 + using such a result would basically introduce a new subgoal stemming
1.769 + from the assumption. How this situation is handled depends on the
1.770 + version of assumption command used: while @{command "assume"}
1.771 + insists on solving the subgoal by unification with some premise of
1.772 + the goal, @{command "presume"} leaves the subgoal unchanged in order
1.773 + to be proved later by the user.
1.774 +
1.775 + Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
1.776 + t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
1.777 + another version of assumption that causes any hypothetical equation
1.778 + @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
1.779 + exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
1.780 + \<phi>[t]"}.
1.781 +
1.782 + \railalias{equiv}{\isasymequiv}
1.783 + \railterm{equiv}
1.784 +
1.785 + \begin{rail}
1.786 + 'fix' (vars + 'and')
1.787 + ;
1.788 + ('assume' | 'presume') (props + 'and')
1.789 + ;
1.790 + 'def' (def + 'and')
1.791 + ;
1.792 + def: thmdecl? \\ name ('==' | equiv) term termpat?
1.793 + ;
1.794 + \end{rail}
1.795 +
1.796 + \begin{descr}
1.797 +
1.798 + \item [@{command "fix"}~@{text x}] introduces a local variable
1.799 + @{text x} that is \emph{arbitrary, but fixed.}
1.800 +
1.801 + \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
1.802 + "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
1.803 + assumption. Subsequent results applied to an enclosing goal (e.g.\
1.804 + by @{command_ref "show"}) are handled as follows: @{command
1.805 + "assume"} expects to be able to unify with existing premises in the
1.806 + goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
1.807 +
1.808 + Several lists of assumptions may be given (separated by
1.809 + @{keyword_ref "and"}; the resulting list of current facts consists
1.810 + of all of these concatenated.
1.811 +
1.812 + \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
1.813 + (non-polymorphic) definition. In results exported from the context,
1.814 + @{text x} is replaced by @{text t}. Basically, ``@{command
1.815 + "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
1.816 + x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
1.817 + hypothetical equation solved by reflexivity.
1.818 +
1.819 + The default name for the definitional equation is @{text x_def}.
1.820 + Several simultaneous definitions may be given at the same time.
1.821 +
1.822 + \end{descr}
1.823 +
1.824 + The special name @{fact_ref prems} refers to all assumptions of the
1.825 + current context as a list of theorems. This feature should be used
1.826 + with great care! It is better avoided in final proof texts.
1.827 +*}
1.828 +
1.829 +
1.830 +subsection {* Facts and forward chaining *}
1.831 +
1.832 +text {*
1.833 + \begin{matharray}{rcl}
1.834 + @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
1.835 + @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
1.836 + @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
1.837 + @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
1.838 + @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
1.839 + @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
1.840 + \end{matharray}
1.841 +
1.842 + New facts are established either by assumption or proof of local
1.843 + statements. Any fact will usually be involved in further proofs,
1.844 + either as explicit arguments of proof methods, or when forward
1.845 + chaining towards the next goal via @{command "then"} (and variants);
1.846 + @{command "from"} and @{command "with"} are composite forms
1.847 + involving @{command "note"}. The @{command "using"} elements
1.848 + augments the collection of used facts \emph{after} a goal has been
1.849 + stated. Note that the special theorem name @{fact_ref this} refers
1.850 + to the most recently established facts, but only \emph{before}
1.851 + issuing a follow-up claim.
1.852 +
1.853 + \begin{rail}
1.854 + 'note' (thmdef? thmrefs + 'and')
1.855 + ;
1.856 + ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
1.857 + ;
1.858 + \end{rail}
1.859 +
1.860 + \begin{descr}
1.861 +
1.862 + \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
1.863 + recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
1.864 + the result as @{text a}. Note that attributes may be involved as
1.865 + well, both on the left and right hand sides.
1.866 +
1.867 + \item [@{command "then"}] indicates forward chaining by the current
1.868 + facts in order to establish the goal to be claimed next. The
1.869 + initial proof method invoked to refine that will be offered the
1.870 + facts to do ``anything appropriate'' (see also
1.871 + \secref{sec:proof-steps}). For example, method @{method_ref rule}
1.872 + (see \secref{sec:pure-meth-att}) would typically do an elimination
1.873 + rather than an introduction. Automatic methods usually insert the
1.874 + facts into the goal state before operation. This provides a simple
1.875 + scheme to control relevance of facts in automated proof search.
1.876 +
1.877 + \item [@{command "from"}~@{text b}] abbreviates ``@{command
1.878 + "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
1.879 + equivalent to ``@{command "from"}~@{text this}''.
1.880 +
1.881 + \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
1.882 + abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
1.883 + this"}''; thus the forward chaining is from earlier facts together
1.884 + with the current ones.
1.885 +
1.886 + \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
1.887 + the facts being currently indicated for use by a subsequent
1.888 + refinement step (such as @{command_ref "apply"} or @{command_ref
1.889 + "proof"}).
1.890 +
1.891 + \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
1.892 + structurally similar to @{command "using"}, but unfolds definitional
1.893 + equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
1.894 + and facts.
1.895 +
1.896 + \end{descr}
1.897 +
1.898 + Forward chaining with an empty list of theorems is the same as not
1.899 + chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
1.900 + effect apart from entering @{text "prove(chain)"} mode, since
1.901 + @{fact_ref nothing} is bound to the empty list of theorems.
1.902 +
1.903 + Basic proof methods (such as @{method_ref rule}) expect multiple
1.904 + facts to be given in their proper order, corresponding to a prefix
1.905 + of the premises of the rule involved. Note that positions may be
1.906 + easily skipped using something like @{command "from"}~@{text "_
1.907 + \<AND> a \<AND> b"}, for example. This involves the trivial rule
1.908 + @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
1.909 + ``@{fact_ref "_"}'' (underscore).
1.910 +
1.911 + Automated methods (such as @{method simp} or @{method auto}) just
1.912 + insert any given facts before their usual operation. Depending on
1.913 + the kind of procedure involved, the order of facts is less
1.914 + significant here.
1.915 +*}
1.916 +
1.917 +
1.918 +subsection {* Goal statements \label{sec:goals} *}
1.919 +
1.920 +text {*
1.921 + \begin{matharray}{rcl}
1.922 + \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
1.923 + \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
1.924 + \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
1.925 + \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
1.926 + \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
1.927 + \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
1.928 + \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
1.929 + \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
1.930 + \end{matharray}
1.931 +
1.932 + From a theory context, proof mode is entered by an initial goal
1.933 + command such as @{command "lemma"}, @{command "theorem"}, or
1.934 + @{command "corollary"}. Within a proof, new claims may be
1.935 + introduced locally as well; four variants are available here to
1.936 + indicate whether forward chaining of facts should be performed
1.937 + initially (via @{command_ref "then"}), and whether the final result
1.938 + is meant to solve some pending goal.
1.939 +
1.940 + Goals may consist of multiple statements, resulting in a list of
1.941 + facts eventually. A pending multi-goal is internally represented as
1.942 + a meta-level conjunction (printed as @{text "&&"}), which is usually
1.943 + split into the corresponding number of sub-goals prior to an initial
1.944 + method application, via @{command_ref "proof"}
1.945 + (\secref{sec:proof-steps}) or @{command_ref "apply"}
1.946 + (\secref{sec:tactic-commands}). The @{method_ref induct} method
1.947 + covered in \secref{sec:cases-induct} acts on multiple claims
1.948 + simultaneously.
1.949 +
1.950 + Claims at the theory level may be either in short or long form. A
1.951 + short goal merely consists of several simultaneous propositions
1.952 + (often just one). A long goal includes an explicit context
1.953 + specification for the subsequent conclusion, involving local
1.954 + parameters and assumptions. Here the role of each part of the
1.955 + statement is explicitly marked by separate keywords (see also
1.956 + \secref{sec:locale}); the local assumptions being introduced here
1.957 + are available as @{fact_ref assms} in the proof. Moreover, there
1.958 + are two kinds of conclusions: @{element_def "shows"} states several
1.959 + simultaneous propositions (essentially a big conjunction), while
1.960 + @{element_def "obtains"} claims several simultaneous simultaneous
1.961 + contexts of (essentially a big disjunction of eliminated parameters
1.962 + and assumptions, cf.\ \secref{sec:obtain}).
1.963 +
1.964 + \begin{rail}
1.965 + ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
1.966 + ;
1.967 + ('have' | 'show' | 'hence' | 'thus') goal
1.968 + ;
1.969 + 'print\_statement' modes? thmrefs
1.970 + ;
1.971 +
1.972 + goal: (props + 'and')
1.973 + ;
1.974 + longgoal: thmdecl? (contextelem *) conclusion
1.975 + ;
1.976 + conclusion: 'shows' goal | 'obtains' (parname? case + '|')
1.977 + ;
1.978 + case: (vars + 'and') 'where' (props + 'and')
1.979 + ;
1.980 + \end{rail}
1.981 +
1.982 + \begin{descr}
1.983 +
1.984 + \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
1.985 + @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
1.986 + \<phi>"} to be put back into the target context. An additional
1.987 + \railnonterm{context} specification may build up an initial proof
1.988 + context for the subsequent claim; this includes local definitions
1.989 + and syntax as well, see the definition of @{syntax contextelem} in
1.990 + \secref{sec:locale}.
1.991 +
1.992 + \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
1.993 + "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
1.994 + "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
1.995 + being of a different kind. This discrimination acts like a formal
1.996 + comment.
1.997 +
1.998 + \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
1.999 + eventually resulting in a fact within the current logical context.
1.1000 + This operation is completely independent of any pending sub-goals of
1.1001 + an enclosing goal statements, so @{command "have"} may be freely
1.1002 + used for experimental exploration of potential results within a
1.1003 + proof body.
1.1004 +
1.1005 + \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
1.1006 + "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
1.1007 + sub-goal for each one of the finished result, after having been
1.1008 + exported into the corresponding context (at the head of the
1.1009 + sub-proof of this @{command "show"} command).
1.1010 +
1.1011 + To accommodate interactive debugging, resulting rules are printed
1.1012 + before being applied internally. Even more, interactive execution
1.1013 + of @{command "show"} predicts potential failure and displays the
1.1014 + resulting error as a warning beforehand. Watch out for the
1.1015 + following message:
1.1016 +
1.1017 + %FIXME proper antiquitation
1.1018 + \begin{ttbox}
1.1019 + Problem! Local statement will fail to solve any pending goal
1.1020 + \end{ttbox}
1.1021 +
1.1022 + \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
1.1023 + "have"}'', i.e.\ claims a local goal to be proven by forward
1.1024 + chaining the current facts. Note that @{command "hence"} is also
1.1025 + equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
1.1026 +
1.1027 + \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
1.1028 + "show"}''. Note that @{command "thus"} is also equivalent to
1.1029 + ``@{command "from"}~@{text this}~@{command "show"}''.
1.1030 +
1.1031 + \item [@{command "print_statement"}~@{text a}] prints facts from the
1.1032 + current theory or proof context in long statement form, according to
1.1033 + the syntax for @{command "lemma"} given above.
1.1034 +
1.1035 + \end{descr}
1.1036 +
1.1037 + Any goal statement causes some term abbreviations (such as
1.1038 + @{variable_ref "?thesis"}) to be bound automatically, see also
1.1039 + \secref{sec:term-abbrev}. Furthermore, the local context of a
1.1040 + (non-atomic) goal is provided via the @{case_ref rule_context} case.
1.1041 +
1.1042 + The optional case names of @{element_ref "obtains"} have a twofold
1.1043 + meaning: (1) during the of this claim they refer to the the local
1.1044 + context introductions, (2) the resulting rule is annotated
1.1045 + accordingly to support symbolic case splits when used with the
1.1046 + @{method_ref cases} method (cf. \secref{sec:cases-induct}).
1.1047 +
1.1048 + \medskip
1.1049 +
1.1050 + \begin{warn}
1.1051 + Isabelle/Isar suffers theory-level goal statements to contain
1.1052 + \emph{unbound schematic variables}, although this does not conform
1.1053 + to the aim of human-readable proof documents! The main problem
1.1054 + with schematic goals is that the actual outcome is usually hard to
1.1055 + predict, depending on the behavior of the proof methods applied
1.1056 + during the course of reasoning. Note that most semi-automated
1.1057 + methods heavily depend on several kinds of implicit rule
1.1058 + declarations within the current theory context. As this would
1.1059 + also result in non-compositional checking of sub-proofs,
1.1060 + \emph{local goals} are not allowed to be schematic at all.
1.1061 + Nevertheless, schematic goals do have their use in Prolog-style
1.1062 + interactive synthesis of proven results, usually by stepwise
1.1063 + refinement via emulation of traditional Isabelle tactic scripts
1.1064 + (see also \secref{sec:tactic-commands}). In any case, users
1.1065 + should know what they are doing.
1.1066 + \end{warn}
1.1067 +*}
1.1068 +
1.1069 +
1.1070 +subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
1.1071 +
1.1072 +text {*
1.1073 + \begin{matharray}{rcl}
1.1074 + @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
1.1075 + @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
1.1076 + @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1.1077 + @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1.1078 + @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1.1079 + @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
1.1080 + \end{matharray}
1.1081 +
1.1082 + Arbitrary goal refinement via tactics is considered harmful.
1.1083 + Structured proof composition in Isar admits proof methods to be
1.1084 + invoked in two places only.
1.1085 +
1.1086 + \begin{enumerate}
1.1087 +
1.1088 + \item An \emph{initial} refinement step @{command_ref
1.1089 + "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
1.1090 + of sub-goals that are to be solved later. Facts are passed to
1.1091 + @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
1.1092 + "proof(chain)"} mode.
1.1093 +
1.1094 + \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
1.1095 + "m\<^sub>2"} is intended to solve remaining goals. No facts are
1.1096 + passed to @{text "m\<^sub>2"}.
1.1097 +
1.1098 + \end{enumerate}
1.1099 +
1.1100 + The only other (proper) way to affect pending goals in a proof body
1.1101 + is by @{command_ref "show"}, which involves an explicit statement of
1.1102 + what is to be solved eventually. Thus we avoid the fundamental
1.1103 + problem of unstructured tactic scripts that consist of numerous
1.1104 + consecutive goal transformations, with invisible effects.
1.1105 +
1.1106 + \medskip As a general rule of thumb for good proof style, initial
1.1107 + proof methods should either solve the goal completely, or constitute
1.1108 + some well-understood reduction to new sub-goals. Arbitrary
1.1109 + automatic proof tools that are prone leave a large number of badly
1.1110 + structured sub-goals are no help in continuing the proof document in
1.1111 + an intelligible manner.
1.1112 +
1.1113 + Unless given explicitly by the user, the default initial method is
1.1114 + ``@{method_ref rule}'', which applies a single standard elimination
1.1115 + or introduction rule according to the topmost symbol involved.
1.1116 + There is no separate default terminal method. Any remaining goals
1.1117 + are always solved by assumption in the very last step.
1.1118 +
1.1119 + \begin{rail}
1.1120 + 'proof' method?
1.1121 + ;
1.1122 + 'qed' method?
1.1123 + ;
1.1124 + 'by' method method?
1.1125 + ;
1.1126 + ('.' | '..' | 'sorry')
1.1127 + ;
1.1128 + \end{rail}
1.1129 +
1.1130 + \begin{descr}
1.1131 +
1.1132 + \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
1.1133 + proof method @{text "m\<^sub>1"}; facts for forward chaining are
1.1134 + passed if so indicated by @{text "proof(chain)"} mode.
1.1135 +
1.1136 + \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
1.1137 + goals by proof method @{text "m\<^sub>2"} and concludes the
1.1138 + sub-proof by assumption. If the goal had been @{text "show"} (or
1.1139 + @{text "thus"}), some pending sub-goal is solved as well by the rule
1.1140 + resulting from the result \emph{exported} into the enclosing goal
1.1141 + context. Thus @{text "qed"} may fail for two reasons: either @{text
1.1142 + "m\<^sub>2"} fails, or the resulting rule does not fit to any
1.1143 + pending goal\footnote{This includes any additional ``strong''
1.1144 + assumptions as introduced by @{text "assume"}.} of the enclosing
1.1145 + context. Debugging such a situation might involve temporarily
1.1146 + changing @{command "show"} into @{command "have"}, or weakening the
1.1147 + local context by replacing occurrences of @{command "assume"} by
1.1148 + @{command "presume"}.
1.1149 +
1.1150 + \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
1.1151 + \emph{terminal proof}\index{proof!terminal}; it abbreviates
1.1152 + @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
1.1153 + "m\<^sub>2"}, but with backtracking across both methods. Debugging
1.1154 + an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
1.1155 + command can be done by expanding its definition; in many cases
1.1156 + @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
1.1157 + "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
1.1158 + problem.
1.1159 +
1.1160 + \item [``@{command ".."}''] is a \emph{default
1.1161 + proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
1.1162 + "rule"}.
1.1163 +
1.1164 + \item [``@{command "."}''] is a \emph{trivial
1.1165 + proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
1.1166 + "this"}.
1.1167 +
1.1168 + \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
1.1169 + pretending to solve the pending claim without further ado. This
1.1170 + only works in interactive development, or if the @{ML
1.1171 + quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
1.1172 + proofs are not the real thing. Internally, each theorem container
1.1173 + is tainted by an oracle invocation, which is indicated as ``@{text
1.1174 + "[!]"}'' in the printed result.
1.1175 +
1.1176 + The most important application of @{command "sorry"} is to support
1.1177 + experimentation and top-down proof development.
1.1178 +
1.1179 + \end{descr}
1.1180 +*}
1.1181 +
1.1182 +
1.1183 +subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
1.1184 +
1.1185 +text {*
1.1186 + The following proof methods and attributes refer to basic logical
1.1187 + operations of Isar. Further methods and attributes are provided by
1.1188 + several generic and object-logic specific tools and packages (see
1.1189 + \chref{ch:gen-tools} and \chref{ch:logics}).
1.1190 +
1.1191 + \begin{matharray}{rcl}
1.1192 + @{method_def "-"} & : & \isarmeth \\
1.1193 + @{method_def "fact"} & : & \isarmeth \\
1.1194 + @{method_def "assumption"} & : & \isarmeth \\
1.1195 + @{method_def "this"} & : & \isarmeth \\
1.1196 + @{method_def "rule"} & : & \isarmeth \\
1.1197 + @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
1.1198 + @{attribute_def "intro"} & : & \isaratt \\
1.1199 + @{attribute_def "elim"} & : & \isaratt \\
1.1200 + @{attribute_def "dest"} & : & \isaratt \\
1.1201 + @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
1.1202 + @{attribute_def "OF"} & : & \isaratt \\
1.1203 + @{attribute_def "of"} & : & \isaratt \\
1.1204 + @{attribute_def "where"} & : & \isaratt \\
1.1205 + \end{matharray}
1.1206 +
1.1207 + \begin{rail}
1.1208 + 'fact' thmrefs?
1.1209 + ;
1.1210 + 'rule' thmrefs?
1.1211 + ;
1.1212 + 'iprover' ('!' ?) (rulemod *)
1.1213 + ;
1.1214 + rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
1.1215 + ;
1.1216 + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
1.1217 + ;
1.1218 + 'rule' 'del'
1.1219 + ;
1.1220 + 'OF' thmrefs
1.1221 + ;
1.1222 + 'of' insts ('concl' ':' insts)?
1.1223 + ;
1.1224 + 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
1.1225 + ;
1.1226 + \end{rail}
1.1227 +
1.1228 + \begin{descr}
1.1229 +
1.1230 + \item [``@{method "-"}''] does nothing but insert the forward
1.1231 + chaining facts as premises into the goal. Note that command
1.1232 + @{command_ref "proof"} without any method actually performs a single
1.1233 + reduction step using the @{method_ref rule} method; thus a plain
1.1234 + \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
1.1235 + "-"}'' rather than @{command "proof"} alone.
1.1236 +
1.1237 + \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
1.1238 + some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
1.1239 + the current proof context) modulo unification of schematic type and
1.1240 + term variables. The rule structure is not taken into account, i.e.\
1.1241 + meta-level implication is considered atomic. This is the same
1.1242 + principle underlying literal facts (cf.\ \secref{sec:syn-att}):
1.1243 + ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
1.1244 + equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
1.1245 + "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
1.1246 + @{text "\<turnstile> \<phi>"} in the proof context.
1.1247 +
1.1248 + \item [@{method assumption}] solves some goal by a single assumption
1.1249 + step. All given facts are guaranteed to participate in the
1.1250 + refinement; this means there may be only 0 or 1 in the first place.
1.1251 + Recall that @{command "qed"} (\secref{sec:proof-steps}) already
1.1252 + concludes any remaining sub-goals by assumption, so structured
1.1253 + proofs usually need not quote the @{method assumption} method at
1.1254 + all.
1.1255 +
1.1256 + \item [@{method this}] applies all of the current facts directly as
1.1257 + rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
1.1258 + "by"}~@{text this}''.
1.1259 +
1.1260 + \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
1.1261 + rule given as argument in backward manner; facts are used to reduce
1.1262 + the rule before applying it to the goal. Thus @{method rule}
1.1263 + without facts is plain introduction, while with facts it becomes
1.1264 + elimination.
1.1265 +
1.1266 + When no arguments are given, the @{method rule} method tries to pick
1.1267 + appropriate rules automatically, as declared in the current context
1.1268 + using the @{attribute intro}, @{attribute elim}, @{attribute dest}
1.1269 + attributes (see below). This is the default behavior of @{command
1.1270 + "proof"} and ``@{command ".."}'' (double-dot) steps (see
1.1271 + \secref{sec:proof-steps}).
1.1272 +
1.1273 + \item [@{method iprover}] performs intuitionistic proof search,
1.1274 + depending on specifically declared rules from the context, or given
1.1275 + as explicit arguments. Chained facts are inserted into the goal
1.1276 + before commencing proof search; ``@{method iprover}@{text "!"}''
1.1277 + means to include the current @{fact prems} as well.
1.1278 +
1.1279 + Rules need to be classified as @{attribute intro}, @{attribute
1.1280 + elim}, or @{attribute dest}; here the ``@{text "!"} indicator refers
1.1281 + to ``safe'' rules, which may be applied aggressively (without
1.1282 + considering back-tracking later). Rules declared with ``@{text
1.1283 + "?"}'' are ignored in proof search (the single-step @{method rule}
1.1284 + method still observes these). An explicit weight annotation may be
1.1285 + given as well; otherwise the number of rule premises will be taken
1.1286 + into account here.
1.1287 +
1.1288 + \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
1.1289 + declare introduction, elimination, and destruct rules, to be used
1.1290 + with the @{method rule} and @{method iprover} methods. Note that
1.1291 + the latter will ignore rules declared with ``@{text "?"}'', while
1.1292 + ``@{text "!"}'' are used most aggressively.
1.1293 +
1.1294 + The classical reasoner (see \secref{sec:classical}) introduces its
1.1295 + own variants of these attributes; use qualified names to access the
1.1296 + present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
1.1297 +
1.1298 + \item [@{attribute rule}~@{text del}] undeclares introduction,
1.1299 + elimination, or destruct rules.
1.1300 +
1.1301 + \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
1.1302 + theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
1.1303 + (in parallel). This corresponds to the @{ML "op MRS"} operation in
1.1304 + ML, but note the reversed order. Positions may be effectively
1.1305 + skipped by including ``@{verbatim _}'' (underscore) as argument.
1.1306 +
1.1307 + \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
1.1308 + positional instantiation of term variables. The terms @{text
1.1309 + "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
1.1310 + variables occurring in a theorem from left to right; ``@{verbatim
1.1311 + _}'' (underscore) indicates to skip a position. Arguments following
1.1312 + a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
1.1313 + of the conclusion of a rule.
1.1314 +
1.1315 + \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
1.1316 + \<AND> x\<^sub>n = t\<^sub>n"}] performs named instantiation of
1.1317 + schematic type and term variables occurring in a theorem. Schematic
1.1318 + variables have to be specified on the left-hand side (e.g.\ @{text
1.1319 + "?x1.3"}). The question mark may be omitted if the variable name is
1.1320 + a plain identifier without index. As type instantiations are
1.1321 + inferred from term instantiations, explicit type instantiations are
1.1322 + seldom necessary.
1.1323 +
1.1324 + \end{descr}
1.1325 +*}
1.1326 +
1.1327 +
1.1328 +subsection {* Term abbreviations \label{sec:term-abbrev} *}
1.1329 +
1.1330 +text {*
1.1331 + \begin{matharray}{rcl}
1.1332 + @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
1.1333 + @{keyword_def "is"} & : & syntax \\
1.1334 + \end{matharray}
1.1335 +
1.1336 + Abbreviations may be either bound by explicit @{command "let"}@{text
1.1337 + "p \<equiv> t"} statements, or by annotating assumptions or goal statements
1.1338 + with a list of patterns ``@{text "\<IS> p\<^sub>1 \<dots> p\<^sub>n"}''.
1.1339 + In both cases, higher-order matching is invoked to bind
1.1340 + extra-logical term variables, which may be either named schematic
1.1341 + variables of the form @{text ?x}, or nameless dummies ``@{variable
1.1342 + _}'' (underscore). Note that in the @{command "let"} form the
1.1343 + patterns occur on the left-hand side, while the @{keyword "is"}
1.1344 + patterns are in postfix position.
1.1345 +
1.1346 + Polymorphism of term bindings is handled in Hindley-Milner style,
1.1347 + similar to ML. Type variables referring to local assumptions or
1.1348 + open goal statements are \emph{fixed}, while those of finished
1.1349 + results or bound by @{command "let"} may occur in \emph{arbitrary}
1.1350 + instances later. Even though actual polymorphism should be rarely
1.1351 + used in practice, this mechanism is essential to achieve proper
1.1352 + incremental type-inference, as the user proceeds to build up the
1.1353 + Isar proof text from left to right.
1.1354 +
1.1355 + \medskip Term abbreviations are quite different from local
1.1356 + definitions as introduced via @{command "def"} (see
1.1357 + \secref{sec:proof-context}). The latter are visible within the
1.1358 + logic as actual equations, while abbreviations disappear during the
1.1359 + input process just after type checking. Also note that @{command
1.1360 + "def"} does not support polymorphism.
1.1361 +
1.1362 + \begin{rail}
1.1363 + 'let' ((term + 'and') '=' term + 'and')
1.1364 + ;
1.1365 + \end{rail}
1.1366 +
1.1367 + The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
1.1368 + or \railnonterm{proppat} (see \secref{sec:term-decls}).
1.1369 +
1.1370 + \begin{descr}
1.1371 +
1.1372 + \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND>
1.1373 + \<dots>p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns
1.1374 + @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order
1.1375 + matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
1.1376 +
1.1377 + \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
1.1378 + "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
1.1379 + preceding statement. Also note that @{keyword "is"} is not a
1.1380 + separate command, but part of others (such as @{command "assume"},
1.1381 + @{command "have"} etc.).
1.1382 +
1.1383 + \end{descr}
1.1384 +
1.1385 + Some \emph{implicit} term abbreviations\index{term abbreviations}
1.1386 + for goals and facts are available as well. For any open goal,
1.1387 + @{variable_ref thesis} refers to its object-level statement,
1.1388 + abstracted over any meta-level parameters (if present). Likewise,
1.1389 + @{variable_ref this} is bound for fact statements resulting from
1.1390 + assumptions or finished goals. In case @{variable this} refers to
1.1391 + an object-logic statement that is an application @{text "f t"}, then
1.1392 + @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
1.1393 + (three dots). The canonical application of this convenience are
1.1394 + calculational proofs (see \secref{sec:calculation}).
1.1395 +*}
1.1396 +
1.1397 +
1.1398 +subsection {* Block structure *}
1.1399 +
1.1400 +text {*
1.1401 + \begin{matharray}{rcl}
1.1402 + @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
1.1403 + @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
1.1404 + @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
1.1405 + \end{matharray}
1.1406 +
1.1407 + While Isar is inherently block-structured, opening and closing
1.1408 + blocks is mostly handled rather casually, with little explicit
1.1409 + user-intervention. Any local goal statement automatically opens
1.1410 + \emph{two} internal blocks, which are closed again when concluding
1.1411 + the sub-proof (by @{command "qed"} etc.). Sections of different
1.1412 + context within a sub-proof may be switched via @{command "next"},
1.1413 + which is just a single block-close followed by block-open again.
1.1414 + The effect of @{command "next"} is to reset the local proof context;
1.1415 + there is no goal focus involved here!
1.1416 +
1.1417 + For slightly more advanced applications, there are explicit block
1.1418 + parentheses as well. These typically achieve a stronger forward
1.1419 + style of reasoning.
1.1420 +
1.1421 + \begin{descr}
1.1422 +
1.1423 + \item [@{command "next"}] switches to a fresh block within a
1.1424 + sub-proof, resetting the local context to the initial one.
1.1425 +
1.1426 + \item [@{command "{"} and @{command "}"}] explicitly open and close
1.1427 + blocks. Any current facts pass through ``@{command "{"}''
1.1428 + unchanged, while ``@{command "}"}'' causes any result to be
1.1429 + \emph{exported} into the enclosing context. Thus fixed variables
1.1430 + are generalized, assumptions discharged, and local definitions
1.1431 + unfolded (cf.\ \secref{sec:proof-context}). There is no difference
1.1432 + of @{command "assume"} and @{command "presume"} in this mode of
1.1433 + forward reasoning --- in contrast to plain backward reasoning with
1.1434 + the result exported at @{command "show"} time.
1.1435 +
1.1436 + \end{descr}
1.1437 +*}
1.1438 +
1.1439 +
1.1440 +subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
1.1441 +
1.1442 +text {*
1.1443 + The Isar provides separate commands to accommodate tactic-style
1.1444 + proof scripts within the same system. While being outside the
1.1445 + orthodox Isar proof language, these might come in handy for
1.1446 + interactive exploration and debugging, or even actual tactical proof
1.1447 + within new-style theories (to benefit from document preparation, for
1.1448 + example). See also \secref{sec:tactics} for actual tactics, that
1.1449 + have been encapsulated as proof methods. Proper proof methods may
1.1450 + be used in scripts, too.
1.1451 +
1.1452 + \begin{matharray}{rcl}
1.1453 + @{command_def "apply"}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
1.1454 + @{command_def "apply_end"}^* & : & \isartrans{proof(state)}{proof(state)} \\
1.1455 + @{command_def "done"}^* & : & \isartrans{proof(prove)}{proof(state)} \\
1.1456 + @{command_def "defer"}^* & : & \isartrans{proof}{proof} \\
1.1457 + @{command_def "prefer"}^* & : & \isartrans{proof}{proof} \\
1.1458 + @{command_def "back"}^* & : & \isartrans{proof}{proof} \\
1.1459 + \end{matharray}
1.1460 +
1.1461 + \begin{rail}
1.1462 + ( 'apply' | 'apply\_end' ) method
1.1463 + ;
1.1464 + 'defer' nat?
1.1465 + ;
1.1466 + 'prefer' nat
1.1467 + ;
1.1468 + \end{rail}
1.1469 +
1.1470 + \begin{descr}
1.1471 +
1.1472 + \item [@{command "apply"}~@{text m}] applies proof method @{text m}
1.1473 + in initial position, but unlike @{command "proof"} it retains
1.1474 + ``@{text "proof(prove)"}'' mode. Thus consecutive method
1.1475 + applications may be given just as in tactic scripts.
1.1476 +
1.1477 + Facts are passed to @{text m} as indicated by the goal's
1.1478 + forward-chain mode, and are \emph{consumed} afterwards. Thus any
1.1479 + further @{command "apply"} command would always work in a purely
1.1480 + backward manner.
1.1481 +
1.1482 + \item [@{command "apply_end"}~@{text "m"}] applies proof method
1.1483 + @{text m} as if in terminal position. Basically, this simulates a
1.1484 + multi-step tactic script for @{command "qed"}, but may be given
1.1485 + anywhere within the proof body.
1.1486 +
1.1487 + No facts are passed to @{method m} here. Furthermore, the static
1.1488 + context is that of the enclosing goal (as for actual @{command
1.1489 + "qed"}). Thus the proof method may not refer to any assumptions
1.1490 + introduced in the current body, for example.
1.1491 +
1.1492 + \item [@{command "done"}] completes a proof script, provided that
1.1493 + the current goal state is solved completely. Note that actual
1.1494 + structured proof commands (e.g.\ ``@{command "."}'' or @{command
1.1495 + "sorry"}) may be used to conclude proof scripts as well.
1.1496 +
1.1497 + \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
1.1498 + n}] shuffle the list of pending goals: @{command "defer"} puts off
1.1499 + sub-goal @{text n} to the end of the list (@{text "n = 1"} by
1.1500 + default), while @{command "prefer"} brings sub-goal @{text n} to the
1.1501 + front.
1.1502 +
1.1503 + \item [@{command "back"}] does back-tracking over the result
1.1504 + sequence of the latest proof command. Basically, any proof command
1.1505 + may return multiple results.
1.1506 +
1.1507 + \end{descr}
1.1508 +
1.1509 + Any proper Isar proof method may be used with tactic script commands
1.1510 + such as @{command "apply"}. A few additional emulations of actual
1.1511 + tactics are provided as well; these would be never used in actual
1.1512 + structured proofs, of course.
1.1513 +*}
1.1514 +
1.1515 +
1.1516 +subsection {* Meta-linguistic features *}
1.1517 +
1.1518 +text {*
1.1519 + \begin{matharray}{rcl}
1.1520 + @{command_def "oops"} & : & \isartrans{proof}{theory} \\
1.1521 + \end{matharray}
1.1522 +
1.1523 + The @{command "oops"} command discontinues the current proof
1.1524 + attempt, while considering the partial proof text as properly
1.1525 + processed. This is conceptually quite different from ``faking''
1.1526 + actual proofs via @{command_ref "sorry"} (see
1.1527 + \secref{sec:proof-steps}): @{command "oops"} does not observe the
1.1528 + proof structure at all, but goes back right to the theory level.
1.1529 + Furthermore, @{command "oops"} does not produce any result theorem
1.1530 + --- there is no intended claim to be able to complete the proof
1.1531 + anyhow.
1.1532 +
1.1533 + A typical application of @{command "oops"} is to explain Isar proofs
1.1534 + \emph{within} the system itself, in conjunction with the document
1.1535 + preparation tools of Isabelle described in \cite{isabelle-sys}.
1.1536 + Thus partial or even wrong proof attempts can be discussed in a
1.1537 + logically sound manner. Note that the Isabelle {\LaTeX} macros can
1.1538 + be easily adapted to print something like ``@{text "\<dots>"}'' instead of
1.1539 + the keyword ``@{command "oops"}''.
1.1540 +
1.1541 + \medskip The @{command "oops"} command is undo-able, unlike
1.1542 + @{command_ref "kill"} (see \secref{sec:history}). The effect is to
1.1543 + get back to the theory just before the opening of the proof.
1.1544 +*}
1.1545 +
1.1546 +
1.1547 +section {* Other commands *}
1.1548 +
1.1549 +subsection {* Diagnostics *}
1.1550 +
1.1551 +text {*
1.1552 + \begin{matharray}{rcl}
1.1553 + \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
1.1554 + \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
1.1555 + \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
1.1556 + \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
1.1557 + \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
1.1558 + \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
1.1559 + \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
1.1560 + \end{matharray}
1.1561 +
1.1562 + These diagnostic commands assist interactive development. Note that
1.1563 + @{command undo} does not apply here, the theory or proof
1.1564 + configuration is not changed.
1.1565 +
1.1566 + \begin{rail}
1.1567 + 'pr' modes? nat? (',' nat)?
1.1568 + ;
1.1569 + 'thm' modes? thmrefs
1.1570 + ;
1.1571 + 'term' modes? term
1.1572 + ;
1.1573 + 'prop' modes? prop
1.1574 + ;
1.1575 + 'typ' modes? type
1.1576 + ;
1.1577 + 'prf' modes? thmrefs?
1.1578 + ;
1.1579 + 'full\_prf' modes? thmrefs?
1.1580 + ;
1.1581 +
1.1582 + modes: '(' (name + ) ')'
1.1583 + ;
1.1584 + \end{rail}
1.1585 +
1.1586 + \begin{descr}
1.1587 +
1.1588 + \item [@{command "pr"}~@{text "goals, prems"}] prints the current
1.1589 + proof state (if present), including the proof context, current facts
1.1590 + and goals. The optional limit arguments affect the number of goals
1.1591 + and premises to be displayed, which is initially 10 for both.
1.1592 + Omitting limit values leaves the current setting unchanged.
1.1593 +
1.1594 + \item [@{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] retrieves
1.1595 + theorems from the current theory or proof context. Note that any
1.1596 + attributes included in the theorem specifications are applied to a
1.1597 + temporary context derived from the current theory or proof; the
1.1598 + result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
1.1599 + \<dots>, a\<^sub>n"} do not have any permanent effect.
1.1600 +
1.1601 + \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}]
1.1602 + read, type-check and print terms or propositions according to the
1.1603 + current theory or proof context; the inferred type of @{text t} is
1.1604 + output as well. Note that these commands are also useful in
1.1605 + inspecting the current environment of term abbreviations.
1.1606 +
1.1607 + \item [@{command "typ"}~@{text \<tau>}] reads and prints types of the
1.1608 + meta-logic according to the current theory or proof context.
1.1609 +
1.1610 + \item [@{command "prf"}] displays the (compact) proof term of the
1.1611 + current proof state (if present), or of the given theorems. Note
1.1612 + that this requires proof terms to be switched on for the current
1.1613 + object logic (see the ``Proof terms'' section of the Isabelle
1.1614 + reference manual for information on how to do this).
1.1615 +
1.1616 + \item [@{command "full_prf"}] is like @{command "prf"}, but displays
1.1617 + the full proof term, i.e.\ also displays information omitted in the
1.1618 + compact proof term, which is denoted by ``@{verbatim _}''
1.1619 + placeholders there.
1.1620 +
1.1621 + \end{descr}
1.1622 +
1.1623 + All of the diagnostic commands above admit a list of @{text modes}
1.1624 + to be specified, which is appended to the current print mode (see
1.1625 + also \cite{isabelle-ref}). Thus the output behavior may be modified
1.1626 + according particular print mode features. For example, @{command
1.1627 + "pr"}~@{text "(latex xsymbols symbols)"} would print the current
1.1628 + proof state with mathematical symbols and special characters
1.1629 + represented in {\LaTeX} source, according to the Isabelle style
1.1630 + \cite{isabelle-sys}.
1.1631 +
1.1632 + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
1.1633 + systematic way to include formal items into the printed text
1.1634 + document.
1.1635 +*}
1.1636 +
1.1637 +
1.1638 +subsection {* Inspecting the context *}
1.1639 +
1.1640 +text {*
1.1641 + \begin{matharray}{rcl}
1.1642 + @{command_def "print_commands"}^* & : & \isarkeep{\cdot} \\
1.1643 + @{command_def "print_theory"}^* & : & \isarkeep{theory~|~proof} \\
1.1644 + @{command_def "print_syntax"}^* & : & \isarkeep{theory~|~proof} \\
1.1645 + @{command_def "print_methods"}^* & : & \isarkeep{theory~|~proof} \\
1.1646 + @{command_def "print_attributes"}^* & : & \isarkeep{theory~|~proof} \\
1.1647 + @{command_def "print_theorems"}^* & : & \isarkeep{theory~|~proof} \\
1.1648 + @{command_def "find_theorems"}^* & : & \isarkeep{theory~|~proof} \\
1.1649 + @{command_def "thms_deps"}^* & : & \isarkeep{theory~|~proof} \\
1.1650 + @{command_def "print_facts"}^* & : & \isarkeep{proof} \\
1.1651 + @{command_def "print_binds"}^* & : & \isarkeep{proof} \\
1.1652 + \end{matharray}
1.1653 +
1.1654 + \begin{rail}
1.1655 + 'print\_theory' ( '!'?)
1.1656 + ;
1.1657 +
1.1658 + 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
1.1659 + ;
1.1660 + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
1.1661 + 'simp' ':' term | term)
1.1662 + ;
1.1663 + 'thm\_deps' thmrefs
1.1664 + ;
1.1665 + \end{rail}
1.1666 +
1.1667 + These commands print certain parts of the theory and proof context.
1.1668 + Note that there are some further ones available, such as for the set
1.1669 + of rules declared for simplifications.
1.1670 +
1.1671 + \begin{descr}
1.1672 +
1.1673 + \item [@{command "print_commands"}] prints Isabelle's outer theory
1.1674 + syntax, including keywords and command.
1.1675 +
1.1676 + \item [@{command "print_theory"}] prints the main logical content of
1.1677 + the theory context; the ``@{text "!"}'' option indicates extra
1.1678 + verbosity.
1.1679 +
1.1680 + \item [@{command "print_syntax"}] prints the inner syntax of types
1.1681 + and terms, depending on the current context. The output can be very
1.1682 + verbose, including grammar tables and syntax translation rules. See
1.1683 + \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
1.1684 + inner syntax.
1.1685 +
1.1686 + \item [@{command "print_methods"}] prints all proof methods
1.1687 + available in the current theory context.
1.1688 +
1.1689 + \item [@{command "print_attributes"}] prints all attributes
1.1690 + available in the current theory context.
1.1691 +
1.1692 + \item [@{command "print_theorems"}] prints theorems resulting from
1.1693 + the last command.
1.1694 +
1.1695 + \item [@{command "find_theorems"}~@{text criteria}] retrieves facts
1.1696 + from the theory or proof context matching all of given search
1.1697 + criteria. The criterion @{text "name: p"} selects all theorems
1.1698 + whose fully qualified name matches pattern @{text p}, which may
1.1699 + contain ``@{text "*"}'' wildcards. The criteria @{text intro},
1.1700 + @{text elim}, and @{text dest} select theorems that match the
1.1701 + current goal as introduction, elimination or destruction rules,
1.1702 + respectively. The criterion @{text "simp: t"} selects all rewrite
1.1703 + rules whose left-hand side matches the given term. The criterion
1.1704 + term @{text t} selects all theorems that contain the pattern @{text
1.1705 + t} -- as usual, patterns may contain occurrences of the dummy
1.1706 + ``@{verbatim _}'', schematic variables, and type constraints.
1.1707 +
1.1708 + Criteria can be preceded by ``@{text "-"}'' to select theorems that
1.1709 + do \emph{not} match. Note that giving the empty list of criteria
1.1710 + yields \emph{all} currently known facts. An optional limit for the
1.1711 + number of printed facts may be given; the default is 40. By
1.1712 + default, duplicates are removed from the search result. Use
1.1713 + @{keyword "with_dups"} to display duplicates.
1.1714 +
1.1715 + \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
1.1716 + visualizes dependencies of facts, using Isabelle's graph browser
1.1717 + tool (see also \cite{isabelle-sys}).
1.1718 +
1.1719 + \item [@{command "print_facts"}] prints all local facts of the
1.1720 + current context, both named and unnamed ones.
1.1721 +
1.1722 + \item [@{command "print_binds"}] prints all term abbreviations
1.1723 + present in the context.
1.1724 +
1.1725 + \end{descr}
1.1726 +*}
1.1727 +
1.1728 +
1.1729 +subsection {* History commands \label{sec:history} *}
1.1730 +
1.1731 +text {*
1.1732 + \begin{matharray}{rcl}
1.1733 + @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1.1734 + @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1.1735 + @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1.1736 + \end{matharray}
1.1737 +
1.1738 + The Isabelle/Isar top-level maintains a two-stage history, for
1.1739 + theory and proof state transformation. Basically, any command can
1.1740 + be undone using @{command "undo"}, excluding mere diagnostic
1.1741 + elements. Its effect may be revoked via @{command "redo"}, unless
1.1742 + the corresponding @{command "undo"} step has crossed the beginning
1.1743 + of a proof or theory. The @{command "kill"} command aborts the
1.1744 + current history node altogether, discontinuing a proof or even the
1.1745 + whole theory. This operation is \emph{not} undo-able.
1.1746 +
1.1747 + \begin{warn}
1.1748 + History commands should never be used with user interfaces such as
1.1749 + Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
1.1750 + care of stepping forth and back itself. Interfering by manual
1.1751 + @{command "undo"}, @{command "redo"}, or even @{command "kill"}
1.1752 + commands would quickly result in utter confusion.
1.1753 + \end{warn}
1.1754 +*}
1.1755 +
1.1756 +
1.1757 +subsection {* System operations *}
1.1758 +
1.1759 +text {*
1.1760 + \begin{matharray}{rcl}
1.1761 + @{command_def "cd"}^* & : & \isarkeep{\cdot} \\
1.1762 + @{command_def "pwd"}^* & : & \isarkeep{\cdot} \\
1.1763 + @{command_def "use_thy"}^* & : & \isarkeep{\cdot} \\
1.1764 + @{command_def "display_drafts"}^* & : & \isarkeep{\cdot} \\
1.1765 + @{command_def "print_drafts"}^* & : & \isarkeep{\cdot} \\
1.1766 + \end{matharray}
1.1767 +
1.1768 + \begin{rail}
1.1769 + ('cd' | 'use\_thy' | 'update\_thy') name
1.1770 + ;
1.1771 + ('display\_drafts' | 'print\_drafts') (name +)
1.1772 + ;
1.1773 + \end{rail}
1.1774 +
1.1775 + \begin{descr}
1.1776 +
1.1777 + \item [@{command "cd"}~@{text path}] changes the current directory
1.1778 + of the Isabelle process.
1.1779 +
1.1780 + \item [@{command "pwd"}] prints the current working directory.
1.1781 +
1.1782 + \item [@{command "use_thy"}~@{text A}] preload theory @{text A}.
1.1783 + These system commands are scarcely used when working interactively,
1.1784 + since loading of theories is done automatically as required.
1.1785 +
1.1786 + \item [@{command "display_drafts"}~@{text paths} and @{command
1.1787 + "print_drafts"}~@{text paths}] perform simple output of a given list
1.1788 + of raw source files. Only those symbols that do not require
1.1789 + additional {\LaTeX} packages are displayed properly, everything else
1.1790 + is left verbatim.
1.1791 +
1.1792 + \end{descr}
1.1793 +*}
1.1794 +
1.1795 +end