230 | "L (STAR r) = (L r)\<star>" |
231 | "L (STAR r) = (L r)\<star>" |
231 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
232 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
232 | "L (NTIMES r n) = (L r) \<up> n" |
233 | "L (NTIMES r n) = (L r) \<up> n" |
233 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
234 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
234 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
235 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
|
236 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)" |
235 |
237 |
236 section {* Nullable, Derivatives *} |
238 section {* Nullable, Derivatives *} |
237 |
239 |
238 fun |
240 fun |
239 nullable :: "rexp \<Rightarrow> bool" |
241 nullable :: "rexp \<Rightarrow> bool" |
246 | "nullable (STAR r) = True" |
248 | "nullable (STAR r) = True" |
247 | "nullable (UPNTIMES r n) = True" |
249 | "nullable (UPNTIMES r n) = True" |
248 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
250 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
249 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
251 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
250 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
252 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
|
253 | "nullable (PLUS r) = (nullable r)" |
251 |
254 |
252 fun |
255 fun |
253 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
256 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
254 where |
257 where |
255 "der c (ZERO) = ZERO" |
258 "der c (ZERO) = ZERO" |
270 | "der c (NMTIMES r n m) = |
273 | "der c (NMTIMES r n m) = |
271 (if m < n then ZERO |
274 (if m < n then ZERO |
272 else (if n = 0 then (if m = 0 then ZERO else |
275 else (if n = 0 then (if m = 0 then ZERO else |
273 SEQ (der c r) (UPNTIMES r (m - 1))) else |
276 SEQ (der c r) (UPNTIMES r (m - 1))) else |
274 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
277 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
|
278 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
275 |
279 |
276 fun |
280 fun |
277 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
281 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
278 where |
282 where |
279 "ders [] r = r" |
283 "ders [] r = r" |
338 apply(subst (asm) test2[symmetric]) |
342 apply(subst (asm) test2[symmetric]) |
339 apply(auto simp add: Der_UNION)[1] |
343 apply(auto simp add: Der_UNION)[1] |
340 apply(subst Sequ_UNION[symmetric]) |
344 apply(subst Sequ_UNION[symmetric]) |
341 apply(subst test2[symmetric]) |
345 apply(subst test2[symmetric]) |
342 apply(auto simp add: Der_UNION)[1] |
346 apply(auto simp add: Der_UNION)[1] |
343 done |
347 (* PLUS *) |
|
348 apply(auto simp add: Sequ_def Star_def)[1] |
|
349 apply(simp add: Der_UNION) |
|
350 apply(rule_tac x="Suc xa" in bexI) |
|
351 apply(auto simp add: Sequ_def Der_def)[2] |
|
352 apply (metis append_Cons) |
|
353 apply(simp add: Der_UNION) |
|
354 apply(erule_tac bexE) |
|
355 apply(case_tac xa) |
|
356 apply(simp) |
|
357 apply(simp) |
|
358 apply(auto) |
|
359 apply(auto simp add: Sequ_def Der_def)[1] |
|
360 using Star_def apply auto[1] |
|
361 apply(case_tac "[] \<in> L r") |
|
362 apply(auto) |
|
363 using Der_UNION Der_star Star_def by fastforce |
344 |
364 |
345 lemma ders_correctness: |
365 lemma ders_correctness: |
346 shows "L (ders s r) = Ders s (L r)" |
366 shows "L (ders s r) = Ders s (L r)" |
347 apply(induct s arbitrary: r) |
367 apply(induct s arbitrary: r) |
348 apply(simp_all add: Ders_def der_correctness Der_def) |
368 apply(simp_all add: Ders_def der_correctness Der_def) |
415 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
435 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
416 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n" |
436 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n" |
417 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n" |
437 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n" |
418 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n" |
438 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n" |
419 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m" |
439 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m" |
|
440 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r" |
|
441 |
420 |
442 |
421 inductive_cases Prf_elims: |
443 inductive_cases Prf_elims: |
422 "\<turnstile> v : ZERO" |
444 "\<turnstile> v : ZERO" |
423 "\<turnstile> v : SEQ r1 r2" |
445 "\<turnstile> v : SEQ r1 r2" |
424 "\<turnstile> v : ALT r1 r2" |
446 "\<turnstile> v : ALT r1 r2" |
549 apply(auto)[1] |
571 apply(auto)[1] |
550 apply(rule_tac x="Stars vs" in exI) |
572 apply(rule_tac x="Stars vs" in exI) |
551 apply(simp) |
573 apply(simp) |
552 apply(rule Prf.intros) |
574 apply(rule Prf.intros) |
553 apply(simp) |
575 apply(simp) |
|
576 apply(simp) |
|
577 apply(simp) |
|
578 using Star_Pow Star_val_length apply blast |
|
579 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
580 apply(auto)[1] |
|
581 apply(rule_tac x="Stars vs" in exI) |
|
582 apply(simp) |
|
583 apply(rule Prf.intros) |
554 apply(simp) |
584 apply(simp) |
555 apply(simp) |
585 apply(simp) |
556 using Star_Pow Star_val_length apply blast |
586 using Star_Pow Star_val_length apply blast |
557 done |
587 done |
558 |
588 |
572 | "mkeps(STAR r) = Stars []" |
602 | "mkeps(STAR r) = Stars []" |
573 | "mkeps(UPNTIMES r n) = Stars []" |
603 | "mkeps(UPNTIMES r n) = Stars []" |
574 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
604 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
575 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
605 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
576 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
606 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
|
607 | "mkeps(PLUS r) = Stars ([mkeps r])" |
577 |
608 |
578 |
609 |
579 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
610 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
580 where |
611 where |
581 "injval (CHAR d) c Void = Char d" |
612 "injval (CHAR d) c Void = Char d" |
587 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
618 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
588 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
619 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
589 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
620 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
590 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
621 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
591 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
622 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
592 |
623 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
593 |
624 |
594 section {* Mkeps, injval *} |
625 section {* Mkeps, injval *} |
595 |
626 |
596 lemma mkeps_nullable: |
627 lemma mkeps_nullable: |
597 assumes "nullable(r)" |
628 assumes "nullable(r)" |
747 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
748 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; |
749 \<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 (NMTIMES r n m))\<rbrakk> |
789 \<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 (NMTIMES r n m))\<rbrakk> |
750 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
790 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
751 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
791 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
|
792 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; |
|
793 \<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> |
|
794 \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)" |
752 |
795 |
753 |
796 |
754 inductive_cases Posix_elims: |
797 inductive_cases Posix_elims: |
755 "s \<in> ZERO \<rightarrow> v" |
798 "s \<in> ZERO \<rightarrow> v" |
756 "s \<in> ONE \<rightarrow> v" |
799 "s \<in> ONE \<rightarrow> v" |
770 apply(rule_tac x="Suc x" in bexI) |
813 apply(rule_tac x="Suc x" in bexI) |
771 using Sequ_def apply auto[2] |
814 using Sequ_def apply auto[2] |
772 apply(simp add: Star_def) |
815 apply(simp add: Star_def) |
773 apply(rule_tac x="Suc x" in bexI) |
816 apply(rule_tac x="Suc x" in bexI) |
774 apply(auto simp add: Sequ_def) |
817 apply(auto simp add: Sequ_def) |
|
818 apply(simp add: Star_def) |
|
819 apply(clarify) |
|
820 apply(rule_tac x="Suc x" in bexI) |
|
821 apply(auto simp add: Sequ_def) |
775 done |
822 done |
776 |
823 |
777 |
824 |
778 lemma Posix1a: |
825 lemma Posix1a: |
779 assumes "s \<in> r \<rightarrow> v" |
826 assumes "s \<in> r \<rightarrow> v" |
925 apply(subst append_Nil[symmetric]) |
977 apply(subst append_Nil[symmetric]) |
926 apply(rule Posix.intros) |
978 apply(rule Posix.intros) |
927 apply(auto) |
979 apply(auto) |
928 apply(rule Posix_NMTIMES_mkeps) |
980 apply(rule Posix_NMTIMES_mkeps) |
929 apply(auto) |
981 apply(auto) |
|
982 apply(subst append_Nil[symmetric]) |
|
983 apply(rule Posix.intros) |
|
984 apply(auto) |
|
985 apply(rule Posix.intros) |
930 done |
986 done |
931 |
987 |
932 |
988 |
933 lemma Posix_determ: |
989 lemma Posix_determ: |
934 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
990 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
1070 by (metis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2) |
1126 by (metis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2) |
1071 moreover |
1127 moreover |
1072 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1128 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1073 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1129 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1074 ultimately show "Stars (v # vs) = v2" by auto |
1130 ultimately show "Stars (v # vs) = v2" by auto |
|
1131 next |
|
1132 case (Posix_PLUS1 s1 r v s2 vs v2) |
|
1133 have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2" |
|
1134 "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs" |
|
1135 "\<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+ |
|
1136 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
1137 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1138 using Posix1(1) apply fastforce |
|
1139 by (metis Posix1(1) Posix_PLUS1.hyps(5) append_Nil2 self_append_conv2) |
|
1140 moreover |
|
1141 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1142 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1143 ultimately show "Stars (v # vs) = v2" by auto |
1075 qed |
1144 qed |
1076 |
1145 |
1077 lemma NTIMES_Stars: |
1146 lemma NTIMES_Stars: |
1078 assumes "\<turnstile> v : NTIMES r n" |
1147 assumes "\<turnstile> v : NTIMES r n" |
1079 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n" |
1148 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n" |
1102 using assms |
1171 using assms |
1103 apply(induct n arbitrary: v) |
1172 apply(induct n arbitrary: v) |
1104 apply(erule Prf.cases) |
1173 apply(erule Prf.cases) |
1105 apply(simp_all) |
1174 apply(simp_all) |
1106 apply(erule Prf.cases) |
1175 apply(erule Prf.cases) |
|
1176 apply(simp_all) |
|
1177 done |
|
1178 |
|
1179 lemma PLUS_Stars: |
|
1180 assumes "\<turnstile> v : PLUS r" |
|
1181 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> 1 \<le> length vs" |
|
1182 using assms |
|
1183 apply(erule_tac Prf.cases) |
1107 apply(simp_all) |
1184 apply(simp_all) |
1108 done |
1185 done |
1109 |
1186 |
1110 lemma NMTIMES_Stars: |
1187 lemma NMTIMES_Stars: |
1111 assumes "\<turnstile> v : NMTIMES r n m" |
1188 assumes "\<turnstile> v : NMTIMES r n m" |
1450 apply(rule IH) |
1527 apply(rule IH) |
1451 apply(blast) |
1528 apply(blast) |
1452 apply(simp) |
1529 apply(simp) |
1453 apply(simp add: der_correctness Der_def) |
1530 apply(simp add: der_correctness Der_def) |
1454 done |
1531 done |
|
1532 next |
|
1533 case (PLUS r) |
|
1534 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
1535 have "s \<in> der c (PLUS r) \<rightarrow> v" by fact |
|
1536 then consider |
|
1537 (cons) v1 vs s1 s2 where |
|
1538 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
|
1539 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
|
1540 "\<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))" |
|
1541 apply(simp) |
|
1542 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
|
1543 defer |
|
1544 apply(rotate_tac 3) |
|
1545 apply(erule_tac Posix_elims(6)) |
|
1546 apply (simp add: Posix.intros(6)) |
|
1547 using Posix.intros(7) by blast |
|
1548 then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" |
|
1549 proof (cases) |
|
1550 case cons |
|
1551 have "s1 \<in> der c r \<rightarrow> v1" by fact |
|
1552 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
|
1553 moreover |
|
1554 have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact |
|
1555 moreover |
|
1556 have "\<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))" by fact |
|
1557 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" |
|
1558 by (simp add: der_correctness Der_def) |
|
1559 ultimately |
|
1560 have "((c # s1) @ s2) \<in> (PLUS r) \<rightarrow> Stars (injval r c v1 # vs)" |
|
1561 apply(rule_tac Posix.intros) |
|
1562 apply(simp_all) |
|
1563 done |
|
1564 then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" using cons by(simp) |
|
1565 qed |
1455 qed |
1566 qed |
1456 |
1567 |
1457 |
1568 |
1458 |
1569 |
1459 section {* The Lexer by Sulzmann and Lu *} |
1570 section {* The Lexer by Sulzmann and Lu *} |