|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{List{\isacharunderscore}Prefix}% |
|
4 % |
|
5 \isamarkupheader{List prefixes and postfixes% |
|
6 } |
|
7 \isamarkuptrue% |
|
8 % |
|
9 \isadelimtheory |
|
10 % |
|
11 \endisadelimtheory |
|
12 % |
|
13 \isatagtheory |
|
14 \isacommand{theory}\isamarkupfalse% |
|
15 \ List{\isacharunderscore}Prefix\isanewline |
|
16 \isakeyword{imports}\ List\ Main\isanewline |
|
17 \isakeyword{begin}% |
|
18 \endisatagtheory |
|
19 {\isafoldtheory}% |
|
20 % |
|
21 \isadelimtheory |
|
22 % |
|
23 \endisadelimtheory |
|
24 % |
|
25 \isamarkupsubsection{Prefix order on lists% |
|
26 } |
|
27 \isamarkuptrue% |
|
28 \isacommand{instantiation}\isamarkupfalse% |
|
29 \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ order\isanewline |
|
30 \isakeyword{begin}\isanewline |
|
31 \isanewline |
|
32 \isacommand{definition}\isamarkupfalse% |
|
33 \isanewline |
|
34 \ \ prefix{\isacharunderscore}def\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
35 \isanewline |
|
36 \isacommand{definition}\isamarkupfalse% |
|
37 \isanewline |
|
38 \ \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys\ {\isacharequal}\ {\isacharparenleft}xs\ {\isasymle}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
39 \isanewline |
|
40 \isacommand{instance}\isamarkupfalse% |
|
41 \isanewline |
|
42 % |
|
43 \isadelimproof |
|
44 \ \ % |
|
45 \endisadelimproof |
|
46 % |
|
47 \isatagproof |
|
48 \isacommand{by}\isamarkupfalse% |
|
49 \ intro{\isacharunderscore}classes\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def\ strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharparenright}% |
|
50 \endisatagproof |
|
51 {\isafoldproof}% |
|
52 % |
|
53 \isadelimproof |
|
54 \isanewline |
|
55 % |
|
56 \endisadelimproof |
|
57 \isanewline |
|
58 \isacommand{end}\isamarkupfalse% |
|
59 \isanewline |
|
60 \isanewline |
|
61 \isacommand{lemma}\isamarkupfalse% |
|
62 \ prefixI\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ zs\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
63 % |
|
64 \isadelimproof |
|
65 \ \ % |
|
66 \endisadelimproof |
|
67 % |
|
68 \isatagproof |
|
69 \isacommand{unfolding}\isamarkupfalse% |
|
70 \ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
71 \ blast% |
|
72 \endisatagproof |
|
73 {\isafoldproof}% |
|
74 % |
|
75 \isadelimproof |
|
76 \isanewline |
|
77 % |
|
78 \endisadelimproof |
|
79 \isanewline |
|
80 \isacommand{lemma}\isamarkupfalse% |
|
81 \ prefixE\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline |
|
82 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
83 \ \ \isakeyword{obtains}\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isachardoublequoteclose}\isanewline |
|
84 % |
|
85 \isadelimproof |
|
86 \ \ % |
|
87 \endisadelimproof |
|
88 % |
|
89 \isatagproof |
|
90 \isacommand{using}\isamarkupfalse% |
|
91 \ assms\ \isacommand{unfolding}\isamarkupfalse% |
|
92 \ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
93 \ blast% |
|
94 \endisatagproof |
|
95 {\isafoldproof}% |
|
96 % |
|
97 \isadelimproof |
|
98 \isanewline |
|
99 % |
|
100 \endisadelimproof |
|
101 \isanewline |
|
102 \isacommand{lemma}\isamarkupfalse% |
|
103 \ strict{\isacharunderscore}prefixI{\isacharprime}\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ z\ {\isacharhash}\ zs\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline |
|
104 % |
|
105 \isadelimproof |
|
106 \ \ % |
|
107 \endisadelimproof |
|
108 % |
|
109 \isatagproof |
|
110 \isacommand{unfolding}\isamarkupfalse% |
|
111 \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
112 \ blast% |
|
113 \endisatagproof |
|
114 {\isafoldproof}% |
|
115 % |
|
116 \isadelimproof |
|
117 \isanewline |
|
118 % |
|
119 \endisadelimproof |
|
120 \isanewline |
|
121 \isacommand{lemma}\isamarkupfalse% |
|
122 \ strict{\isacharunderscore}prefixE{\isacharprime}\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline |
|
123 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline |
|
124 \ \ \isakeyword{obtains}\ z\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ z\ {\isacharhash}\ zs{\isachardoublequoteclose}\isanewline |
|
125 % |
|
126 \isadelimproof |
|
127 % |
|
128 \endisadelimproof |
|
129 % |
|
130 \isatagproof |
|
131 \isacommand{proof}\isamarkupfalse% |
|
132 \ {\isacharminus}\isanewline |
|
133 \ \ \isacommand{from}\isamarkupfalse% |
|
134 \ {\isacharbackquoteopen}xs\ {\isacharless}\ ys{\isacharbackquoteclose}\ \isacommand{obtain}\isamarkupfalse% |
|
135 \ us\ \isakeyword{where}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ us{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline |
|
136 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
137 \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
138 \ blast\isanewline |
|
139 \ \ \isacommand{with}\isamarkupfalse% |
|
140 \ that\ \isacommand{show}\isamarkupfalse% |
|
141 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
142 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ neq{\isacharunderscore}Nil{\isacharunderscore}conv{\isacharparenright}\isanewline |
|
143 \isacommand{qed}\isamarkupfalse% |
|
144 % |
|
145 \endisatagproof |
|
146 {\isafoldproof}% |
|
147 % |
|
148 \isadelimproof |
|
149 \isanewline |
|
150 % |
|
151 \endisadelimproof |
|
152 \isanewline |
|
153 \isacommand{lemma}\isamarkupfalse% |
|
154 \ strict{\isacharunderscore}prefixI\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymnoteq}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
155 % |
|
156 \isadelimproof |
|
157 \ \ % |
|
158 \endisadelimproof |
|
159 % |
|
160 \isatagproof |
|
161 \isacommand{unfolding}\isamarkupfalse% |
|
162 \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
163 \ blast% |
|
164 \endisatagproof |
|
165 {\isafoldproof}% |
|
166 % |
|
167 \isadelimproof |
|
168 \isanewline |
|
169 % |
|
170 \endisadelimproof |
|
171 \isanewline |
|
172 \isacommand{lemma}\isamarkupfalse% |
|
173 \ strict{\isacharunderscore}prefixE\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline |
|
174 \ \ \isakeyword{fixes}\ xs\ ys\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline |
|
175 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline |
|
176 \ \ \isakeyword{obtains}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline |
|
177 % |
|
178 \isadelimproof |
|
179 \ \ % |
|
180 \endisadelimproof |
|
181 % |
|
182 \isatagproof |
|
183 \isacommand{using}\isamarkupfalse% |
|
184 \ assms\ \isacommand{unfolding}\isamarkupfalse% |
|
185 \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
186 \ blast% |
|
187 \endisatagproof |
|
188 {\isafoldproof}% |
|
189 % |
|
190 \isadelimproof |
|
191 % |
|
192 \endisadelimproof |
|
193 % |
|
194 \isamarkupsubsection{Basic properties of prefixes% |
|
195 } |
|
196 \isamarkuptrue% |
|
197 \isacommand{theorem}\isamarkupfalse% |
|
198 \ Nil{\isacharunderscore}prefix\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline |
|
199 % |
|
200 \isadelimproof |
|
201 \ \ % |
|
202 \endisadelimproof |
|
203 % |
|
204 \isatagproof |
|
205 \isacommand{by}\isamarkupfalse% |
|
206 \ {\isacharparenleft}simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
207 \endisatagproof |
|
208 {\isafoldproof}% |
|
209 % |
|
210 \isadelimproof |
|
211 \isanewline |
|
212 % |
|
213 \endisadelimproof |
|
214 \isanewline |
|
215 \isacommand{theorem}\isamarkupfalse% |
|
216 \ prefix{\isacharunderscore}Nil\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
217 % |
|
218 \isadelimproof |
|
219 \ \ % |
|
220 \endisadelimproof |
|
221 % |
|
222 \isatagproof |
|
223 \isacommand{by}\isamarkupfalse% |
|
224 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
225 \endisatagproof |
|
226 {\isafoldproof}% |
|
227 % |
|
228 \isadelimproof |
|
229 \isanewline |
|
230 % |
|
231 \endisadelimproof |
|
232 \isanewline |
|
233 \isacommand{lemma}\isamarkupfalse% |
|
234 \ prefix{\isacharunderscore}snoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isasymor}\ xs\ {\isasymle}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
235 % |
|
236 \isadelimproof |
|
237 % |
|
238 \endisadelimproof |
|
239 % |
|
240 \isatagproof |
|
241 \isacommand{proof}\isamarkupfalse% |
|
242 \isanewline |
|
243 \ \ \isacommand{assume}\isamarkupfalse% |
|
244 \ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
245 \ \ \isacommand{then}\isamarkupfalse% |
|
246 \ \isacommand{obtain}\isamarkupfalse% |
|
247 \ zs\ \isakeyword{where}\ zs{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
248 \isanewline |
|
249 \ \ \isacommand{show}\isamarkupfalse% |
|
250 \ {\isachardoublequoteopen}xs\ {\isacharequal}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isasymor}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
251 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
252 \ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ butlast{\isacharunderscore}append\ butlast{\isacharunderscore}snoc\ prefixI\ zs{\isacharparenright}\isanewline |
|
253 \isacommand{next}\isamarkupfalse% |
|
254 \isanewline |
|
255 \ \ \isacommand{assume}\isamarkupfalse% |
|
256 \ {\isachardoublequoteopen}xs\ {\isacharequal}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}\ {\isasymor}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
257 \ \ \isacommand{then}\isamarkupfalse% |
|
258 \ \isacommand{show}\isamarkupfalse% |
|
259 \ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharat}\ {\isacharbrackleft}y{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
260 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
261 \ {\isacharparenleft}metis\ order{\isacharunderscore}eq{\isacharunderscore}iff\ strict{\isacharunderscore}prefixE\ strict{\isacharunderscore}prefixI{\isacharprime}\ xt{\isadigit{1}}{\isacharparenleft}{\isadigit{7}}{\isacharparenright}{\isacharparenright}\isanewline |
|
262 \isacommand{qed}\isamarkupfalse% |
|
263 % |
|
264 \endisatagproof |
|
265 {\isafoldproof}% |
|
266 % |
|
267 \isadelimproof |
|
268 \isanewline |
|
269 % |
|
270 \endisadelimproof |
|
271 \isanewline |
|
272 \isacommand{lemma}\isamarkupfalse% |
|
273 \ Cons{\isacharunderscore}prefix{\isacharunderscore}Cons\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs\ {\isasymle}\ y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isasymle}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
274 % |
|
275 \isadelimproof |
|
276 \ \ % |
|
277 \endisadelimproof |
|
278 % |
|
279 \isatagproof |
|
280 \isacommand{by}\isamarkupfalse% |
|
281 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
282 \endisatagproof |
|
283 {\isafoldproof}% |
|
284 % |
|
285 \isadelimproof |
|
286 \isanewline |
|
287 % |
|
288 \endisadelimproof |
|
289 \isanewline |
|
290 \isacommand{lemma}\isamarkupfalse% |
|
291 \ same{\isacharunderscore}prefix{\isacharunderscore}prefix\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys\ {\isasymle}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}ys\ {\isasymle}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
292 % |
|
293 \isadelimproof |
|
294 \ \ % |
|
295 \endisadelimproof |
|
296 % |
|
297 \isatagproof |
|
298 \isacommand{by}\isamarkupfalse% |
|
299 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% |
|
300 \endisatagproof |
|
301 {\isafoldproof}% |
|
302 % |
|
303 \isadelimproof |
|
304 \isanewline |
|
305 % |
|
306 \endisadelimproof |
|
307 \isanewline |
|
308 \isacommand{lemma}\isamarkupfalse% |
|
309 \ same{\isacharunderscore}prefix{\isacharunderscore}nil\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys\ {\isasymle}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
310 % |
|
311 \isadelimproof |
|
312 \ \ % |
|
313 \endisadelimproof |
|
314 % |
|
315 \isatagproof |
|
316 \isacommand{by}\isamarkupfalse% |
|
317 \ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ append{\isacharunderscore}self{\isacharunderscore}conv\ order{\isacharunderscore}eq{\isacharunderscore}iff\ prefixI{\isacharparenright}% |
|
318 \endisatagproof |
|
319 {\isafoldproof}% |
|
320 % |
|
321 \isadelimproof |
|
322 \isanewline |
|
323 % |
|
324 \endisadelimproof |
|
325 \isanewline |
|
326 \isacommand{lemma}\isamarkupfalse% |
|
327 \ prefix{\isacharunderscore}prefix\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymle}\ ys\ {\isacharat}\ zs{\isachardoublequoteclose}\isanewline |
|
328 % |
|
329 \isadelimproof |
|
330 \ \ % |
|
331 \endisadelimproof |
|
332 % |
|
333 \isatagproof |
|
334 \isacommand{by}\isamarkupfalse% |
|
335 \ {\isacharparenleft}metis\ order{\isacharunderscore}le{\isacharunderscore}less{\isacharunderscore}trans\ prefixI\ strict{\isacharunderscore}prefixE\ strict{\isacharunderscore}prefixI{\isacharparenright}% |
|
336 \endisatagproof |
|
337 {\isafoldproof}% |
|
338 % |
|
339 \isadelimproof |
|
340 \isanewline |
|
341 % |
|
342 \endisadelimproof |
|
343 \isanewline |
|
344 \isacommand{lemma}\isamarkupfalse% |
|
345 \ append{\isacharunderscore}prefixD{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharat}\ ys\ {\isasymle}\ zs\ {\isasymLongrightarrow}\ xs\ {\isasymle}\ zs{\isachardoublequoteclose}\isanewline |
|
346 % |
|
347 \isadelimproof |
|
348 \ \ % |
|
349 \endisadelimproof |
|
350 % |
|
351 \isatagproof |
|
352 \isacommand{by}\isamarkupfalse% |
|
353 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
354 \endisatagproof |
|
355 {\isafoldproof}% |
|
356 % |
|
357 \isadelimproof |
|
358 \isanewline |
|
359 % |
|
360 \endisadelimproof |
|
361 \isanewline |
|
362 \isacommand{theorem}\isamarkupfalse% |
|
363 \ prefix{\isacharunderscore}Cons{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}zs{\isachardot}\ xs\ {\isacharequal}\ y\ {\isacharhash}\ zs\ {\isasymand}\ zs\ {\isasymle}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
364 % |
|
365 \isadelimproof |
|
366 \ \ % |
|
367 \endisadelimproof |
|
368 % |
|
369 \isatagproof |
|
370 \isacommand{by}\isamarkupfalse% |
|
371 \ {\isacharparenleft}cases\ xs{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
372 \endisatagproof |
|
373 {\isafoldproof}% |
|
374 % |
|
375 \isadelimproof |
|
376 \isanewline |
|
377 % |
|
378 \endisadelimproof |
|
379 \isanewline |
|
380 \isacommand{theorem}\isamarkupfalse% |
|
381 \ prefix{\isacharunderscore}append{\isacharcolon}\isanewline |
|
382 \ \ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymle}\ ys\ {\isacharat}\ zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isasymle}\ ys\ {\isasymor}\ {\isacharparenleft}{\isasymexists}us{\isachardot}\ xs\ {\isacharequal}\ ys\ {\isacharat}\ us\ {\isasymand}\ us\ {\isasymle}\ zs{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
383 % |
|
384 \isadelimproof |
|
385 \ \ % |
|
386 \endisadelimproof |
|
387 % |
|
388 \isatagproof |
|
389 \isacommand{apply}\isamarkupfalse% |
|
390 \ {\isacharparenleft}induct\ zs\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline |
|
391 \ \ \ \isacommand{apply}\isamarkupfalse% |
|
392 \ force\isanewline |
|
393 \ \ \isacommand{apply}\isamarkupfalse% |
|
394 \ {\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}assoc\ add{\isacharcolon}\ append{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
|
395 \ \ \isacommand{apply}\isamarkupfalse% |
|
396 \ {\isacharparenleft}metis\ append{\isacharunderscore}eq{\isacharunderscore}appendI{\isacharparenright}\isanewline |
|
397 \ \ \isacommand{done}\isamarkupfalse% |
|
398 % |
|
399 \endisatagproof |
|
400 {\isafoldproof}% |
|
401 % |
|
402 \isadelimproof |
|
403 \isanewline |
|
404 % |
|
405 \endisadelimproof |
|
406 \isanewline |
|
407 \isacommand{lemma}\isamarkupfalse% |
|
408 \ append{\isacharunderscore}one{\isacharunderscore}prefix{\isacharcolon}\isanewline |
|
409 \ \ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ length\ xs\ {\isacharless}\ length\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ {\isacharbrackleft}ys\ {\isacharbang}\ length\ xs{\isacharbrackright}\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
410 % |
|
411 \isadelimproof |
|
412 \ \ % |
|
413 \endisadelimproof |
|
414 % |
|
415 \isatagproof |
|
416 \isacommand{unfolding}\isamarkupfalse% |
|
417 \ prefix{\isacharunderscore}def\isanewline |
|
418 \ \ \isacommand{by}\isamarkupfalse% |
|
419 \ {\isacharparenleft}metis\ Cons{\isacharunderscore}eq{\isacharunderscore}appendI\ append{\isacharunderscore}eq{\isacharunderscore}appendI\ append{\isacharunderscore}eq{\isacharunderscore}conv{\isacharunderscore}conj\isanewline |
|
420 \ \ \ \ eq{\isacharunderscore}Nil{\isacharunderscore}appendI\ nth{\isacharunderscore}drop{\isacharprime}{\isacharparenright}% |
|
421 \endisatagproof |
|
422 {\isafoldproof}% |
|
423 % |
|
424 \isadelimproof |
|
425 \isanewline |
|
426 % |
|
427 \endisadelimproof |
|
428 \isanewline |
|
429 \isacommand{theorem}\isamarkupfalse% |
|
430 \ prefix{\isacharunderscore}length{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ length\ xs\ {\isasymle}\ length\ ys{\isachardoublequoteclose}\isanewline |
|
431 % |
|
432 \isadelimproof |
|
433 \ \ % |
|
434 \endisadelimproof |
|
435 % |
|
436 \isatagproof |
|
437 \isacommand{by}\isamarkupfalse% |
|
438 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
439 \endisatagproof |
|
440 {\isafoldproof}% |
|
441 % |
|
442 \isadelimproof |
|
443 \isanewline |
|
444 % |
|
445 \endisadelimproof |
|
446 \isanewline |
|
447 \isacommand{lemma}\isamarkupfalse% |
|
448 \ prefix{\isacharunderscore}same{\isacharunderscore}cases{\isacharcolon}\isanewline |
|
449 \ \ {\isachardoublequoteopen}{\isacharparenleft}xs\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ xs\isactrlisub {\isadigit{2}}\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ xs\isactrlisub {\isadigit{1}}\ {\isasymle}\ xs\isactrlisub {\isadigit{2}}\ {\isasymor}\ xs\isactrlisub {\isadigit{2}}\ {\isasymle}\ xs\isactrlisub {\isadigit{1}}{\isachardoublequoteclose}\isanewline |
|
450 % |
|
451 \isadelimproof |
|
452 \ \ % |
|
453 \endisadelimproof |
|
454 % |
|
455 \isatagproof |
|
456 \isacommand{unfolding}\isamarkupfalse% |
|
457 \ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
458 \ {\isacharparenleft}metis\ append{\isacharunderscore}eq{\isacharunderscore}append{\isacharunderscore}conv{\isadigit{2}}{\isacharparenright}% |
|
459 \endisatagproof |
|
460 {\isafoldproof}% |
|
461 % |
|
462 \isadelimproof |
|
463 \isanewline |
|
464 % |
|
465 \endisadelimproof |
|
466 \isanewline |
|
467 \isacommand{lemma}\isamarkupfalse% |
|
468 \ set{\isacharunderscore}mono{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ set\ xs\ {\isasymsubseteq}\ set\ ys{\isachardoublequoteclose}\isanewline |
|
469 % |
|
470 \isadelimproof |
|
471 \ \ % |
|
472 \endisadelimproof |
|
473 % |
|
474 \isatagproof |
|
475 \isacommand{by}\isamarkupfalse% |
|
476 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
477 \endisatagproof |
|
478 {\isafoldproof}% |
|
479 % |
|
480 \isadelimproof |
|
481 \isanewline |
|
482 % |
|
483 \endisadelimproof |
|
484 \isanewline |
|
485 \isacommand{lemma}\isamarkupfalse% |
|
486 \ take{\isacharunderscore}is{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}take\ n\ xs\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline |
|
487 % |
|
488 \isadelimproof |
|
489 \ \ % |
|
490 \endisadelimproof |
|
491 % |
|
492 \isatagproof |
|
493 \isacommand{unfolding}\isamarkupfalse% |
|
494 \ prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
495 \ {\isacharparenleft}metis\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}% |
|
496 \endisatagproof |
|
497 {\isafoldproof}% |
|
498 % |
|
499 \isadelimproof |
|
500 \isanewline |
|
501 % |
|
502 \endisadelimproof |
|
503 \isanewline |
|
504 \isacommand{lemma}\isamarkupfalse% |
|
505 \ map{\isacharunderscore}prefixI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys\ {\isasymLongrightarrow}\ map\ f\ xs\ {\isasymle}\ map\ f\ ys{\isachardoublequoteclose}\isanewline |
|
506 % |
|
507 \isadelimproof |
|
508 \ \ % |
|
509 \endisadelimproof |
|
510 % |
|
511 \isatagproof |
|
512 \isacommand{by}\isamarkupfalse% |
|
513 \ {\isacharparenleft}auto\ simp{\isacharcolon}\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
514 \endisatagproof |
|
515 {\isafoldproof}% |
|
516 % |
|
517 \isadelimproof |
|
518 \isanewline |
|
519 % |
|
520 \endisadelimproof |
|
521 \isanewline |
|
522 \isacommand{lemma}\isamarkupfalse% |
|
523 \ prefix{\isacharunderscore}length{\isacharunderscore}less{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys\ {\isasymLongrightarrow}\ length\ xs\ {\isacharless}\ length\ ys{\isachardoublequoteclose}\isanewline |
|
524 % |
|
525 \isadelimproof |
|
526 \ \ % |
|
527 \endisadelimproof |
|
528 % |
|
529 \isatagproof |
|
530 \isacommand{by}\isamarkupfalse% |
|
531 \ {\isacharparenleft}auto\ simp{\isacharcolon}\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ prefix{\isacharunderscore}def{\isacharparenright}% |
|
532 \endisatagproof |
|
533 {\isafoldproof}% |
|
534 % |
|
535 \isadelimproof |
|
536 \isanewline |
|
537 % |
|
538 \endisadelimproof |
|
539 \isanewline |
|
540 \isacommand{lemma}\isamarkupfalse% |
|
541 \ strict{\isacharunderscore}prefix{\isacharunderscore}simps\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
|
542 \ \ \ \ {\isachardoublequoteopen}xs\ {\isacharless}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline |
|
543 \ \ \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline |
|
544 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isacharless}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
545 % |
|
546 \isadelimproof |
|
547 \ \ % |
|
548 \endisadelimproof |
|
549 % |
|
550 \isatagproof |
|
551 \isacommand{by}\isamarkupfalse% |
|
552 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ cong{\isacharcolon}\ conj{\isacharunderscore}cong{\isacharparenright}% |
|
553 \endisatagproof |
|
554 {\isafoldproof}% |
|
555 % |
|
556 \isadelimproof |
|
557 \isanewline |
|
558 % |
|
559 \endisadelimproof |
|
560 \isanewline |
|
561 \isacommand{lemma}\isamarkupfalse% |
|
562 \ take{\isacharunderscore}strict{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}\ ys\ {\isasymLongrightarrow}\ take\ n\ xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline |
|
563 % |
|
564 \isadelimproof |
|
565 \ \ % |
|
566 \endisadelimproof |
|
567 % |
|
568 \isatagproof |
|
569 \isacommand{apply}\isamarkupfalse% |
|
570 \ {\isacharparenleft}induct\ n\ arbitrary{\isacharcolon}\ xs\ ys{\isacharparenright}\isanewline |
|
571 \ \ \ \isacommand{apply}\isamarkupfalse% |
|
572 \ {\isacharparenleft}case{\isacharunderscore}tac\ ys{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline |
|
573 \ \ \isacommand{apply}\isamarkupfalse% |
|
574 \ {\isacharparenleft}metis\ order{\isacharunderscore}less{\isacharunderscore}trans\ strict{\isacharunderscore}prefixI\ take{\isacharunderscore}is{\isacharunderscore}prefix{\isacharparenright}\isanewline |
|
575 \ \ \isacommand{done}\isamarkupfalse% |
|
576 % |
|
577 \endisatagproof |
|
578 {\isafoldproof}% |
|
579 % |
|
580 \isadelimproof |
|
581 \isanewline |
|
582 % |
|
583 \endisadelimproof |
|
584 \isanewline |
|
585 \isacommand{lemma}\isamarkupfalse% |
|
586 \ not{\isacharunderscore}prefix{\isacharunderscore}cases{\isacharcolon}\isanewline |
|
587 \ \ \isakeyword{assumes}\ pfx{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ ps\ {\isasymle}\ ls{\isachardoublequoteclose}\isanewline |
|
588 \ \ \isakeyword{obtains}\isanewline |
|
589 \ \ \ \ {\isacharparenleft}c{\isadigit{1}}{\isacharparenright}\ {\isachardoublequoteopen}ps\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}ls\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
590 \ \ {\isacharbar}\ {\isacharparenleft}c{\isadigit{2}}{\isacharparenright}\ a\ as\ x\ xs\ \isakeyword{where}\ {\isachardoublequoteopen}ps\ {\isacharequal}\ a{\isacharhash}as{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}ls\ {\isacharequal}\ x{\isacharhash}xs{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isacharequal}\ a{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymnot}\ as\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline |
|
591 \ \ {\isacharbar}\ {\isacharparenleft}c{\isadigit{3}}{\isacharparenright}\ a\ as\ x\ xs\ \isakeyword{where}\ {\isachardoublequoteopen}ps\ {\isacharequal}\ a{\isacharhash}as{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}ls\ {\isacharequal}\ x{\isacharhash}xs{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ a{\isachardoublequoteclose}\isanewline |
|
592 % |
|
593 \isadelimproof |
|
594 % |
|
595 \endisadelimproof |
|
596 % |
|
597 \isatagproof |
|
598 \isacommand{proof}\isamarkupfalse% |
|
599 \ {\isacharparenleft}cases\ ps{\isacharparenright}\isanewline |
|
600 \ \ \isacommand{case}\isamarkupfalse% |
|
601 \ Nil\ \isacommand{then}\isamarkupfalse% |
|
602 \ \isacommand{show}\isamarkupfalse% |
|
603 \ {\isacharquery}thesis\ \isacommand{using}\isamarkupfalse% |
|
604 \ pfx\ \isacommand{by}\isamarkupfalse% |
|
605 \ simp\isanewline |
|
606 \isacommand{next}\isamarkupfalse% |
|
607 \isanewline |
|
608 \ \ \isacommand{case}\isamarkupfalse% |
|
609 \ {\isacharparenleft}Cons\ a\ as{\isacharparenright}\isanewline |
|
610 \ \ \isacommand{note}\isamarkupfalse% |
|
611 \ c\ {\isacharequal}\ {\isacharbackquoteopen}ps\ {\isacharequal}\ a{\isacharhash}as{\isacharbackquoteclose}\isanewline |
|
612 \ \ \isacommand{show}\isamarkupfalse% |
|
613 \ {\isacharquery}thesis\isanewline |
|
614 \ \ \isacommand{proof}\isamarkupfalse% |
|
615 \ {\isacharparenleft}cases\ ls{\isacharparenright}\isanewline |
|
616 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
617 \ Nil\ \isacommand{then}\isamarkupfalse% |
|
618 \ \isacommand{show}\isamarkupfalse% |
|
619 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
620 \ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ pfx\ c{\isadigit{1}}\ same{\isacharunderscore}prefix{\isacharunderscore}nil{\isacharparenright}\isanewline |
|
621 \ \ \isacommand{next}\isamarkupfalse% |
|
622 \isanewline |
|
623 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
624 \ {\isacharparenleft}Cons\ x\ xs{\isacharparenright}\isanewline |
|
625 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
626 \ {\isacharquery}thesis\isanewline |
|
627 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
|
628 \ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isacharequal}\ a{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
629 \ \ \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
630 \ True\isanewline |
|
631 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse% |
|
632 \ {\isachardoublequoteopen}{\isasymnot}\ as\ {\isasymle}\ xs{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
|
633 \ pfx\ c\ Cons\ True\ \isacommand{by}\isamarkupfalse% |
|
634 \ simp\isanewline |
|
635 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
636 \ c\ Cons\ True\ \isacommand{show}\isamarkupfalse% |
|
637 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
638 \ {\isacharparenleft}rule\ c{\isadigit{2}}{\isacharparenright}\isanewline |
|
639 \ \ \ \ \isacommand{next}\isamarkupfalse% |
|
640 \isanewline |
|
641 \ \ \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
642 \ False\isanewline |
|
643 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
644 \ c\ Cons\ \isacommand{show}\isamarkupfalse% |
|
645 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
646 \ {\isacharparenleft}rule\ c{\isadigit{3}}{\isacharparenright}\isanewline |
|
647 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
|
648 \isanewline |
|
649 \ \ \isacommand{qed}\isamarkupfalse% |
|
650 \isanewline |
|
651 \isacommand{qed}\isamarkupfalse% |
|
652 % |
|
653 \endisatagproof |
|
654 {\isafoldproof}% |
|
655 % |
|
656 \isadelimproof |
|
657 \isanewline |
|
658 % |
|
659 \endisadelimproof |
|
660 \isanewline |
|
661 \isacommand{lemma}\isamarkupfalse% |
|
662 \ not{\isacharunderscore}prefix{\isacharunderscore}induct\ {\isacharbrackleft}consumes\ {\isadigit{1}}{\isacharcomma}\ case{\isacharunderscore}names\ Nil\ Neq\ Eq{\isacharbrackright}{\isacharcolon}\isanewline |
|
663 \ \ \isakeyword{assumes}\ np{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ ps\ {\isasymle}\ ls{\isachardoublequoteclose}\isanewline |
|
664 \ \ \ \ \isakeyword{and}\ base{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ xs{\isachardot}\ P\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
665 \ \ \ \ \isakeyword{and}\ r{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ xs\ y\ ys{\isachardot}\ x\ {\isasymnoteq}\ y\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}y{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
666 \ \ \ \ \isakeyword{and}\ r{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ xs\ y\ ys{\isachardot}\ {\isasymlbrakk}\ x\ {\isacharequal}\ y{\isacharsemicolon}\ {\isasymnot}\ xs\ {\isasymle}\ ys{\isacharsemicolon}\ P\ xs\ ys\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}y{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
667 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}P\ ps\ ls{\isachardoublequoteclose}% |
|
668 \isadelimproof |
|
669 \ % |
|
670 \endisadelimproof |
|
671 % |
|
672 \isatagproof |
|
673 \isacommand{using}\isamarkupfalse% |
|
674 \ np\isanewline |
|
675 \isacommand{proof}\isamarkupfalse% |
|
676 \ {\isacharparenleft}induct\ ls\ arbitrary{\isacharcolon}\ ps{\isacharparenright}\isanewline |
|
677 \ \ \isacommand{case}\isamarkupfalse% |
|
678 \ Nil\ \isacommand{then}\isamarkupfalse% |
|
679 \ \isacommand{show}\isamarkupfalse% |
|
680 \ {\isacharquery}case\isanewline |
|
681 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
682 \ {\isacharparenleft}auto\ simp{\isacharcolon}\ neq{\isacharunderscore}Nil{\isacharunderscore}conv\ elim{\isacharbang}{\isacharcolon}\ not{\isacharunderscore}prefix{\isacharunderscore}cases\ intro{\isacharbang}{\isacharcolon}\ base{\isacharparenright}\isanewline |
|
683 \isacommand{next}\isamarkupfalse% |
|
684 \isanewline |
|
685 \ \ \isacommand{case}\isamarkupfalse% |
|
686 \ {\isacharparenleft}Cons\ y\ ys{\isacharparenright}\isanewline |
|
687 \ \ \isacommand{then}\isamarkupfalse% |
|
688 \ \isacommand{have}\isamarkupfalse% |
|
689 \ npfx{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ ps\ {\isasymle}\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
690 \ simp\isanewline |
|
691 \ \ \isacommand{then}\isamarkupfalse% |
|
692 \ \isacommand{obtain}\isamarkupfalse% |
|
693 \ x\ xs\ \isakeyword{where}\ pv{\isacharcolon}\ {\isachardoublequoteopen}ps\ {\isacharequal}\ x\ {\isacharhash}\ xs{\isachardoublequoteclose}\isanewline |
|
694 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
695 \ {\isacharparenleft}rule\ not{\isacharunderscore}prefix{\isacharunderscore}cases{\isacharparenright}\ auto\isanewline |
|
696 \ \ \isacommand{show}\isamarkupfalse% |
|
697 \ {\isacharquery}case\ \isacommand{by}\isamarkupfalse% |
|
698 \ {\isacharparenleft}metis\ Cons{\isachardot}hyps\ Cons{\isacharunderscore}prefix{\isacharunderscore}Cons\ npfx\ pv\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}\isanewline |
|
699 \isacommand{qed}\isamarkupfalse% |
|
700 % |
|
701 \endisatagproof |
|
702 {\isafoldproof}% |
|
703 % |
|
704 \isadelimproof |
|
705 % |
|
706 \endisadelimproof |
|
707 % |
|
708 \isamarkupsubsection{Parallel lists% |
|
709 } |
|
710 \isamarkuptrue% |
|
711 \isacommand{definition}\isamarkupfalse% |
|
712 \isanewline |
|
713 \ \ parallel\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymparallel}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
714 \ \ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isasymparallel}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ xs\ {\isasymle}\ ys\ {\isasymand}\ {\isasymnot}\ ys\ {\isasymle}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
715 \isanewline |
|
716 \isacommand{lemma}\isamarkupfalse% |
|
717 \ parallelI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ xs\ {\isasymle}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ {\isasymnot}\ ys\ {\isasymle}\ xs\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline |
|
718 % |
|
719 \isadelimproof |
|
720 \ \ % |
|
721 \endisadelimproof |
|
722 % |
|
723 \isatagproof |
|
724 \isacommand{unfolding}\isamarkupfalse% |
|
725 \ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
726 \ blast% |
|
727 \endisatagproof |
|
728 {\isafoldproof}% |
|
729 % |
|
730 \isadelimproof |
|
731 \isanewline |
|
732 % |
|
733 \endisadelimproof |
|
734 \isanewline |
|
735 \isacommand{lemma}\isamarkupfalse% |
|
736 \ parallelE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\isanewline |
|
737 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline |
|
738 \ \ \isakeyword{obtains}\ {\isachardoublequoteopen}{\isasymnot}\ xs\ {\isasymle}\ ys\ {\isasymand}\ {\isasymnot}\ ys\ {\isasymle}\ xs{\isachardoublequoteclose}\isanewline |
|
739 % |
|
740 \isadelimproof |
|
741 \ \ % |
|
742 \endisadelimproof |
|
743 % |
|
744 \isatagproof |
|
745 \isacommand{using}\isamarkupfalse% |
|
746 \ assms\ \isacommand{unfolding}\isamarkupfalse% |
|
747 \ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
748 \ blast% |
|
749 \endisatagproof |
|
750 {\isafoldproof}% |
|
751 % |
|
752 \isadelimproof |
|
753 \isanewline |
|
754 % |
|
755 \endisadelimproof |
|
756 \isanewline |
|
757 \isacommand{theorem}\isamarkupfalse% |
|
758 \ prefix{\isacharunderscore}cases{\isacharcolon}\isanewline |
|
759 \ \ \isakeyword{obtains}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\ {\isacharbar}\ {\isachardoublequoteopen}ys\ {\isacharless}\ xs{\isachardoublequoteclose}\ {\isacharbar}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline |
|
760 % |
|
761 \isadelimproof |
|
762 \ \ % |
|
763 \endisadelimproof |
|
764 % |
|
765 \isatagproof |
|
766 \isacommand{unfolding}\isamarkupfalse% |
|
767 \ parallel{\isacharunderscore}def\ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
768 \ blast% |
|
769 \endisatagproof |
|
770 {\isafoldproof}% |
|
771 % |
|
772 \isadelimproof |
|
773 \isanewline |
|
774 % |
|
775 \endisadelimproof |
|
776 \isanewline |
|
777 \isacommand{theorem}\isamarkupfalse% |
|
778 \ parallel{\isacharunderscore}decomp{\isacharcolon}\isanewline |
|
779 \ \ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ {\isasymexists}as\ b\ bs\ c\ cs{\isachardot}\ b\ {\isasymnoteq}\ c\ {\isasymand}\ xs\ {\isacharequal}\ as\ {\isacharat}\ b\ {\isacharhash}\ bs\ {\isasymand}\ ys\ {\isacharequal}\ as\ {\isacharat}\ c\ {\isacharhash}\ cs{\isachardoublequoteclose}\isanewline |
|
780 % |
|
781 \isadelimproof |
|
782 % |
|
783 \endisadelimproof |
|
784 % |
|
785 \isatagproof |
|
786 \isacommand{proof}\isamarkupfalse% |
|
787 \ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline |
|
788 \ \ \isacommand{case}\isamarkupfalse% |
|
789 \ Nil\isanewline |
|
790 \ \ \isacommand{then}\isamarkupfalse% |
|
791 \ \isacommand{have}\isamarkupfalse% |
|
792 \ False\ \isacommand{by}\isamarkupfalse% |
|
793 \ auto\isanewline |
|
794 \ \ \isacommand{then}\isamarkupfalse% |
|
795 \ \isacommand{show}\isamarkupfalse% |
|
796 \ {\isacharquery}case\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
797 \isanewline |
|
798 \isacommand{next}\isamarkupfalse% |
|
799 \isanewline |
|
800 \ \ \isacommand{case}\isamarkupfalse% |
|
801 \ {\isacharparenleft}snoc\ x\ xs{\isacharparenright}\isanewline |
|
802 \ \ \isacommand{show}\isamarkupfalse% |
|
803 \ {\isacharquery}case\isanewline |
|
804 \ \ \isacommand{proof}\isamarkupfalse% |
|
805 \ {\isacharparenleft}rule\ prefix{\isacharunderscore}cases{\isacharparenright}\isanewline |
|
806 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
807 \ le{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
808 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
809 \ \isacommand{obtain}\isamarkupfalse% |
|
810 \ ys{\isacharprime}\ \isakeyword{where}\ ys{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ xs\ {\isacharat}\ ys{\isacharprime}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
811 \isanewline |
|
812 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
813 \ {\isacharquery}thesis\isanewline |
|
814 \ \ \ \ \isacommand{proof}\isamarkupfalse% |
|
815 \ {\isacharparenleft}cases\ ys{\isacharprime}{\isacharparenright}\isanewline |
|
816 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
817 \ {\isachardoublequoteopen}ys{\isacharprime}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
818 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
819 \ \isacommand{show}\isamarkupfalse% |
|
820 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
821 \ {\isacharparenleft}metis\ append{\isacharunderscore}Nil{\isadigit{2}}\ parallelE\ prefixI\ snoc{\isachardot}prems\ ys{\isacharparenright}\isanewline |
|
822 \ \ \ \ \isacommand{next}\isamarkupfalse% |
|
823 \isanewline |
|
824 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
825 \ c\ cs\ \isacommand{assume}\isamarkupfalse% |
|
826 \ ys{\isacharprime}{\isacharcolon}\ {\isachardoublequoteopen}ys{\isacharprime}\ {\isacharequal}\ c\ {\isacharhash}\ cs{\isachardoublequoteclose}\isanewline |
|
827 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
828 \ \isacommand{show}\isamarkupfalse% |
|
829 \ {\isacharquery}thesis\isanewline |
|
830 \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
831 \ {\isacharparenleft}metis\ Cons{\isacharunderscore}eq{\isacharunderscore}appendI\ eq{\isacharunderscore}Nil{\isacharunderscore}appendI\ parallelE\ prefixI\isanewline |
|
832 \ \ \ \ \ \ \ \ \ \ same{\isacharunderscore}prefix{\isacharunderscore}prefix\ snoc{\isachardot}prems\ ys{\isacharparenright}\isanewline |
|
833 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
|
834 \isanewline |
|
835 \ \ \isacommand{next}\isamarkupfalse% |
|
836 \isanewline |
|
837 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
838 \ {\isachardoublequoteopen}ys\ {\isacharless}\ xs{\isachardoublequoteclose}\ \isacommand{then}\isamarkupfalse% |
|
839 \ \isacommand{have}\isamarkupfalse% |
|
840 \ {\isachardoublequoteopen}ys\ {\isasymle}\ xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
841 \ {\isacharparenleft}simp\ add{\isacharcolon}\ strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharparenright}\isanewline |
|
842 \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
843 \ snoc\ \isacommand{have}\isamarkupfalse% |
|
844 \ False\ \isacommand{by}\isamarkupfalse% |
|
845 \ blast\isanewline |
|
846 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
847 \ \isacommand{show}\isamarkupfalse% |
|
848 \ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
849 \isanewline |
|
850 \ \ \isacommand{next}\isamarkupfalse% |
|
851 \isanewline |
|
852 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
|
853 \ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline |
|
854 \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
855 \ snoc\ \isacommand{obtain}\isamarkupfalse% |
|
856 \ as\ b\ bs\ c\ cs\ \isakeyword{where}\ neq{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}b{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharparenright}\ {\isasymnoteq}\ c{\isachardoublequoteclose}\isanewline |
|
857 \ \ \ \ \ \ \isakeyword{and}\ xs{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ as\ {\isacharat}\ b\ {\isacharhash}\ bs{\isachardoublequoteclose}\ \isakeyword{and}\ ys{\isacharcolon}\ {\isachardoublequoteopen}ys\ {\isacharequal}\ as\ {\isacharat}\ c\ {\isacharhash}\ cs{\isachardoublequoteclose}\isanewline |
|
858 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
859 \ blast\isanewline |
|
860 \ \ \ \ \isacommand{from}\isamarkupfalse% |
|
861 \ xs\ \isacommand{have}\isamarkupfalse% |
|
862 \ {\isachardoublequoteopen}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ as\ {\isacharat}\ b\ {\isacharhash}\ {\isacharparenleft}bs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
863 \ simp\isanewline |
|
864 \ \ \ \ \isacommand{with}\isamarkupfalse% |
|
865 \ neq\ ys\ \isacommand{show}\isamarkupfalse% |
|
866 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
867 \ blast\isanewline |
|
868 \ \ \isacommand{qed}\isamarkupfalse% |
|
869 \isanewline |
|
870 \isacommand{qed}\isamarkupfalse% |
|
871 % |
|
872 \endisatagproof |
|
873 {\isafoldproof}% |
|
874 % |
|
875 \isadelimproof |
|
876 \isanewline |
|
877 % |
|
878 \endisadelimproof |
|
879 \isanewline |
|
880 \isacommand{lemma}\isamarkupfalse% |
|
881 \ parallel{\isacharunderscore}append{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymparallel}\ b\ {\isasymLongrightarrow}\ a\ {\isacharat}\ c\ {\isasymparallel}\ b\ {\isacharat}\ d{\isachardoublequoteclose}\isanewline |
|
882 % |
|
883 \isadelimproof |
|
884 \ \ % |
|
885 \endisadelimproof |
|
886 % |
|
887 \isatagproof |
|
888 \isacommand{apply}\isamarkupfalse% |
|
889 \ {\isacharparenleft}rule\ parallelI{\isacharparenright}\isanewline |
|
890 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
|
891 \ {\isacharparenleft}erule\ parallelE{\isacharcomma}\ erule\ conjE{\isacharcomma}\isanewline |
|
892 \ \ \ \ \ \ induct\ rule{\isacharcolon}\ not{\isacharunderscore}prefix{\isacharunderscore}induct{\isacharcomma}\ simp{\isacharplus}{\isacharparenright}{\isacharplus}\isanewline |
|
893 \ \ \isacommand{done}\isamarkupfalse% |
|
894 % |
|
895 \endisatagproof |
|
896 {\isafoldproof}% |
|
897 % |
|
898 \isadelimproof |
|
899 \isanewline |
|
900 % |
|
901 \endisadelimproof |
|
902 \isanewline |
|
903 \isacommand{lemma}\isamarkupfalse% |
|
904 \ parallel{\isacharunderscore}appendI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ xs\ {\isacharat}\ xs{\isacharprime}\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ ys\ {\isacharat}\ ys{\isacharprime}\ {\isasymLongrightarrow}\ x\ {\isasymparallel}\ y{\isachardoublequoteclose}\isanewline |
|
905 % |
|
906 \isadelimproof |
|
907 \ \ % |
|
908 \endisadelimproof |
|
909 % |
|
910 \isatagproof |
|
911 \isacommand{by}\isamarkupfalse% |
|
912 \ {\isacharparenleft}simp\ add{\isacharcolon}\ parallel{\isacharunderscore}append{\isacharparenright}% |
|
913 \endisatagproof |
|
914 {\isafoldproof}% |
|
915 % |
|
916 \isadelimproof |
|
917 \isanewline |
|
918 % |
|
919 \endisadelimproof |
|
920 \isanewline |
|
921 \isacommand{lemma}\isamarkupfalse% |
|
922 \ parallel{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymparallel}\ b\ {\isasymlongleftrightarrow}\ b\ {\isasymparallel}\ a{\isachardoublequoteclose}\isanewline |
|
923 % |
|
924 \isadelimproof |
|
925 \ \ % |
|
926 \endisadelimproof |
|
927 % |
|
928 \isatagproof |
|
929 \isacommand{unfolding}\isamarkupfalse% |
|
930 \ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
931 \ auto% |
|
932 \endisatagproof |
|
933 {\isafoldproof}% |
|
934 % |
|
935 \isadelimproof |
|
936 % |
|
937 \endisadelimproof |
|
938 % |
|
939 \isamarkupsubsection{Postfix order on lists% |
|
940 } |
|
941 \isamarkuptrue% |
|
942 \isacommand{definition}\isamarkupfalse% |
|
943 \isanewline |
|
944 \ \ postfix\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ bool{\isachardoublequoteclose}\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isacharslash}\ {\isachargreater}{\isachargreater}{\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{5}}{\isadigit{1}}{\isacharcomma}\ {\isadigit{5}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline |
|
945 \ \ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}zs{\isachardot}\ xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
946 \isanewline |
|
947 \isacommand{lemma}\isamarkupfalse% |
|
948 \ postfixI\ {\isacharbrackleft}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
949 % |
|
950 \isadelimproof |
|
951 \ \ % |
|
952 \endisadelimproof |
|
953 % |
|
954 \isatagproof |
|
955 \isacommand{unfolding}\isamarkupfalse% |
|
956 \ postfix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
957 \ blast% |
|
958 \endisatagproof |
|
959 {\isafoldproof}% |
|
960 % |
|
961 \isadelimproof |
|
962 \isanewline |
|
963 % |
|
964 \endisadelimproof |
|
965 \isanewline |
|
966 \isacommand{lemma}\isamarkupfalse% |
|
967 \ postfixE\ {\isacharbrackleft}elim{\isacharquery}{\isacharbrackright}{\isacharcolon}\isanewline |
|
968 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
969 \ \ \isakeyword{obtains}\ zs\ \isakeyword{where}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline |
|
970 % |
|
971 \isadelimproof |
|
972 \ \ % |
|
973 \endisadelimproof |
|
974 % |
|
975 \isatagproof |
|
976 \isacommand{using}\isamarkupfalse% |
|
977 \ assms\ \isacommand{unfolding}\isamarkupfalse% |
|
978 \ postfix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
979 \ blast% |
|
980 \endisatagproof |
|
981 {\isafoldproof}% |
|
982 % |
|
983 \isadelimproof |
|
984 \isanewline |
|
985 % |
|
986 \endisadelimproof |
|
987 \isanewline |
|
988 \isacommand{lemma}\isamarkupfalse% |
|
989 \ postfix{\isacharunderscore}refl\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
|
990 % |
|
991 \isadelimproof |
|
992 \ \ % |
|
993 \endisadelimproof |
|
994 % |
|
995 \isatagproof |
|
996 \isacommand{by}\isamarkupfalse% |
|
997 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
998 \endisatagproof |
|
999 {\isafoldproof}% |
|
1000 % |
|
1001 \isadelimproof |
|
1002 \isanewline |
|
1003 % |
|
1004 \endisadelimproof |
|
1005 \isacommand{lemma}\isamarkupfalse% |
|
1006 \ postfix{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isacharsemicolon}\ ys\ {\isachargreater}{\isachargreater}{\isacharequal}\ zs{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ zs{\isachardoublequoteclose}\isanewline |
|
1007 % |
|
1008 \isadelimproof |
|
1009 \ \ % |
|
1010 \endisadelimproof |
|
1011 % |
|
1012 \isatagproof |
|
1013 \isacommand{by}\isamarkupfalse% |
|
1014 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1015 \endisatagproof |
|
1016 {\isafoldproof}% |
|
1017 % |
|
1018 \isadelimproof |
|
1019 \isanewline |
|
1020 % |
|
1021 \endisadelimproof |
|
1022 \isacommand{lemma}\isamarkupfalse% |
|
1023 \ postfix{\isacharunderscore}antisym{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isacharsemicolon}\ ys\ {\isachargreater}{\isachargreater}{\isacharequal}\ xs{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1024 % |
|
1025 \isadelimproof |
|
1026 \ \ % |
|
1027 \endisadelimproof |
|
1028 % |
|
1029 \isatagproof |
|
1030 \isacommand{by}\isamarkupfalse% |
|
1031 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1032 \endisatagproof |
|
1033 {\isafoldproof}% |
|
1034 % |
|
1035 \isadelimproof |
|
1036 \isanewline |
|
1037 % |
|
1038 \endisadelimproof |
|
1039 \isanewline |
|
1040 \isacommand{lemma}\isamarkupfalse% |
|
1041 \ Nil{\isacharunderscore}postfix\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
1042 % |
|
1043 \isadelimproof |
|
1044 \ \ % |
|
1045 \endisadelimproof |
|
1046 % |
|
1047 \isatagproof |
|
1048 \isacommand{by}\isamarkupfalse% |
|
1049 \ {\isacharparenleft}simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1050 \endisatagproof |
|
1051 {\isafoldproof}% |
|
1052 % |
|
1053 \isadelimproof |
|
1054 \isanewline |
|
1055 % |
|
1056 \endisadelimproof |
|
1057 \isacommand{lemma}\isamarkupfalse% |
|
1058 \ postfix{\isacharunderscore}Nil\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isachargreater}{\isachargreater}{\isacharequal}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
1059 % |
|
1060 \isadelimproof |
|
1061 \ \ % |
|
1062 \endisadelimproof |
|
1063 % |
|
1064 \isatagproof |
|
1065 \isacommand{by}\isamarkupfalse% |
|
1066 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1067 \endisatagproof |
|
1068 {\isafoldproof}% |
|
1069 % |
|
1070 \isadelimproof |
|
1071 \isanewline |
|
1072 % |
|
1073 \endisadelimproof |
|
1074 \isanewline |
|
1075 \isacommand{lemma}\isamarkupfalse% |
|
1076 \ postfix{\isacharunderscore}ConsI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ x{\isacharhash}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1077 % |
|
1078 \isadelimproof |
|
1079 \ \ % |
|
1080 \endisadelimproof |
|
1081 % |
|
1082 \isatagproof |
|
1083 \isacommand{by}\isamarkupfalse% |
|
1084 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1085 \endisatagproof |
|
1086 {\isafoldproof}% |
|
1087 % |
|
1088 \isadelimproof |
|
1089 \isanewline |
|
1090 % |
|
1091 \endisadelimproof |
|
1092 \isacommand{lemma}\isamarkupfalse% |
|
1093 \ postfix{\isacharunderscore}ConsD{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ y{\isacharhash}ys\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1094 % |
|
1095 \isadelimproof |
|
1096 \ \ % |
|
1097 \endisadelimproof |
|
1098 % |
|
1099 \isatagproof |
|
1100 \isacommand{by}\isamarkupfalse% |
|
1101 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1102 \endisatagproof |
|
1103 {\isafoldproof}% |
|
1104 % |
|
1105 \isadelimproof |
|
1106 \isanewline |
|
1107 % |
|
1108 \endisadelimproof |
|
1109 \isanewline |
|
1110 \isacommand{lemma}\isamarkupfalse% |
|
1111 \ postfix{\isacharunderscore}appendI{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ zs\ {\isacharat}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1112 % |
|
1113 \isadelimproof |
|
1114 \ \ % |
|
1115 \endisadelimproof |
|
1116 % |
|
1117 \isatagproof |
|
1118 \isacommand{by}\isamarkupfalse% |
|
1119 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1120 \endisatagproof |
|
1121 {\isafoldproof}% |
|
1122 % |
|
1123 \isadelimproof |
|
1124 \isanewline |
|
1125 % |
|
1126 \endisadelimproof |
|
1127 \isacommand{lemma}\isamarkupfalse% |
|
1128 \ postfix{\isacharunderscore}appendD{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ zs\ {\isacharat}\ ys\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1129 % |
|
1130 \isadelimproof |
|
1131 \ \ % |
|
1132 \endisadelimproof |
|
1133 % |
|
1134 \isatagproof |
|
1135 \isacommand{by}\isamarkupfalse% |
|
1136 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ postfix{\isacharunderscore}def{\isacharparenright}% |
|
1137 \endisatagproof |
|
1138 {\isafoldproof}% |
|
1139 % |
|
1140 \isadelimproof |
|
1141 \isanewline |
|
1142 % |
|
1143 \endisadelimproof |
|
1144 \isanewline |
|
1145 \isacommand{lemma}\isamarkupfalse% |
|
1146 \ postfix{\isacharunderscore}is{\isacharunderscore}subset{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ set\ ys\ {\isasymsubseteq}\ set\ xs{\isachardoublequoteclose}\isanewline |
|
1147 % |
|
1148 \isadelimproof |
|
1149 % |
|
1150 \endisadelimproof |
|
1151 % |
|
1152 \isatagproof |
|
1153 \isacommand{proof}\isamarkupfalse% |
|
1154 \ {\isacharminus}\isanewline |
|
1155 \ \ \isacommand{assume}\isamarkupfalse% |
|
1156 \ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1157 \ \ \isacommand{then}\isamarkupfalse% |
|
1158 \ \isacommand{obtain}\isamarkupfalse% |
|
1159 \ zs\ \isakeyword{where}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
1160 \isanewline |
|
1161 \ \ \isacommand{then}\isamarkupfalse% |
|
1162 \ \isacommand{show}\isamarkupfalse% |
|
1163 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
1164 \ {\isacharparenleft}induct\ zs{\isacharparenright}\ auto\isanewline |
|
1165 \isacommand{qed}\isamarkupfalse% |
|
1166 % |
|
1167 \endisatagproof |
|
1168 {\isafoldproof}% |
|
1169 % |
|
1170 \isadelimproof |
|
1171 \isanewline |
|
1172 % |
|
1173 \endisadelimproof |
|
1174 \isanewline |
|
1175 \isacommand{lemma}\isamarkupfalse% |
|
1176 \ postfix{\isacharunderscore}ConsD{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}x{\isacharhash}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ y{\isacharhash}ys\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1177 % |
|
1178 \isadelimproof |
|
1179 % |
|
1180 \endisadelimproof |
|
1181 % |
|
1182 \isatagproof |
|
1183 \isacommand{proof}\isamarkupfalse% |
|
1184 \ {\isacharminus}\isanewline |
|
1185 \ \ \isacommand{assume}\isamarkupfalse% |
|
1186 \ {\isachardoublequoteopen}x{\isacharhash}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ y{\isacharhash}ys{\isachardoublequoteclose}\isanewline |
|
1187 \ \ \isacommand{then}\isamarkupfalse% |
|
1188 \ \isacommand{obtain}\isamarkupfalse% |
|
1189 \ zs\ \isakeyword{where}\ {\isachardoublequoteopen}x{\isacharhash}xs\ {\isacharequal}\ zs\ {\isacharat}\ y{\isacharhash}ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
1190 \isanewline |
|
1191 \ \ \isacommand{then}\isamarkupfalse% |
|
1192 \ \isacommand{show}\isamarkupfalse% |
|
1193 \ {\isacharquery}thesis\isanewline |
|
1194 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
1195 \ {\isacharparenleft}induct\ zs{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharbang}{\isacharcolon}\ postfix{\isacharunderscore}appendI\ postfix{\isacharunderscore}ConsI{\isacharparenright}\isanewline |
|
1196 \isacommand{qed}\isamarkupfalse% |
|
1197 % |
|
1198 \endisatagproof |
|
1199 {\isafoldproof}% |
|
1200 % |
|
1201 \isadelimproof |
|
1202 \isanewline |
|
1203 % |
|
1204 \endisadelimproof |
|
1205 \isanewline |
|
1206 \isacommand{lemma}\isamarkupfalse% |
|
1207 \ postfix{\isacharunderscore}to{\isacharunderscore}prefix{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymlongleftrightarrow}\ rev\ ys\ {\isasymle}\ rev\ xs{\isachardoublequoteclose}\isanewline |
|
1208 % |
|
1209 \isadelimproof |
|
1210 % |
|
1211 \endisadelimproof |
|
1212 % |
|
1213 \isatagproof |
|
1214 \isacommand{proof}\isamarkupfalse% |
|
1215 \isanewline |
|
1216 \ \ \isacommand{assume}\isamarkupfalse% |
|
1217 \ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\isanewline |
|
1218 \ \ \isacommand{then}\isamarkupfalse% |
|
1219 \ \isacommand{obtain}\isamarkupfalse% |
|
1220 \ zs\ \isakeyword{where}\ {\isachardoublequoteopen}xs\ {\isacharequal}\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
1221 \isanewline |
|
1222 \ \ \isacommand{then}\isamarkupfalse% |
|
1223 \ \isacommand{have}\isamarkupfalse% |
|
1224 \ {\isachardoublequoteopen}rev\ xs\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ zs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
1225 \ simp\isanewline |
|
1226 \ \ \isacommand{then}\isamarkupfalse% |
|
1227 \ \isacommand{show}\isamarkupfalse% |
|
1228 \ {\isachardoublequoteopen}rev\ ys\ {\isacharless}{\isacharequal}\ rev\ xs{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
1229 \isanewline |
|
1230 \isacommand{next}\isamarkupfalse% |
|
1231 \isanewline |
|
1232 \ \ \isacommand{assume}\isamarkupfalse% |
|
1233 \ {\isachardoublequoteopen}rev\ ys\ {\isacharless}{\isacharequal}\ rev\ xs{\isachardoublequoteclose}\isanewline |
|
1234 \ \ \isacommand{then}\isamarkupfalse% |
|
1235 \ \isacommand{obtain}\isamarkupfalse% |
|
1236 \ zs\ \isakeyword{where}\ {\isachardoublequoteopen}rev\ xs\ {\isacharequal}\ rev\ ys\ {\isacharat}\ zs{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
1237 \isanewline |
|
1238 \ \ \isacommand{then}\isamarkupfalse% |
|
1239 \ \isacommand{have}\isamarkupfalse% |
|
1240 \ {\isachardoublequoteopen}rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ zs\ {\isacharat}\ rev\ {\isacharparenleft}rev\ ys{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
1241 \ simp\isanewline |
|
1242 \ \ \isacommand{then}\isamarkupfalse% |
|
1243 \ \isacommand{have}\isamarkupfalse% |
|
1244 \ {\isachardoublequoteopen}xs\ {\isacharequal}\ rev\ zs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
1245 \ simp\isanewline |
|
1246 \ \ \isacommand{then}\isamarkupfalse% |
|
1247 \ \isacommand{show}\isamarkupfalse% |
|
1248 \ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
1249 \isanewline |
|
1250 \isacommand{qed}\isamarkupfalse% |
|
1251 % |
|
1252 \endisatagproof |
|
1253 {\isafoldproof}% |
|
1254 % |
|
1255 \isadelimproof |
|
1256 \isanewline |
|
1257 % |
|
1258 \endisadelimproof |
|
1259 \isanewline |
|
1260 \isacommand{lemma}\isamarkupfalse% |
|
1261 \ distinct{\isacharunderscore}postfix{\isacharcolon}\ {\isachardoublequoteopen}distinct\ xs\ {\isasymLongrightarrow}\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ distinct\ ys{\isachardoublequoteclose}\isanewline |
|
1262 % |
|
1263 \isadelimproof |
|
1264 \ \ % |
|
1265 \endisadelimproof |
|
1266 % |
|
1267 \isatagproof |
|
1268 \isacommand{by}\isamarkupfalse% |
|
1269 \ {\isacharparenleft}clarsimp\ elim{\isacharbang}{\isacharcolon}\ postfixE{\isacharparenright}% |
|
1270 \endisatagproof |
|
1271 {\isafoldproof}% |
|
1272 % |
|
1273 \isadelimproof |
|
1274 \isanewline |
|
1275 % |
|
1276 \endisadelimproof |
|
1277 \isanewline |
|
1278 \isacommand{lemma}\isamarkupfalse% |
|
1279 \ postfix{\isacharunderscore}map{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ map\ f\ xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ map\ f\ ys{\isachardoublequoteclose}\isanewline |
|
1280 % |
|
1281 \isadelimproof |
|
1282 \ \ % |
|
1283 \endisadelimproof |
|
1284 % |
|
1285 \isatagproof |
|
1286 \isacommand{by}\isamarkupfalse% |
|
1287 \ {\isacharparenleft}auto\ elim{\isacharbang}{\isacharcolon}\ postfixE\ intro{\isacharcolon}\ postfixI{\isacharparenright}% |
|
1288 \endisatagproof |
|
1289 {\isafoldproof}% |
|
1290 % |
|
1291 \isadelimproof |
|
1292 \isanewline |
|
1293 % |
|
1294 \endisadelimproof |
|
1295 \isanewline |
|
1296 \isacommand{lemma}\isamarkupfalse% |
|
1297 \ postfix{\isacharunderscore}drop{\isacharcolon}\ {\isachardoublequoteopen}as\ {\isachargreater}{\isachargreater}{\isacharequal}\ drop\ n\ as{\isachardoublequoteclose}\isanewline |
|
1298 % |
|
1299 \isadelimproof |
|
1300 \ \ % |
|
1301 \endisadelimproof |
|
1302 % |
|
1303 \isatagproof |
|
1304 \isacommand{unfolding}\isamarkupfalse% |
|
1305 \ postfix{\isacharunderscore}def\isanewline |
|
1306 \ \ \isacommand{apply}\isamarkupfalse% |
|
1307 \ {\isacharparenleft}rule\ exI\ {\isacharbrackleft}\isakeyword{where}\ x\ {\isacharequal}\ {\isachardoublequoteopen}take\ n\ as{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline |
|
1308 \ \ \isacommand{apply}\isamarkupfalse% |
|
1309 \ simp\isanewline |
|
1310 \ \ \isacommand{done}\isamarkupfalse% |
|
1311 % |
|
1312 \endisatagproof |
|
1313 {\isafoldproof}% |
|
1314 % |
|
1315 \isadelimproof |
|
1316 \isanewline |
|
1317 % |
|
1318 \endisadelimproof |
|
1319 \isanewline |
|
1320 \isacommand{lemma}\isamarkupfalse% |
|
1321 \ postfix{\isacharunderscore}take{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isachargreater}{\isachargreater}{\isacharequal}\ ys\ {\isasymLongrightarrow}\ xs\ {\isacharequal}\ take\ {\isacharparenleft}length\ xs\ {\isacharminus}\ length\ ys{\isacharparenright}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline |
|
1322 % |
|
1323 \isadelimproof |
|
1324 \ \ % |
|
1325 \endisadelimproof |
|
1326 % |
|
1327 \isatagproof |
|
1328 \isacommand{by}\isamarkupfalse% |
|
1329 \ {\isacharparenleft}clarsimp\ elim{\isacharbang}{\isacharcolon}\ postfixE{\isacharparenright}% |
|
1330 \endisatagproof |
|
1331 {\isafoldproof}% |
|
1332 % |
|
1333 \isadelimproof |
|
1334 \isanewline |
|
1335 % |
|
1336 \endisadelimproof |
|
1337 \isanewline |
|
1338 \isacommand{lemma}\isamarkupfalse% |
|
1339 \ parallelD{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymparallel}\ y\ {\isasymLongrightarrow}\ {\isasymnot}\ x\ {\isasymle}\ y{\isachardoublequoteclose}\isanewline |
|
1340 % |
|
1341 \isadelimproof |
|
1342 \ \ % |
|
1343 \endisadelimproof |
|
1344 % |
|
1345 \isatagproof |
|
1346 \isacommand{by}\isamarkupfalse% |
|
1347 \ blast% |
|
1348 \endisatagproof |
|
1349 {\isafoldproof}% |
|
1350 % |
|
1351 \isadelimproof |
|
1352 \isanewline |
|
1353 % |
|
1354 \endisadelimproof |
|
1355 \isanewline |
|
1356 \isacommand{lemma}\isamarkupfalse% |
|
1357 \ parallelD{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymparallel}\ y\ {\isasymLongrightarrow}\ {\isasymnot}\ y\ {\isasymle}\ x{\isachardoublequoteclose}\isanewline |
|
1358 % |
|
1359 \isadelimproof |
|
1360 \ \ % |
|
1361 \endisadelimproof |
|
1362 % |
|
1363 \isatagproof |
|
1364 \isacommand{by}\isamarkupfalse% |
|
1365 \ blast% |
|
1366 \endisatagproof |
|
1367 {\isafoldproof}% |
|
1368 % |
|
1369 \isadelimproof |
|
1370 \isanewline |
|
1371 % |
|
1372 \endisadelimproof |
|
1373 \isanewline |
|
1374 \isacommand{lemma}\isamarkupfalse% |
|
1375 \ parallel{\isacharunderscore}Nil{\isadigit{1}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ x\ {\isasymparallel}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
1376 % |
|
1377 \isadelimproof |
|
1378 \ \ % |
|
1379 \endisadelimproof |
|
1380 % |
|
1381 \isatagproof |
|
1382 \isacommand{unfolding}\isamarkupfalse% |
|
1383 \ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
1384 \ simp% |
|
1385 \endisatagproof |
|
1386 {\isafoldproof}% |
|
1387 % |
|
1388 \isadelimproof |
|
1389 \isanewline |
|
1390 % |
|
1391 \endisadelimproof |
|
1392 \isanewline |
|
1393 \isacommand{lemma}\isamarkupfalse% |
|
1394 \ parallel{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymparallel}\ x{\isachardoublequoteclose}\isanewline |
|
1395 % |
|
1396 \isadelimproof |
|
1397 \ \ % |
|
1398 \endisadelimproof |
|
1399 % |
|
1400 \isatagproof |
|
1401 \isacommand{unfolding}\isamarkupfalse% |
|
1402 \ parallel{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
1403 \ simp% |
|
1404 \endisatagproof |
|
1405 {\isafoldproof}% |
|
1406 % |
|
1407 \isadelimproof |
|
1408 \isanewline |
|
1409 % |
|
1410 \endisadelimproof |
|
1411 \isanewline |
|
1412 \isacommand{lemma}\isamarkupfalse% |
|
1413 \ Cons{\isacharunderscore}parallelI{\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymnoteq}\ b\ {\isasymLongrightarrow}\ a\ {\isacharhash}\ as\ {\isasymparallel}\ b\ {\isacharhash}\ bs{\isachardoublequoteclose}\isanewline |
|
1414 % |
|
1415 \isadelimproof |
|
1416 \ \ % |
|
1417 \endisadelimproof |
|
1418 % |
|
1419 \isatagproof |
|
1420 \isacommand{by}\isamarkupfalse% |
|
1421 \ auto% |
|
1422 \endisatagproof |
|
1423 {\isafoldproof}% |
|
1424 % |
|
1425 \isadelimproof |
|
1426 \isanewline |
|
1427 % |
|
1428 \endisadelimproof |
|
1429 \isanewline |
|
1430 \isacommand{lemma}\isamarkupfalse% |
|
1431 \ Cons{\isacharunderscore}parallelI{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ a\ {\isacharequal}\ b{\isacharsemicolon}\ as\ {\isasymparallel}\ bs\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a\ {\isacharhash}\ as\ {\isasymparallel}\ b\ {\isacharhash}\ bs{\isachardoublequoteclose}\isanewline |
|
1432 % |
|
1433 \isadelimproof |
|
1434 \ \ % |
|
1435 \endisadelimproof |
|
1436 % |
|
1437 \isatagproof |
|
1438 \isacommand{by}\isamarkupfalse% |
|
1439 \ {\isacharparenleft}metis\ Cons{\isacharunderscore}prefix{\isacharunderscore}Cons\ parallelE\ parallelI{\isacharparenright}% |
|
1440 \endisatagproof |
|
1441 {\isafoldproof}% |
|
1442 % |
|
1443 \isadelimproof |
|
1444 \isanewline |
|
1445 % |
|
1446 \endisadelimproof |
|
1447 \isanewline |
|
1448 \isacommand{lemma}\isamarkupfalse% |
|
1449 \ not{\isacharunderscore}equal{\isacharunderscore}is{\isacharunderscore}parallel{\isacharcolon}\isanewline |
|
1450 \ \ \isakeyword{assumes}\ neq{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline |
|
1451 \ \ \ \ \isakeyword{and}\ len{\isacharcolon}\ {\isachardoublequoteopen}length\ xs\ {\isacharequal}\ length\ ys{\isachardoublequoteclose}\isanewline |
|
1452 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}xs\ {\isasymparallel}\ ys{\isachardoublequoteclose}\isanewline |
|
1453 % |
|
1454 \isadelimproof |
|
1455 \ \ % |
|
1456 \endisadelimproof |
|
1457 % |
|
1458 \isatagproof |
|
1459 \isacommand{using}\isamarkupfalse% |
|
1460 \ len\ neq\isanewline |
|
1461 \isacommand{proof}\isamarkupfalse% |
|
1462 \ {\isacharparenleft}induct\ rule{\isacharcolon}\ list{\isacharunderscore}induct{\isadigit{2}}{\isacharparenright}\isanewline |
|
1463 \ \ \isacommand{case}\isamarkupfalse% |
|
1464 \ Nil\isanewline |
|
1465 \ \ \isacommand{then}\isamarkupfalse% |
|
1466 \ \isacommand{show}\isamarkupfalse% |
|
1467 \ {\isacharquery}case\ \isacommand{by}\isamarkupfalse% |
|
1468 \ simp\isanewline |
|
1469 \isacommand{next}\isamarkupfalse% |
|
1470 \isanewline |
|
1471 \ \ \isacommand{case}\isamarkupfalse% |
|
1472 \ {\isacharparenleft}Cons\ a\ as\ b\ bs{\isacharparenright}\isanewline |
|
1473 \ \ \isacommand{have}\isamarkupfalse% |
|
1474 \ ih{\isacharcolon}\ {\isachardoublequoteopen}as\ {\isasymnoteq}\ bs\ {\isasymLongrightarrow}\ as\ {\isasymparallel}\ bs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
1475 \ fact\isanewline |
|
1476 \ \ \isacommand{show}\isamarkupfalse% |
|
1477 \ {\isacharquery}case\isanewline |
|
1478 \ \ \isacommand{proof}\isamarkupfalse% |
|
1479 \ {\isacharparenleft}cases\ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
1480 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1481 \ True\isanewline |
|
1482 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1483 \ \isacommand{have}\isamarkupfalse% |
|
1484 \ {\isachardoublequoteopen}as\ {\isasymnoteq}\ bs{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
|
1485 \ Cons\ \isacommand{by}\isamarkupfalse% |
|
1486 \ simp\isanewline |
|
1487 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1488 \ \isacommand{show}\isamarkupfalse% |
|
1489 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
1490 \ {\isacharparenleft}rule\ Cons{\isacharunderscore}parallelI{\isadigit{2}}\ {\isacharbrackleft}OF\ True\ ih{\isacharbrackright}{\isacharparenright}\isanewline |
|
1491 \ \ \isacommand{next}\isamarkupfalse% |
|
1492 \isanewline |
|
1493 \ \ \ \ \isacommand{case}\isamarkupfalse% |
|
1494 \ False\isanewline |
|
1495 \ \ \ \ \isacommand{then}\isamarkupfalse% |
|
1496 \ \isacommand{show}\isamarkupfalse% |
|
1497 \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% |
|
1498 \ {\isacharparenleft}rule\ Cons{\isacharunderscore}parallelI{\isadigit{1}}{\isacharparenright}\isanewline |
|
1499 \ \ \isacommand{qed}\isamarkupfalse% |
|
1500 \isanewline |
|
1501 \isacommand{qed}\isamarkupfalse% |
|
1502 % |
|
1503 \endisatagproof |
|
1504 {\isafoldproof}% |
|
1505 % |
|
1506 \isadelimproof |
|
1507 % |
|
1508 \endisadelimproof |
|
1509 % |
|
1510 \isamarkupsubsection{Executable code% |
|
1511 } |
|
1512 \isamarkuptrue% |
|
1513 \isacommand{lemma}\isamarkupfalse% |
|
1514 \ less{\isacharunderscore}eq{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
1515 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ list{\isacharparenright}\ {\isasymle}\ xs\ {\isasymlongleftrightarrow}\ True{\isachardoublequoteclose}\isanewline |
|
1516 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharhash}\ xs\ {\isasymle}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ False{\isachardoublequoteclose}\isanewline |
|
1517 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharhash}\ xs\ {\isasymle}\ y\ {\isacharhash}\ ys\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isasymle}\ ys{\isachardoublequoteclose}\isanewline |
|
1518 % |
|
1519 \isadelimproof |
|
1520 \ \ % |
|
1521 \endisadelimproof |
|
1522 % |
|
1523 \isatagproof |
|
1524 \isacommand{by}\isamarkupfalse% |
|
1525 \ simp{\isacharunderscore}all% |
|
1526 \endisatagproof |
|
1527 {\isafoldproof}% |
|
1528 % |
|
1529 \isadelimproof |
|
1530 \isanewline |
|
1531 % |
|
1532 \endisadelimproof |
|
1533 \isanewline |
|
1534 \isacommand{lemma}\isamarkupfalse% |
|
1535 \ less{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline |
|
1536 \ \ \ \ {\isachardoublequoteopen}xs\ {\isacharless}\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ list{\isacharparenright}\ {\isasymlongleftrightarrow}\ False{\isachardoublequoteclose}\isanewline |
|
1537 \ \ \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}{\isacharhash}\ xs\ {\isasymlongleftrightarrow}\ True{\isachardoublequoteclose}\isanewline |
|
1538 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharhash}\ xs\ {\isacharless}\ y\ {\isacharhash}\ ys\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y\ {\isasymand}\ xs\ {\isacharless}\ ys{\isachardoublequoteclose}\isanewline |
|
1539 % |
|
1540 \isadelimproof |
|
1541 \ \ % |
|
1542 \endisadelimproof |
|
1543 % |
|
1544 \isatagproof |
|
1545 \isacommand{unfolding}\isamarkupfalse% |
|
1546 \ strict{\isacharunderscore}prefix{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
1547 \ auto% |
|
1548 \endisatagproof |
|
1549 {\isafoldproof}% |
|
1550 % |
|
1551 \isadelimproof |
|
1552 \isanewline |
|
1553 % |
|
1554 \endisadelimproof |
|
1555 \isanewline |
|
1556 \isacommand{lemmas}\isamarkupfalse% |
|
1557 \ {\isacharbrackleft}code{\isacharbrackright}\ {\isacharequal}\ postfix{\isacharunderscore}to{\isacharunderscore}prefix\isanewline |
|
1558 % |
|
1559 \isadelimtheory |
|
1560 \isanewline |
|
1561 % |
|
1562 \endisadelimtheory |
|
1563 % |
|
1564 \isatagtheory |
|
1565 \isacommand{end}\isamarkupfalse% |
|
1566 % |
|
1567 \endisatagtheory |
|
1568 {\isafoldtheory}% |
|
1569 % |
|
1570 \isadelimtheory |
|
1571 \isanewline |
|
1572 % |
|
1573 \endisadelimtheory |
|
1574 \end{isabellebody}% |
|
1575 %%% Local Variables: |
|
1576 %%% mode: latex |
|
1577 %%% TeX-master: "root" |
|
1578 %%% End: |