63 \noindent The runtime of the corresponding code grows exponential due |
63 \noindent The runtime of the corresponding code grows exponential due |
64 to two recursive calls:% |
64 to two recursive calls:% |
65 \end{isamarkuptext}% |
65 \end{isamarkuptext}% |
66 \isamarkuptrue% |
66 \isamarkuptrue% |
67 % |
67 % |
68 \isadelimquote |
68 \isadelimtypewriter |
69 % |
69 % |
70 \endisadelimquote |
70 \endisadelimtypewriter |
71 % |
71 % |
72 \isatagquote |
72 \isatagtypewriter |
73 % |
73 % |
74 \begin{isamarkuptext}% |
74 \begin{isamarkuptext}% |
75 \begin{typewriter} |
75 fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
76 fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
|
77 fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline |
76 fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline |
78 fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline |
77 fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline |
79 fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon} |
78 fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline% |
80 \end{typewriter}% |
79 \end{isamarkuptext}% |
81 \end{isamarkuptext}% |
80 \isamarkuptrue% |
82 \isamarkuptrue% |
81 % |
83 % |
82 \endisatagtypewriter |
84 \endisatagquote |
83 {\isafoldtypewriter}% |
85 {\isafoldquote}% |
84 % |
86 % |
85 \isadelimtypewriter |
87 \isadelimquote |
86 % |
88 % |
87 \endisadelimtypewriter |
89 \endisadelimquote |
|
90 % |
88 % |
91 \begin{isamarkuptext}% |
89 \begin{isamarkuptext}% |
92 \noindent A more efficient implementation would use dynamic |
90 \noindent A more efficient implementation would use dynamic |
93 programming, e.g.~sharing of common intermediate results between |
91 programming, e.g.~sharing of common intermediate results between |
94 recursive calls. This idea is expressed by an auxiliary operation |
92 recursive calls. This idea is expressed by an auxiliary operation |
161 \begin{isamarkuptext}% |
159 \begin{isamarkuptext}% |
162 \noindent The resulting code shows only linear growth of runtime:% |
160 \noindent The resulting code shows only linear growth of runtime:% |
163 \end{isamarkuptext}% |
161 \end{isamarkuptext}% |
164 \isamarkuptrue% |
162 \isamarkuptrue% |
165 % |
163 % |
166 \isadelimquote |
164 \isadelimtypewriter |
167 % |
165 % |
168 \endisadelimquote |
166 \endisadelimtypewriter |
169 % |
167 % |
170 \isatagquote |
168 \isatagtypewriter |
171 % |
169 % |
172 \begin{isamarkuptext}% |
170 \begin{isamarkuptext}% |
173 \begin{typewriter} |
171 fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline |
174 fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline |
|
175 fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline |
172 fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline |
176 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline |
173 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline |
177 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline |
174 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline |
178 fib{\isacharunderscore}step\ Zero{\isacharunderscore}nat\ {\isacharequal}\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharsemicolon}\isanewline |
175 fib{\isacharunderscore}step\ Zero{\isacharunderscore}nat\ {\isacharequal}\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharsemicolon}\isanewline |
179 \isanewline |
176 \isanewline |
180 fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
177 fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
181 fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline |
178 fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline |
182 fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon} |
179 fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline% |
183 \end{typewriter}% |
180 \end{isamarkuptext}% |
184 \end{isamarkuptext}% |
181 \isamarkuptrue% |
185 \isamarkuptrue% |
182 % |
186 % |
183 \endisatagtypewriter |
187 \endisatagquote |
184 {\isafoldtypewriter}% |
188 {\isafoldquote}% |
185 % |
189 % |
186 \isadelimtypewriter |
190 \isadelimquote |
187 % |
191 % |
188 \endisadelimtypewriter |
192 \endisadelimquote |
|
193 % |
189 % |
194 \isamarkupsubsection{Datatype refinement% |
190 \isamarkupsubsection{Datatype refinement% |
195 } |
191 } |
196 \isamarkuptrue% |
192 \isamarkuptrue% |
197 % |
193 % |
339 \begin{isamarkuptext}% |
335 \begin{isamarkuptext}% |
340 \noindent The resulting code looks as expected:% |
336 \noindent The resulting code looks as expected:% |
341 \end{isamarkuptext}% |
337 \end{isamarkuptext}% |
342 \isamarkuptrue% |
338 \isamarkuptrue% |
343 % |
339 % |
344 \isadelimquote |
340 \isadelimtypewriter |
345 % |
341 % |
346 \endisadelimquote |
342 \endisadelimtypewriter |
347 % |
343 % |
348 \isatagquote |
344 \isatagtypewriter |
349 % |
345 % |
350 \begin{isamarkuptext}% |
346 \begin{isamarkuptext}% |
351 \begin{typewriter} |
347 structure\ Example\ {\isacharcolon}\ sig\isanewline |
352 structure\ Example\ {\isacharcolon}\ sig\isanewline |
|
353 \ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
348 \ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
354 \ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline |
349 \ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline |
355 \ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline |
350 \ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline |
356 \ \ val\ null\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ bool\isanewline |
351 \ \ val\ null\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ bool\isanewline |
357 \ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline |
352 \ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline |
379 \ \ \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
374 \ \ \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
380 \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
375 \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
381 \isanewline |
376 \isanewline |
382 fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline |
377 fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline |
383 \isanewline |
378 \isanewline |
384 end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline |
379 end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% |
385 |
380 \end{isamarkuptext}% |
386 \end{typewriter}% |
381 \isamarkuptrue% |
387 \end{isamarkuptext}% |
382 % |
388 \isamarkuptrue% |
383 \endisatagtypewriter |
389 % |
384 {\isafoldtypewriter}% |
390 \endisatagquote |
385 % |
391 {\isafoldquote}% |
386 \isadelimtypewriter |
392 % |
387 % |
393 \isadelimquote |
388 \endisadelimtypewriter |
394 % |
|
395 \endisadelimquote |
|
396 % |
389 % |
397 \begin{isamarkuptext}% |
390 \begin{isamarkuptext}% |
398 The same techniques can also be applied to types which are not |
391 The same techniques can also be applied to types which are not |
399 specified as datatypes, e.g.~type \isa{int} is originally specified |
392 specified as datatypes, e.g.~type \isa{int} is originally specified |
400 as quotient type by means of \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}}, but for code |
393 as quotient type by means of \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}}, but for code |
576 \begin{isamarkuptext}% |
569 \begin{isamarkuptext}% |
577 \noindent Then the corresponding code is as follows:% |
570 \noindent Then the corresponding code is as follows:% |
578 \end{isamarkuptext}% |
571 \end{isamarkuptext}% |
579 \isamarkuptrue% |
572 \isamarkuptrue% |
580 % |
573 % |
581 \isadelimquote |
574 \isadelimtypewriter |
582 % |
575 % |
583 \endisadelimquote |
576 \endisadelimtypewriter |
584 % |
577 % |
585 \isatagquote |
578 \isatagtypewriter |
586 % |
579 % |
587 \begin{isamarkuptext}% |
580 \begin{isamarkuptext}% |
588 \begin{typewriter} |
581 module\ Example\ where\ {\isacharbraceleft}\isanewline |
589 module\ Example\ where\ {\isacharbraceleft}\isanewline |
|
590 \isanewline |
582 \isanewline |
591 newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline |
583 newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline |
592 \isanewline |
584 \isanewline |
593 empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a{\isacharsemicolon}\isanewline |
585 empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Dlist\ a{\isacharsemicolon}\isanewline |
594 empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline |
586 empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline |
611 remove{\isadigit{1}}\ x\ {\isacharparenleft}y\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isacharequal}{\isacharequal}\ y\ then\ xs\ else\ y\ {\isacharcolon}\ remove{\isadigit{1}}\ x\ xs{\isacharparenright}{\isacharsemicolon}\isanewline |
603 remove{\isadigit{1}}\ x\ {\isacharparenleft}y\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isacharequal}{\isacharequal}\ y\ then\ xs\ else\ y\ {\isacharcolon}\ remove{\isadigit{1}}\ x\ xs{\isacharparenright}{\isacharsemicolon}\isanewline |
612 \isanewline |
604 \isanewline |
613 remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline |
605 remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline |
614 remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
606 remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
615 \isanewline |
607 \isanewline |
616 {\isacharbraceright}\isanewline |
608 {\isacharbraceright}\isanewline% |
617 |
609 \end{isamarkuptext}% |
618 \end{typewriter}% |
610 \isamarkuptrue% |
619 \end{isamarkuptext}% |
611 % |
620 \isamarkuptrue% |
612 \endisatagtypewriter |
621 % |
613 {\isafoldtypewriter}% |
622 \endisatagquote |
614 % |
623 {\isafoldquote}% |
615 \isadelimtypewriter |
624 % |
616 % |
625 \isadelimquote |
617 \endisadelimtypewriter |
626 % |
|
627 \endisadelimquote |
|
628 % |
618 % |
629 \begin{isamarkuptext}% |
619 \begin{isamarkuptext}% |
630 Typical data structures implemented by representations involving |
620 Typical data structures implemented by representations involving |
631 invariants are available in the library, e.g.~theories \hyperlink{theory.Fset}{\mbox{\isa{Fset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isacharprime}a\ fset}) and |
621 invariants are available in the library, e.g.~theories \hyperlink{theory.Fset}{\mbox{\isa{Fset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isacharprime}a\ fset}) and |
632 key-value-mappings (type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ mapping}) respectively; |
622 key-value-mappings (type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ mapping}) respectively; |