doc-src/IsarRef/hol.tex

'cases' and 'induct' methods;

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

\section{Miscellaneous attributes}

\indexisaratt{rulify}\indexisaratt{rulify-prems}
\begin{matharray}{rcl}
  rulify & : & \isaratt \\
  rulify_prems & : & \isaratt \\
\end{matharray}

\begin{descr}

\item [$rulify$] puts a theorem into object-rule form, replacing implication
  and universal quantification of HOL by the corresponding meta-logical
  connectives.  This is the same operation as performed by the
  \texttt{qed_spec_mp} ML function.
  
\item [$rulify_prems$] is similar to $rulify$, but acts on the premises 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}

%FIXME record_split method
\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' (parname? typespec infix? \\ '=' (constructor + '|') + 'and')
  ;
  repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
  ;

  constructor: name (type * ) mixfix? comment?
  ;
\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.


\section{Recursive functions}

\indexisarcmd{primrec}\indexisarcmd{recdef}
\begin{matharray}{rcl}
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
%FIXME
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
\end{matharray}

\begin{rail}
  'primrec' parname? (thmdecl? prop comment? + )
  ;
  'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
  ;
\end{rail}

\begin{descr}
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
  datatypes.
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
  functions (using the TFL package).
\end{descr}

Both definitions accommodate reasoning proof 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$).

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


\section{(Co)Inductive sets}

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

\railalias{condefs}{con\_defs}
\railalias{indcases}{inductive\_cases}
\railterm{condefs,indcases}

\begin{rail}
  ('inductive' | 'coinductive') (term comment? +) \\
    'intrs' attributes? (thmdecl? prop comment? +) \\
    'monos' thmrefs comment? \\ condefs thmrefs comment?
  ;
  indcases thmdef? nameref ':' \\ (prop +) comment?
  ;
  'mono' (() | 'add' | 'del')
  ;
\end{rail}

\begin{descr}
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
  (co)inductive sets from the given introduction rules.
\item [$mono$] adds or deletes monotonicity rules from the theory or proof
  context (the default is to add).  These rule are involved in the automated
  monotonicity proof of $\isarkeyword{inductive}$.
\item [$\isarkeyword{inductive_cases}$] creates instances of elimination rules
  of (co)inductive sets, solving obvious cases by simplification.
  
  The $cases$ proof method (see \S\ref{sec:induct-method}) provides a more
  direct way for reasoning by cases (including optional simplification).
  
  Unlike the \texttt{mk_cases} ML function exported with any inductive
  definition \cite{isabelle-HOL}, $\isarkeyword{inductive_cases}$ it does
  \emph{not} modify cases by simplification, apart from trying to solve
  completely (e.g.\ due to contradictory assumptions.  Thus
  $\isarkeyword{inductive_cases}$ conforms to way Isar proofs are conducted,
  rather than old-style tactic scripts.
\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}

\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:proof-context}).  This accommodates compact proof texts even when
reasoning about large specifications.

\begin{rail}
  'cases' ('simplified' ':')? term? rule?  ;

  'induct' ('stripped' ':')? (inst * 'and') rule?
  ;

  inst: (term +)
  ;
  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
  ;
\end{rail}

\begin{descr}
\item [$cases~t~R$] applies method $rule$ with an appropriate case distinction
  theorem, instantiated to the subject $t$.  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}

  The $simplified$ option causes ``obvious cases'' of the rule to be solved
  beforehand, while the others are left unscathed.
  
\item [$induct~insts~R$] 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.
  
  The $stripped$ option causes implications and (bounded) universal
  quantifiers to be removed from each new subgoal emerging from the
  application of the induction rule.
\end{descr}

Above methods produce named local contexts (cf.\ \S\ref{sec:proof-context}),
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 that contain schematic
variables.

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


\subsection{Augmenting the context}

\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.


\section{Arithmetic}

\indexisarmeth{arith}
\begin{matharray}{rcl}
  arith & : & \isarmeth \\
\end{matharray}

The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
$real$).  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: