summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

5 text{*

6 \subsection{Definition}

7 \label{sec:fun-examples}

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

10 *}

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)"

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.

23 Slightly more interesting is the insertion of a fixed element

24 between any two elements of a list:

25 *}

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)"

32 text{*\noindent

33 This time the length of the list decreases with the

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

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

37 need not be exhaustive and may employ wildcards:

38 *}

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

41 "last [x] = x" |

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

44 text{*

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

46 account, just as in functional programming:

47 *}

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"

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.

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

61 for the definition of non-recursive functions:

62 *}

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

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

66 "swap12 zs = zs"

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.

77 \subsection{Termination}

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.

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: *}

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"

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}.

101 \subsection{Simplification}

102 \label{sec:fun-simplification}

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 *}

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

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

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.

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.

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 *}

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

151 "gcd1 m 0 = m" |

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

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.

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 *}

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))"

166 text{*\noindent

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

168 always available.

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 *}

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

176 apply(simp)

177 done

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

180 apply(simp)

181 done

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 *}

189 declare gcd.simps [simp del]

191 text{*

192 \index{induction!recursion|(}

193 \index{recursion induction|(}

195 \subsection{Induction}

196 \label{sec:fun-induction}

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 *}

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

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 *}

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

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 *}

229 apply simp_all

230 done

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.

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