8745

1 
(*<*)


2 
theory Fundata = Main:


3 
(*>*)

10420

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

8745

5 

9792

6 
text{*\noindent


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

10420

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

9792

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

10420

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

9541

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

8771

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

9792

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

8745

18 

9792

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

8745

20 
*}


21 

9933

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

8745

23 
primrec

10420

24 
"map_bt f Tip = Tip"


25 
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"

8745

26 


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

9792

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


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

9541

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


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

8745

32 
Isabelle because the termination proof is not as obvious since

9792

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

8745

34 


35 
The following lemma has a canonical proof *}


36 

8771

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

10171

38 
apply(induct_tac T, simp_all)


39 
done

10420

40 
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";


41 
apply(induct_tac T, rename_tac[2] F)(*>*)


42 
txt{*\noindent

8745

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:

10420

45 
@{subgoals[display,indent=0]}

8745

46 
*}


47 
(*<*)

10420

48 
oops

8745

49 
end


50 
(*>*)
