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

added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)

(*  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)"

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"

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 can prove termination.
*}

termination 
  by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto

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 (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto


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"}:
*}

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 (relation "measure (sum_case (%n. n) (%n. n))") auto



(* FIXME: Mutual induction *)



section {* Nested recursion *}

text {* FIXME *}

section {* More general patterns *}

text {* FIXME *}




end