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