--- a/doc-src/IsarRef/hol.tex Thu Jan 03 17:01:59 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,356 +0,0 @@
-
-\chapter{Isabelle/HOL specific elements}\label{ch:hol-tools}
-
-\section{Miscellaneous attributes}
-
-\indexisarattof{HOL}{split-format}
-\begin{matharray}{rcl}
- split_format^* & : & \isaratt \\
-\end{matharray}
-
-\railalias{splitformat}{split\_format}
-\railterm{splitformat}
-\railterm{complete}
-
-\begin{rail}
- splitformat (((name * ) + 'and') | ('(' complete ')'))
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into
- canonical form as specified by the arguments given; $\vec p@i$ refers to
- occurrences in premise $i$ of the rule. The $split_format~(complete)$ form
- causes \emph{all} arguments in function applications to be represented
- canonically according to their tuple type structure.
-
- Note that these operations tend to invent funny names for new local
- parameters to be introduced.
-
-\end{descr}
-
-
-\section{Primitive types}\label{sec:typedef}
-
-\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{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:hol-record}) and
- $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
-\end{descr}
-
-
-\section{Records}\label{sec:hol-record}
-
-FIXME proof tools (simp, cases/induct; no split!?);
-
-\indexisarcmdof{HOL}{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 on
- simply-typed extensible records.
-\end{descr}
-
-
-\section{Datatypes}\label{sec:hol-datatype}
-
-\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{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:cases-induct}).
-
-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}\label{sec:recursion}
-
-\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{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' ('(' 'permissive' ')')? \\ 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
- $(permissive)$ option tells TFL to recover from failed proof attempts,
- returning unfinished results. 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:cases-induct}): 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.
-
-\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{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:hol-inductive}
-
-\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{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' (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{Arithmetic}
-
-\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{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.
-
-
-\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
-
-The following important tactical tools of Isabelle/HOL have been ported to
-Isar. These should be never used in proper proof texts!
-
-\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
-\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{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 rule cases
- are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
- methods (see \S\ref{sec:cases-induct}).
-
-\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
- to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
- forward manner.
-
- 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}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "isar-ref"
-%%% End: