1 |
|
2 \chapter{Isabelle/HOL specific elements}\label{ch:hol-tools} |
|
3 |
|
4 \section{Miscellaneous attributes} |
|
5 |
|
6 \indexisarattof{HOL}{split-format} |
|
7 \begin{matharray}{rcl} |
|
8 split_format^* & : & \isaratt \\ |
|
9 \end{matharray} |
|
10 |
|
11 \railalias{splitformat}{split\_format} |
|
12 \railterm{splitformat} |
|
13 \railterm{complete} |
|
14 |
|
15 \begin{rail} |
|
16 splitformat (((name * ) + 'and') | ('(' complete ')')) |
|
17 ; |
|
18 \end{rail} |
|
19 |
|
20 \begin{descr} |
|
21 |
|
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 |
|
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. |
|
27 |
|
28 Note that these operations tend to invent funny names for new local |
|
29 parameters to be introduced. |
|
30 |
|
31 \end{descr} |
|
32 |
|
33 |
|
34 \section{Primitive types}\label{sec:typedef} |
|
35 |
|
36 \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} |
|
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 |
|
49 \begin{descr} |
|
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 |
|
56 augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} |
|
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 |
|
59 packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and |
|
60 $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). |
|
61 \end{descr} |
|
62 |
|
63 |
|
64 \section{Records}\label{sec:hol-record} |
|
65 |
|
66 FIXME proof tools (simp, cases/induct; no split!?); |
|
67 |
|
68 \indexisarcmdof{HOL}{record} |
|
69 \begin{matharray}{rcl} |
|
70 \isarcmd{record} & : & \isartrans{theory}{theory} \\ |
|
71 \end{matharray} |
|
72 |
|
73 \begin{rail} |
|
74 'record' typespec '=' (type '+')? (field +) |
|
75 ; |
|
76 |
|
77 field: name '::' type comment? |
|
78 ; |
|
79 \end{rail} |
|
80 |
|
81 \begin{descr} |
|
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$. |
|
85 See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on |
|
86 simply-typed extensible records. |
|
87 \end{descr} |
|
88 |
|
89 |
|
90 \section{Datatypes}\label{sec:hol-datatype} |
|
91 |
|
92 \indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} |
|
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} |
|
102 'datatype' (dtspec + 'and') |
|
103 ; |
|
104 repdatatype (name * ) dtrules |
|
105 ; |
|
106 |
|
107 dtspec: parname? typespec infix? '=' (cons + '|') |
|
108 ; |
|
109 cons: name (type * ) mixfix? comment? |
|
110 ; |
|
111 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs |
|
112 \end{rail} |
|
113 |
|
114 \begin{descr} |
|
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.). |
|
119 \end{descr} |
|
120 |
|
121 The induction and exhaustion theorems generated provide case names according |
|
122 to the constructors involved, while parameters are named after the types (see |
|
123 also \S\ref{sec:cases-induct}). |
|
124 |
|
125 See \cite{isabelle-HOL} for more details on datatypes. Note that the theory |
|
126 syntax above has been slightly simplified over the old version, usually |
|
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 |
|
129 \texttt{case_tac} and \texttt{induct_tac} available, see |
|
130 \S\ref{sec:induct_tac}. |
|
131 |
|
132 |
|
133 \section{Recursive functions}\label{sec:recursion} |
|
134 |
|
135 \indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} |
|
136 \begin{matharray}{rcl} |
|
137 \isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
|
138 \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
|
139 \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ |
|
140 %FIXME |
|
141 % \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\ |
|
142 \end{matharray} |
|
143 |
|
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 |
|
153 \railalias{recdeftc}{recdef\_tc} |
|
154 \railterm{recdeftc} |
|
155 |
|
156 \begin{rail} |
|
157 'primrec' parname? (equation + ) |
|
158 ; |
|
159 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints? |
|
160 ; |
|
161 recdeftc thmdecl? tc comment? |
|
162 ; |
|
163 |
|
164 equation: thmdecl? eqn |
|
165 ; |
|
166 eqn: prop comment? |
|
167 ; |
|
168 hints: '(' 'hints' (recdefmod * ) ')' |
|
169 ; |
|
170 recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod |
|
171 ; |
|
172 tc: nameref ('(' nat ')')? |
|
173 ; |
|
174 \end{rail} |
|
175 |
|
176 \begin{descr} |
|
177 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over |
|
178 datatypes, see also \cite{isabelle-HOL}. |
|
179 \item [$\isarkeyword{recdef}$] defines general well-founded recursive |
|
180 functions (using the TFL package), see also \cite{isabelle-HOL}. The |
|
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}). |
|
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. |
|
194 \end{descr} |
|
195 |
|
196 Both kinds of recursive definitions accommodate reasoning by induction (cf.\ |
|
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 |
|
200 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of |
|
201 $\isarkeyword{recdef}$ are numbered (starting from $1$). |
|
202 |
|
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 |
|
209 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using |
|
210 the following attributes. |
|
211 |
|
212 \indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} |
|
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 |
|
233 |
|
234 \section{(Co)Inductive sets}\label{sec:hol-inductive} |
|
235 |
|
236 \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono} |
|
237 \begin{matharray}{rcl} |
|
238 \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
|
239 \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
|
240 mono & : & \isaratt \\ |
|
241 \end{matharray} |
|
242 |
|
243 \railalias{condefs}{con\_defs} |
|
244 \railterm{condefs} |
|
245 |
|
246 \begin{rail} |
|
247 ('inductive' | 'coinductive') sets intros monos? |
|
248 ; |
|
249 'mono' (() | 'add' | 'del') |
|
250 ; |
|
251 |
|
252 sets: (term comment? +) |
|
253 ; |
|
254 intros: 'intros' (thmdecl? prop comment? +) |
|
255 ; |
|
256 monos: 'monos' thmrefs comment? |
|
257 ; |
|
258 \end{rail} |
|
259 |
|
260 \begin{descr} |
|
261 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define |
|
262 (co)inductive sets from the given introduction rules. |
|
263 \item [$mono$] declares monotonicity rules. These rule are involved in the |
|
264 automated monotonicity proof of $\isarkeyword{inductive}$. |
|
265 \end{descr} |
|
266 |
|
267 See \cite{isabelle-HOL} for further information on inductive definitions in |
|
268 HOL. |
|
269 |
|
270 |
|
271 \section{Arithmetic} |
|
272 |
|
273 \indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split} |
|
274 \begin{matharray}{rcl} |
|
275 arith & : & \isarmeth \\ |
|
276 arith_split & : & \isaratt \\ |
|
277 \end{matharray} |
|
278 |
|
279 \begin{rail} |
|
280 'arith' '!'? |
|
281 ; |
|
282 \end{rail} |
|
283 |
|
284 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, |
|
285 $real$). Any current facts are inserted into the goal before running the |
|
286 procedure. The ``!''~argument causes the full context of assumptions to be |
|
287 included. The $arith_split$ attribute declares case split rules to be |
|
288 expanded before the arithmetic procedure is invoked. |
|
289 |
|
290 Note that a simpler (but faster) version of arithmetic reasoning is already |
|
291 performed by the Simplifier. |
|
292 |
|
293 |
|
294 \section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac} |
|
295 |
|
296 The following important tactical tools of Isabelle/HOL have been ported to |
|
297 Isar. These should be never used in proper proof texts! |
|
298 |
|
299 \indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} |
|
300 \indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} |
|
301 \begin{matharray}{rcl} |
|
302 case_tac^* & : & \isarmeth \\ |
|
303 induct_tac^* & : & \isarmeth \\ |
|
304 ind_cases^* & : & \isarmeth \\ |
|
305 \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
|
306 \end{matharray} |
|
307 |
|
308 \railalias{casetac}{case\_tac} |
|
309 \railterm{casetac} |
|
310 |
|
311 \railalias{inducttac}{induct\_tac} |
|
312 \railterm{inducttac} |
|
313 |
|
314 \railalias{indcases}{ind\_cases} |
|
315 \railterm{indcases} |
|
316 |
|
317 \railalias{inductivecases}{inductive\_cases} |
|
318 \railterm{inductivecases} |
|
319 |
|
320 \begin{rail} |
|
321 casetac goalspec? term rule? |
|
322 ; |
|
323 inducttac goalspec? (insts * 'and') rule? |
|
324 ; |
|
325 indcases (prop +) |
|
326 ; |
|
327 inductivecases thmdecl? (prop +) comment? |
|
328 ; |
|
329 |
|
330 rule: ('rule' ':' thmref) |
|
331 ; |
|
332 \end{rail} |
|
333 |
|
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 |
|
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}). |
|
342 |
|
343 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface |
|
344 to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted |
|
345 forward manner. |
|
346 |
|
347 While $ind_cases$ is a proof method to apply the result immediately as |
|
348 elimination rules, $\isarkeyword{inductive_cases}$ provides case split |
|
349 theorems at the theory level for later use, |
|
350 \end{descr} |
|
351 |
|
352 |
|
353 %%% Local Variables: |
|
354 %%% mode: latex |
|
355 %%% TeX-master: "isar-ref" |
|
356 %%% End: |
|