doc-src/IsarRef/hol.tex

tuned;

\chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}

\section{Miscellaneous attributes}\label{sec:rule-format}

\indexisaratt{rule-format}
\begin{matharray}{rcl}
  rule_format & : & \isaratt \\
\end{matharray}

\railalias{ruleformat}{rule\_format}
\railterm{ruleformat}

\begin{rail}
  ruleformat ('(' noasm ')')?
  ;
\end{rail}

\begin{descr}
  
\item [$rule_format$] causes a theorem to be put into standard object-rule
  form, replacing implication and (bounded) universal quantification of HOL by
  the corresponding meta-logical connectives.  By default, the result is fully
  normalized, including assumptions and conclusions at any depth.  The
  $no_asm$ option restricts the transformation to the conclusion of a rule.
\end{descr}


\section{Primitive types}

\indexisarcmd{typedecl}\indexisarcmd{typedef}
\begin{matharray}{rcl}
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}

\begin{rail}
  'typedecl' typespec infix? comment?
  ;
  'typedef' parname? typespec infix? \\ '=' term comment?
  ;
\end{rail}

\begin{descr}
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
  actual HOL type constructor.
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
  non-emptiness of the set $A$.  After finishing the proof, the theory will be
  augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
  for more information.  Note that user-level theories usually do not directly
  refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
  packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and
  $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).
\end{descr}


\section{Records}\label{sec:record}

\indexisarcmd{record}
\begin{matharray}{rcl}
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
\end{matharray}

\begin{rail}
  'record' typespec '=' (type '+')? (field +)
  ;

  field: name '::' type comment?
  ;
\end{rail}

\begin{descr}
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
  defines extensible record type $(\vec\alpha)t$, derived from the optional
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
  simply-typed extensible records.
\end{descr}


\section{Datatypes}\label{sec:datatype}

\indexisarcmd{datatype}\indexisarcmd{rep-datatype}
\begin{matharray}{rcl}
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
\end{matharray}

\railalias{repdatatype}{rep\_datatype}
\railterm{repdatatype}

\begin{rail}
  'datatype' (dtspec + 'and')
  ;
  repdatatype (name * ) dtrules
  ;

  dtspec: parname? typespec infix? '=' (cons + '|')
  ;
  cons: name (type * ) mixfix? comment?
  ;
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}

\begin{descr}
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
  ones, generating the standard infrastructure of derived concepts (primitive
  recursion etc.).
\end{descr}

The induction and exhaustion theorems generated provide case names according
to the constructors involved, while parameters are named after the types (see
also \S\ref{sec:induct-method}).

See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
syntax above has been slightly simplified over the old version, usually
requiring more quotes and less parentheses.  Apart from proper proof methods
for case-analysis and induction, there are also emulations of ML tactics
\texttt{case_tac} and \texttt{induct_tac} available, see
\S\ref{sec:induct_tac}.


\section{Recursive functions}

\indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
\begin{matharray}{rcl}
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
%FIXME
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
\end{matharray}

\railalias{recdefsimp}{recdef\_simp}
\railterm{recdefsimp}

\railalias{recdefcong}{recdef\_cong}
\railterm{recdefcong}

\railalias{recdefwf}{recdef\_wf}
\railterm{recdefwf}

\railalias{recdeftc}{recdef\_tc}
\railterm{recdeftc}

\begin{rail}
  'primrec' parname? (equation + )
  ;
  'recdef' name term (eqn + ) hints?
  ;
  recdeftc thmdecl? tc comment?
  ;

  equation: thmdecl? eqn
  ;
  eqn: prop comment?
  ;
  hints: '(' 'hints' (recdefmod * ) ')'
  ;
  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
  ;
  tc: nameref ('(' nat ')')?
  ;
\end{rail}

\begin{descr}
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
  datatypes, see also \cite{isabelle-HOL}.
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
  $recdef_simp$, $recdef_cong$, and $recdef_wf$ hints refer to auxiliary rules
  to be used in the internal automated proof process of TFL.  Additional
  $clasimpmod$ declarations (cf.\ \S\ref{sec:clasimp}) may be given to tune
  the context of the Simplifier (cf.\ \S\ref{sec:simplifier}) and Classical
  reasoner (cf.\ \S\ref{sec:classical}).
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
  termination condition number $i$ (default $1$) as generated by a
  $\isarkeyword{recdef}$ definition of constant $c$.
  
  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
  internal proofs without manual intervention.
\end{descr}

Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
\S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
of the function definition) refers to a specific induction rule, with
parameters named according to the user-specified equations.  Case names of
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
$\isarkeyword{recdef}$ are numbered (starting from $1$).

The equations provided by these packages may be referred later as theorem list
$f\mathord.simps$, where $f$ is the (collective) name of the functions
defined.  Individual equations may be named explicitly as well; note that for
$\isarkeyword{recdef}$ each specification given by the user may result in
several theorems.

\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
the following attributes.

\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
\begin{matharray}{rcl}
  recdef_simp & : & \isaratt \\
  recdef_cong & : & \isaratt \\
  recdef_wf & : & \isaratt \\
\end{matharray}

\railalias{recdefsimp}{recdef\_simp}
\railterm{recdefsimp}

\railalias{recdefcong}{recdef\_cong}
\railterm{recdefcong}

\railalias{recdefwf}{recdef\_wf}
\railterm{recdefwf}

\begin{rail}
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
  ;
\end{rail}


\section{(Co)Inductive sets}\label{sec:inductive}

\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
\begin{matharray}{rcl}
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
  mono & : & \isaratt \\
\end{matharray}

\railalias{condefs}{con\_defs}
\railterm{condefs}

\begin{rail}
  ('inductive' | 'coinductive') sets intros monos?
  ;
  'mono' (() | 'add' | 'del')
  ;

  sets: (term comment? +)
  ;
  intros: 'intros' attributes? (thmdecl? prop comment? +)
  ;
  monos: 'monos' thmrefs comment?
  ;
\end{rail}

\begin{descr}
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
  (co)inductive sets from the given introduction rules.
\item [$mono$] declares monotonicity rules.  These rule are involved in the
  automated monotonicity proof of $\isarkeyword{inductive}$.
\end{descr}

See \cite{isabelle-HOL} for further information on inductive definitions in
HOL.


\section{Proof by cases and induction}\label{sec:induct-method}

\subsection{Proof methods}\label{sec:induct-method-proper}

\indexisarmeth{cases}\indexisarmeth{induct}
\begin{matharray}{rcl}
  cases & : & \isarmeth \\
  induct & : & \isarmeth \\
\end{matharray}

The $cases$ and $induct$ methods provide a uniform interface to case analysis
and induction over datatypes, inductive sets, and recursive functions.  The
corresponding rules may be specified and instantiated in a casual manner.
Furthermore, these methods provide named local contexts that may be invoked
via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
about large specifications.

\begin{rail}
  'cases' ('(' 'simplified' ')')? spec
  ;
  'induct' ('(' 'stripped' ')')? spec
  ;

  spec: open? args rule? params?
  ;
  open: '(' 'open' ')'
  ;
  args: (insts * 'and') 
  ;
  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
  ;
  params: 'of' ':' insts
  ;
\end{rail}

\begin{descr}
\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
  names are bound according to the rule's local contexts.
  
  The rule is determined as follows, according to the facts and arguments
  passed to the $cases$ method:
  \begin{matharray}{llll}
    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
                    & cases &           & \Text{classical case split} \\
                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
  \end{matharray}
  
  Several instantiations may be given, referring to the \emph{suffix} of
  premises of the case rule; within each premise, the \emph{prefix} of
  variables is instantiated.  In most situations, only a single term needs to
  be specified; this refers to the first variable of the last premise (it is
  usually the same for all cases).
  
  Additional parameters may be specified as $ps$; these are applied after the
  primary instantiation in the same manner as by the $of$ attribute (cf.\ 
  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
  typical application would be to specify additional arguments for rules
  stemming from parameterized inductive definitions (see also
  \S\ref{sec:inductive}).

  The $simplified$ option causes ``obvious cases'' of the rule to be solved
  beforehand, while the others are left unscathed.
  
  The $open$ option causes the parameters of the new local contexts to be
  exposed to the current proof context.  Thus local variables stemming from
  distant parts of the theory development may be introduced in an implicit
  manner, which can be quite confusing to the reader.  Furthermore, this
  option may cause unwanted hiding of existing local variables, resulting in
  less robust proof texts.
  
\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
  induction rules, which are determined as follows:
  \begin{matharray}{llll}
    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
  \end{matharray}
  
  Several instantiations may be given, each referring to some part of a mutual
  inductive definition or datatype --- only related partial induction rules
  may be used together, though.  Any of the lists of terms $P, x, \dots$
  refers to the \emph{suffix} of variables present in the induction rule.
  This enables the writer to specify only induction variables, or both
  predicates and variables, for example.
  
  Additional parameters may be given in the same way as for $cases$.
  
  The $stripped$ option causes implications and (bounded) universal
  quantifiers to be removed from each new subgoal emerging from the
  application of the induction rule.  This accommodates special applications
  of ``strengthened induction predicates''.  This option is rarely needed, the
  $induct$ method already handles proper rules appropriately by default.
  
  The $open$ option has the same effect as for the $cases$ method, see above.
\end{descr}

Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
determined by the instantiated rule \emph{before} it has been applied to the
internal proof state.\footnote{As a general principle, Isar proof text may
  never refer to parts of proof states directly.} Thus proper use of symbolic
cases usually require the rule to be instantiated fully, as far as the
emerging local contexts and subgoals are concerned.  In particular, for
induction both the predicates and variables have to be specified.  Otherwise
the $\CASENAME$ command would refuse to invoke cases containing schematic
variables.  Furthermore the resulting local goal statement is bound to the
term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
fully specified.

The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
cases present in the current proof state.

\medskip

It is important to note that there is a fundamental difference of the $cases$
and $induct$ methods in handling of non-atomic goal statements: $cases$ just
applies a certain rule in backward fashion, splitting the result into new
goals with the local contexts being augmented in a purely monotonic manner.

In contrast, $induct$ passes the full goal statement through the ``recursive''
course involved in the induction.  Thus the original statement is basically
replaced by separate copies, corresponding to the induction hypotheses and
conclusion; the original goal context is no longer available.  This behavior
allows \emph{strengthened induction predicates} to be expressed concisely as
meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
  x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.

\medskip

Facts presented to either method are consumed according to the number of
``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
remaining facts are inserted into the goal verbatim before the actual $cases$
or $induct$ rule is applied (thus facts may be even passed through an
induction).

Note that whenever facts are present, the default rule selection scheme would
provide a ``set'' rule only, with the first fact consumed and the rest
inserted into the goal.  In order to pass all facts into a ``type'' rule
instead, one would have to specify this explicitly, e.g.\ by appending
``$type: name$'' to the method argument.


\subsection{Declaring rules}\label{sec:induct-att}

\indexisaratt{cases}\indexisaratt{induct}
\begin{matharray}{rcl}
  cases & : & \isaratt \\
  induct & : & \isaratt \\
\end{matharray}

\begin{rail}
  'cases' spec
  ;
  'induct' spec
  ;

  spec: ('type' | 'set') ':' nameref
  ;
\end{rail}

The $cases$ and $induct$ attributes augment the corresponding context of rules
for reasoning about inductive sets and types.  The standard rules are already
declared by HOL definitional packages.  For special applications, these may be
replaced manually by variant versions.

Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
adjust names of cases and parameters of a rule.

The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
automatically (if none had been given already): $consumes~0$ is specified for
``type'' rules and $consumes~1$ for ``set'' rules.


\subsection{Emulating tactic scripts}\label{sec:induct_tac}

\indexisarmeth{case-tac}\indexisarmeth{induct-tac}
\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
\begin{matharray}{rcl}
  case_tac^* & : & \isarmeth \\
  induct_tac^* & : & \isarmeth \\
  ind_cases^* & : & \isarmeth \\
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
\end{matharray}

\railalias{casetac}{case\_tac}
\railterm{casetac}

\railalias{inducttac}{induct\_tac}
\railterm{inducttac}

\railalias{indcases}{ind\_cases}
\railterm{indcases}

\railalias{inductivecases}{inductive\_cases}
\railterm{inductivecases}

\begin{rail}
  casetac goalspec? term rule?
  ;
  inducttac goalspec? (insts * 'and') rule?
  ;
  indcases (prop +)
  ;
  inductivecases thmdecl? (prop +) comment?
  ;

  rule: ('rule' ':' thmref)
  ;
\end{rail}

\begin{descr}
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
  only (unless an alternative rule is given explicitly).  Furthermore,
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
  variables to be given as instantiation.  These tactic emulations feature
  both goal addressing and dynamic instantiation.  Note that named local
  contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the
  proper $induct$ and $cases$ proof methods (see
  \S\ref{sec:induct-method-proper}).
  
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
  forward manner, unlike the proper $cases$ method (see
  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
  solved completely.
  
  While $ind_cases$ is a proof method to apply the result immediately as
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
  theorems at the theory level for later use,
\end{descr}


\section{Arithmetic}

\indexisarmeth{arith}\indexisaratt{arith-split}
\begin{matharray}{rcl}
  arith & : & \isarmeth \\
  arith_split & : & \isaratt \\
\end{matharray}

\begin{rail}
  'arith' '!'?
  ;
\end{rail}

The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
$real$).  Any current facts are inserted into the goal before running the
procedure.  The ``!''~argument causes the full context of assumptions to be
included.  The $arith_split$ attribute declares case split rules to be
expanded before the arithmetic procedure is invoked.

Note that a simpler (but faster) version of arithmetic reasoning is already
performed by the Simplifier.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: