340 section {* Our Alternative Posix definition *} |
340 section {* Our Alternative Posix definition *} |
341 |
341 |
342 inductive |
342 inductive |
343 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
343 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
344 where |
344 where |
345 "[] \<in> ONE \<rightarrow> Void" |
345 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
346 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
346 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
347 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
347 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
348 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
348 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
349 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
349 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
350 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
350 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
351 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
351 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
352 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
352 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
353 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
353 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
354 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
354 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
355 | "[] \<in> STAR r \<rightarrow> Stars []" |
355 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
356 |
356 |
357 inductive_cases Posix_elims: |
357 inductive_cases Posix_elims: |
358 "s \<in> ZERO \<rightarrow> v" |
358 "s \<in> ZERO \<rightarrow> v" |
359 "s \<in> ONE \<rightarrow> v" |
359 "s \<in> ONE \<rightarrow> v" |
360 "s \<in> CHAR c \<rightarrow> v" |
360 "s \<in> CHAR c \<rightarrow> v" |
387 apply(subst append.simps(1)[symmetric]) |
387 apply(subst append.simps(1)[symmetric]) |
388 apply(rule Posix.intros) |
388 apply(rule Posix.intros) |
389 apply(auto) |
389 apply(auto) |
390 done |
390 done |
391 |
391 |
392 (* |
392 |
393 lemma Posix_determ: |
393 lemma Posix_determ: |
394 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
394 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
395 shows "v1 = v2" |
395 shows "v1 = v2" |
396 using assms |
396 using assms |
397 |
|
398 |
|
399 |
|
400 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
397 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
401 case (1 v2)lemma Posix_determ: |
398 case (Posix_ONE v2) |
402 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
399 have "[] \<in> ONE \<rightarrow> v2" by fact |
403 shows "v1 = v2" |
400 then show "Void = v2" by cases auto |
404 using assms |
401 next |
405 apply(induct s r v1 arbitrary: v2 rule: Posix.induct) |
402 case (Posix_CHAR c v2) |
406 apply(erule Posix.cases) |
403 have "[c] \<in> CHAR c \<rightarrow> v2" by fact |
407 apply(simp_all)[7] |
404 then show "Char c = v2" by cases auto |
408 apply(erule Posix.cases) |
405 next |
409 apply(simp_all)[7] |
406 case (Posix_ALT1 s r1 v r2 v2) |
410 apply(rotate_tac 2) |
407 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
411 apply(erule Posix.cases) |
408 moreover |
412 apply(simp_all (no_asm_use))[7] |
409 have "s \<in> r1 \<rightarrow> v" by fact |
413 apply(clarify) |
410 then have "s \<in> L r1" by (simp add: Posix1) |
414 apply(force) |
411 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
415 apply(clarify) |
412 moreover |
416 apply(drule Posix1(1)) |
413 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
417 apply(simp) |
414 ultimately have "v = v'" by simp |
418 apply(rotate_tac 3) |
415 then show "Left v = v2" using eq by simp |
419 apply(erule Posix.cases) |
416 next |
420 apply(simp_all (no_asm_use))[7] |
417 case (Posix_ALT2 s r2 v r1 v2) |
421 apply(drule Posix1(1))+ |
418 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
422 apply(simp) |
419 moreover |
423 apply(simp) |
420 have "s \<notin> L r1" by fact |
424 apply(rotate_tac 5) |
421 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
425 apply(erule Posix.cases) |
422 by cases (auto simp add: Posix1) |
426 apply(simp_all (no_asm_use))[7] |
423 moreover |
427 apply(clarify) |
424 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
428 apply(subgoal_tac "s1 = s1a") |
425 ultimately have "v = v'" by simp |
429 apply(blast) |
426 then show "Right v = v2" using eq by simp |
430 apply(simp add: append_eq_append_conv2) |
427 next |
431 apply(clarify) |
428 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
432 apply (metis Posix1(1) append_self_conv) |
429 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
433 apply(rotate_tac 6) |
430 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
434 apply(erule Posix.cases) |
431 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact+ |
435 apply(simp_all (no_asm_use))[7] |
432 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
436 apply(clarify) |
433 apply(cases) apply (auto simp add: append_eq_append_conv2) |
437 apply(subgoal_tac "s1 = s1a") |
434 using Posix1(1) by fastforce+ |
438 apply(simp) |
435 moreover |
439 apply(blast) |
436 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
440 apply(simp (no_asm_use) add: append_eq_append_conv2) |
437 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
441 apply(clarify) |
438 ultimately show "Seq v1 v2 = v'" by simp |
442 apply (metis L.simps(6) Posix1(1) append_self_conv) |
439 next |
443 apply(clarify) |
440 case (Posix_STAR1 s1 r v s2 vs v2) |
444 apply(rotate_tac 2) |
441 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
445 apply(erule Posix.cases) |
442 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
446 apply(simp_all (no_asm_use))[7] |
443 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+ |
447 using Posix1(2) apply auto[1] |
444 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
448 using Posix1(2) apply blast |
445 apply(cases) apply (auto simp add: append_eq_append_conv2) |
449 apply(erule Posix.cases) |
446 using Posix1(1) apply fastforce |
450 apply(simp_all (no_asm_use))[7] |
447 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
451 apply(clarify) |
448 using Posix1(2) by blast |
452 apply (simp add: Posix1(2)) |
449 moreover |
453 apply(simp) |
450 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
454 done |
451 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
455 then have "[] \<in> ONE \<rightarrow> v2" by simp |
452 ultimately show "Stars (v # vs) = v2" by auto |
456 then show "Void = v2" |
453 next |
457 apply(auto: elim Posix_elims)[1] |
454 case (Posix_STAR2 r v2) |
458 |
455 have "[] \<in> STAR r \<rightarrow> v2" by fact |
459 apply(erule Posix.cases) |
456 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
460 apply(simp_all)[7] |
457 qed |
461 apply(erule Posix.cases) |
458 |
462 apply(simp_all)[7] |
|
463 apply(rotate_tac 2) |
|
464 apply(erule Posix.cases) |
|
465 apply(simp_all (no_asm_use))[7] |
|
466 apply(clarify) |
|
467 apply(force) |
|
468 apply(clarify) |
|
469 apply(drule Posix1(1)) |
|
470 apply(simp) |
|
471 apply(rotate_tac 3) |
|
472 apply(erule Posix.cases) |
|
473 apply(simp_all (no_asm_use))[7] |
|
474 apply(drule Posix1(1))+ |
|
475 apply(simp) |
|
476 apply(simp) |
|
477 apply(rotate_tac 5) |
|
478 apply(erule Posix.cases) |
|
479 apply(simp_all (no_asm_use))[7] |
|
480 apply(clarify) |
|
481 apply(subgoal_tac "s1 = s1a") |
|
482 apply(blast) |
|
483 apply(simp add: append_eq_append_conv2) |
|
484 apply(clarify) |
|
485 apply (metis Posix1(1) append_self_conv) |
|
486 apply(rotate_tac 6) |
|
487 apply(erule Posix.cases) |
|
488 apply(simp_all (no_asm_use))[7] |
|
489 apply(clarify) |
|
490 apply(subgoal_tac "s1 = s1a") |
|
491 apply(simp) |
|
492 apply(blast) |
|
493 apply(simp (no_asm_use) add: append_eq_append_conv2) |
|
494 apply(clarify) |
|
495 apply (metis L.simps(6) Posix1(1) append_self_conv) |
|
496 apply(clarify) |
|
497 apply(rotate_tac 2) |
|
498 apply(erule Posix.cases) |
|
499 apply(simp_all (no_asm_use))[7] |
|
500 using Posix1(2) apply auto[1] |
|
501 using Posix1(2) apply blast |
|
502 apply(erule Posix.cases) |
|
503 apply(simp_all (no_asm_use))[7] |
|
504 apply(clarify) |
|
505 apply (simp add: Posix1(2)) |
|
506 apply(simp) |
|
507 done |
|
508 *) |
|
509 |
|
510 lemma Posix_determ: |
|
511 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
512 shows "v1 = v2" |
|
513 using assms |
|
514 apply(induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
515 apply(erule Posix.cases) |
|
516 apply(simp_all)[7] |
|
517 apply(erule Posix.cases) |
|
518 apply(simp_all)[7] |
|
519 apply(rotate_tac 2) |
|
520 apply(erule Posix.cases) |
|
521 apply(simp_all (no_asm_use))[7] |
|
522 apply(clarify) |
|
523 apply(force) |
|
524 apply(clarify) |
|
525 apply(drule Posix1(1)) |
|
526 apply(simp) |
|
527 apply(rotate_tac 3) |
|
528 apply(erule Posix.cases) |
|
529 apply(simp_all (no_asm_use))[7] |
|
530 apply(drule Posix1(1))+ |
|
531 apply(simp) |
|
532 apply(simp) |
|
533 apply(rotate_tac 5) |
|
534 apply(erule Posix.cases) |
|
535 apply(simp_all (no_asm_use))[7] |
|
536 apply(clarify) |
|
537 apply(subgoal_tac "s1 = s1a") |
|
538 apply(blast) |
|
539 apply(simp add: append_eq_append_conv2) |
|
540 apply(clarify) |
|
541 apply (metis Posix1(1) append_self_conv) |
|
542 apply(rotate_tac 6) |
|
543 apply(erule Posix.cases) |
|
544 apply(simp_all (no_asm_use))[7] |
|
545 apply(clarify) |
|
546 apply(subgoal_tac "s1 = s1a") |
|
547 apply(simp) |
|
548 apply(blast) |
|
549 apply(simp (no_asm_use) add: append_eq_append_conv2) |
|
550 apply(clarify) |
|
551 apply (metis L.simps(6) Posix1(1) append_self_conv) |
|
552 apply(clarify) |
|
553 apply(rotate_tac 2) |
|
554 apply(erule Posix.cases) |
|
555 apply(simp_all (no_asm_use))[7] |
|
556 using Posix1(2) apply auto[1] |
|
557 using Posix1(2) apply blast |
|
558 apply(erule Posix.cases) |
|
559 apply(simp_all (no_asm_use))[7] |
|
560 apply(clarify) |
|
561 apply (simp add: Posix1(2)) |
|
562 apply(simp) |
|
563 done |
|
564 |
459 |
565 (* a proof that does not need proj *) |
460 (* a proof that does not need proj *) |
566 lemma Posix2_roy_version: |
461 lemma Posix2_roy_version: |
567 assumes "s \<in> (der c r) \<rightarrow> v" |
462 assumes "s \<in> (der c r) \<rightarrow> v" |
568 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
463 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
722 | "lexer r (c#s) = (case (lexer (der c r) s) of |
617 | "lexer r (c#s) = (case (lexer (der c r) s) of |
723 None \<Rightarrow> None |
618 None \<Rightarrow> None |
724 | Some(v) \<Rightarrow> Some(injval r c v))" |
619 | Some(v) \<Rightarrow> Some(injval r c v))" |
725 |
620 |
726 |
621 |
727 |
622 lemma lexer_correct_None: |
728 lemma lex_correct1: |
623 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
729 assumes "s \<notin> L r" |
|
730 shows "lexer r s = None" |
|
731 using assms |
624 using assms |
732 apply(induct s arbitrary: r) |
625 apply(induct s arbitrary: r) |
733 apply(simp add: nullable_correctness) |
626 apply(simp add: nullable_correctness) |
734 apply(drule_tac x="der a r" in meta_spec) |
627 apply(drule_tac x="der a r" in meta_spec) |
735 apply(auto simp add: der_correctness Der_def) |
628 apply(auto simp add: der_correctness Der_def) |
736 done |
629 done |
737 |
630 |
738 lemma lex_correct1a: |
631 lemma lexer_correct_Some: |
739 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
632 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
740 using assms |
633 using assms |
741 apply(induct s arbitrary: r) |
634 apply(induct s arbitrary: r) |
742 apply(simp add: nullable_correctness) |
635 apply(auto simp add: Posix_mkeps nullable_correctness)[1] |
743 apply(drule_tac x="der a r" in meta_spec) |
|
744 apply(auto simp add: der_correctness Der_def) |
|
745 done |
|
746 |
|
747 lemma lex_correct2: |
|
748 assumes "s \<in> L r" |
|
749 shows "\<exists>v. lexer r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
|
750 using assms |
|
751 apply(induct s arbitrary: r) |
|
752 apply(simp) |
|
753 apply (metis mkeps_flat mkeps_nullable nullable_correctness) |
|
754 apply(drule_tac x="der a r" in meta_spec) |
|
755 apply(drule meta_mp) |
|
756 apply(simp add: der_correctness Der_def) |
|
757 apply(auto) |
|
758 apply (metis Prf_injval) |
|
759 apply(rule Prf_injval_flat) |
|
760 by simp |
|
761 |
|
762 lemma lex_correct3: |
|
763 assumes "s \<in> L r" |
|
764 shows "\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v" |
|
765 using assms |
|
766 apply(induct s arbitrary: r) |
|
767 apply(simp) |
|
768 apply (metis Posix_mkeps nullable_correctness) |
|
769 apply(drule_tac x="der a r" in meta_spec) |
|
770 apply(drule meta_mp) |
|
771 apply(simp add: der_correctness Der_def) |
|
772 apply(auto) |
|
773 by (metis Posix2_roy_version) |
|
774 |
|
775 lemma lex_correct3a: |
|
776 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
|
777 using assms |
|
778 apply(induct s arbitrary: r) |
|
779 apply(simp) |
|
780 apply (metis Posix_mkeps nullable_correctness) |
|
781 apply(drule_tac x="der a r" in meta_spec) |
|
782 apply(auto) |
|
783 apply(metis Posix2_roy_version) |
|
784 apply(simp add: der_correctness Der_def) |
|
785 using lex_correct1a |
|
786 apply fastforce |
|
787 apply(simp add: der_correctness Der_def) |
|
788 by (simp add: lex_correct1a) |
|
789 |
|
790 lemma lex_correct3b: |
|
791 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
|
792 using assms |
|
793 apply(induct s arbitrary: r) |
|
794 apply(simp) |
|
795 apply (metis Posix_mkeps nullable_correctness) |
|
796 apply(drule_tac x="der a r" in meta_spec) |
636 apply(drule_tac x="der a r" in meta_spec) |
797 apply(simp add: der_correctness Der_def) |
637 apply(simp add: der_correctness Der_def) |
798 apply(case_tac "lexer (der a r) s = None") |
|
799 apply(simp) |
|
800 apply(simp) |
|
801 apply(clarify) |
|
802 apply(rule iffI) |
638 apply(rule iffI) |
803 apply(auto) |
639 apply(auto intro: Posix2_roy_version simp add: Posix1(1)) |
804 apply(rule Posix2_roy_version) |
640 done |
805 apply(simp) |
|
806 using Posix1(1) by auto |
|
807 |
|
808 |
|
809 |
641 |
810 |
642 |
811 end |
643 end |