doc-src/IsarRef/hol.tex
 author wenzelm Sat Apr 01 20:21:39 2000 +0200 (2000-04-01 ago) changeset 8657 b9475dad85ed parent 8547 93b8685d004b child 8665 403c2985e65e permissions -rw-r--r--
     1

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

     3

     4 \section{Miscellaneous attributes}

     5

     6 \indexisaratt{rulify}\indexisaratt{rulify-prems}

     7 \begin{matharray}{rcl}

     8   rulify & : & \isaratt \\

     9   rulify_prems & : & \isaratt \\

    10 \end{matharray}

    11

    12 \begin{descr}

    13

    14 \item [$rulify$] puts a theorem into object-rule form, replacing implication

    15   and universal quantification of HOL by the corresponding meta-logical

    16   connectives.  This is the same operation as performed by the

    17   \texttt{qed_spec_mp} ML function.

    18

    19 \item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a

    20   rule.

    21

    22 \end{descr}

    23

    24

    25 \section{Primitive types}

    26

    27 \indexisarcmd{typedecl}\indexisarcmd{typedef}

    28 \begin{matharray}{rcl}

    29   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\

    30   \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\

    31 \end{matharray}

    32

    33 \begin{rail}

    34   'typedecl' typespec infix? comment?

    35   ;

    36   'typedef' parname? typespec infix? \\ '=' term comment?

    37   ;

    38 \end{rail}

    39

    40 \begin{descr}

    41 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original

    42   $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but

    43   also declares type arity $t :: (term, \dots, term) term$, making $t$ an

    44   actual HOL type constructor.

    45 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating

    46   non-emptiness of the set $A$.  After finishing the proof, the theory will be

    47   augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}

    48   for more information.  Note that user-level theories usually do not directly

    49   refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced

    50   packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and

    51   $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).

    52 \end{descr}

    53

    54

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

    56

    57 %FIXME record_split method

    58 \indexisarcmd{record}

    59 \begin{matharray}{rcl}

    60   \isarcmd{record} & : & \isartrans{theory}{theory} \\

    61 \end{matharray}

    62

    63 \begin{rail}

    64   'record' typespec '=' (type '+')? (field +)

    65   ;

    66

    67   field: name '::' type comment?

    68   ;

    69 \end{rail}

    70

    71 \begin{descr}

    72 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]

    73   defines extensible record type $(\vec\alpha)t$, derived from the optional

    74   parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.

    75   See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only

    76   simply-typed extensible records.

    77 \end{descr}

    78

    79

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

    81

    82 \indexisarcmd{datatype}\indexisarcmd{rep-datatype}

    83 \begin{matharray}{rcl}

    84   \isarcmd{datatype} & : & \isartrans{theory}{theory} \\

    85   \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\

    86 \end{matharray}

    87

    88 \railalias{repdatatype}{rep\_datatype}

    89 \railterm{repdatatype}

    90

    91 \begin{rail}

    92   'datatype' (parname? typespec infix? \\ '=' (constructor + '|') + 'and')

    93   ;

    94   repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs

    95   ;

    96

    97   constructor: name (type * ) mixfix? comment?

    98   ;

    99 \end{rail}

   100

   101 \begin{descr}

   102 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.

   103 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive

   104   ones, generating the standard infrastructure of derived concepts (primitive

   105   recursion etc.).

   106 \end{descr}

   107

   108 The induction and exhaustion theorems generated provide case names according

   109 to the constructors involved, while parameters are named after the types (see

   110 also \S\ref{sec:induct-method}).

   111

   112 See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory

   113 syntax above has been slightly simplified over the old version, usually

   114 requiring more quotes and less parentheses.  Apart from proper proof methods

   115 for case-analysis and induction, there are also emulations of ML tactics

   116 \texttt{case_tac}\indexisarmeth{case-tac} and

   117 \texttt{induct_tac}\indexisarmeth{induct-tac} available, with similar syntax

   118 as $subgoal_tac$, see \S\ref{sec:tactical-proof}.

   119

   120

   121 \section{Recursive functions}

   122

   123 \indexisarcmd{primrec}\indexisarcmd{recdef}

   124 \begin{matharray}{rcl}

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

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

   127 %FIXME

   128 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\

   129 \end{matharray}

   130

   131 \begin{rail}

   132   'primrec' parname? (equation + )

   133   ;

   134   'recdef' name term (equation +) hints

   135   ;

   136

   137   equation: thmdecl? prop comment?

   138   ;

   139   hints: ('congs' thmrefs)? ('simpset' name)?

   140   ;

   141 \end{rail}

   142

   143 \begin{descr}

   144 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over

   145   datatypes.

   146 \item [$\isarkeyword{recdef}$] defines general well-founded recursive

   147   functions (using the TFL package).

   148 \end{descr}

   149

   150 Both definitions accommodate reasoning proof by induction (cf.\

   151 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name

   152 of the function definition) refers to a specific induction rule, with

   153 parameters named according to the user-specified equations.  Case names of

   154 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of

   155 $\isarkeyword{recdef}$ are numbered (starting from $1$).

   156

   157 The equations provided by these packages may be referred later as theorem list

   158 $f\mathord.simps$, where $f$ is the (collective) name of the functions

   159 defined.  Individual equations may be named explicitly as well; note that for

   160 $\isarkeyword{recdef}$ each specification given by the user may result in

   161 several theorems.

   162

   163 See \cite{isabelle-HOL} for further information on recursive function

   164 definitions in HOL.

   165

   166

   167 \section{(Co)Inductive sets}

   168

   169 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}

   170 \indexisaratt{mono}

   171 \begin{matharray}{rcl}

   172   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\

   173   \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\

   174   mono & : & \isaratt \\

   175   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\

   176 \end{matharray}

   177

   178 \railalias{condefs}{con\_defs}

   179 \railalias{indcases}{inductive\_cases}

   180 \railterm{condefs,indcases}

   181

   182 \begin{rail}

   183   ('inductive' | 'coinductive') (term comment? +) \\

   184     'intrs' attributes? (thmdecl? prop comment? +) \\

   185     'monos' thmrefs comment? \\ condefs thmrefs comment?

   186   ;

   187   indcases thmdef? nameref ':' \\ (prop +) comment?

   188   ;

   189   'mono' (() | 'add' | 'del')

   190   ;

   191 \end{rail}

   192

   193 \begin{descr}

   194 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define

   195   (co)inductive sets from the given introduction rules.

   196 \item [$mono$] declares monotonicity rules.  These rule are involved in the

   197   automated monotonicity proof of $\isarkeyword{inductive}$.

   198 \item [$\isarkeyword{inductive_cases}$] creates instances of elimination rules

   199   of (co)inductive sets, solving obvious cases by simplification.

   200

   201   The $cases$ proof method (see \S\ref{sec:induct-method}) provides a more

   202   direct way for reasoning by cases (including optional simplification).

   203

   204   Unlike the \texttt{mk_cases} ML function exported with any inductive

   205   definition \cite{isabelle-HOL}, $\isarkeyword{inductive_cases}$ it does

   206   \emph{not} modify cases by simplification that are not solved completely

   207   anyway (e.g.\ due to contradictory assumptions).  Thus

   208   $\isarkeyword{inductive_cases}$ conforms to the way Isar proofs are

   209   conducted, rather than old-style tactic scripts.

   210 \end{descr}

   211

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

   213 HOL.

   214

   215

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

   217

   218 \subsection{Proof methods}

   219

   220 \indexisarmeth{cases}\indexisarmeth{induct}

   221 \begin{matharray}{rcl}

   222   cases & : & \isarmeth \\

   223   induct & : & \isarmeth \\

   224 \end{matharray}

   225

   226 The $cases$ and $induct$ methods provide a uniform interface to case analysis

   227 and induction over datatypes, inductive sets, and recursive functions.  The

   228 corresponding rules may be specified and instantiated in a casual manner.

   229 Furthermore, these methods provide named local contexts that may be invoked

   230 via the $\CASENAME$ proof command within the subsequent proof text (cf.\

   231 \S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning

   232 about large specifications.

   233

   234 \begin{rail}

   235   'cases' ('simplified' ':')? term? rule?  ;

   236

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

   238   ;

   239

   240   inst: (term +)

   241   ;

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

   243   ;

   244 \end{rail}

   245

   246 \begin{descr}

   247 \item [$cases~t~R$] applies method $rule$ with an appropriate case distinction

   248   theorem, instantiated to the subject $t$.  Symbolic case names are bound

   249   according to the rule's local contexts.

   250

   251   The rule is determined as follows, according to the facts and arguments

   252   passed to the $cases$ method:

   253   \begin{matharray}{llll}

   254     \text{facts}    &       & \text{arguments} & \text{rule} \\\hline

   255                     & cases &           & \text{classical case split} \\

   256                     & cases & t         & \text{datatype exhaustion (type of $t$)} \\

   257     \edrv a \in A   & cases & \dots     & \text{inductive set elimination (of $A$)} \\

   258     \dots           & cases & \dots ~ R & \text{explicit rule $R$} \\

   259   \end{matharray}

   260

   261   The $simplified$ option causes obvious cases'' of the rule to be solved

   262   beforehand, while the others are left unscathed.

   263

   264 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to

   265   induction rules, which are determined as follows:

   266   \begin{matharray}{llll}

   267     \text{facts}    &        & \text{arguments} & \text{rule} \\\hline

   268                     & induct & P ~ x ~ \dots & \text{datatype induction (type of $x$)} \\

   269     \edrv x \in A   & induct & \dots         & \text{set induction (of $A$)} \\

   270     \dots           & induct & \dots ~ R     & \text{explicit rule $R$} \\

   271   \end{matharray}

   272

   273   Several instantiations may be given, each referring to some part of a mutual

   274   inductive definition or datatype --- only related partial induction rules

   275   may be used together, though.  Any of the lists of terms $P, x, \dots$

   276   refers to the \emph{suffix} of variables present in the induction rule.

   277   This enables the writer to specify only induction variables, or both

   278   predicates and variables, for example.

   279

   280   The $stripped$ option causes implications and (bounded) universal

   281   quantifiers to be removed from each new subgoal emerging from the

   282   application of the induction rule.  This accommodates typical

   283   strengthening of induction'' predicates.

   284 \end{descr}

   285

   286 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as

   287 determined by the instantiated rule \emph{before} it has been applied to the

   288 internal proof state.\footnote{As a general principle, Isar proof text may

   289   never refer to parts of proof states directly.} Thus proper use of symbolic

   290 cases usually require the rule to be instantiated fully, as far as the

   291 emerging local contexts and subgoals are concerned.  In particular, for

   292 induction both the predicates and variables have to be specified.  Otherwise

   293 the $\CASENAME$ command would refuse to invoke cases containing schematic

   294 variables.

   295

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

   297 cases present in the current proof state.

   298

   299

   300 \subsection{Declaring rules}

   301

   302 \indexisaratt{cases}\indexisaratt{induct}

   303 \begin{matharray}{rcl}

   304   cases & : & \isaratt \\

   305   induct & : & \isaratt \\

   306 \end{matharray}

   307

   308 \begin{rail}

   309   'cases' spec

   310   ;

   311   'induct' spec

   312   ;

   313

   314   spec: ('type' | 'set') ':' nameref

   315   ;

   316 \end{rail}

   317

   318 The $cases$ and $induct$ attributes augment the corresponding context of rules

   319 for reasoning about inductive sets and types.  The standard rules are already

   320 declared by HOL definitional packages.  For special applications, these may be

   321 replaced manually by variant versions.

   322

   323 Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to

   324 adjust names of cases and parameters of a rule.

   325

   326

   327 \section{Arithmetic}

   328

   329 \indexisarmeth{arith}

   330 \begin{matharray}{rcl}

   331   arith & : & \isarmeth \\

   332 \end{matharray}

   333

   334 \begin{rail}

   335   'arith' '!'?

   336   ;

   337 \end{rail}

   338

   339 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,

   340 $real$).  Any current facts are inserted into the goal before running the

   341 procedure.  The !''~argument causes the full context of assumptions to be

   342 included as well.

   343

   344 Note that a simpler (but faster) version of arithmetic reasoning is already

   345 performed by the Simplifier.

   346

   347

   348 %%% Local Variables:

   349 %%% mode: latex

   350 %%% TeX-master: "isar-ref"

   351 %%% End: