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