(*<*)

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. In general, every datatype @{text t} comes

with its own size function (named @{text"t.size"}) which counts the

number of constructors in a term of type @{text t} --- more precisely

those constructors where one of the arguments is of the type itself:

@{const Suc} in the case of @{typ nat} and @{const "op #"} in the case

of lists. 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 an $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

(*>*)