Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/ReStar.thy
changeset 91 f067e59b58d9
parent 90 3c8cfdf95252
child 92 98d0d77005f3
equal deleted inserted replaced
90:3c8cfdf95252 91:f067e59b58d9 
   199 done
 
   199 done
 
   200 
   200 
   201 section {* Relation between values and regular expressions *}
 
   201 section {* Relation between values and regular expressions *}
 
   202 
   202 
   203 inductive 
   203 inductive 
       
   204   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
       
   205 where
 
       
   206  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
 
       
   207 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
       
   208 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
       
   209 | "\<Turnstile> Void : EMPTY"
 
       
   210 | "\<Turnstile> Char c : CHAR c"
 
       
   211 | "\<Turnstile> Star [] : STAR r"
 
       
   212 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Star vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Star (v # vs) : STAR r"
 
       
   213 
       
   214 
       
   215 inductive 
   204   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   216   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   205 where
 
   217 where
 
   206  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   218  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   207 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   219 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   208 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   220 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   209 | "\<turnstile> Void : EMPTY"
 
   221 | "\<turnstile> Void : EMPTY"
 
   210 | "\<turnstile> Char c : CHAR c"
 
   222 | "\<turnstile> Char c : CHAR c"
 
   211 | "\<turnstile> Star [] : STAR r"
 
   223 | "\<turnstile> Star [] : STAR r"
 
   212 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v#vs) : STAR r"
 
   224 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v # vs) : STAR r"
 
       
   225 
       
   226 lemma NPrf_imp_Prf:
 
       
   227   assumes "\<Turnstile> v : r" 
       
   228   shows "\<turnstile> v : r"
 
       
   229 using assms
 
       
   230 apply(induct)
 
       
   231 apply(auto intro: Prf.intros)
 
       
   232 done
 
   213 
   233 
   214 lemma not_nullable_flat:
 
   234 lemma not_nullable_flat:
 
   215   assumes "\<turnstile> v : r" "\<not>nullable r"
 
   235   assumes "\<turnstile> v : r" "\<not>nullable r"
 
   216   shows "flat v \<noteq> []"
 
   236   shows "flat v \<noteq> []"
 
   217 using assms
 
   237 using assms
 
   274 apply(simp)
 
   294 apply(simp)
 
   275 apply(drule Star_string)
 
   295 apply(drule Star_string)
 
   276 apply(auto)
 
   296 apply(auto)
 
   277 apply(rule Star_val)
 
   297 apply(rule Star_val)
 
   278 apply(simp)
 
   298 apply(simp)
 
       
   299 done
 
       
   300 
       
   301 lemma Prf_Star_flat_L:
 
       
   302   assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
 
       
   303 using assms
 
       
   304 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)
 
       
   305 apply(auto)
 
       
   306 apply(simp add: star3)
 
       
   307 apply(auto)
 
       
   308 apply(rule_tac x="Suc x" in exI)
 
       
   309 apply(auto simp add: Sequ_def)
 
       
   310 apply(rule_tac x="flat v" in exI)
 
       
   311 apply(rule_tac x="flat (Star vs)" in exI)
 
       
   312 apply(auto)
 
       
   313 by (metis Prf_flat_L)
 
       
   314 
       
   315 lemma L_flat_Prf2:
 
       
   316   "L(r) = {flat v | v. \<turnstile> v : r}"
 
       
   317 apply(induct r)
 
       
   318 apply(auto)
 
       
   319 using L.simps(1) Prf_flat_L 
       
   320 apply(blast)
 
       
   321 using Prf.intros(4) 
       
   322 apply(force)
 
       
   323 using L.simps(2) Prf_flat_L 
       
   324 apply(blast)
 
       
   325 using Prf.intros(5) apply force
 
       
   326 using L.simps(3) Prf_flat_L apply blast
 
       
   327 using L_flat_Prf apply auto[1]
 
       
   328 apply (smt L.simps(4) Sequ_def mem_Collect_eq)
 
       
   329 using Prf_flat_L 
       
   330 apply(fastforce)
 
       
   331 apply(metis Prf.intros(2) flat.simps(3))
 
       
   332 apply(metis Prf.intros(3) flat.simps(4))
 
       
   333 apply(erule Prf.cases)
 
       
   334 apply(simp)
 
       
   335 apply(simp)
 
       
   336 apply(auto)
 
       
   337 using L_flat_Prf apply auto[1]
 
       
   338 apply (smt Collect_cong L.simps(6) mem_Collect_eq)
 
       
   339 using Prf_Star_flat_L 
       
   340 apply(fastforce)
 
   279 done
 
   341 done
 
   280 
   342 
   281 
   343 
   282 section {* Values Sets *}
 
   344 section {* Values Sets *}
 
   283 
   345 
   448 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
   510 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
   449 | "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
 
   511 | "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
 
   450 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
   512 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
   451 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
   513 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
   452 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
   514 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
       
   515 | "injval (STAR r) c (Seq v (Star vs)) = Star ((injval r c v) # vs)" 
   453 
   516 
   454 fun 
   517 fun 
   455   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
 
   518   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
 
   456 where
 
   519 where
 
   457   "lex r [] = (if nullable r then Some(mkeps r) else None)"
 
   520   "lex r [] = (if nullable r then Some(mkeps r) else None)"
 
   475 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 
   538 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 
   476 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
   539 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
   477      (if flat v1 = [] then Right(projval r2 c v2) 
   540      (if flat v1 = [] then Right(projval r2 c v2) 
   478       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
   541       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
   479                           else Seq (projval r1 c v1) v2)"
 
   542                           else Seq (projval r1 c v1) v2)"
 
       
   543 | "projval (STAR r) c (Star (v # vs)) = Seq (projval r c v) (Star vs)"
 
   480 
   544 
   481 
   545 
   482 
   546 
   483 lemma mkeps_nullable:
 
   547 lemma mkeps_nullable:
 
   484   assumes "nullable(r)" 
   548   assumes "nullable(r)" 
   494 using assms
 
   558 using assms
 
   495 apply(induct rule: nullable.induct)
 
   559 apply(induct rule: nullable.induct)
 
   496 apply(auto)
 
   560 apply(auto)
 
   497 done
 
   561 done
 
   498 
   562 
   499 (* HERE *)
 
       
   500 
       
   501 lemma v3:
 
   563 lemma v3:
 
   502   assumes "\<turnstile> v : der c r" 
   564   assumes "\<turnstile> v : der c r" 
   503   shows "\<turnstile> (injval r c v) : r"
 
   565   shows "\<turnstile> (injval r c v) : r"
 
   504 using assms
 
   566 using assms
 
   505 apply(induct arbitrary: v rule: der.induct)
 
   567 apply(induct arbitrary: v rule: der.induct)
 
   506 apply(simp)
 
   568 apply(simp)
 
   507 apply(erule Prf.cases)
 
   569 apply(erule Prf.cases)
 
   508 apply(simp_all)[5]
 
   570 apply(simp_all)[7]
 
   509 apply(simp)
 
   571 apply(simp)
 
   510 apply(erule Prf.cases)
 
   572 apply(erule Prf.cases)
 
   511 apply(simp_all)[5]
 
   573 apply(simp_all)[7]
 
   512 apply(case_tac "c = c'")
 
   574 apply(case_tac "c = c'")
 
   513 apply(simp)
 
   575 apply(simp)
 
   514 apply(erule Prf.cases)
 
   576 apply(erule Prf.cases)
 
   515 apply(simp_all)[5]
 
   577 apply(simp_all)[7]
 
   516 apply (metis Prf.intros(5))
 
   578 apply (metis Prf.intros(5))
 
   517 apply(simp)
 
   579 apply(simp)
 
   518 apply(erule Prf.cases)
 
   580 apply(erule Prf.cases)
 
   519 apply(simp_all)[5]
 
   581 apply(simp_all)[7]
 
   520 apply(simp)
 
   582 apply(simp)
 
   521 apply(erule Prf.cases)
 
   583 apply(erule Prf.cases)
 
   522 apply(simp_all)[5]
 
   584 apply(simp_all)[7]
 
   523 apply (metis Prf.intros(2))
 
   585 apply (metis Prf.intros(2))
 
   524 apply (metis Prf.intros(3))
 
   586 apply (metis Prf.intros(3))
 
   525 apply(simp)
 
   587 apply(simp)
 
   526 apply(case_tac "nullable r1")
 
   588 apply(case_tac "nullable r1")
 
   527 apply(simp)
 
   589 apply(simp)
 
   528 apply(erule Prf.cases)
 
   590 apply(erule Prf.cases)
 
   529 apply(simp_all)[5]
 
   591 apply(simp_all)[7]
 
   530 apply(auto)[1]
 
   592 apply(auto)[1]
 
   531 apply(erule Prf.cases)
 
   593 apply(erule Prf.cases)
 
   532 apply(simp_all)[5]
 
   594 apply(simp_all)[7]
 
   533 apply(auto)[1]
 
   595 apply(auto)[1]
 
   534 apply (metis Prf.intros(1))
 
   596 apply (metis Prf.intros(1))
 
   535 apply(auto)[1]
 
   597 apply(auto)[1]
 
   536 apply (metis Prf.intros(1) mkeps_nullable)
 
   598 apply (metis Prf.intros(1) mkeps_nullable)
 
   537 apply(simp)
 
   599 apply(simp)
 
   538 apply(erule Prf.cases)
 
   600 apply(erule Prf.cases)
 
   539 apply(simp_all)[5]
 
   601 apply(simp_all)[7]
 
   540 apply(auto)[1]
 
   602 apply(auto)[1]
 
   541 apply(rule Prf.intros)
 
   603 apply(rule Prf.intros)
 
   542 apply(auto)[2]
 
   604 apply(auto)[2]
 
   543 done
 
   605 apply(simp)
 
       
   606 apply(erule Prf.cases)
 
       
   607 apply(simp_all)[7]
 
       
   608 apply(clarify)
 
       
   609 apply(rotate_tac 2)
 
       
   610 apply(erule Prf.cases)
 
       
   611 apply(simp_all)[7]
 
       
   612 apply(auto)
 
       
   613 apply (metis Prf.intros(6) Prf.intros(7))
 
       
   614 by (metis Prf.intros(7))
 
   544 
   615 
   545 lemma v3_proj:
 
   616 lemma v3_proj:
 
   546   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
   617   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
   547   shows "\<turnstile> (projval r c v) : der c r"
 
   618   shows "\<Turnstile> (projval r c v) : der c r"
 
   548 using assms
 
   619 using assms
 
   549 apply(induct rule: Prf.induct)
 
   620 apply(induct rule: NPrf.induct)
 
   550 prefer 4
 
   621 prefer 4
 
   551 apply(simp)
 
   622 apply(simp)
 
   552 prefer 4
 
   623 prefer 4
 
   553 apply(simp)
 
   624 apply(simp)
 
   554 apply (metis Prf.intros(4))
 
   625 apply (metis NPrf.intros(4))
 
   555 prefer 2
 
   626 prefer 2
 
   556 apply(simp)
 
   627 apply(simp)
 
   557 apply (metis Prf.intros(2))
 
   628 apply (metis NPrf.intros(2))
 
   558 prefer 2
 
   629 prefer 2
 
   559 apply(simp)
 
   630 apply(simp)
 
   560 apply (metis Prf.intros(3))
 
   631 apply (metis NPrf.intros(3))
 
   561 apply(auto)
 
   632 apply(auto)
 
   562 apply(rule Prf.intros)
 
   633 apply(rule NPrf.intros)
 
   563 apply(simp)
 
   634 apply(simp)
 
   564 apply (metis Prf_flat_L nullable_correctness)
 
   635 apply (metis NPrf_imp_Prf not_nullable_flat)
 
   565 apply(rule Prf.intros)
 
   636 apply(rule NPrf.intros)
 
   566 apply(rule Prf.intros)
 
   637 apply(rule NPrf.intros)
 
   567 apply (metis Cons_eq_append_conv)
 
   638 apply (metis Cons_eq_append_conv)
 
   568 apply(simp)
 
   639 apply(simp)
 
   569 apply(rule Prf.intros)
 
   640 apply(rule NPrf.intros)
 
   570 apply (metis Cons_eq_append_conv)
 
   641 apply (metis Cons_eq_append_conv)
 
   571 apply(simp)
 
   642 apply(simp)
 
       
   643 (* Star case *)
 
       
   644 apply(rule NPrf.intros)
 
       
   645 apply (metis Cons_eq_append_conv)
 
       
   646 apply(auto)
 
   572 done
 
   647 done
 
   573 
   648 
   574 lemma v4:
 
   649 lemma v4:
 
   575   assumes "\<turnstile> v : der c r" 
   650   assumes "\<turnstile> v : der c r" 
   576   shows "flat (injval r c v) = c # (flat v)"
 
   651   shows "flat (injval r c v) = c # (flat v)"
 
   577 using assms
 
   652 using assms
 
   578 apply(induct arbitrary: v rule: der.induct)
 
   653 apply(induct arbitrary: v rule: der.induct)
 
   579 apply(simp)
 
   654 apply(simp)
 
   580 apply(erule Prf.cases)
 
   655 apply(erule Prf.cases)
 
   581 apply(simp_all)[5]
 
   656 apply(simp_all)[7]
 
   582 apply(simp)
 
   657 apply(simp)
 
   583 apply(erule Prf.cases)
 
   658 apply(erule Prf.cases)
 
   584 apply(simp_all)[5]
 
   659 apply(simp_all)[7]
 
   585 apply(simp)
 
   660 apply(simp)
 
   586 apply(case_tac "c = c'")
 
   661 apply(case_tac "c = c'")
 
   587 apply(simp)
 
   662 apply(simp)
 
   588 apply(auto)[1]
 
   663 apply(auto)[1]
 
   589 apply(erule Prf.cases)
 
   664 apply(erule Prf.cases)
 
   590 apply(simp_all)[5]
 
   665 apply(simp_all)[7]
 
   591 apply(simp)
 
   666 apply(simp)
 
   592 apply(erule Prf.cases)
 
   667 apply(erule Prf.cases)
 
   593 apply(simp_all)[5]
 
   668 apply(simp_all)[7]
 
   594 apply(simp)
 
   669 apply(simp)
 
   595 apply(erule Prf.cases)
 
   670 apply(erule Prf.cases)
 
   596 apply(simp_all)[5]
 
   671 apply(simp_all)[7]
 
   597 apply(simp)
 
   672 apply(simp)
 
   598 apply(case_tac "nullable r1")
 
   673 apply(case_tac "nullable r1")
 
   599 apply(simp)
 
   674 apply(simp)
 
   600 apply(erule Prf.cases)
 
   675 apply(erule Prf.cases)
 
   601 apply(simp_all (no_asm_use))[5]
 
   676 apply(simp_all (no_asm_use))[7]
 
   602 apply(auto)[1]
 
   677 apply(auto)[1]
 
   603 apply(erule Prf.cases)
 
   678 apply(erule Prf.cases)
 
   604 apply(simp_all)[5]
 
   679 apply(simp_all)[7]
 
   605 apply(clarify)
 
   680 apply(clarify)
 
   606 apply(simp only: injval.simps flat.simps)
 
   681 apply(simp only: injval.simps flat.simps)
 
   607 apply(auto)[1]
 
   682 apply(auto)[1]
 
   608 apply (metis mkeps_flat)
 
   683 apply (metis mkeps_flat)
 
   609 apply(simp)
 
   684 apply(simp)
 
   610 apply(erule Prf.cases)
 
   685 apply(erule Prf.cases)
 
   611 apply(simp_all)[5]
 
   686 apply(simp_all)[7]
 
       
   687 apply(simp)
 
       
   688 apply(erule Prf.cases)
 
       
   689 apply(simp_all)[7]
 
       
   690 apply(auto)
 
       
   691 apply(rotate_tac 2)
 
       
   692 apply(erule Prf.cases)
 
       
   693 apply(simp_all)[7]
 
   612 done
 
   694 done
 
   613 
   695 
   614 lemma v4_proj:
 
   696 lemma v4_proj:
 
   615   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
   697   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
   616   shows "c # flat (projval r c v) = flat v"
 
   698   shows "c # flat (projval r c v) = flat v"
 
   617 using assms
 
   699 using assms
 
   618 apply(induct rule: Prf.induct)
 
   700 apply(induct rule: NPrf.induct)
 
   619 prefer 4
 
   701 prefer 4
 
   620 apply(simp)
 
   702 apply(simp)
 
   621 prefer 4
 
   703 prefer 4
 
   622 apply(simp)
 
   704 apply(simp)
 
   623 prefer 2
 
   705 prefer 2
 
   624 apply(simp)
 
   706 apply(simp)
 
   625 prefer 2
 
   707 prefer 2
 
   626 apply(simp)
 
   708 apply(simp)
 
   627 apply(auto)
 
   709 apply(auto)
 
   628 by (metis Cons_eq_append_conv)
 
   710 apply (metis Cons_eq_append_conv)
 
       
   711 apply(simp add: append_eq_Cons_conv)
 
       
   712 apply(auto)
 
       
   713 done
 
   629 
   714 
   630 lemma v4_proj2:
 
   715 lemma v4_proj2:
 
   631   assumes "\<turnstile> v : r" and "(flat v) = c # s"
 
   716   assumes "\<Turnstile> v : r" and "(flat v) = c # s"
 
   632   shows "flat (projval r c v) = s"
 
   717   shows "flat (projval r c v) = s"
 
   633 using assms
 
   718 using assms
 
   634 by (metis list.inject v4_proj)
 
   719 by (metis list.inject v4_proj)
 
       
   720 
   635 
   721 
   636 
   722 
   637 section {* Alternative Posix definition *}
 
   723 section {* Alternative Posix definition *}
 
   638 
   724 
   639 inductive 
   725 inductive 
   644 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
   730 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
   645 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
   731 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
   646 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
   732 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
   647     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
   733     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
   648     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
   734     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
   649 
   735 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk> \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)"
 
       
   736 | "[] \<in> STAR r \<rightarrow> Star []"
 
   650 
   737 
   651 lemma PMatch_mkeps:
 
   738 lemma PMatch_mkeps:
 
   652   assumes "nullable r"
 
   739   assumes "nullable r"
 
   653   shows "[] \<in> r \<rightarrow> mkeps r"
 
   740   shows "[] \<in> r \<rightarrow> mkeps r"
 
   654 using assms
 
   741 using assms
 
   664 apply(simp)
 
   751 apply(simp)
 
   665 apply (rule PMatch.intros)
 
   752 apply (rule PMatch.intros)
 
   666 apply(simp)
 
   753 apply(simp)
 
   667 apply (rule PMatch.intros)
 
   754 apply (rule PMatch.intros)
 
   668 apply(simp)
 
   755 apply(simp)
 
   669 by (metis nullable_correctness)
 
   756 apply (metis nullable_correctness)
 
   670 
   757 apply(metis PMatch.intros(7))
 
       
   758 done
 
   671 
   759 
   672 lemma PMatch1:
 
   760 lemma PMatch1:
 
   673   assumes "s \<in> r \<rightarrow> v"
 
   761   assumes "s \<in> r \<rightarrow> v"
 
   674   shows "\<turnstile> v : r" "flat v = s"
 
   762   shows "\<turnstile> v : r" "flat v = s"
 
   675 using assms
 
   763 using assms
 
   678 apply (metis Prf.intros(4))
 
   766 apply (metis Prf.intros(4))
 
   679 apply (metis Prf.intros(5))
 
   767 apply (metis Prf.intros(5))
 
   680 apply (metis Prf.intros(2))
 
   768 apply (metis Prf.intros(2))
 
   681 apply (metis Prf.intros(3))
 
   769 apply (metis Prf.intros(3))
 
   682 apply (metis Prf.intros(1))
 
   770 apply (metis Prf.intros(1))
 
       
   771 apply (metis Prf.intros(7))
 
       
   772 by (metis Prf.intros(6))
 
       
   773 
       
   774 lemma PMatch1N:
 
       
   775   assumes "s \<in> r \<rightarrow> v"
 
       
   776   shows "\<Turnstile> v : r" 
       
   777 using assms
 
       
   778 apply(induct s r v rule: PMatch.induct)
 
       
   779 apply(auto)
 
       
   780 apply (metis NPrf.intros(4))
 
       
   781 apply (metis NPrf.intros(5))
 
       
   782 apply (metis NPrf.intros(2))
 
       
   783 apply (metis NPrf.intros(3))
 
       
   784 apply (metis NPrf.intros(1))
 
       
   785 apply (metis NPrf.intros(7) PMatch1(2))
 
       
   786 apply(rule NPrf.intros)
 
   683 done
 
   787 done
 
   684 
   788 
   685 lemma PMatch_Values:
 
   789 lemma PMatch_Values:
 
   686   assumes "s \<in> r \<rightarrow> v"
 
   790   assumes "s \<in> r \<rightarrow> v"
 
   687   shows "v \<in> Values r s"
 
   791   shows "v \<in> Values r s"
 
   694   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 
   798   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 
   695 using assms
 
   799 using assms
 
   696 apply(induct c r arbitrary: s v rule: der.induct)
 
   800 apply(induct c r arbitrary: s v rule: der.induct)
 
   697 apply(auto)
 
   801 apply(auto)
 
   698 apply(erule PMatch.cases)
 
   802 apply(erule PMatch.cases)
 
   699 apply(simp_all)[5]
 
   803 apply(simp_all)[7]
 
   700 apply(erule PMatch.cases)
 
   804 apply(erule PMatch.cases)
 
   701 apply(simp_all)[5]
 
   805 apply(simp_all)[7]
 
   702 apply(case_tac "c = c'")
 
   806 apply(case_tac "c = c'")
 
   703 apply(simp)
 
   807 apply(simp)
 
   704 apply(erule PMatch.cases)
 
   808 apply(erule PMatch.cases)
 
   705 apply(simp_all)[5]
 
   809 apply(simp_all)[7]
 
   706 apply (metis PMatch.intros(2))
 
   810 apply (metis PMatch.intros(2))
 
   707 apply(simp)
 
   811 apply(simp)
 
   708 apply(erule PMatch.cases)
 
   812 apply(erule PMatch.cases)
 
   709 apply(simp_all)[5]
 
   813 apply(simp_all)[7]
 
   710 apply(erule PMatch.cases)
 
   814 apply(erule PMatch.cases)
 
   711 apply(simp_all)[5]
 
   815 apply(simp_all)[7]
 
   712 apply (metis PMatch.intros(3))
 
   816 apply (metis PMatch.intros(3))
 
   713 apply(clarify)
 
   817 apply(clarify)
 
   714 apply(rule PMatch.intros)
 
   818 apply(rule PMatch.intros)
 
   715 apply metis
 
   819 apply metis
 
   716 apply(simp add: L_flat_Prf)
 
   820 apply(simp add: L_flat_Prf)
 
   717 apply(auto)[1]
 
   821 apply(auto)[1]
 
   718 thm v3_proj
 
   822 apply(subgoal_tac "\<Turnstile> v : r1")
 
   719 apply(frule_tac c="c" in v3_proj)
 
   823 apply(frule_tac c="c" in v3_proj)
 
   720 apply metis
 
   824 apply metis
 
   721 apply(drule_tac x="projval r1 c v" in spec)
 
   825 apply(drule_tac x="projval r1 c v" in spec)
 
   722 apply(drule mp)
 
   826 apply(drule mp)
 
   723 apply (metis v4_proj2)
 
   827 apply (metis v4_proj2)
 
   724 apply(simp)
 
   828 apply (metis NPrf_imp_Prf)
 
       
   829 defer
 
       
   830 (* SEQ case *)
 
   725 apply(case_tac "nullable r1")
 
   831 apply(case_tac "nullable r1")
 
   726 apply(simp)
 
   832 apply(simp)
 
   727 defer
 
   833 prefer 2
 
   728 apply(simp)
 
   834 apply(simp)
 
   729 apply(erule PMatch.cases)
 
   835 apply(erule PMatch.cases)
 
   730 apply(simp_all)[5]
 
   836 apply(simp_all)[7]
 
   731 apply(clarify)
 
   837 apply(clarify)
 
   732 apply(subst append.simps(2)[symmetric])
 
   838 apply(subst append.simps(2)[symmetric])
 
   733 apply(rule PMatch.intros)
 
   839 apply(rule PMatch.intros)
 
   734 apply metis
 
   840 apply metis
 
   735 apply metis
 
   841 apply metis
 
   736 apply(auto)[1]
 
   842 apply(auto)[1]
 
   737 apply(simp add: L_flat_Prf)
 
   843 apply(simp add: L_flat_Prf)
 
   738 apply(auto)[1]
 
   844 apply(auto)[1]
 
       
   845 apply(subgoal_tac "\<Turnstile> v : r1")
 
   739 apply(frule_tac c="c" in v3_proj)
 
   846 apply(frule_tac c="c" in v3_proj)
 
   740 apply metis
 
   847 apply metis
 
   741 apply(drule_tac x="s3" in spec)
 
   848 apply(drule_tac x="s3" in spec)
 
   742 apply(drule mp)
 
   849 apply(drule mp)
 
   743 apply(rule_tac x="projval r1 c v" in exI)
 
   850 apply(rule_tac x="projval r1 c v" in exI)
 
   744 apply(rule conjI)
 
   851 apply(rule conjI)
 
   745 apply (metis v4_proj2)
 
   852 apply (metis v4_proj2)
 
   746 apply(simp)
 
   853 apply (metis NPrf_imp_Prf)
 
   747 apply metis
 
   854 apply metis
 
       
   855 defer
 
   748 (* nullable case *)
 
   856 (* nullable case *)
 
   749 apply(erule PMatch.cases)
 
   857 apply(erule PMatch.cases)
 
   750 apply(simp_all)[5]
 
   858 apply(simp_all)[7]
 
   751 apply(clarify)
 
   859 apply(clarify)
 
   752 apply(erule PMatch.cases)
 
   860 apply(erule PMatch.cases)
 
   753 apply(simp_all)[5]
 
   861 apply(simp_all)[7]
 
   754 apply(clarify)
 
   862 apply(clarify)
 
   755 apply(subst append.simps(2)[symmetric])
 
   863 apply(subst append.simps(2)[symmetric])
 
   756 apply(rule PMatch.intros)
 
   864 apply(rule PMatch.intros)
 
   757 apply metis
 
   865 apply metis
 
   758 apply metis
 
   866 apply metis
 
   759 apply(auto)[1]
 
   867 apply(auto)[1]
 
   760 apply(simp add: L_flat_Prf)
 
   868 apply(simp add: L_flat_Prf)
 
   761 apply(auto)[1]
 
   869 apply(auto)[1]
 
       
   870 apply(subgoal_tac "\<Turnstile> v : r1")
 
   762 apply(frule_tac c="c" in v3_proj)
 
   871 apply(frule_tac c="c" in v3_proj)
 
   763 apply metis
 
   872 apply metis
 
   764 apply(drule_tac x="s3" in spec)
 
   873 apply(drule_tac x="s3" in spec)
 
   765 apply(drule mp)
 
   874 apply(drule mp)
 
   766 apply (metis v4_proj2)
 
   875 apply (metis NPrf_imp_Prf v4_proj2)
 
   767 apply(simp)
 
   876 apply(simp)
 
       
   877 defer
 
   768 (* interesting case *)
 
   878 (* interesting case *)
 
   769 apply(clarify)
 
   879 apply(clarify)
 
   770 apply(simp)
 
   880 apply(simp)
 
   771 thm L.simps
 
       
   772 apply(subst (asm) L.simps(4)[symmetric])
 
   881 apply(subst (asm) L.simps(4)[symmetric])
 
   773 apply(simp only: L_flat_Prf)
 
   882 apply(simp only: L_flat_Prf)
 
   774 apply(simp)
 
   883 apply(simp)
 
   775 apply(subst append.simps(1)[symmetric])
 
   884 apply(subst append.simps(1)[symmetric])
 
   776 apply(rule PMatch.intros)
 
   885 apply(rule PMatch.intros)
 
   781 apply(simp)
 
   890 apply(simp)
 
   782 apply(auto)
 
   891 apply(auto)
 
   783 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
 
   892 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
 
   784 apply(drule mp)
 
   893 apply(drule mp)
 
   785 apply(simp)
 
   894 apply(simp)
 
   786 apply (metis append_Cons butlast_snoc last_snoc neq_Nil_conv rotate1.simps(2) v4_proj2)
 
   895 apply(subgoal_tac "\<Turnstile> v : r1")
 
       
   896 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
 
       
   897 defer
 
   787 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
 
   898 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
 
   788 apply (metis Prf.intros(1))
 
   899 apply (metis Prf.intros(1))
 
       
   900 apply(rule NPrf_imp_Prf)
 
   789 apply(rule v3_proj)
 
   901 apply(rule v3_proj)
 
   790 apply(simp)
 
   902 defer
 
   791 by (metis Cons_eq_append_conv)
 
   903 apply (metis Cons_eq_append_conv)
 
       
   904 (* Star case *)
 
       
   905 apply(erule PMatch.cases)
 
       
   906 apply(simp_all)[7]
 
       
   907 apply(clarify)
 
       
   908 apply(rotate_tac 2)
 
       
   909 apply(frule_tac PMatch1)
 
       
   910 apply(erule PMatch.cases)
 
       
   911 apply(simp_all)[7]
 
       
   912 apply(subst append.simps(2)[symmetric])
 
       
   913 apply(rule PMatch.intros)
 
       
   914 apply metis
 
       
   915 apply (metis Nil_is_append_conv PMatch.intros(6))
 
       
   916 apply (metis PMatch1(2) list.distinct(1))
 
       
   917 apply(auto)[1]
 
       
   918 (* HERE *)
 
       
   919 (* oops *)
 
       
   920 
       
   921 
   792 
   922 
   793 lemma lex_correct1:
 
   923 lemma lex_correct1:
 
   794   assumes "s \<notin> L r"
 
   924   assumes "s \<notin> L r"
 
   795   shows "lex r s = None"
 
   925   shows "lex r s = None"
 
   796 using assms
 
   926 using assms
lexing