1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Fundata}% |
3 \def\isabellecontext{Fundata}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
4 \isamarkupfalse% |
17 \isamarkupfalse% |
5 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isamarkupfalse% |
18 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isamarkuptrue% |
6 % |
19 % |
7 \begin{isamarkuptext}% |
20 \begin{isamarkuptext}% |
8 \noindent |
21 \noindent |
9 Parameter \isa{{\isacharprime}a} is the type of values stored in |
22 Parameter \isa{{\isacharprime}a} is the type of values stored in |
10 the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index |
23 the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index |
20 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
33 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
21 has merely \isa{Tip}s as further subtrees. |
34 has merely \isa{Tip}s as further subtrees. |
22 |
35 |
23 Function \isa{map{\isacharunderscore}bt} applies a function to all labels in a \isa{bigtree}:% |
36 Function \isa{map{\isacharunderscore}bt} applies a function to all labels in a \isa{bigtree}:% |
24 \end{isamarkuptext}% |
37 \end{isamarkuptext}% |
25 \isamarkuptrue% |
38 \isamarkupfalse% |
26 \isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\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{\isachardoublequote}\isanewline |
39 \isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\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{\isachardoublequote}\isanewline |
27 \isamarkupfalse% |
40 \isamarkupfalse% |
28 \isacommand{primrec}\isanewline |
41 \isacommand{primrec}\isanewline |
29 {\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline |
42 {\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline |
30 {\isachardoublequote}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}{\isachardoublequote}\isamarkupfalse% |
43 {\isachardoublequote}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}{\isachardoublequote}\isamarkuptrue% |
31 % |
44 % |
32 \begin{isamarkuptext}% |
45 \begin{isamarkuptext}% |
33 \noindent This is a valid \isacommand{primrec} definition because the |
46 \noindent This is a valid \isacommand{primrec} definition because the |
34 recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees of |
47 recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees of |
35 \isa{F}, which is itself a subterm of the left-hand side. Thus termination |
48 \isa{F}, which is itself a subterm of the left-hand side. Thus termination |
38 however will reject. Applying \isa{map{\isacharunderscore}bt} to only one of its arguments |
51 however will reject. Applying \isa{map{\isacharunderscore}bt} to only one of its arguments |
39 makes the termination proof less obvious. |
52 makes the termination proof less obvious. |
40 |
53 |
41 The following lemma has a simple proof by induction:% |
54 The following lemma has a simple proof by induction:% |
42 \end{isamarkuptext}% |
55 \end{isamarkuptext}% |
43 \isamarkuptrue% |
56 \isamarkupfalse% |
44 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline |
57 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline |
|
58 % |
|
59 \isadelimproof |
|
60 % |
|
61 \endisadelimproof |
|
62 % |
|
63 \isatagproof |
45 \isamarkupfalse% |
64 \isamarkupfalse% |
46 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
65 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
47 \isamarkupfalse% |
66 \isamarkupfalse% |
48 \isacommand{done}\isamarkupfalse% |
67 \isacommand{done}% |
49 \isamarkupfalse% |
68 \endisatagproof |
50 \isamarkupfalse% |
69 {\isafoldproof}% |
|
70 % |
|
71 \isadelimproof |
|
72 % |
|
73 \endisadelimproof |
|
74 % |
|
75 \isadelimproof |
|
76 % |
|
77 \endisadelimproof |
|
78 % |
|
79 \isatagproof |
|
80 \isamarkuptrue% |
51 % |
81 % |
52 \begin{isamarkuptxt}% |
82 \begin{isamarkuptxt}% |
53 \noindent |
83 \noindent |
54 Because of the function type, the proof state after induction looks unusual. |
84 Because of the function type, the proof state after induction looks unusual. |
55 Notice the quantified induction hypothesis: |
85 Notice the quantified induction hypothesis: |
57 \ {\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 |
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 |
58 \ {\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 |
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 |
59 \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}% |
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}% |
60 \end{isabelle}% |
90 \end{isabelle}% |
61 \end{isamarkuptxt}% |
91 \end{isamarkuptxt}% |
62 \isamarkuptrue% |
92 % |
63 \isamarkupfalse% |
93 \endisatagproof |
64 \isamarkupfalse% |
94 {\isafoldproof}% |
|
95 % |
|
96 \isadelimproof |
|
97 % |
|
98 \endisadelimproof |
|
99 % |
|
100 \isadelimtheory |
|
101 % |
|
102 \endisadelimtheory |
|
103 % |
|
104 \isatagtheory |
|
105 % |
|
106 \endisatagtheory |
|
107 {\isafoldtheory}% |
|
108 % |
|
109 \isadelimtheory |
|
110 % |
|
111 \endisadelimtheory |
65 \end{isabellebody}% |
112 \end{isabellebody}% |
66 %%% Local Variables: |
113 %%% Local Variables: |
67 %%% mode: latex |
114 %%% mode: latex |
68 %%% TeX-master: "root" |
115 %%% TeX-master: "root" |
69 %%% End: |
116 %%% End: |