doc-src/IsarRef/hol.tex
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9935 a87965201c34
child 9949 1741a61d4b33
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
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@9941
     6
\indexisaratt{rule-format}
wenzelm@7990
     7
\begin{matharray}{rcl}
wenzelm@9941
     8
  rule_format & : & \isaratt \\
wenzelm@7990
     9
\end{matharray}
wenzelm@7990
    10
wenzelm@9941
    11
\railalias{ruleformat}{rule\_format}
wenzelm@9941
    12
\railterm{ruleformat}
wenzelm@9941
    13
wenzelm@9905
    14
\begin{rail}
wenzelm@9941
    15
  ruleformat ('(' noasm ')')?
wenzelm@9905
    16
  ;
wenzelm@9905
    17
\end{rail}
wenzelm@9905
    18
wenzelm@7990
    19
\begin{descr}
wenzelm@9848
    20
  
wenzelm@9941
    21
\item [$rule_format$] causes a theorem to be put into standard object-rule
wenzelm@9941
    22
  form, replacing implication and (bounded) universal quantification of HOL by
wenzelm@9941
    23
  the corresponding meta-logical connectives.  By default, the result is fully
wenzelm@9905
    24
  normalized, including assumptions and conclusions at any depth.  The
wenzelm@9905
    25
  $no_asm$ option restricts the transformation to the conclusion of a rule.
wenzelm@7990
    26
\end{descr}
wenzelm@7990
    27
wenzelm@7990
    28
wenzelm@7135
    29
\section{Primitive types}
wenzelm@7135
    30
wenzelm@7141
    31
\indexisarcmd{typedecl}\indexisarcmd{typedef}
wenzelm@7141
    32
\begin{matharray}{rcl}
wenzelm@7141
    33
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    34
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7141
    35
\end{matharray}
wenzelm@7141
    36
wenzelm@7141
    37
\begin{rail}
wenzelm@7141
    38
  'typedecl' typespec infix? comment?
wenzelm@7141
    39
  ;
wenzelm@7141
    40
  'typedef' parname? typespec infix? \\ '=' term comment?
wenzelm@7141
    41
  ;
wenzelm@7141
    42
\end{rail}
wenzelm@7141
    43
wenzelm@7167
    44
\begin{descr}
wenzelm@7141
    45
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
wenzelm@7141
    46
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
wenzelm@7141
    47
  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
wenzelm@7141
    48
  actual HOL type constructor.
wenzelm@7141
    49
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
wenzelm@7141
    50
  non-emptiness of the set $A$.  After finishing the proof, the theory will be
wenzelm@7175
    51
  augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
wenzelm@7335
    52
  for more information.  Note that user-level theories usually do not directly
wenzelm@7335
    53
  refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
wenzelm@7335
    54
  packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and
wenzelm@7175
    55
  $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).
wenzelm@7167
    56
\end{descr}
wenzelm@7141
    57
wenzelm@7141
    58
wenzelm@7141
    59
\section{Records}\label{sec:record}
wenzelm@7141
    60
wenzelm@7141
    61
\indexisarcmd{record}
wenzelm@7141
    62
\begin{matharray}{rcl}
wenzelm@7141
    63
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    64
\end{matharray}
wenzelm@7141
    65
wenzelm@7141
    66
\begin{rail}
wenzelm@7141
    67
  'record' typespec '=' (type '+')? (field +)
wenzelm@7141
    68
  ;
wenzelm@7135
    69
wenzelm@7141
    70
  field: name '::' type comment?
wenzelm@7141
    71
  ;
wenzelm@7141
    72
\end{rail}
wenzelm@7141
    73
wenzelm@7167
    74
\begin{descr}
wenzelm@7141
    75
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
wenzelm@7141
    76
  defines extensible record type $(\vec\alpha)t$, derived from the optional
wenzelm@7141
    77
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
wenzelm@7335
    78
  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
wenzelm@7335
    79
  simply-typed extensible records.
wenzelm@7167
    80
\end{descr}
wenzelm@7141
    81
wenzelm@7141
    82
wenzelm@7141
    83
\section{Datatypes}\label{sec:datatype}
wenzelm@7141
    84
wenzelm@7167
    85
\indexisarcmd{datatype}\indexisarcmd{rep-datatype}
wenzelm@7141
    86
\begin{matharray}{rcl}
wenzelm@7141
    87
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    88
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
wenzelm@7141
    89
\end{matharray}
wenzelm@7141
    90
wenzelm@7141
    91
\railalias{repdatatype}{rep\_datatype}
wenzelm@7141
    92
\railterm{repdatatype}
wenzelm@7141
    93
wenzelm@7141
    94
\begin{rail}
wenzelm@9848
    95
  'datatype' (dtspec + 'and')
wenzelm@7141
    96
  ;
wenzelm@9848
    97
  repdatatype (name * ) dtrules
wenzelm@7141
    98
  ;
wenzelm@7141
    99
wenzelm@9848
   100
  dtspec: parname? typespec infix? '=' (cons + '|')
wenzelm@7141
   101
  ;
wenzelm@9848
   102
  cons: name (type * ) mixfix? comment?
wenzelm@9848
   103
  ;
wenzelm@9848
   104
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
wenzelm@7141
   105
\end{rail}
wenzelm@7141
   106
wenzelm@7167
   107
\begin{descr}
wenzelm@7319
   108
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
wenzelm@7319
   109
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
wenzelm@7319
   110
  ones, generating the standard infrastructure of derived concepts (primitive
wenzelm@7319
   111
  recursion etc.).
wenzelm@7167
   112
\end{descr}
wenzelm@7141
   113
wenzelm@8449
   114
The induction and exhaustion theorems generated provide case names according
wenzelm@8449
   115
to the constructors involved, while parameters are named after the types (see
wenzelm@8449
   116
also \S\ref{sec:induct-method}).
wenzelm@8449
   117
wenzelm@7319
   118
See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
wenzelm@7335
   119
syntax above has been slightly simplified over the old version, usually
wenzelm@8531
   120
requiring more quotes and less parentheses.  Apart from proper proof methods
wenzelm@8531
   121
for case-analysis and induction, there are also emulations of ML tactics
wenzelm@8945
   122
\texttt{case_tac} and \texttt{induct_tac} available, see
wenzelm@8665
   123
\S\ref{sec:induct_tac}.
wenzelm@7319
   124
wenzelm@7135
   125
wenzelm@7135
   126
\section{Recursive functions}
wenzelm@7135
   127
wenzelm@7141
   128
\indexisarcmd{primrec}\indexisarcmd{recdef}
wenzelm@7141
   129
\begin{matharray}{rcl}
wenzelm@7141
   130
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   131
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   132
%FIXME
wenzelm@7141
   133
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   134
\end{matharray}
wenzelm@7141
   135
wenzelm@7141
   136
\begin{rail}
wenzelm@8657
   137
  'primrec' parname? (equation + )
wenzelm@8657
   138
  ;
wenzelm@9848
   139
  'recdef' name term (eqn + ) hints?
wenzelm@9848
   140
  ;
wenzelm@8657
   141
wenzelm@9848
   142
  equation: thmdecl? eqn
wenzelm@9848
   143
  ;
wenzelm@9848
   144
  eqn: prop comment?
wenzelm@8657
   145
  ;
wenzelm@9848
   146
  hints: '(' 'hints' (recdefmod * ) ')'
wenzelm@9848
   147
  ;
wenzelm@9848
   148
  recdefmod: (('simp' | 'cong' | 'wf' | 'split' | 'iff') (() | 'add' | 'del') ':' thmrefs) | clamod
wenzelm@7141
   149
  ;
wenzelm@7141
   150
\end{rail}
wenzelm@7141
   151
wenzelm@7167
   152
\begin{descr}
wenzelm@7319
   153
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
wenzelm@9848
   154
  datatypes, see also \cite{isabelle-HOL}.
wenzelm@7319
   155
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
wenzelm@9848
   156
  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
wenzelm@9848
   157
  $simp$, $cong$, and $wf$ hints refer to auxiliary rules to be used in the
wenzelm@9848
   158
  internal automated proof process of TFL; the other declarations refer to the
wenzelm@9848
   159
  Simplifier and Classical reasoner (\S\ref{sec:simplifier},
wenzelm@9848
   160
  \S\ref{sec:classical}, \S\ref{sec:clasimp}) that are used internally.
wenzelm@7167
   161
\end{descr}
wenzelm@7141
   162
wenzelm@9848
   163
Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
wenzelm@8449
   164
\S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
wenzelm@8449
   165
of the function definition) refers to a specific induction rule, with
wenzelm@8449
   166
parameters named according to the user-specified equations.  Case names of
wenzelm@8449
   167
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
wenzelm@8449
   168
$\isarkeyword{recdef}$ are numbered (starting from $1$).
wenzelm@8449
   169
wenzelm@8657
   170
The equations provided by these packages may be referred later as theorem list
wenzelm@8657
   171
$f\mathord.simps$, where $f$ is the (collective) name of the functions
wenzelm@8657
   172
defined.  Individual equations may be named explicitly as well; note that for
wenzelm@8657
   173
$\isarkeyword{recdef}$ each specification given by the user may result in
wenzelm@8657
   174
several theorems.
wenzelm@8657
   175
wenzelm@9935
   176
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
wenzelm@9935
   177
the following attributes.
wenzelm@9935
   178
wenzelm@9935
   179
\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
wenzelm@9935
   180
\begin{matharray}{rcl}
wenzelm@9935
   181
  recdef_simp & : & \isaratt \\
wenzelm@9935
   182
  recdef_cong & : & \isaratt \\
wenzelm@9935
   183
  recdef_wf & : & \isaratt \\
wenzelm@9935
   184
\end{matharray}
wenzelm@9935
   185
wenzelm@9935
   186
\railalias{recdefsimp}{recdef\_simp}
wenzelm@9935
   187
\railterm{recdefsimp}
wenzelm@9935
   188
wenzelm@9935
   189
\railalias{recdefcong}{recdef\_cong}
wenzelm@9935
   190
\railterm{recdefcong}
wenzelm@9935
   191
wenzelm@9935
   192
\railalias{recdefwf}{recdef\_wf}
wenzelm@9935
   193
\railterm{recdefwf}
wenzelm@9935
   194
wenzelm@9935
   195
\begin{rail}
wenzelm@9935
   196
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
wenzelm@9935
   197
  ;
wenzelm@9935
   198
\end{rail}
wenzelm@9935
   199
wenzelm@7141
   200
wenzelm@7135
   201
\section{(Co)Inductive sets}
wenzelm@7135
   202
wenzelm@9602
   203
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
wenzelm@7141
   204
\begin{matharray}{rcl}
wenzelm@7141
   205
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
wenzelm@9848
   206
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
wenzelm@7990
   207
  mono & : & \isaratt \\
wenzelm@7141
   208
\end{matharray}
wenzelm@7141
   209
wenzelm@7141
   210
\railalias{condefs}{con\_defs}
wenzelm@9602
   211
\railterm{condefs}
wenzelm@7141
   212
wenzelm@7141
   213
\begin{rail}
wenzelm@9848
   214
  ('inductive' | 'coinductive') sets intros monos?
wenzelm@7141
   215
  ;
wenzelm@7990
   216
  'mono' (() | 'add' | 'del')
wenzelm@7990
   217
  ;
wenzelm@9848
   218
wenzelm@9848
   219
  sets: (term comment? +)
wenzelm@9848
   220
  ;
wenzelm@9848
   221
  intros: 'intros' attributes? (thmdecl? prop comment? +)
wenzelm@9848
   222
  ;
wenzelm@9848
   223
  monos: 'monos' thmrefs comment?
wenzelm@9848
   224
  ;
wenzelm@7141
   225
\end{rail}
wenzelm@7141
   226
wenzelm@7167
   227
\begin{descr}
wenzelm@7319
   228
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
wenzelm@7319
   229
  (co)inductive sets from the given introduction rules.
wenzelm@8547
   230
\item [$mono$] declares monotonicity rules.  These rule are involved in the
wenzelm@8547
   231
  automated monotonicity proof of $\isarkeyword{inductive}$.
wenzelm@7167
   232
\end{descr}
wenzelm@7141
   233
wenzelm@8449
   234
See \cite{isabelle-HOL} for further information on inductive definitions in
wenzelm@8449
   235
HOL.
wenzelm@7319
   236
wenzelm@7141
   237
wenzelm@8449
   238
\section{Proof by cases and induction}\label{sec:induct-method}
wenzelm@8449
   239
wenzelm@8666
   240
\subsection{Proof methods}\label{sec:induct-method-proper}
wenzelm@7141
   241
wenzelm@8449
   242
\indexisarmeth{cases}\indexisarmeth{induct}
wenzelm@7319
   243
\begin{matharray}{rcl}
wenzelm@8449
   244
  cases & : & \isarmeth \\
wenzelm@7319
   245
  induct & : & \isarmeth \\
wenzelm@7319
   246
\end{matharray}
wenzelm@7319
   247
wenzelm@8449
   248
The $cases$ and $induct$ methods provide a uniform interface to case analysis
wenzelm@8449
   249
and induction over datatypes, inductive sets, and recursive functions.  The
wenzelm@8449
   250
corresponding rules may be specified and instantiated in a casual manner.
wenzelm@8449
   251
Furthermore, these methods provide named local contexts that may be invoked
wenzelm@8449
   252
via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
wenzelm@8484
   253
\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
wenzelm@8484
   254
about large specifications.
wenzelm@7319
   255
wenzelm@7319
   256
\begin{rail}
wenzelm@9848
   257
  'cases' simplified? open? args rule?
wenzelm@9848
   258
  ;
wenzelm@9848
   259
  'induct' stripped? open? args rule?
wenzelm@7319
   260
  ;
wenzelm@7319
   261
wenzelm@9848
   262
  simplified: '(' 'simplified' ')'
wenzelm@9848
   263
  ;
wenzelm@9848
   264
  stripped: '(' 'stripped' ')'
wenzelm@9848
   265
  ;
wenzelm@9848
   266
  open: '(' 'open' ')'
wenzelm@9848
   267
  ;
wenzelm@9848
   268
  args: (insts * 'and') 
wenzelm@9848
   269
  ;
wenzelm@8449
   270
  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
wenzelm@7319
   271
  ;
wenzelm@7319
   272
\end{rail}
wenzelm@7319
   273
wenzelm@7319
   274
\begin{descr}
wenzelm@9602
   275
\item [$cases~insts~R$] applies method $rule$ with an appropriate case
wenzelm@9602
   276
  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
wenzelm@9602
   277
  names are bound according to the rule's local contexts.
wenzelm@8449
   278
  
wenzelm@8449
   279
  The rule is determined as follows, according to the facts and arguments
wenzelm@8449
   280
  passed to the $cases$ method:
wenzelm@8449
   281
  \begin{matharray}{llll}
wenzelm@9695
   282
    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
wenzelm@9695
   283
                    & cases &           & \Text{classical case split} \\
wenzelm@9695
   284
                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
wenzelm@9695
   285
    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
wenzelm@9695
   286
    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
wenzelm@8449
   287
  \end{matharray}
wenzelm@9602
   288
  
wenzelm@9602
   289
  Several instantiations may be given, referring to the \emph{suffix} of
wenzelm@9602
   290
  premises of the case rule; within each premise, the \emph{prefix} of
wenzelm@9602
   291
  variables is instantiated.  In most situations, only a single term needs to
wenzelm@9602
   292
  be specified; this refers to the first variable of the last premise (it is
wenzelm@9602
   293
  usually the same for all cases).
wenzelm@8449
   294
wenzelm@8449
   295
  The $simplified$ option causes ``obvious cases'' of the rule to be solved
wenzelm@8449
   296
  beforehand, while the others are left unscathed.
wenzelm@8449
   297
  
wenzelm@9616
   298
  The $open$ option causes the parameters of the new local contexts to be
wenzelm@9616
   299
  exposed to the current proof context.  Thus local variables stemming from
wenzelm@9616
   300
  distant parts of the theory development may be introduced in an implicit
wenzelm@9616
   301
  manner, which can be quite confusing to the reader.  Furthermore, this
wenzelm@9616
   302
  option may cause unwanted hiding of existing local variables, resulting in
wenzelm@9616
   303
  less robust proof texts.
wenzelm@9616
   304
wenzelm@8449
   305
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
wenzelm@8449
   306
  induction rules, which are determined as follows:
wenzelm@8449
   307
  \begin{matharray}{llll}
wenzelm@9695
   308
    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
wenzelm@9695
   309
                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
wenzelm@9695
   310
    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
wenzelm@9695
   311
    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
wenzelm@8449
   312
  \end{matharray}
wenzelm@8449
   313
  
wenzelm@8449
   314
  Several instantiations may be given, each referring to some part of a mutual
wenzelm@8449
   315
  inductive definition or datatype --- only related partial induction rules
wenzelm@8449
   316
  may be used together, though.  Any of the lists of terms $P, x, \dots$
wenzelm@8449
   317
  refers to the \emph{suffix} of variables present in the induction rule.
wenzelm@8449
   318
  This enables the writer to specify only induction variables, or both
wenzelm@8449
   319
  predicates and variables, for example.
wenzelm@7507
   320
  
wenzelm@8449
   321
  The $stripped$ option causes implications and (bounded) universal
wenzelm@8449
   322
  quantifiers to be removed from each new subgoal emerging from the
wenzelm@8547
   323
  application of the induction rule.  This accommodates typical
wenzelm@8547
   324
  ``strengthening of induction'' predicates.
wenzelm@9307
   325
  
wenzelm@9616
   326
  The $open$ option has the same effect as for the $cases$ method, see above.
wenzelm@7319
   327
\end{descr}
wenzelm@7141
   328
wenzelm@8484
   329
Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
wenzelm@8484
   330
determined by the instantiated rule \emph{before} it has been applied to the
wenzelm@8484
   331
internal proof state.\footnote{As a general principle, Isar proof text may
wenzelm@8449
   332
  never refer to parts of proof states directly.} Thus proper use of symbolic
wenzelm@8449
   333
cases usually require the rule to be instantiated fully, as far as the
wenzelm@8449
   334
emerging local contexts and subgoals are concerned.  In particular, for
wenzelm@8449
   335
induction both the predicates and variables have to be specified.  Otherwise
wenzelm@8547
   336
the $\CASENAME$ command would refuse to invoke cases containing schematic
wenzelm@8449
   337
variables.
wenzelm@8449
   338
wenzelm@9602
   339
The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
wenzelm@8547
   340
cases present in the current proof state.
wenzelm@8449
   341
wenzelm@8449
   342
wenzelm@8484
   343
\subsection{Declaring rules}
wenzelm@8449
   344
wenzelm@8449
   345
\indexisaratt{cases}\indexisaratt{induct}
wenzelm@8449
   346
\begin{matharray}{rcl}
wenzelm@8449
   347
  cases & : & \isaratt \\
wenzelm@8449
   348
  induct & : & \isaratt \\
wenzelm@8449
   349
\end{matharray}
wenzelm@8449
   350
wenzelm@8449
   351
\begin{rail}
wenzelm@8449
   352
  'cases' spec
wenzelm@8449
   353
  ;
wenzelm@8449
   354
  'induct' spec
wenzelm@8449
   355
  ;
wenzelm@8449
   356
wenzelm@8449
   357
  spec: ('type' | 'set') ':' nameref
wenzelm@8449
   358
  ;
wenzelm@8449
   359
\end{rail}
wenzelm@8449
   360
wenzelm@8449
   361
The $cases$ and $induct$ attributes augment the corresponding context of rules
wenzelm@8449
   362
for reasoning about inductive sets and types.  The standard rules are already
wenzelm@8449
   363
declared by HOL definitional packages.  For special applications, these may be
wenzelm@8449
   364
replaced manually by variant versions.
wenzelm@8449
   365
wenzelm@8484
   366
Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
wenzelm@8484
   367
adjust names of cases and parameters of a rule.
wenzelm@8484
   368
wenzelm@7046
   369
wenzelm@8665
   370
\subsection{Emulating tactic scripts}\label{sec:induct_tac}
wenzelm@8665
   371
wenzelm@8665
   372
\indexisarmeth{case-tac}\indexisarmeth{induct-tac}
wenzelm@9616
   373
\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
wenzelm@8665
   374
\begin{matharray}{rcl}
wenzelm@9616
   375
  case_tac^* & : & \isarmeth \\
wenzelm@9616
   376
  induct_tac^* & : & \isarmeth \\
wenzelm@9616
   377
  ind_cases^* & : & \isarmeth \\
wenzelm@9602
   378
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
wenzelm@8665
   379
\end{matharray}
wenzelm@8665
   380
wenzelm@8665
   381
\railalias{casetac}{case\_tac}
wenzelm@8665
   382
\railterm{casetac}
wenzelm@9602
   383
wenzelm@8665
   384
\railalias{inducttac}{induct\_tac}
wenzelm@8665
   385
\railterm{inducttac}
wenzelm@8665
   386
wenzelm@9616
   387
\railalias{indcases}{ind\_cases}
wenzelm@9616
   388
\railterm{indcases}
wenzelm@9602
   389
wenzelm@9616
   390
\railalias{inductivecases}{inductive\_cases}
wenzelm@9616
   391
\railterm{inductivecases}
wenzelm@9602
   392
wenzelm@8665
   393
\begin{rail}
wenzelm@8666
   394
  casetac goalspec? term rule?
wenzelm@8665
   395
  ;
wenzelm@8692
   396
  inducttac goalspec? (insts * 'and') rule?
wenzelm@8666
   397
  ;
wenzelm@9616
   398
  indcases (prop +)
wenzelm@9602
   399
  ;
wenzelm@9616
   400
  inductivecases thmdecl? (prop +) comment?
wenzelm@9602
   401
  ;
wenzelm@8666
   402
wenzelm@8666
   403
  rule: ('rule' ':' thmref)
wenzelm@8665
   404
  ;
wenzelm@8665
   405
\end{rail}
wenzelm@8665
   406
wenzelm@9602
   407
\begin{descr}
wenzelm@9602
   408
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
wenzelm@9602
   409
  only (unless an alternative rule is given explicitly).  Furthermore,
wenzelm@9602
   410
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
wenzelm@9602
   411
  variables to be given as instantiation.  These tactic emulations feature
wenzelm@9602
   412
  both goal addressing and dynamic instantiation.  Note that named local
wenzelm@9602
   413
  contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the
wenzelm@9602
   414
  proper $induct$ and $cases$ proof methods (see
wenzelm@9602
   415
  \S\ref{sec:induct-method-proper}).
wenzelm@9602
   416
  
wenzelm@9616
   417
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
wenzelm@9616
   418
  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
wenzelm@9616
   419
  forward manner, unlike the proper $cases$ method (see
wenzelm@9602
   420
  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
wenzelm@9602
   421
  solved completely.
wenzelm@9602
   422
  
wenzelm@9616
   423
  While $ind_cases$ is a proof method to apply the result immediately as
wenzelm@9602
   424
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
wenzelm@9602
   425
  theorems at the theory level for later use,
wenzelm@9602
   426
\end{descr}
wenzelm@8665
   427
wenzelm@8665
   428
wenzelm@7390
   429
\section{Arithmetic}
wenzelm@7390
   430
wenzelm@9642
   431
\indexisarmeth{arith}\indexisaratt{arith-split}
wenzelm@7390
   432
\begin{matharray}{rcl}
wenzelm@7390
   433
  arith & : & \isarmeth \\
wenzelm@9602
   434
  arith_split & : & \isaratt \\
wenzelm@7390
   435
\end{matharray}
wenzelm@7390
   436
wenzelm@8506
   437
\begin{rail}
wenzelm@8506
   438
  'arith' '!'?
wenzelm@8506
   439
  ;
wenzelm@8506
   440
\end{rail}
wenzelm@8506
   441
wenzelm@7390
   442
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
wenzelm@8506
   443
$real$).  Any current facts are inserted into the goal before running the
wenzelm@8506
   444
procedure.  The ``!''~argument causes the full context of assumptions to be
wenzelm@9602
   445
included.  The $arith_split$ attribute declares case split rules to be
wenzelm@9602
   446
expanded before the arithmetic procedure is invoked.
wenzelm@8506
   447
wenzelm@8506
   448
Note that a simpler (but faster) version of arithmetic reasoning is already
wenzelm@8506
   449
performed by the Simplifier.
wenzelm@7390
   450
wenzelm@7390
   451
wenzelm@7046
   452
%%% Local Variables: 
wenzelm@7046
   453
%%% mode: latex
wenzelm@7046
   454
%%% TeX-master: "isar-ref"
wenzelm@7046
   455
%%% End: