1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Nested}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \index{datatypes!and nested recursion}% |
|
20 So far, all datatypes had the property that on the right-hand side of their |
|
21 definition they occurred only at the top-level: directly below a |
|
22 constructor. Now we consider \emph{nested recursion}, where the recursive |
|
23 datatype occurs nested in some other datatype (but not inside itself!). |
|
24 Consider the following model of terms |
|
25 where function symbols can be applied to a list of arguments:% |
|
26 \end{isamarkuptext}% |
|
27 \isamarkuptrue% |
|
28 \isacommand{datatype}\isamarkupfalse% |
|
29 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{22}{\isachardoublequoteclose}}% |
|
30 \begin{isamarkuptext}% |
|
31 \noindent |
|
32 Note that we need to quote \isa{term} on the left to avoid confusion with |
|
33 the Isabelle command \isacommand{term}. |
|
34 Parameter \isa{{\isaliteral{27}{\isacharprime}}v} is the type of variables and \isa{{\isaliteral{27}{\isacharprime}}f} the type of |
|
35 function symbols. |
|
36 A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isaliteral{5B}{\isacharbrackleft}}Var\ x{\isaliteral{2C}{\isacharcomma}}\ App\ g\ {\isaliteral{5B}{\isacharbrackleft}}Var\ y{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are |
|
37 suitable values, e.g.\ numbers or strings. |
|
38 |
|
39 What complicates the definition of \isa{term} is the nested occurrence of |
|
40 \isa{term} inside \isa{list} on the right-hand side. In principle, |
|
41 nested recursion can be eliminated in favour of mutual recursion by unfolding |
|
42 the offending datatypes, here \isa{list}. The result for \isa{term} |
|
43 would be something like |
|
44 \medskip |
|
45 |
|
46 \input{Datatype/document/unfoldnested.tex} |
|
47 \medskip |
|
48 |
|
49 \noindent |
|
50 Although we do not recommend this unfolding to the user, it shows how to |
|
51 simulate nested recursion by mutual recursion. |
|
52 Now we return to the initial definition of \isa{term} using |
|
53 nested recursion. |
|
54 |
|
55 Let us define a substitution function on terms. Because terms involve term |
|
56 lists, we need to define two substitution functions simultaneously:% |
|
57 \end{isamarkuptext}% |
|
58 \isamarkuptrue% |
|
59 \isacommand{primrec}\isamarkupfalse% |
|
60 \isanewline |
|
61 subst\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ \ \ \ \ \ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline |
|
62 substs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
63 \isakeyword{where}\isanewline |
|
64 {\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ s\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
65 \ \ subst{\isaliteral{5F}{\isacharunderscore}}App{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
66 {\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}substs\ s\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
67 \isanewline |
|
68 {\isaliteral{22}{\isachardoublequoteopen}}substs\ s\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
69 {\isaliteral{22}{\isachardoublequoteopen}}substs\ s\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{23}{\isacharhash}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ subst\ s\ t\ {\isaliteral{23}{\isacharhash}}\ substs\ s\ ts{\isaliteral{22}{\isachardoublequoteclose}}% |
|
70 \begin{isamarkuptext}% |
|
71 \noindent |
|
72 Individual equations in a \commdx{primrec} definition may be |
|
73 named as shown for \isa{subst{\isaliteral{5F}{\isacharunderscore}}App}. |
|
74 The significance of this device will become apparent below. |
|
75 |
|
76 Similarly, when proving a statement about terms inductively, we need |
|
77 to prove a related statement about term lists simultaneously. For example, |
|
78 the fact that the identity substitution does not change a term needs to be |
|
79 strengthened and proved as follows:% |
|
80 \end{isamarkuptext}% |
|
81 \isamarkuptrue% |
|
82 \isacommand{lemma}\isamarkupfalse% |
|
83 \ subst{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst\ \ Var\ t\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline |
|
84 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}ts{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
85 % |
|
86 \isadelimproof |
|
87 % |
|
88 \endisadelimproof |
|
89 % |
|
90 \isatagproof |
|
91 \isacommand{apply}\isamarkupfalse% |
|
92 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ t\ \isakeyword{and}\ ts{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline |
|
93 \isacommand{done}\isamarkupfalse% |
|
94 % |
|
95 \endisatagproof |
|
96 {\isafoldproof}% |
|
97 % |
|
98 \isadelimproof |
|
99 % |
|
100 \endisadelimproof |
|
101 % |
|
102 \begin{isamarkuptext}% |
|
103 \noindent |
|
104 Note that \isa{Var} is the identity substitution because by definition it |
|
105 leaves variables unchanged: \isa{subst\ Var\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ x}. Note also |
|
106 that the type annotations are necessary because otherwise there is nothing in |
|
107 the goal to enforce that both halves of the goal talk about the same type |
|
108 parameters \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}}. As a result, induction would fail |
|
109 because the two halves of the goal would be unrelated. |
|
110 |
|
111 \begin{exercise} |
|
112 The fact that substitution distributes over composition can be expressed |
|
113 roughly as follows: |
|
114 \begin{isabelle}% |
|
115 \ \ \ \ \ subst\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ g{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ subst\ f\ {\isaliteral{28}{\isacharparenleft}}subst\ g\ t{\isaliteral{29}{\isacharparenright}}% |
|
116 \end{isabelle} |
|
117 Correct this statement (you will find that it does not type-check), |
|
118 strengthen it, and prove it. (Note: \isa{{\isaliteral{5C3C636972633E}{\isasymcirc}}} is function composition; |
|
119 its definition is found in theorem \isa{o{\isaliteral{5F}{\isacharunderscore}}def}). |
|
120 \end{exercise} |
|
121 \begin{exercise}\label{ex:trev-trev} |
|
122 Define a function \isa{trev} of type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}\ Nested{\isaliteral{2E}{\isachardot}}term\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}\ Nested{\isaliteral{2E}{\isachardot}}term} |
|
123 that recursively reverses the order of arguments of all function symbols in a |
|
124 term. Prove that \isa{trev\ {\isaliteral{28}{\isacharparenleft}}trev\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ t}. |
|
125 \end{exercise} |
|
126 |
|
127 The experienced functional programmer may feel that our definition of |
|
128 \isa{subst} is too complicated in that \isa{substs} is |
|
129 unnecessary. The \isa{App}-case can be defined directly as |
|
130 \begin{isabelle}% |
|
131 \ \ \ \ \ subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}subst\ s{\isaliteral{29}{\isacharparenright}}\ ts{\isaliteral{29}{\isacharparenright}}% |
|
132 \end{isabelle} |
|
133 where \isa{map} is the standard list function such that |
|
134 \isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}xn{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}f\ x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}f\ xn{\isaliteral{5D}{\isacharbrackright}}}. This is true, but Isabelle |
|
135 insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
|
136 that the suggested equation holds:% |
|
137 \end{isamarkuptext}% |
|
138 \isamarkuptrue% |
|
139 % |
|
140 \isadelimproof |
|
141 % |
|
142 \endisadelimproof |
|
143 % |
|
144 \isatagproof |
|
145 % |
|
146 \endisatagproof |
|
147 {\isafoldproof}% |
|
148 % |
|
149 \isadelimproof |
|
150 % |
|
151 \endisadelimproof |
|
152 % |
|
153 \isadelimproof |
|
154 % |
|
155 \endisadelimproof |
|
156 % |
|
157 \isatagproof |
|
158 % |
|
159 \endisatagproof |
|
160 {\isafoldproof}% |
|
161 % |
|
162 \isadelimproof |
|
163 % |
|
164 \endisadelimproof |
|
165 % |
|
166 \isadelimproof |
|
167 % |
|
168 \endisadelimproof |
|
169 % |
|
170 \isatagproof |
|
171 % |
|
172 \endisatagproof |
|
173 {\isafoldproof}% |
|
174 % |
|
175 \isadelimproof |
|
176 \isanewline |
|
177 % |
|
178 \endisadelimproof |
|
179 \isacommand{lemma}\isamarkupfalse% |
|
180 \ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}subst\ s{\isaliteral{29}{\isacharparenright}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
181 % |
|
182 \isadelimproof |
|
183 % |
|
184 \endisadelimproof |
|
185 % |
|
186 \isatagproof |
|
187 \isacommand{apply}\isamarkupfalse% |
|
188 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ ts{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline |
|
189 \isacommand{done}\isamarkupfalse% |
|
190 % |
|
191 \endisatagproof |
|
192 {\isafoldproof}% |
|
193 % |
|
194 \isadelimproof |
|
195 % |
|
196 \endisadelimproof |
|
197 % |
|
198 \begin{isamarkuptext}% |
|
199 \noindent |
|
200 What is more, we can now disable the old defining equation as a |
|
201 simplification rule:% |
|
202 \end{isamarkuptext}% |
|
203 \isamarkuptrue% |
|
204 \isacommand{declare}\isamarkupfalse% |
|
205 \ subst{\isaliteral{5F}{\isacharunderscore}}App\ {\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}% |
|
206 \begin{isamarkuptext}% |
|
207 \noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of |
|
208 pre-proved lemmas about \isa{map}. Unfortunately, inductive proofs |
|
209 about type \isa{term} are still awkward because they expect a |
|
210 conjunction. One could derive a new induction principle as well (see |
|
211 \S\ref{sec:derive-ind}), but simpler is to stop using |
|
212 \isacommand{primrec} and to define functions with \isacommand{fun} |
|
213 instead. Simple uses of \isacommand{fun} are described in |
|
214 \S\ref{sec:fun} below. Advanced applications, including functions |
|
215 over nested datatypes like \isa{term}, are discussed in a |
|
216 separate tutorial~\cite{isabelle-function}. |
|
217 |
|
218 Of course, you may also combine mutual and nested recursion of datatypes. For example, |
|
219 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
|
220 expressions as its argument: \isa{Sum}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp\ list{\isaliteral{22}{\isachardoublequote}}}.% |
|
221 \end{isamarkuptext}% |
|
222 \isamarkuptrue% |
|
223 % |
|
224 \isadelimtheory |
|
225 % |
|
226 \endisadelimtheory |
|
227 % |
|
228 \isatagtheory |
|
229 % |
|
230 \endisatagtheory |
|
231 {\isafoldtheory}% |
|
232 % |
|
233 \isadelimtheory |
|
234 % |
|
235 \endisadelimtheory |
|
236 \end{isabellebody}% |
|
237 %%% Local Variables: |
|
238 %%% mode: latex |
|
239 %%% TeX-master: "root" |
|
240 %%% End: |
|