1 |
1 |
2 \chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools} |
2 \chapter{Isabelle/HOL specific elements}\label{ch:hol-tools} |
3 |
3 |
4 \section{Miscellaneous attributes}\label{sec:rule-format} |
4 \section{Miscellaneous attributes} |
5 |
5 |
6 \indexisaratt{rule-format}\indexisaratt{split-format} |
6 \indexisarattof{HOL}{split-format} |
7 \begin{matharray}{rcl} |
7 \begin{matharray}{rcl} |
8 rule_format & : & \isaratt \\ |
|
9 split_format^* & : & \isaratt \\ |
8 split_format^* & : & \isaratt \\ |
10 \end{matharray} |
9 \end{matharray} |
11 |
|
12 \railalias{ruleformat}{rule\_format} |
|
13 \railterm{ruleformat} |
|
14 |
10 |
15 \railalias{splitformat}{split\_format} |
11 \railalias{splitformat}{split\_format} |
16 \railterm{splitformat} |
12 \railterm{splitformat} |
17 \railterm{complete} |
13 \railterm{complete} |
18 |
14 |
19 \begin{rail} |
15 \begin{rail} |
20 ruleformat ('(' noasm ')')? |
|
21 ; |
|
22 splitformat (((name * ) + 'and') | ('(' complete ')')) |
16 splitformat (((name * ) + 'and') | ('(' complete ')')) |
23 ; |
17 ; |
24 \end{rail} |
18 \end{rail} |
25 |
19 |
26 \begin{descr} |
20 \begin{descr} |
27 |
|
28 \item [$rule_format$] causes a theorem to be put into standard object-rule |
|
29 form, replacing implication and (bounded) universal quantification of HOL by |
|
30 the corresponding meta-logical connectives. By default, the result is fully |
|
31 normalized, including assumptions and conclusions at any depth. The |
|
32 $no_asm$ option restricts the transformation to the conclusion of a rule. |
|
33 |
21 |
34 \item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into |
22 \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 |
23 canonical form as specified by the arguments given; $\vec p@i$ refers to |
36 occurrences in premise $i$ of the rule. The $split_format~(complete)$ form |
24 occurrences in premise $i$ of the rule. The $split_format~(complete)$ form |
37 causes \emph{all} arguments in function applications to be represented |
25 causes \emph{all} arguments in function applications to be represented |
43 \end{descr} |
31 \end{descr} |
44 |
32 |
45 |
33 |
46 \section{Primitive types}\label{sec:typedef} |
34 \section{Primitive types}\label{sec:typedef} |
47 |
35 |
48 \indexisarcmd{typedecl}\indexisarcmd{typedef} |
36 \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} |
49 \begin{matharray}{rcl} |
37 \begin{matharray}{rcl} |
50 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
38 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
51 \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ |
39 \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ |
52 \end{matharray} |
40 \end{matharray} |
53 |
41 |
66 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating |
54 \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 |
55 non-emptiness of the set $A$. After finishing the proof, the theory will be |
68 augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} |
56 augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} |
69 for more information. Note that user-level theories usually do not directly |
57 for more information. Note that user-level theories usually do not directly |
70 refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced |
58 refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced |
71 packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and |
59 packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and |
72 $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}). |
60 $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). |
73 \end{descr} |
61 \end{descr} |
74 |
62 |
75 |
63 |
76 \section{Records}\label{sec:record} |
64 \section{Records}\label{sec:hol-record} |
77 |
65 |
78 \indexisarcmd{record} |
66 FIXME proof tools (simp, cases/induct; no split!?); |
|
67 |
|
68 \indexisarcmdof{HOL}{record} |
79 \begin{matharray}{rcl} |
69 \begin{matharray}{rcl} |
80 \isarcmd{record} & : & \isartrans{theory}{theory} \\ |
70 \isarcmd{record} & : & \isartrans{theory}{theory} \\ |
81 \end{matharray} |
71 \end{matharray} |
82 |
72 |
83 \begin{rail} |
73 \begin{rail} |
95 See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on |
85 See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on |
96 simply-typed extensible records. |
86 simply-typed extensible records. |
97 \end{descr} |
87 \end{descr} |
98 |
88 |
99 |
89 |
100 \section{Datatypes}\label{sec:datatype} |
90 \section{Datatypes}\label{sec:hol-datatype} |
101 |
91 |
102 \indexisarcmd{datatype}\indexisarcmd{rep-datatype} |
92 \indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} |
103 \begin{matharray}{rcl} |
93 \begin{matharray}{rcl} |
104 \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ |
94 \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ |
105 \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ |
95 \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ |
106 \end{matharray} |
96 \end{matharray} |
107 |
97 |
128 recursion etc.). |
118 recursion etc.). |
129 \end{descr} |
119 \end{descr} |
130 |
120 |
131 The induction and exhaustion theorems generated provide case names according |
121 The induction and exhaustion theorems generated provide case names according |
132 to the constructors involved, while parameters are named after the types (see |
122 to the constructors involved, while parameters are named after the types (see |
133 also \S\ref{sec:induct-method}). |
123 also \S\ref{sec:cases-induct}). |
134 |
124 |
135 See \cite{isabelle-HOL} for more details on datatypes. Note that the theory |
125 See \cite{isabelle-HOL} for more details on datatypes. Note that the theory |
136 syntax above has been slightly simplified over the old version, usually |
126 syntax above has been slightly simplified over the old version, usually |
137 requiring more quotes and less parentheses. Apart from proper proof methods |
127 requiring more quotes and less parentheses. Apart from proper proof methods |
138 for case-analysis and induction, there are also emulations of ML tactics |
128 for case-analysis and induction, there are also emulations of ML tactics |
140 \S\ref{sec:induct_tac}. |
130 \S\ref{sec:induct_tac}. |
141 |
131 |
142 |
132 |
143 \section{Recursive functions}\label{sec:recursion} |
133 \section{Recursive functions}\label{sec:recursion} |
144 |
134 |
145 \indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc} |
135 \indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} |
146 \begin{matharray}{rcl} |
136 \begin{matharray}{rcl} |
147 \isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
137 \isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
148 \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
138 \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
149 \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ |
139 \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ |
150 %FIXME |
140 %FIXME |
202 Note that in most cases, $\isarkeyword{recdef}$ is able to finish its |
192 Note that in most cases, $\isarkeyword{recdef}$ is able to finish its |
203 internal proofs without manual intervention. |
193 internal proofs without manual intervention. |
204 \end{descr} |
194 \end{descr} |
205 |
195 |
206 Both kinds of recursive definitions accommodate reasoning by induction (cf.\ |
196 Both kinds of recursive definitions accommodate reasoning by induction (cf.\ |
207 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name |
197 \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of |
208 of the function definition) refers to a specific induction rule, with |
198 the function definition) refers to a specific induction rule, with parameters |
209 parameters named according to the user-specified equations. Case names of |
199 named according to the user-specified equations. Case names of |
210 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of |
200 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of |
211 $\isarkeyword{recdef}$ are numbered (starting from $1$). |
201 $\isarkeyword{recdef}$ are numbered (starting from $1$). |
212 |
202 |
213 The equations provided by these packages may be referred later as theorem list |
203 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 |
204 $f\mathord.simps$, where $f$ is the (collective) name of the functions |
217 several theorems. |
207 several theorems. |
218 |
208 |
219 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using |
209 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using |
220 the following attributes. |
210 the following attributes. |
221 |
211 |
222 \indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf} |
212 \indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} |
223 \begin{matharray}{rcl} |
213 \begin{matharray}{rcl} |
224 recdef_simp & : & \isaratt \\ |
214 recdef_simp & : & \isaratt \\ |
225 recdef_cong & : & \isaratt \\ |
215 recdef_cong & : & \isaratt \\ |
226 recdef_wf & : & \isaratt \\ |
216 recdef_wf & : & \isaratt \\ |
227 \end{matharray} |
217 \end{matharray} |
239 (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') |
229 (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') |
240 ; |
230 ; |
241 \end{rail} |
231 \end{rail} |
242 |
232 |
243 |
233 |
244 \section{(Co)Inductive sets}\label{sec:inductive} |
234 \section{(Co)Inductive sets}\label{sec:hol-inductive} |
245 |
235 |
246 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono} |
236 \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono} |
247 \begin{matharray}{rcl} |
237 \begin{matharray}{rcl} |
248 \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
238 \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
249 \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
239 \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
250 mono & : & \isaratt \\ |
240 mono & : & \isaratt \\ |
251 \end{matharray} |
241 \end{matharray} |
304 \section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac} |
294 \section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac} |
305 |
295 |
306 The following important tactical tools of Isabelle/HOL have been ported to |
296 The following important tactical tools of Isabelle/HOL have been ported to |
307 Isar. These should be never used in proper proof texts! |
297 Isar. These should be never used in proper proof texts! |
308 |
298 |
309 \indexisarmeth{case-tac}\indexisarmeth{induct-tac} |
299 \indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} |
310 \indexisarmeth{ind-cases}\indexisarcmd{inductive-cases} |
300 \indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} |
311 \begin{matharray}{rcl} |
301 \begin{matharray}{rcl} |
312 case_tac^* & : & \isarmeth \\ |
302 case_tac^* & : & \isarmeth \\ |
313 induct_tac^* & : & \isarmeth \\ |
303 induct_tac^* & : & \isarmeth \\ |
314 ind_cases^* & : & \isarmeth \\ |
304 ind_cases^* & : & \isarmeth \\ |
315 \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
305 \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
344 \begin{descr} |
334 \begin{descr} |
345 \item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes |
335 \item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes |
346 only (unless an alternative rule is given explicitly). Furthermore, |
336 only (unless an alternative rule is given explicitly). Furthermore, |
347 $case_tac$ does a classical case split on booleans; $induct_tac$ allows only |
337 $case_tac$ does a classical case split on booleans; $induct_tac$ allows only |
348 variables to be given as instantiation. These tactic emulations feature |
338 variables to be given as instantiation. These tactic emulations feature |
349 both goal addressing and dynamic instantiation. Note that named local |
339 both goal addressing and dynamic instantiation. Note that named rule cases |
350 contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the |
340 are \emph{not} provided as would be by the proper $induct$ and $cases$ proof |
351 proper $induct$ and $cases$ proof methods (see |
341 methods (see \S\ref{sec:cases-induct}). |
352 \S\ref{sec:induct-method-proper}). |
|
353 |
342 |
354 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface |
343 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface |
355 to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted |
344 to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted |
356 forward manner. |
345 forward manner. |
357 |
346 |