1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Tue Nov 07 12:20:11 2006 +0100
1.3 @@ -0,0 +1,250 @@
1.4 +(* Title: Doc/IsarAdvanced/Functions/Thy/Fundefs.thy
1.5 + ID: $Id$
1.6 + Author: Alexander Krauss, TU Muenchen
1.7 +
1.8 +Tutorial for function definitions with the new "function" package.
1.9 +*)
1.10 +
1.11 +theory Functions
1.12 +imports Main
1.13 +begin
1.14 +
1.15 +chapter {* Defining Recursive Functions in Isabelle/HOL *}
1.16 +text {* \cite{isa-tutorial} *}
1.17 +
1.18 +section {* Function Definition for Dummies *}
1.19 +
1.20 +text {*
1.21 + In most cases, defining a recursive function is just as simple as other definitions:
1.22 + *}
1.23 +
1.24 +fun fib :: "nat \<Rightarrow> nat"
1.25 +where
1.26 + "fib 0 = 1"
1.27 +| "fib (Suc 0) = 1"
1.28 +| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
1.29 +
1.30 +(*<*)termination by lexicographic_order(*>*)
1.31 +
1.32 +text {*
1.33 + The function always terminates, since the argument of gets smaller in every
1.34 + recursive call. Termination is an
1.35 + important requirement, since it prevents inconsistencies: From
1.36 + the "definition" @{text "f(n) = f(n) + 1"} we could prove
1.37 + @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.
1.38 +
1.39 + Isabelle tries to prove termination automatically when a function is
1.40 + defined. We will later look at cases where this fails and see what to
1.41 + do then.
1.42 +*}
1.43 +
1.44 +subsection {* Pattern matching *}
1.45 +
1.46 +text {*
1.47 + Like in functional programming, functions can be defined by pattern
1.48 + matching. At the moment we will only consider \emph{datatype
1.49 + patterns}, which only consist of datatype constructors and
1.50 + variables.
1.51 +
1.52 + If patterns overlap, the order of the equations is taken into
1.53 + account. The following function inserts a fixed element between any
1.54 + two elements of a list:
1.55 +*}
1.56 +
1.57 +fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.58 +where
1.59 + "sep a (x#y#xs) = x # a # sep a (y # xs)"
1.60 +| "sep a xs = xs"
1.61 +(*<*)termination by lexicographic_order(*>*)
1.62 +
1.63 +text {*
1.64 + Overlapping patterns are interpreted as "increments" to what is
1.65 + already there: The second equation is only meant for the cases where
1.66 + the first one does not match. Consequently, Isabelle replaces it
1.67 + internally by the remaining cases, making the patterns disjoint.
1.68 + This results in the equations @{thm [display] sep.simps[no_vars]}
1.69 +*}
1.70 +
1.71 +
1.72 +
1.73 +
1.74 +
1.75 +
1.76 +
1.77 +text {*
1.78 + The equations from function definitions are automatically used in
1.79 + simplification:
1.80 +*}
1.81 +
1.82 +lemma "fib (Suc (Suc 0)) = (Suc (Suc 0))"
1.83 +by simp
1.84 +
1.85 +
1.86 +
1.87 +
1.88 +subsection {* Induction *}
1.89 +
1.90 +text {* FIXME *}
1.91 +
1.92 +
1.93 +section {* If it does not work *}
1.94 +
1.95 +text {*
1.96 + Up to now, we were using the \cmd{fun} command, which provides a
1.97 + convenient shorthand notation for simple function definitions. In
1.98 + this mode, Isabelle tries to solve all the necessary proof obligations
1.99 + automatically. If a proof does not go through, the definition is
1.100 + rejected. This can mean that the definition is indeed faulty, like,
1.101 + or that the default proof procedures are not smart enough (or
1.102 + rather: not designed) to handle the specific definition.
1.103 +.
1.104 + By expanding the abbreviation to the full \cmd{function} command, the
1.105 + proof obligations become visible and can be analyzed and solved manually.
1.106 +*}
1.107 +
1.108 +(*<*)types "\<tau>" = "nat \<Rightarrow> nat"
1.109 +(*>*)
1.110 +fun f :: "\<tau>"
1.111 +where
1.112 + (*<*)"f x = x" (*>*)text {* \vspace{-0.8cm}\emph{equations} *}
1.113 +
1.114 +text {* \noindent abbreviates *}
1.115 +
1.116 +function (sequential) fo :: "\<tau>"
1.117 +where
1.118 + (*<*)"fo x = x" (*>*)txt {* \vspace{-0.8cm}\emph{equations} *}
1.119 +by pat_completeness auto
1.120 +termination by lexicographic_order
1.121 +
1.122 +text {*
1.123 + Some declarations and proofs have now become explicit:
1.124 +
1.125 + \begin{enumerate}
1.126 + \item The "sequential" option enables the preprocessing of
1.127 + pattern overlaps we already saw. Without this option, the equations
1.128 + must already be disjoint and complete. The automatic completion only
1.129 + works with datatype patterns.
1.130 +
1.131 + \item A function definition now produces a proof obligation which
1.132 + expresses completeness and compatibility of patterns (We talk about
1.133 + this later). The combination of the methods {\tt pat\_completeness} and
1.134 + {\tt auto} is used to solve this proof obligation.
1.135 +
1.136 + \item A termination proof follows the definition, started by the
1.137 + \cmd{termination} command. The {\tt lexicographic\_order} method can prove termination of a
1.138 + certain class of functions by searching for a suitable lexicographic combination of size
1.139 + measures.
1.140 + \end{enumerate}
1.141 + *}
1.142 +
1.143 +
1.144 +section {* Proving termination *}
1.145 +
1.146 +text {*
1.147 + Consider the following function, which sums up natural numbers up to
1.148 + @{text "N"}, using a counter @{text "i"}
1.149 +*}
1.150 +
1.151 +function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.152 +where
1.153 + "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
1.154 + by pat_completeness auto
1.155 +
1.156 +text {*
1.157 + The {\tt lexicographic\_order} method fails on this example, because none of the
1.158 + arguments decreases in the recursive call.
1.159 +
1.160 + A more general method for termination proofs is to supply a wellfounded
1.161 + relation on the argument type, and to show that the argument
1.162 + decreases in every recursive call.
1.163 +
1.164 + The termination argument for @{text "sum"} is based on the fact that
1.165 + the \emph{difference} between @{text "i"} and @{text "N"} gets
1.166 + smaller in every step, and that the recursion stops when @{text "i"}
1.167 + is greater then @{text "n"}. Phrased differently, the expression
1.168 + @{text "N + 1 - i"} decreases in every recursive call.
1.169 +
1.170 + We can use this expression as a measure function to construct a
1.171 + wellfounded relation, which is a proof of termination:
1.172 +*}
1.173 +
1.174 +termination
1.175 + by (auto_term "measure (\<lambda>(i,N). N + 1 - i)")
1.176 +
1.177 +text {*
1.178 + Note that the two (curried) function arguments appear as a pair in
1.179 + the measure function. The \cmd{function} command packs together curried
1.180 + arguments into a tuple to simplify its internal operation. Hence,
1.181 + measure functions and termination relations always work on the
1.182 + tupled type.
1.183 +
1.184 + Let us complicate the function a little, by adding some more recursive calls:
1.185 +*}
1.186 +
1.187 +function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.188 +where
1.189 + "foo i N = (if i > N
1.190 + then (if N = 0 then 0 else foo 0 (N - 1))
1.191 + else i + foo (Suc i) N)"
1.192 +by pat_completeness auto
1.193 +
1.194 +text {*
1.195 + When @{text "i"} has reached @{text "N"}, it starts at zero again
1.196 + and @{text "N"} is decremented.
1.197 + This corresponds to a nested
1.198 + loop where one index counts up and the other down. Termination can
1.199 + be proved using a lexicographic combination of two measures, namely
1.200 + the value of @{text "N"} and the above difference. The @{text "measures"}
1.201 + combinator generalizes @{text "measure"} by taking a list of measure functions.
1.202 +*}
1.203 +
1.204 +termination
1.205 + by (auto_term "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]")
1.206 +
1.207 +
1.208 +section {* Mutual Recursion *}
1.209 +
1.210 +text {*
1.211 + If two or more functions call one another mutually, they have to be defined
1.212 + in one step. The simplest example are probably @{text "even"} and @{text "odd"}:
1.213 +*}
1.214 +(*<*)hide const even odd(*>*)
1.215 +
1.216 +function even odd :: "nat \<Rightarrow> bool"
1.217 +where
1.218 + "even 0 = True"
1.219 +| "odd 0 = False"
1.220 +| "even (Suc n) = odd n"
1.221 +| "odd (Suc n) = even n"
1.222 + by pat_completeness auto
1.223 +
1.224 +text {*
1.225 + To solve the problem of mutual dependencies, Isabelle internally
1.226 + creates a single function operating on the sum
1.227 + type. Then the original functions are defined as
1.228 + projections. Consequently, termination has to be proved
1.229 + simultaneously for both functions, by specifying a measure on the
1.230 + sum type:
1.231 +*}
1.232 +
1.233 +termination
1.234 + by (auto_term "measure (sum_case (%n. n) (%n. n))")
1.235 +
1.236 +
1.237 +
1.238 +(* FIXME: Mutual induction *)
1.239 +
1.240 +
1.241 +
1.242 +section {* Nested recursion *}
1.243 +
1.244 +text {* FIXME *}
1.245 +
1.246 +section {* More general patterns *}
1.247 +
1.248 +text {* FIXME *}
1.249 +
1.250 +
1.251 +
1.252 +
1.253 +end