8745

1 
(*<*)


2 
theory Fundata = Main:


3 
(*>*)


4 
datatype ('a,'i)bigtree = Tip  Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"


5 

9792

6 
text{*\noindent


7 
Parameter @{typ"'a"} is the type of values stored in


8 
the @{term"Branch"}es of the tree, whereas @{typ"'i"} is the index


9 
type over which the tree branches. If @{typ"'i"} is instantiated to


10 
@{typ"bool"}, the result is a binary tree; if it is instantiated to


11 
@{typ"nat"}, we have an infinitely branching tree because each node

8745

12 
has as many subtrees as there are natural numbers. How can we possibly

9541

13 
write down such a tree? Using functional notation! For example, the term


14 
\begin{quote}


15 
@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}


16 
\end{quote}


17 
of type @{typ"(nat,nat)bigtree"} is the tree whose

8771

18 
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and

9792

19 
has merely @{term"Tip"}s as further subtrees.

8745

20 

9792

21 
Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:

8745

22 
*}


23 


24 
consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"


25 
primrec


26 
"map_bt f Tip = Tip"


27 
"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"


28 


29 
text{*\noindent This is a valid \isacommand{primrec} definition because the

9792

30 
recursive calls of @{term"map_bt"} involve only subtrees obtained from


31 
@{term"F"}, i.e.\ the lefthand side. Thus termination is assured. The

9541

32 
seasoned functional programmer might have written @{term"map_bt f o F"}


33 
instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by

8745

34 
Isabelle because the termination proof is not as obvious since

9792

35 
@{term"map_bt"} is only partially applied.

8745

36 


37 
The following lemma has a canonical proof *}


38 

8771

39 
lemma "map_bt (g o f) T = map_bt g (map_bt f T)";

9689

40 
by(induct_tac "T", simp_all)

8745

41 


42 
text{*\noindent


43 
but it is worth taking a look at the proof state after the induction step


44 
to understand what the presence of the function type entails:

9723

45 
\begin{isabelle}

8745

46 
~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline


47 
~2.~{\isasymAnd}a~F.\isanewline


48 
~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline


49 
~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%

9723

50 
\end{isabelle}

8745

51 
*}


52 
(*<*)


53 
end


54 
(*>*)
