doc-src/IsarAdvanced/Functions/Thy/Functions.thy

+(*  Title:      Doc/IsarAdvanced/Functions/Thy/Fundefs.thy
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+Tutorial for function definitions with the new "function" package.
+*)
+
+theory Functions
+imports Main
+begin
+
+chapter {* Defining Recursive Functions in Isabelle/HOL *}
+text {* \cite{isa-tutorial} *}
+
+section {* Function Definition for Dummies *}
+
+text {*
+  In most cases, defining a recursive function is just as simple as other definitions:
+  *}
+
+fun fib :: "nat \<Rightarrow> nat"
+where
+  "fib 0 = 1"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+(*<*)termination by lexicographic_order(*>*)
+
+text {*
+  The function always terminates, since the argument of gets smaller in every
+  recursive call. Termination is an
+  important requirement, since it prevents inconsistencies: From
+  the "definition" @{text "f(n) = f(n) + 1"} we could prove 
+  @{text "0  = 1"} by subtracting @{text "f(n)"} on both sides.
+
+  Isabelle tries to prove termination automatically when a function is
+  defined. We will later look at cases where this fails and see what to
+  do then.
+*}
+
+subsection {* Pattern matching *}
+
+text {* 
+  Like in functional programming, functions can be defined by pattern
+  matching. At the moment we will only consider \emph{datatype
+  patterns}, which only consist of datatype constructors and
+  variables.
+
+  If patterns overlap, the order of the equations is taken into
+  account. The following function inserts a fixed element between any
+  two elements of a list:
+*}
+
+fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "sep a (x#y#xs) = x # a # sep a (y # xs)"
+| "sep a xs       = xs"
+(*<*)termination by lexicographic_order(*>*)
+
+text {* 
+  Overlapping patterns are interpreted as "increments" to what is
+  already there: The second equation is only meant for the cases where
+  the first one does not match. Consequently, Isabelle replaces it
+  internally by the remaining cases, making the patterns disjoint.
+  This results in the equations @{thm [display] sep.simps[no_vars]}
+*}
+
+
+
+
+
+
+
+text {* 
+  The equations from function definitions are automatically used in
+  simplification:
+*}
+
+lemma "fib (Suc (Suc 0)) = (Suc (Suc 0))"
+by simp
+
+
+  
+
+subsection {* Induction *}
+
+text {* FIXME *}
+
+
+section {* If it does not work *}
+
+text {* 
+  Up to now, we were using the \cmd{fun} command, which provides a
+  convenient shorthand notation for simple function definitions. In
+  this mode, Isabelle tries to solve all the necessary proof obligations
+  automatically. If a proof does not go through, the definition is
+  rejected. This can mean that the definition is indeed faulty, like,
+  or that the default proof procedures are not smart enough (or
+  rather: not designed) to handle the specific definition.
+.
+  By expanding the abbreviation to the full \cmd{function} command, the
+  proof obligations become visible and can be analyzed and solved manually.
+*}
+
+(*<*)types "\<tau>" = "nat \<Rightarrow> nat"
+(*>*)
+fun f :: "\<tau>"
+where
+  (*<*)"f x = x" (*>*)text {* \vspace{-0.8cm}\emph{equations} *}
+
+text {* \noindent abbreviates *}
+
+function (sequential) fo :: "\<tau>"
+where
+  (*<*)"fo x = x" (*>*)txt {* \vspace{-0.8cm}\emph{equations} *}
+by pat_completeness auto 
+termination by lexicographic_order
+
+text {* 
+  Some declarations and proofs have now become explicit:
+
+  \begin{enumerate}
+  \item The "sequential" option enables the preprocessing of
+  pattern overlaps we already saw. Without this option, the equations
+  must already be disjoint and complete. The automatic completion only
+  works with datatype patterns.
+
+  \item A function definition now produces a proof obligation which
+  expresses completeness and compatibility of patterns (We talk about
+  this later). The combination of the methods {\tt pat\_completeness} and
+  {\tt auto} is used to solve this proof obligation.
+
+  \item A termination proof follows the definition, started by the
+  \cmd{termination} command. The {\tt lexicographic\_order} method can prove termination of a
+  certain class of functions by searching for a suitable lexicographic combination of size
+  measures.
+  \end{enumerate}
+ *}
+
+
+section {* Proving termination *}
+
+text {*
+  Consider the following function, which sums up natural numbers up to
+  @{text "N"}, using a counter @{text "i"}
+*}
+
+function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
+  by pat_completeness auto
+
+text {*
+  The {\tt lexicographic\_order} method fails on this example, because none of the
+  arguments decreases in the recursive call.
+
+  A more general method for termination proofs is to supply a wellfounded
+  relation on the argument type, and to show that the argument
+  decreases in every recursive call. 
+
+  The termination argument for @{text "sum"} is based on the fact that
+  the \emph{difference} between @{text "i"} and @{text "N"} gets
+  smaller in every step, and that the recursion stops when @{text "i"}
+  is greater then @{text "n"}. Phrased differently, the expression 
+  @{text "N + 1 - i"} decreases in every recursive call.
+
+  We can use this expression as a measure function to construct a
+  wellfounded relation, which is a proof of termination:
+*}
+
+termination 
+  by (auto_term "measure (\<lambda>(i,N). N + 1 - i)")
+
+text {*
+  Note that the two (curried) function arguments appear as a pair in
+  the measure function. The \cmd{function} command packs together curried
+  arguments into a tuple to simplify its internal operation. Hence,
+  measure functions and termination relations always work on the
+  tupled type.
+
+  Let us complicate the function a little, by adding some more recursive calls:
+*}
+
+function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "foo i N = (if i > N 
+              then (if N = 0 then 0 else foo 0 (N - 1))
+              else i + foo (Suc i) N)"
+by pat_completeness auto
+
+text {*
+  When @{text "i"} has reached @{text "N"}, it starts at zero again
+  and @{text "N"} is decremented.
+  This corresponds to a nested
+  loop where one index counts up and the other down. Termination can
+  be proved using a lexicographic combination of two measures, namely
+  the value of @{text "N"} and the above difference. The @{text "measures"}
+  combinator generalizes @{text "measure"} by taking a list of measure functions.
+*}
+
+termination 
+  by (auto_term "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]")
+
+
+section {* Mutual Recursion *}
+
+text {*
+  If two or more functions call one another mutually, they have to be defined
+  in one step. The simplest example are probably @{text "even"} and @{text "odd"}:
+*}
+(*<*)hide const even odd(*>*)
+
+function even odd :: "nat \<Rightarrow> bool"
+where
+  "even 0 = True"
+| "odd 0 = False"
+| "even (Suc n) = odd n"
+| "odd (Suc n) = even n"
+  by pat_completeness auto
+
+text {*
+  To solve the problem of mutual dependencies, Isabelle internally
+  creates a single function operating on the sum
+  type. Then the original functions are defined as
+  projections. Consequently, termination has to be proved
+  simultaneously for both functions, by specifying a measure on the
+  sum type: 
+*}
+
+termination 
+  by (auto_term "measure (sum_case (%n. n) (%n. n))")
+
+
+
+(* FIXME: Mutual induction *)
+
+
+
+section {* Nested recursion *}
+
+text {* FIXME *}
+
+section {* More general patterns *}
+
+text {* FIXME *}
+
+
+
+
+end