35 {\makeatother\input{ToyList/document/ToyList.tex}} |
35 {\makeatother\input{ToyList/document/ToyList.tex}} |
36 |
36 |
37 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The |
37 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The |
38 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} |
38 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} |
39 constitutes the complete theory \texttt{ToyList} and should reside in file |
39 constitutes the complete theory \texttt{ToyList} and should reside in file |
40 \texttt{ToyList.thy}. It is good practice to present all declarations and |
40 \texttt{ToyList.thy}. |
41 definitions at the beginning of a theory to facilitate browsing.% |
41 % It is good practice to present all declarations and |
|
42 %definitions at the beginning of a theory to facilitate browsing.% |
42 \index{*ToyList example|)} |
43 \index{*ToyList example|)} |
43 |
44 |
44 \begin{figure}[htbp] |
45 \begin{figure}[htbp] |
45 \begin{ttbox}\makeatother |
46 \begin{ttbox}\makeatother |
46 \input{ToyList2/ToyList2}\end{ttbox} |
47 \input{ToyList2/ToyList2}\end{ttbox} |
68 and can be skipped by casual readers. |
69 and can be skipped by casual readers. |
69 |
70 |
70 There are two kinds of commands used during a proof: the actual proof |
71 There are two kinds of commands used during a proof: the actual proof |
71 commands and auxiliary commands for examining the proof state and controlling |
72 commands and auxiliary commands for examining the proof state and controlling |
72 the display. Simple proof commands are of the form |
73 the display. Simple proof commands are of the form |
73 \commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically |
74 \commdx{apply}(\textit{method}), where \textit{method} is typically |
74 \isa{induct_tac} or \isa{auto}. All such theorem proving operations |
75 \isa{induct_tac} or \isa{auto}. All such theorem proving operations |
75 are referred to as \bfindex{methods}, and further ones are |
76 are referred to as \bfindex{methods}, and further ones are |
76 introduced throughout the tutorial. Unless stated otherwise, you may |
77 introduced throughout the tutorial. Unless stated otherwise, you may |
77 assume that a method attacks merely the first subgoal. An exception is |
78 assume that a method attacks merely the first subgoal. An exception is |
78 \isa{auto}, which tries to solve all subgoals. |
79 \isa{auto}, which tries to solve all subgoals. |
142 % The only time when you need to load a theory by hand is when you simply |
143 % The only time when you need to load a theory by hand is when you simply |
143 % want to check if it loads successfully without wanting to make use of the |
144 % want to check if it loads successfully without wanting to make use of the |
144 % theory itself. This you can do by typing |
145 % theory itself. This you can do by typing |
145 % \isa{\commdx{use\_thy}~"T"}. |
146 % \isa{\commdx{use\_thy}~"T"}. |
146 \end{description} |
147 \end{description} |
147 Further commands are found in the Isabelle/Isar Reference Manual. |
148 Further commands are found in the Isabelle/Isar Reference |
|
149 Manual~\cite{isabelle-isar-ref}. |
148 |
150 |
149 We now examine Isabelle's functional programming constructs systematically, |
151 We now examine Isabelle's functional programming constructs systematically, |
150 starting with inductive datatypes. |
152 starting with inductive datatypes. |
151 |
153 |
152 |
154 |
173 preferable to \isa{hd} and \isa{tl}.) |
175 preferable to \isa{hd} and \isa{tl}.) |
174 Also available are higher-order functions like \isa{map} and \isa{filter}. |
176 Also available are higher-order functions like \isa{map} and \isa{filter}. |
175 Theory \isa{List} also contains |
177 Theory \isa{List} also contains |
176 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates |
178 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates |
177 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we |
179 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we |
178 always use HOL's predefined lists. |
180 always use HOL's predefined lists by building on theory \isa{Main}. |
179 |
181 |
180 |
182 |
181 \subsection{The General Format} |
183 \subsection{The General Format} |
182 \label{sec:general-datatype} |
184 \label{sec:general-datatype} |
183 |
185 |
196 Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and |
198 Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and |
197 \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically |
199 \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically |
198 during proofs by simplification. The same is true for the equations in |
200 during proofs by simplification. The same is true for the equations in |
199 primitive recursive function definitions. |
201 primitive recursive function definitions. |
200 |
202 |
201 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into |
203 Every\footnote{Except for advanced datatypes where the recursion involves |
202 the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is |
204 ``\isasymRightarrow'' as in {\S}\ref{sec:nested-fun-datatype}.} datatype $t$ |
203 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs + |
205 comes equipped with a \isa{size} function from $t$ into the natural numbers |
204 1}. In general, \cdx{size} returns |
206 (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\ |
|
207 \isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}. In general, |
|
208 \cdx{size} returns |
205 \begin{itemize} |
209 \begin{itemize} |
206 \item zero for all constructors |
210 \item zero for all constructors |
207 that do not have an argument of type $t$\\ |
211 that do not have an argument of type $t$\\ |
208 \item one plus the sum of the sizes of all arguments of type~$t$, |
212 \item one plus the sum of the sizes of all arguments of type~$t$, |
209 for all other constructors |
213 for all other constructors |
273 definitions. |
277 definitions. |
274 |
278 |
275 |
279 |
276 \subsection{Type Synonyms} |
280 \subsection{Type Synonyms} |
277 |
281 |
278 \index{type synonyms|(}% |
282 \index{type synonyms}% |
279 Type synonyms are similar to those found in ML\@. They are created by a |
283 Type synonyms are similar to those found in ML\@. They are created by a |
280 \commdx{types} command: |
284 \commdx{types} command: |
281 |
285 |
282 \input{Misc/document/types.tex}% |
286 \input{Misc/document/types.tex} |
283 \index{type synonyms|)} |
|
284 |
287 |
285 \input{Misc/document/prime_def.tex} |
288 \input{Misc/document/prime_def.tex} |
286 |
289 |
287 \input{Misc/document/Translations.tex} |
290 \input{Misc/document/Translations.tex} |
288 |
291 |
395 |
398 |
396 {\makeatother\input{Datatype/document/Nested.tex}} |
399 {\makeatother\input{Datatype/document/Nested.tex}} |
397 |
400 |
398 |
401 |
399 \subsection{The Limits of Nested Recursion} |
402 \subsection{The Limits of Nested Recursion} |
|
403 \label{sec:nested-fun-datatype} |
400 |
404 |
401 How far can we push nested recursion? By the unfolding argument above, we can |
405 How far can we push nested recursion? By the unfolding argument above, we can |
402 reduce nested to mutual recursion provided the nested recursion only involves |
406 reduce nested to mutual recursion provided the nested recursion only involves |
403 previously defined datatypes. This does not include functions: |
407 previously defined datatypes. This does not include functions: |
404 \begin{isabelle} |
408 \begin{isabelle} |