author  wenzelm 
Fri, 10 Nov 2000 19:02:37 +0100  
changeset 10432  3dfbc913d184 
parent 10240  9ac0fe356ea7 
child 10456  166fc12ce153 
permissions  rwrr 
7046  1 

7167  2 
\chapter{Isabelle/HOL Tools and Packages}\label{ch:holtools} 
7135  3 

10240  4 
\section{Miscellaneous attributes}\label{sec:ruleformat} 
7990  5 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

6 
\indexisaratt{ruleformat} 
7990  7 
\begin{matharray}{rcl} 
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

8 
rule_format & : & \isaratt \\ 
7990  9 
\end{matharray} 
10 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

11 
\railalias{ruleformat}{rule\_format} 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

12 
\railterm{ruleformat} 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

13 

9905  14 
\begin{rail} 
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

15 
ruleformat ('(' noasm ')')? 
9905  16 
; 
17 
\end{rail} 

18 

7990  19 
\begin{descr} 
9848  20 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

21 
\item [$rule_format$] causes a theorem to be put into standard objectrule 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

22 
form, replacing implication and (bounded) universal quantification of HOL by 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset

23 
the corresponding metalogical connectives. By default, the result is fully 
9905  24 
normalized, including assumptions and conclusions at any depth. The 
25 
$no_asm$ option restricts the transformation to the conclusion of a rule. 

7990  26 
\end{descr} 
27 

28 

7135  29 
\section{Primitive types} 
30 

7141  31 
\indexisarcmd{typedecl}\indexisarcmd{typedef} 
32 
\begin{matharray}{rcl} 

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

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

35 
\end{matharray} 

36 

37 
\begin{rail} 

38 
'typedecl' typespec infix? comment? 

39 
; 

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

41 
; 

42 
\end{rail} 

43 

7167  44 
\begin{descr} 
7141  45 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original 
46 
$\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:typespure}), but 

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

48 
actual HOL type constructor. 

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

50 
nonemptiness of the set $A$. After finishing the proof, the theory will be 

7175  51 
augmented by a Gordon/HOLstyle type definition. See \cite{isabelleHOL} 
7335  52 
for more information. Note that userlevel theories usually do not directly 
53 
refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced 

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

7175  55 
$\isarkeyword{datatype}$ (see \S\ref{sec:datatype}). 
7167  56 
\end{descr} 
7141  57 

58 

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

60 

61 
\indexisarcmd{record} 

62 
\begin{matharray}{rcl} 

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

64 
\end{matharray} 

65 

66 
\begin{rail} 

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

68 
; 

7135  69 

7141  70 
field: name '::' type comment? 
71 
; 

72 
\end{rail} 

73 

7167  74 
\begin{descr} 
7141  75 
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] 
76 
defines extensible record type $(\vec\alpha)t$, derived from the optional 

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

7335  78 
See \cite{isabelleHOL,NaraschewskiWTPHOLs98} for more information only 
79 
simplytyped extensible records. 

7167  80 
\end{descr} 
7141  81 

82 

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

84 

7167  85 
\indexisarcmd{datatype}\indexisarcmd{repdatatype} 
7141  86 
\begin{matharray}{rcl} 
87 
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\ 

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

89 
\end{matharray} 

90 

91 
\railalias{repdatatype}{rep\_datatype} 

92 
\railterm{repdatatype} 

93 

94 
\begin{rail} 

9848  95 
'datatype' (dtspec + 'and') 
7141  96 
; 
9848  97 
repdatatype (name * ) dtrules 
7141  98 
; 
99 

9848  100 
dtspec: parname? typespec infix? '=' (cons + '') 
7141  101 
; 
9848  102 
cons: name (type * ) mixfix? comment? 
103 
; 

104 
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs 

7141  105 
\end{rail} 
106 

7167  107 
\begin{descr} 
7319  108 
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. 
109 
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive 

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

111 
recursion etc.). 

7167  112 
\end{descr} 
7141  113 

8449  114 
The induction and exhaustion theorems generated provide case names according 
115 
to the constructors involved, while parameters are named after the types (see 

116 
also \S\ref{sec:inductmethod}). 

117 

7319  118 
See \cite{isabelleHOL} for more details on datatypes. Note that the theory 
7335  119 
syntax above has been slightly simplified over the old version, usually 
8531  120 
requiring more quotes and less parentheses. Apart from proper proof methods 
121 
for caseanalysis and induction, there are also emulations of ML tactics 

8945  122 
\texttt{case_tac} and \texttt{induct_tac} available, see 
8665  123 
\S\ref{sec:induct_tac}. 
7319  124 

7135  125 

126 
\section{Recursive functions} 

127 

7141  128 
\indexisarcmd{primrec}\indexisarcmd{recdef} 
129 
\begin{matharray}{rcl} 

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

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

132 
%FIXME 

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

134 
\end{matharray} 

135 

9949  136 
\railalias{recdefsimp}{recdef\_simp} 
137 
\railterm{recdefsimp} 

138 

139 
\railalias{recdefcong}{recdef\_cong} 

140 
\railterm{recdefcong} 

141 

142 
\railalias{recdefwf}{recdef\_wf} 

143 
\railterm{recdefwf} 

144 

7141  145 
\begin{rail} 
8657  146 
'primrec' parname? (equation + ) 
147 
; 

9848  148 
'recdef' name term (eqn + ) hints? 
149 
; 

8657  150 

9848  151 
equation: thmdecl? eqn 
152 
; 

153 
eqn: prop comment? 

8657  154 
; 
9848  155 
hints: '(' 'hints' (recdefmod * ) ')' 
156 
; 

9949  157 
recdefmod: ((recdefsimp  recdefcong  recdefwf) (()  'add'  'del') ':' thmrefs)  clasimpmod 
7141  158 
; 
159 
\end{rail} 

160 

7167  161 
\begin{descr} 
7319  162 
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over 
9848  163 
datatypes, see also \cite{isabelleHOL}. 
7319  164 
\item [$\isarkeyword{recdef}$] defines general wellfounded recursive 
9848  165 
functions (using the TFL package), see also \cite{isabelleHOL}. The 
9949  166 
$recdef_simp$, $recdef_cong$, and $recdef_wf$ hints refer to auxiliary rules 
167 
to be used in the internal automated proof process of TFL. Additional 

168 
$clasimpmod$ declarations (cf.\ \S\ref{sec:clasimp}) may be given to tune 

169 
the context of the Simplifier (cf.\ \S\ref{sec:simplifier}) and Classical 

170 
reasoner (cf.\ \S\ref{sec:classical}). 

7167  171 
\end{descr} 
7141  172 

9848  173 
Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
8449  174 
\S\ref{sec:inductmethod}): rule $c\mathord{.}induct$ (where $c$ is the name 
175 
of the function definition) refers to a specific induction rule, with 

176 
parameters named according to the userspecified equations. Case names of 

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

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

179 

8657  180 
The equations provided by these packages may be referred later as theorem list 
181 
$f\mathord.simps$, where $f$ is the (collective) name of the functions 

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

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

184 
several theorems. 

185 

9935  186 
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using 
187 
the following attributes. 

188 

189 
\indexisaratt{recdefsimp}\indexisaratt{recdefcong}\indexisaratt{recdefwf} 

190 
\begin{matharray}{rcl} 

191 
recdef_simp & : & \isaratt \\ 

192 
recdef_cong & : & \isaratt \\ 

193 
recdef_wf & : & \isaratt \\ 

194 
\end{matharray} 

195 

196 
\railalias{recdefsimp}{recdef\_simp} 

197 
\railterm{recdefsimp} 

198 

199 
\railalias{recdefcong}{recdef\_cong} 

200 
\railterm{recdefcong} 

201 

202 
\railalias{recdefwf}{recdef\_wf} 

203 
\railterm{recdefwf} 

204 

205 
\begin{rail} 

206 
(recdefsimp  recdefcong  recdefwf) (()  'add'  'del') 

207 
; 

208 
\end{rail} 

209 

7141  210 

7135  211 
\section{(Co)Inductive sets} 
212 

9602  213 
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono} 
7141  214 
\begin{matharray}{rcl} 
215 
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\ 

9848  216 
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ 
7990  217 
mono & : & \isaratt \\ 
7141  218 
\end{matharray} 
219 

220 
\railalias{condefs}{con\_defs} 

9602  221 
\railterm{condefs} 
7141  222 

223 
\begin{rail} 

9848  224 
('inductive'  'coinductive') sets intros monos? 
7141  225 
; 
7990  226 
'mono' (()  'add'  'del') 
227 
; 

9848  228 

229 
sets: (term comment? +) 

230 
; 

231 
intros: 'intros' attributes? (thmdecl? prop comment? +) 

232 
; 

233 
monos: 'monos' thmrefs comment? 

234 
; 

7141  235 
\end{rail} 
236 

7167  237 
\begin{descr} 
7319  238 
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define 
239 
(co)inductive sets from the given introduction rules. 

8547  240 
\item [$mono$] declares monotonicity rules. These rule are involved in the 
241 
automated monotonicity proof of $\isarkeyword{inductive}$. 

7167  242 
\end{descr} 
7141  243 

8449  244 
See \cite{isabelleHOL} for further information on inductive definitions in 
245 
HOL. 

7319  246 

7141  247 

8449  248 
\section{Proof by cases and induction}\label{sec:inductmethod} 
249 

8666  250 
\subsection{Proof methods}\label{sec:inductmethodproper} 
7141  251 

8449  252 
\indexisarmeth{cases}\indexisarmeth{induct} 
7319  253 
\begin{matharray}{rcl} 
8449  254 
cases & : & \isarmeth \\ 
7319  255 
induct & : & \isarmeth \\ 
256 
\end{matharray} 

257 

8449  258 
The $cases$ and $induct$ methods provide a uniform interface to case analysis 
259 
and induction over datatypes, inductive sets, and recursive functions. The 

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

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

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

8484  263 
\S\ref{sec:cases}). This accommodates compact proof texts even when reasoning 
264 
about large specifications. 

7319  265 

266 
\begin{rail} 

9848  267 
'cases' simplified? open? args rule? 
268 
; 

269 
'induct' stripped? open? args rule? 

7319  270 
; 
271 

9848  272 
simplified: '(' 'simplified' ')' 
273 
; 

274 
stripped: '(' 'stripped' ')' 

275 
; 

276 
open: '(' 'open' ')' 

277 
; 

278 
args: (insts * 'and') 

279 
; 

8449  280 
rule: ('type'  'set') ':' nameref  'rule' ':' thmref 
7319  281 
; 
282 
\end{rail} 

283 

284 
\begin{descr} 

9602  285 
\item [$cases~insts~R$] applies method $rule$ with an appropriate case 
286 
distinction theorem, instantiated to the subjects $insts$. Symbolic case 

287 
names are bound according to the rule's local contexts. 

8449  288 

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

290 
passed to the $cases$ method: 

291 
\begin{matharray}{llll} 

9695  292 
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline 
293 
& cases & & \Text{classical case split} \\ 

294 
& cases & t & \Text{datatype exhaustion (type of $t$)} \\ 

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

296 
\dots & cases & \dots ~ R & \Text{explicit rule $R$} \\ 

8449  297 
\end{matharray} 
9602  298 

299 
Several instantiations may be given, referring to the \emph{suffix} of 

300 
premises of the case rule; within each premise, the \emph{prefix} of 

301 
variables is instantiated. In most situations, only a single term needs to 

302 
be specified; this refers to the first variable of the last premise (it is 

303 
usually the same for all cases). 

8449  304 

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

306 
beforehand, while the others are left unscathed. 

307 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

308 
The $open$ option causes the parameters of the new local contexts to be 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

309 
exposed to the current proof context. Thus local variables stemming from 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

310 
distant parts of the theory development may be introduced in an implicit 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

311 
manner, which can be quite confusing to the reader. Furthermore, this 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

312 
option may cause unwanted hiding of existing local variables, resulting in 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

313 
less robust proof texts. 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

314 

8449  315 
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to 
316 
induction rules, which are determined as follows: 

317 
\begin{matharray}{llll} 

9695  318 
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline 
319 
& induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\ 

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

321 
\dots & induct & \dots ~ R & \Text{explicit rule $R$} \\ 

8449  322 
\end{matharray} 
323 

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

325 
inductive definition or datatype  only related partial induction rules 

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

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

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

329 
predicates and variables, for example. 

7507  330 

8449  331 
The $stripped$ option causes implications and (bounded) universal 
332 
quantifiers to be removed from each new subgoal emerging from the 

8547  333 
application of the induction rule. This accommodates typical 
334 
``strengthening of induction'' predicates. 

9307  335 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

336 
The $open$ option has the same effect as for the $cases$ method, see above. 
7319  337 
\end{descr} 
7141  338 

8484  339 
Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as 
340 
determined by the instantiated rule \emph{before} it has been applied to the 

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

8449  342 
never refer to parts of proof states directly.} Thus proper use of symbolic 
343 
cases usually require the rule to be instantiated fully, as far as the 

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

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

8547  346 
the $\CASENAME$ command would refuse to invoke cases containing schematic 
8449  347 
variables. 
348 

9602  349 
The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named 
8547  350 
cases present in the current proof state. 
8449  351 

352 

8484  353 
\subsection{Declaring rules} 
8449  354 

355 
\indexisaratt{cases}\indexisaratt{induct} 

356 
\begin{matharray}{rcl} 

357 
cases & : & \isaratt \\ 

358 
induct & : & \isaratt \\ 

359 
\end{matharray} 

360 

361 
\begin{rail} 

362 
'cases' spec 

363 
; 

364 
'induct' spec 

365 
; 

366 

367 
spec: ('type'  'set') ':' nameref 

368 
; 

369 
\end{rail} 

370 

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

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

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

374 
replaced manually by variant versions. 

375 

8484  376 
Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to 
377 
adjust names of cases and parameters of a rule. 

378 

7046  379 

8665  380 
\subsection{Emulating tactic scripts}\label{sec:induct_tac} 
381 

382 
\indexisarmeth{casetac}\indexisarmeth{inducttac} 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

383 
\indexisarmeth{indcases}\indexisarcmd{inductivecases} 
8665  384 
\begin{matharray}{rcl} 
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

385 
case_tac^* & : & \isarmeth \\ 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

386 
induct_tac^* & : & \isarmeth \\ 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

387 
ind_cases^* & : & \isarmeth \\ 
9602  388 
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ 
8665  389 
\end{matharray} 
390 

391 
\railalias{casetac}{case\_tac} 

392 
\railterm{casetac} 

9602  393 

8665  394 
\railalias{inducttac}{induct\_tac} 
395 
\railterm{inducttac} 

396 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

397 
\railalias{indcases}{ind\_cases} 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

398 
\railterm{indcases} 
9602  399 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

400 
\railalias{inductivecases}{inductive\_cases} 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

401 
\railterm{inductivecases} 
9602  402 

8665  403 
\begin{rail} 
8666  404 
casetac goalspec? term rule? 
8665  405 
; 
8692  406 
inducttac goalspec? (insts * 'and') rule? 
8666  407 
; 
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

408 
indcases (prop +) 
9602  409 
; 
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

410 
inductivecases thmdecl? (prop +) comment? 
9602  411 
; 
8666  412 

413 
rule: ('rule' ':' thmref) 

8665  414 
; 
415 
\end{rail} 

416 

9602  417 
\begin{descr} 
418 
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes 

419 
only (unless an alternative rule is given explicitly). Furthermore, 

420 
$case_tac$ does a classical case split on booleans; $induct_tac$ allows only 

421 
variables to be given as instantiation. These tactic emulations feature 

422 
both goal addressing and dynamic instantiation. Note that named local 

423 
contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the 

424 
proper $induct$ and $cases$ proof methods (see 

425 
\S\ref{sec:inductmethodproper}). 

426 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

427 
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

428 
to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted 
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

429 
forward manner, unlike the proper $cases$ method (see 
9602  430 
\S\ref{sec:inductmethodproper}) which requires simplified cases to be 
431 
solved completely. 

432 

9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset

433 
While $ind_cases$ is a proof method to apply the result immediately as 
9602  434 
elimination rules, $\isarkeyword{inductive_cases}$ provides case split 
435 
theorems at the theory level for later use, 

436 
\end{descr} 

8665  437 

438 

7390  439 
\section{Arithmetic} 
440 

9642  441 
\indexisarmeth{arith}\indexisaratt{arithsplit} 
7390  442 
\begin{matharray}{rcl} 
443 
arith & : & \isarmeth \\ 

9602  444 
arith_split & : & \isaratt \\ 
7390  445 
\end{matharray} 
446 

8506  447 
\begin{rail} 
448 
'arith' '!'? 

449 
; 

450 
\end{rail} 

451 

7390  452 
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, 
8506  453 
$real$). Any current facts are inserted into the goal before running the 
454 
procedure. The ``!''~argument causes the full context of assumptions to be 

9602  455 
included. The $arith_split$ attribute declares case split rules to be 
456 
expanded before the arithmetic procedure is invoked. 

8506  457 

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

459 
performed by the Simplifier. 

7390  460 

461 

7046  462 
%%% Local Variables: 
463 
%%% mode: latex 

464 
%%% TeXmaster: "isarref" 

465 
%%% End: 