diff -r f51d4a302962 -r 5386df44a037 src/Doc/Tutorial/Fun/fun0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/Fun/fun0.thy	Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,261 @@
+(*<*)
+theory fun0 imports Main begin
+(*>*)
+
+text{*
+\subsection{Definition}
+\label{sec:fun-examples}
+
+Here is a simple example, the \rmindex{Fibonacci function}:
+*}
+
+fun fib :: "nat \<Rightarrow> nat" where
+"fib 0 = 0" |
+"fib (Suc 0) = 1" |
+"fib (Suc(Suc x)) = fib x + fib (Suc x)"
+
+text{*\noindent
+This resembles ordinary functional programming languages. Note the obligatory
+\isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
+defines the function in one go. Isabelle establishes termination automatically
+because @{const fib}'s argument decreases in every recursive call.
+
+Slightly more interesting is the insertion of a fixed element
+between any two elements of a list:
+*}
+
+fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"sep a []     = []" |
+"sep a [x]    = [x]" |
+"sep a (x#y#zs) = x # a # sep a (y#zs)";
+
+text{*\noindent
+This time the length of the list decreases with the
+recursive call; the first argument is irrelevant for termination.
+
+Pattern matching\index{pattern matching!and \isacommand{fun}}
+need not be exhaustive and may employ wildcards:
+*}
+
+fun last :: "'a list \<Rightarrow> 'a" where
+"last [x]      = x" |
+"last (_#y#zs) = last (y#zs)"
+
+text{*
+Overlapping patterns are disambiguated by taking the order of equations into
+account, just as in functional programming:
+*}
+
+fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
+"sep1 _ xs       = xs"
+
+text{*\noindent
+To guarantee that the second equation can only be applied if the first
+one does not match, Isabelle internally replaces the second equation
+by the two possibilities that are left: @{prop"sep1 a [] = []"} and
+@{prop"sep1 a [x] = [x]"}.  Thus the functions @{const sep} and
+@{const sep1} are identical.
+
+Because of its pattern matching syntax, \isacommand{fun} is also useful
+for the definition of non-recursive functions:
+*}
+
+fun swap12 :: "'a list \<Rightarrow> 'a list" where
+"swap12 (x#y#zs) = y#x#zs" |
+"swap12 zs       = zs"
+
+text{*
+After a function~$f$ has been defined via \isacommand{fun},
+its defining equations (or variants derived from them) are available
+under the name $f$@{text".simps"} as theorems.
+For example, look (via \isacommand{thm}) at
+@{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
+the same function. What is more, those equations are automatically declared as
+simplification rules.
+
+\subsection{Termination}
+
+Isabelle's automatic termination prover for \isacommand{fun} has a
+fixed notion of the \emph{size} (of type @{typ nat}) of an
+argument. The size of a natural number is the number itself. The size
+of a list is its length. For the general case see \S\ref{sec:general-datatype}.
+A recursive function is accepted if \isacommand{fun} can
+show that the size of one fixed argument becomes smaller with each
+recursive call.
+
+More generally, \isacommand{fun} allows any \emph{lexicographic
+combination} of size measures in case there are multiple
+arguments. For example, the following version of \rmindex{Ackermann's
+function} is accepted: *}
+
+fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"ack2 n 0 = Suc n" |
+"ack2 0 (Suc m) = ack2 (Suc 0) m" |
+"ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
+
+text{* The order of arguments has no influence on whether
+\isacommand{fun} can prove termination of a function. For more details
+see elsewhere~\cite{bulwahnKN07}.
+
+\subsection{Simplification}
+\label{sec:fun-simplification}
+
+Upon a successful termination proof, the recursion equations become
+simplification rules, just as with \isacommand{primrec}.
+In most cases this works fine, but there is a subtle
+problem that must be mentioned: simplification may not
+terminate because of automatic splitting of @{text "if"}.
+\index{*if expressions!splitting of}
+Let us look at an example:
+*}
+
+fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"gcd m n = (if n=0 then m else gcd n (m mod n))"
+
+text{*\noindent
+The second argument decreases with each recursive call.
+The termination condition
+@{prop[display]"n ~= (0::nat) ==> m mod n < n"}
+is proved automatically because it is already present as a lemma in
+HOL\@.  Thus the recursion equation becomes a simplification
+rule. Of course the equation is nonterminating if we are allowed to unfold
+the recursive call inside the @{text else} branch, which is why programming
+languages and our simplifier don't do that. Unfortunately the simplifier does
+something else that leads to the same problem: it splits 
+each @{text "if"}-expression unless its
+condition simplifies to @{term True} or @{term False}.  For
+example, simplification reduces
+@{prop[display]"gcd m n = k"}
+in one step to
+@{prop[display]"(if n=0 then m else gcd n (m mod n)) = k"}
+where the condition cannot be reduced further, and splitting leads to
+@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd n (m mod n)=k)"}
+Since the recursive call @{term"gcd n (m mod n)"} is no longer protected by
+an @{text "if"}, it is unfolded again, which leads to an infinite chain of
+simplification steps. Fortunately, this problem can be avoided in many
+different ways.
+
+The most radical solution is to disable the offending theorem
+@{thm[source]split_if},
+as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
+approach: you will often have to invoke the rule explicitly when
+@{text "if"} is involved.
+
+If possible, the definition should be given by pattern matching on the left
+rather than @{text "if"} on the right. In the case of @{term gcd} the
+following alternative definition suggests itself:
+*}
+
+fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"gcd1 m 0 = m" |
+"gcd1 m n = gcd1 n (m mod n)"
+
+text{*\noindent
+The order of equations is important: it hides the side condition
+@{prop"n ~= (0::nat)"}.  Unfortunately, not all conditionals can be
+expressed by pattern matching.
+
+A simple alternative is to replace @{text "if"} by @{text case}, 
+which is also available for @{typ bool} and is not split automatically:
+*}
+
+fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))"
+
+text{*\noindent
+This is probably the neatest solution next to pattern matching, and it is
+always available.
+
+A final alternative is to replace the offending simplification rules by
+derived conditional ones. For @{term gcd} it means we have to prove
+these lemmas:
+*}
+
+lemma [simp]: "gcd m 0 = m"
+apply(simp)
+done
+
+lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
+apply(simp)
+done
+
+text{*\noindent
+Simplification terminates for these proofs because the condition of the @{text
+"if"} simplifies to @{term True} or @{term False}.
+Now we can disable the original simplification rule:
+*}
+
+declare gcd.simps [simp del]
+
+text{*
+\index{induction!recursion|(}
+\index{recursion induction|(}
+
+\subsection{Induction}
+\label{sec:fun-induction}
+
+Having defined a function we might like to prove something about it.
+Since the function is recursive, the natural proof principle is
+again induction. But this time the structural form of induction that comes
+with datatypes is unlikely to work well --- otherwise we could have defined the
+function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
+proves a suitable induction rule $f$@{text".induct"} that follows the
+recursion pattern of the particular function $f$. We call this
+\textbf{recursion induction}. Roughly speaking, it
+requires you to prove for each \isacommand{fun} equation that the property
+you are trying to establish holds for the left-hand side provided it holds
+for all recursive calls on the right-hand side. Here is a simple example
+involving the predefined @{term"map"} functional on lists:
+*}
+
+lemma "map f (sep x xs) = sep (f x) (map f xs)"
+
+txt{*\noindent
+Note that @{term"map f xs"}
+is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
+this lemma by recursion induction over @{term"sep"}:
+*}
+
+apply(induct_tac x xs rule: sep.induct);
+
+txt{*\noindent
+The resulting proof state has three subgoals corresponding to the three
+clauses for @{term"sep"}:
+@{subgoals[display,indent=0]}
+The rest is pure simplification:
+*}
+
+apply simp_all;
+done
+
+text{*\noindent The proof goes smoothly because the induction rule
+follows the recursion of @{const sep}.  Try proving the above lemma by
+structural induction, and you find that you need an additional case
+distinction.
+
+In general, the format of invoking recursion induction is
+\begin{quote}
+\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
+\end{quote}\index{*induct_tac (method)}%
+where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
+name of a function that takes $n$ arguments. Usually the subgoal will
+contain the term $f x@1 \dots x@n$ but this need not be the case. The
+induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
+\begin{isabelle}
+{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
+~~{\isasymAnd}a~x.~P~a~[x];\isanewline
+~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}~P~u~v%
+\end{isabelle}
+It merely says that in order to prove a property @{term"P"} of @{term"u"} and
+@{term"v"} you need to prove it for the three cases where @{term"v"} is the
+empty list, the singleton list, and the list with at least two elements.
+The final case has an induction hypothesis:  you may assume that @{term"P"}
+holds for the tail of that list.
+\index{induction!recursion|)}
+\index{recursion induction|)}
+*}
+(*<*)
+end
+(*>*)