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