199 @{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\ |
199 @{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\ |
200 @{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad |
200 @{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad |
201 @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\ |
201 @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\ |
202 \end{tabular} |
202 \end{tabular} |
203 \end{center} |
203 \end{center} |
|
204 |
|
205 \noindent |
|
206 A prefix of a string s |
|
207 |
|
208 \begin{center} |
|
209 \begin{tabular}{c} |
|
210 @{thm prefix_def[of "s\<^sub>1" "s\<^sub>2"]} |
|
211 \end{tabular} |
|
212 \end{center} |
|
213 |
|
214 \noindent |
|
215 Values and non-problematic values |
|
216 |
|
217 \begin{center} |
|
218 \begin{tabular}{c} |
|
219 @{thm Values_def}\medskip\\ |
|
220 @{thm NValues_def} |
|
221 \end{tabular} |
|
222 \end{center} |
|
223 |
|
224 |
|
225 \noindent |
|
226 The point is that for a given @{text s} and @{text r} there are only finitely many |
|
227 non-problematic values. |
204 *} |
228 *} |
205 |
229 |
206 text {* |
230 text {* |
207 \noindent |
231 \noindent |
208 Some lemmas |
232 Some lemmas we have proved:\bigskip |
209 |
233 |
|
234 @{thm L_flat_Prf} |
|
235 |
|
236 @{thm L_flat_NPrf} |
210 |
237 |
211 @{thm[mode=IfThen] mkeps_nullable} |
238 @{thm[mode=IfThen] mkeps_nullable} |
212 |
239 |
213 @{thm[mode=IfThen] mkeps_flat} |
240 @{thm[mode=IfThen] mkeps_flat} |
214 |
241 |
215 \ldots |
242 @{thm[mode=IfThen] v3} |
|
243 |
|
244 @{thm[mode=IfThen] v4} |
|
245 |
|
246 @{thm[mode=IfThen] PMatch_mkeps} |
|
247 |
|
248 @{thm[mode=IfThen] PMatch1(2)} |
|
249 |
|
250 @{thm[mode=IfThen] PMatch1N} |
|
251 |
|
252 \noindent |
|
253 This is the main theorem that lets us prove that the algorithm is correct according to |
|
254 @{term "s \<in> r \<rightarrow> v"}: |
|
255 |
|
256 @{thm[mode=IfThen] PMatch2} |
|
257 |
|
258 \mbox{}\bigskip |
|
259 *} |
|
260 |
|
261 text {* |
|
262 \noindent |
|
263 Things we like to prove, but cannot:\bigskip |
|
264 |
|
265 If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"} |
|
266 |
216 *} |
267 *} |
217 |
268 |
218 |
269 |
219 text {* |
270 text {* |
220 %\noindent |
271 %\noindent |