author | wenzelm |
Fri, 10 Nov 2000 19:02:37 +0100 | |
changeset 10432 | 3dfbc913d184 |
parent 10240 | 9ac0fe356ea7 |
child 10456 | 166fc12ce153 |
permissions | -rw-r--r-- |
7046 | 1 |
|
7167 | 2 |
\chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools} |
7135 | 3 |
|
10240 | 4 |
\section{Miscellaneous attributes}\label{sec:rule-format} |
7990 | 5 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset
|
6 |
\indexisaratt{rule-format} |
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 object-rule |
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 meta-logical 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:types-pure}), 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 |
non-emptiness of the set $A$. After finishing the proof, the theory will be |
|
7175 | 51 |
augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} |
7335 | 52 |
for more information. Note that user-level 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{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only |
79 |
simply-typed extensible records. |
|
7167 | 80 |
\end{descr} |
7141 | 81 |
|
82 |
||
83 |
\section{Datatypes}\label{sec:datatype} |
|
84 |
||
7167 | 85 |
\indexisarcmd{datatype}\indexisarcmd{rep-datatype} |
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:induct-method}). |
|
117 |
||
7319 | 118 |
See \cite{isabelle-HOL} 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 case-analysis 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{isabelle-HOL}. |
7319 | 164 |
\item [$\isarkeyword{recdef}$] defines general well-founded recursive |
9848 | 165 |
functions (using the TFL package), see also \cite{isabelle-HOL}. 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:induct-method}): 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 user-specified 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{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf} |
|
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{isabelle-HOL} for further information on inductive definitions in |
245 |
HOL. |
|
7319 | 246 |
|
7141 | 247 |
|
8449 | 248 |
\section{Proof by cases and induction}\label{sec:induct-method} |
249 |
||
8666 | 250 |
\subsection{Proof methods}\label{sec:induct-method-proper} |
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{case-tac}\indexisarmeth{induct-tac} |
|
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
383 |
\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases} |
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:induct-method-proper}). |
|
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:induct-method-proper}) 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{arith-split} |
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 |
%%% TeX-master: "isar-ref" |
|
465 |
%%% End: |