8745
|
1 |
(*<*)
|
|
2 |
theory Fundata = Main:
|
|
3 |
(*>*)
|
|
4 |
datatype ('a,'i)bigtree = Tip | Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"
|
|
5 |
|
|
6 |
text{*\noindent Parameter \isa{'a} is the type of values stored in
|
|
7 |
the \isa{Branch}es of the tree, whereas \isa{'i} is the index
|
|
8 |
type over which the tree branches. If \isa{'i} is instantiated to
|
|
9 |
\isa{bool}, the result is a binary tree; if it is instantiated to
|
|
10 |
\isa{nat}, we have an infinitely branching tree because each node
|
|
11 |
has as many subtrees as there are natural numbers. How can we possibly
|
|
12 |
write down such a tree? Using functional notation! For example, the *}
|
|
13 |
|
|
14 |
term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
|
|
15 |
|
|
16 |
text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
|
|
17 |
root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
|
|
18 |
has merely \isa{Tip}s as further subtrees.
|
|
19 |
|
|
20 |
Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:
|
|
21 |
*}
|
|
22 |
|
|
23 |
consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"
|
|
24 |
primrec
|
|
25 |
"map_bt f Tip = Tip"
|
|
26 |
"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"
|
|
27 |
|
|
28 |
text{*\noindent This is a valid \isacommand{primrec} definition because the
|
|
29 |
recursive calls of \isa{map_bt} involve only subtrees obtained from
|
|
30 |
\isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
|
|
31 |
seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
|
|
32 |
of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
|
|
33 |
Isabelle because the termination proof is not as obvious since
|
|
34 |
\isa{map_bt} is only partially applied.
|
|
35 |
|
|
36 |
The following lemma has a canonical proof *}
|
|
37 |
|
|
38 |
lemma "map_bt g (map_bt f T) = map_bt (g o f) T";
|
|
39 |
apply(induct_tac "T", auto).
|
|
40 |
|
|
41 |
text{*\noindent
|
|
42 |
but it is worth taking a look at the proof state after the induction step
|
|
43 |
to understand what the presence of the function type entails:
|
|
44 |
\begin{isabellepar}%
|
|
45 |
~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
|
|
46 |
~2.~{\isasymAnd}a~F.\isanewline
|
|
47 |
~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
|
|
48 |
~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
|
|
49 |
\end{isabellepar}%
|
|
50 |
*}
|
|
51 |
(*<*)
|
|
52 |
end
|
|
53 |
(*>*)
|