5 \isadelimtheory |
5 \isadelimtheory |
6 % |
6 % |
7 \endisadelimtheory |
7 \endisadelimtheory |
8 % |
8 % |
9 \isatagtheory |
9 \isatagtheory |
|
10 \isamarkupfalse% |
10 % |
11 % |
11 \endisatagtheory |
12 \endisatagtheory |
12 {\isafoldtheory}% |
13 {\isafoldtheory}% |
13 % |
14 % |
14 \isadelimtheory |
15 \isadelimtheory |
15 % |
16 % |
16 \endisadelimtheory |
17 \endisadelimtheory |
17 \isamarkuptrue% |
|
18 % |
18 % |
19 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
20 \index{datatypes!and nested recursion}% |
20 \index{datatypes!and nested recursion}% |
21 So far, all datatypes had the property that on the right-hand side of their |
21 So far, all datatypes had the property that on the right-hand side of their |
22 definition they occurred only at the top-level: directly below a |
22 definition they occurred only at the top-level: directly below a |
23 constructor. Now we consider \emph{nested recursion}, where the recursive |
23 constructor. Now we consider \emph{nested recursion}, where the recursive |
24 datatype occurs nested in some other datatype (but not inside itself!). |
24 datatype occurs nested in some other datatype (but not inside itself!). |
25 Consider the following model of terms |
25 Consider the following model of terms |
26 where function symbols can be applied to a list of arguments:% |
26 where function symbols can be applied to a list of arguments:% |
27 \end{isamarkuptext}% |
27 \end{isamarkuptext}% |
28 \isamarkupfalse% |
28 \isamarkuptrue% |
29 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}\isamarkuptrue% |
29 \isamarkupfalse% |
30 % |
30 \isacommand{datatype}\isamarkupfalse% |
|
31 \ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequoteopen}term{\isachardoublequoteclose}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}% |
31 \begin{isamarkuptext}% |
32 \begin{isamarkuptext}% |
32 \noindent |
33 \noindent |
33 Note that we need to quote \isa{term} on the left to avoid confusion with |
34 Note that we need to quote \isa{term} on the left to avoid confusion with |
34 the Isabelle command \isacommand{term}. |
35 the Isabelle command \isacommand{term}. |
35 Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of |
36 Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of |
54 nested recursion. |
55 nested recursion. |
55 |
56 |
56 Let us define a substitution function on terms. Because terms involve term |
57 Let us define a substitution function on terms. Because terms involve term |
57 lists, we need to define two substitution functions simultaneously:% |
58 lists, we need to define two substitution functions simultaneously:% |
58 \end{isamarkuptext}% |
59 \end{isamarkuptext}% |
59 \isamarkupfalse% |
60 \isamarkuptrue% |
60 \isacommand{consts}\isanewline |
61 \isacommand{consts}\isamarkupfalse% |
61 subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\isanewline |
62 \isanewline |
62 substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}\isanewline |
63 subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequoteclose}\isanewline |
63 \isanewline |
64 substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}\isanewline |
64 \isamarkupfalse% |
65 \isanewline |
65 \isacommand{primrec}\isanewline |
66 \isacommand{primrec}\isamarkupfalse% |
66 \ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequote}\isanewline |
67 \isanewline |
|
68 \ \ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequoteclose}\isanewline |
67 \ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline |
69 \ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline |
68 \ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequote}\isanewline |
70 \ \ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequoteclose}\isanewline |
69 \isanewline |
71 \isanewline |
70 \ \ {\isachardoublequote}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
72 \ \ {\isachardoublequoteopen}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
71 \ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}\isamarkuptrue% |
73 \ \ {\isachardoublequoteopen}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequoteclose}% |
72 % |
|
73 \begin{isamarkuptext}% |
74 \begin{isamarkuptext}% |
74 \noindent |
75 \noindent |
75 Individual equations in a \commdx{primrec} definition may be |
76 Individual equations in a \commdx{primrec} definition may be |
76 named as shown for \isa{subst{\isacharunderscore}App}. |
77 named as shown for \isa{subst{\isacharunderscore}App}. |
77 The significance of this device will become apparent below. |
78 The significance of this device will become apparent below. |
79 Similarly, when proving a statement about terms inductively, we need |
80 Similarly, when proving a statement about terms inductively, we need |
80 to prove a related statement about term lists simultaneously. For example, |
81 to prove a related statement about term lists simultaneously. For example, |
81 the fact that the identity substitution does not change a term needs to be |
82 the fact that the identity substitution does not change a term needs to be |
82 strengthened and proved as follows:% |
83 strengthened and proved as follows:% |
83 \end{isamarkuptext}% |
84 \end{isamarkuptext}% |
84 \isamarkupfalse% |
85 \isamarkuptrue% |
85 \isacommand{lemma}\ subst{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline |
86 \isacommand{lemma}\isamarkupfalse% |
86 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline |
87 \ subst{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequoteopen}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline |
87 % |
88 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequoteclose}\isanewline |
88 \isadelimproof |
89 % |
89 % |
90 \isadelimproof |
90 \endisadelimproof |
91 % |
91 % |
92 \endisadelimproof |
92 \isatagproof |
93 % |
93 \isamarkupfalse% |
94 \isatagproof |
94 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
95 \isacommand{apply}\isamarkupfalse% |
95 \isamarkupfalse% |
96 {\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
96 \isacommand{done}% |
97 \isacommand{done}\isamarkupfalse% |
97 \endisatagproof |
98 % |
98 {\isafoldproof}% |
99 \endisatagproof |
99 % |
100 {\isafoldproof}% |
100 \isadelimproof |
101 % |
101 % |
102 \isadelimproof |
102 \endisadelimproof |
103 % |
103 \isamarkuptrue% |
104 \endisadelimproof |
104 % |
105 % |
105 \begin{isamarkuptext}% |
106 \begin{isamarkuptext}% |
106 \noindent |
107 \noindent |
107 Note that \isa{Var} is the identity substitution because by definition it |
108 Note that \isa{Var} is the identity substitution because by definition it |
108 leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also |
109 leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also |
136 where \isa{map} is the standard list function such that |
137 where \isa{map} is the standard list function such that |
137 \isa{map\ f\ {\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle |
138 \isa{map\ f\ {\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle |
138 insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
139 insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
139 that the suggested equation holds:% |
140 that the suggested equation holds:% |
140 \end{isamarkuptext}% |
141 \end{isamarkuptext}% |
141 % |
142 \isamarkuptrue% |
142 \isadelimproof |
143 \isamarkupfalse% |
143 % |
144 % |
144 \endisadelimproof |
145 \isadelimproof |
145 % |
146 % |
146 \isatagproof |
147 \endisadelimproof |
147 % |
148 % |
148 \endisatagproof |
149 \isatagproof |
149 {\isafoldproof}% |
150 \isamarkupfalse% |
150 % |
151 \isamarkupfalse% |
151 \isadelimproof |
152 \isamarkupfalse% |
152 % |
153 % |
153 \endisadelimproof |
154 \endisatagproof |
154 % |
155 {\isafoldproof}% |
155 \isadelimproof |
156 % |
156 % |
157 \isadelimproof |
157 \endisadelimproof |
158 % |
158 % |
159 \endisadelimproof |
159 \isatagproof |
160 \isamarkupfalse% |
160 % |
161 \isamarkupfalse% |
161 \endisatagproof |
162 \isamarkupfalse% |
162 {\isafoldproof}% |
163 % |
163 % |
164 \isadelimproof |
164 \isadelimproof |
165 % |
165 % |
166 \endisadelimproof |
166 \endisadelimproof |
167 % |
167 % |
168 \isatagproof |
168 \isadelimproof |
169 \isamarkupfalse% |
169 % |
170 \isamarkupfalse% |
170 \endisadelimproof |
171 % |
171 % |
172 \endisatagproof |
172 \isatagproof |
173 {\isafoldproof}% |
173 % |
174 % |
174 \endisatagproof |
175 \isadelimproof |
175 {\isafoldproof}% |
176 % |
176 % |
177 \endisadelimproof |
177 \isadelimproof |
178 \isamarkupfalse% |
178 \isanewline |
179 % |
179 % |
180 \isadelimproof |
180 \endisadelimproof |
181 % |
181 \isamarkupfalse% |
182 \endisadelimproof |
182 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline |
183 % |
183 % |
184 \isatagproof |
184 \isadelimproof |
185 \isamarkupfalse% |
185 % |
186 \isamarkupfalse% |
186 \endisadelimproof |
187 % |
187 % |
188 \endisatagproof |
188 \isatagproof |
189 {\isafoldproof}% |
189 \isamarkupfalse% |
190 % |
190 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
191 \isadelimproof |
191 \isamarkupfalse% |
192 \isanewline |
192 \isacommand{done}% |
193 % |
193 \endisatagproof |
194 \endisadelimproof |
194 {\isafoldproof}% |
195 \isacommand{lemma}\isamarkupfalse% |
195 % |
196 \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequoteclose}\isanewline |
196 \isadelimproof |
197 % |
197 % |
198 \isadelimproof |
198 \endisadelimproof |
199 % |
199 \isamarkuptrue% |
200 \endisadelimproof |
|
201 % |
|
202 \isatagproof |
|
203 \isacommand{apply}\isamarkupfalse% |
|
204 {\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
|
205 \isacommand{done}\isamarkupfalse% |
|
206 % |
|
207 \endisatagproof |
|
208 {\isafoldproof}% |
|
209 % |
|
210 \isadelimproof |
|
211 % |
|
212 \endisadelimproof |
200 % |
213 % |
201 \begin{isamarkuptext}% |
214 \begin{isamarkuptext}% |
202 \noindent |
215 \noindent |
203 What is more, we can now disable the old defining equation as a |
216 What is more, we can now disable the old defining equation as a |
204 simplification rule:% |
217 simplification rule:% |
205 \end{isamarkuptext}% |
218 \end{isamarkuptext}% |
206 \isamarkupfalse% |
219 \isamarkuptrue% |
207 \isacommand{declare}\ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isamarkuptrue% |
220 \isacommand{declare}\isamarkupfalse% |
208 % |
221 \ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}% |
209 \begin{isamarkuptext}% |
222 \begin{isamarkuptext}% |
210 \noindent |
223 \noindent |
211 The advantage is that now we have replaced \isa{substs} by |
224 The advantage is that now we have replaced \isa{substs} by |
212 \isa{map}, we can profit from the large number of pre-proved lemmas |
225 \isa{map}, we can profit from the large number of pre-proved lemmas |
213 about \isa{map}. Unfortunately inductive proofs about type |
226 about \isa{map}. Unfortunately inductive proofs about type |