author | wenzelm |
Thu, 04 Oct 2001 16:09:12 +0200 | |
changeset 11691 | fc9bd420162c |
parent 11662 | 744399c9dd6a |
child 12618 | 43a97a2155d0 |
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 |
|
11039 | 6 |
\indexisaratt{rule-format}\indexisaratt{split-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 \\ |
11051 | 9 |
split_format^* & : & \isaratt \\ |
7990 | 10 |
\end{matharray} |
11 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset
|
12 |
\railalias{ruleformat}{rule\_format} |
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset
|
13 |
\railterm{ruleformat} |
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset
|
14 |
|
11039 | 15 |
\railalias{splitformat}{split\_format} |
16 |
\railterm{splitformat} |
|
17 |
\railterm{complete} |
|
18 |
||
9905 | 19 |
\begin{rail} |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset
|
20 |
ruleformat ('(' noasm ')')? |
9905 | 21 |
; |
11039 | 22 |
splitformat (((name * ) + 'and') | ('(' complete ')')) |
23 |
; |
|
9905 | 24 |
\end{rail} |
25 |
||
7990 | 26 |
\begin{descr} |
9848 | 27 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9935
diff
changeset
|
28 |
\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
|
29 |
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
|
30 |
the corresponding meta-logical connectives. By default, the result is fully |
9905 | 31 |
normalized, including assumptions and conclusions at any depth. The |
32 |
$no_asm$ option restricts the transformation to the conclusion of a rule. |
|
11039 | 33 |
|
34 |
\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into |
|
35 |
canonical form as specified by the arguments given; $\vec p@i$ refers to |
|
11051 | 36 |
occurrences in premise $i$ of the rule. The $split_format~(complete)$ form |
37 |
causes \emph{all} arguments in function applications to be represented |
|
38 |
canonically according to their tuple type structure. |
|
11039 | 39 |
|
11051 | 40 |
Note that these operations tend to invent funny names for new local |
41 |
parameters to be introduced. |
|
11039 | 42 |
|
7990 | 43 |
\end{descr} |
44 |
||
45 |
||
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
46 |
\section{Primitive types}\label{sec:typedef} |
7135 | 47 |
|
7141 | 48 |
\indexisarcmd{typedecl}\indexisarcmd{typedef} |
49 |
\begin{matharray}{rcl} |
|
50 |
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
|
51 |
\isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ |
|
52 |
\end{matharray} |
|
53 |
||
54 |
\begin{rail} |
|
55 |
'typedecl' typespec infix? comment? |
|
56 |
; |
|
57 |
'typedef' parname? typespec infix? \\ '=' term comment? |
|
58 |
; |
|
59 |
\end{rail} |
|
60 |
||
7167 | 61 |
\begin{descr} |
7141 | 62 |
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original |
63 |
$\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but |
|
64 |
also declares type arity $t :: (term, \dots, term) term$, making $t$ an |
|
65 |
actual HOL type constructor. |
|
66 |
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating |
|
67 |
non-emptiness of the set $A$. After finishing the proof, the theory will be |
|
7175 | 68 |
augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} |
7335 | 69 |
for more information. Note that user-level theories usually do not directly |
70 |
refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced |
|
71 |
packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and |
|
7175 | 72 |
$\isarkeyword{datatype}$ (see \S\ref{sec:datatype}). |
7167 | 73 |
\end{descr} |
7141 | 74 |
|
75 |
||
76 |
\section{Records}\label{sec:record} |
|
77 |
||
78 |
\indexisarcmd{record} |
|
79 |
\begin{matharray}{rcl} |
|
80 |
\isarcmd{record} & : & \isartrans{theory}{theory} \\ |
|
81 |
\end{matharray} |
|
82 |
||
83 |
\begin{rail} |
|
84 |
'record' typespec '=' (type '+')? (field +) |
|
85 |
; |
|
7135 | 86 |
|
7141 | 87 |
field: name '::' type comment? |
88 |
; |
|
89 |
\end{rail} |
|
90 |
||
7167 | 91 |
\begin{descr} |
7141 | 92 |
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] |
93 |
defines extensible record type $(\vec\alpha)t$, derived from the optional |
|
94 |
parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. |
|
11498 | 95 |
See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on |
7335 | 96 |
simply-typed extensible records. |
7167 | 97 |
\end{descr} |
7141 | 98 |
|
99 |
||
100 |
\section{Datatypes}\label{sec:datatype} |
|
101 |
||
7167 | 102 |
\indexisarcmd{datatype}\indexisarcmd{rep-datatype} |
7141 | 103 |
\begin{matharray}{rcl} |
104 |
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\ |
|
105 |
\isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ |
|
106 |
\end{matharray} |
|
107 |
||
108 |
\railalias{repdatatype}{rep\_datatype} |
|
109 |
\railterm{repdatatype} |
|
110 |
||
111 |
\begin{rail} |
|
9848 | 112 |
'datatype' (dtspec + 'and') |
7141 | 113 |
; |
9848 | 114 |
repdatatype (name * ) dtrules |
7141 | 115 |
; |
116 |
||
9848 | 117 |
dtspec: parname? typespec infix? '=' (cons + '|') |
7141 | 118 |
; |
9848 | 119 |
cons: name (type * ) mixfix? comment? |
120 |
; |
|
121 |
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs |
|
7141 | 122 |
\end{rail} |
123 |
||
7167 | 124 |
\begin{descr} |
7319 | 125 |
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. |
126 |
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive |
|
127 |
ones, generating the standard infrastructure of derived concepts (primitive |
|
128 |
recursion etc.). |
|
7167 | 129 |
\end{descr} |
7141 | 130 |
|
8449 | 131 |
The induction and exhaustion theorems generated provide case names according |
132 |
to the constructors involved, while parameters are named after the types (see |
|
133 |
also \S\ref{sec:induct-method}). |
|
134 |
||
7319 | 135 |
See \cite{isabelle-HOL} for more details on datatypes. Note that the theory |
7335 | 136 |
syntax above has been slightly simplified over the old version, usually |
8531 | 137 |
requiring more quotes and less parentheses. Apart from proper proof methods |
138 |
for case-analysis and induction, there are also emulations of ML tactics |
|
8945 | 139 |
\texttt{case_tac} and \texttt{induct_tac} available, see |
8665 | 140 |
\S\ref{sec:induct_tac}. |
7319 | 141 |
|
7135 | 142 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
143 |
\section{Recursive functions}\label{sec:recursion} |
7135 | 144 |
|
10771 | 145 |
\indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc} |
7141 | 146 |
\begin{matharray}{rcl} |
147 |
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
|
148 |
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
|
10771 | 149 |
\isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ |
7141 | 150 |
%FIXME |
151 |
% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\ |
|
152 |
\end{matharray} |
|
153 |
||
9949 | 154 |
\railalias{recdefsimp}{recdef\_simp} |
155 |
\railterm{recdefsimp} |
|
156 |
||
157 |
\railalias{recdefcong}{recdef\_cong} |
|
158 |
\railterm{recdefcong} |
|
159 |
||
160 |
\railalias{recdefwf}{recdef\_wf} |
|
161 |
\railterm{recdefwf} |
|
162 |
||
10771 | 163 |
\railalias{recdeftc}{recdef\_tc} |
164 |
\railterm{recdeftc} |
|
165 |
||
7141 | 166 |
\begin{rail} |
8657 | 167 |
'primrec' parname? (equation + ) |
168 |
; |
|
11634 | 169 |
'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints? |
9848 | 170 |
; |
10771 | 171 |
recdeftc thmdecl? tc comment? |
172 |
; |
|
8657 | 173 |
|
9848 | 174 |
equation: thmdecl? eqn |
175 |
; |
|
176 |
eqn: prop comment? |
|
8657 | 177 |
; |
9848 | 178 |
hints: '(' 'hints' (recdefmod * ) ')' |
179 |
; |
|
9949 | 180 |
recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod |
7141 | 181 |
; |
10771 | 182 |
tc: nameref ('(' nat ')')? |
183 |
; |
|
7141 | 184 |
\end{rail} |
185 |
||
7167 | 186 |
\begin{descr} |
7319 | 187 |
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over |
9848 | 188 |
datatypes, see also \cite{isabelle-HOL}. |
7319 | 189 |
\item [$\isarkeyword{recdef}$] defines general well-founded recursive |
9848 | 190 |
functions (using the TFL package), see also \cite{isabelle-HOL}. The |
11634 | 191 |
$(permissive)$ option tells TFL to recover from failed proof attempts, |
192 |
returning unfinished results. The $recdef_simp$, $recdef_cong$, and |
|
193 |
$recdef_wf$ hints refer to auxiliary rules to be used in the internal |
|
194 |
automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ |
|
195 |
\S\ref{sec:clasimp}) may be given to tune the context of the Simplifier |
|
196 |
(cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ |
|
197 |
\S\ref{sec:classical}). |
|
10771 | 198 |
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover |
199 |
termination condition number $i$ (default $1$) as generated by a |
|
200 |
$\isarkeyword{recdef}$ definition of constant $c$. |
|
201 |
||
202 |
Note that in most cases, $\isarkeyword{recdef}$ is able to finish its |
|
203 |
internal proofs without manual intervention. |
|
7167 | 204 |
\end{descr} |
7141 | 205 |
|
9848 | 206 |
Both kinds of recursive definitions accommodate reasoning by induction (cf.\ |
8449 | 207 |
\S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name |
208 |
of the function definition) refers to a specific induction rule, with |
|
209 |
parameters named according to the user-specified equations. Case names of |
|
210 |
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of |
|
211 |
$\isarkeyword{recdef}$ are numbered (starting from $1$). |
|
212 |
||
8657 | 213 |
The equations provided by these packages may be referred later as theorem list |
214 |
$f\mathord.simps$, where $f$ is the (collective) name of the functions |
|
215 |
defined. Individual equations may be named explicitly as well; note that for |
|
216 |
$\isarkeyword{recdef}$ each specification given by the user may result in |
|
217 |
several theorems. |
|
218 |
||
9935 | 219 |
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using |
220 |
the following attributes. |
|
221 |
||
222 |
\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf} |
|
223 |
\begin{matharray}{rcl} |
|
224 |
recdef_simp & : & \isaratt \\ |
|
225 |
recdef_cong & : & \isaratt \\ |
|
226 |
recdef_wf & : & \isaratt \\ |
|
227 |
\end{matharray} |
|
228 |
||
229 |
\railalias{recdefsimp}{recdef\_simp} |
|
230 |
\railterm{recdefsimp} |
|
231 |
||
232 |
\railalias{recdefcong}{recdef\_cong} |
|
233 |
\railterm{recdefcong} |
|
234 |
||
235 |
\railalias{recdefwf}{recdef\_wf} |
|
236 |
\railterm{recdefwf} |
|
237 |
||
238 |
\begin{rail} |
|
239 |
(recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') |
|
240 |
; |
|
241 |
\end{rail} |
|
242 |
||
7141 | 243 |
|
10549
5e19ae8d9582
cases/induct: tuned handling of facts ('consumes');
wenzelm
parents:
10456
diff
changeset
|
244 |
\section{(Co)Inductive sets}\label{sec:inductive} |
7135 | 245 |
|
9602 | 246 |
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono} |
7141 | 247 |
\begin{matharray}{rcl} |
248 |
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
|
9848 | 249 |
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
7990 | 250 |
mono & : & \isaratt \\ |
7141 | 251 |
\end{matharray} |
252 |
||
253 |
\railalias{condefs}{con\_defs} |
|
9602 | 254 |
\railterm{condefs} |
7141 | 255 |
|
256 |
\begin{rail} |
|
9848 | 257 |
('inductive' | 'coinductive') sets intros monos? |
7141 | 258 |
; |
7990 | 259 |
'mono' (() | 'add' | 'del') |
260 |
; |
|
9848 | 261 |
|
262 |
sets: (term comment? +) |
|
263 |
; |
|
11634 | 264 |
intros: 'intros' (thmdecl? prop comment? +) |
9848 | 265 |
; |
266 |
monos: 'monos' thmrefs comment? |
|
267 |
; |
|
7141 | 268 |
\end{rail} |
269 |
||
7167 | 270 |
\begin{descr} |
7319 | 271 |
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define |
272 |
(co)inductive sets from the given introduction rules. |
|
8547 | 273 |
\item [$mono$] declares monotonicity rules. These rule are involved in the |
274 |
automated monotonicity proof of $\isarkeyword{inductive}$. |
|
7167 | 275 |
\end{descr} |
7141 | 276 |
|
8449 | 277 |
See \cite{isabelle-HOL} for further information on inductive definitions in |
278 |
HOL. |
|
7319 | 279 |
|
7141 | 280 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
281 |
\section{Arithmetic} |
7141 | 282 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
283 |
\indexisarmeth{arith}\indexisaratt{arith-split} |
7319 | 284 |
\begin{matharray}{rcl} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
285 |
arith & : & \isarmeth \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
286 |
arith_split & : & \isaratt \\ |
7319 | 287 |
\end{matharray} |
288 |
||
289 |
\begin{rail} |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
290 |
'arith' '!'? |
10802
7fa042e28c43
'cases' / 'induct' method: ?case binding, 'of:' spec;
wenzelm
parents:
10771
diff
changeset
|
291 |
; |
7319 | 292 |
\end{rail} |
293 |
||
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
294 |
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
295 |
$real$). Any current facts are inserted into the goal before running the |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
296 |
procedure. The ``!''~argument causes the full context of assumptions to be |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
297 |
included. The $arith_split$ attribute declares case split rules to be |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
298 |
expanded before the arithmetic procedure is invoked. |
8449 | 299 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
300 |
Note that a simpler (but faster) version of arithmetic reasoning is already |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
301 |
performed by the Simplifier. |
10549
5e19ae8d9582
cases/induct: tuned handling of facts ('consumes');
wenzelm
parents:
10456
diff
changeset
|
302 |
|
5e19ae8d9582
cases/induct: tuned handling of facts ('consumes');
wenzelm
parents:
10456
diff
changeset
|
303 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
304 |
\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac} |
8449 | 305 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
306 |
The following important tactical tools of Isabelle/HOL have been ported to |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
307 |
Isar. These should be never used in proper proof texts! |
8665 | 308 |
|
309 |
\indexisarmeth{case-tac}\indexisarmeth{induct-tac} |
|
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
310 |
\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases} |
8665 | 311 |
\begin{matharray}{rcl} |
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
312 |
case_tac^* & : & \isarmeth \\ |
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
313 |
induct_tac^* & : & \isarmeth \\ |
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
314 |
ind_cases^* & : & \isarmeth \\ |
9602 | 315 |
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
8665 | 316 |
\end{matharray} |
317 |
||
318 |
\railalias{casetac}{case\_tac} |
|
319 |
\railterm{casetac} |
|
9602 | 320 |
|
8665 | 321 |
\railalias{inducttac}{induct\_tac} |
322 |
\railterm{inducttac} |
|
323 |
||
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
324 |
\railalias{indcases}{ind\_cases} |
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
325 |
\railterm{indcases} |
9602 | 326 |
|
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
327 |
\railalias{inductivecases}{inductive\_cases} |
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
328 |
\railterm{inductivecases} |
9602 | 329 |
|
8665 | 330 |
\begin{rail} |
8666 | 331 |
casetac goalspec? term rule? |
8665 | 332 |
; |
8692 | 333 |
inducttac goalspec? (insts * 'and') rule? |
8666 | 334 |
; |
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
335 |
indcases (prop +) |
9602 | 336 |
; |
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
337 |
inductivecases thmdecl? (prop +) comment? |
9602 | 338 |
; |
8666 | 339 |
|
340 |
rule: ('rule' ':' thmref) |
|
8665 | 341 |
; |
342 |
\end{rail} |
|
343 |
||
9602 | 344 |
\begin{descr} |
345 |
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes |
|
346 |
only (unless an alternative rule is given explicitly). Furthermore, |
|
347 |
$case_tac$ does a classical case split on booleans; $induct_tac$ allows only |
|
348 |
variables to be given as instantiation. These tactic emulations feature |
|
349 |
both goal addressing and dynamic instantiation. Note that named local |
|
350 |
contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the |
|
351 |
proper $induct$ and $cases$ proof methods (see |
|
352 |
\S\ref{sec:induct-method-proper}). |
|
353 |
||
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
354 |
\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
|
355 |
to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11662
diff
changeset
|
356 |
forward manner. |
9602 | 357 |
|
9616
b80ea2b32f8e
cases/induct method: 'opaque' by default; added 'open' option;
wenzelm
parents:
9602
diff
changeset
|
358 |
While $ind_cases$ is a proof method to apply the result immediately as |
9602 | 359 |
elimination rules, $\isarkeyword{inductive_cases}$ provides case split |
360 |
theorems at the theory level for later use, |
|
361 |
\end{descr} |
|
8665 | 362 |
|
363 |
||
7046 | 364 |
%%% Local Variables: |
365 |
%%% mode: latex |
|
366 |
%%% TeX-master: "isar-ref" |
|
367 |
%%% End: |