author | paulson |

Fri Jul 13 18:07:01 2001 +0200 (2001-07-13) | |

changeset 11419 | 9577530e8a5a |

parent 11418 | 53a402c10ba9 |

child 11420 | 9529d31f39e0 |

more indexing

1.1 --- a/doc-src/TutorialI/fp.tex Fri Jul 13 17:58:39 2001 +0200 1.2 +++ b/doc-src/TutorialI/fp.tex Fri Jul 13 18:07:01 2001 +0200 1.3 @@ -1,4 +1,54 @@ 1.4 -\chapter{Functional Programming in HOL} Although on the surface this chapter is mainly concerned with how to write functional programs in HOL and how to verify them, most of the constructs and proof procedures introduced are general purpose and recur in any specification or verification task. In fact, we really should speak of functional \emph{modelling} rather than \emph{programming}: our primary aim is not to write programs but to design abstract models of systems. HOL is a specification language that goes well beyond what can be expressed as a program. However, for the time being we concentrate on the computable. The dedicated functional programmer should be warned: HOL offers only \emph{total functional programming} --- all functions in HOL must be total, i.e.\ they must terminate for all inputs; lazy data structures are not directly available. \section{An Introductory Theory} \label{sec:intro-theory} Functional programming needs datatypes and functions. Both of them can be defined in a theory with a syntax reminiscent of languages like ML or Haskell. As an example consider the theory in figure~\ref{fig:ToyList}. We will now examine it line by line. \begin{figure}[htbp] \begin{ttbox}\makeatother \input{ToyList2/ToyList1}\end{ttbox} \caption{A theory of lists} \label{fig:ToyList} \end{figure} {\makeatother\input{ToyList/document/ToyList.tex}} The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} constitutes the complete theory \texttt{ToyList} and should reside in file \texttt{ToyList.thy}. It is good practice to present all declarations and definitions at the beginning of a theory to facilitate browsing. \begin{figure}[htbp] \begin{ttbox}\makeatother \input{ToyList2/ToyList2}\end{ttbox} \caption{Proofs about lists} \label{fig:ToyList-proofs} \end{figure} \subsubsection*{Review} This is the end of our toy proof. It should have familiarized you with \begin{itemize} \item the standard theorem proving procedure: 1.5 +\chapter{Functional Programming in HOL} 1.6 + 1.7 +Although on the surface this chapter is mainly concerned with how to write 1.8 +functional programs in HOL and how to verify them, most of the constructs and 1.9 +proof procedures introduced are general purpose and recur in any specification 1.10 +or verification task. In fact, we really should speak of functional 1.11 +\emph{modelling} rather than \emph{programming}: our primary aim is not 1.12 +to write programs but to design abstract models of systems. HOL is 1.13 +a specification language that goes well beyond what can be expressed as a 1.14 +program. However, for the time being we concentrate on the computable. 1.15 + 1.16 +The dedicated functional programmer should be warned: HOL offers only 1.17 +\emph{total functional programming} --- all functions in HOL must be total, 1.18 +i.e.\ they must terminate for all inputs; lazy data structures are not 1.19 +directly available. 1.20 + 1.21 +\section{An Introductory Theory} 1.22 +\label{sec:intro-theory} 1.23 + 1.24 +Functional programming needs datatypes and functions. Both of them can be 1.25 +defined in a theory with a syntax reminiscent of languages like ML or 1.26 +Haskell. As an example consider the theory in figure~\ref{fig:ToyList}. 1.27 +We will now examine it line by line. 1.28 + 1.29 +\begin{figure}[htbp] 1.30 +\begin{ttbox}\makeatother 1.31 +\input{ToyList2/ToyList1}\end{ttbox} 1.32 +\caption{A theory of lists} 1.33 +\label{fig:ToyList} 1.34 +\end{figure} 1.35 + 1.36 +{\makeatother\input{ToyList/document/ToyList.tex}} 1.37 + 1.38 +The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The 1.39 +concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} 1.40 +constitutes the complete theory \texttt{ToyList} and should reside in file 1.41 +\texttt{ToyList.thy}. It is good practice to present all declarations and 1.42 +definitions at the beginning of a theory to facilitate browsing. 1.43 + 1.44 +\begin{figure}[htbp] 1.45 +\begin{ttbox}\makeatother 1.46 +\input{ToyList2/ToyList2}\end{ttbox} 1.47 +\caption{Proofs about lists} 1.48 +\label{fig:ToyList-proofs} 1.49 +\end{figure} 1.50 + 1.51 +\subsubsection*{Review} 1.52 + 1.53 +This is the end of our toy proof. It should have familiarized you with 1.54 +\begin{itemize} 1.55 +\item the standard theorem proving procedure: 1.56 state a goal (lemma or theorem); proceed with proof until a separate lemma is 1.57 required; prove that lemma; come back to the original goal. 1.58 \item a specific procedure that works well for functional programs: 1.59 @@ -16,30 +66,32 @@ 1.60 There are two kinds of commands used during a proof: the actual proof 1.61 commands and auxiliary commands for examining the proof state and controlling 1.62 the display. Simple proof commands are of the form 1.63 -\isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a 1.64 -synonym for ``theorem proving function''. Typical examples are 1.65 -\isa{induct_tac} and \isa{auto}. Further methods are introduced throughout 1.66 -the tutorial. Unless stated otherwise you may assume that a method attacks 1.67 -merely the first subgoal. An exception is \isa{auto} which tries to solve all 1.68 -subgoals. 1.69 +\commdx{apply}\isa{(method)}, where \isa{method} is typically 1.70 +\isa{induct_tac} or \isa{auto}. All such theorem proving operations 1.71 +are referred to as \bfindex{methods}, and further ones are 1.72 +introduced throughout the tutorial. Unless stated otherwise, you may 1.73 +assume that a method attacks merely the first subgoal. An exception is 1.74 +\isa{auto}, which tries to solve all subgoals. 1.75 1.76 -The most useful auxiliary commands are: 1.77 +The most useful auxiliary commands are as follows: 1.78 \begin{description} 1.79 -\item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the 1.80 +\item[Undoing:] \commdx{undo} undoes the effect of 1.81 +the 1.82 last command; \isacommand{undo} can be undone by 1.83 - \isacommand{redo}\indexbold{*redo}. Both are only needed at the shell 1.84 + \commdx{redo}. Both are only needed at the shell 1.85 level and should not occur in the final theory. 1.86 -\item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays 1.87 +\item[Printing the current state:] \commdx{pr} 1.88 +redisplays 1.89 the current proof state, for example when it has scrolled past the top of 1.90 the screen. 1.91 \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to 1.92 print only the first $n$ subgoals from now on and redisplays the current 1.93 proof state. This is helpful when there are many subgoals. 1.94 \item[Modifying the order of subgoals:] 1.95 -\isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and 1.96 -\isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front. 1.97 +\commdx{defer} moves the first subgoal to the end and 1.98 +\commdx{prefer}~$n$ moves subgoal $n$ to the front. 1.99 \item[Printing theorems:] 1.100 - \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$ 1.101 + \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$ 1.102 prints the named theorems. 1.103 \item[Displaying types:] We have already mentioned the flag 1.104 \ttindex{show_types} above. It can also be useful for detecting typos in 1.105 @@ -62,10 +114,10 @@ 1.106 \end{isabelle}% 1.107 \par\noindent 1.108 would have alerted us because of the unexpected variable \isa{re}. 1.109 -\item[Reading terms and types:] \isacommand{term}\indexbold{*term} 1.110 +\item[Reading terms and types:] \commdx{term} 1.111 \textit{string} reads, type-checks and prints the given string as a term in 1.112 the current context; the inferred type is output as well. 1.113 - \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given 1.114 + \commdx{typ} \textit{string} reads and prints the given 1.115 string as a type in the current context. 1.116 \item[(Re)loading theories:] When you start your interaction you must open a 1.117 named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle 1.118 @@ -76,7 +128,7 @@ 1.119 If you suddenly discover that you need to modify a parent theory of your 1.120 current theory, you must first abandon your current theory\indexbold{abandon 1.121 theory}\indexbold{theory!abandon} (at the shell 1.122 - level type \isacommand{kill}\indexbold{*kill}). After the parent theory has 1.123 + level type \commdx{kill}). After the parent theory has 1.124 been modified, you go back to your original theory. When its first line 1.125 \isa{\isacommand{theory}~T~=~\dots~:} is processed, the 1.126 modified parent is reloaded automatically. 1.127 @@ -84,7 +136,7 @@ 1.128 % The only time when you need to load a theory by hand is when you simply 1.129 % want to check if it loads successfully without wanting to make use of the 1.130 % theory itself. This you can do by typing 1.131 -% \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. 1.132 +% \isa{\commdx{use\_thy}~"T"}. 1.133 \end{description} 1.134 Further commands are found in the Isabelle/Isar Reference Manual. 1.135 1.136 @@ -109,7 +161,7 @@ 1.137 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory 1.138 \isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. 1.139 The latter contains many further operations. For example, the functions 1.140 -\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first 1.141 +\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first 1.142 element and the remainder of a list. (However, pattern-matching is usually 1.143 preferable to \isa{hd} and \isa{tl}.) 1.144 Also available are higher-order functions like \isa{map} and \isa{filter}. 1.145 @@ -142,11 +194,11 @@ 1.146 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into 1.147 the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is 1.148 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1.149 - 1}. In general, \isaindexbold{size} returns \isa{0} for all constructors 1.150 + 1}. In general, \cdx{size} returns \isa{0} for all constructors 1.151 that do not have an argument of type $t$, and for all other constructors 1.152 \isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because 1.153 \isa{size} is defined on every datatype, it is overloaded; on lists 1.154 -\isa{size} is also called \isaindexbold{length}, which is not overloaded. 1.155 +\isa{size} is also called \sdx{length}, which is not overloaded. 1.156 Isabelle will always show \isa{size} on lists as \isa{length}. 1.157 1.158 1.159 @@ -324,7 +376,59 @@ 1.160 {\makeatother\input{Datatype/document/Nested.tex}} 1.161 1.162 1.163 -\subsection{The Limits of Nested Recursion} How far can we push nested recursion? By the unfolding argument above, we can reduce nested to mutual recursion provided the nested recursion only involves previously defined datatypes. This does not include functions: \begin{isabelle} \isacommand{datatype} t = C "t \isasymRightarrow\ bool" \end{isabelle} This declaration is a real can of worms. In HOL it must be ruled out because it requires a type \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the same cardinality --- an impossibility. For the same reason it is not possible to allow recursion involving the type \isa{set}, which is isomorphic to \isa{t \isasymFun\ bool}. Fortunately, a limited form of recursion involving function spaces is permitted: the recursive type may occur on the right of a function arrow, but never on the left. Hence the above can of worms is ruled out but the following example of a potentially infinitely branching tree is accepted: \smallskip \input{Datatype/document/Fundata.tex} \bigskip If you need nested recursion on the left of a function arrow, there are alternatives to pure HOL\@. In the Logic for Computable Functions (LCF), types like \begin{isabelle} \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" \end{isabelle} do indeed make sense~\cite{paulson87}. Note the different arrow, \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, expressing the type of \emph{continuous} functions. There is even a version of LCF on top of HOL, called HOLCF~\cite{MuellerNvOS99}. \index{*primrec|)} \index{*datatype|)} \subsection{Case Study: Tries} \label{sec:Trie} Tries are a classic search tree data structure~\cite{Knuth3-75} for fast indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and ``cat''. When searching a string in a trie, the letters of the string are examined sequentially. Each letter determines which subtrie to search next. In this case study we model tries as a datatype, define a lookup and an update function, and prove that they behave as expected. \begin{figure}[htbp] \begin{center} 1.164 +\subsection{The Limits of Nested Recursion} 1.165 + 1.166 +How far can we push nested recursion? By the unfolding argument above, we can 1.167 +reduce nested to mutual recursion provided the nested recursion only involves 1.168 +previously defined datatypes. This does not include functions: 1.169 +\begin{isabelle} 1.170 +\isacommand{datatype} t = C "t \isasymRightarrow\ bool" 1.171 +\end{isabelle} 1.172 +This declaration is a real can of worms. 1.173 +In HOL it must be ruled out because it requires a type 1.174 +\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the 1.175 +same cardinality --- an impossibility. For the same reason it is not possible 1.176 +to allow recursion involving the type \isa{set}, which is isomorphic to 1.177 +\isa{t \isasymFun\ bool}. 1.178 + 1.179 +Fortunately, a limited form of recursion 1.180 +involving function spaces is permitted: the recursive type may occur on the 1.181 +right of a function arrow, but never on the left. Hence the above can of worms 1.182 +is ruled out but the following example of a potentially infinitely branching tree is 1.183 +accepted: 1.184 +\smallskip 1.185 + 1.186 +\input{Datatype/document/Fundata.tex} 1.187 +\bigskip 1.188 + 1.189 +If you need nested recursion on the left of a function arrow, there are 1.190 +alternatives to pure HOL\@. In the Logic for Computable Functions 1.191 +(LCF), types like 1.192 +\begin{isabelle} 1.193 +\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" 1.194 +\end{isabelle} 1.195 +do indeed make sense~\cite{paulson87}. Note the different arrow, 1.196 +\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, 1.197 +expressing the type of \emph{continuous} functions. 1.198 +There is even a version of LCF on top of HOL, 1.199 +called HOLCF~\cite{MuellerNvOS99}. 1.200 + 1.201 +\index{*primrec|)} 1.202 +\index{*datatype|)} 1.203 + 1.204 +\subsection{Case Study: Tries} 1.205 +\label{sec:Trie} 1.206 + 1.207 +Tries are a classic search tree data structure~\cite{Knuth3-75} for fast 1.208 +indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a 1.209 +trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and 1.210 +``cat''. When searching a string in a trie, the letters of the string are 1.211 +examined sequentially. Each letter determines which subtrie to search next. 1.212 +In this case study we model tries as a datatype, define a lookup and an 1.213 +update function, and prove that they behave as expected. 1.214 + 1.215 +\begin{figure}[htbp] 1.216 +\begin{center} 1.217 \unitlength1mm 1.218 \begin{picture}(60,30) 1.219 \put( 5, 0){\makebox(0,0)[b]{l}} 1.220 @@ -341,7 +445,58 @@ 1.221 % 1.222 \put( 5,10){\makebox(0,0)[b]{l}} 1.223 \put(15,10){\makebox(0,0)[b]{n}} 1.224 -\put(25,10){\makebox(0,0)[b]{p}} \put(45,10){\makebox(0,0)[b]{a}} % \put(14,19){\line(-3,-2){9}} \put(15,19){\line(0,-1){5}} \put(16,19){\line(3,-2){9}} \put(45,19){\line(0,-1){5}} % \put(15,20){\makebox(0,0)[b]{a}} \put(45,20){\makebox(0,0)[b]{c}} % \put(30,30){\line(-3,-2){13}} \put(30,30){\line(3,-2){13}} \end{picture} \end{center} \caption{A sample trie} \label{fig:trie} \end{figure} Proper tries associate some value with each string. Since the information is stored only in the final node associated with the string, many nodes do not carry any value. This distinction is modeled with the help of the predefined datatype \isa{option} (see {\S}\ref{sec:option}). \input{Trie/document/Trie.tex} \section{Total Recursive Functions} \label{sec:recdef} \index{*recdef|(} Although many total functions have a natural primitive recursive definition, this is not always the case. Arbitrary total recursive functions can be defined by means of \isacommand{recdef}: you can use full pattern-matching, recursion need not involve datatypes, and termination is proved by showing that the arguments of all recursive calls are smaller in a suitable (user supplied) sense. In this section we restrict ourselves to measure functions; more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. \subsection{Defining Recursive Functions} \label{sec:recdef-examples} \input{Recdef/document/examples.tex} \subsection{Proving Termination} \input{Recdef/document/termination.tex} \subsection{Simplification with Recdef} \label{sec:recdef-simplification} \input{Recdef/document/simplification.tex} \subsection{Induction} \index{induction!recursion|(} 1.225 +\put(25,10){\makebox(0,0)[b]{p}} 1.226 +\put(45,10){\makebox(0,0)[b]{a}} 1.227 +% 1.228 +\put(14,19){\line(-3,-2){9}} 1.229 +\put(15,19){\line(0,-1){5}} 1.230 +\put(16,19){\line(3,-2){9}} 1.231 +\put(45,19){\line(0,-1){5}} 1.232 +% 1.233 +\put(15,20){\makebox(0,0)[b]{a}} 1.234 +\put(45,20){\makebox(0,0)[b]{c}} 1.235 +% 1.236 +\put(30,30){\line(-3,-2){13}} 1.237 +\put(30,30){\line(3,-2){13}} 1.238 +\end{picture} 1.239 +\end{center} 1.240 +\caption{A sample trie} 1.241 +\label{fig:trie} 1.242 +\end{figure} 1.243 + 1.244 +Proper tries associate some value with each string. Since the 1.245 +information is stored only in the final node associated with the string, many 1.246 +nodes do not carry any value. This distinction is modeled with the help 1.247 +of the predefined datatype \isa{option} (see {\S}\ref{sec:option}). 1.248 +\input{Trie/document/Trie.tex} 1.249 + 1.250 +\section{Total Recursive Functions} 1.251 +\label{sec:recdef} 1.252 +\index{*recdef|(} 1.253 + 1.254 +Although many total functions have a natural primitive recursive definition, 1.255 +this is not always the case. Arbitrary total recursive functions can be 1.256 +defined by means of \isacommand{recdef}: you can use full pattern-matching, 1.257 +recursion need not involve datatypes, and termination is proved by showing 1.258 +that the arguments of all recursive calls are smaller in a suitable (user 1.259 +supplied) sense. In this section we restrict ourselves to measure functions; 1.260 +more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. 1.261 + 1.262 +\subsection{Defining Recursive Functions} 1.263 +\label{sec:recdef-examples} 1.264 +\input{Recdef/document/examples.tex} 1.265 + 1.266 +\subsection{Proving Termination} 1.267 + 1.268 +\input{Recdef/document/termination.tex} 1.269 + 1.270 +\subsection{Simplification with Recdef} 1.271 +\label{sec:recdef-simplification} 1.272 + 1.273 +\input{Recdef/document/simplification.tex} 1.274 + 1.275 +\subsection{Induction} 1.276 +\index{induction!recursion|(} 1.277 \index{recursion induction|(} 1.278 1.279 \input{Recdef/document/Induction.tex}