234 |
205 |
235 lemma flat_Stars [simp]: |
206 lemma flat_Stars [simp]: |
236 "flat (Stars vs) = flats vs" |
207 "flat (Stars vs) = flats vs" |
237 by (induct vs) (auto) |
208 by (induct vs) (auto) |
238 |
209 |
239 |
|
240 section {* Relation between values and regular expressions *} |
|
241 |
|
242 inductive |
|
243 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
244 where |
|
245 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
|
246 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
|
247 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" |
|
248 | "\<turnstile> Void : ONE" |
|
249 | "\<turnstile> Char c : CHAR c" |
|
250 | "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
|
251 |
|
252 inductive_cases Prf_elims: |
|
253 "\<turnstile> v : ZERO" |
|
254 "\<turnstile> v : SEQ r1 r2" |
|
255 "\<turnstile> v : ALT r1 r2" |
|
256 "\<turnstile> v : ONE" |
|
257 "\<turnstile> v : CHAR c" |
|
258 "\<turnstile> vs : STAR r" |
|
259 |
|
260 lemma Star_concat: |
210 lemma Star_concat: |
261 assumes "\<forall>s \<in> set ss. s \<in> A" |
211 assumes "\<forall>s \<in> set ss. s \<in> A" |
262 shows "concat ss \<in> A\<star>" |
212 shows "concat ss \<in> A\<star>" |
263 using assms by (induct ss) (auto) |
213 using assms by (induct ss) (auto) |
264 |
214 |
265 lemma Star_string: |
215 lemma Star_cstring: |
266 assumes "s \<in> A\<star>" |
216 assumes "s \<in> A\<star>" |
267 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
217 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])" |
268 using assms |
218 using assms |
269 apply(induct rule: Star.induct) |
219 apply(induct rule: Star.induct) |
270 apply(auto) |
220 apply(auto)[1] |
271 apply(rule_tac x="[]" in exI) |
221 apply(rule_tac x="[]" in exI) |
272 apply(simp) |
222 apply(simp) |
|
223 apply(erule exE) |
|
224 apply(clarify) |
|
225 apply(case_tac "s1 = []") |
|
226 apply(rule_tac x="ss" in exI) |
|
227 apply(simp) |
273 apply(rule_tac x="s1#ss" in exI) |
228 apply(rule_tac x="s1#ss" in exI) |
274 apply(simp) |
229 apply(simp) |
275 done |
230 done |
276 |
231 |
277 lemma Star_val: |
232 |
278 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
233 section {* Lexical Values *} |
279 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
280 using assms |
|
281 apply(induct ss) |
|
282 apply(auto) |
|
283 apply(rule_tac x="[]" in exI) |
|
284 apply(simp) |
|
285 apply(rule_tac x="v#vs" in exI) |
|
286 apply(simp) |
|
287 done |
|
288 |
|
289 lemma Prf_Stars_append: |
|
290 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
|
291 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
|
292 using assms |
|
293 by (auto intro!: Prf.intros elim!: Prf_elims) |
|
294 |
|
295 lemma Prf_flat_L: |
|
296 assumes "\<turnstile> v : r" |
|
297 shows "flat v \<in> L r" |
|
298 using assms |
|
299 by (induct v r rule: Prf.induct) |
|
300 (auto simp add: Sequ_def Star_concat) |
|
301 |
|
302 |
|
303 lemma L_flat_Prf1: |
|
304 assumes "\<turnstile> v : r" |
|
305 shows "flat v \<in> L r" |
|
306 using assms |
|
307 by (induct) (auto simp add: Sequ_def Star_concat) |
|
308 |
|
309 lemma L_flat_Prf2: |
|
310 assumes "s \<in> L r" |
|
311 shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
|
312 using assms |
|
313 proof(induct r arbitrary: s) |
|
314 case (STAR r s) |
|
315 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact |
|
316 have "s \<in> L (STAR r)" by fact |
|
317 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r" |
|
318 using Star_string by auto |
|
319 then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r" |
|
320 using IH Star_val by blast |
|
321 then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s" |
|
322 using Prf.intros(6) flat_Stars by blast |
|
323 next |
|
324 case (SEQ r1 r2 s) |
|
325 then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s" |
|
326 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
|
327 next |
|
328 case (ALT r1 r2 s) |
|
329 then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s" |
|
330 unfolding L.simps by (fastforce intro: Prf.intros) |
|
331 qed (auto intro: Prf.intros) |
|
332 |
|
333 lemma L_flat_Prf: |
|
334 shows "L(r) = {flat v | v. \<turnstile> v : r}" |
|
335 using L_flat_Prf1 L_flat_Prf2 by blast |
|
336 |
|
337 |
|
338 section {* Canonical Values *} |
|
339 |
234 |
340 inductive |
235 inductive |
341 CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
236 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
342 where |
237 where |
343 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
238 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
344 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
239 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
345 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
240 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
346 | "\<Turnstile> Void : ONE" |
241 | "\<Turnstile> Void : ONE" |
347 | "\<Turnstile> Char c : CHAR c" |
242 | "\<Turnstile> Char c : CHAR c" |
348 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
243 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
349 |
244 |
350 lemma Prf_CPrf: |
245 inductive_cases Prf_elims: |
351 assumes "\<Turnstile> v : r" |
246 "\<Turnstile> v : ZERO" |
352 shows "\<turnstile> v : r" |
247 "\<Turnstile> v : SEQ r1 r2" |
353 using assms |
248 "\<Turnstile> v : ALT r1 r2" |
354 by (induct)(auto intro: Prf.intros) |
249 "\<Turnstile> v : ONE" |
355 |
250 "\<Turnstile> v : CHAR c" |
356 lemma CPrf_Stars_appendE: |
251 "\<Turnstile> vs : STAR r" |
|
252 |
|
253 lemma Prf_Stars_appendE: |
357 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
254 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
358 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
255 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
359 using assms |
256 using assms |
360 apply(erule_tac CPrf.cases) |
257 by (auto intro: Prf.intros elim!: Prf_elims) |
361 apply(auto intro: CPrf.intros) |
258 |
|
259 |
|
260 lemma Star_cval: |
|
261 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
262 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
|
263 using assms |
|
264 apply(induct ss) |
|
265 apply(auto) |
|
266 apply(rule_tac x="[]" in exI) |
|
267 apply(simp) |
|
268 apply(case_tac "flat v = []") |
|
269 apply(rule_tac x="vs" in exI) |
|
270 apply(simp) |
|
271 apply(rule_tac x="v#vs" in exI) |
|
272 apply(simp) |
362 done |
273 done |
363 |
274 |
364 |
275 |
365 section {* Sets of Lexical and Canonical Values *} |
276 lemma L_flat_Prf1: |
366 |
277 assumes "\<Turnstile> v : r" |
367 definition |
278 shows "flat v \<in> L r" |
|
279 using assms |
|
280 by (induct) (auto simp add: Sequ_def Star_concat) |
|
281 |
|
282 lemma L_flat_Prf2: |
|
283 assumes "s \<in> L r" |
|
284 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
|
285 using assms |
|
286 proof(induct r arbitrary: s) |
|
287 case (STAR r s) |
|
288 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
289 have "s \<in> L (STAR r)" by fact |
|
290 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" |
|
291 using Star_cstring by auto |
|
292 then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" |
|
293 using IH Star_cval by metis |
|
294 then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s" |
|
295 using Prf.intros(6) flat_Stars by blast |
|
296 next |
|
297 case (SEQ r1 r2 s) |
|
298 then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" |
|
299 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
|
300 next |
|
301 case (ALT r1 r2 s) |
|
302 then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" |
|
303 unfolding L.simps by (fastforce intro: Prf.intros) |
|
304 qed (auto intro: Prf.intros) |
|
305 |
|
306 |
|
307 lemma L_flat_Prf: |
|
308 shows "L(r) = {flat v | v. \<Turnstile> v : r}" |
|
309 using L_flat_Prf1 L_flat_Prf2 by blast |
|
310 |
|
311 |
|
312 |
|
313 section {* Sets of Lexical Values *} |
|
314 |
|
315 text {* |
|
316 Shows that lexical values are finite for a given regex and string. |
|
317 *} |
|
318 |
|
319 definition |
368 LV :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
320 LV :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
369 where "LV r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}" |
321 where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}" |
370 |
322 |
371 definition |
323 lemma LV_simps: |
372 CV :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
324 shows "LV ZERO s = {}" |
373 where "CV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}" |
325 and "LV ONE s = (if s = [] then {Void} else {})" |
374 |
326 and "LV (CHAR c) s = (if s = [c] then {Char c} else {})" |
375 lemma LV_CV_subset: |
327 and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" |
376 shows "CV r s \<subseteq> LV r s" |
328 unfolding LV_def |
377 unfolding CV_def LV_def by(auto simp add: Prf_CPrf) |
329 by (auto intro: Prf.intros elim: Prf.cases) |
|
330 |
378 |
331 |
379 abbreviation |
332 abbreviation |
380 "Prefixes s \<equiv> {s'. prefixeq s' s}" |
333 "Prefixes s \<equiv> {s'. prefixeq s' s}" |
381 |
334 |
382 abbreviation |
335 abbreviation |
421 unfolding suffixeq_def prefixeq_def image_def |
367 unfolding suffixeq_def prefixeq_def image_def |
422 by (auto)(metis rev_append rev_rev_ident)+ |
368 by (auto)(metis rev_append rev_rev_ident)+ |
423 ultimately show "finite (Prefixes s)" by simp |
369 ultimately show "finite (Prefixes s)" by simp |
424 qed |
370 qed |
425 |
371 |
426 lemma CV_SEQ_subset: |
372 lemma LV_STAR_finite: |
427 "CV (SEQ r1 r2) s \<subseteq> (\<lambda>(v1,v2). Seq v1 v2) ` ((\<Union>s' \<in> Prefixes s. CV r1 s') \<times> (\<Union>s' \<in> Suffixes s. CV r2 s'))" |
373 assumes "\<forall>s. finite (LV r s)" |
428 unfolding image_def CV_def prefixeq_def suffixeq_def |
374 shows "finite (LV (STAR r) s)" |
429 by (auto elim: CPrf.cases) |
|
430 |
|
431 lemma CV_STAR_subset: |
|
432 "CV (STAR r) s \<subseteq> {Stars []} \<union> |
|
433 (\<lambda>(v,vs). Stars (v#vs)) ` ((\<Union>s' \<in> Prefixes s. CV r s') \<times> (\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)))" |
|
434 unfolding image_def CV_def prefixeq_def suffix_def |
|
435 apply(auto) |
|
436 apply(erule CPrf.cases) |
|
437 apply(auto) |
|
438 apply(case_tac vs) |
|
439 apply(auto intro: CPrf.intros) |
|
440 done |
|
441 |
|
442 |
|
443 lemma CV_STAR_finite: |
|
444 assumes "\<forall>s. finite (CV r s)" |
|
445 shows "finite (CV (STAR r) s)" |
|
446 proof(induct s rule: length_induct) |
375 proof(induct s rule: length_induct) |
447 fix s::"char list" |
376 fix s::"char list" |
448 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (CV (STAR r) s')" |
377 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
449 then have IH: "\<forall>s' \<in> SSuffixes s. finite (CV (STAR r) s')" |
378 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
450 by (auto simp add: suffix_def) |
379 by (auto simp add: suffix_def) |
451 def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" |
380 def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" |
452 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r s'" |
381 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'" |
453 def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)" |
382 def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
454 have "finite S1" using assms |
383 have "finite S1" using assms |
455 unfolding S1_def by (simp_all add: finite_Prefixes) |
384 unfolding S1_def by (simp_all add: finite_Prefixes) |
456 moreover |
385 moreover |
457 with IH have "finite S2" unfolding S2_def |
386 with IH have "finite S2" unfolding S2_def |
458 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
387 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
459 ultimately |
388 ultimately |
460 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
389 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
461 moreover |
390 moreover |
462 have "CV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" unfolding S1_def S2_def f_def |
391 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
463 by (rule CV_STAR_subset) |
392 unfolding S1_def S2_def f_def |
|
393 unfolding LV_def image_def prefixeq_def suffix_def |
|
394 apply(auto elim: Prf_elims) |
|
395 apply(erule Prf_elims) |
|
396 apply(auto) |
|
397 apply(case_tac vs) |
|
398 apply(auto intro: Prf.intros) |
|
399 done |
464 ultimately |
400 ultimately |
465 show "finite (CV (STAR r) s)" by (simp add: finite_subset) |
401 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
466 qed |
402 qed |
467 |
403 |
468 |
404 |
469 lemma CV_finite: |
405 lemma LV_finite: |
470 shows "finite (CV r s)" |
406 shows "finite (LV r s)" |
471 proof(induct r arbitrary: s) |
407 proof(induct r arbitrary: s) |
472 case (ZERO s) |
408 case (ZERO s) |
473 show "finite (CV ZERO s)" by (simp add: CV_simps) |
409 show "finite (LV ZERO s)" by (simp add: LV_simps) |
474 next |
410 next |
475 case (ONE s) |
411 case (ONE s) |
476 show "finite (CV ONE s)" by (simp add: CV_simps) |
412 show "finite (LV ONE s)" by (simp add: LV_simps) |
477 next |
413 next |
478 case (CHAR c s) |
414 case (CHAR c s) |
479 show "finite (CV (CHAR c) s)" by (simp add: CV_simps) |
415 show "finite (LV (CHAR c) s)" by (simp add: LV_simps) |
480 next |
416 next |
481 case (ALT r1 r2 s) |
417 case (ALT r1 r2 s) |
482 then show "finite (CV (ALT r1 r2) s)" by (simp add: CV_simps) |
418 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
483 next |
419 next |
484 case (SEQ r1 r2 s) |
420 case (SEQ r1 r2 s) |
485 def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2" |
421 def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2" |
486 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r1 s'" |
422 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'" |
487 def S2 \<equiv> "\<Union>s' \<in> Suffixes s. CV r2 s'" |
423 def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'" |
488 have IHs: "\<And>s. finite (CV r1 s)" "\<And>s. finite (CV r2 s)" by fact+ |
424 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
489 then have "finite S1" "finite S2" unfolding S1_def S2_def |
425 then have "finite S1" "finite S2" unfolding S1_def S2_def |
490 by (simp_all add: finite_Prefixes finite_Suffixes) |
426 by (simp_all add: finite_Prefixes finite_Suffixes) |
491 moreover |
427 moreover |
492 have "CV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
428 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
493 unfolding f_def S1_def S2_def by (auto simp add: CV_SEQ_subset) |
429 unfolding f_def S1_def S2_def |
|
430 unfolding LV_def image_def prefixeq_def suffixeq_def |
|
431 by (auto elim: Prf.cases) |
494 ultimately |
432 ultimately |
495 show "finite (CV (SEQ r1 r2) s)" |
433 show "finite (LV (SEQ r1 r2) s)" |
496 by (simp add: finite_subset) |
434 by (simp add: finite_subset) |
497 next |
435 next |
498 case (STAR r s) |
436 case (STAR r s) |
499 then show "finite (CV (STAR r) s)" by (simp add: CV_STAR_finite) |
437 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
500 qed |
438 qed |
501 |
439 |
502 |
440 |
503 |
441 |
504 section {* Our POSIX Definition *} |
442 section {* Our POSIX Definition *} |