8745
|
1 |
(*<*)
|
|
2 |
theory Fundata = Main:
|
|
3 |
(*>*)
|
9933
|
4 |
datatype ('a,'i)bigtree = Tip | Branch 'a "'i \<Rightarrow> ('a,'i)bigtree"
|
8745
|
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 |
@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
|
|
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
|
|
24 |
"map_bt f Tip = Tip"
|
9933
|
25 |
"map_bt f (Branch a F) = Branch (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 left-hand 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
|
8745
|
40 |
|
|
41 |
text{*\noindent
|
9933
|
42 |
%apply(induct_tac T);
|
|
43 |
%pr(latex xsymbols symbols)
|
8745
|
44 |
but it is worth taking a look at the proof state after the induction step
|
|
45 |
to understand what the presence of the function type entails:
|
9723
|
46 |
\begin{isabelle}
|
9933
|
47 |
\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
|
|
48 |
\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
|
|
49 |
\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
|
|
50 |
\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
|
9723
|
51 |
\end{isabelle}
|
8745
|
52 |
*}
|
|
53 |
(*<*)
|
|
54 |
end
|
|
55 |
(*>*)
|