98 \begin{isabelle}% |
98 \begin{isabelle}% |
99 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline |
99 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline |
100 \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k% |
100 \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k% |
101 \end{isabelle} |
101 \end{isabelle} |
102 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, |
102 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, |
103 \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the |
103 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the |
104 integer 1 (see \S\ref{sec:numbers}). |
104 integer 1 (see \S\ref{sec:numbers}). |
105 |
105 |
106 First we show that the our specific function, the difference between the |
106 First we show that the our specific function, the difference between the |
107 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every |
107 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every |
108 move to the right. At this point we also start generalizing from \isa{a}'s |
108 move to the right. At this point we also start generalizing from \isa{a}'s |
109 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have |
109 and \isa{b}'s to an arbitrary property \isa{P}. Otherwise we would have |
110 to prove the desired lemma twice, once as stated above and once with the |
110 to prove the desired lemma twice, once as stated above and once with the |
111 roles of \isa{a}'s and \isa{b}'s interchanged.% |
111 roles of \isa{a}'s and \isa{b}'s interchanged.% |
112 \end{isamarkuptext}% |
112 \end{isamarkuptext}% |
113 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
113 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
114 \ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline |
114 \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
115 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline |
115 \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}% |
116 \ \ \ \ \ \ {\isacharminus}\isanewline |
|
117 \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline |
|
118 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}% |
|
119 \begin{isamarkuptxt}% |
116 \begin{isamarkuptxt}% |
120 \noindent |
117 \noindent |
121 The lemma is a bit hard to read because of the coercion function |
118 The lemma is a bit hard to read because of the coercion function |
122 \isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns |
119 \isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns |
123 a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing. |
120 a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing. |
124 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of |
121 Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of |
125 length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which |
122 length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which |
126 is what remains after that prefix has been dropped from \isa{xs}. |
123 is what remains after that prefix has been dropped from \isa{xs}. |
127 |
124 |
139 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
136 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
140 \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline |
137 \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline |
141 \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}% |
138 \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}% |
142 \begin{isamarkuptxt}% |
139 \begin{isamarkuptxt}% |
143 \noindent |
140 \noindent |
144 This is proved with the help of the intermediate value theorem, instantiated |
141 This is proved by force with the help of the intermediate value theorem, |
145 appropriately and with its first premise disposed of by lemma |
142 instantiated appropriately and with its first premise disposed of by lemma |
146 \isa{step{\isadigit{1}}}.% |
143 \isa{step{\isadigit{1}}}:% |
147 \end{isamarkuptxt}% |
144 \end{isamarkuptxt}% |
148 \isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
145 \isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
149 \isacommand{apply}\ simp\isanewline |
146 \isacommand{by}\ force% |
150 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}% |
147 \begin{isamarkuptext}% |
151 \begin{isamarkuptext}% |
148 \noindent |
152 \noindent |
|
153 The additional lemmas are needed to mediate between \isa{nat} and \isa{int}. |
|
154 |
149 |
155 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
150 Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}. |
156 The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:% |
151 The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:% |
157 \end{isamarkuptext}% |
152 \end{isamarkuptext}% |
158 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline |
153 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline |