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;
 nipkow@25260  1 (*<*)  nipkow@25260  2 theory fun0 imports Main begin  nipkow@25260  3 (*>*)  nipkow@25260  4 nipkow@25260  5 text{*  nipkow@25260  6 \subsection{Definition}  nipkow@25260  7 \label{sec:fun-examples}  nipkow@25260  8 nipkow@25260  9 Here is a simple example, the \rmindex{Fibonacci function}:  nipkow@25260  10 *}  nipkow@25260  11 nipkow@25260  12 fun fib :: "nat \ nat" where  nipkow@27015  13 "fib 0 = 0" |  nipkow@27015  14 "fib (Suc 0) = 1" |  nipkow@27015  15 "fib (Suc(Suc x)) = fib x + fib (Suc x)"  nipkow@25260  16 nipkow@25260  17 text{*\noindent  nipkow@25260  18 This resembles ordinary functional programming languages. Note the obligatory  nipkow@25260  19 \isacommand{where} and \isa{|}. Command \isacommand{fun} declares and  nipkow@25260  20 defines the function in one go. Isabelle establishes termination automatically  nipkow@25260  21 because @{const fib}'s argument decreases in every recursive call.  nipkow@25260  22 nipkow@25260  23 Slightly more interesting is the insertion of a fixed element  nipkow@25260  24 between any two elements of a list:  nipkow@25260  25 *}  nipkow@25260  26 nipkow@25260  27 fun sep :: "'a \ 'a list \ 'a list" where  nipkow@27015  28 "sep a [] = []" |  nipkow@27015  29 "sep a [x] = [x]" |  wenzelm@58860  30 "sep a (x#y#zs) = x # a # sep a (y#zs)"  nipkow@25260  31 nipkow@25260  32 text{*\noindent  nipkow@25260  33 This time the length of the list decreases with the  nipkow@25260  34 recursive call; the first argument is irrelevant for termination.  nipkow@25260  35 nipkow@25260  36 Pattern matching\index{pattern matching!and \isacommand{fun}}  nipkow@25260  37 need not be exhaustive and may employ wildcards:  nipkow@25260  38 *}  nipkow@25260  39 nipkow@25260  40 fun last :: "'a list \ 'a" where  nipkow@27015  41 "last [x] = x" |  nipkow@27015  42 "last (_#y#zs) = last (y#zs)"  nipkow@25260  43 nipkow@25260  44 text{*  nipkow@25260  45 Overlapping patterns are disambiguated by taking the order of equations into  nipkow@25260  46 account, just as in functional programming:  nipkow@25260  47 *}  nipkow@25260  48 nipkow@25260  49 fun sep1 :: "'a \ 'a list \ 'a list" where  nipkow@27015  50 "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |  nipkow@27015  51 "sep1 _ xs = xs"  nipkow@25260  52 nipkow@25260  53 text{*\noindent  nipkow@25260  54 To guarantee that the second equation can only be applied if the first  nipkow@25260  55 one does not match, Isabelle internally replaces the second equation  nipkow@25260  56 by the two possibilities that are left: @{prop"sep1 a [] = []"} and  nipkow@25260  57 @{prop"sep1 a [x] = [x]"}. Thus the functions @{const sep} and  nipkow@25260  58 @{const sep1} are identical.  nipkow@25260  59 nipkow@25263  60 Because of its pattern matching syntax, \isacommand{fun} is also useful  nipkow@25260  61 for the definition of non-recursive functions:  nipkow@25260  62 *}  nipkow@25260  63 nipkow@25260  64 fun swap12 :: "'a list \ 'a list" where  nipkow@27015  65 "swap12 (x#y#zs) = y#x#zs" |  nipkow@27015  66 "swap12 zs = zs"  nipkow@25260  67 nipkow@25260  68 text{*  nipkow@25260  69 After a function~$f$ has been defined via \isacommand{fun},  nipkow@25260  70 its defining equations (or variants derived from them) are available  nipkow@25260  71 under the name $f$@{text".simps"} as theorems.  nipkow@25260  72 For example, look (via \isacommand{thm}) at  nipkow@25260  73 @{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define  nipkow@25260  74 the same function. What is more, those equations are automatically declared as  nipkow@25260  75 simplification rules.  nipkow@25260  76 nipkow@25260  77 \subsection{Termination}  nipkow@25260  78 nipkow@25260  79 Isabelle's automatic termination prover for \isacommand{fun} has a  nipkow@25260  80 fixed notion of the \emph{size} (of type @{typ nat}) of an  nipkow@25260  81 argument. The size of a natural number is the number itself. The size  nipkow@25339  82 of a list is its length. For the general case see \S\ref{sec:general-datatype}.  nipkow@25339  83 A recursive function is accepted if \isacommand{fun} can  nipkow@25260  84 show that the size of one fixed argument becomes smaller with each  nipkow@25260  85 recursive call.  nipkow@25260  86 nipkow@25261  87 More generally, \isacommand{fun} allows any \emph{lexicographic  nipkow@25260  88 combination} of size measures in case there are multiple  nipkow@25261  89 arguments. For example, the following version of \rmindex{Ackermann's  nipkow@25260  90 function} is accepted: *}  nipkow@25260  91 nipkow@25260  92 fun ack2 :: "nat \ nat \ nat" where  nipkow@27015  93 "ack2 n 0 = Suc n" |  nipkow@27015  94 "ack2 0 (Suc m) = ack2 (Suc 0) m" |  nipkow@27015  95 "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"  nipkow@25260  96 nipkow@25263  97 text{* The order of arguments has no influence on whether  nipkow@25260  98 \isacommand{fun} can prove termination of a function. For more details  wenzelm@58620  99 see elsewhere~@{cite bulwahnKN07}.  nipkow@25260  100 nipkow@25260  101 \subsection{Simplification}  nipkow@25260  102 \label{sec:fun-simplification}  nipkow@25260  103 paulson@25265  104 Upon a successful termination proof, the recursion equations become  nipkow@25260  105 simplification rules, just as with \isacommand{primrec}.  nipkow@25260  106 In most cases this works fine, but there is a subtle  nipkow@25260  107 problem that must be mentioned: simplification may not  nipkow@25260  108 terminate because of automatic splitting of @{text "if"}.  nipkow@25260  109 \index{*if expressions!splitting of}  nipkow@25260  110 Let us look at an example:  nipkow@25260  111 *}  nipkow@25260  112 nipkow@25261  113 fun gcd :: "nat \ nat \ nat" where  nipkow@27015  114 "gcd m n = (if n=0 then m else gcd n (m mod n))"  nipkow@25260  115 nipkow@25260  116 text{*\noindent  nipkow@25260  117 The second argument decreases with each recursive call.  nipkow@25260  118 The termination condition  nipkow@25260  119 @{prop[display]"n ~= (0::nat) ==> m mod n < n"}  nipkow@25260  120 is proved automatically because it is already present as a lemma in  nipkow@25260  121 HOL\@. Thus the recursion equation becomes a simplification  nipkow@25260  122 rule. Of course the equation is nonterminating if we are allowed to unfold  nipkow@25260  123 the recursive call inside the @{text else} branch, which is why programming  nipkow@25260  124 languages and our simplifier don't do that. Unfortunately the simplifier does  nipkow@25260  125 something else that leads to the same problem: it splits  nipkow@25260  126 each @{text "if"}-expression unless its  nipkow@25260  127 condition simplifies to @{term True} or @{term False}. For  nipkow@25260  128 example, simplification reduces  nipkow@25261  129 @{prop[display]"gcd m n = k"}  nipkow@25260  130 in one step to  nipkow@25261  131 @{prop[display]"(if n=0 then m else gcd n (m mod n)) = k"}  nipkow@25260  132 where the condition cannot be reduced further, and splitting leads to  nipkow@25261  133 @{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd n (m mod n)=k)"}  nipkow@25261  134 Since the recursive call @{term"gcd n (m mod n)"} is no longer protected by  nipkow@25260  135 an @{text "if"}, it is unfolded again, which leads to an infinite chain of  nipkow@25260  136 simplification steps. Fortunately, this problem can be avoided in many  nipkow@25260  137 different ways.  nipkow@25260  138 nipkow@25260  139 The most radical solution is to disable the offending theorem  nipkow@25260  140 @{thm[source]split_if},  nipkow@25260  141 as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this  nipkow@25260  142 approach: you will often have to invoke the rule explicitly when  nipkow@25260  143 @{text "if"} is involved.  nipkow@25260  144 nipkow@25260  145 If possible, the definition should be given by pattern matching on the left  nipkow@25260  146 rather than @{text "if"} on the right. In the case of @{term gcd} the  nipkow@25260  147 following alternative definition suggests itself:  nipkow@25260  148 *}  nipkow@25260  149 nipkow@25260  150 fun gcd1 :: "nat \ nat \ nat" where  nipkow@27015  151 "gcd1 m 0 = m" |  nipkow@27015  152 "gcd1 m n = gcd1 n (m mod n)"  nipkow@25260  153 nipkow@25260  154 text{*\noindent  nipkow@25260  155 The order of equations is important: it hides the side condition  nipkow@25263  156 @{prop"n ~= (0::nat)"}. Unfortunately, not all conditionals can be  nipkow@25263  157 expressed by pattern matching.  nipkow@25260  158 nipkow@25260  159 A simple alternative is to replace @{text "if"} by @{text case},  nipkow@25260  160 which is also available for @{typ bool} and is not split automatically:  nipkow@25260  161 *}  nipkow@25260  162 nipkow@25260  163 fun gcd2 :: "nat \ nat \ nat" where  nipkow@27015  164 "gcd2 m n = (case n=0 of True \ m | False \ gcd2 n (m mod n))"  nipkow@25260  165 nipkow@25260  166 text{*\noindent  nipkow@25260  167 This is probably the neatest solution next to pattern matching, and it is  nipkow@25260  168 always available.  nipkow@25260  169 nipkow@25260  170 A final alternative is to replace the offending simplification rules by  nipkow@25260  171 derived conditional ones. For @{term gcd} it means we have to prove  nipkow@25260  172 these lemmas:  nipkow@25260  173 *}  nipkow@25260  174 nipkow@25261  175 lemma [simp]: "gcd m 0 = m"  nipkow@25260  176 apply(simp)  nipkow@25260  177 done  nipkow@25260  178 nipkow@25261  179 lemma [simp]: "n \ 0 \ gcd m n = gcd n (m mod n)"  nipkow@25260  180 apply(simp)  nipkow@25260  181 done  nipkow@25260  182 nipkow@25260  183 text{*\noindent  nipkow@25260  184 Simplification terminates for these proofs because the condition of the @{text  nipkow@25260  185 "if"} simplifies to @{term True} or @{term False}.  nipkow@25260  186 Now we can disable the original simplification rule:  nipkow@25260  187 *}  nipkow@25260  188 nipkow@25260  189 declare gcd.simps [simp del]  nipkow@25260  190 nipkow@25260  191 text{*  nipkow@25260  192 \index{induction!recursion|(}  nipkow@25260  193 \index{recursion induction|(}  nipkow@25260  194 nipkow@25260  195 \subsection{Induction}  nipkow@25260  196 \label{sec:fun-induction}  nipkow@25260  197 nipkow@25260  198 Having defined a function we might like to prove something about it.  nipkow@25260  199 Since the function is recursive, the natural proof principle is  nipkow@25260  200 again induction. But this time the structural form of induction that comes  nipkow@25260  201 with datatypes is unlikely to work well --- otherwise we could have defined the  nipkow@25260  202 function by \isacommand{primrec}. Therefore \isacommand{fun} automatically  nipkow@25260  203 proves a suitable induction rule $f$@{text".induct"} that follows the  nipkow@25260  204 recursion pattern of the particular function $f$. We call this  nipkow@25260  205 \textbf{recursion induction}. Roughly speaking, it  nipkow@25260  206 requires you to prove for each \isacommand{fun} equation that the property  nipkow@25260  207 you are trying to establish holds for the left-hand side provided it holds  nipkow@25260  208 for all recursive calls on the right-hand side. Here is a simple example  nipkow@25260  209 involving the predefined @{term"map"} functional on lists:  nipkow@25260  210 *}  nipkow@25260  211 nipkow@25260  212 lemma "map f (sep x xs) = sep (f x) (map f xs)"  nipkow@25260  213 nipkow@25260  214 txt{*\noindent  nipkow@25260  215 Note that @{term"map f xs"}  nipkow@25260  216 is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove  nipkow@25260  217 this lemma by recursion induction over @{term"sep"}:  nipkow@25260  218 *}  nipkow@25260  219 wenzelm@58860  220 apply(induct_tac x xs rule: sep.induct)  nipkow@25260  221 nipkow@25260  222 txt{*\noindent  nipkow@25260  223 The resulting proof state has three subgoals corresponding to the three  nipkow@25260  224 clauses for @{term"sep"}:  nipkow@25260  225 @{subgoals[display,indent=0]}  nipkow@25260  226 The rest is pure simplification:  nipkow@25260  227 *}  nipkow@25260  228 wenzelm@58860  229 apply simp_all  nipkow@25260  230 done  nipkow@25260  231 nipkow@25263  232 text{*\noindent The proof goes smoothly because the induction rule  nipkow@25263  233 follows the recursion of @{const sep}. Try proving the above lemma by  nipkow@25263  234 structural induction, and you find that you need an additional case  nipkow@25263  235 distinction.  nipkow@25260  236 nipkow@25260  237 In general, the format of invoking recursion induction is  nipkow@25260  238 \begin{quote}  nipkow@25260  239 \isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}  nipkow@25260  240 \end{quote}\index{*induct_tac (method)}%  nipkow@25260  241 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the  nipkow@27167  242 name of a function that takes $n$ arguments. Usually the subgoal will  nipkow@25263  243 contain the term $f x@1 \dots x@n$ but this need not be the case. The  nipkow@25260  244 induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:  nipkow@25260  245 \begin{isabelle}  nipkow@25260  246 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline  nipkow@25260  247 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline  nipkow@25260  248 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline  nipkow@25260  249 {\isasymLongrightarrow}~P~u~v%  nipkow@25260  250 \end{isabelle}  nipkow@25260  251 It merely says that in order to prove a property @{term"P"} of @{term"u"} and  nipkow@25260  252 @{term"v"} you need to prove it for the three cases where @{term"v"} is the  nipkow@25260  253 empty list, the singleton list, and the list with at least two elements.  nipkow@25260  254 The final case has an induction hypothesis: you may assume that @{term"P"}  nipkow@25260  255 holds for the tail of that list.  nipkow@25260  256 \index{induction!recursion|)}  nipkow@25260  257 \index{recursion induction|)}  nipkow@25260  258 *}  nipkow@25260  259 (*<*)  nipkow@25260  260 end  nipkow@25260  261 (*>*)