166 | "L (CHAR c) = {[c]}" |
167 | "L (CHAR c) = {[c]}" |
167 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
168 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
168 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
169 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
169 | "L (STAR r) = (L r)\<star>" |
170 | "L (STAR r) = (L r)\<star>" |
170 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
171 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
171 | "L (NTIMES r n) = ((L r) \<up> n)" |
172 | "L (NTIMES r n) = (L r) \<up> n" |
172 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
173 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
|
174 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
173 |
175 |
174 section {* Nullable, Derivatives *} |
176 section {* Nullable, Derivatives *} |
175 |
177 |
176 fun |
178 fun |
177 nullable :: "rexp \<Rightarrow> bool" |
179 nullable :: "rexp \<Rightarrow> bool" |
183 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
185 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
184 | "nullable (STAR r) = True" |
186 | "nullable (STAR r) = True" |
185 | "nullable (UPNTIMES r n) = True" |
187 | "nullable (UPNTIMES r n) = True" |
186 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
188 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
187 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
189 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
|
190 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
188 |
191 |
189 fun |
192 fun |
190 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
193 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
191 where |
194 where |
192 "der c (ZERO) = ZERO" |
195 "der c (ZERO) = ZERO" |
202 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)" |
205 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)" |
203 | "der c (NTIMES r 0) = ZERO" |
206 | "der c (NTIMES r 0) = ZERO" |
204 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)" |
207 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)" |
205 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)" |
208 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)" |
206 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)" |
209 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)" |
|
210 | "der c (NMTIMES r n m) = |
|
211 (if m < n then ZERO else (if n = 0 then (if m = 0 then ZERO else SEQ (der c r) (UPNTIMES r (m - 1))) else |
|
212 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
207 |
213 |
208 fun |
214 fun |
209 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
215 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
210 where |
216 where |
211 "ders [] r = r" |
217 "ders [] r = r" |
267 apply(case_tac "[] \<in> L r") |
273 apply(case_tac "[] \<in> L r") |
268 apply(simp) |
274 apply(simp) |
269 apply(simp) |
275 apply(simp) |
270 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem) |
276 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem) |
271 |
277 |
|
278 lemma test2: |
|
279 shows "(\<Union>x\<in>(Suc ` A). Der c (L r \<up> x)) = (\<Union>x\<in>A. Der c (L r) ;; L r \<up> x)" |
|
280 apply(auto)[1] |
|
281 apply(case_tac "[] \<in> L r") |
|
282 apply(simp) |
|
283 defer |
|
284 apply(simp) |
|
285 using Der_Pow_subseteq by blast |
272 |
286 |
273 |
287 |
274 lemma Der_Pow_notin: |
288 lemma Der_Pow_notin: |
275 assumes "[] \<notin> A" |
289 assumes "[] \<notin> A" |
276 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
290 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
297 apply(simp) |
311 apply(simp) |
298 using Der_star Star_def2 apply auto[1] |
312 using Der_star Star_def2 apply auto[1] |
299 apply(simp only: der.simps) |
313 apply(simp only: der.simps) |
300 apply(simp only: L.simps) |
314 apply(simp only: L.simps) |
301 apply(simp add: Der_UNION) |
315 apply(simp add: Der_UNION) |
302 by (smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1) |
316 apply(smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1) |
|
317 (* NMTIMES *) |
|
318 apply(case_tac "n \<le> m") |
|
319 prefer 2 |
|
320 apply(simp only: der.simps if_True) |
|
321 apply(simp only: L.simps) |
|
322 apply(simp) |
|
323 apply(auto) |
|
324 apply(subst (asm) Seq_UNION[symmetric]) |
|
325 apply(subst (asm) test[symmetric]) |
|
326 apply(auto simp add: Der_UNION)[1] |
|
327 apply(auto simp add: Der_UNION)[1] |
|
328 apply(subst Seq_UNION[symmetric]) |
|
329 apply(subst test[symmetric]) |
|
330 apply(auto)[1] |
|
331 apply(subst (asm) Seq_UNION[symmetric]) |
|
332 apply(subst (asm) test2[symmetric]) |
|
333 apply(auto simp add: Der_UNION)[1] |
|
334 apply(subst Seq_UNION[symmetric]) |
|
335 apply(subst test2[symmetric]) |
|
336 apply(auto simp add: Der_UNION)[1] |
|
337 done |
303 |
338 |
304 lemma ders_correctness: |
339 lemma ders_correctness: |
305 shows "L (ders s r) = Ders s (L r)" |
340 shows "L (ders s r) = Ders s (L r)" |
306 apply(induct s arbitrary: r) |
341 apply(induct s arbitrary: r) |
307 apply(simp_all add: Ders_def der_correctness Der_def) |
342 apply(simp_all add: Ders_def der_correctness Der_def) |
373 | "\<turnstile> Char c : CHAR c" |
408 | "\<turnstile> Char c : CHAR c" |
374 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
409 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
375 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n" |
410 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n" |
376 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n" |
411 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n" |
377 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n" |
412 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n" |
|
413 | "\<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" |
378 |
414 |
379 inductive_cases Prf_elims: |
415 inductive_cases Prf_elims: |
380 "\<turnstile> v : ZERO" |
416 "\<turnstile> v : ZERO" |
381 "\<turnstile> v : SEQ r1 r2" |
417 "\<turnstile> v : SEQ r1 r2" |
382 "\<turnstile> v : ALT r1 r2" |
418 "\<turnstile> v : ALT r1 r2" |
499 apply(simp) |
539 apply(simp) |
500 apply(rule Prf.intros) |
540 apply(rule Prf.intros) |
501 apply(simp) |
541 apply(simp) |
502 apply(simp) |
542 apply(simp) |
503 using Star_Pow Star_val_length apply blast |
543 using Star_Pow Star_val_length apply blast |
|
544 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)") |
|
545 apply(auto)[1] |
|
546 apply(rule_tac x="Stars vs" in exI) |
|
547 apply(simp) |
|
548 apply(rule Prf.intros) |
|
549 apply(simp) |
|
550 apply(simp) |
|
551 apply(simp) |
|
552 using Star_Pow Star_val_length apply blast |
504 done |
553 done |
505 |
554 |
506 lemma L_flat_Prf: |
555 lemma L_flat_Prf: |
507 "L(r) = {flat v | v. \<turnstile> v : r}" |
556 "L(r) = {flat v | v. \<turnstile> v : r}" |
508 using Prf_flat_L L_flat_Prf2 by blast |
557 using Prf_flat_L L_flat_Prf2 by blast |
513 fun |
562 fun |
514 mkeps :: "rexp \<Rightarrow> val" |
563 mkeps :: "rexp \<Rightarrow> val" |
515 where |
564 where |
516 "mkeps(ONE) = Void" |
565 "mkeps(ONE) = Void" |
517 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
566 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
518 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
567 | "mkeps(ALT r1 r2) = (if nullable r1 then Left (mkeps r1) else Right (mkeps r2))" |
519 | "mkeps(STAR r) = Stars []" |
568 | "mkeps(STAR r) = Stars []" |
520 | "mkeps(UPNTIMES r n) = Stars []" |
569 | "mkeps(UPNTIMES r n) = Stars []" |
521 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
570 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
522 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
571 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
|
572 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
|
573 |
523 |
574 |
524 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
575 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
525 where |
576 where |
526 "injval (CHAR d) c Void = Char d" |
577 "injval (CHAR d) c Void = Char d" |
527 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
578 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
531 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
582 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
532 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
583 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
533 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
584 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
534 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
585 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
535 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
586 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
587 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
588 |
536 |
589 |
537 section {* Mkeps, injval *} |
590 section {* Mkeps, injval *} |
538 |
591 |
539 lemma mkeps_nullable: |
592 lemma mkeps_nullable: |
540 assumes "nullable(r)" |
593 assumes "nullable(r)" |
541 shows "\<turnstile> mkeps r : r" |
594 shows "\<turnstile> mkeps r : r" |
542 using assms |
595 using assms |
543 apply(induct r rule: mkeps.induct) |
596 apply(induct r rule: mkeps.induct) |
544 apply(auto intro: Prf.intros) |
597 apply(auto intro: Prf.intros) |
545 done |
598 by (metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl) |
546 |
599 |
547 lemma mkeps_flat: |
600 lemma mkeps_flat: |
548 assumes "nullable(r)" |
601 assumes "nullable(r)" |
549 shows "flat (mkeps r) = []" |
602 shows "flat (mkeps r) = []" |
550 using assms |
603 using assms |
551 by (induct rule: nullable.induct) (auto) |
604 apply (induct rule: nullable.induct) |
|
605 apply(auto) |
|
606 by meson |
552 |
607 |
553 |
608 |
554 lemma Prf_injval: |
609 lemma Prf_injval: |
555 assumes "\<turnstile> v : der c r" |
610 assumes "\<turnstile> v : der c r" |
556 shows "\<turnstile> (injval r c v) : r" |
611 shows "\<turnstile> (injval r c v) : r" |
606 apply(clarify) |
661 apply(clarify) |
607 apply(rotate_tac 2) |
662 apply(rotate_tac 2) |
608 apply(erule Prf.cases) |
663 apply(erule Prf.cases) |
609 apply(simp_all) |
664 apply(simp_all) |
610 apply(clarify) |
665 apply(clarify) |
611 using Prf.intros(9) by auto |
666 using Prf.intros(9) apply auto |
|
667 (* NMTIMES *) |
|
668 apply(rotate_tac 3) |
|
669 apply(erule Prf.cases) |
|
670 apply(simp_all) |
|
671 apply(clarify) |
|
672 apply(rule Prf.intros) |
|
673 apply(auto)[2] |
|
674 apply simp |
|
675 apply(rotate_tac 4) |
|
676 apply(erule Prf.cases) |
|
677 apply(simp_all) |
|
678 apply(clarify) |
|
679 apply(rule Prf.intros) |
|
680 apply(auto)[2] |
|
681 apply simp |
|
682 done |
612 |
683 |
613 |
684 |
614 lemma Prf_injval_flat: |
685 lemma Prf_injval_flat: |
615 assumes "\<turnstile> v : der c r" |
686 assumes "\<turnstile> v : der c r" |
616 shows "flat (injval r c v) = c # (flat v)" |
687 shows "flat (injval r c v) = c # (flat v)" |
662 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
739 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
663 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
740 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
664 \<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 (FROMNTIMES r n))\<rbrakk> |
741 \<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 (FROMNTIMES r n))\<rbrakk> |
665 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
742 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
666 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
743 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
|
744 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; |
|
745 \<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> |
|
746 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
|
747 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
667 |
748 |
668 |
749 |
669 inductive_cases Posix_elims: |
750 inductive_cases Posix_elims: |
670 "s \<in> ZERO \<rightarrow> v" |
751 "s \<in> ZERO \<rightarrow> v" |
671 "s \<in> ONE \<rightarrow> v" |
752 "s \<in> ONE \<rightarrow> v" |
682 apply(auto simp add: Sequ_def) |
763 apply(auto simp add: Sequ_def) |
683 apply(rule_tac x="Suc x" in bexI) |
764 apply(rule_tac x="Suc x" in bexI) |
684 apply(auto simp add: Sequ_def) |
765 apply(auto simp add: Sequ_def) |
685 apply(rule_tac x="Suc x" in bexI) |
766 apply(rule_tac x="Suc x" in bexI) |
686 apply(auto simp add: Sequ_def) |
767 apply(auto simp add: Sequ_def) |
687 by (simp add: Star_in_Pow) |
768 apply(simp add: Star_in_Pow) |
|
769 apply(rule_tac x="Suc x" in bexI) |
|
770 apply(auto simp add: Sequ_def) |
|
771 done |
688 |
772 |
689 |
773 |
690 lemma Posix1a: |
774 lemma Posix1a: |
691 assumes "s \<in> r \<rightarrow> v" |
775 assumes "s \<in> r \<rightarrow> v" |
692 shows "\<turnstile> v : r" |
776 shows "\<turnstile> v : r" |
701 apply(rule Prf.intros) |
785 apply(rule Prf.intros) |
702 apply(auto)[1] |
786 apply(auto)[1] |
703 apply(rotate_tac 3) |
787 apply(rotate_tac 3) |
704 apply(erule Prf.cases) |
788 apply(erule Prf.cases) |
705 apply(simp_all) |
789 apply(simp_all) |
706 apply (smt Posix_UPNTIMES2 Posix_elims(2) Prf.simps le_0_eq le_Suc_eq length_0_conv nat_induct nullable.simps(3) nullable.simps(7) rexp.distinct(61) rexp.distinct(67) rexp.distinct(69) rexp.inject(5) val.inject(5) val.simps(29) val.simps(33) val.simps(35)) |
790 apply(rotate_tac 3) |
|
791 apply(erule Prf.cases) |
|
792 apply(simp_all) |
707 apply(rule Prf.intros) |
793 apply(rule Prf.intros) |
708 apply(auto)[1] |
794 apply(auto)[1] |
709 apply(rotate_tac 3) |
795 apply(rotate_tac 3) |
710 apply(erule Prf.cases) |
796 apply(erule Prf.cases) |
711 apply(simp_all) |
797 apply(simp_all) |
712 apply (smt Prf.simps rexp.distinct(63) rexp.distinct(67) rexp.distinct(71) rexp.inject(6) val.distinct(17) val.distinct(9) val.inject(5) val.simps(29) val.simps(33) val.simps(35)) |
798 apply(rotate_tac 3) |
|
799 apply(erule Prf.cases) |
|
800 apply(simp_all) |
713 apply(rule Prf.intros) |
801 apply(rule Prf.intros) |
714 apply(auto)[1] |
802 apply(auto)[1] |
715 apply(rotate_tac 3) |
803 apply(rotate_tac 3) |
716 apply(erule Prf.cases) |
804 apply(erule Prf.cases) |
717 apply(simp_all) |
805 apply(simp_all) |
718 using Prf.simps apply blast |
806 apply(rotate_tac 3) |
719 by (smt Prf.simps le0 rexp.distinct(61) rexp.distinct(63) rexp.distinct(65) rexp.inject(4) val.distinct(17) val.distinct(9) val.simps(29) val.simps(33) val.simps(35)) |
807 apply(erule Prf.cases) |
|
808 apply(simp_all) |
|
809 apply(rule Prf.intros) |
|
810 apply(auto)[2] |
|
811 apply(rotate_tac 3) |
|
812 apply(erule Prf.cases) |
|
813 apply(simp_all) |
|
814 apply(rule Prf.intros) |
|
815 apply(auto)[3] |
|
816 apply(rotate_tac 3) |
|
817 apply(erule Prf.cases) |
|
818 apply(simp_all) |
|
819 apply(rotate_tac 3) |
|
820 apply(erule Prf.cases) |
|
821 apply(simp_all) |
|
822 apply(rotate_tac 3) |
|
823 apply(erule Prf.cases) |
|
824 apply(simp_all) |
|
825 apply(rule Prf.intros) |
|
826 apply(auto)[3] |
|
827 apply(rotate_tac 3) |
|
828 apply(erule Prf.cases) |
|
829 apply(simp_all) |
|
830 apply(erule Prf.cases) |
|
831 apply(simp_all) |
|
832 done |
|
833 |
720 |
834 |
721 lemma Posix_NTIMES_mkeps: |
835 lemma Posix_NTIMES_mkeps: |
722 assumes "[] \<in> r \<rightarrow> mkeps r" |
836 assumes "[] \<in> r \<rightarrow> mkeps r" |
723 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
837 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
724 apply(induct n) |
838 apply(induct n) |
743 apply (rule Posix_FROMNTIMES1) |
857 apply (rule Posix_FROMNTIMES1) |
744 apply(auto) |
858 apply(auto) |
745 apply(rule assms) |
859 apply(rule assms) |
746 done |
860 done |
747 |
861 |
|
862 lemma Posix_NMTIMES_mkeps: |
|
863 assumes "[] \<in> r \<rightarrow> mkeps r" "n \<le> m" |
|
864 shows "[] \<in> NMTIMES r n m \<rightarrow> Stars (replicate n (mkeps r))" |
|
865 using assms(2) |
|
866 apply(induct n arbitrary: m) |
|
867 apply(simp) |
|
868 apply(rule Posix.intros) |
|
869 apply(rule Posix.intros) |
|
870 apply(case_tac m) |
|
871 apply(simp) |
|
872 apply(simp) |
|
873 apply(subst append_Nil[symmetric]) |
|
874 apply(rule Posix.intros) |
|
875 apply(auto) |
|
876 apply(rule assms) |
|
877 done |
|
878 |
|
879 |
748 |
880 |
749 lemma Posix_mkeps: |
881 lemma Posix_mkeps: |
750 assumes "nullable r" |
882 assumes "nullable r" |
751 shows "[] \<in> r \<rightarrow> mkeps r" |
883 shows "[] \<in> r \<rightarrow> mkeps r" |
752 using assms |
884 using assms |
774 apply(subst append.simps(1)[symmetric]) |
906 apply(subst append.simps(1)[symmetric]) |
775 apply(rule Posix.intros) |
907 apply(rule Posix.intros) |
776 apply(auto) |
908 apply(auto) |
777 apply(rule Posix_FROMNTIMES_mkeps) |
909 apply(rule Posix_FROMNTIMES_mkeps) |
778 apply(simp) |
910 apply(simp) |
|
911 apply(rule Posix.intros) |
|
912 apply(rule Posix.intros) |
|
913 apply(case_tac n) |
|
914 apply(simp) |
|
915 apply(rule Posix.intros) |
|
916 apply(rule Posix.intros) |
|
917 apply(simp) |
|
918 apply(case_tac m) |
|
919 apply(simp) |
|
920 apply(simp) |
|
921 apply(subst append_Nil[symmetric]) |
|
922 apply(rule Posix.intros) |
|
923 apply(auto) |
|
924 apply(rule Posix_NMTIMES_mkeps) |
|
925 apply(auto) |
779 done |
926 done |
780 |
927 |
781 |
928 |
782 lemma Posix_determ: |
929 lemma Posix_determ: |
783 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
930 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
898 by (metis Posix1(1) Posix_FROMNTIMES1.hyps(5) append_Nil2 self_append_conv2) |
1045 by (metis Posix1(1) Posix_FROMNTIMES1.hyps(5) append_Nil2 self_append_conv2) |
899 moreover |
1046 moreover |
900 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1047 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
901 "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1048 "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
902 ultimately show "Stars (v # vs) = v2" by auto |
1049 ultimately show "Stars (v # vs) = v2" by auto |
|
1050 next |
|
1051 case (Posix_NMTIMES2 s r m v1 v2) |
|
1052 have "s \<in> NMTIMES r 0 m \<rightarrow> v2" "s \<in> UPNTIMES r m \<rightarrow> Stars v1" |
|
1053 "\<And>v3. s \<in> UPNTIMES r m \<rightarrow> v3 \<Longrightarrow> Stars v1 = v3" by fact+ |
|
1054 then show ?case |
|
1055 apply(cases) |
|
1056 apply(auto) |
|
1057 done |
|
1058 next |
|
1059 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
|
1060 have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" |
|
1061 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs" |
|
1062 "\<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))" by fact+ |
|
1063 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')" |
|
1064 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1065 using Posix1(1) apply fastforce |
|
1066 by (metis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2) |
|
1067 moreover |
|
1068 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1069 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1070 ultimately show "Stars (v # vs) = v2" by auto |
903 qed |
1071 qed |
904 |
1072 |
905 lemma NTIMES_Stars: |
1073 lemma NTIMES_Stars: |
906 assumes "\<turnstile> v : NTIMES r n" |
1074 assumes "\<turnstile> v : NTIMES r n" |
907 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n" |
1075 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n" |
927 lemma FROMNTIMES_Stars: |
1095 lemma FROMNTIMES_Stars: |
928 assumes "\<turnstile> v : FROMNTIMES r n" |
1096 assumes "\<turnstile> v : FROMNTIMES r n" |
929 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs" |
1097 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs" |
930 using assms |
1098 using assms |
931 apply(induct n arbitrary: v) |
1099 apply(induct n arbitrary: v) |
|
1100 apply(erule Prf.cases) |
|
1101 apply(simp_all) |
|
1102 apply(erule Prf.cases) |
|
1103 apply(simp_all) |
|
1104 done |
|
1105 |
|
1106 lemma NMTIMES_Stars: |
|
1107 assumes "\<turnstile> v : NMTIMES r n m" |
|
1108 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs \<and> length vs \<le> m" |
|
1109 using assms |
|
1110 apply(induct n arbitrary: m v) |
932 apply(erule Prf.cases) |
1111 apply(erule Prf.cases) |
933 apply(simp_all) |
1112 apply(simp_all) |
934 apply(erule Prf.cases) |
1113 apply(erule Prf.cases) |
935 apply(simp_all) |
1114 apply(simp_all) |
936 done |
1115 done |
1218 apply(simp only: der_correctness Der_def) |
1397 apply(simp only: der_correctness Der_def) |
1219 apply(simp) |
1398 apply(simp) |
1220 done |
1399 done |
1221 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp |
1400 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp |
1222 qed |
1401 qed |
|
1402 next |
|
1403 case (NMTIMES r n m) |
|
1404 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
1405 have "s \<in> der c (NMTIMES r n m) \<rightarrow> v" by fact |
|
1406 then show "(c # s) \<in> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v" |
|
1407 apply(case_tac "m < n") |
|
1408 apply(simp) |
|
1409 using Posix_elims(1) apply blast |
|
1410 apply(case_tac n) |
|
1411 apply(simp_all) |
|
1412 apply(case_tac m) |
|
1413 apply(simp) |
|
1414 apply(erule Posix_elims(1)) |
|
1415 apply(simp) |
|
1416 apply(erule Posix.cases) |
|
1417 apply(simp_all) |
|
1418 apply(clarify) |
|
1419 apply(rotate_tac 5) |
|
1420 apply(frule Posix1a) |
|
1421 apply(drule UPNTIMES_Stars) |
|
1422 apply(clarify) |
|
1423 apply(simp) |
|
1424 apply(subst append_Cons[symmetric]) |
|
1425 apply(rule Posix.intros) |
|
1426 apply(rule Posix.intros) |
|
1427 apply(auto) |
|
1428 apply(rule IH) |
|
1429 apply blast |
|
1430 using Posix1a Prf_injval_flat apply auto[1] |
|
1431 apply(simp add: der_correctness Der_def) |
|
1432 apply blast |
|
1433 apply(case_tac m) |
|
1434 apply(simp) |
|
1435 apply(simp) |
|
1436 apply(erule Posix.cases) |
|
1437 apply(simp_all) |
|
1438 apply(clarify) |
|
1439 apply(rotate_tac 6) |
|
1440 apply(frule Posix1a) |
|
1441 apply(drule NMTIMES_Stars) |
|
1442 apply(clarify) |
|
1443 apply(simp) |
|
1444 apply(subst append_Cons[symmetric]) |
|
1445 apply(rule Posix.intros) |
|
1446 apply(rule IH) |
|
1447 apply(blast) |
|
1448 apply(simp) |
|
1449 apply(simp add: der_correctness Der_def) |
|
1450 done |
1223 qed |
1451 qed |
|
1452 |
1224 |
1453 |
1225 |
1454 |
1226 section {* The Lexer by Sulzmann and Lu *} |
1455 section {* The Lexer by Sulzmann and Lu *} |
1227 |
1456 |
1228 fun |
1457 fun |