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

 \begin{matharray}{rcl}

   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\

   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\

 %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}

 \begin{rail}

   'primrec' parname? (equation + )

   ;

   'recdef' name term (eqn + ) hints?

   ;

   equation: thmdecl? eqn

   ;

   eqn: prop comment?

   ;

   hints: '(' 'hints' (recdefmod * ) ')'

   ;

   recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod

   ;

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

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

 \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? open? args rule?

   ;

   'induct' stripped? open? args rule?

   ;

   simplified: '(' 'simplified' ')'

   ;

   stripped: '(' 'stripped' ')'

   ;

   open: '(' 'open' ')'

   ;

   args: (insts * 'and') 

   ;

   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref

   ;

 \end{rail}

 \begin{descr}

 \item [$cases~insts~R$] 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).

   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$] 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.  This accommodates typical

   ``strengthening of induction'' predicates.

   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.

 The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named

 cases present in the current proof state.

 \subsection{Declaring rules}

 \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 $params$ attributes (see \S\ref{sec:cases}) to

 adjust names of cases and parameters of a rule.

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