doc-src/IsarRef/hol.tex
author wenzelm
Sat Apr 01 20:21:39 2000 +0200 (2000-04-01)
changeset 8657 b9475dad85ed
parent 8547 93b8685d004b
child 8665 403c2985e65e
permissions -rw-r--r--
recdef: admit names/atts;
wenzelm@7046
     1
wenzelm@7167
     2
\chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
wenzelm@7135
     3
wenzelm@7990
     4
\section{Miscellaneous attributes}
wenzelm@7990
     5
wenzelm@7990
     6
\indexisaratt{rulify}\indexisaratt{rulify-prems}
wenzelm@7990
     7
\begin{matharray}{rcl}
wenzelm@7990
     8
  rulify & : & \isaratt \\
wenzelm@7990
     9
  rulify_prems & : & \isaratt \\
wenzelm@7990
    10
\end{matharray}
wenzelm@7990
    11
wenzelm@7990
    12
\begin{descr}
wenzelm@7990
    13
wenzelm@7990
    14
\item [$rulify$] puts a theorem into object-rule form, replacing implication
wenzelm@7990
    15
  and universal quantification of HOL by the corresponding meta-logical
wenzelm@7990
    16
  connectives.  This is the same operation as performed by the
wenzelm@7990
    17
  \texttt{qed_spec_mp} ML function.
wenzelm@7990
    18
  
wenzelm@7990
    19
\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
wenzelm@7990
    20
  rule.
wenzelm@7990
    21
wenzelm@7990
    22
\end{descr}
wenzelm@7990
    23
wenzelm@7990
    24
wenzelm@7135
    25
\section{Primitive types}
wenzelm@7135
    26
wenzelm@7141
    27
\indexisarcmd{typedecl}\indexisarcmd{typedef}
wenzelm@7141
    28
\begin{matharray}{rcl}
wenzelm@7141
    29
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    30
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7141
    31
\end{matharray}
wenzelm@7141
    32
wenzelm@7141
    33
\begin{rail}
wenzelm@7141
    34
  'typedecl' typespec infix? comment?
wenzelm@7141
    35
  ;
wenzelm@7141
    36
  'typedef' parname? typespec infix? \\ '=' term comment?
wenzelm@7141
    37
  ;
wenzelm@7141
    38
\end{rail}
wenzelm@7141
    39
wenzelm@7167
    40
\begin{descr}
wenzelm@7141
    41
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
wenzelm@7141
    42
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
wenzelm@7141
    43
  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
wenzelm@7141
    44
  actual HOL type constructor.
wenzelm@7141
    45
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
wenzelm@7141
    46
  non-emptiness of the set $A$.  After finishing the proof, the theory will be
wenzelm@7175
    47
  augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
wenzelm@7335
    48
  for more information.  Note that user-level theories usually do not directly
wenzelm@7335
    49
  refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
wenzelm@7335
    50
  packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and
wenzelm@7175
    51
  $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).
wenzelm@7167
    52
\end{descr}
wenzelm@7141
    53
wenzelm@7141
    54
wenzelm@7141
    55
\section{Records}\label{sec:record}
wenzelm@7141
    56
wenzelm@7141
    57
%FIXME record_split method
wenzelm@7141
    58
\indexisarcmd{record}
wenzelm@7141
    59
\begin{matharray}{rcl}
wenzelm@7141
    60
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    61
\end{matharray}
wenzelm@7141
    62
wenzelm@7141
    63
\begin{rail}
wenzelm@7141
    64
  'record' typespec '=' (type '+')? (field +)
wenzelm@7141
    65
  ;
wenzelm@7135
    66
wenzelm@7141
    67
  field: name '::' type comment?
wenzelm@7141
    68
  ;
wenzelm@7141
    69
\end{rail}
wenzelm@7141
    70
wenzelm@7167
    71
\begin{descr}
wenzelm@7141
    72
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
wenzelm@7141
    73
  defines extensible record type $(\vec\alpha)t$, derived from the optional
wenzelm@7141
    74
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
wenzelm@7335
    75
  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
wenzelm@7335
    76
  simply-typed extensible records.
wenzelm@7167
    77
\end{descr}
wenzelm@7141
    78
wenzelm@7141
    79
wenzelm@7141
    80
\section{Datatypes}\label{sec:datatype}
wenzelm@7141
    81
wenzelm@7167
    82
\indexisarcmd{datatype}\indexisarcmd{rep-datatype}
wenzelm@7141
    83
\begin{matharray}{rcl}
wenzelm@7141
    84
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    85
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    86
\end{matharray}
wenzelm@7141
    87
wenzelm@7141
    88
\railalias{repdatatype}{rep\_datatype}
wenzelm@7141
    89
\railterm{repdatatype}
wenzelm@7141
    90
wenzelm@7141
    91
\begin{rail}
wenzelm@7175
    92
  'datatype' (parname? typespec infix? \\ '=' (constructor + '|') + 'and')
wenzelm@7141
    93
  ;
wenzelm@7141
    94
  repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
wenzelm@7141
    95
  ;
wenzelm@7141
    96
wenzelm@7175
    97
  constructor: name (type * ) mixfix? comment?
wenzelm@7141
    98
  ;
wenzelm@7141
    99
\end{rail}
wenzelm@7141
   100
wenzelm@7167
   101
\begin{descr}
wenzelm@7319
   102
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
wenzelm@7319
   103
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
wenzelm@7319
   104
  ones, generating the standard infrastructure of derived concepts (primitive
wenzelm@7319
   105
  recursion etc.).
wenzelm@7167
   106
\end{descr}
wenzelm@7141
   107
wenzelm@8449
   108
The induction and exhaustion theorems generated provide case names according
wenzelm@8449
   109
to the constructors involved, while parameters are named after the types (see
wenzelm@8449
   110
also \S\ref{sec:induct-method}).
wenzelm@8449
   111
wenzelm@7319
   112
See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
wenzelm@7335
   113
syntax above has been slightly simplified over the old version, usually
wenzelm@8531
   114
requiring more quotes and less parentheses.  Apart from proper proof methods
wenzelm@8531
   115
for case-analysis and induction, there are also emulations of ML tactics
wenzelm@8531
   116
\texttt{case_tac}\indexisarmeth{case-tac} and
wenzelm@8531
   117
\texttt{induct_tac}\indexisarmeth{induct-tac} available, with similar syntax
wenzelm@8531
   118
as $subgoal_tac$, see \S\ref{sec:tactical-proof}.
wenzelm@7319
   119
wenzelm@7135
   120
wenzelm@7135
   121
\section{Recursive functions}
wenzelm@7135
   122
wenzelm@7141
   123
\indexisarcmd{primrec}\indexisarcmd{recdef}
wenzelm@7141
   124
\begin{matharray}{rcl}
wenzelm@7141
   125
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   126
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   127
%FIXME
wenzelm@7141
   128
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   129
\end{matharray}
wenzelm@7141
   130
wenzelm@7141
   131
\begin{rail}
wenzelm@8657
   132
  'primrec' parname? (equation + )
wenzelm@8657
   133
  ;
wenzelm@8657
   134
  'recdef' name term (equation +) hints
wenzelm@7141
   135
  ;
wenzelm@8657
   136
wenzelm@8657
   137
  equation: thmdecl? prop comment?
wenzelm@8657
   138
  ;
wenzelm@8657
   139
  hints: ('congs' thmrefs)? ('simpset' name)?
wenzelm@7141
   140
  ;
wenzelm@7141
   141
\end{rail}
wenzelm@7141
   142
wenzelm@7167
   143
\begin{descr}
wenzelm@7319
   144
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
wenzelm@7319
   145
  datatypes.
wenzelm@7319
   146
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
wenzelm@7319
   147
  functions (using the TFL package).
wenzelm@7167
   148
\end{descr}
wenzelm@7141
   149
wenzelm@8449
   150
Both definitions accommodate reasoning proof by induction (cf.\ 
wenzelm@8449
   151
\S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
wenzelm@8449
   152
of the function definition) refers to a specific induction rule, with
wenzelm@8449
   153
parameters named according to the user-specified equations.  Case names of
wenzelm@8449
   154
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
wenzelm@8449
   155
$\isarkeyword{recdef}$ are numbered (starting from $1$).
wenzelm@8449
   156
wenzelm@8657
   157
The equations provided by these packages may be referred later as theorem list
wenzelm@8657
   158
$f\mathord.simps$, where $f$ is the (collective) name of the functions
wenzelm@8657
   159
defined.  Individual equations may be named explicitly as well; note that for
wenzelm@8657
   160
$\isarkeyword{recdef}$ each specification given by the user may result in
wenzelm@8657
   161
several theorems.
wenzelm@8657
   162
wenzelm@8449
   163
See \cite{isabelle-HOL} for further information on recursive function
wenzelm@8449
   164
definitions in HOL.
wenzelm@7319
   165
wenzelm@7141
   166
wenzelm@7135
   167
\section{(Co)Inductive sets}
wenzelm@7135
   168
wenzelm@7167
   169
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
wenzelm@7990
   170
\indexisaratt{mono}
wenzelm@7141
   171
\begin{matharray}{rcl}
wenzelm@7141
   172
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   173
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
wenzelm@7990
   174
  mono & : & \isaratt \\
wenzelm@7141
   175
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   176
\end{matharray}
wenzelm@7141
   177
wenzelm@7141
   178
\railalias{condefs}{con\_defs}
wenzelm@7141
   179
\railalias{indcases}{inductive\_cases}
wenzelm@7141
   180
\railterm{condefs,indcases}
wenzelm@7141
   181
wenzelm@7141
   182
\begin{rail}
wenzelm@7141
   183
  ('inductive' | 'coinductive') (term comment? +) \\
wenzelm@7141
   184
    'intrs' attributes? (thmdecl? prop comment? +) \\
wenzelm@7141
   185
    'monos' thmrefs comment? \\ condefs thmrefs comment?
wenzelm@7141
   186
  ;
wenzelm@7141
   187
  indcases thmdef? nameref ':' \\ (prop +) comment?
wenzelm@7141
   188
  ;
wenzelm@7990
   189
  'mono' (() | 'add' | 'del')
wenzelm@7990
   190
  ;
wenzelm@7141
   191
\end{rail}
wenzelm@7141
   192
wenzelm@7167
   193
\begin{descr}
wenzelm@7319
   194
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
wenzelm@7319
   195
  (co)inductive sets from the given introduction rules.
wenzelm@8547
   196
\item [$mono$] declares monotonicity rules.  These rule are involved in the
wenzelm@8547
   197
  automated monotonicity proof of $\isarkeyword{inductive}$.
wenzelm@8449
   198
\item [$\isarkeyword{inductive_cases}$] creates instances of elimination rules
wenzelm@8449
   199
  of (co)inductive sets, solving obvious cases by simplification.
wenzelm@8449
   200
  
wenzelm@8449
   201
  The $cases$ proof method (see \S\ref{sec:induct-method}) provides a more
wenzelm@8449
   202
  direct way for reasoning by cases (including optional simplification).
wenzelm@8449
   203
  
wenzelm@8449
   204
  Unlike the \texttt{mk_cases} ML function exported with any inductive
wenzelm@8449
   205
  definition \cite{isabelle-HOL}, $\isarkeyword{inductive_cases}$ it does
wenzelm@8547
   206
  \emph{not} modify cases by simplification that are not solved completely
wenzelm@8547
   207
  anyway (e.g.\ due to contradictory assumptions).  Thus
wenzelm@8547
   208
  $\isarkeyword{inductive_cases}$ conforms to the way Isar proofs are
wenzelm@8547
   209
  conducted, rather than old-style tactic scripts.
wenzelm@7167
   210
\end{descr}
wenzelm@7141
   211
wenzelm@8449
   212
See \cite{isabelle-HOL} for further information on inductive definitions in
wenzelm@8449
   213
HOL.
wenzelm@7319
   214
wenzelm@7141
   215
wenzelm@8449
   216
\section{Proof by cases and induction}\label{sec:induct-method}
wenzelm@8449
   217
wenzelm@8449
   218
\subsection{Proof methods}
wenzelm@7141
   219
wenzelm@8449
   220
\indexisarmeth{cases}\indexisarmeth{induct}
wenzelm@7319
   221
\begin{matharray}{rcl}
wenzelm@8449
   222
  cases & : & \isarmeth \\
wenzelm@7319
   223
  induct & : & \isarmeth \\
wenzelm@7319
   224
\end{matharray}
wenzelm@7319
   225
wenzelm@8449
   226
The $cases$ and $induct$ methods provide a uniform interface to case analysis
wenzelm@8449
   227
and induction over datatypes, inductive sets, and recursive functions.  The
wenzelm@8449
   228
corresponding rules may be specified and instantiated in a casual manner.
wenzelm@8449
   229
Furthermore, these methods provide named local contexts that may be invoked
wenzelm@8449
   230
via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
wenzelm@8484
   231
\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
wenzelm@8484
   232
about large specifications.
wenzelm@7319
   233
wenzelm@7319
   234
\begin{rail}
wenzelm@8449
   235
  'cases' ('simplified' ':')? term? rule?  ;
wenzelm@8449
   236
wenzelm@8449
   237
  'induct' ('stripped' ':')? (inst * 'and') rule?
wenzelm@7319
   238
  ;
wenzelm@7319
   239
wenzelm@8449
   240
  inst: (term +)
wenzelm@7319
   241
  ;
wenzelm@8449
   242
  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
wenzelm@7319
   243
  ;
wenzelm@7319
   244
\end{rail}
wenzelm@7319
   245
wenzelm@7319
   246
\begin{descr}
wenzelm@8449
   247
\item [$cases~t~R$] applies method $rule$ with an appropriate case distinction
wenzelm@8449
   248
  theorem, instantiated to the subject $t$.  Symbolic case names are bound
wenzelm@8449
   249
  according to the rule's local contexts.
wenzelm@8449
   250
  
wenzelm@8449
   251
  The rule is determined as follows, according to the facts and arguments
wenzelm@8449
   252
  passed to the $cases$ method:
wenzelm@8449
   253
  \begin{matharray}{llll}
wenzelm@8449
   254
    \text{facts}    &       & \text{arguments} & \text{rule} \\\hline
wenzelm@8449
   255
                    & cases &           & \text{classical case split} \\
wenzelm@8449
   256
                    & cases & t         & \text{datatype exhaustion (type of $t$)} \\
wenzelm@8449
   257
    \edrv a \in A   & cases & \dots     & \text{inductive set elimination (of $A$)} \\
wenzelm@8449
   258
    \dots           & cases & \dots ~ R & \text{explicit rule $R$} \\
wenzelm@8449
   259
  \end{matharray}
wenzelm@8449
   260
wenzelm@8449
   261
  The $simplified$ option causes ``obvious cases'' of the rule to be solved
wenzelm@8449
   262
  beforehand, while the others are left unscathed.
wenzelm@8449
   263
  
wenzelm@8449
   264
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
wenzelm@8449
   265
  induction rules, which are determined as follows:
wenzelm@8449
   266
  \begin{matharray}{llll}
wenzelm@8449
   267
    \text{facts}    &        & \text{arguments} & \text{rule} \\\hline
wenzelm@8449
   268
                    & induct & P ~ x ~ \dots & \text{datatype induction (type of $x$)} \\
wenzelm@8449
   269
    \edrv x \in A   & induct & \dots         & \text{set induction (of $A$)} \\
wenzelm@8449
   270
    \dots           & induct & \dots ~ R     & \text{explicit rule $R$} \\
wenzelm@8449
   271
  \end{matharray}
wenzelm@8449
   272
  
wenzelm@8449
   273
  Several instantiations may be given, each referring to some part of a mutual
wenzelm@8449
   274
  inductive definition or datatype --- only related partial induction rules
wenzelm@8449
   275
  may be used together, though.  Any of the lists of terms $P, x, \dots$
wenzelm@8449
   276
  refers to the \emph{suffix} of variables present in the induction rule.
wenzelm@8449
   277
  This enables the writer to specify only induction variables, or both
wenzelm@8449
   278
  predicates and variables, for example.
wenzelm@7507
   279
  
wenzelm@8449
   280
  The $stripped$ option causes implications and (bounded) universal
wenzelm@8449
   281
  quantifiers to be removed from each new subgoal emerging from the
wenzelm@8547
   282
  application of the induction rule.  This accommodates typical
wenzelm@8547
   283
  ``strengthening of induction'' predicates.
wenzelm@7319
   284
\end{descr}
wenzelm@7141
   285
wenzelm@8484
   286
Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
wenzelm@8484
   287
determined by the instantiated rule \emph{before} it has been applied to the
wenzelm@8484
   288
internal proof state.\footnote{As a general principle, Isar proof text may
wenzelm@8449
   289
  never refer to parts of proof states directly.} Thus proper use of symbolic
wenzelm@8449
   290
cases usually require the rule to be instantiated fully, as far as the
wenzelm@8449
   291
emerging local contexts and subgoals are concerned.  In particular, for
wenzelm@8449
   292
induction both the predicates and variables have to be specified.  Otherwise
wenzelm@8547
   293
the $\CASENAME$ command would refuse to invoke cases containing schematic
wenzelm@8449
   294
variables.
wenzelm@8449
   295
wenzelm@8449
   296
The $\isarkeyword{print_cases}$ command (\S\ref{sec:diag}) prints all named
wenzelm@8547
   297
cases present in the current proof state.
wenzelm@8449
   298
wenzelm@8449
   299
wenzelm@8484
   300
\subsection{Declaring rules}
wenzelm@8449
   301
wenzelm@8449
   302
\indexisaratt{cases}\indexisaratt{induct}
wenzelm@8449
   303
\begin{matharray}{rcl}
wenzelm@8449
   304
  cases & : & \isaratt \\
wenzelm@8449
   305
  induct & : & \isaratt \\
wenzelm@8449
   306
\end{matharray}
wenzelm@8449
   307
wenzelm@8449
   308
\begin{rail}
wenzelm@8449
   309
  'cases' spec
wenzelm@8449
   310
  ;
wenzelm@8449
   311
  'induct' spec
wenzelm@8449
   312
  ;
wenzelm@8449
   313
wenzelm@8449
   314
  spec: ('type' | 'set') ':' nameref
wenzelm@8449
   315
  ;
wenzelm@8449
   316
\end{rail}
wenzelm@8449
   317
wenzelm@8449
   318
The $cases$ and $induct$ attributes augment the corresponding context of rules
wenzelm@8449
   319
for reasoning about inductive sets and types.  The standard rules are already
wenzelm@8449
   320
declared by HOL definitional packages.  For special applications, these may be
wenzelm@8449
   321
replaced manually by variant versions.
wenzelm@8449
   322
wenzelm@8484
   323
Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
wenzelm@8484
   324
adjust names of cases and parameters of a rule.
wenzelm@8484
   325
wenzelm@7046
   326
wenzelm@7390
   327
\section{Arithmetic}
wenzelm@7390
   328
wenzelm@7390
   329
\indexisarmeth{arith}
wenzelm@7390
   330
\begin{matharray}{rcl}
wenzelm@7390
   331
  arith & : & \isarmeth \\
wenzelm@7390
   332
\end{matharray}
wenzelm@7390
   333
wenzelm@8506
   334
\begin{rail}
wenzelm@8506
   335
  'arith' '!'?
wenzelm@8506
   336
  ;
wenzelm@8506
   337
\end{rail}
wenzelm@8506
   338
wenzelm@7390
   339
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
wenzelm@8506
   340
$real$).  Any current facts are inserted into the goal before running the
wenzelm@8506
   341
procedure.  The ``!''~argument causes the full context of assumptions to be
wenzelm@8506
   342
included as well.
wenzelm@8506
   343
wenzelm@8506
   344
Note that a simpler (but faster) version of arithmetic reasoning is already
wenzelm@8506
   345
performed by the Simplifier.
wenzelm@7390
   346
wenzelm@7390
   347
wenzelm@7046
   348
%%% Local Variables: 
wenzelm@7046
   349
%%% mode: latex
wenzelm@7046
   350
%%% TeX-master: "isar-ref"
wenzelm@7046
   351
%%% End: