169 | "L (CHAR c) = {[c]}" |
170 | "L (CHAR c) = {[c]}" |
170 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
171 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
171 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
172 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
172 | "L (STAR r) = (L r)\<star>" |
173 | "L (STAR r) = (L r)\<star>" |
173 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
174 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
|
175 | "L (NTIMES r n) = ((L r) \<up> n)" |
174 |
176 |
175 |
177 |
176 section {* Nullable, Derivatives *} |
178 section {* Nullable, Derivatives *} |
177 |
179 |
178 fun |
180 fun |
183 | "nullable (CHAR c) = False" |
185 | "nullable (CHAR c) = False" |
184 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
186 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
185 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
187 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
186 | "nullable (STAR r) = True" |
188 | "nullable (STAR r) = True" |
187 | "nullable (UPNTIMES r n) = True" |
189 | "nullable (UPNTIMES r n) = True" |
|
190 | "nullable (NTIMES r n) = (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" |
198 then ALT (SEQ (der c r1) r2) (der c r2) |
201 then ALT (SEQ (der c r1) r2) (der c r2) |
199 else SEQ (der c r1) r2)" |
202 else SEQ (der c r1) r2)" |
200 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
203 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
201 | "der c (UPNTIMES r 0) = ZERO" |
204 | "der c (UPNTIMES r 0) = 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)" |
|
206 | "der c (NTIMES r 0) = ZERO" |
|
207 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)" |
203 |
208 |
204 |
209 |
205 fun |
210 fun |
206 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
211 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
207 where |
212 where |
209 | "ders (c # s) r = ders s (der c r)" |
214 | "ders (c # s) r = ders s (der c r)" |
210 |
215 |
211 |
216 |
212 lemma nullable_correctness: |
217 lemma nullable_correctness: |
213 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
218 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
214 by (induct r) (auto simp add: Sequ_def) |
219 apply(induct r) |
|
220 apply(auto simp add: Sequ_def) |
|
221 done |
215 |
222 |
216 lemma Suc_reduce_Union: |
223 lemma Suc_reduce_Union: |
217 "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))" |
224 "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))" |
218 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) |
225 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) |
219 |
226 |
242 lemma Suc_Union: |
249 lemma Suc_Union: |
243 "(\<Union>x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union>x\<le>m. B x))" |
250 "(\<Union>x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union>x\<le>m. B x))" |
244 by (metis UN_insert atMost_Suc) |
251 by (metis UN_insert atMost_Suc) |
245 |
252 |
246 |
253 |
|
254 lemma Der_Pow_subseteq: |
|
255 assumes "[] \<in> A" |
|
256 shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)" |
|
257 using assms |
|
258 apply(induct n) |
|
259 apply(simp add: Sequ_def Der_def) |
|
260 apply(simp) |
|
261 apply(rule conjI) |
|
262 apply (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI) |
|
263 apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))") |
|
264 apply(auto)[1] |
|
265 by (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI) |
|
266 |
247 lemma test: |
267 lemma test: |
248 shows "(\<Union>x\<le>Suc n. Der c (L r \<up> x)) = (\<Union>x\<le>n. Der c (L r) ;; L r \<up> x)" |
268 shows "(\<Union>x\<le>Suc n. Der c (L r \<up> x)) = (\<Union>x\<le>n. Der c (L r) ;; L r \<up> x)" |
249 apply(induct n) |
269 apply(induct n) |
250 apply(simp) |
270 apply(simp) |
251 apply(auto)[1] |
271 apply(auto)[1] |
256 apply(case_tac "[] \<in> L r") |
276 apply(case_tac "[] \<in> L r") |
257 apply(simp) |
277 apply(simp) |
258 apply(simp) |
278 apply(simp) |
259 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem) |
279 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem) |
260 |
280 |
|
281 lemma Der_Pow_in: |
|
282 assumes "[] \<in> A" |
|
283 shows "Der c (A \<up> n) = (\<Union>x\<le>n. Der c (A \<up> x))" |
|
284 using assms |
|
285 apply(induct n) |
|
286 apply(simp) |
|
287 apply(simp add: Suc_Union) |
|
288 done |
|
289 |
|
290 lemma Der_Pow_notin: |
|
291 assumes "[] \<notin> A" |
|
292 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
|
293 using assms |
|
294 by(simp) |
261 |
295 |
262 lemma der_correctness: |
296 lemma der_correctness: |
263 shows "L (der c r) = Der c (L r)" |
297 shows "L (der c r) = Der c (L r)" |
264 apply(induct c r rule: der.induct) |
298 apply(induct c r rule: der.induct) |
265 apply(simp_all add: nullable_correctness)[7] |
299 apply(simp_all add: nullable_correctness)[7] |
266 apply(simp only: der.simps L.simps) |
300 apply(simp only: der.simps L.simps) |
267 apply(simp only: Der_UNION) |
301 apply(simp only: Der_UNION) |
268 apply(simp only: Seq_UNION[symmetric]) |
302 apply(simp only: Seq_UNION[symmetric]) |
269 apply(simp add: test) |
303 apply(simp add: test) |
270 done |
304 apply(simp) |
|
305 (* NTIMES *) |
|
306 apply(simp only: L.simps der.simps) |
|
307 apply(simp) |
|
308 apply(rule impI) |
|
309 by (simp add: Der_Pow_subseteq sup_absorb1) |
271 |
310 |
272 |
311 |
273 lemma ders_correctness: |
312 lemma ders_correctness: |
274 shows "L (ders s r) = Ders s (L r)" |
313 shows "L (ders s r) = Ders s (L r)" |
275 apply(induct s arbitrary: r) |
314 apply(induct s arbitrary: r) |
343 | "\<turnstile> Stars [] : STAR r" |
382 | "\<turnstile> Stars [] : STAR r" |
344 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r" |
383 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r" |
345 | "\<turnstile> Stars [] : UPNTIMES r 0" |
384 | "\<turnstile> Stars [] : UPNTIMES r 0" |
346 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc n)" |
385 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc n)" |
347 | "\<lbrakk>\<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r (Suc n)" |
386 | "\<lbrakk>\<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r (Suc n)" |
348 |
387 | "\<turnstile> Stars [] : NTIMES r 0" |
|
388 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : NTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : NTIMES r (Suc n)" |
349 |
389 |
350 |
390 |
351 inductive_cases Prf_elims: |
391 inductive_cases Prf_elims: |
352 "\<turnstile> v : ZERO" |
392 "\<turnstile> v : ZERO" |
353 "\<turnstile> v : SEQ r1 r2" |
393 "\<turnstile> v : SEQ r1 r2" |
370 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
410 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
371 shows "\<turnstile> Stars vs : STAR r" |
411 shows "\<turnstile> Stars vs : STAR r" |
372 using assms |
412 using assms |
373 by(induct vs) (auto intro: Prf.intros) |
413 by(induct vs) (auto intro: Prf.intros) |
374 |
414 |
|
415 lemma Prf_Stars_NTIMES: |
|
416 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n" |
|
417 shows "\<turnstile> Stars vs : NTIMES r n" |
|
418 using assms |
|
419 apply(induct vs arbitrary: n) |
|
420 apply(auto intro: Prf.intros) |
|
421 done |
|
422 |
375 lemma Prf_Stars_UPNTIMES: |
423 lemma Prf_Stars_UPNTIMES: |
376 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n" |
424 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n" |
377 shows "\<turnstile> Stars vs : UPNTIMES r n" |
425 shows "\<turnstile> Stars vs : UPNTIMES r n" |
378 using assms |
426 using assms |
379 apply(induct vs arbitrary: n) |
427 apply(induct vs arbitrary: n) |
397 apply(simp_all) |
445 apply(simp_all) |
398 apply(erule Prf.cases) |
446 apply(erule Prf.cases) |
399 apply(simp_all) |
447 apply(simp_all) |
400 apply(auto) |
448 apply(auto) |
401 using le_SucI by blast |
449 using le_SucI by blast |
|
450 |
|
451 lemma NTIMES_Stars: |
|
452 assumes "\<turnstile> v : NTIMES r n" |
|
453 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n" |
|
454 using assms |
|
455 apply(induct n arbitrary: v) |
|
456 apply(erule Prf.cases) |
|
457 apply(simp_all) |
|
458 apply(erule Prf.cases) |
|
459 apply(simp_all) |
|
460 apply(auto) |
|
461 done |
402 |
462 |
403 lemma Star_string: |
463 lemma Star_string: |
404 assumes "s \<in> A\<star>" |
464 assumes "s \<in> A\<star>" |
405 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
465 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
406 using assms |
466 using assms |
475 apply(drule_tac n="length vs" in Prf_Stars_UPNTIMES) |
535 apply(drule_tac n="length vs" in Prf_Stars_UPNTIMES) |
476 apply(simp) |
536 apply(simp) |
477 using Prf_UPNTIMES_bigger apply blast |
537 using Prf_UPNTIMES_bigger apply blast |
478 apply(drule Star_Pow) |
538 apply(drule Star_Pow) |
479 apply(auto) |
539 apply(auto) |
480 using Star_val_length by blast |
540 using Star_val_length apply blast |
|
541 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)") |
|
542 apply(auto)[1] |
|
543 apply(rule_tac x="Stars vs" in exI) |
|
544 apply(simp) |
|
545 apply(rule Prf_Stars_NTIMES) |
|
546 apply(simp) |
|
547 apply(simp) |
|
548 using Star_Pow Star_val_length by blast |
|
549 |
481 |
550 |
482 lemma L_flat_Prf: |
551 lemma L_flat_Prf: |
483 "L(r) = {flat v | v. \<turnstile> v : r}" |
552 "L(r) = {flat v | v. \<turnstile> v : r}" |
484 using L_flat_Prf1 L_flat_Prf2 by blast |
553 using L_flat_Prf1 L_flat_Prf2 by blast |
485 |
554 |
492 "mkeps(ONE) = Void" |
561 "mkeps(ONE) = Void" |
493 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
562 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
494 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
563 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
495 | "mkeps(STAR r) = Stars []" |
564 | "mkeps(STAR r) = Stars []" |
496 | "mkeps(UPNTIMES r n) = Stars []" |
565 | "mkeps(UPNTIMES r n) = Stars []" |
|
566 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
497 |
567 |
498 |
568 |
499 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
569 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
500 where |
570 where |
501 "injval (CHAR d) c Void = Char d" |
571 "injval (CHAR d) c Void = Char d" |
504 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
574 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
505 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
575 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
506 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
576 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
507 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
577 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
508 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
578 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
579 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
580 |
509 |
581 |
510 section {* Mkeps, injval *} |
582 section {* Mkeps, injval *} |
511 |
583 |
512 lemma mkeps_nullable: |
584 lemma mkeps_nullable: |
513 assumes "nullable(r)" |
585 assumes "nullable(r)" |
514 shows "\<turnstile> mkeps r : r" |
586 shows "\<turnstile> mkeps r : r" |
515 using assms |
587 using assms |
516 apply(induct rule: nullable.induct) |
588 apply(induct r rule: mkeps.induct) |
517 apply(auto intro: Prf.intros) |
589 apply(auto intro: Prf.intros) |
518 using Prf.intros(8) Prf_UPNTIMES_bigger by blast |
590 using Prf.intros(8) Prf_UPNTIMES_bigger apply blast |
519 |
591 apply(case_tac n) |
|
592 apply(auto) |
|
593 apply(rule Prf.intros) |
|
594 apply(rule Prf_Stars_NTIMES) |
|
595 apply(simp) |
|
596 apply(simp) |
|
597 done |
520 |
598 |
521 lemma mkeps_flat: |
599 lemma mkeps_flat: |
522 assumes "nullable(r)" |
600 assumes "nullable(r)" |
523 shows "flat (mkeps r) = []" |
601 shows "flat (mkeps r) = []" |
524 using assms |
602 using assms |
549 apply(drule UPNTIMES_Stars) |
627 apply(drule UPNTIMES_Stars) |
550 apply(clarify) |
628 apply(clarify) |
551 apply(simp) |
629 apply(simp) |
552 apply(rule Prf.intros(9)) |
630 apply(rule Prf.intros(9)) |
553 apply(simp) |
631 apply(simp) |
554 using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger by blast |
632 using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger apply blast |
|
633 (* NTIMES *) |
|
634 apply(case_tac x2) |
|
635 apply(simp) |
|
636 using Prf_elims(1) apply auto[1] |
|
637 apply(simp) |
|
638 apply(erule Prf.cases) |
|
639 apply(simp_all) |
|
640 apply(clarify) |
|
641 apply(drule NTIMES_Stars) |
|
642 apply(clarify) |
|
643 apply(simp) |
|
644 apply(rule Prf.intros) |
|
645 apply(simp) |
|
646 using Prf_Stars_NTIMES by blast |
555 |
647 |
556 lemma Prf_injval_flat: |
648 lemma Prf_injval_flat: |
557 assumes "\<turnstile> v : der c r" |
649 assumes "\<turnstile> v : der c r" |
558 shows "flat (injval r c v) = c # (flat v)" |
650 shows "flat (injval r c v) = c # (flat v)" |
559 using assms |
651 using assms |
588 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
683 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
589 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r n \<rightarrow> Stars vs; flat v \<noteq> []; |
684 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r n \<rightarrow> Stars vs; flat v \<noteq> []; |
590 \<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 (UPNTIMES r n))\<rbrakk> |
685 \<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 (UPNTIMES r n))\<rbrakk> |
591 \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
686 \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
592 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
687 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
|
688 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; |
|
689 \<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 (NTIMES r n))\<rbrakk> |
|
690 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
|
691 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
593 |
692 |
594 |
693 |
595 inductive_cases Posix_elims: |
694 inductive_cases Posix_elims: |
596 "s \<in> ZERO \<rightarrow> v" |
695 "s \<in> ZERO \<rightarrow> v" |
597 "s \<in> ONE \<rightarrow> v" |
696 "s \<in> ONE \<rightarrow> v" |
617 using assms |
716 using assms |
618 apply(induct s r v rule: Posix.induct) |
717 apply(induct s r v rule: Posix.induct) |
619 apply(auto intro: Prf.intros) |
718 apply(auto intro: Prf.intros) |
620 using Prf.intros(8) Prf_UPNTIMES_bigger by blast |
719 using Prf.intros(8) Prf_UPNTIMES_bigger by blast |
621 |
720 |
|
721 lemma Posix_NTIMES_mkeps: |
|
722 assumes "[] \<in> r \<rightarrow> mkeps r" |
|
723 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
|
724 apply(induct n) |
|
725 apply(simp) |
|
726 apply (rule Posix_NTIMES2) |
|
727 apply(simp) |
|
728 apply(subst append_Nil[symmetric]) |
|
729 apply (rule Posix_NTIMES1) |
|
730 apply(auto) |
|
731 apply(rule assms) |
|
732 done |
622 |
733 |
623 lemma Posix_mkeps: |
734 lemma Posix_mkeps: |
624 assumes "nullable r" |
735 assumes "nullable r" |
625 shows "[] \<in> r \<rightarrow> mkeps r" |
736 shows "[] \<in> r \<rightarrow> mkeps r" |
626 using assms |
737 using assms |
627 apply(induct r rule: nullable.induct) |
738 apply(induct r rule: nullable.induct) |
628 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
739 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
629 apply(subst append.simps(1)[symmetric]) |
740 apply(subst append.simps(1)[symmetric]) |
630 apply(rule Posix.intros) |
741 apply(rule Posix.intros) |
631 apply(auto) |
742 apply(auto) |
|
743 apply(case_tac n) |
|
744 apply(simp) |
|
745 apply (simp add: Posix_NTIMES2) |
|
746 apply(rule Posix_NTIMES_mkeps) |
|
747 apply(simp) |
632 done |
748 done |
633 |
749 |
634 |
750 |
635 lemma Posix_determ: |
751 lemma Posix_determ: |
636 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
752 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
712 ultimately show "Stars (v # vs) = v2" by auto |
828 ultimately show "Stars (v # vs) = v2" by auto |
713 next |
829 next |
714 case (Posix_UPNTIMES2 r n v2) |
830 case (Posix_UPNTIMES2 r n v2) |
715 have "[] \<in> UPNTIMES r n \<rightarrow> v2" by fact |
831 have "[] \<in> UPNTIMES r n \<rightarrow> v2" by fact |
716 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
832 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
833 next |
|
834 case (Posix_NTIMES2 r v2) |
|
835 have "[] \<in> NTIMES r 0 \<rightarrow> v2" by fact |
|
836 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
837 next |
|
838 case (Posix_NTIMES1 s1 r v s2 n vs v2) |
|
839 have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2" |
|
840 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NTIMES r n) \<rightarrow> Stars vs" |
|
841 "\<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 (NTIMES r n))" by fact+ |
|
842 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')" |
|
843 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
844 using Posix1(1) apply fastforce |
|
845 apply (metis Posix1(1) Posix_NTIMES1.hyps(5) append_Nil append_Nil2) |
|
846 done |
|
847 moreover |
|
848 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
849 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
850 ultimately show "Stars (v # vs) = v2" by auto |
717 qed |
851 qed |
718 |
852 |
719 |
853 |
720 lemma Posix_injval: |
854 lemma Posix_injval: |
721 assumes "s \<in> (der c r) \<rightarrow> v" |
855 assumes "s \<in> (der c r) \<rightarrow> v" |
902 apply(rule_tac Posix.intros(8)) |
1036 apply(rule_tac Posix.intros(8)) |
903 apply(simp_all) |
1037 apply(simp_all) |
904 done |
1038 done |
905 then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" using cons by(simp) |
1039 then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" using cons by(simp) |
906 qed |
1040 qed |
|
1041 next |
|
1042 case (NTIMES r n) |
|
1043 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
1044 have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact |
|
1045 then consider |
|
1046 (cons) m v1 vs s1 s2 where |
|
1047 "n = Suc m" |
|
1048 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
|
1049 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r m) \<rightarrow> (Stars vs)" |
|
1050 "\<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 (NTIMES r m))" |
|
1051 apply(case_tac n) |
|
1052 apply(simp) |
|
1053 using Posix_elims(1) apply blast |
|
1054 apply(simp) |
|
1055 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
|
1056 by (metis NTIMES_Stars Posix1a) |
|
1057 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" |
|
1058 proof (cases) |
|
1059 case cons |
|
1060 have "n = Suc m" by fact |
|
1061 moreover |
|
1062 have "s1 \<in> der c r \<rightarrow> v1" by fact |
|
1063 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
|
1064 moreover |
|
1065 have "s2 \<in> NTIMES r m \<rightarrow> Stars vs" by fact |
|
1066 moreover |
|
1067 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 (NTIMES r m))" by fact |
|
1068 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 (NTIMES r m))" |
|
1069 by (simp add: der_correctness Der_def) |
|
1070 ultimately |
|
1071 have "((c # s1) @ s2) \<in> NTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
|
1072 apply(rule_tac Posix.intros(10)) |
|
1073 apply(simp_all) |
|
1074 done |
|
1075 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
|
1076 qed |
907 qed |
1077 qed |
908 |
1078 |
909 |
1079 |
910 section {* The Lexer by Sulzmann and Lu *} |
1080 section {* The Lexer by Sulzmann and Lu *} |
911 |
1081 |