doc-src/IsarRef/pure.tex

 
 Subsequently, we introduce the main part of Pure Isar theory and proof
 commands, together with fundamental proof methods and attributes.
 Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
 tools and packages (such as the Simplifier) that are either part of Pure
-Isabelle or pre-installed by most object logics.  Chapter~\ref{ch:hol-tools}
-refers to actual object-logic specific elements of Isabelle/HOL.
+Isabelle or pre-installed by most object logics.  Chapter~\ref{ch:logics}
+refers to object-logic specific elements (mainly for HOL and ZF).
 
 \medskip
 
 Isar commands may be either \emph{proper} document constructors, or
 \emph{improper commands}.  Some proof methods and attributes introduced later
 are classified as improper as well.  Improper Isar language elements, which
 are subsequently marked by ``$^*$'', are often helpful when developing proof
 documents, while their use is discouraged for the final outcome.  Typical
 examples are diagnostic commands that print terms or theorems according to the
-current context; other commands even emulate old-style tactical theorem
-proving.
-
-
-\section{Theory specification commands}
+current context; other commands emulate old-style tactical theorem proving.
+
+
+\section{Theory commands}
 
 \subsection{Defining theories}\label{sec:begin-thy}
 
-\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
+\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end}
 \begin{matharray}{rcl}
   \isarcmd{header} & : & \isarkeep{toplevel} \\
   \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
   \isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\
   \isarcmd{end} & : & \isartrans{theory}{toplevel} \\

 interactively.  Both theory-level specifications and proofs are handled
 uniformly --- occasionally definitional mechanisms even require some explicit
 proof as well.  In contrast, ``old-style'' Isabelle theories support batch
 processing only, with the proof scripts collected in separate ML files.
 
-The first actual command of any theory has to be $\THEORY$, starting a new
-theory based on the merge of existing ones.  Just preceding $\THEORY$, there
-may be an optional $\isarkeyword{header}$ declaration, which is relevant to
-document preparation only; it acts very much like a special pre-theory markup
-command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The theory
-context may be also changed by $\CONTEXT$ without creating a new theory.  In
-both cases, $\END$ concludes the theory development; it has to be the very
-last command of any theory file.
+The first ``real'' command of any theory has to be $\THEORY$, which starts a
+new theory based on the merge of existing ones.  Just preceding $\THEORY$,
+there may be an optional $\isarkeyword{header}$ declaration, which is relevant
+to document preparation only; it acts very much like a special pre-theory
+markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The
+$\END$ commands concludes a theory development; it has to be the very last
+command of any theory file to loaded in batch-mode.  The theory context may be
+also changed interactively by $\CONTEXT$ without creating a new theory.
 
 \begin{rail}
   'header' text
   ;
   'theory' name '=' (name + '+') filespecs? ':'
   ;
   'context' name
   ;
-  'end'
-  ;;
 
   filespecs: 'files' ((name | parname) +);
 \end{rail}
 
 \begin{descr}

   the formal beginning of a theory.  In actual document preparation the
   corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
   produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
   \S\ref{sec:markup-prf} for further markup commands.
   
-\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
-  based on existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader
-  system ensures that any of the base theories are properly loaded (and fully
-  up-to-date when $\THEORY$ is executed interactively).  The optional
-  $\isarkeyword{files}$ specification declares additional dependencies on ML
-  files.  Unless put in parentheses, any file will be loaded immediately via
-  $\isarcmd{use}$ (see also \S\ref{sec:ML}).  The optional ML file
-  \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
-  included in $\isarkeyword{files}$, though.
+\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based
+  on the merge of existing theories $B@1, \dots, B@n$.
+  
+  Due to inclusion of several ancestors, the overall theory structure emerging
+  in an Isabelle session forms a directed acyclic graph (DAG).  Isabelle's
+  theory loader ensures that the sources contributing to the development graph
+  are always up-to-date.  Changed files are automatically reloaded when
+  processing theory headers interactively; batch-mode explicitly distinguishes
+  \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
+  
+  The optional $\isarkeyword{files}$ specification declares additional
+  dependencies on ML files.  Files will be loaded immediately, unless the name
+  is put in parentheses, which merely documents the dependency to be resolved
+  later in the text (typically via explicit $\isarcmd{use}$ in the body text,
+  see \S\ref{sec:ML}).  In reminiscence of the old-style theory system of
+  Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
+  \texttt{$A$.ML} consisting of ML code that is executed in the context of the
+  \emph{finished} theory $A$.  That file should not be included in the
+  $\isarkeyword{files}$ dependency declaration, though.
   
 \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
   mode, so only a limited set of commands may be performed without destroying
   the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
   loaded and up-to-date.
   
+  This command is occasionally useful for quick interactive experiments;
+  normally one should always commence a new context via $\THEORY$.
+  
 \item [$\END$] concludes the current theory definition or context switch.
-Note that this command cannot be undone, but the whole theory definition has
-to be retracted.
-\end{descr}
-
-
-\subsection{Theory markup commands}\label{sec:markup-thy}
+  Note that this command cannot be undone, but the whole theory definition has
+  to be retracted.
+
+\end{descr}
+
+
+\subsection{Markup commands}\label{sec:markup-thy}
 
 \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
 \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
 \begin{matharray}{rcl}
   \isarcmd{chapter} & : & \isartrans{theory}{theory} \\

 
 
 \subsection{Type classes and sorts}\label{sec:classes}
 
 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
-\begin{matharray}{rcl}
+\begin{matharray}{rcll}
   \isarcmd{classes} & : & \isartrans{theory}{theory} \\
-  \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
+  \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
 \begin{rail}
   'classes' (classdecl comment? +)

   between existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
   $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
   proven class relations.
 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
   any type variables given without sort constraints.  Usually, the default
-  sort would be only changed when defining new object-logics.
+  sort would be only changed when defining a new object-logic.
 \end{descr}
 
 
 \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
 
 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
-\begin{matharray}{rcl}
+\begin{matharray}{rcll}
   \isarcmd{types} & : & \isartrans{theory}{theory} \\
   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
   \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
-  \isarcmd{arities} & : & \isartrans{theory}{theory} \\
+  \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\
 \end{matharray}
 
 \begin{rail}
   'types' (typespec '=' type infix? comment? +)
   ;

   
   The $overloaded$ option declares definitions to be potentially overloaded.
   Unless this option is given, a warning message would be issued for any
   definitional equation with a more special type than that of the
   corresponding constant declaration.
-
-\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
-  definitions of constants, using the canonical name $c_def$ for the
-  definitional axiom.
+  
+\item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of
+  constants, using the canonical name $c_def$ for the definitional axiom.
 \end{descr}
 
 
 \subsection{Syntax and translations}\label{sec:syn-trans}
 

 
 
 \subsection{Axioms and theorems}\label{sec:axms-thms}
 
 \indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
-\begin{matharray}{rcl}
-  \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
+\begin{matharray}{rcll}
+  \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
   \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
 \begin{rail}

   
 \item [$\isarkeyword{hide}~space~names$] removes declarations from a given
   name space (which may be $class$, $type$, or $const$).  Hidden objects
   remain valid within the logic, but are inaccessible from user input.  In
   output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
-  full internal name.
-  
-  Unqualified (global) names may not be hidden deliberately.
+  full internal name.  Unqualified (global) names may not be hidden.
 \end{descr}
 
 
 \subsection{Incorporating ML code}\label{sec:ML}
 

   $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
   register) have been just picked up in order to be used when refining the
   goal claimed next.
 \end{descr}
 
-%FIXME diagram?
-
-\subsection{Proof markup commands}\label{sec:markup-prf}
+The proof mode indicator may be read as a verb telling the writer what kind of
+operation may be performed next.  The corresponding typings of proof commands
+restricts the shape of well-formed proof texts to particular command
+sequences.  So dynamic arrangements of commands eventually turn out as static
+texts.  Appendix~\ref{ap:refcard} gives a simplified grammar of the overall
+(extensible) language emerging that way.
+
+
+\subsection{Markup commands}\label{sec:markup-prf}
 
 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
 \indexisarcmd{txt}\indexisarcmd{txt-raw}
 \begin{matharray}{rcl}
   \isarcmd{sect} & : & \isartrans{proof}{proof} \\

   ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
   ;
 \end{rail}
 
 
-\subsection{Proof context}\label{sec:proof-context}
+\subsection{Context elements}\label{sec:proof-context}
 
 \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
 \begin{matharray}{rcl}
   \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\

 bound in Isabelle/Pure as ``\texttt{_}''
 (underscore).\indexisarthm{_@\texttt{_}}
 
 Forward chaining with an empty list of theorems is the same as not chaining.
 Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode,
-since $nothing$\indexisarthm{nothing} is bound to the empty list of facts.
+since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems.
 
 
 \subsection{Goal statements}
 
 \indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}

   \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
   \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
 \end{matharray}
 
-From a theory context, proof mode is entered from theory mode by initial goal
-commands $\LEMMANAME$, $\THEOREMNAME$, and $\COROLLARYNAME$.  Within a proof,
-new claims may be introduced locally as well; four variants are available,
-indicating whether the result is meant to solve some pending goal or whether
-forward chaining is indicated.
+From a theory context, proof mode is entered by an initial goal command such
+as $\LEMMANAME$, $\THEOREMNAME$, $\COROLLARYNAME$.  Within a proof, new claims
+may be introduced locally as well; four variants are available here to
+indicate whether forward chaining of facts should be performed initially (via
+$\THEN$), and whether the emerging result is meant to solve some pending goal.
 
 Goals may consist of multiple statements, resulting in a list of facts
 eventually.  A pending multi-goal is internally represented as a meta-level
 conjunction (printed as \verb,&&,), which is automatically split into the
 corresponding number of sub-goals prior to any initial method application, via
 $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
 (\S\ref{sec:tactic-commands}).\footnote{Deviating from the latter principle,
   the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on
   multiple claims simultaneously.}
 
-%FIXME define locale, context
-
-\begin{rail}
-  ('lemma' | 'theorem' | 'corollary') locale context goal
+\begin{rail}
+  ('lemma' | 'theorem' | 'corollary') goalprefix goal
   ;
   ('have' | 'show' | 'hence' | 'thus') goal
   ;
 
   goal: (props comment? + 'and')
+  ;
+
+  goalprefix: thmdecl? locale? context?
+  ;
+  locale: '(' 'in' name ')'
+  ;
+  context: '(' (contextelem +) ')'
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal,
   eventually resulting in some fact $\turn \vec\phi$ to be put back into the
   theory context, and optionally into the specified locale, cf.\ 
   \S\ref{sec:locale}.  An additional \railnonterm{context} specification may
   build an initial proof context for the subsequent claim; this may include
-  local definitions and syntax as well, see \S\ref{sec:locale} for more
-  information.
+  local definitions and syntax as well, see the definition of $contextelem$ in
+  \S\ref{sec:locale}.
   
 \item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
   the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
   being of a different kind.  This discrimination acts like a formal comment.
   

   
 \item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
   remaining goals.  No facts are passed to $m@2$.
 \end{enumerate}
 
-The only other proper way to affect pending goals is by $\SHOWNAME$, which
-involves an explicit statement of what is to be solved.
+The only other proper way to affect pending goals in a proof body is by
+$\SHOWNAME$, which involves an explicit statement of what is to be solved
+eventually.  Thus we avoid the fundamental problem of unstructured tactic
+scripts that consist of numerous consecutive goal transformations, with
+invisible effects.
 
 \medskip
 
-Also note that initial proof methods should either solve the goal completely,
-or constitute some well-understood reduction to new sub-goals.  Arbitrary
-automatic proof tools that are prone leave a large number of badly structured
-sub-goals are no help in continuing the proof document in any intelligible
-way.
-
-\medskip
+As a general rule of thumb for good proof style, initial proof methods should
+either solve the goal completely, or constitute some well-understood reduction
+to new sub-goals.  Arbitrary automatic proof tools that are prone leave a
+large number of badly structured sub-goals are no help in continuing the proof
+document in any intelligible way.
 
 Unless given explicitly by the user, the default initial method is ``$rule$'',
 which applies a single standard elimination or introduction rule according to
 the topmost symbol involved.  There is no separate default terminal method.
 Any remaining goals are always solved by assumption in the very last step.

 \subsection{Fundamental methods and attributes}\label{sec:pure-meth-att}
 
 The following proof methods and attributes refer to basic logical operations
 of Isar.  Further methods and attributes are provided by several generic and
 object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
-\ref{ch:hol-tools}).
+\ref{ch:logics}).
 
 \indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
-\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
 \indexisaratt{OF}\indexisaratt{of}
+\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
+\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
 \begin{matharray}{rcl}
   assumption & : & \isarmeth \\
   this & : & \isarmeth \\
   rule & : & \isarmeth \\
   - & : & \isarmeth \\

   intro & : & \isaratt \\
   elim & : & \isaratt \\
   dest & : & \isaratt \\
   rule & : & \isaratt \\
 \end{matharray}
+
+%FIXME intro!, intro, intro?
 
 \begin{rail}
   'rule' thmrefs?
   ;
   'OF' thmrefs

 variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
 (underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
 patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
 postfix position.
 
-Polymorphism of term bindings is handled in Hindley-Milner style, as in ML.
-Type variables referring to local assumptions or open goal statements are
+Polymorphism of term bindings is handled in Hindley-Milner style, similar to
+ML.  Type variables referring to local assumptions or open goal statements are
 \emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
 in \emph{arbitrary} instances later.  Even though actual polymorphism should
 be rarely used in practice, this mechanism is essential to achieve proper
 incremental type-inference, as the user proceeds to build up the Isar proof
 text.