summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 12 Jan 1999 15:48:59 +0100 | |

changeset 6099 | d4866f6ff2f9 |

parent 6098 | 8648c6651f07 |

child 6100 | 40d66bc3e83f |

verbatim

--- a/doc-src/Tutorial/IsaMakefile Tue Jan 12 15:40:53 1999 +0100 +++ b/doc-src/Tutorial/IsaMakefile Tue Jan 12 15:48:59 1999 +0100 @@ -4,7 +4,7 @@ ## targets -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Misc +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Recdef HOL-Misc ## global settings @@ -89,6 +89,24 @@ Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML @$(ISATOOL) usedir $(OUT)/HOL Datatype +## HOL-Recdef + +HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz + +Recdef/Examples.thy: Recdef/exprolog Recdef/fib Recdef/sep Recdef/last \ + Recdef/constsgcd Recdef/gcd Recdef/ack + cd Recdef; cat exprolog fib sep last constsgcd gcd ack end > Examples.thy + +Recdef/Sep1.thy: Recdef/sep1prolog Recdef/sep1 + cd Recdef; cat sep1prolog sep1 end > Sep1.thy + +Recdef/Sep2.thy: Recdef/sep2prolog Recdef/sep2 + cd Recdef; cat sep2prolog sep2 end > Sep2.thy + +$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML \ + Recdef/Examples.thy Recdef/Sep1.thy Recdef/Sep2.thy + @$(ISATOOL) usedir $(OUT)/HOL Recdef + ## HOL-Misc HOL-Misc: HOL $(LOG)/HOL-Misc.gz

--- a/doc-src/Tutorial/fp.tex Tue Jan 12 15:40:53 1999 +0100 +++ b/doc-src/Tutorial/fp.tex Tue Jan 12 15:48:59 1999 +0100 @@ -1229,7 +1229,7 @@ have the following lemma about executing the concatenation of two instruction sequences: \begin{ttbox}\makeatother -\input{CodeGen/goal2.ML}\end{ttbox} +\input{CodeGen/goal1.ML}\end{ttbox} This requires induction on \texttt{xs} and ordinary simplification for the base cases. In the induction step, simplification leaves us with a formula that contains two \texttt{case}-expressions over instructions. Thus we add @@ -1247,6 +1247,9 @@ \index{*datatype|(} \index{*primrec|(} +This section presents advanced forms of \texttt{datatype}s and (in the near +future!) records. + \subsection{Mutual recursion} Sometimes it is necessary to define two datatypes that depend on each @@ -1349,7 +1352,7 @@ Although we do not recommend this unfolding to the user, this is how Isabelle deals with nested recursion internally. Strictly speaking, this information is irrelevant at the user level (and might change in the future), but it -motivates why \texttt{primrec} and induction work for nested types they way +motivates why \texttt{primrec} and induction work for nested types the way they do. We now return to the initial definition of \texttt{term} using nested recursion. @@ -1369,13 +1372,13 @@ Note that \texttt{Var} is the identity substitution because by definition it leaves variables unchanged: \texttt{subst Var (Var $x$) = Var $x$}. Note also that the type annotations are necessary because otherwise there is nothing in -the goal to enforce that both halfs of the goal talk about the same type +the goal to enforce that both halves of the goal talk about the same type parameters \texttt{('a,'b)}. As a result, induction would fail -because the two halfs of the goal would be unrelated. +because the two halves of the goal would be unrelated. \begin{exercise} -Substitution distributes over composition can be expressed roughly as -follows: +The fact that substitution distributes over composition can be expressed +roughly as follows: \begin{ttbox} subst (f o g) t = subst f (subst g t) \end{ttbox} @@ -1437,7 +1440,7 @@ \begin{ttbox} datatype t = C (t -> t) \end{ttbox} -makes enormous sense (note the intentionally different arrow \texttt{->}!). +do indeed make sense (note the intentionally different arrow \texttt{->}!). There is even a version of LCF on top of HOL, called HOLCF~\cite{MuellerNvOS98}. @@ -1491,16 +1494,16 @@ \label{fig:trie} \end{figure} -Proper tries associates some value with each string. Since the +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 captured by the following predefined datatype: \begin{ttbox} datatype 'a option = None | Some 'a -\end{ttbox} +\end{ttbox}\indexbold{*option}\indexbold{*None}\indexbold{*Some} To minimize running time, each node of a trie should contain an array that maps -letters to subtries. We have chose a more space efficient representation +letters to subtries. We have chosen a more space efficient representation where the subtries are held in an association list, i.e.\ a list of (letter,trie) pairs. Abstracting over the alphabet \texttt{'a} and the values \texttt{'v} we define a trie as follows: @@ -1603,12 +1606,7 @@ Here is a simple example, the Fibonacci function: \begin{ttbox} -consts fib :: nat => nat -recdef fib "measure(\%n. n)" - "fib 0 = 0" - "fib 1 = 1" - "fib (Suc(Suc x)) = fib x + fib (Suc x)" -\end{ttbox} +\input{Recdef/fib}\end{ttbox} The definition of \texttt{fib} is accompanied by a \bfindex{measure function} \texttt{\%n.$\;$n} that maps the argument of \texttt{fib} to a natural number. The requirement is that in each equation the measure of the argument @@ -1620,35 +1618,29 @@ Slightly more interesting is the insertion of a fixed element between any two elements of a list: \begin{ttbox} -consts sep :: "'a * 'a list => 'a list" -recdef sep "measure (\%(a,xs). length xs)" - "sep(a, []) = []" - "sep(a, [x]) = [x]" - "sep(a, x#y#zs) = x # a # sep(a,y#zs)" -\end{ttbox} +\input{Recdef/sep1}\end{ttbox} This time the measure is the length of the list, which decreases with the recursive call; the first component of the argument tuple is irrelevant. Pattern matching need not be exhaustive: \begin{ttbox} -consts last :: 'a list => bool -recdef last "measure (\%xs. length xs)" - "last [x] = x" - "last (x#y#zs) = last (y#zs)" -\end{ttbox} +\input{Recdef/last}\end{ttbox} Overlapping patterns are disambiguated by taking the order of equations into account, just as in functional programming: -v\begin{ttbox} -recdef sep "measure (\%(a,xs). length xs)" - "sep(a, x#y#zs) = x # a # sep(a,y#zs)" - "sep(a, xs) = xs" -\end{ttbox} +\begin{ttbox} +\input{Recdef/sep1}\end{ttbox} This defines exactly the same function \texttt{sep} as further above. \begin{warn} -Currently \texttt{recdef} only accepts functions with a single argument, -possibly of tuple type. + Currently \texttt{recdef} only takes the first argument of a (curried) + recursive function into account. This means both the termination measure + and pattern matching can only use that first argument. In general, you will + therefore have to combine several arguments into a tuple. In case only one + argument is relevant for termination, you can also rearrange the order of + arguments as in +\begin{ttbox} +\input{Recdef/sep2}\end{ttbox} \end{warn} When loading a theory containing a \texttt{recdef} of a function $f$, @@ -1665,9 +1657,8 @@ In general, Isabelle may not be able to prove all termination conditions automatically. For example, termination of \begin{ttbox} -consts gcd :: "nat*nat => nat" -recdef gcd "measure ((\%(m,n).n))" - "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" +\input{Recdef/constsgcd}recdef gcd "measure ((\%(m,n).n))" + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" \end{ttbox} relies on the lemma \texttt{mod_less_divisor} \begin{ttbox} @@ -1681,10 +1672,7 @@ We need to instruct \texttt{recdef} to use an extended simpset to prove the termination condition: \begin{ttbox} -recdef gcd "measure ((\%(m,n).n))" - simpset "simpset() addsimps [mod_less_divisor]" - "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" -\end{ttbox} +\input{Recdef/gcd}\end{ttbox} This time everything works fine and \texttt{gcd.rules} contains precisely the stated recursion equation for \texttt{gcd}. @@ -1698,17 +1686,14 @@ allows arbitrary wellfounded relations. For example, termination of Ackermann's function requires the lexicographic product \texttt{**}: \begin{ttbox} -recdef ack "measure(\%m. m) ** measure(\%n. n)" - "ack(0,n) = Suc n" - "ack(Suc m,0) = ack(m, 1)" - "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))" -\end{ttbox} -For details see~\cite{Isa-Logics-Man} and the examples in the library. +\input{Recdef/ack}\end{ttbox} +For details see the manual~\cite{Isa-Logics-Man} and the examples in the +library. \subsection{Deriving simplification rules} -Once we have succeeded to prove all termination conditions, we can start to +Once we have succeeded in proving all termination conditions, we can start to derive some theorems. In contrast to \texttt{primrec} definitions, which are automatically added to the simpset, \texttt{recdef} rules must be included explicitly, for example as in

--- a/doc-src/Tutorial/tutorial.ind Tue Jan 12 15:40:53 1999 +0100 +++ b/doc-src/Tutorial/tutorial.ind Tue Jan 12 15:48:59 1999 +0100 @@ -91,6 +91,11 @@ \indexspace \item {\tt nat}, 2, \bold{16} + \item {\tt None}, \bold{32} + + \indexspace + + \item {\tt option}, \bold{32} \indexspace @@ -114,6 +119,7 @@ \item {\tt simp_tac}, \bold{21} \item simplifier, \bold{19} \item simpset, \bold{20} + \item {\tt Some}, \bold{32} \indexspace

--- a/doc-src/Tutorial/tutorial.tex Tue Jan 12 15:40:53 1999 +0100 +++ b/doc-src/Tutorial/tutorial.tex Tue Jan 12 15:48:59 1999 +0100 @@ -1,5 +1,5 @@ \documentclass[11pt]{report} -\usepackage{a4,latexsym,moreverb} +\usepackage{a4,latexsym,verbatim} \usepackage{graphicx} \makeatletter @@ -54,9 +54,9 @@ \subsubsection*{Acknowledgements} This tutorial owes a lot to the constant discussions with and the valuable feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller, -Wolfgang Naraschewski, David von Oheimb, Leonor Prensa-Nieto, Cornelia Pusch -and Markus Wenzel. Stefan Merz was also kind enough to read and comment on a -draft version. +Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch +and Markus Wenzel. Stefan Berghofer and Stefan Merz were also kind enough to +read and comment on a draft version. \clearfirst \input{basics}