15 simplification rules. |
28 simplification rules. |
16 |
29 |
17 Isabelle may fail to prove the termination condition for some |
30 Isabelle may fail to prove the termination condition for some |
18 recursive call. Let us try to define Quicksort:% |
31 recursive call. Let us try to define Quicksort:% |
19 \end{isamarkuptext}% |
32 \end{isamarkuptext}% |
20 \isamarkuptrue% |
33 \isamarkupfalse% |
21 \isacommand{consts}\ qs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline |
34 \isacommand{consts}\ qs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline |
22 \isamarkupfalse% |
35 \isamarkupfalse% |
23 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
36 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
24 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
37 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
25 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
38 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
26 % |
39 % |
27 \begin{isamarkuptext}% |
40 \begin{isamarkuptext}% |
28 \noindent where \isa{filter} is predefined and \isa{filter\ P\ xs} |
41 \noindent where \isa{filter} is predefined and \isa{filter\ P\ xs} |
29 is the list of elements of \isa{xs} satisfying \isa{P}. |
42 is the list of elements of \isa{xs} satisfying \isa{P}. |
30 This definition of \isa{qs} fails, and Isabelle prints an error message |
43 This definition of \isa{qs} fails, and Isabelle prints an error message |
44 proved). Because \isacommand{recdef}'s termination prover involves |
57 proved). Because \isacommand{recdef}'s termination prover involves |
45 simplification, we include in our second attempt a hint: the |
58 simplification, we include in our second attempt a hint: the |
46 \attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a |
59 \attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a |
47 simplification rule.\cmmdx{hints}% |
60 simplification rule.\cmmdx{hints}% |
48 \end{isamarkuptext}% |
61 \end{isamarkuptext}% |
49 \isamarkuptrue% |
|
50 \isamarkupfalse% |
|
51 \isamarkupfalse% |
62 \isamarkupfalse% |
52 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
63 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
53 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
64 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
54 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
65 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
55 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse% |
66 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkuptrue% |
56 \isamarkupfalse% |
|
57 % |
67 % |
58 \begin{isamarkuptext}% |
68 \begin{isamarkuptext}% |
59 \noindent |
69 \noindent |
60 This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely |
70 This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely |
61 the stated recursion equations for \isa{qs} and they have become |
71 the stated recursion equations for \isa{qs} and they have become |
62 simplification rules. |
72 simplification rules. |
63 Thus we can automatically prove results such as this one:% |
73 Thus we can automatically prove results such as this one:% |
64 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
65 \isamarkuptrue% |
75 \isamarkupfalse% |
66 \isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline |
76 \isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline |
|
77 % |
|
78 \isadelimproof |
|
79 % |
|
80 \endisadelimproof |
|
81 % |
|
82 \isatagproof |
67 \isamarkupfalse% |
83 \isamarkupfalse% |
68 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
84 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
69 \isamarkupfalse% |
85 \isamarkupfalse% |
70 \isacommand{done}\isamarkupfalse% |
86 \isacommand{done}% |
|
87 \endisatagproof |
|
88 {\isafoldproof}% |
|
89 % |
|
90 \isadelimproof |
|
91 % |
|
92 \endisadelimproof |
|
93 \isamarkuptrue% |
71 % |
94 % |
72 \begin{isamarkuptext}% |
95 \begin{isamarkuptext}% |
73 \noindent |
96 \noindent |
74 More exciting theorems require induction, which is discussed below. |
97 More exciting theorems require induction, which is discussed below. |
75 |
98 |
76 If the termination proof requires a lemma that is of general use, you can |
99 If the termination proof requires a lemma that is of general use, you can |
77 turn it permanently into a simplification rule, in which case the above |
100 turn it permanently into a simplification rule, in which case the above |
78 \isacommand{hint} is not necessary. But in the case of |
101 \isacommand{hint} is not necessary. But in the case of |
79 \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.% |
102 \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.% |
80 \end{isamarkuptext}% |
103 \end{isamarkuptext}% |
81 \isamarkuptrue% |
104 % |
82 \isamarkupfalse% |
105 \isadelimtheory |
|
106 % |
|
107 \endisadelimtheory |
|
108 % |
|
109 \isatagtheory |
|
110 % |
|
111 \endisatagtheory |
|
112 {\isafoldtheory}% |
|
113 % |
|
114 \isadelimtheory |
|
115 % |
|
116 \endisadelimtheory |
83 \end{isabellebody}% |
117 \end{isabellebody}% |
84 %%% Local Variables: |
118 %%% Local Variables: |
85 %%% mode: latex |
119 %%% mode: latex |
86 %%% TeX-master: "root" |
120 %%% TeX-master: "root" |
87 %%% End: |
121 %%% End: |