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 | "[] \<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> ONE \<rightarrow> v" |
359 "s \<in> ONE \<rightarrow> v" |
359 "s \<in> CHAR c \<rightarrow> v" |
360 "s \<in> CHAR c \<rightarrow> v" |
360 "s \<in> ALT r1 r2 \<rightarrow> v" |
361 "s \<in> ALT r1 r2 \<rightarrow> v" |
361 "s \<in> SEQ r1 r2 \<rightarrow> v" |
362 "s \<in> SEQ r1 r2 \<rightarrow> v" |
362 "s \<in> STAR r \<rightarrow> v" |
363 "s \<in> STAR r \<rightarrow> v" |
386 apply(subst append.simps(1)[symmetric]) |
387 apply(subst append.simps(1)[symmetric]) |
387 apply(rule Posix.intros) |
388 apply(rule Posix.intros) |
388 apply(auto) |
389 apply(auto) |
389 done |
390 done |
390 |
391 |
|
392 (* |
|
393 lemma Posix_determ: |
|
394 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
395 shows "v1 = v2" |
|
396 using assms |
|
397 |
|
398 |
|
399 |
|
400 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
401 case (1 v2)lemma Posix_determ: |
|
402 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
403 shows "v1 = v2" |
|
404 using assms |
|
405 apply(induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
406 apply(erule Posix.cases) |
|
407 apply(simp_all)[7] |
|
408 apply(erule Posix.cases) |
|
409 apply(simp_all)[7] |
|
410 apply(rotate_tac 2) |
|
411 apply(erule Posix.cases) |
|
412 apply(simp_all (no_asm_use))[7] |
|
413 apply(clarify) |
|
414 apply(force) |
|
415 apply(clarify) |
|
416 apply(drule Posix1(1)) |
|
417 apply(simp) |
|
418 apply(rotate_tac 3) |
|
419 apply(erule Posix.cases) |
|
420 apply(simp_all (no_asm_use))[7] |
|
421 apply(drule Posix1(1))+ |
|
422 apply(simp) |
|
423 apply(simp) |
|
424 apply(rotate_tac 5) |
|
425 apply(erule Posix.cases) |
|
426 apply(simp_all (no_asm_use))[7] |
|
427 apply(clarify) |
|
428 apply(subgoal_tac "s1 = s1a") |
|
429 apply(blast) |
|
430 apply(simp add: append_eq_append_conv2) |
|
431 apply(clarify) |
|
432 apply (metis Posix1(1) append_self_conv) |
|
433 apply(rotate_tac 6) |
|
434 apply(erule Posix.cases) |
|
435 apply(simp_all (no_asm_use))[7] |
|
436 apply(clarify) |
|
437 apply(subgoal_tac "s1 = s1a") |
|
438 apply(simp) |
|
439 apply(blast) |
|
440 apply(simp (no_asm_use) add: append_eq_append_conv2) |
|
441 apply(clarify) |
|
442 apply (metis L.simps(6) Posix1(1) append_self_conv) |
|
443 apply(clarify) |
|
444 apply(rotate_tac 2) |
|
445 apply(erule Posix.cases) |
|
446 apply(simp_all (no_asm_use))[7] |
|
447 using Posix1(2) apply auto[1] |
|
448 using Posix1(2) apply blast |
|
449 apply(erule Posix.cases) |
|
450 apply(simp_all (no_asm_use))[7] |
|
451 apply(clarify) |
|
452 apply (simp add: Posix1(2)) |
|
453 apply(simp) |
|
454 done |
|
455 then have "[] \<in> ONE \<rightarrow> v2" by simp |
|
456 then show "Void = v2" |
|
457 apply(auto: elim Posix_elims)[1] |
|
458 |
|
459 apply(erule Posix.cases) |
|
460 apply(simp_all)[7] |
|
461 apply(erule Posix.cases) |
|
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 *) |
391 |
509 |
392 lemma Posix_determ: |
510 lemma Posix_determ: |
393 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
511 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
394 shows "v1 = v2" |
512 shows "v1 = v2" |
395 using assms |
513 using assms |
566 then consider |
684 then consider |
567 (cons) v1 vs s1 s2 where |
685 (cons) v1 vs s1 s2 where |
568 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
686 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
569 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
687 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
570 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" |
688 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" |
571 apply(auto elim!: Posix_elims(1-4) simp add: der_correctness Der_def intro: Posix.intros) |
689 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
572 apply(rotate_tac 3) |
690 apply(rotate_tac 3) |
573 apply(erule_tac Posix_elims(5)) |
691 apply(erule_tac Posix_elims(6)) |
574 apply (simp add: Posix.intros(6)) |
692 apply (simp add: Posix.intros(6)) |
575 using Posix.intros(7) by blast |
693 using Posix.intros(7) by blast |
576 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" |
694 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" |
577 proof (cases) |
695 proof (cases) |
578 case cons |
696 case cons |
696 fun F_LEFT where |
814 fun F_LEFT where |
697 "F_LEFT f v = Left (f v)" |
815 "F_LEFT f v = Left (f v)" |
698 |
816 |
699 fun F_ALT where |
817 fun F_ALT where |
700 "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)" |
818 "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)" |
701 | "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" |
819 | "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" |
|
820 | "F_ALT f1 f2 v = v" |
|
821 |
702 |
822 |
703 fun F_SEQ1 where |
823 fun F_SEQ1 where |
704 "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)" |
824 "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)" |
705 |
825 |
706 fun F_SEQ2 where |
826 fun F_SEQ2 where |
707 "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)" |
827 "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)" |
708 |
828 |
709 fun F_SEQ where |
829 fun F_SEQ where |
710 "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)" |
830 "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)" |
|
831 | "F_SEQ f1 f2 v = v" |
711 |
832 |
712 fun simp_ALT where |
833 fun simp_ALT where |
713 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
834 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
714 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
835 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
715 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
836 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
717 fun simp_SEQ where |
838 fun simp_SEQ where |
718 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
839 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
719 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
840 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
720 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
841 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
721 |
842 |
|
843 lemma simp_SEQ_simps: |
|
844 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
|
845 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
|
846 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))" |
|
847 apply(auto) |
|
848 apply(case_tac p1) |
|
849 apply(case_tac p2) |
|
850 apply(simp) |
|
851 apply(case_tac p1) |
|
852 apply(case_tac p2) |
|
853 apply(simp) |
|
854 apply(case_tac a) |
|
855 apply(simp_all) |
|
856 apply(case_tac p1) |
|
857 apply(case_tac p2) |
|
858 apply(simp) |
|
859 apply(case_tac p1) |
|
860 apply(case_tac p2) |
|
861 apply(simp) |
|
862 apply(case_tac a) |
|
863 apply(simp_all) |
|
864 apply(case_tac aa) |
|
865 apply(simp_all) |
|
866 apply(auto) |
|
867 apply(case_tac aa) |
|
868 apply(simp_all) |
|
869 apply(case_tac aa) |
|
870 apply(simp_all) |
|
871 apply(case_tac aa) |
|
872 apply(simp_all) |
|
873 apply(case_tac aa) |
|
874 apply(simp_all) |
|
875 done |
|
876 |
|
877 lemma simp_ALT_simps: |
|
878 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
|
879 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
|
880 else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))" |
|
881 apply(auto) |
|
882 apply(case_tac p1) |
|
883 apply(case_tac p2) |
|
884 apply(simp) |
|
885 apply(case_tac p1) |
|
886 apply(case_tac p2) |
|
887 apply(simp) |
|
888 apply(case_tac a) |
|
889 apply(simp_all) |
|
890 apply(case_tac p1) |
|
891 apply(case_tac p2) |
|
892 apply(simp) |
|
893 apply(case_tac p1) |
|
894 apply(case_tac p2) |
|
895 apply(simp) |
|
896 apply(case_tac a) |
|
897 apply(simp_all) |
|
898 apply(case_tac aa) |
|
899 apply(simp_all) |
|
900 apply(auto) |
|
901 apply(case_tac aa) |
|
902 apply(simp_all) |
|
903 apply(case_tac aa) |
|
904 apply(simp_all) |
|
905 apply(case_tac aa) |
|
906 apply(simp_all) |
|
907 apply(case_tac aa) |
|
908 apply(simp_all) |
|
909 done |
|
910 |
|
911 |
722 fun |
912 fun |
723 simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)" |
913 simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)" |
724 where |
914 where |
725 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
915 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
726 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" |
916 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" |
733 | "slexer r (c#s) = (let (rs, fr) = simp (der c r) in |
923 | "slexer r (c#s) = (let (rs, fr) = simp (der c r) in |
734 (case (slexer rs s) of |
924 (case (slexer rs s) of |
735 None \<Rightarrow> None |
925 None \<Rightarrow> None |
736 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
926 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
737 |
927 |
|
928 |
|
929 lemma L_fst_simp: |
|
930 shows "L(r) = L(fst (simp r))" |
|
931 using assms |
|
932 apply(induct r rule: rexp.induct) |
|
933 apply(auto simp add: simp_SEQ_simps simp_ALT_simps) |
|
934 done |
|
935 |
|
936 lemma |
|
937 shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))" |
|
938 using assms |
|
939 apply(induct r arbitrary: v rule: simp.induct) |
|
940 apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros) |
|
941 using Prf_elims(3) apply blast |
|
942 apply(erule Prf_elims) |
|
943 apply(simp) |
|
944 apply(clarify) |
|
945 apply(blast) |
|
946 apply(simp) |
|
947 apply(erule Prf_elims) |
|
948 apply(simp) |
|
949 apply(simp) |
|
950 apply(clarify) |
|
951 apply(blast) |
|
952 apply(erule Prf_elims) |
|
953 apply(case_tac v) |
|
954 apply(simp_all) |
|
955 apply(rule Prf.intros) |
|
956 apply(clarify) |
|
957 apply(simp) |
|
958 apply(case_tac v) |
|
959 apply(simp_all) |
|
960 apply(rule Prf.intros) |
|
961 apply(clarify) |
|
962 apply(simp) |
|
963 apply(erule Prf_elims) |
|
964 apply(simp) |
|
965 apply(rule Prf.intros) |
|
966 apply(simp) |
|
967 apply(simp) |
|
968 apply(rule Prf.intros) |
|
969 apply(simp) |
|
970 apply(erule Prf_elims) |
|
971 apply(simp) |
|
972 apply(blast) |
|
973 apply(rule Prf.intros) |
|
974 apply(erule Prf_elims) |
|
975 apply(simp) |
|
976 apply(rule Prf.intros) |
|
977 apply(erule Prf_elims) |
|
978 apply(simp) |
|
979 apply(rule Prf.intros) |
|
980 apply(erule Prf_elims) |
|
981 apply(simp) |
|
982 apply(clarify) |
|
983 apply(blast) |
|
984 apply(rule Prf.intros) |
|
985 apply(blast) |
|
986 using Prf.intros(4) apply blast |
|
987 apply(erule Prf_elims) |
|
988 apply(simp) |
|
989 apply(clarify) |
|
990 apply(blast) |
|
991 apply(rule Prf.intros) |
|
992 using Prf.intros(4) apply blast |
|
993 apply blast |
|
994 apply(erule Prf_elims) |
|
995 apply(case_tac v) |
|
996 apply(simp_all) |
|
997 apply(rule Prf.intros) |
|
998 apply(clarify) |
|
999 apply(simp) |
|
1000 apply(clarify) |
|
1001 apply(blast) |
|
1002 apply(erule Prf_elims) |
|
1003 apply(case_tac v) |
|
1004 apply(simp_all) |
|
1005 apply(rule Prf.intros) |
|
1006 apply(clarify) |
|
1007 apply(simp) |
|
1008 apply(simp) |
|
1009 done |
|
1010 |
|
1011 lemma Posix_simp_nullable: |
|
1012 assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v" |
|
1013 shows "((snd (simp r)) v) = mkeps r" |
|
1014 using assms |
|
1015 apply(induct r arbitrary: v) |
|
1016 apply(auto simp add: simp_SEQ_simps simp_ALT_simps) |
|
1017 apply(erule Posix_elims) |
|
1018 apply(simp) |
|
1019 apply(erule Posix_elims) |
|
1020 apply(clarify) |
|
1021 using Posix.intros(1) apply blast |
|
1022 using Posix.intros(1) apply blast |
|
1023 using Posix.intros(1) apply blast |
|
1024 apply(erule Posix_elims) |
|
1025 apply(simp) |
|
1026 apply(erule Posix_elims) |
|
1027 apply (metis L_fst_simp nullable.simps(1) nullable_correctness) |
|
1028 apply(erule Posix_elims) |
|
1029 apply(clarify) |
|
1030 apply(simp) |
|
1031 apply(clarify) |
|
1032 apply(simp) |
|
1033 apply(simp only: L_fst_simp[symmetric]) |
|
1034 apply (simp add: nullable_correctness) |
|
1035 apply(erule Posix_elims) |
|
1036 using L_fst_simp Posix1(1) nullable_correctness apply blast |
|
1037 apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable) |
|
1038 apply(erule Posix_elims) |
|
1039 apply(clarify) |
|
1040 apply(simp) |
|
1041 apply(simp only: L_fst_simp[symmetric]) |
|
1042 apply (simp add: nullable_correctness) |
|
1043 apply(erule Posix_elims) |
|
1044 apply(clarify) |
|
1045 apply(simp) |
|
1046 using L_fst_simp Posix1(1) nullable_correctness apply blast |
|
1047 apply(simp) |
|
1048 apply(erule Posix_elims) |
|
1049 apply(clarify) |
|
1050 apply(simp) |
|
1051 using Posix1(2) apply auto[1] |
|
1052 apply(simp) |
|
1053 done |
|
1054 |
|
1055 lemma Posix_simp: |
|
1056 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
|
1057 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
|
1058 using assms |
|
1059 apply(induct r arbitrary: s v rule: rexp.induct) |
|
1060 apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps) |
|
1061 prefer 3 |
|
1062 apply(erule Posix_elims) |
|
1063 apply(clarify) |
|
1064 apply(simp) |
|
1065 apply(rule Posix.intros) |
|
1066 apply(blast) |
|
1067 apply(blast) |
|
1068 apply(auto)[1] |
|
1069 apply(simp add: L_fst_simp[symmetric]) |
|
1070 apply(auto)[1] |
|
1071 prefer 3 |
|
1072 apply(rule Posix.intros) |
|
1073 apply(blast) |
|
1074 apply (metis L.simps(1) L_fst_simp equals0D) |
|
1075 prefer 3 |
|
1076 apply(rule Posix.intros) |
|
1077 apply(blast) |
|
1078 prefer 3 |
|
1079 apply(erule Posix_elims) |
|
1080 apply(clarify) |
|
1081 apply(simp) |
|
1082 apply(rule Posix.intros) |
|
1083 apply(blast) |
|
1084 apply(simp) |
|
1085 apply(rule Posix.intros) |
|
1086 apply(blast) |
|
1087 apply(simp add: L_fst_simp[symmetric]) |
|
1088 apply(subst append.simps[symmetric]) |
|
1089 apply(rule Posix.intros) |
|
1090 prefer 2 |
|
1091 apply(blast) |
|
1092 prefer 2 |
|
1093 apply(auto)[1] |
|
1094 apply (metis L_fst_simp Posix_elims(2) lex_correct3a) |
|
1095 apply(subst Posix_simp_nullable) |
|
1096 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
1097 apply(simp) |
|
1098 apply(rule Posix.intros) |
|
1099 apply(rule Posix_mkeps) |
|
1100 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
1101 apply(subst append_Nil2[symmetric]) |
|
1102 apply(rule Posix.intros) |
|
1103 apply(blast) |
|
1104 apply(subst Posix_simp_nullable) |
|
1105 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
1106 apply(simp) |
|
1107 apply(rule Posix.intros) |
|
1108 apply(rule Posix_mkeps) |
|
1109 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
1110 apply(auto) |
|
1111 done |
|
1112 |
|
1113 lemma slexer_correctness: |
|
1114 shows "slexer r s = lexer r s" |
|
1115 apply(induct s arbitrary: r) |
|
1116 apply(simp) |
|
1117 apply(simp) |
|
1118 apply(auto split: option.split prod.split) |
|
1119 apply (metis L_fst_simp fst_conv lex_correct1a) |
|
1120 using L_fst_simp lex_correct1a apply fastforce |
|
1121 by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv) |
|
1122 |
|
1123 |
|
1124 |
|
1125 |
|
1126 |
738 end |
1127 end |