src/Doc/Tutorial/Fun/fun0.thy
 author wenzelm Sat Nov 01 14:20:38 2014 +0100 (2014-11-01) changeset 58860 fee7cfa69c50 parent 58620 7435b6a3f72e child 62392 747d36865c2c permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)

     2 theory fun0 imports Main begin

     3 (*>*)

     4

     5 text{*

     6 \subsection{Definition}

     7 \label{sec:fun-examples}

     8

     9 Here is a simple example, the \rmindex{Fibonacci function}:

    10 *}

    11

    12 fun fib :: "nat \<Rightarrow> nat" where

    13 "fib 0 = 0" |

    14 "fib (Suc 0) = 1" |

    15 "fib (Suc(Suc x)) = fib x + fib (Suc x)"

    16

    17 text{*\noindent

    18 This resembles ordinary functional programming languages. Note the obligatory

    19 \isacommand{where} and \isa{|}. Command \isacommand{fun} declares and

    20 defines the function in one go. Isabelle establishes termination automatically

    21 because @{const fib}'s argument decreases in every recursive call.

    22

    23 Slightly more interesting is the insertion of a fixed element

    24 between any two elements of a list:

    25 *}

    26

    27 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

    28 "sep a []     = []" |

    29 "sep a [x]    = [x]" |

    30 "sep a (x#y#zs) = x # a # sep a (y#zs)"

    31

    32 text{*\noindent

    33 This time the length of the list decreases with the

    34 recursive call; the first argument is irrelevant for termination.

    35

    36 Pattern matching\index{pattern matching!and \isacommand{fun}}

    37 need not be exhaustive and may employ wildcards:

    38 *}

    39

    40 fun last :: "'a list \<Rightarrow> 'a" where

    41 "last [x]      = x" |

    42 "last (_#y#zs) = last (y#zs)"

    43

    44 text{*

    45 Overlapping patterns are disambiguated by taking the order of equations into

    46 account, just as in functional programming:

    47 *}

    48

    49 fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

    50 "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |

    51 "sep1 _ xs       = xs"

    52

    53 text{*\noindent

    54 To guarantee that the second equation can only be applied if the first

    55 one does not match, Isabelle internally replaces the second equation

    56 by the two possibilities that are left: @{prop"sep1 a [] = []"} and

    57 @{prop"sep1 a [x] = [x]"}.  Thus the functions @{const sep} and

    58 @{const sep1} are identical.

    59

    60 Because of its pattern matching syntax, \isacommand{fun} is also useful

    61 for the definition of non-recursive functions:

    62 *}

    63

    64 fun swap12 :: "'a list \<Rightarrow> 'a list" where

    65 "swap12 (x#y#zs) = y#x#zs" |

    66 "swap12 zs       = zs"

    67

    68 text{*

    69 After a function~$f$ has been defined via \isacommand{fun},

    70 its defining equations (or variants derived from them) are available

    71 under the name $f$@{text".simps"} as theorems.

    72 For example, look (via \isacommand{thm}) at

    73 @{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define

    74 the same function. What is more, those equations are automatically declared as

    75 simplification rules.

    76

    77 \subsection{Termination}

    78

    79 Isabelle's automatic termination prover for \isacommand{fun} has a

    80 fixed notion of the \emph{size} (of type @{typ nat}) of an

    81 argument. The size of a natural number is the number itself. The size

    82 of a list is its length. For the general case see \S\ref{sec:general-datatype}.

    83 A recursive function is accepted if \isacommand{fun} can

    84 show that the size of one fixed argument becomes smaller with each

    85 recursive call.

    86

    87 More generally, \isacommand{fun} allows any \emph{lexicographic

    88 combination} of size measures in case there are multiple

    89 arguments. For example, the following version of \rmindex{Ackermann's

    90 function} is accepted: *}

    91

    92 fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

    93 "ack2 n 0 = Suc n" |

    94 "ack2 0 (Suc m) = ack2 (Suc 0) m" |

    95 "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"

    96

    97 text{* The order of arguments has no influence on whether

    98 \isacommand{fun} can prove termination of a function. For more details

    99 see elsewhere~@{cite bulwahnKN07}.

   100

   101 \subsection{Simplification}

   102 \label{sec:fun-simplification}

   103

   104 Upon a successful termination proof, the recursion equations become

   105 simplification rules, just as with \isacommand{primrec}.

   106 In most cases this works fine, but there is a subtle

   107 problem that must be mentioned: simplification may not

   108 terminate because of automatic splitting of @{text "if"}.

   109 \index{*if expressions!splitting of}

   110 Let us look at an example:

   111 *}

   112

   113 fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   114 "gcd m n = (if n=0 then m else gcd n (m mod n))"

   115

   116 text{*\noindent

   117 The second argument decreases with each recursive call.

   118 The termination condition

   119 @{prop[display]"n ~= (0::nat) ==> m mod n < n"}

   120 is proved automatically because it is already present as a lemma in

   121 HOL\@.  Thus the recursion equation becomes a simplification

   122 rule. Of course the equation is nonterminating if we are allowed to unfold

   123 the recursive call inside the @{text else} branch, which is why programming

   124 languages and our simplifier don't do that. Unfortunately the simplifier does

   125 something else that leads to the same problem: it splits

   126 each @{text "if"}-expression unless its

   127 condition simplifies to @{term True} or @{term False}.  For

   128 example, simplification reduces

   129 @{prop[display]"gcd m n = k"}

   130 in one step to

   131 @{prop[display]"(if n=0 then m else gcd n (m mod n)) = k"}

   132 where the condition cannot be reduced further, and splitting leads to

   133 @{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd n (m mod n)=k)"}

   134 Since the recursive call @{term"gcd n (m mod n)"} is no longer protected by

   135 an @{text "if"}, it is unfolded again, which leads to an infinite chain of

   136 simplification steps. Fortunately, this problem can be avoided in many

   137 different ways.

   138

   139 The most radical solution is to disable the offending theorem

   140 @{thm[source]split_if},

   141 as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this

   142 approach: you will often have to invoke the rule explicitly when

   143 @{text "if"} is involved.

   144

   145 If possible, the definition should be given by pattern matching on the left

   146 rather than @{text "if"} on the right. In the case of @{term gcd} the

   147 following alternative definition suggests itself:

   148 *}

   149

   150 fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   151 "gcd1 m 0 = m" |

   152 "gcd1 m n = gcd1 n (m mod n)"

   153

   154 text{*\noindent

   155 The order of equations is important: it hides the side condition

   156 @{prop"n ~= (0::nat)"}.  Unfortunately, not all conditionals can be

   157 expressed by pattern matching.

   158

   159 A simple alternative is to replace @{text "if"} by @{text case},

   160 which is also available for @{typ bool} and is not split automatically:

   161 *}

   162

   163 fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   164 "gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))"

   165

   166 text{*\noindent

   167 This is probably the neatest solution next to pattern matching, and it is

   168 always available.

   169

   170 A final alternative is to replace the offending simplification rules by

   171 derived conditional ones. For @{term gcd} it means we have to prove

   172 these lemmas:

   173 *}

   174

   175 lemma [simp]: "gcd m 0 = m"

   176 apply(simp)

   177 done

   178

   179 lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"

   180 apply(simp)

   181 done

   182

   183 text{*\noindent

   184 Simplification terminates for these proofs because the condition of the @{text

   185 "if"} simplifies to @{term True} or @{term False}.

   186 Now we can disable the original simplification rule:

   187 *}

   188

   189 declare gcd.simps [simp del]

   190

   191 text{*

   192 \index{induction!recursion|(}

   193 \index{recursion induction|(}

   194

   195 \subsection{Induction}

   196 \label{sec:fun-induction}

   197

   198 Having defined a function we might like to prove something about it.

   199 Since the function is recursive, the natural proof principle is

   200 again induction. But this time the structural form of induction that comes

   201 with datatypes is unlikely to work well --- otherwise we could have defined the

   202 function by \isacommand{primrec}. Therefore \isacommand{fun} automatically

   203 proves a suitable induction rule $f$@{text".induct"} that follows the

   204 recursion pattern of the particular function $f$. We call this

   205 \textbf{recursion induction}. Roughly speaking, it

   206 requires you to prove for each \isacommand{fun} equation that the property

   207 you are trying to establish holds for the left-hand side provided it holds

   208 for all recursive calls on the right-hand side. Here is a simple example

   209 involving the predefined @{term"map"} functional on lists:

   210 *}

   211

   212 lemma "map f (sep x xs) = sep (f x) (map f xs)"

   213

   214 txt{*\noindent

   215 Note that @{term"map f xs"}

   216 is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove

   217 this lemma by recursion induction over @{term"sep"}:

   218 *}

   219

   220 apply(induct_tac x xs rule: sep.induct)

   221

   222 txt{*\noindent

   223 The resulting proof state has three subgoals corresponding to the three

   224 clauses for @{term"sep"}:

   225 @{subgoals[display,indent=0]}

   226 The rest is pure simplification:

   227 *}

   228

   229 apply simp_all

   230 done

   231

   232 text{*\noindent The proof goes smoothly because the induction rule

   233 follows the recursion of @{const sep}.  Try proving the above lemma by

   234 structural induction, and you find that you need an additional case

   235 distinction.

   236

   237 In general, the format of invoking recursion induction is

   238 \begin{quote}

   239 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}

   240 \end{quote}\index{*induct_tac (method)}%

   241 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the

   242 name of a function that takes $n$ arguments. Usually the subgoal will

   243 contain the term $f x@1 \dots x@n$ but this need not be the case. The

   244 induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:

   245 \begin{isabelle}

   246 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline

   247 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline

   248 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline

   249 {\isasymLongrightarrow}~P~u~v%

   250 \end{isabelle}

   251 It merely says that in order to prove a property @{term"P"} of @{term"u"} and

   252 @{term"v"} you need to prove it for the three cases where @{term"v"} is the

   253 empty list, the singleton list, and the list with at least two elements.

   254 The final case has an induction hypothesis:  you may assume that @{term"P"}

   255 holds for the tail of that list.

   256 \index{induction!recursion|)}

   257 \index{recursion induction|)}

   258 *}

   259 (*<*)

   260 end

   261 (*>*)