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