doc-src/IsarRef/hol.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9642 d8d1f70024bd
child 9751 1287787744a7
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
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@8945
   116
\texttt{case_tac} and \texttt{induct_tac} available, see
wenzelm@8665
   117
\S\ref{sec:induct_tac}.
wenzelm@7319
   118
wenzelm@7135
   119
wenzelm@7135
   120
\section{Recursive functions}
wenzelm@7135
   121
wenzelm@7141
   122
\indexisarcmd{primrec}\indexisarcmd{recdef}
wenzelm@7141
   123
\begin{matharray}{rcl}
wenzelm@7141
   124
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   125
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   126
%FIXME
wenzelm@7141
   127
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
wenzelm@7141
   128
\end{matharray}
wenzelm@7141
   129
wenzelm@7141
   130
\begin{rail}
wenzelm@8657
   131
  'primrec' parname? (equation + )
wenzelm@8657
   132
  ;
wenzelm@8657
   133
  'recdef' name term (equation +) hints
wenzelm@7141
   134
  ;
wenzelm@8657
   135
wenzelm@8657
   136
  equation: thmdecl? prop comment?
wenzelm@8657
   137
  ;
wenzelm@8710
   138
  hints: ('congs' thmrefs)?
wenzelm@7141
   139
  ;
wenzelm@7141
   140
\end{rail}
wenzelm@7141
   141
wenzelm@7167
   142
\begin{descr}
wenzelm@7319
   143
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
wenzelm@7319
   144
  datatypes.
wenzelm@7319
   145
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
wenzelm@7319
   146
  functions (using the TFL package).
wenzelm@7167
   147
\end{descr}
wenzelm@7141
   148
wenzelm@8449
   149
Both definitions accommodate reasoning proof by induction (cf.\ 
wenzelm@8449
   150
\S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
wenzelm@8449
   151
of the function definition) refers to a specific induction rule, with
wenzelm@8449
   152
parameters named according to the user-specified equations.  Case names of
wenzelm@8449
   153
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
wenzelm@8449
   154
$\isarkeyword{recdef}$ are numbered (starting from $1$).
wenzelm@8449
   155
wenzelm@8657
   156
The equations provided by these packages may be referred later as theorem list
wenzelm@8657
   157
$f\mathord.simps$, where $f$ is the (collective) name of the functions
wenzelm@8657
   158
defined.  Individual equations may be named explicitly as well; note that for
wenzelm@8657
   159
$\isarkeyword{recdef}$ each specification given by the user may result in
wenzelm@8657
   160
several theorems.
wenzelm@8657
   161
wenzelm@8449
   162
See \cite{isabelle-HOL} for further information on recursive function
wenzelm@8449
   163
definitions in HOL.
wenzelm@7319
   164
wenzelm@7141
   165
wenzelm@7135
   166
\section{(Co)Inductive sets}
wenzelm@7135
   167
wenzelm@9602
   168
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
wenzelm@7141
   169
\begin{matharray}{rcl}
wenzelm@7141
   170
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
wenzelm@9602
   171
  \isarcmd{coinductive}^* & : & \isartrans{theory}{theory} \\
wenzelm@7990
   172
  mono & : & \isaratt \\
wenzelm@7141
   173
\end{matharray}
wenzelm@7141
   174
wenzelm@7141
   175
\railalias{condefs}{con\_defs}
wenzelm@9602
   176
\railterm{condefs}
wenzelm@7141
   177
wenzelm@7141
   178
\begin{rail}
wenzelm@7141
   179
  ('inductive' | 'coinductive') (term comment? +) \\
wenzelm@9602
   180
    'intros' attributes? (thmdecl? prop comment? +) \\
wenzelm@7141
   181
    'monos' thmrefs comment? \\ condefs thmrefs comment?
wenzelm@7141
   182
  ;
wenzelm@7990
   183
  'mono' (() | 'add' | 'del')
wenzelm@7990
   184
  ;
wenzelm@7141
   185
\end{rail}
wenzelm@7141
   186
wenzelm@7167
   187
\begin{descr}
wenzelm@7319
   188
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
wenzelm@7319
   189
  (co)inductive sets from the given introduction rules.
wenzelm@8547
   190
\item [$mono$] declares monotonicity rules.  These rule are involved in the
wenzelm@8547
   191
  automated monotonicity proof of $\isarkeyword{inductive}$.
wenzelm@7167
   192
\end{descr}
wenzelm@7141
   193
wenzelm@8449
   194
See \cite{isabelle-HOL} for further information on inductive definitions in
wenzelm@8449
   195
HOL.
wenzelm@7319
   196
wenzelm@7141
   197
wenzelm@8449
   198
\section{Proof by cases and induction}\label{sec:induct-method}
wenzelm@8449
   199
wenzelm@8666
   200
\subsection{Proof methods}\label{sec:induct-method-proper}
wenzelm@7141
   201
wenzelm@8449
   202
\indexisarmeth{cases}\indexisarmeth{induct}
wenzelm@7319
   203
\begin{matharray}{rcl}
wenzelm@8449
   204
  cases & : & \isarmeth \\
wenzelm@7319
   205
  induct & : & \isarmeth \\
wenzelm@7319
   206
\end{matharray}
wenzelm@7319
   207
wenzelm@8449
   208
The $cases$ and $induct$ methods provide a uniform interface to case analysis
wenzelm@8449
   209
and induction over datatypes, inductive sets, and recursive functions.  The
wenzelm@8449
   210
corresponding rules may be specified and instantiated in a casual manner.
wenzelm@8449
   211
Furthermore, these methods provide named local contexts that may be invoked
wenzelm@8449
   212
via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
wenzelm@8484
   213
\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
wenzelm@8484
   214
about large specifications.
wenzelm@7319
   215
wenzelm@7319
   216
\begin{rail}
wenzelm@9616
   217
  'cases' ('(simplified)')? ('(open)')? \\ (insts * 'and') rule?  ;
wenzelm@8449
   218
wenzelm@9616
   219
  'induct' ('(stripped)')? ('(open)')? \\ (insts * 'and') rule?
wenzelm@7319
   220
  ;
wenzelm@7319
   221
wenzelm@8449
   222
  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
wenzelm@7319
   223
  ;
wenzelm@7319
   224
\end{rail}
wenzelm@7319
   225
wenzelm@7319
   226
\begin{descr}
wenzelm@9602
   227
\item [$cases~insts~R$] applies method $rule$ with an appropriate case
wenzelm@9602
   228
  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
wenzelm@9602
   229
  names are bound according to the rule's local contexts.
wenzelm@8449
   230
  
wenzelm@8449
   231
  The rule is determined as follows, according to the facts and arguments
wenzelm@8449
   232
  passed to the $cases$ method:
wenzelm@8449
   233
  \begin{matharray}{llll}
wenzelm@9695
   234
    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
wenzelm@9695
   235
                    & cases &           & \Text{classical case split} \\
wenzelm@9695
   236
                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
wenzelm@9695
   237
    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
wenzelm@9695
   238
    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
wenzelm@8449
   239
  \end{matharray}
wenzelm@9602
   240
  
wenzelm@9602
   241
  Several instantiations may be given, referring to the \emph{suffix} of
wenzelm@9602
   242
  premises of the case rule; within each premise, the \emph{prefix} of
wenzelm@9602
   243
  variables is instantiated.  In most situations, only a single term needs to
wenzelm@9602
   244
  be specified; this refers to the first variable of the last premise (it is
wenzelm@9602
   245
  usually the same for all cases).
wenzelm@8449
   246
wenzelm@8449
   247
  The $simplified$ option causes ``obvious cases'' of the rule to be solved
wenzelm@8449
   248
  beforehand, while the others are left unscathed.
wenzelm@8449
   249
  
wenzelm@9616
   250
  The $open$ option causes the parameters of the new local contexts to be
wenzelm@9616
   251
  exposed to the current proof context.  Thus local variables stemming from
wenzelm@9616
   252
  distant parts of the theory development may be introduced in an implicit
wenzelm@9616
   253
  manner, which can be quite confusing to the reader.  Furthermore, this
wenzelm@9616
   254
  option may cause unwanted hiding of existing local variables, resulting in
wenzelm@9616
   255
  less robust proof texts.
wenzelm@9616
   256
wenzelm@8449
   257
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
wenzelm@8449
   258
  induction rules, which are determined as follows:
wenzelm@8449
   259
  \begin{matharray}{llll}
wenzelm@9695
   260
    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
wenzelm@9695
   261
                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
wenzelm@9695
   262
    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
wenzelm@9695
   263
    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
wenzelm@8449
   264
  \end{matharray}
wenzelm@8449
   265
  
wenzelm@8449
   266
  Several instantiations may be given, each referring to some part of a mutual
wenzelm@8449
   267
  inductive definition or datatype --- only related partial induction rules
wenzelm@8449
   268
  may be used together, though.  Any of the lists of terms $P, x, \dots$
wenzelm@8449
   269
  refers to the \emph{suffix} of variables present in the induction rule.
wenzelm@8449
   270
  This enables the writer to specify only induction variables, or both
wenzelm@8449
   271
  predicates and variables, for example.
wenzelm@7507
   272
  
wenzelm@8449
   273
  The $stripped$ option causes implications and (bounded) universal
wenzelm@8449
   274
  quantifiers to be removed from each new subgoal emerging from the
wenzelm@8547
   275
  application of the induction rule.  This accommodates typical
wenzelm@8547
   276
  ``strengthening of induction'' predicates.
wenzelm@9307
   277
  
wenzelm@9616
   278
  The $open$ option has the same effect as for the $cases$ method, see above.
wenzelm@7319
   279
\end{descr}
wenzelm@7141
   280
wenzelm@8484
   281
Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
wenzelm@8484
   282
determined by the instantiated rule \emph{before} it has been applied to the
wenzelm@8484
   283
internal proof state.\footnote{As a general principle, Isar proof text may
wenzelm@8449
   284
  never refer to parts of proof states directly.} Thus proper use of symbolic
wenzelm@8449
   285
cases usually require the rule to be instantiated fully, as far as the
wenzelm@8449
   286
emerging local contexts and subgoals are concerned.  In particular, for
wenzelm@8449
   287
induction both the predicates and variables have to be specified.  Otherwise
wenzelm@8547
   288
the $\CASENAME$ command would refuse to invoke cases containing schematic
wenzelm@8449
   289
variables.
wenzelm@8449
   290
wenzelm@9602
   291
The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
wenzelm@8547
   292
cases present in the current proof state.
wenzelm@8449
   293
wenzelm@8449
   294
wenzelm@8484
   295
\subsection{Declaring rules}
wenzelm@8449
   296
wenzelm@8449
   297
\indexisaratt{cases}\indexisaratt{induct}
wenzelm@8449
   298
\begin{matharray}{rcl}
wenzelm@8449
   299
  cases & : & \isaratt \\
wenzelm@8449
   300
  induct & : & \isaratt \\
wenzelm@8449
   301
\end{matharray}
wenzelm@8449
   302
wenzelm@8449
   303
\begin{rail}
wenzelm@8449
   304
  'cases' spec
wenzelm@8449
   305
  ;
wenzelm@8449
   306
  'induct' spec
wenzelm@8449
   307
  ;
wenzelm@8449
   308
wenzelm@8449
   309
  spec: ('type' | 'set') ':' nameref
wenzelm@8449
   310
  ;
wenzelm@8449
   311
\end{rail}
wenzelm@8449
   312
wenzelm@8449
   313
The $cases$ and $induct$ attributes augment the corresponding context of rules
wenzelm@8449
   314
for reasoning about inductive sets and types.  The standard rules are already
wenzelm@8449
   315
declared by HOL definitional packages.  For special applications, these may be
wenzelm@8449
   316
replaced manually by variant versions.
wenzelm@8449
   317
wenzelm@8484
   318
Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
wenzelm@8484
   319
adjust names of cases and parameters of a rule.
wenzelm@8484
   320
wenzelm@7046
   321
wenzelm@8665
   322
\subsection{Emulating tactic scripts}\label{sec:induct_tac}
wenzelm@8665
   323
wenzelm@8665
   324
\indexisarmeth{case-tac}\indexisarmeth{induct-tac}
wenzelm@9616
   325
\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
wenzelm@8665
   326
\begin{matharray}{rcl}
wenzelm@9616
   327
  case_tac^* & : & \isarmeth \\
wenzelm@9616
   328
  induct_tac^* & : & \isarmeth \\
wenzelm@9616
   329
  ind_cases^* & : & \isarmeth \\
wenzelm@9602
   330
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
wenzelm@8665
   331
\end{matharray}
wenzelm@8665
   332
wenzelm@8665
   333
\railalias{casetac}{case\_tac}
wenzelm@8665
   334
\railterm{casetac}
wenzelm@9602
   335
wenzelm@8665
   336
\railalias{inducttac}{induct\_tac}
wenzelm@8665
   337
\railterm{inducttac}
wenzelm@8665
   338
wenzelm@9616
   339
\railalias{indcases}{ind\_cases}
wenzelm@9616
   340
\railterm{indcases}
wenzelm@9602
   341
wenzelm@9616
   342
\railalias{inductivecases}{inductive\_cases}
wenzelm@9616
   343
\railterm{inductivecases}
wenzelm@9602
   344
wenzelm@8665
   345
\begin{rail}
wenzelm@8666
   346
  casetac goalspec? term rule?
wenzelm@8665
   347
  ;
wenzelm@8692
   348
  inducttac goalspec? (insts * 'and') rule?
wenzelm@8666
   349
  ;
wenzelm@9616
   350
  indcases (prop +)
wenzelm@9602
   351
  ;
wenzelm@9616
   352
  inductivecases thmdecl? (prop +) comment?
wenzelm@9602
   353
  ;
wenzelm@8666
   354
wenzelm@8666
   355
  rule: ('rule' ':' thmref)
wenzelm@8665
   356
  ;
wenzelm@8665
   357
\end{rail}
wenzelm@8665
   358
wenzelm@9602
   359
\begin{descr}
wenzelm@9602
   360
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
wenzelm@9602
   361
  only (unless an alternative rule is given explicitly).  Furthermore,
wenzelm@9602
   362
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
wenzelm@9602
   363
  variables to be given as instantiation.  These tactic emulations feature
wenzelm@9602
   364
  both goal addressing and dynamic instantiation.  Note that named local
wenzelm@9602
   365
  contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the
wenzelm@9602
   366
  proper $induct$ and $cases$ proof methods (see
wenzelm@9602
   367
  \S\ref{sec:induct-method-proper}).
wenzelm@9602
   368
  
wenzelm@9616
   369
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
wenzelm@9616
   370
  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
wenzelm@9616
   371
  forward manner, unlike the proper $cases$ method (see
wenzelm@9602
   372
  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
wenzelm@9602
   373
  solved completely.
wenzelm@9602
   374
  
wenzelm@9616
   375
  While $ind_cases$ is a proof method to apply the result immediately as
wenzelm@9602
   376
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
wenzelm@9602
   377
  theorems at the theory level for later use,
wenzelm@9602
   378
\end{descr}
wenzelm@8665
   379
wenzelm@8665
   380
wenzelm@7390
   381
\section{Arithmetic}
wenzelm@7390
   382
wenzelm@9642
   383
\indexisarmeth{arith}\indexisaratt{arith-split}
wenzelm@7390
   384
\begin{matharray}{rcl}
wenzelm@7390
   385
  arith & : & \isarmeth \\
wenzelm@9602
   386
  arith_split & : & \isaratt \\
wenzelm@7390
   387
\end{matharray}
wenzelm@7390
   388
wenzelm@8506
   389
\begin{rail}
wenzelm@8506
   390
  'arith' '!'?
wenzelm@8506
   391
  ;
wenzelm@8506
   392
\end{rail}
wenzelm@8506
   393
wenzelm@7390
   394
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
wenzelm@8506
   395
$real$).  Any current facts are inserted into the goal before running the
wenzelm@8506
   396
procedure.  The ``!''~argument causes the full context of assumptions to be
wenzelm@9602
   397
included.  The $arith_split$ attribute declares case split rules to be
wenzelm@9602
   398
expanded before the arithmetic procedure is invoked.
wenzelm@8506
   399
wenzelm@8506
   400
Note that a simpler (but faster) version of arithmetic reasoning is already
wenzelm@8506
   401
performed by the Simplifier.
wenzelm@7390
   402
wenzelm@7390
   403
wenzelm@7046
   404
%%% Local Variables: 
wenzelm@7046
   405
%%% mode: latex
wenzelm@7046
   406
%%% TeX-master: "isar-ref"
wenzelm@7046
   407
%%% End: