13 % |
13 % |
14 \isadelimtheory |
14 \isadelimtheory |
15 % |
15 % |
16 \endisadelimtheory |
16 \endisadelimtheory |
17 \isacommand{datatype}\isamarkupfalse% |
17 \isacommand{datatype}\isamarkupfalse% |
18 \ {\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}% |
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}% |
19 \begin{isamarkuptext}% |
20 \noindent |
20 \noindent |
21 Parameter \isa{{\isacharprime}a} is the type of values stored in |
21 Parameter \isa{{\isaliteral{27}{\isacharprime}}a} is the type of values stored in |
22 the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index |
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{{\isacharprime}i} is instantiated to |
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 |
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 |
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 |
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 |
27 write down such a tree? Using functional notation! For example, the term |
28 \begin{isabelle}% |
28 \begin{isabelle}% |
29 \ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% |
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} |
30 \end{isabelle} |
31 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose |
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 |
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. |
33 has merely \isa{Tip}s as further subtrees. |
34 |
34 |
35 Function \isa{map{\isacharunderscore}bt} applies a function to all labels in a \isa{bigtree}:% |
35 Function \isa{map{\isaliteral{5F}{\isacharunderscore}}bt} applies a function to all labels in a \isa{bigtree}:% |
36 \end{isamarkuptext}% |
36 \end{isamarkuptext}% |
37 \isamarkuptrue% |
37 \isamarkuptrue% |
38 \isacommand{primrec}\isamarkupfalse% |
38 \isacommand{primrec}\isamarkupfalse% |
39 \ 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 |
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 |
40 \isakeyword{where}\isanewline |
41 {\isachardoublequoteopen}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
41 {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ Tip\ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ Tip{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
42 {\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}% |
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}% |
43 \begin{isamarkuptext}% |
44 \noindent This is a valid \isacommand{primrec} definition because the |
44 \noindent This is a valid \isacommand{primrec} definition because the |
45 recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees of |
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 |
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 |
47 is assured. The seasoned functional programmer might try expressing |
48 \isa{{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}} as \isa{map{\isacharunderscore}bt\ f\ {\isasymcirc}\ F}, which Isabelle |
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{\isacharunderscore}bt} to only one of its arguments |
49 however will reject. Applying \isa{map{\isaliteral{5F}{\isacharunderscore}}bt} to only one of its arguments |
50 makes the termination proof less obvious. |
50 makes the termination proof less obvious. |
51 |
51 |
52 The following lemma has a simple proof by induction:% |
52 The following lemma has a simple proof by induction:% |
53 \end{isamarkuptext}% |
53 \end{isamarkuptext}% |
54 \isamarkuptrue% |
54 \isamarkuptrue% |
55 \isacommand{lemma}\isamarkupfalse% |
55 \isacommand{lemma}\isamarkupfalse% |
56 \ {\isachardoublequoteopen}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequoteclose}\isanewline |
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 % |
57 % |
58 \isadelimproof |
58 \isadelimproof |
59 % |
59 % |
60 \endisadelimproof |
60 \endisadelimproof |
61 % |
61 % |
62 \isatagproof |
62 \isatagproof |
63 \isacommand{apply}\isamarkupfalse% |
63 \isacommand{apply}\isamarkupfalse% |
64 {\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
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% |
65 \isacommand{done}\isamarkupfalse% |
66 % |
66 % |
67 \endisatagproof |
67 \endisatagproof |
68 {\isafoldproof}% |
68 {\isafoldproof}% |
69 % |
69 % |