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