9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{Fundata}%
|
17181
|
4 |
\isamarkupfalse%
|
17056
|
5 |
%
|
|
6 |
\isadelimtheory
|
|
7 |
%
|
|
8 |
\endisadelimtheory
|
|
9 |
%
|
|
10 |
\isatagtheory
|
|
11 |
%
|
|
12 |
\endisatagtheory
|
|
13 |
{\isafoldtheory}%
|
|
14 |
%
|
|
15 |
\isadelimtheory
|
|
16 |
%
|
|
17 |
\endisadelimtheory
|
17175
|
18 |
\isacommand{datatype}\isamarkupfalse%
|
|
19 |
\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequoteclose}%
|
8749
|
20 |
\begin{isamarkuptext}%
|
9792
|
21 |
\noindent
|
|
22 |
Parameter \isa{{\isacharprime}a} is the type of values stored in
|
10420
|
23 |
the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index
|
9792
|
24 |
type over which the tree branches. If \isa{{\isacharprime}i} is instantiated to
|
8749
|
25 |
\isa{bool}, the result is a binary tree; if it is instantiated to
|
|
26 |
\isa{nat}, we have an infinitely branching tree because each node
|
|
27 |
has as many subtrees as there are natural numbers. How can we possibly
|
9541
|
28 |
write down such a tree? Using functional notation! For example, the term
|
|
29 |
\begin{isabelle}%
|
12627
|
30 |
\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
|
9924
|
31 |
\end{isabelle}
|
9673
|
32 |
of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
|
8771
|
33 |
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
|
8749
|
34 |
has merely \isa{Tip}s as further subtrees.
|
|
35 |
|
9792
|
36 |
Function \isa{map{\isacharunderscore}bt} applies a function to all labels in a \isa{bigtree}:%
|
8749
|
37 |
\end{isamarkuptext}%
|
17175
|
38 |
\isamarkuptrue%
|
|
39 |
\isacommand{consts}\isamarkupfalse%
|
|
40 |
\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequoteclose}\isanewline
|
|
41 |
\isacommand{primrec}\isamarkupfalse%
|
|
42 |
\isanewline
|
|
43 |
{\isachardoublequoteopen}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequoteclose}\isanewline
|
|
44 |
{\isachardoublequoteopen}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ Br\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
|
8749
|
45 |
\begin{isamarkuptext}%
|
|
46 |
\noindent This is a valid \isacommand{primrec} definition because the
|
14188
|
47 |
recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees of
|
|
48 |
\isa{F}, which is itself a subterm of the left-hand side. Thus termination
|
|
49 |
is assured. The seasoned functional programmer might try expressing
|
11458
|
50 |
\isa{{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}} as \isa{map{\isacharunderscore}bt\ f\ {\isasymcirc}\ F}, which Isabelle
|
|
51 |
however will reject. Applying \isa{map{\isacharunderscore}bt} to only one of its arguments
|
|
52 |
makes the termination proof less obvious.
|
8749
|
53 |
|
11309
|
54 |
The following lemma has a simple proof by induction:%
|
8749
|
55 |
\end{isamarkuptext}%
|
17175
|
56 |
\isamarkuptrue%
|
|
57 |
\isacommand{lemma}\isamarkupfalse%
|
|
58 |
\ {\isachardoublequoteopen}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
59 |
%
|
|
60 |
\isadelimproof
|
|
61 |
%
|
|
62 |
\endisadelimproof
|
|
63 |
%
|
|
64 |
\isatagproof
|
|
65 |
\isacommand{apply}\isamarkupfalse%
|
|
66 |
{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
|
|
67 |
\isacommand{done}\isamarkupfalse%
|
|
68 |
%
|
|
69 |
\endisatagproof
|
|
70 |
{\isafoldproof}%
|
|
71 |
%
|
|
72 |
\isadelimproof
|
|
73 |
%
|
|
74 |
\endisadelimproof
|
17056
|
75 |
%
|
|
76 |
\isadelimproof
|
|
77 |
%
|
|
78 |
\endisadelimproof
|
|
79 |
%
|
|
80 |
\isatagproof
|
16069
|
81 |
%
|
|
82 |
\begin{isamarkuptxt}%
|
|
83 |
\noindent
|
|
84 |
Because of the function type, the proof state after induction looks unusual.
|
|
85 |
Notice the quantified induction hypothesis:
|
|
86 |
\begin{isabelle}%
|
|
87 |
\ {\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
|
|
88 |
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ {\isacharparenleft}{\isasymAnd}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}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
|
|
89 |
\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ }map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}{\isacharparenright}%
|
|
90 |
\end{isabelle}%
|
|
91 |
\end{isamarkuptxt}%
|
17175
|
92 |
\isamarkuptrue%
|
17056
|
93 |
%
|
|
94 |
\endisatagproof
|
|
95 |
{\isafoldproof}%
|
|
96 |
%
|
|
97 |
\isadelimproof
|
|
98 |
%
|
|
99 |
\endisadelimproof
|
|
100 |
%
|
|
101 |
\isadelimtheory
|
|
102 |
%
|
|
103 |
\endisadelimtheory
|
|
104 |
%
|
|
105 |
\isatagtheory
|
|
106 |
%
|
|
107 |
\endisatagtheory
|
|
108 |
{\isafoldtheory}%
|
|
109 |
%
|
|
110 |
\isadelimtheory
|
|
111 |
%
|
|
112 |
\endisadelimtheory
|
9722
|
113 |
\end{isabellebody}%
|
9145
|
114 |
%%% Local Variables:
|
|
115 |
%%% mode: latex
|
|
116 |
%%% TeX-master: "root"
|
|
117 |
%%% End:
|