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 104 59bad592a009
parent 103 ffe5d850df62
child 105 80218dddbb15
equal deleted inserted replaced
103:ffe5d850df62 104:59bad592a009 
   244 apply(auto)
 
   244 apply(auto)
 
   245 done
 
   245 done
 
   246 
   246 
   247 section {* Relation between values and regular expressions *}
 
   247 section {* Relation between values and regular expressions *}
 
   248 
   248 
       
   249 (* non-problematic values...needed in order to fix the *) 
       
   250 (* proj lemma in Sulzmann & lu *)
 
       
   251 
   249 inductive 
   252 inductive 
   250   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
   253   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
   251 where
 
   254 where
 
   252  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
 
   255  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
 
   253 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   256 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   437 
   440 
   438 lemma L_flat_NPrf:
 
   441 lemma L_flat_NPrf:
 
   439   "L(r) = {flat v | v. \<Turnstile> v : r}"
 
   442   "L(r) = {flat v | v. \<Turnstile> v : r}"
 
   440 by (metis L_flat_Prf NPrf_Prf)
 
   443 by (metis L_flat_Prf NPrf_Prf)
 
   441 
   444 
   442 text {* nicer proofs by Fahad *}
 
       
   443 
       
   444 lemma Prf_Star_flat_L:
 
       
   445   assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
 
       
   446 using assms
 
       
   447 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)
 
       
   448 apply(auto)
 
       
   449 apply(simp add: star3)
 
       
   450 apply(auto)
 
       
   451 apply(rule_tac x="Suc x" in exI)
 
       
   452 apply(auto simp add: Sequ_def)
 
       
   453 apply(rule_tac x="flat v" in exI)
 
       
   454 apply(rule_tac x="flat (Stars vs)" in exI)
 
       
   455 apply(auto)
 
       
   456 by (metis Prf_flat_L)
 
       
   457 
       
   458 lemma L_flat_Prf2:
 
       
   459   "L(r) = {flat v | v. \<turnstile> v : r}"
 
       
   460 apply(induct r)
 
       
   461 apply(auto)
 
       
   462 using L.simps(1) Prf_flat_L 
       
   463 apply(blast)
 
       
   464 using Prf.intros(4) 
       
   465 apply(force)
 
       
   466 using L.simps(2) Prf_flat_L 
       
   467 apply(blast)
 
       
   468 using Prf.intros(5) apply force
 
       
   469 using L.simps(3) Prf_flat_L apply blast
 
       
   470 using L_flat_Prf apply auto[1]
 
       
   471 apply (smt L.simps(4) Sequ_def mem_Collect_eq)
 
       
   472 using Prf_flat_L 
       
   473 apply(fastforce)
 
       
   474 apply(metis Prf.intros(2) flat.simps(3))
 
       
   475 apply(metis Prf.intros(3) flat.simps(4))
 
       
   476 apply(erule Prf.cases)
 
       
   477 apply(simp)
 
       
   478 apply(simp)
 
       
   479 apply(auto)
 
       
   480 using L_flat_Prf apply auto[1]
 
       
   481 apply (smt Collect_cong L.simps(6) mem_Collect_eq)
 
       
   482 using Prf_Star_flat_L 
       
   483 apply(fastforce)
 
       
   484 done
 
       
   485 
       
   486 
       
   487 section {* Values Sets *}
 
   445 section {* Values Sets *}
 
   488 
   446 
   489 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
   447 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
   490 where
 
   448 where
 
   491   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
   449   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
   556 done
 
   514 done
 
   557 
   515 
   558 
   516 
   559 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
   517 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
   560   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
   518   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
       
   519 
       
   520 definition SValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
       
   521   "SValues r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
 
   561 
   522 
   562 definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
   523 definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
   563   "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
   524   "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
   564 
   525 
   565 lemma NValues_STAR_Nil:
 
   526 lemma NValues_STAR_Nil:
 
   691 apply (metis NPrf.intros(6))
 
   652 apply (metis NPrf.intros(6))
 
   692 apply (metis append_Nil prefix_def)
 
   653 apply (metis append_Nil prefix_def)
 
   693 apply (metis NPrf.intros(7))
 
   654 apply (metis NPrf.intros(7))
 
   694 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
   655 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
   695 
   656 
       
   657 lemma SValues_recs:
 
       
   658  "SValues (NULL) s = {}"
 
       
   659  "SValues (EMPTY) s = (if s = [] then {Void} else {})"
 
       
   660  "SValues (CHAR c) s = (if [c] = s then {Char c} else {})" 
       
   661  "SValues (ALT r1 r2) s = {Left v | v. v \<in> SValues r1 s} \<union> {Right v | v. v \<in> SValues r2 s}"
 
       
   662  "SValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. \<exists>s1 s2. s = s1 @ s2 \<and> v1 \<in> SValues r1 s1 \<and> v2 \<in> SValues r2 s2}"
 
       
   663  "SValues (STAR r) s = (if s = [] then {Stars []} else {}) \<union> 
       
   664    {Stars (v # vs) | v vs. \<exists>s1 s2. s = s1 @ s2 \<and> v \<in> SValues r s1 \<and> Stars vs \<in> SValues (STAR r) s2}"
 
       
   665 unfolding SValues_def
 
       
   666 apply(auto)
 
       
   667 (*NULL*)
 
       
   668 apply(erule Prf.cases)
 
       
   669 apply(simp_all)[7]
 
       
   670 (*EMPTY*)
 
       
   671 apply(erule Prf.cases)
 
       
   672 apply(simp_all)[7]
 
       
   673 apply(rule Prf.intros)
 
       
   674 apply(erule Prf.cases)
 
       
   675 apply(simp_all)[7]
 
       
   676 (*CHAR*)
 
       
   677 apply(erule Prf.cases)
 
       
   678 apply(simp_all)[7]
 
       
   679 apply (metis Prf.intros(5))
 
       
   680 apply(erule Prf.cases)
 
       
   681 apply(simp_all)[7]
 
       
   682 (*ALT*)
 
       
   683 apply(erule Prf.cases)
 
       
   684 apply(simp_all)[7]
 
       
   685 apply metis
 
       
   686 apply(erule Prf.intros)
 
       
   687 apply(erule Prf.intros)
 
       
   688 (* SEQ case *)
 
       
   689 apply(erule Prf.cases)
 
       
   690 apply(simp_all)[7]
 
       
   691 apply (metis Prf.intros(1))
 
       
   692 (* STAR case *)
 
       
   693 apply(erule Prf.cases)
 
       
   694 apply(simp_all)[7]
 
       
   695 apply(rule Prf.intros)
 
       
   696 apply (metis Prf.intros(7))
 
       
   697 apply(erule Prf.cases)
 
       
   698 apply(simp_all)[7]
 
       
   699 apply (metis Prf.intros(7))
 
       
   700 by (metis Prf.intros(7))
 
   696 
   701 
   697 lemma finite_image_set2:
 
   702 lemma finite_image_set2:
 
   698   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
 
   703   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
 
   699   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
 
   704   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
 
   700 
   705 
   847   lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
 
   852   lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
 
   848 where
 
   853 where
 
   849   "lex2 r [] = mkeps r"
 
   854   "lex2 r [] = mkeps r"
 
   850 | "lex2 r (c#s) = injval r c (lex2 (der c r) s)"
 
   855 | "lex2 r (c#s) = injval r c (lex2 (der c r) s)"
 
   851 
   856 
   852 
       
   853 section {* Projection function *}
 
   857 section {* Projection function *}
 
   854 
   858 
   855 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   859 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   856 where
 
   860 where
 
   857   "projval (CHAR d) c _ = Void"
 
   861   "projval (CHAR d) c _ = Void"
 
   862       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
   866       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
   863                           else Seq (projval r1 c v1) v2)"
 
   867                           else Seq (projval r1 c v1) v2)"
 
   864 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
 
   868 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
 
   865 
   869 
   866 
   870 
   867 
       
   868 lemma mkeps_nullable:
 
   871 lemma mkeps_nullable:
 
   869   assumes "nullable(r)" 
   872   assumes "nullable(r)" 
   870   shows "\<turnstile> mkeps r : r"
 
   873   shows "\<turnstile> mkeps r : r"
 
   871 using assms
 
   874 using assms
 
   872 apply(induct rule: nullable.induct)
 
   875 apply(induct rule: nullable.induct)
 
  1039   shows "flat (projval r c v) = s"
 
  1042   shows "flat (projval r c v) = s"
 
  1040 using assms
 
  1043 using assms
 
  1041 by (metis list.inject v4_proj)
 
  1044 by (metis list.inject v4_proj)
 
  1042 
  1045 
  1043 
  1046 
  1044 section {* Roy's Definition *}
 
  1047 section {* Our Alternative Posix definition *}
 
  1045 
       
  1046 inductive 
       
  1047   Roy :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<rhd> _ : _" [100, 100] 100)
 
       
  1048 where
 
       
  1049   "\<rhd> Void : EMPTY"
 
       
  1050 | "\<rhd> Char c : CHAR c"
 
       
  1051 | "\<rhd> v : r1 \<Longrightarrow> \<rhd> Left v : ALT r1 r2"
 
       
  1052 | "\<lbrakk>\<rhd> v : r2; flat v \<notin> L r1\<rbrakk> \<Longrightarrow> \<rhd> Right v : ALT r1 r2"
 
       
  1053 | "\<lbrakk>\<rhd> v1 : r1; \<rhd> v2 : r2; \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
 
       
  1054       \<rhd> Seq v1 v2 : SEQ r1 r2"
 
       
  1055 | "\<lbrakk>\<rhd> v : r; \<rhd> Stars vs : STAR r; flat v \<noteq> []; 
       
  1056    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> (flat v @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> \<Longrightarrow>
 
       
  1057       \<rhd> Stars (v#vs) : STAR r"
 
       
  1058 | "\<rhd> Stars [] : STAR r"
 
       
  1059 
       
  1060 lemma drop_append:
 
       
  1061   assumes "s1 \<sqsubseteq> s2"
 
       
  1062   shows "s1 @ drop (length s1) s2 = s2"
 
       
  1063 using assms
 
       
  1064 apply(simp add: prefix_def)
 
       
  1065 apply(auto)
 
       
  1066 done
 
       
  1067 
       
  1068 lemma royA: 
       
  1069   assumes "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
 
       
  1070   shows "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1071               s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])" 
       
  1072 using assms
 
       
  1073 apply -
 
       
  1074 apply(rule allI)
 
       
  1075 apply(rule impI)
 
       
  1076 apply(simp add: ders_correctness)
 
       
  1077 apply(simp add: Ders_def)
 
       
  1078 thm rest_def
 
       
  1079 apply(drule_tac x="s" in spec)
 
       
  1080 apply(simp)
 
       
  1081 apply(erule disjE)
 
       
  1082 apply(simp)
 
       
  1083 apply(drule_tac x="drop (length s) (flat v2)" in spec)
 
       
  1084 apply(simp add: drop_append)
 
       
  1085 done
 
       
  1086 
       
  1087 lemma royB:
 
       
  1088   assumes "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1089               s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])"
 
       
  1090   shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
       
  1091 using assms
 
       
  1092 apply -
 
       
  1093 apply(auto simp add: prefix_def ders_correctness Ders_def)
 
       
  1094 by (metis append_eq_conv_conj)
 
       
  1095 
       
  1096 lemma royC: 
       
  1097   assumes "\<forall>s t. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1098                 s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2 @ t) \<in> L r2 \<longrightarrow> s = [])" 
       
  1099   shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
 
       
  1100 using assms
 
       
  1101 apply -
 
       
  1102 apply(rule royB)
 
       
  1103 apply(rule allI)
 
       
  1104 apply(drule_tac x="s" in spec)
 
       
  1105 apply(drule_tac x="[]" in spec)
 
       
  1106 apply(simp)
 
       
  1107 done
 
       
  1108 
       
  1109 inductive 
       
  1110   Roy2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("2\<rhd> _ : _" [100, 100] 100)
 
       
  1111 where
 
       
  1112   "2\<rhd> Void : EMPTY"
 
       
  1113 | "2\<rhd> Char c : CHAR c"
 
       
  1114 | "2\<rhd> v : r1 \<Longrightarrow> 2\<rhd> Left v : ALT r1 r2"
 
       
  1115 | "\<lbrakk>2\<rhd> v : r2; flat v \<notin> L r1\<rbrakk> \<Longrightarrow> 2\<rhd> Right v : ALT r1 r2"
 
       
  1116 | "\<lbrakk>2\<rhd> v1 : r1; 2\<rhd> v2 : r2;
 
       
  1117     \<forall>s t. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1118                 s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2) \<in> (L r2 ;; {t}) \<longrightarrow> s = [])\<rbrakk> \<Longrightarrow>
 
       
  1119     2\<rhd> Seq v1 v2 : SEQ r1 r2"
 
       
  1120 | "\<lbrakk>2\<rhd> v : r; 2\<rhd> Stars vs : STAR r; flat v \<noteq> []; 
       
  1121     \<forall>s t. (s \<in> L(ders (flat v) r) \<and> 
       
  1122               s \<sqsubseteq> (flat (Stars vs) @ t) \<and> drop (length s) (flat (Stars vs)) \<in> (L (STAR r) ;; {t}) \<longrightarrow> s = [])\<rbrakk>\<Longrightarrow>
 
       
  1123     2\<rhd> Stars (v#vs) : STAR r"
 
       
  1124 | "2\<rhd> Stars [] : STAR r"
 
       
  1125 
       
  1126 lemma Roy2_props:
 
       
  1127   assumes "2\<rhd> v : r"
 
       
  1128   shows "\<turnstile> v : r"
 
       
  1129 using assms
 
       
  1130 apply(induct)
 
       
  1131 apply(auto intro: Prf.intros)
 
       
  1132 done
 
       
  1133 
       
  1134 lemma Roy_mkeps_nullable:
 
       
  1135   assumes "nullable(r)" 
       
  1136   shows "2\<rhd> (mkeps r) : r"
 
       
  1137 using assms
 
       
  1138 apply(induct rule: nullable.induct)
 
       
  1139 apply(auto intro: Roy2.intros)
 
       
  1140 apply (metis Roy2.intros(4) mkeps_flat nullable_correctness)
 
       
  1141 apply(rule Roy2.intros)
 
       
  1142 apply(simp_all)
 
       
  1143 apply(rule allI)
 
       
  1144 apply(rule impI)
 
       
  1145 apply(simp add: ders_correctness Ders_def)
 
       
  1146 apply(auto simp add: Sequ_def)
 
       
  1147 apply(simp add: mkeps_flat)
 
       
  1148 apply(auto simp add: prefix_def)
 
       
  1149 done
 
       
  1150 
       
  1151 section {* Alternative Posix definition *}
 
       
  1152 
  1048 
  1153 inductive 
  1049 inductive 
  1154   PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
  1050   PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
  1155 where
 
  1051 where
 
  1156   "[] \<in> EMPTY \<rightarrow> Void"
 
  1052   "[] \<in> EMPTY \<rightarrow> Void"
 
  1163 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
 
  1059 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
 
  1164     \<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>
 
  1060     \<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>
 
  1165     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 
  1061     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 
  1166 | "[] \<in> STAR r \<rightarrow> Stars []"
 
  1062 | "[] \<in> STAR r \<rightarrow> Stars []"
 
  1167 
  1063 
  1168 inductive 
       
  1169   PMatchX :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("\<turnstile> _ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
       
  1170 where
 
       
  1171   "\<turnstile> s \<in> EMPTY \<rightarrow> Void"
 
       
  1172 | "\<turnstile> (c # s) \<in> (CHAR c) \<rightarrow> (Char c)"
 
       
  1173 | "\<turnstile> s \<in> r1 \<rightarrow> v \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
       
  1174 | "\<lbrakk>\<turnstile> s \<in> r2 \<rightarrow> v; \<not>(\<exists>s'. s' \<sqsubseteq> s \<and> flat v \<sqsubseteq> s' \<and> s' \<in> L(r1))\<rbrakk> \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
       
  1175 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; \<turnstile> s2 \<in> r2 \<rightarrow> v2;
 
       
  1176     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> (s3 @ s4) \<sqsubseteq> s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
       
  1177     \<turnstile> (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
       
  1178 | "\<lbrakk>s1 \<in> r \<rightarrow> v; \<turnstile> s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
 
       
  1179     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> (s\<^sub>3 @ s\<^sub>4) \<sqsubseteq> s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
 
       
  1180     \<Longrightarrow> \<turnstile> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 
       
  1181 | "\<turnstile> s \<in> STAR r \<rightarrow> Stars []"
 
       
  1182 
       
  1183 lemma PMatch1:
 
  1064 lemma PMatch1:
 
  1184   assumes "s \<in> r \<rightarrow> v"
 
  1065   assumes "s \<in> r \<rightarrow> v"
 
  1185   shows "\<turnstile> v : r" "flat v = s"
 
  1066   shows "\<turnstile> v : r" "flat v = s"
 
  1186 using assms
 
  1067 using assms
 
  1187 apply(induct s r v rule: PMatch.induct)
 
  1068 apply(induct s r v rule: PMatch.induct)
 
  1192 apply (metis Prf.intros(3))
 
  1073 apply (metis Prf.intros(3))
 
  1193 apply (metis Prf.intros(1))
 
  1074 apply (metis Prf.intros(1))
 
  1194 apply (metis Prf.intros(7))
 
  1075 apply (metis Prf.intros(7))
 
  1195 by (metis Prf.intros(6))
 
  1076 by (metis Prf.intros(6))
 
  1196 
  1077 
  1197 
       
  1198 lemma PMatchX1:
 
       
  1199   assumes "\<turnstile> s \<in> r \<rightarrow> v"
 
       
  1200   shows "\<turnstile> v : r"
 
       
  1201 using assms
 
       
  1202 apply(induct s r v rule: PMatchX.induct)
 
       
  1203 apply(auto simp add: prefix_def intro: Prf.intros)
 
       
  1204 apply (metis PMatch1(1) Prf.intros(1))
 
       
  1205 by (metis PMatch1(1) Prf.intros(7))
 
       
  1206 
       
  1207 
       
  1208 lemma PMatchX:
 
       
  1209   assumes "\<turnstile> s \<in> r \<rightarrow> v"
 
       
  1210   shows "flat v \<sqsubseteq> s"
 
       
  1211 using assms
 
       
  1212 apply(induct s r v rule: PMatchX.induct)
 
       
  1213 apply(auto simp add: prefix_def PMatch1)
 
       
  1214 done
 
       
  1215 
       
  1216 lemma PMatchX_PMatch:
 
       
  1217   assumes "\<turnstile> s \<in> r \<rightarrow> v" "flat v = s"
 
       
  1218   shows "s \<in> r \<rightarrow> v"
 
       
  1219 using assms
 
       
  1220 apply(induct s r v rule: PMatchX.induct)
 
       
  1221 apply(auto intro: PMatch.intros)
 
       
  1222 apply(rule PMatch.intros)
 
       
  1223 apply(simp)
 
       
  1224 apply (metis PMatchX Prefixes_def mem_Collect_eq)
 
       
  1225 apply (smt2 PMatch.intros(5) PMatch1(2) PMatchX append_Nil2 append_assoc append_self_conv prefix_def)
 
       
  1226 by (metis L.simps(6) PMatch.intros(6) PMatch1(2) append_Nil2 append_eq_conv_conj prefix_def)
 
       
  1227 
       
  1228 lemma PMatch_PMatchX:
 
       
  1229   assumes "s \<in> r \<rightarrow> v" 
       
  1230   shows "\<turnstile> s \<in> r \<rightarrow> v"
 
       
  1231 using assms
 
       
  1232 apply(induct s r v arbitrary: s' rule: PMatch.induct)
 
       
  1233 apply(auto intro: PMatchX.intros)
 
       
  1234 apply(rule PMatchX.intros)
 
       
  1235 apply(simp)
 
       
  1236 apply(rule notI)
 
       
  1237 apply(auto)[1]
 
       
  1238 apply (metis PMatch1(2) append_eq_conv_conj length_sprefix less_imp_le_nat prefix_def sprefix_def take_all)
 
       
  1239 apply(rule PMatchX.intros)
 
       
  1240 apply(simp)
 
       
  1241 apply(simp)
 
       
  1242 apply(auto)[1]
 
       
  1243 oops
 
       
  1244 
       
  1245 lemma 
       
  1246   assumes "\<rhd> v : r"
 
       
  1247   shows "(flat v) \<in> r \<rightarrow> v"
 
       
  1248 using assms
 
       
  1249 apply(induct)
 
       
  1250 apply(auto intro: PMatch.intros)
 
       
  1251 apply(rule PMatch.intros)
 
       
  1252 apply(simp)
 
       
  1253 apply(simp)
 
       
  1254 apply(simp)
 
       
  1255 apply(auto)[1]
 
       
  1256 done
 
       
  1257 
       
  1258 lemma 
       
  1259   assumes "s \<in> r \<rightarrow> v"
 
       
  1260   shows "\<rhd> v : r"
 
       
  1261 using assms
 
       
  1262 apply(induct)
 
       
  1263 apply(auto intro: Roy.intros)
 
       
  1264 apply (metis PMatch1(2) Roy.intros(4))
 
       
  1265 apply (metis PMatch1(2) Roy.intros(5))
 
       
  1266 by (metis L.simps(6) PMatch1(2) Roy.intros(6))
 
       
  1267 
       
  1268 
       
  1269 lemma PMatch_mkeps:
 
  1078 lemma PMatch_mkeps:
 
  1270   assumes "nullable r"
 
  1079   assumes "nullable r"
 
  1271   shows "[] \<in> r \<rightarrow> mkeps r"
 
  1080   shows "[] \<in> r \<rightarrow> mkeps r"
 
  1272 using assms
 
  1081 using assms
 
  1273 apply(induct r)
 
  1082 apply(induct r)
 
  1286 apply(simp)
 
  1095 apply(simp)
 
  1287 apply (metis nullable_correctness)
 
  1096 apply (metis nullable_correctness)
 
  1288 apply(metis PMatch.intros(7))
 
  1097 apply(metis PMatch.intros(7))
 
  1289 done
 
  1098 done
 
  1290 
  1099 
       
  1100 lemma PMatch_determ:
 
       
  1101   shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
 
       
  1102   and   "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
 
       
  1103 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts)
 
       
  1104 apply(erule PMatch.cases)
 
       
  1105 apply(simp_all)[7]
 
       
  1106 apply(erule PMatch.cases)
 
       
  1107 apply(simp_all)[7]
 
       
  1108 apply(erule PMatch.cases)
 
       
  1109 apply(simp_all)[7]
 
       
  1110 apply(erule PMatch.cases)
 
       
  1111 apply(simp_all)[7]
 
       
  1112 apply(erule PMatch.cases)
 
       
  1113 apply(simp_all)[7]
 
       
  1114 apply(erule PMatch.cases)
 
       
  1115 apply(simp_all)[7]
 
       
  1116 apply(clarify)
 
       
  1117 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
 
       
  1118 apply metis
 
       
  1119 apply(rule conjI)
 
       
  1120 apply(simp add: append_eq_append_conv2)
 
       
  1121 apply(auto)[1]
 
       
  1122 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1123 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1124 apply(simp add: append_eq_append_conv2)
 
       
  1125 apply(auto)[1]
 
       
  1126 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1127 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1128 apply(erule PMatch.cases)
 
       
  1129 apply(simp_all)[7]
 
       
  1130 apply(clarify)
 
       
  1131 apply(erule PMatch.cases)
 
       
  1132 apply(simp_all)[7]
 
       
  1133 apply(clarify)
 
       
  1134 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1135 apply(erule PMatch.cases)
 
       
  1136 apply(simp_all)[7]
 
       
  1137 apply(clarify)
 
       
  1138 apply(erule PMatch.cases)
 
       
  1139 apply(simp_all)[7]
 
       
  1140 apply(clarify)
 
       
  1141 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1142 (* star case *)
 
       
  1143 defer
 
       
  1144 apply(erule PMatch.cases)
 
       
  1145 apply(simp_all)[7]
 
       
  1146 apply(clarify)
 
       
  1147 apply(erule PMatch.cases)
 
       
  1148 apply(simp_all)[7]
 
       
  1149 apply(clarify)
 
       
  1150 apply (metis PMatch1(2))
 
       
  1151 apply(rotate_tac  3)
 
       
  1152 apply(erule PMatch.cases)
 
       
  1153 apply(simp_all)[7]
 
       
  1154 apply(clarify)
 
       
  1155 apply(erule PMatch.cases)
 
       
  1156 apply(simp_all)[7]
 
       
  1157 apply(clarify)
 
       
  1158 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
 
       
  1159 apply metis
 
       
  1160 apply(simp add: append_eq_append_conv2)
 
       
  1161 apply(auto)[1]
 
       
  1162 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1163 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1164 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1165 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1166 apply(erule PMatch.cases)
 
       
  1167 apply(simp_all)[7]
 
       
  1168 apply(clarify)
 
       
  1169 apply (metis PMatch1(2))
 
       
  1170 apply(erule PMatch.cases)
 
       
  1171 apply(simp_all)[7]
 
       
  1172 apply(clarify)
 
       
  1173 apply(erule PMatch.cases)
 
       
  1174 apply(simp_all)[7]
 
       
  1175 apply(clarify)
 
       
  1176 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
 
       
  1177 apply(drule_tac x="s1 @ s2" in meta_spec)
 
       
  1178 apply(drule_tac x="rb" in meta_spec)
 
       
  1179 apply(drule_tac x="(va#vsa)" in meta_spec)
 
       
  1180 apply(simp)
 
       
  1181 apply(drule meta_mp)
 
       
  1182 apply (metis L.simps(6) PMatch.intros(6))
 
       
  1183 apply (metis L.simps(6) PMatch.intros(6))
 
       
  1184 apply(simp add: append_eq_append_conv2)
 
       
  1185 apply(auto)[1]
 
       
  1186 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1187 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1188 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1189 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1190 apply (metis PMatch1(2))
 
       
  1191 apply(erule PMatch.cases)
 
       
  1192 apply(simp_all)[7]
 
       
  1193 apply(clarify)
 
       
  1194 by (metis PMatch1(2))
 
  1291 
  1195 
  1292 lemma PMatch1N:
 
  1196 lemma PMatch1N:
 
  1293   assumes "s \<in> r \<rightarrow> v"
 
  1197   assumes "s \<in> r \<rightarrow> v"
 
  1294   shows "\<Turnstile> v : r" 
  1198   shows "\<Turnstile> v : r" 
  1295 using assms
 
  1199 using assms
 
  1305 apply(simp)
 
  1209 apply(simp)
 
  1306 apply(simp)
 
  1210 apply(simp)
 
  1307 apply(rule NPrf.intros)
 
  1211 apply(rule NPrf.intros)
 
  1308 done
 
  1212 done
 
  1309 
  1213 
  1310 lemma PMatch_determ:
 
       
  1311   shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
 
       
  1312   and   "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
 
       
  1313 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts)
 
       
  1314 apply(erule PMatch.cases)
 
       
  1315 apply(simp_all)[7]
 
       
  1316 apply(erule PMatch.cases)
 
       
  1317 apply(simp_all)[7]
 
       
  1318 apply(erule PMatch.cases)
 
       
  1319 apply(simp_all)[7]
 
       
  1320 apply(erule PMatch.cases)
 
       
  1321 apply(simp_all)[7]
 
       
  1322 apply(erule PMatch.cases)
 
       
  1323 apply(simp_all)[7]
 
       
  1324 apply(erule PMatch.cases)
 
       
  1325 apply(simp_all)[7]
 
       
  1326 apply(clarify)
 
       
  1327 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
 
       
  1328 apply metis
 
       
  1329 apply(rule conjI)
 
       
  1330 apply(simp add: append_eq_append_conv2)
 
       
  1331 apply(auto)[1]
 
       
  1332 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1333 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1334 apply(simp add: append_eq_append_conv2)
 
       
  1335 apply(auto)[1]
 
       
  1336 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1337 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1338 apply(erule PMatch.cases)
 
       
  1339 apply(simp_all)[7]
 
       
  1340 apply(clarify)
 
       
  1341 apply(erule PMatch.cases)
 
       
  1342 apply(simp_all)[7]
 
       
  1343 apply(clarify)
 
       
  1344 apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
 
       
  1345 apply(erule PMatch.cases)
 
       
  1346 apply(simp_all)[7]
 
       
  1347 apply(clarify)
 
       
  1348 apply(erule PMatch.cases)
 
       
  1349 apply(simp_all)[7]
 
       
  1350 apply(clarify)
 
       
  1351 apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
 
       
  1352 (* star case *)
 
       
  1353 defer
 
       
  1354 apply(erule PMatch.cases)
 
       
  1355 apply(simp_all)[7]
 
       
  1356 apply(clarify)
 
       
  1357 apply(erule PMatch.cases)
 
       
  1358 apply(simp_all)[7]
 
       
  1359 apply(clarify)
 
       
  1360 apply (metis PMatch1(2))
 
       
  1361 apply(rotate_tac  3)
 
       
  1362 apply(erule PMatch.cases)
 
       
  1363 apply(simp_all)[7]
 
       
  1364 apply(clarify)
 
       
  1365 apply(erule PMatch.cases)
 
       
  1366 apply(simp_all)[7]
 
       
  1367 apply(clarify)
 
       
  1368 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
 
       
  1369 apply metis
 
       
  1370 apply(simp add: append_eq_append_conv2)
 
       
  1371 apply(auto)[1]
 
       
  1372 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1373 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1374 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1375 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
 
       
  1376 apply(erule PMatch.cases)
 
       
  1377 apply(simp_all)[7]
 
       
  1378 apply(clarify)
 
       
  1379 apply (metis PMatch1(2))
 
       
  1380 apply(erule PMatch.cases)
 
       
  1381 apply(simp_all)[7]
 
       
  1382 apply(clarify)
 
       
  1383 apply(erule PMatch.cases)
 
       
  1384 apply(simp_all)[7]
 
       
  1385 apply(clarify)
 
       
  1386 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
 
       
  1387 apply(drule_tac x="s1 @ s2" in meta_spec)
 
       
  1388 apply(drule_tac x="rb" in meta_spec)
 
       
  1389 apply(drule_tac x="(va#vsa)" in meta_spec)
 
       
  1390 apply(simp)
 
       
  1391 apply(drule meta_mp)
 
       
  1392 apply (metis L.simps(6) PMatch.intros(6))
 
       
  1393 apply (metis L.simps(6) PMatch.intros(6))
 
       
  1394 apply(simp add: append_eq_append_conv2)
 
       
  1395 apply(auto)[1]
 
       
  1396 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
 
       
  1397 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
 
       
  1398 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
 
       
  1399 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
 
       
  1400 apply (metis PMatch1(2))
 
       
  1401 apply(erule PMatch.cases)
 
       
  1402 apply(simp_all)[7]
 
       
  1403 apply(clarify)
 
       
  1404 by (metis PMatch1(2))
 
       
  1405 
       
  1406 
       
  1407 lemma PMatch_Values:
 
  1214 lemma PMatch_Values:
 
  1408   assumes "s \<in> r \<rightarrow> v"
 
  1215   assumes "s \<in> r \<rightarrow> v"
 
  1409   shows "v \<in> Values r s"
 
  1216   shows "v \<in> Values r s"
 
  1410 using assms
 
  1217 using assms
 
  1411 apply(simp add: Values_def PMatch1)
 
  1218 apply(simp add: Values_def PMatch1)
 
  1433 apply(simp_all)[7]
 
  1240 apply(simp_all)[7]
 
  1434 apply (metis PMatch.intros(3))
 
  1241 apply (metis PMatch.intros(3))
 
  1435 apply(clarify)
 
  1242 apply(clarify)
 
  1436 apply(rule PMatch.intros)
 
  1243 apply(rule PMatch.intros)
 
  1437 apply metis
 
  1244 apply metis
 
  1438 apply(simp add: L_flat_NPrf)
 
  1245 apply(simp add: der_correctness Der_def)
 
  1439 apply(auto)[1]
 
       
  1440 apply(frule_tac c="c" in v3_proj)
 
       
  1441 apply metis
 
       
  1442 apply(drule_tac x="projval r1 c v" in spec)
 
       
  1443 apply(drule mp)
 
       
  1444 apply (metis v4_proj2)
 
       
  1445 apply (metis NPrf_imp_Prf)
 
       
  1446 (* SEQ case *)
 
  1246 (* SEQ case *)
 
  1447 apply(case_tac "nullable r1")
 
  1247 apply(case_tac "nullable r1")
 
  1448 apply(simp)
 
  1248 apply(simp)
 
  1449 prefer 2
 
  1249 prefer 2
 
  1450 apply(simp)
 
  1250 apply(simp)
 
  1471 apply metis
 
  1271 apply metis
 
  1472 apply metis
 
  1272 apply metis
 
  1473 apply(erule contrapos_nn)
 
  1273 apply(erule contrapos_nn)
 
  1474 apply(erule exE)+
 
  1274 apply(erule exE)+
 
  1475 apply(auto)[1]
 
  1275 apply(auto)[1]
 
  1476 apply(simp add: L_flat_NPrf)
 
  1276 apply(simp add: der_correctness Der_def)
 
  1477 apply(auto)[1]
 
       
  1478 thm v3_proj
 
       
  1479 apply(frule_tac c="c" in v3_proj)
 
       
  1480 apply metis
 
  1277 apply metis
 
  1481 apply(rule_tac x="s\<^sub>3" in exI)
 
       
  1482 apply(simp)
 
       
  1483 apply (metis NPrf_imp_Prf v4_proj2)
 
       
  1484 apply(simp)
 
  1278 apply(simp)
 
  1485 (* interesting case *)
 
  1279 (* interesting case *)
 
  1486 apply(clarify)
 
  1280 apply(clarify)
 
  1487 apply(clarify)
 
  1281 apply(clarify)
 
  1488 apply(simp)
 
  1282 apply(simp)
 
  1544 apply(simp)
 
  1338 apply(simp)
 
  1545 apply(subst der_correctness)
 
  1339 apply(subst der_correctness)
 
  1546 apply(simp add: Der_def)
 
  1340 apply(simp add: Der_def)
 
  1547 done
 
  1341 done
 
  1548 
  1342 
  1549 lemma PMatch_Roy2:
 
       
  1550   assumes "2\<rhd> v : (der c r)"
 
       
  1551   shows "2\<rhd> (injval r c v) : r"
 
       
  1552 using assms
 
       
  1553 apply(induct c r arbitrary: v rule: der.induct)
 
       
  1554 apply(auto)
 
       
  1555 apply(erule Roy2.cases)
 
       
  1556 apply(simp_all)
 
       
  1557 apply(erule Roy2.cases)
 
       
  1558 apply(simp_all)
 
       
  1559 apply(case_tac "c = c'")
 
       
  1560 apply(simp)
 
       
  1561 apply(erule Roy2.cases)
 
       
  1562 apply(simp_all)
 
       
  1563 apply (metis Roy2.intros(2))
 
       
  1564 apply(erule Roy2.cases)
 
       
  1565 apply(simp_all)
 
       
  1566 apply(erule Roy2.cases)
 
       
  1567 apply(simp_all)
 
       
  1568 apply(clarify)
 
       
  1569 apply (metis Roy2.intros(3))
 
       
  1570 apply(clarify)
 
       
  1571 apply(rule Roy2.intros(4))
 
       
  1572 apply(metis)
 
       
  1573 apply(simp add: der_correctness Der_def)
 
       
  1574 apply(subst v4)
 
       
  1575 apply (metis Roy2_props)
 
       
  1576 apply(simp)
 
       
  1577 apply(case_tac "nullable r1")
 
       
  1578 apply(simp)
 
       
  1579 apply(erule Roy2.cases)
 
       
  1580 apply(simp_all)
 
       
  1581 apply(clarify)
 
       
  1582 apply(erule Roy2.cases)
 
       
  1583 apply(simp_all)
 
       
  1584 apply(clarify)
 
       
  1585 apply(rule Roy2.intros)
 
       
  1586 apply metis
 
       
  1587 apply(simp)
 
       
  1588 apply(auto)[1]
 
       
  1589 apply(simp add: ders_correctness Ders_def)
 
       
  1590 apply(simp add: der_correctness Der_def)
 
       
  1591 apply(drule_tac x="s" in spec)
 
       
  1592 apply(drule mp)
 
       
  1593 apply(rule conjI)
 
       
  1594 apply(subst (asm) v4)
 
       
  1595 apply (metis Roy2_props)
 
       
  1596 apply(simp)
 
       
  1597 apply(rule_tac x="t" in exI)
 
       
  1598 apply(simp)
 
       
  1599 apply(simp)
 
       
  1600 apply(rule Roy2.intros)
 
       
  1601 apply (metis Roy_mkeps_nullable)
 
       
  1602 apply metis
 
       
  1603 apply(auto)[1]
 
       
  1604 apply(simp add: ders_correctness Ders_def)
 
       
  1605 apply(subst (asm) mkeps_flat)
 
       
  1606 apply(simp)
 
       
  1607 apply(simp)
 
       
  1608 apply(subst (asm) v4)
 
       
  1609 apply (metis Roy2_props)
 
       
  1610 apply(subst (asm) v4)
 
       
  1611 apply (metis Roy2_props)
 
       
  1612 apply(simp add: Sequ_def prefix_def)
 
       
  1613 apply(auto)[1]
 
       
  1614 apply(simp add: append_eq_Cons_conv)
 
       
  1615 apply(auto)
 
       
  1616 apply(drule_tac x="ys'" in spec)
 
       
  1617 apply(drule mp)
 
       
  1618 apply(simp add: der_correctness Der_def)
 
       
  1619 apply(simp add: append_eq_append_conv2)
 
       
  1620 apply(auto)[1]
 
       
  1621 prefer 2
 
       
  1622 apply(erule Roy2.cases)
 
       
  1623 apply(simp_all)
 
       
  1624 apply(rule Roy2.intros)
 
       
  1625 apply metis
 
       
  1626 apply(simp)
 
       
  1627 apply(auto)[1]
 
       
  1628 apply(simp add: ders_correctness Ders_def)
 
       
  1629 apply(subst (asm) v4)
 
       
  1630 apply (metis Roy2_props)
 
       
  1631 apply(drule_tac x="s" in spec)
 
       
  1632 apply(drule mp)
 
       
  1633 apply(rule conjI)
 
       
  1634 apply(simp add: der_correctness Der_def)
 
       
  1635 apply(auto)[1]
 
       
  1636 oops
 
       
  1637 
       
  1638 
       
  1639 lemma lex_correct1:
 
  1343 lemma lex_correct1:
 
  1640   assumes "s \<notin> L r"
 
  1344   assumes "s \<notin> L r"
 
  1641   shows "lex r s = None"
 
  1345   shows "lex r s = None"
 
  1642 using assms
 
  1346 using assms
 
  1643 apply(induct s arbitrary: r)
 
  1347 apply(induct s arbitrary: r)
 
  1710 
  1414 
  1711 lemma 
  1415 lemma 
  1712   "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
 
  1416   "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
 
  1713 apply(simp)
 
  1417 apply(simp)
 
  1714 done
 
  1418 done
 
  1715 
       
  1716 
       
  1717 (* NOT DONE YET *)
 
       
  1718 
  1419 
  1719 section {* Sulzmann's Ordering of values *}
 
  1420 section {* Sulzmann's Ordering of values *}
 
  1720 
  1421 
  1721 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
  1422 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
  1722 where
 
  1423 where
 
  1732 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
 
  1433 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
 
  1733 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
 
  1434 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
 
  1734 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 
  1435 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 
  1735 | "(Stars []) \<succ>(STAR r) (Stars [])"
 
  1436 | "(Stars []) \<succ>(STAR r) (Stars [])"
 
  1736 
  1437 
  1737 inductive ValOrd2 :: "val \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ>_ _" [100, 100, 100] 100)
 
       
  1738 where
 
       
  1739   "v2 2\<succ>s v2' \<Longrightarrow> (Seq v1 v2) 2\<succ>(flat v1 @ s) (Seq v1 v2')" 
       
  1740 | "\<lbrakk>v1 2\<succ>s v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ>s (Seq v1' v2')" 
       
  1741 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ>(flat v1) (Right v2)"
 
       
  1742 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ>(flat v2) (Left v1)"
 
       
  1743 | "v2 2\<succ>s v2' \<Longrightarrow> (Right v2) 2\<succ>s (Right v2')"
 
       
  1744 | "v1 2\<succ>s v1' \<Longrightarrow> (Left v1) 2\<succ>s (Left v1')"
 
       
  1745 | "Void 2\<succ>[] Void"
 
       
  1746 | "(Char c) 2\<succ>[c] (Char c)"
 
       
  1747 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) 2\<succ>[] (Stars (v # vs))"
 
       
  1748 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) 2\<succ>(flat (Stars (v # vs))) (Stars [])"
 
       
  1749 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) 2\<succ>(flat v1) (Stars (v2 # vs2))"
 
       
  1750 | "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))"
 
       
  1751 | "(Stars []) 2\<succ>[] (Stars [])"
 
       
  1752 
       
  1753 lemma admissibility:
 
       
  1754   assumes "\<turnstile> s \<in> r \<rightarrow> v" "\<turnstile> v' : r" 
       
  1755   shows "v \<succ>r v'"
 
       
  1756 using assms
 
       
  1757 apply(induct arbitrary: v')
 
       
  1758 apply(erule Prf.cases)
 
       
  1759 apply(simp_all)[7]
 
       
  1760 apply (metis ValOrd.intros(7))
 
       
  1761 apply(erule Prf.cases)
 
       
  1762 apply(simp_all)[7]
 
       
  1763 apply (metis ValOrd.intros(8))
 
       
  1764 apply(erule Prf.cases)
 
       
  1765 apply(simp_all)[7]
 
       
  1766 apply (metis ValOrd.intros(6))
 
       
  1767 oops
 
       
  1768 
       
  1769 lemma admissibility:
 
       
  1770   assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
 
       
  1771   shows "v \<succ>r v'"
 
       
  1772 using assms
 
       
  1773 apply(induct arbitrary: v')
 
       
  1774 apply(erule Prf.cases)
 
       
  1775 apply(simp_all)[7]
 
       
  1776 apply (metis ValOrd.intros(7))
 
       
  1777 apply(erule Prf.cases)
 
       
  1778 apply(simp_all)[7]
 
       
  1779 apply (metis ValOrd.intros(8))
 
       
  1780 apply(erule Prf.cases)
 
       
  1781 apply(simp_all)[7]
 
       
  1782 apply (metis ValOrd.intros(6))
 
       
  1783 apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
       
  1784 apply(erule Prf.cases)
 
       
  1785 apply(simp_all)[7]
 
       
  1786 apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
       
  1787 apply (metis ValOrd.intros(5))
 
       
  1788 (* Seq case *)
 
       
  1789 apply(erule Prf.cases)
 
       
  1790 apply(clarify)+
 
       
  1791 prefer 2
 
       
  1792 apply(clarify)
 
       
  1793 prefer 2
 
       
  1794 apply(clarify)
 
       
  1795 prefer 2
 
       
  1796 apply(clarify)
 
       
  1797 prefer 2
 
       
  1798 apply(clarify)
 
       
  1799 prefer 2
 
       
  1800 apply(clarify)
 
       
  1801 prefer 2
 
       
  1802 apply(clarify)
 
       
  1803 apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1")
 
       
  1804 prefer 2
 
       
  1805 apply(simp add: prefix_def sprefix_def)
 
       
  1806 apply (metis append_eq_append_conv2)
 
       
  1807 apply(erule disjE)
 
       
  1808 apply(subst (asm) sprefix_def)
 
       
  1809 apply(subst (asm) (5) prefix_def)
 
       
  1810 apply(clarify)
 
       
  1811 apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2")
 
       
  1812 prefer 2
 
       
  1813 apply(simp)
 
       
  1814 apply (metis append_assoc prefix_append)
 
       
  1815 apply(subgoal_tac "s3 \<noteq> []")
 
       
  1816 prefer 2
 
       
  1817 apply (metis append_Nil2)
 
       
  1818 apply(subst (asm) (5) prefix_def)
 
       
  1819 apply(erule exE)
 
       
  1820 apply(drule_tac x="s3" in spec)
 
       
  1821 apply(drule_tac x="s3a" in spec)
 
       
  1822 apply(drule mp)
 
       
  1823 apply(rule conjI)
 
       
  1824 apply(simp add: ders_correctness Ders_def)
 
       
  1825 apply (metis Prf_flat_L)
 
       
  1826 apply(rule conjI)
 
       
  1827 apply(simp)
 
       
  1828 apply (metis append_assoc prefix_def)
 
       
  1829 apply(simp)
 
       
  1830 apply(subgoal_tac "drop (length s3) (flat v2) = flat v2a @ s3a")
 
       
  1831 apply(simp add: Sequ_def)
 
       
  1832 apply (metis Prf_flat_L)
 
       
  1833 thm drop_append
 
       
  1834 apply (metis append_eq_conv_conj)
 
       
  1835 apply(simp)
 
       
  1836 apply (metis ValOrd.intros(1) ValOrd.intros(2) flat.simps(5) prefix_append)
 
       
  1837 (* star cases *)
 
       
  1838 oops
 
       
  1839 
       
  1840 
       
  1841 lemma admisibility:
 
       
  1842   assumes "\<rhd> v : r" "\<turnstile> v' : r"
 
       
  1843   shows "v \<succ>r v'"
 
       
  1844 using assms
 
       
  1845 apply(induct arbitrary: v')
 
       
  1846 prefer 5
 
       
  1847 apply(drule royA)
 
       
  1848 apply(erule Prf.cases)
 
       
  1849 apply(simp_all)[7]
 
       
  1850 apply(clarify)
 
       
  1851 apply(case_tac "v1 = v1a")
 
       
  1852 apply(simp)
 
       
  1853 apply(rule ValOrd.intros)
 
       
  1854 apply metis
 
       
  1855 apply (metis ValOrd.intros(2))
 
       
  1856 apply(erule Prf.cases)
 
       
  1857 apply(simp_all)[7]
 
       
  1858 apply (metis ValOrd.intros(7))
 
       
  1859 apply(erule Prf.cases)
 
       
  1860 apply(simp_all)[7]
 
       
  1861 apply (metis ValOrd.intros(8))
 
       
  1862 apply(erule Prf.cases)
 
       
  1863 apply(simp_all)[7]
 
       
  1864 apply (metis ValOrd.intros(6))
 
       
  1865 apply(rule ValOrd.intros)
 
       
  1866 defer
 
       
  1867 apply(erule Prf.cases)
 
       
  1868 apply(simp_all)[7]
 
       
  1869 apply(clarify)
 
       
  1870 apply(rule ValOrd.intros)
 
       
  1871 (* seq case goes through *)
 
       
  1872 oops
 
       
  1873 
       
  1874 
       
  1875 lemma admisibility:
 
       
  1876   assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
 
       
  1877   shows "v \<succ>r v'"
 
       
  1878 using assms
 
       
  1879 apply(induct arbitrary: v')
 
       
  1880 prefer 5
 
       
  1881 apply(drule royA)
 
       
  1882 apply(erule Prf.cases)
 
       
  1883 apply(simp_all)[7]
 
       
  1884 apply(clarify)
 
       
  1885 apply(case_tac "v1 = v1a")
 
       
  1886 apply(simp)
 
       
  1887 apply(rule ValOrd.intros)
 
       
  1888 apply(subst (asm) (3) prefix_def)
 
       
  1889 apply(erule exE)
 
       
  1890 apply(simp)
 
       
  1891 apply (metis prefix_def)
 
       
  1892 (* the unequal case *)
 
       
  1893 apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1")
 
       
  1894 prefer 2
 
       
  1895 apply(simp add: prefix_def sprefix_def)
 
       
  1896 apply (metis append_eq_append_conv2)
 
       
  1897 apply(erule disjE)
 
       
  1898 (* first case  flat v1 \<sqsubset> flat v1a *)
 
       
  1899 apply(subst (asm) sprefix_def)
 
       
  1900 apply(subst (asm) (5) prefix_def)
 
       
  1901 apply(clarify)
 
       
  1902 apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2")
 
       
  1903 prefer 2
 
       
  1904 apply(simp)
 
       
  1905 apply (metis append_assoc prefix_append)
 
       
  1906 apply(subgoal_tac "s3 \<noteq> []")
 
       
  1907 prefer 2
 
       
  1908 apply (metis append_Nil2)
 
       
  1909 (* HERE *)
 
       
  1910 apply(subst (asm) (5) prefix_def)
 
       
  1911 apply(erule exE)
 
       
  1912 apply(simp add: ders_correctness Ders_def)
 
       
  1913 apply(simp add: prefix_def)
 
       
  1914 apply(clarify)
 
       
  1915 apply(subst (asm) append_eq_append_conv2)
 
       
  1916 apply(erule exE)
 
       
  1917 apply(erule disjE)
 
       
  1918 apply(clarify)
 
       
  1919 oops
 
       
  1920 
       
  1921 
       
  1922 
       
  1923 lemma ValOrd_refl:
 
       
  1924   assumes "\<turnstile> v : r"
 
       
  1925   shows "v \<succ>r v"
 
       
  1926 using assms
 
       
  1927 apply(induct)
 
       
  1928 apply(auto intro: ValOrd.intros)
 
       
  1929 done
 
       
  1930 
       
  1931 lemma ValOrd_total:
 
       
  1932   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
 
       
  1933 apply(induct r arbitrary: v1 v2)
 
       
  1934 apply(auto)
 
       
  1935 apply(erule Prf.cases)
 
       
  1936 apply(simp_all)[7]
 
       
  1937 apply(erule Prf.cases)
 
       
  1938 apply(simp_all)[7]
 
       
  1939 apply(erule Prf.cases)
 
       
  1940 apply(simp_all)[7]
 
       
  1941 apply (metis ValOrd.intros(7))
 
       
  1942 apply(erule Prf.cases)
 
       
  1943 apply(simp_all)[7]
 
       
  1944 apply(erule Prf.cases)
 
       
  1945 apply(simp_all)[7]
 
       
  1946 apply (metis ValOrd.intros(8))
 
       
  1947 apply(erule Prf.cases)
 
       
  1948 apply(simp_all)[7]
 
       
  1949 apply(erule Prf.cases)
 
       
  1950 apply(simp_all)[7]
 
       
  1951 apply(clarify)
 
       
  1952 apply(case_tac "v1a = v1b")
 
       
  1953 apply(simp)
 
       
  1954 apply(rule ValOrd.intros(1))
 
       
  1955 apply (metis ValOrd.intros(1))
 
       
  1956 apply(rule ValOrd.intros(2))
 
       
  1957 apply(auto)[2]
 
       
  1958 apply(erule contrapos_np)
 
       
  1959 apply(rule ValOrd.intros(2))
 
       
  1960 apply(auto)
 
       
  1961 apply(erule Prf.cases)
 
       
  1962 apply(simp_all)[7]
 
       
  1963 apply(erule Prf.cases)
 
       
  1964 apply(simp_all)[7]
 
       
  1965 apply(clarify)
 
       
  1966 apply (metis ValOrd.intros(6))
 
       
  1967 apply(rule ValOrd.intros)
 
       
  1968 apply(erule contrapos_np)
 
       
  1969 apply(rule ValOrd.intros)
 
       
  1970 apply (metis le_eq_less_or_eq neq_iff)
 
       
  1971 apply(erule Prf.cases)
 
       
  1972 apply(simp_all)[7]
 
       
  1973 apply(rule ValOrd.intros)
 
       
  1974 apply(erule contrapos_np)
 
       
  1975 apply(rule ValOrd.intros)
 
       
  1976 apply (metis le_eq_less_or_eq neq_iff)
 
       
  1977 apply(rule ValOrd.intros)
 
       
  1978 apply(erule contrapos_np)
 
       
  1979 apply(rule ValOrd.intros)
 
       
  1980 apply(metis)
 
       
  1981 apply(erule Prf.cases)
 
       
  1982 apply(simp_all)[7]
 
       
  1983 apply(erule Prf.cases)
 
       
  1984 apply(simp_all)[7]
 
       
  1985 apply(auto)
 
       
  1986 apply (metis ValOrd.intros(13))
 
       
  1987 apply (metis ValOrd.intros(10) ValOrd.intros(9))
 
       
  1988 apply(erule Prf.cases)
 
       
  1989 apply(simp_all)[7]
 
       
  1990 apply(auto)
 
       
  1991 apply (metis ValOrd.intros(10) ValOrd.intros(9))
 
       
  1992 apply(case_tac "v = va")
 
       
  1993 prefer 2
 
       
  1994 apply (metis ValOrd.intros(11))
 
       
  1995 apply(simp)
 
       
  1996 apply(rule ValOrd.intros(12))
 
       
  1997 apply(erule contrapos_np)
 
       
  1998 apply(rule ValOrd.intros(12))
 
       
  1999 oops
 
       
  2000 
       
  2001 lemma Roy_posix:
 
       
  2002   assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
 
       
  2003   shows "v \<succ>r v'"
 
       
  2004 using assms
 
       
  2005 apply(induct r arbitrary: v v' rule: rexp.induct)
 
       
  2006 apply(erule Prf.cases)
 
       
  2007 apply(simp_all)[7]
 
       
  2008 apply(erule Prf.cases)
 
       
  2009 apply(simp_all)[7]
 
       
  2010 apply(erule Roy.cases)
 
       
  2011 apply(simp_all)
 
       
  2012 apply (metis ValOrd.intros(7))
 
       
  2013 apply(erule Prf.cases)
 
       
  2014 apply(simp_all)[7]
 
       
  2015 apply(erule Roy.cases)
 
       
  2016 apply(simp_all)
 
       
  2017 apply (metis ValOrd.intros(8))
 
       
  2018 prefer 2
 
       
  2019 apply(erule Prf.cases)
 
       
  2020 apply(simp_all)[7]
 
       
  2021 apply(erule Roy.cases)
 
       
  2022 apply(simp_all)
 
       
  2023 apply(clarify)
 
       
  2024 apply (metis ValOrd.intros(6))
 
       
  2025 apply(clarify)
 
       
  2026 apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
       
  2027 apply(erule Roy.cases)
 
       
  2028 apply(simp_all)
 
       
  2029 apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
       
  2030 apply(clarify)
 
       
  2031 apply (metis ValOrd.intros(5))
 
       
  2032 apply(erule Prf.cases)
 
       
  2033 apply(simp_all)[7]
 
       
  2034 apply(erule Roy.cases)
 
       
  2035 apply(simp_all)
 
       
  2036 apply(clarify)
 
       
  2037 apply(case_tac "v1a = v1")
 
       
  2038 apply(simp)
 
       
  2039 apply(rule ValOrd.intros)
 
       
  2040 apply (metis prefix_append)
 
       
  2041 apply(rule ValOrd.intros)
 
       
  2042 prefer 2
 
       
  2043 apply(simp)
 
       
  2044 apply(simp add: prefix_def)
 
       
  2045 apply(auto)[1]
 
       
  2046 apply(simp add: append_eq_append_conv2)
 
       
  2047 apply(auto)[1]
 
       
  2048 apply(drule_tac x="v1a" in meta_spec)
 
       
  2049 apply(rotate_tac 9)
 
       
  2050 apply(drule_tac x="v1" in meta_spec)
 
       
  2051 apply(drule_tac meta_mp)
 
       
  2052 apply(simp)
 
       
  2053 apply(drule_tac meta_mp)
 
       
  2054 apply(simp)
 
       
  2055 apply(drule_tac meta_mp)
 
       
  2056 apply(simp)
 
       
  2057 apply(drule_tac x="us" in spec)
 
       
  2058 apply(drule_tac mp)
 
       
  2059 apply (metis Prf_flat_L)
 
       
  2060 apply(auto)[1]
 
       
  2061 oops
 
       
  2062 
       
  2063 
       
  2064 lemma ValOrd_anti:
 
       
  2065   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
 
       
  2066   and   "\<lbrakk>\<turnstile> Stars vs1 : r; \<turnstile> Stars vs2 : r; Stars vs1 \<succ>r Stars vs2; Stars vs2 \<succ>r Stars vs1\<rbrakk>  \<Longrightarrow> vs1 = vs2"
 
       
  2067 apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts)
 
       
  2068 apply(erule Prf.cases)
 
       
  2069 apply(simp_all)[7]
 
       
  2070 apply(erule Prf.cases)
 
       
  2071 apply(simp_all)[7]
 
       
  2072 apply(erule Prf.cases)
 
       
  2073 apply(simp_all)[7]
 
       
  2074 apply(erule Prf.cases)
 
       
  2075 apply(simp_all)[7]
 
       
  2076 apply(erule Prf.cases)
 
       
  2077 apply(simp_all)[7]
 
       
  2078 apply(erule Prf.cases)
 
       
  2079 apply(simp_all)[7]
 
       
  2080 apply(erule ValOrd.cases)
 
       
  2081 apply(simp_all)
 
       
  2082 apply(erule ValOrd.cases)
 
       
  2083 apply(simp_all)
 
       
  2084 apply(erule ValOrd.cases)
 
       
  2085 apply(simp_all)
 
       
  2086 apply(erule Prf.cases)
 
       
  2087 apply(simp_all)[7]
 
       
  2088 apply(erule Prf.cases)
 
       
  2089 apply(simp_all)[7]
 
       
  2090 apply(erule ValOrd.cases)
 
       
  2091 apply(simp_all)
 
       
  2092 apply(erule ValOrd.cases)
 
       
  2093 apply(simp_all)
 
       
  2094 apply(erule ValOrd.cases)
 
       
  2095 apply(simp_all)
 
       
  2096 apply(erule ValOrd.cases)
 
       
  2097 apply(simp_all)
 
       
  2098 apply(erule Prf.cases)
 
       
  2099 apply(simp_all)[7]
 
       
  2100 apply(erule Prf.cases)
 
       
  2101 apply(simp_all)[7]
 
       
  2102 apply(erule ValOrd.cases)
 
       
  2103 apply(simp_all)
 
       
  2104 apply(erule ValOrd.cases)
 
       
  2105 apply(simp_all)
 
       
  2106 apply(erule ValOrd.cases)
 
       
  2107 apply(simp_all)
 
       
  2108 apply(erule ValOrd.cases)
 
       
  2109 apply(simp_all)
 
       
  2110 apply(erule Prf.cases)
 
       
  2111 apply(simp_all)[7]
 
       
  2112 apply(erule Prf.cases)
 
       
  2113 apply(simp_all)[7]
 
       
  2114 apply(erule ValOrd.cases)
 
       
  2115 apply(simp_all)
 
       
  2116 apply(erule ValOrd.cases)
 
       
  2117 apply(simp_all)
 
       
  2118 apply(erule Prf.cases)
 
       
  2119 apply(simp_all)[7]
 
       
  2120 apply(erule ValOrd.cases)
 
       
  2121 apply(simp_all)
 
       
  2122 apply(erule ValOrd.cases)
 
       
  2123 apply(simp_all)
 
       
  2124 apply(erule ValOrd.cases)
 
       
  2125 apply(simp_all)
 
       
  2126 apply(erule ValOrd.cases)
 
       
  2127 apply(simp_all)
 
       
  2128 apply(auto)[1]
 
       
  2129 prefer 2
 
       
  2130 oops
 
       
  2131 
       
  2132 
       
  2133 (*
 
       
  2134 
       
  2135 lemma ValOrd_PMatch:
 
       
  2136   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
 
       
  2137   shows "v1 \<succ>r v2"
 
       
  2138 using assms
 
       
  2139 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
 
       
  2140 apply(erule Prf.cases)
 
       
  2141 apply(simp_all)[7]
 
       
  2142 apply(erule Prf.cases)
 
       
  2143 apply(simp_all)[7]
 
       
  2144 apply(erule PMatch.cases)
 
       
  2145 apply(simp_all)[7]
 
       
  2146 apply (metis ValOrd.intros(7))
 
       
  2147 apply(erule Prf.cases)
 
       
  2148 apply(simp_all)[7]
 
       
  2149 apply(erule PMatch.cases)
 
       
  2150 apply(simp_all)[7]
 
       
  2151 apply (metis ValOrd.intros(8))
 
       
  2152 defer
 
       
  2153 apply(erule Prf.cases)
 
       
  2154 apply(simp_all)[7]
 
       
  2155 apply(erule PMatch.cases)
 
       
  2156 apply(simp_all)[7]
 
       
  2157 apply (metis ValOrd.intros(6))
 
       
  2158 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
       
  2159 apply(clarify)
 
       
  2160 apply(erule PMatch.cases)
 
       
  2161 apply(simp_all)[7]
 
       
  2162 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
       
  2163 apply(clarify)
 
       
  2164 apply (metis ValOrd.intros(5))
 
       
  2165 (* Stars case *)
 
       
  2166 apply(erule Prf.cases)
 
       
  2167 apply(simp_all)[7]
 
       
  2168 apply(erule PMatch.cases)
 
       
  2169 apply(simp_all)
 
       
  2170 apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
 
       
  2171 apply (metis ValOrd.intros(13))
 
       
  2172 apply(clarify)
 
       
  2173 apply(erule PMatch.cases)
 
       
  2174 apply(simp_all)
 
       
  2175 prefer 2
 
       
  2176 apply(rule ValOrd.intros)
 
       
  2177 apply(simp add: prefix_def)
 
       
  2178 apply(rule ValOrd.intros)
 
       
  2179 apply(drule_tac x="s1" in meta_spec)
 
       
  2180 apply(drule_tac x="va" in meta_spec)
 
       
  2181 apply(drule_tac x="v" in meta_spec)
 
       
  2182 apply(drule_tac meta_mp)
 
       
  2183 apply(simp)
 
       
  2184 apply(drule_tac meta_mp)
 
       
  2185 apply(simp)
 
       
  2186 apply(drule_tac meta_mp)
 
       
  2187 apply(simp add: prefix_def)
 
       
  2188 apply(auto)[1]
 
       
  2189 prefer 3
 
       
  2190 (* Seq case *)
 
       
  2191 apply(erule Prf.cases)
 
       
  2192 apply(simp_all)[5]
 
       
  2193 apply(auto)
 
       
  2194 apply(erule PMatch.cases)
 
       
  2195 apply(simp_all)[5]
 
       
  2196 apply(auto)
 
       
  2197 apply(case_tac "v1b = v1a")
 
       
  2198 apply(auto)
 
       
  2199 apply(simp add: prefix_def)
 
       
  2200 apply(auto)[1]
 
       
  2201 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
 
       
  2202 apply(simp add: prefix_def)
 
       
  2203 apply(auto)[1]
 
       
  2204 apply(simp add: append_eq_append_conv2)
 
       
  2205 apply(auto)
 
       
  2206 prefer 2
 
       
  2207 apply (metis ValOrd.intros(2))
 
       
  2208 prefer 2
 
       
  2209 apply (metis ValOrd.intros(2))
 
       
  2210 apply(case_tac "us = []")
 
       
  2211 apply(simp)
 
       
  2212 apply (metis ValOrd.intros(2) append_Nil2)
 
       
  2213 apply(drule_tac x="us" in spec)
 
       
  2214 apply(simp)
 
       
  2215 apply(drule_tac mp)
 
       
  2216 apply (metis Prf_flat_L)
 
       
  2217 apply(drule_tac x="s1 @ us" in meta_spec)
 
       
  2218 apply(drule_tac x="v1b" in meta_spec)
 
       
  2219 apply(drule_tac x="v1a" in meta_spec)
 
       
  2220 apply(drule_tac meta_mp)
 
       
  2221 
       
  2222 apply(simp)
 
       
  2223 apply(drule_tac meta_mp)
 
       
  2224 apply(simp)
 
       
  2225 apply(simp)
 
       
  2226 apply(simp)
 
       
  2227 apply(clarify)
 
       
  2228 apply (metis ValOrd.intros(6))
 
       
  2229 apply(clarify)
 
       
  2230 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
       
  2231 apply(erule Prf.cases)
 
       
  2232 apply(simp_all)[5]
 
       
  2233 apply(clarify)
 
       
  2234 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
       
  2235 apply (metis ValOrd.intros(5))
 
       
  2236 (* Seq case *)
 
       
  2237 apply(erule Prf.cases)
 
       
  2238 apply(simp_all)[5]
 
       
  2239 apply(auto)
 
       
  2240 apply(case_tac "v1 = v1a")
 
       
  2241 apply(auto)
 
       
  2242 apply(simp add: prefix_def)
 
       
  2243 apply(auto)[1]
 
       
  2244 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
 
       
  2245 apply(simp add: prefix_def)
 
       
  2246 apply(auto)[1]
 
       
  2247 apply(frule PMatch1)
 
       
  2248 apply(frule PMatch1(2)[symmetric])
 
       
  2249 apply(clarify)
 
       
  2250 apply(simp add: append_eq_append_conv2)
 
       
  2251 apply(auto)
 
       
  2252 prefer 2
 
       
  2253 apply (metis ValOrd.intros(2))
 
       
  2254 prefer 2
 
       
  2255 apply (metis ValOrd.intros(2))
 
       
  2256 apply(case_tac "us = []")
 
       
  2257 apply(simp)
 
       
  2258 apply (metis ValOrd.intros(2) append_Nil2)
 
       
  2259 apply(drule_tac x="us" in spec)
 
       
  2260 apply(simp)
 
       
  2261 apply(drule mp)
 
       
  2262 apply (metis  Prf_flat_L)
 
       
  2263 apply(drule_tac x="v1a" in meta_spec)
 
       
  2264 apply(drule_tac meta_mp)
 
       
  2265 apply(simp)
 
       
  2266 apply(drule_tac meta_mp)
 
       
  2267 apply(simp)
 
       
  2268 
       
  2269 lemma ValOrd_PMatch:
 
       
  2270   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
 
       
  2271   shows "v1 \<succ>r v2"
 
       
  2272 using assms
 
       
  2273 apply(induct arbitrary: v2 rule: .induct)
 
       
  2274 apply(erule Prf.cases)
 
       
  2275 apply(simp_all)[5]
 
       
  2276 apply (metis ValOrd.intros(7))
 
       
  2277 apply(erule Prf.cases)
 
       
  2278 apply(simp_all)[5]
 
       
  2279 apply (metis ValOrd.intros(8))
 
       
  2280 apply(erule Prf.cases)
 
       
  2281 apply(simp_all)[5]
 
       
  2282 apply(clarify)
 
       
  2283 apply (metis ValOrd.intros(6))
 
       
  2284 apply(clarify)
 
       
  2285 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 
       
  2286 apply(erule Prf.cases)
 
       
  2287 apply(simp_all)[5]
 
       
  2288 apply(clarify)
 
       
  2289 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 
       
  2290 apply (metis ValOrd.intros(5))
 
       
  2291 (* Seq case *)
 
       
  2292 apply(erule Prf.cases)
 
       
  2293 apply(simp_all)[5]
 
       
  2294 apply(auto)
 
       
  2295 apply(case_tac "v1 = v1a")
 
       
  2296 apply(auto)
 
       
  2297 apply(simp add: prefix_def)
 
       
  2298 apply(auto)[1]
 
       
  2299 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
 
       
  2300 apply(simp add: prefix_def)
 
       
  2301 apply(auto)[1]
 
       
  2302 apply(frule PMatch1)
 
       
  2303 apply(frule PMatch1(2)[symmetric])
 
       
  2304 apply(clarify)
 
       
  2305 apply(simp add: append_eq_append_conv2)
 
       
  2306 apply(auto)
 
       
  2307 prefer 2
 
       
  2308 apply (metis ValOrd.intros(2))
 
       
  2309 prefer 2
 
       
  2310 apply (metis ValOrd.intros(2))
 
       
  2311 apply(case_tac "us = []")
 
       
  2312 apply(simp)
 
       
  2313 apply (metis ValOrd.intros(2) append_Nil2)
 
       
  2314 apply(drule_tac x="us" in spec)
 
       
  2315 apply(simp)
 
       
  2316 apply(drule mp)
 
       
  2317 apply (metis  Prf_flat_L)
 
       
  2318 apply(drule_tac x="v1a" in meta_spec)
 
       
  2319 apply(drule_tac meta_mp)
 
       
  2320 apply(simp)
 
       
  2321 apply(drule_tac meta_mp)
 
       
  2322 apply(simp)
 
       
  2323 
       
  2324 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
 
       
  2325 apply(rule ValOrd.intros(2))
 
       
  2326 apply(auto)
 
       
  2327 apply(drule_tac x="v1a" in meta_spec)
 
       
  2328 apply(drule_tac meta_mp)
 
       
  2329 apply(simp)
 
       
  2330 apply(drule_tac meta_mp)
 
       
  2331 prefer 2
 
       
  2332 apply(simp)
 
       
  2333 thm append_eq_append_conv
 
       
  2334 apply(simp add: append_eq_append_conv2)
 
       
  2335 apply(auto)
 
       
  2336 apply (metis Prf_flat_L)
 
       
  2337 apply(case_tac "us = []")
 
       
  2338 apply(simp)
 
       
  2339 apply(drule_tac x="us" in spec)
 
       
  2340 apply(drule mp)
 
       
  2341 
       
  2342 
       
  2343 inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100)
 
       
  2344 where
 
       
  2345   "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" 
       
  2346 | "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" 
       
  2347 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"
 
       
  2348 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ> (Left v1)"
 
       
  2349 | "v2 2\<succ> v2' \<Longrightarrow> (Right v2) 2\<succ> (Right v2')"
 
       
  2350 | "v1 2\<succ> v1' \<Longrightarrow> (Left v1) 2\<succ> (Left v1')"
 
       
  2351 | "Void 2\<succ> Void"
 
       
  2352 | "(Char c) 2\<succ> (Char c)"
 
       
  2353 
       
  2354 lemma Ord1:
 
       
  2355   "v1 \<succ>r v2 \<Longrightarrow> v1 2\<succ> v2"
 
       
  2356 apply(induct rule: ValOrd.induct)
 
       
  2357 apply(auto intro: ValOrd2.intros)
 
       
  2358 done
 
       
  2359 
       
  2360 lemma Ord2:
 
       
  2361   "v1 2\<succ> v2 \<Longrightarrow> \<exists>r. v1 \<succ>r v2"
 
       
  2362 apply(induct v1 v2 rule: ValOrd2.induct)
 
       
  2363 apply(auto intro: ValOrd.intros)
 
       
  2364 done
 
       
  2365 
       
  2366 lemma Ord3:
 
       
  2367   "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2"
 
       
  2368 apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct)
 
       
  2369 apply(auto intro: ValOrd.intros elim: Prf.cases)
 
       
  2370 done
 
       
  2371 
       
  2372 section {* Posix definition *}
 
       
  2373 
       
  2374 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
  2375 where
 
       
  2376   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v' \<sqsubseteq> flat v) \<longrightarrow> v \<succ>r v'))"
 
       
  2377 
       
  2378 lemma ValOrd_refl:
 
       
  2379   assumes "\<turnstile> v : r"
 
       
  2380   shows "v \<succ>r v"
 
       
  2381 using assms
 
       
  2382 apply(induct)
 
       
  2383 apply(auto intro: ValOrd.intros)
 
       
  2384 done
 
       
  2385 
       
  2386 lemma ValOrd_total:
 
       
  2387   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
 
       
  2388 apply(induct r arbitrary: v1 v2)
 
       
  2389 apply(auto)
 
       
  2390 apply(erule Prf.cases)
 
       
  2391 apply(simp_all)[5]
 
       
  2392 apply(erule Prf.cases)
 
       
  2393 apply(simp_all)[5]
 
       
  2394 apply(erule Prf.cases)
 
       
  2395 apply(simp_all)[5]
 
       
  2396 apply (metis ValOrd.intros(7))
 
       
  2397 apply(erule Prf.cases)
 
       
  2398 apply(simp_all)[5]
 
       
  2399 apply(erule Prf.cases)
 
       
  2400 apply(simp_all)[5]
 
       
  2401 apply (metis ValOrd.intros(8))
 
       
  2402 apply(erule Prf.cases)
 
       
  2403 apply(simp_all)[5]
 
       
  2404 apply(erule Prf.cases)
 
       
  2405 apply(simp_all)[5]
 
       
  2406 apply(clarify)
 
       
  2407 apply(case_tac "v1a = v1b")
 
       
  2408 apply(simp)
 
       
  2409 apply(rule ValOrd.intros(1))
 
       
  2410 apply (metis ValOrd.intros(1))
 
       
  2411 apply(rule ValOrd.intros(2))
 
       
  2412 apply(auto)[2]
 
       
  2413 apply(erule contrapos_np)
 
       
  2414 apply(rule ValOrd.intros(2))
 
       
  2415 apply(auto)
 
       
  2416 apply(erule Prf.cases)
 
       
  2417 apply(simp_all)[5]
 
       
  2418 apply(erule Prf.cases)
 
       
  2419 apply(simp_all)[5]
 
       
  2420 apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
 
       
  2421 apply(rule ValOrd.intros)
 
       
  2422 apply(erule contrapos_np)
 
       
  2423 apply(rule ValOrd.intros)
 
       
  2424 apply (metis le_eq_less_or_eq neq_iff)
 
       
  2425 apply(erule Prf.cases)
 
       
  2426 apply(simp_all)[5]
 
       
  2427 apply(rule ValOrd.intros)
 
       
  2428 apply(erule contrapos_np)
 
       
  2429 apply(rule ValOrd.intros)
 
       
  2430 apply (metis le_eq_less_or_eq neq_iff)
 
       
  2431 apply(rule ValOrd.intros)
 
       
  2432 apply(erule contrapos_np)
 
       
  2433 apply(rule ValOrd.intros)
 
       
  2434 by metis
 
       
  2435 
       
  2436 lemma ValOrd_anti:
 
       
  2437   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
 
       
  2438 apply(induct r arbitrary: v1 v2)
 
       
  2439 apply(erule Prf.cases)
 
       
  2440 apply(simp_all)[5]
 
       
  2441 apply(erule Prf.cases)
 
       
  2442 apply(simp_all)[5]
 
       
  2443 apply(erule Prf.cases)
 
       
  2444 apply(simp_all)[5]
 
       
  2445 apply(erule Prf.cases)
 
       
  2446 apply(simp_all)[5]
 
       
  2447 apply(erule Prf.cases)
 
       
  2448 apply(simp_all)[5]
 
       
  2449 apply(erule Prf.cases)
 
       
  2450 apply(simp_all)[5]
 
       
  2451 apply(erule Prf.cases)
 
       
  2452 apply(simp_all)[5]
 
       
  2453 apply(erule ValOrd.cases)
 
       
  2454 apply(simp_all)[8]
 
       
  2455 apply(erule ValOrd.cases)
 
       
  2456 apply(simp_all)[8]
 
       
  2457 apply(erule ValOrd.cases)
 
       
  2458 apply(simp_all)[8]
 
       
  2459 apply(erule Prf.cases)
 
       
  2460 apply(simp_all)[5]
 
       
  2461 apply(erule Prf.cases)
 
       
  2462 apply(simp_all)[5]
 
       
  2463 apply(erule ValOrd.cases)
 
       
  2464 apply(simp_all)[8]
 
       
  2465 apply(erule ValOrd.cases)
 
       
  2466 apply(simp_all)[8]
 
       
  2467 apply(erule ValOrd.cases)
 
       
  2468 apply(simp_all)[8]
 
       
  2469 apply(erule ValOrd.cases)
 
       
  2470 apply(simp_all)[8]
 
       
  2471 apply(erule Prf.cases)
 
       
  2472 apply(simp_all)[5]
 
       
  2473 apply(erule ValOrd.cases)
 
       
  2474 apply(simp_all)[8]
 
       
  2475 apply(erule ValOrd.cases)
 
       
  2476 apply(simp_all)[8]
 
       
  2477 apply(erule ValOrd.cases)
 
       
  2478 apply(simp_all)[8]
 
       
  2479 apply(erule ValOrd.cases)
 
       
  2480 apply(simp_all)[8]
 
       
  2481 done
 
       
  2482 
       
  2483 lemma POSIX_ALT_I1:
 
       
  2484   assumes "POSIX v1 r1" 
       
  2485   shows "POSIX (Left v1) (ALT r1 r2)"
 
       
  2486 using assms
 
       
  2487 unfolding POSIX_def
 
       
  2488 apply(auto)
 
       
  2489 apply (metis Prf.intros(2))
 
       
  2490 apply(rotate_tac 2)
 
       
  2491 apply(erule Prf.cases)
 
       
  2492 apply(simp_all)[5]
 
       
  2493 apply(auto)
 
       
  2494 apply(rule ValOrd.intros)
 
       
  2495 apply(auto)
 
       
  2496 apply(rule ValOrd.intros)
 
       
  2497 by (metis le_eq_less_or_eq length_sprefix sprefix_def)
 
       
  2498 
       
  2499 lemma POSIX_ALT_I2:
 
       
  2500   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
 
       
  2501   shows "POSIX (Right v2) (ALT r1 r2)"
 
       
  2502 using assms
 
       
  2503 unfolding POSIX_def
 
       
  2504 apply(auto)
 
       
  2505 apply (metis Prf.intros)
 
       
  2506 apply(rotate_tac 3)
 
       
  2507 apply(erule Prf.cases)
 
       
  2508 apply(simp_all)[5]
 
       
  2509 apply(auto)
 
       
  2510 apply(rule ValOrd.intros)
 
       
  2511 apply metis
 
       
  2512 apply(rule ValOrd.intros)
 
       
  2513 apply metis
 
       
  2514 done
 
       
  2515 
       
  2516 thm PMatch.intros[no_vars]
 
       
  2517 
       
  2518 lemma POSIX_PMatch:
 
       
  2519   assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
 
       
  2520   shows "length (flat v') \<le> length (flat v)" 
       
  2521 using assms
 
       
  2522 apply(induct arbitrary: s v v' rule: rexp.induct)
 
       
  2523 apply(erule Prf.cases)
 
       
  2524 apply(simp_all)[5]
 
       
  2525 apply(erule Prf.cases)
 
       
  2526 apply(simp_all)[5]
 
       
  2527 apply(erule Prf.cases)
 
       
  2528 apply(simp_all)[5]
 
       
  2529 apply(erule PMatch.cases)
 
       
  2530 apply(simp_all)[5]
 
       
  2531 defer
 
       
  2532 apply(erule Prf.cases)
 
       
  2533 apply(simp_all)[5]
 
       
  2534 apply(erule PMatch.cases)
 
       
  2535 apply(simp_all)[5]
 
       
  2536 apply(clarify)
 
       
  2537 apply(simp add: L_flat_Prf)
 
       
  2538 
       
  2539 apply(clarify)
 
       
  2540 apply (metis ValOrd.intros(8))
 
       
  2541 apply (metis POSIX_ALT_I1)
 
       
  2542 apply(rule POSIX_ALT_I2)
 
       
  2543 apply(simp)
 
       
  2544 apply(auto)[1]
 
       
  2545 apply(simp add: POSIX_def)
 
       
  2546 apply(frule PMatch1(1))
 
       
  2547 apply(frule PMatch1(2))
 
       
  2548 apply(simp)
 
       
  2549 
       
  2550 
       
  2551 lemma POSIX_PMatch:
 
       
  2552   assumes "s \<in> r \<rightarrow> v" 
       
  2553   shows "POSIX v r" 
       
  2554 using assms
 
       
  2555 apply(induct arbitrary: rule: PMatch.induct)
 
       
  2556 apply(auto)
 
       
  2557 apply(simp add: POSIX_def)
 
       
  2558 apply(auto)[1]
 
       
  2559 apply (metis Prf.intros(4))
 
       
  2560 apply(erule Prf.cases)
 
       
  2561 apply(simp_all)[5]
 
       
  2562 apply (metis ValOrd.intros(7))
 
       
  2563 apply(simp add: POSIX_def)
 
       
  2564 apply(auto)[1]
 
       
  2565 apply (metis Prf.intros(5))
 
       
  2566 apply(erule Prf.cases)
 
       
  2567 apply(simp_all)[5]
 
       
  2568 apply (metis ValOrd.intros(8))
 
       
  2569 apply (metis POSIX_ALT_I1)
 
       
  2570 apply(rule POSIX_ALT_I2)
 
       
  2571 apply(simp)
 
       
  2572 apply(auto)[1]
 
       
  2573 apply(simp add: POSIX_def)
 
       
  2574 apply(frule PMatch1(1))
 
       
  2575 apply(frule PMatch1(2))
 
       
  2576 apply(simp)
 
       
  2577 
       
  2578 
       
  2579 
       
  2580 lemma ValOrd_PMatch:
 
       
  2581   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s"
 
       
  2582   shows "v1 \<succ>r v2"
 
       
  2583 using assms
 
       
  2584 apply(induct arbitrary: v2 rule: PMatch.induct)
 
       
  2585 apply(erule Prf.cases)
 
       
  2586 apply(simp_all)[5]
 
       
  2587 apply (metis ValOrd.intros(7))
 
       
  2588 apply(erule Prf.cases)
 
       
  2589 apply(simp_all)[5]
 
       
  2590 apply (metis ValOrd.intros(8))
 
       
  2591 apply(erule Prf.cases)
 
       
  2592 apply(simp_all)[5]
 
       
  2593 apply(clarify)
 
       
  2594 apply (metis ValOrd.intros(6))
 
       
  2595 apply(clarify)
 
       
  2596 apply (metis PMatch1(2) ValOrd.intros(3) order_refl)
 
       
  2597 apply(erule Prf.cases)
 
       
  2598 apply(simp_all)[5]
 
       
  2599 apply(clarify)
 
       
  2600 apply (metis Prf_flat_L)
 
       
  2601 apply (metis ValOrd.intros(5))
 
       
  2602 (* Seq case *)
 
       
  2603 apply(erule Prf.cases)
 
       
  2604 apply(simp_all)[5]
 
       
  2605 apply(auto)
 
       
  2606 apply(case_tac "v1 = v1a")
 
       
  2607 apply(auto)
 
       
  2608 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
 
       
  2609 apply(rule ValOrd.intros(2))
 
       
  2610 apply(auto)
 
       
  2611 apply(drule_tac x="v1a" in meta_spec)
 
       
  2612 apply(drule_tac meta_mp)
 
       
  2613 apply(simp)
 
       
  2614 apply(drule_tac meta_mp)
 
       
  2615 prefer 2
 
       
  2616 apply(simp)
 
       
  2617 apply(simp add: append_eq_append_conv2)
 
       
  2618 apply(auto)
 
       
  2619 apply (metis Prf_flat_L)
 
       
  2620 apply(case_tac "us = []")
 
       
  2621 apply(simp)
 
       
  2622 apply(drule_tac x="us" in spec)
 
       
  2623 apply(drule mp)
 
       
  2624 
       
  2625 thm L_flat_Prf
 
       
  2626 apply(simp add: L_flat_Prf)
 
       
  2627 thm append_eq_append_conv2
 
       
  2628 apply(simp add: append_eq_append_conv2)
 
       
  2629 apply(auto)
 
       
  2630 apply(drule_tac x="us" in spec)
 
       
  2631 apply(drule mp)
 
       
  2632 apply metis
 
       
  2633 apply (metis append_Nil2)
 
       
  2634 apply(case_tac "us = []")
 
       
  2635 apply(auto)
 
       
  2636 apply(drule_tac x="s2" in spec)
 
       
  2637 apply(drule mp)
 
       
  2638 
       
  2639 apply(auto)[1]
 
       
  2640 apply(drule_tac x="v1a" in meta_spec)
 
       
  2641 apply(simp)
 
       
  2642 
       
  2643 lemma refl_on_ValOrd:
 
       
  2644   "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}"
 
       
  2645 unfolding refl_on_def
 
       
  2646 apply(auto)
 
       
  2647 apply(rule ValOrd_refl)
 
       
  2648 apply(simp add: Values_def)
 
       
  2649 done
 
       
  2650 
       
  2651 
       
  2652 section {* Posix definition *}
 
       
  2653 
       
  2654 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
  2655 where
 
       
  2656   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
 
       
  2657 
       
  2658 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
  2659 where
 
       
  2660   "POSIX2 v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v 2\<succ> v'))"
 
       
  2661 
       
  2662 lemma "POSIX v r = POSIX2 v r"
 
       
  2663 unfolding POSIX_def POSIX2_def
 
       
  2664 apply(auto)
 
       
  2665 apply(rule Ord1)
 
       
  2666 apply(auto)
 
       
  2667 apply(rule Ord3)
 
       
  2668 apply(auto)
 
       
  2669 done
 
       
  2670 
       
  2671 section {* POSIX for some constructors *}
 
       
  2672 
       
  2673 lemma POSIX_SEQ1:
 
       
  2674   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
       
  2675   shows "POSIX v1 r1"
 
       
  2676 using assms
 
       
  2677 unfolding POSIX_def
 
       
  2678 apply(auto)
 
       
  2679 apply(drule_tac x="Seq v' v2" in spec)
 
       
  2680 apply(simp)
 
       
  2681 apply(erule impE)
 
       
  2682 apply(rule Prf.intros)
 
       
  2683 apply(simp)
 
       
  2684 apply(simp)
 
       
  2685 apply(erule ValOrd.cases)
 
       
  2686 apply(simp_all)
 
       
  2687 apply(clarify)
 
       
  2688 by (metis ValOrd_refl)
 
       
  2689 
       
  2690 lemma POSIX_SEQ2:
 
       
  2691   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
       
  2692   shows "POSIX v2 r2"
 
       
  2693 using assms
 
       
  2694 unfolding POSIX_def
 
       
  2695 apply(auto)
 
       
  2696 apply(drule_tac x="Seq v1 v'" in spec)
 
       
  2697 apply(simp)
 
       
  2698 apply(erule impE)
 
       
  2699 apply(rule Prf.intros)
 
       
  2700 apply(simp)
 
       
  2701 apply(simp)
 
       
  2702 apply(erule ValOrd.cases)
 
       
  2703 apply(simp_all)
 
       
  2704 done
 
       
  2705 
       
  2706 lemma POSIX_ALT2:
 
       
  2707   assumes "POSIX (Left v1) (ALT r1 r2)"
 
       
  2708   shows "POSIX v1 r1"
 
       
  2709 using assms
 
       
  2710 unfolding POSIX_def
 
       
  2711 apply(auto)
 
       
  2712 apply(erule Prf.cases)
 
       
  2713 apply(simp_all)[5]
 
       
  2714 apply(drule_tac x="Left v'" in spec)
 
       
  2715 apply(simp)
 
       
  2716 apply(drule mp)
 
       
  2717 apply(rule Prf.intros)
 
       
  2718 apply(auto)
 
       
  2719 apply(erule ValOrd.cases)
 
       
  2720 apply(simp_all)
 
       
  2721 done
 
       
  2722 
       
  2723 lemma POSIX_ALT1a:
 
       
  2724   assumes "POSIX (Right v2) (ALT r1 r2)"
 
       
  2725   shows "POSIX v2 r2"
 
       
  2726 using assms
 
       
  2727 unfolding POSIX_def
 
       
  2728 apply(auto)
 
       
  2729 apply(erule Prf.cases)
 
       
  2730 apply(simp_all)[5]
 
       
  2731 apply(drule_tac x="Right v'" in spec)
 
       
  2732 apply(simp)
 
       
  2733 apply(drule mp)
 
       
  2734 apply(rule Prf.intros)
 
       
  2735 apply(auto)
 
       
  2736 apply(erule ValOrd.cases)
 
       
  2737 apply(simp_all)
 
       
  2738 done
 
       
  2739 
       
  2740 lemma POSIX_ALT1b:
 
       
  2741   assumes "POSIX (Right v2) (ALT r1 r2)"
 
       
  2742   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
 
       
  2743 using assms
 
       
  2744 apply(drule_tac POSIX_ALT1a)
 
       
  2745 unfolding POSIX_def
 
       
  2746 apply(auto)
 
       
  2747 done
 
       
  2748 
       
  2749 lemma POSIX_ALT_I1:
 
       
  2750   assumes "POSIX v1 r1" 
       
  2751   shows "POSIX (Left v1) (ALT r1 r2)"
 
       
  2752 using assms
 
       
  2753 unfolding POSIX_def
 
       
  2754 apply(auto)
 
       
  2755 apply (metis Prf.intros(2))
 
       
  2756 apply(rotate_tac 2)
 
       
  2757 apply(erule Prf.cases)
 
       
  2758 apply(simp_all)[5]
 
       
  2759 apply(auto)
 
       
  2760 apply(rule ValOrd.intros)
 
       
  2761 apply(auto)
 
       
  2762 apply(rule ValOrd.intros)
 
       
  2763 by simp
 
       
  2764 
       
  2765 lemma POSIX_ALT_I2:
 
       
  2766   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
 
       
  2767   shows "POSIX (Right v2) (ALT r1 r2)"
 
       
  2768 using assms
 
       
  2769 unfolding POSIX_def
 
       
  2770 apply(auto)
 
       
  2771 apply (metis Prf.intros)
 
       
  2772 apply(rotate_tac 3)
 
       
  2773 apply(erule Prf.cases)
 
       
  2774 apply(simp_all)[5]
 
       
  2775 apply(auto)
 
       
  2776 apply(rule ValOrd.intros)
 
       
  2777 apply metis
 
       
  2778 done
 
       
  2779 
       
  2780 lemma mkeps_POSIX:
 
       
  2781   assumes "nullable r"
 
       
  2782   shows "POSIX (mkeps r) r"
 
       
  2783 using assms
 
       
  2784 apply(induct r)
 
       
  2785 apply(auto)[1]
 
       
  2786 apply(simp add: POSIX_def)
 
       
  2787 apply(auto)[1]
 
       
  2788 apply (metis Prf.intros(4))
 
       
  2789 apply(erule Prf.cases)
 
       
  2790 apply(simp_all)[5]
 
       
  2791 apply (metis ValOrd.intros)
 
       
  2792 apply(simp)
 
       
  2793 apply(auto)[1]
 
       
  2794 apply(simp add: POSIX_def)
 
       
  2795 apply(auto)[1]
 
       
  2796 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
 
       
  2797 apply(rotate_tac 6)
 
       
  2798 apply(erule Prf.cases)
 
       
  2799 apply(simp_all)[5]
 
       
  2800 apply (simp add: mkeps_flat)
 
       
  2801 apply(case_tac "mkeps r1a = v1")
 
       
  2802 apply(simp)
 
       
  2803 apply (metis ValOrd.intros(1))
 
       
  2804 apply (rule ValOrd.intros(2))
 
       
  2805 apply metis
 
       
  2806 apply(simp)
 
       
  2807 (* ALT case *)
 
       
  2808 thm mkeps.simps
 
       
  2809 apply(simp)
 
       
  2810 apply(erule disjE)
 
       
  2811 apply(simp)
 
       
  2812 apply (metis POSIX_ALT_I1)
 
       
  2813 (* *)
 
       
  2814 apply(auto)[1]
 
       
  2815 thm  POSIX_ALT_I1
 
       
  2816 apply (metis POSIX_ALT_I1)
 
       
  2817 apply(simp (no_asm) add: POSIX_def)
 
       
  2818 apply(auto)[1]
 
       
  2819 apply(rule Prf.intros(3))
 
       
  2820 apply(simp only: POSIX_def)
 
       
  2821 apply(rotate_tac 4)
 
       
  2822 apply(erule Prf.cases)
 
       
  2823 apply(simp_all)[5]
 
       
  2824 thm mkeps_flat
 
       
  2825 apply(simp add: mkeps_flat)
 
       
  2826 apply(auto)[1]
 
       
  2827 thm Prf_flat_L nullable_correctness
 
       
  2828 apply (metis Prf_flat_L nullable_correctness)
 
       
  2829 apply(rule ValOrd.intros)
 
       
  2830 apply(subst (asm) POSIX_def)
 
       
  2831 apply(clarify)
 
       
  2832 apply(drule_tac x="v2" in spec)
 
       
  2833 by simp
 
       
  2834 
       
  2835 
       
  2836 
       
  2837 text {*
 
       
  2838   Injection value is related to r
 
       
  2839 *}
 
       
  2840 
       
  2841 
       
  2842 
       
  2843 text {*
 
       
  2844   The string behind the injection value is an added c
 
       
  2845 *}
 
       
  2846 
       
  2847 
       
  2848 lemma injval_inj: "inj_on (injval r c) {v. \<turnstile> v : der c r}"
 
       
  2849 apply(induct c r rule: der.induct)
 
       
  2850 unfolding inj_on_def
 
       
  2851 apply(auto)[1]
 
       
  2852 apply(erule Prf.cases)
 
       
  2853 apply(simp_all)[5]
 
       
  2854 apply(auto)[1]
 
       
  2855 apply(erule Prf.cases)
 
       
  2856 apply(simp_all)[5]
 
       
  2857 apply(auto)[1]
 
       
  2858 apply(erule Prf.cases)
 
       
  2859 apply(simp_all)[5]
 
       
  2860 apply(erule Prf.cases)
 
       
  2861 apply(simp_all)[5]
 
       
  2862 apply(erule Prf.cases)
 
       
  2863 apply(simp_all)[5]
 
       
  2864 apply(auto)[1]
 
       
  2865 apply(erule Prf.cases)
 
       
  2866 apply(simp_all)[5]
 
       
  2867 apply(erule Prf.cases)
 
       
  2868 apply(simp_all)[5]
 
       
  2869 apply(erule Prf.cases)
 
       
  2870 apply(simp_all)[5]
 
       
  2871 apply(auto)[1]
 
       
  2872 apply(erule Prf.cases)
 
       
  2873 apply(simp_all)[5]
 
       
  2874 apply(erule Prf.cases)
 
       
  2875 apply(simp_all)[5]
 
       
  2876 apply(clarify)
 
       
  2877 apply(erule Prf.cases)
 
       
  2878 apply(simp_all)[5]
 
       
  2879 apply(erule Prf.cases)
 
       
  2880 apply(simp_all)[5]
 
       
  2881 apply(clarify)
 
       
  2882 apply(erule Prf.cases)
 
       
  2883 apply(simp_all)[5]
 
       
  2884 apply(clarify)
 
       
  2885 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2886 apply(erule Prf.cases)
 
       
  2887 apply(simp_all)[5]
 
       
  2888 apply(clarify)
 
       
  2889 apply(rotate_tac 6)
 
       
  2890 apply(erule Prf.cases)
 
       
  2891 apply(simp_all)[5]
 
       
  2892 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2893 apply(erule Prf.cases)
 
       
  2894 apply(simp_all)[5]
 
       
  2895 apply(erule Prf.cases)
 
       
  2896 apply(simp_all)[5]
 
       
  2897 done
 
       
  2898 
       
  2899 lemma Values_nullable:
 
       
  2900   assumes "nullable r1"
 
       
  2901   shows "mkeps r1 \<in> Values r1 s"
 
       
  2902 using assms
 
       
  2903 apply(induct r1 arbitrary: s)
 
       
  2904 apply(simp_all)
 
       
  2905 apply(simp add: Values_recs)
 
       
  2906 apply(simp add: Values_recs)
 
       
  2907 apply(simp add: Values_recs)
 
       
  2908 apply(auto)[1]
 
       
  2909 done
 
       
  2910 
       
  2911 lemma Values_injval:
 
       
  2912   assumes "v \<in> Values (der c r) s"
 
       
  2913   shows "injval r c v \<in> Values r (c#s)"
 
       
  2914 using assms
 
       
  2915 apply(induct c r arbitrary: v s rule: der.induct)
 
       
  2916 apply(simp add: Values_recs)
 
       
  2917 apply(simp add: Values_recs)
 
       
  2918 apply(case_tac "c = c'")
 
       
  2919 apply(simp)
 
       
  2920 apply(simp add: Values_recs)
 
       
  2921 apply(simp add: prefix_def)
 
       
  2922 apply(simp)
 
       
  2923 apply(simp add: Values_recs)
 
       
  2924 apply(simp)
 
       
  2925 apply(simp add: Values_recs)
 
       
  2926 apply(auto)[1]
 
       
  2927 apply(case_tac "nullable r1")
 
       
  2928 apply(simp)
 
       
  2929 apply(simp add: Values_recs)
 
       
  2930 apply(auto)[1]
 
       
  2931 apply(simp add: rest_def)
 
       
  2932 apply(subst v4)
 
       
  2933 apply(simp add: Values_def)
 
       
  2934 apply(simp add: Values_def)
 
       
  2935 apply(rule Values_nullable)
 
       
  2936 apply(assumption)
 
       
  2937 apply(simp add: rest_def)
 
       
  2938 apply(subst mkeps_flat)
 
       
  2939 apply(assumption)
 
       
  2940 apply(simp)
 
       
  2941 apply(simp)
 
       
  2942 apply(simp add: Values_recs)
 
       
  2943 apply(auto)[1]
 
       
  2944 apply(simp add: rest_def)
 
       
  2945 apply(subst v4)
 
       
  2946 apply(simp add: Values_def)
 
       
  2947 apply(simp add: Values_def)
 
       
  2948 done
 
       
  2949 
       
  2950 lemma Values_projval:
 
       
  2951   assumes "v \<in> Values r (c#s)" "\<exists>s. flat v = c # s"
 
       
  2952   shows "projval r c v \<in> Values (der c r) s"
 
       
  2953 using assms
 
       
  2954 apply(induct r arbitrary: v s c rule: rexp.induct)
 
       
  2955 apply(simp add: Values_recs)
 
       
  2956 apply(simp add: Values_recs)
 
       
  2957 apply(case_tac "c = char")
 
       
  2958 apply(simp)
 
       
  2959 apply(simp add: Values_recs)
 
       
  2960 apply(simp)
 
       
  2961 apply(simp add: Values_recs)
 
       
  2962 apply(simp add: prefix_def)
 
       
  2963 apply(case_tac "nullable rexp1")
 
       
  2964 apply(simp)
 
       
  2965 apply(simp add: Values_recs)
 
       
  2966 apply(auto)[1]
 
       
  2967 apply(simp add: rest_def)
 
       
  2968 apply (metis hd_Cons_tl hd_append2 list.sel(1))
 
       
  2969 apply(simp add: rest_def)
 
       
  2970 apply(simp add: append_eq_Cons_conv)
 
       
  2971 apply(auto)[1]
 
       
  2972 apply(subst v4_proj2)
 
       
  2973 apply(simp add: Values_def)
 
       
  2974 apply(assumption)
 
       
  2975 apply(simp)
 
       
  2976 apply(simp)
 
       
  2977 apply(simp add: Values_recs)
 
       
  2978 apply(auto)[1]
 
       
  2979 apply(auto simp add: Values_def not_nullable_flat)[1]
 
       
  2980 apply(simp add: append_eq_Cons_conv)
 
       
  2981 apply(auto)[1]
 
       
  2982 apply(simp add: append_eq_Cons_conv)
 
       
  2983 apply(auto)[1]
 
       
  2984 apply(simp add: rest_def)
 
       
  2985 apply(subst v4_proj2)
 
       
  2986 apply(simp add: Values_def)
 
       
  2987 apply(assumption)
 
       
  2988 apply(simp)
 
       
  2989 apply(simp add: Values_recs)
 
       
  2990 apply(auto)[1]
 
       
  2991 done
 
       
  2992 
       
  2993 
       
  2994 definition "MValue v r s \<equiv> (v \<in> Values r s \<and> (\<forall>v' \<in> Values r s. v 2\<succ> v'))"
 
       
  2995 
       
  2996 lemma MValue_ALTE:
 
       
  2997   assumes "MValue v (ALT r1 r2) s"
 
       
  2998   shows "(\<exists>vl. v = Left vl \<and> MValue vl r1 s \<and> (\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl))) \<or> 
       
  2999          (\<exists>vr. v = Right vr \<and> MValue vr r2 s \<and> (\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)))"
 
       
  3000 using assms
 
       
  3001 apply(simp add: MValue_def)
 
       
  3002 apply(simp add: Values_recs)
 
       
  3003 apply(auto)
 
       
  3004 apply(drule_tac x="Left x" in bspec)
 
       
  3005 apply(simp)
 
       
  3006 apply(erule ValOrd2.cases)
 
       
  3007 apply(simp_all)
 
       
  3008 apply(drule_tac x="Right vr" in bspec)
 
       
  3009 apply(simp)
 
       
  3010 apply(erule ValOrd2.cases)
 
       
  3011 apply(simp_all)
 
       
  3012 apply(drule_tac x="Right x" in bspec)
 
       
  3013 apply(simp)
 
       
  3014 apply(erule ValOrd2.cases)
 
       
  3015 apply(simp_all)
 
       
  3016 apply(drule_tac x="Left vl" in bspec)
 
       
  3017 apply(simp)
 
       
  3018 apply(erule ValOrd2.cases)
 
       
  3019 apply(simp_all)
 
       
  3020 done
 
       
  3021 
       
  3022 lemma MValue_ALTI1:
 
       
  3023   assumes "MValue vl r1 s"  "\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl)"
 
       
  3024   shows "MValue (Left vl) (ALT r1 r2) s"
 
       
  3025 using assms
 
       
  3026 apply(simp add: MValue_def)
 
       
  3027 apply(simp add: Values_recs)
 
       
  3028 apply(auto)
 
       
  3029 apply(rule ValOrd2.intros)
 
       
  3030 apply metis
 
       
  3031 apply(rule ValOrd2.intros)
 
       
  3032 apply metis
 
       
  3033 done
 
       
  3034 
       
  3035 lemma MValue_ALTI2:
 
       
  3036   assumes "MValue vr r2 s"  "\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)"
 
       
  3037   shows "MValue (Right vr) (ALT r1 r2) s"
 
       
  3038 using assms
 
       
  3039 apply(simp add: MValue_def)
 
       
  3040 apply(simp add: Values_recs)
 
       
  3041 apply(auto)
 
       
  3042 apply(rule ValOrd2.intros)
 
       
  3043 apply metis
 
       
  3044 apply(rule ValOrd2.intros)
 
       
  3045 apply metis
 
       
  3046 done
 
       
  3047 
       
  3048 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 
       
  3049 by (metis list.sel(3))
 
       
  3050 
       
  3051 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
       
  3052 by (metis)
 
       
  3053 
       
  3054 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
       
  3055 by (metis Prf_flat_L nullable_correctness)
 
       
  3056 
       
  3057 
       
  3058 lemma LeftRight:
 
       
  3059   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
 
       
  3060   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
       
  3061   shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"
 
       
  3062 using assms
 
       
  3063 apply(simp)
 
       
  3064 apply(erule ValOrd.cases)
 
       
  3065 apply(simp_all)[8]
 
       
  3066 apply(rule ValOrd.intros)
 
       
  3067 apply(clarify)
 
       
  3068 apply(subst v4)
 
       
  3069 apply(simp)
 
       
  3070 apply(subst v4)
 
       
  3071 apply(simp)
 
       
  3072 apply(simp)
 
       
  3073 done
 
       
  3074 
       
  3075 lemma RightLeft:
 
       
  3076   assumes "(Right v1) \<succ>(der c (ALT r1 r2)) (Left v2)"
 
       
  3077   and "\<turnstile> v1 : der c r2" "\<turnstile> v2 : der c r1" 
       
  3078   shows "(injval (ALT r1 r2) c (Right v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Left v2))"
 
       
  3079 using assms
 
       
  3080 apply(simp)
 
       
  3081 apply(erule ValOrd.cases)
 
       
  3082 apply(simp_all)[8]
 
       
  3083 apply(rule ValOrd.intros)
 
       
  3084 apply(clarify)
 
       
  3085 apply(subst v4)
 
       
  3086 apply(simp)
 
       
  3087 apply(subst v4)
 
       
  3088 apply(simp)
 
       
  3089 apply(simp)
 
       
  3090 done
 
       
  3091 
       
  3092 lemma h: 
       
  3093   assumes "nullable r1" "\<turnstile> v1 : der c r1"
 
       
  3094   shows "injval r1 c v1 \<succ>r1 mkeps r1"
 
       
  3095 using assms
 
       
  3096 apply(induct r1 arbitrary: v1 rule: der.induct)
 
       
  3097 apply(simp)
 
       
  3098 apply(simp)
 
       
  3099 apply(erule Prf.cases)
 
       
  3100 apply(simp_all)[5]
 
       
  3101 apply(simp)
 
       
  3102 apply(simp)
 
       
  3103 apply(erule Prf.cases)
 
       
  3104 apply(simp_all)[5]
 
       
  3105 apply(clarify)
 
       
  3106 apply(auto)[1]
 
       
  3107 apply (metis ValOrd.intros(6))
 
       
  3108 apply (metis ValOrd.intros(6))
 
       
  3109 apply (metis ValOrd.intros(3) le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral)
 
       
  3110 apply(auto)[1]
 
       
  3111 apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
 
       
  3112 apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
 
       
  3113 apply (metis ValOrd.intros(5))
 
       
  3114 apply(simp)
 
       
  3115 apply(erule Prf.cases)
 
       
  3116 apply(simp_all)[5]
 
       
  3117 apply(clarify)
 
       
  3118 apply(erule Prf.cases)
 
       
  3119 apply(simp_all)[5]
 
       
  3120 apply(clarify)
 
       
  3121 apply (metis ValOrd.intros(2) list.distinct(1) mkeps_flat v4)
 
       
  3122 apply(clarify)
 
       
  3123 by (metis ValOrd.intros(1))
 
       
  3124 
       
  3125 lemma LeftRightSeq:
 
       
  3126   assumes "(Left (Seq v1 v2)) \<succ>(der c (SEQ r1 r2)) (Right v3)"
 
       
  3127   and "nullable r1" "\<turnstile> v1 : der c r1"
 
       
  3128   shows "(injval (SEQ r1 r2) c (Seq v1 v2)) \<succ>(SEQ r1 r2) (injval (SEQ r1 r2) c (Right v2))"
 
       
  3129 using assms
 
       
  3130 apply(simp)
 
       
  3131 apply(erule ValOrd.cases)
 
       
  3132 apply(simp_all)[8]
 
       
  3133 apply(clarify)
 
       
  3134 apply(simp)
 
       
  3135 apply(rule ValOrd.intros(2))
 
       
  3136 prefer 2
 
       
  3137 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  3138 by (metis h)
 
       
  3139 
       
  3140 lemma rr1: 
       
  3141   assumes "\<turnstile> v : r" "\<not>nullable r" 
       
  3142   shows "flat v \<noteq> []"
 
       
  3143 using assms
 
       
  3144 by (metis Prf_flat_L nullable_correctness)
 
       
  3145 
       
  3146 (* HERE *)
 
       
  3147 
       
  3148 lemma Prf_inj_test:
 
       
  3149   assumes "v1 \<succ>(der c r) v2" 
       
  3150           "v1 \<in> Values (der c r) s"
 
       
  3151           "v2 \<in> Values (der c r) s"
 
       
  3152           "injval r c v1 \<in> Values r (c#s)"
 
       
  3153           "injval r c v2 \<in> Values r (c#s)"
 
       
  3154   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
       
  3155 using assms
 
       
  3156 apply(induct c r arbitrary: v1 v2 s rule: der.induct)
 
       
  3157 (* NULL case *)
 
       
  3158 apply(simp add: Values_recs)
 
       
  3159 (* EMPTY case *)
 
       
  3160 apply(simp add: Values_recs)
 
       
  3161 (* CHAR case *)
 
       
  3162 apply(case_tac "c = c'")
 
       
  3163 apply(simp)
 
       
  3164 apply(simp add: Values_recs)
 
       
  3165 apply (metis ValOrd2.intros(8))
 
       
  3166 apply(simp add: Values_recs)
 
       
  3167 (* ALT case *)
 
       
  3168 apply(simp)
 
       
  3169 apply(simp add: Values_recs)
 
       
  3170 apply(auto)[1]
 
       
  3171 apply(erule ValOrd.cases)
 
       
  3172 apply(simp_all)[8]
 
       
  3173 apply (metis ValOrd2.intros(6))
 
       
  3174 apply(erule ValOrd.cases)
 
       
  3175 apply(simp_all)[8]
 
       
  3176 apply(rule ValOrd2.intros)
 
       
  3177 apply(subst v4)
 
       
  3178 apply(simp add: Values_def)
 
       
  3179 apply(subst v4)
 
       
  3180 apply(simp add: Values_def)
 
       
  3181 apply(simp)
 
       
  3182 apply(erule ValOrd.cases)
 
       
  3183 apply(simp_all)[8]
 
       
  3184 apply(rule ValOrd2.intros)
 
       
  3185 apply(subst v4)
 
       
  3186 apply(simp add: Values_def)
 
       
  3187 apply(subst v4)
 
       
  3188 apply(simp add: Values_def)
 
       
  3189 apply(simp)
 
       
  3190 apply(erule ValOrd.cases)
 
       
  3191 apply(simp_all)[8]
 
       
  3192 apply (metis ValOrd2.intros(5))
 
       
  3193 (* SEQ case*)
 
       
  3194 apply(simp)
 
       
  3195 apply(case_tac "nullable r1")
 
       
  3196 apply(simp)
 
       
  3197 defer
 
       
  3198 apply(simp)
 
       
  3199 apply(simp add: Values_recs)
 
       
  3200 apply(auto)[1]
 
       
  3201 apply(erule ValOrd.cases)
 
       
  3202 apply(simp_all)[8]
 
       
  3203 apply(clarify)
 
       
  3204 apply(rule ValOrd2.intros)
 
       
  3205 apply(simp)
 
       
  3206 apply (metis Ord1)
 
       
  3207 apply(clarify)
 
       
  3208 apply(rule ValOrd2.intros)
 
       
  3209 apply(subgoal_tac "rest v1 (flat v1 @ flat v2) = flat v2")
 
       
  3210 apply(simp)
 
       
  3211 apply(subgoal_tac "rest (injval r1 c v1) (c # flat v1 @ flat v2) = flat v2")
 
       
  3212 apply(simp)
 
       
  3213 oops
 
       
  3214 
       
  3215 lemma Prf_inj_test:
 
       
  3216   assumes "v1 \<succ>(der c r) v2" 
       
  3217           "v1 \<in> Values (der c r) s"
 
       
  3218           "v2 \<in> Values (der c r) s"
 
       
  3219           "injval r c v1 \<in> Values r (c#s)"
 
       
  3220           "injval r c v2 \<in> Values r (c#s)"
 
       
  3221   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
       
  3222 using assms
 
       
  3223 apply(induct c r arbitrary: v1 v2 s rule: der.induct)
 
       
  3224 (* NULL case *)
 
       
  3225 apply(simp add: Values_recs)
 
       
  3226 (* EMPTY case *)
 
       
  3227 apply(simp add: Values_recs)
 
       
  3228 (* CHAR case *)
 
       
  3229 apply(case_tac "c = c'")
 
       
  3230 apply(simp)
 
       
  3231 apply(simp add: Values_recs)
 
       
  3232 apply (metis ValOrd2.intros(8))
 
       
  3233 apply(simp add: Values_recs)
 
       
  3234 (* ALT case *)
 
       
  3235 apply(simp)
 
       
  3236 apply(simp add: Values_recs)
 
       
  3237 apply(auto)[1]
 
       
  3238 apply(erule ValOrd.cases)
 
       
  3239 apply(simp_all)[8]
 
       
  3240 apply (metis ValOrd2.intros(6))
 
       
  3241 apply(erule ValOrd.cases)
 
       
  3242 apply(simp_all)[8]
 
       
  3243 apply(rule ValOrd2.intros)
 
       
  3244 apply(subst v4)
 
       
  3245 apply(simp add: Values_def)
 
       
  3246 apply(subst v4)
 
       
  3247 apply(simp add: Values_def)
 
       
  3248 apply(simp)
 
       
  3249 apply(erule ValOrd.cases)
 
       
  3250 apply(simp_all)[8]
 
       
  3251 apply(rule ValOrd2.intros)
 
       
  3252 apply(subst v4)
 
       
  3253 apply(simp add: Values_def)
 
       
  3254 apply(subst v4)
 
       
  3255 apply(simp add: Values_def)
 
       
  3256 apply(simp)
 
       
  3257 apply(erule ValOrd.cases)
 
       
  3258 apply(simp_all)[8]
 
       
  3259 apply (metis ValOrd2.intros(5))
 
       
  3260 (* SEQ case*)
 
       
  3261 apply(simp)
 
       
  3262 apply(case_tac "nullable r1")
 
       
  3263 apply(simp)
 
       
  3264 defer
 
       
  3265 apply(simp)
 
       
  3266 apply(simp add: Values_recs)
 
       
  3267 apply(auto)[1]
 
       
  3268 apply(erule ValOrd.cases)
 
       
  3269 apply(simp_all)[8]
 
       
  3270 apply(clarify)
 
       
  3271 apply(rule ValOrd2.intros)
 
       
  3272 apply(simp)
 
       
  3273 apply (metis Ord1)
 
       
  3274 apply(clarify)
 
       
  3275 apply(rule ValOrd2.intros)
 
       
  3276 apply metis
 
       
  3277 using injval_inj
 
       
  3278 apply(simp add: Values_def inj_on_def)
 
       
  3279 apply metis
 
       
  3280 apply(simp add: Values_recs)
 
       
  3281 apply(auto)[1]
 
       
  3282 apply(erule ValOrd.cases)
 
       
  3283 apply(simp_all)[8]
 
       
  3284 apply(clarify)
 
       
  3285 apply(erule ValOrd.cases)
 
       
  3286 apply(simp_all)[8]
 
       
  3287 apply(clarify)
 
       
  3288 apply (metis Ord1 ValOrd2.intros(1))
 
       
  3289 apply(clarify)
 
       
  3290 apply(rule ValOrd2.intros(2))
 
       
  3291 apply metis
 
       
  3292 using injval_inj
 
       
  3293 apply(simp add: Values_def inj_on_def)
 
       
  3294 apply metis
 
       
  3295 apply(erule ValOrd.cases)
 
       
  3296 apply(simp_all)[8]
 
       
  3297 apply(rule ValOrd2.intros(2))
 
       
  3298 thm h
 
       
  3299 apply(rule Ord1)
 
       
  3300 apply(rule h)
 
       
  3301 apply(simp)
 
       
  3302 apply(simp add: Values_def)
 
       
  3303 apply(simp add: Values_def)
 
       
  3304 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  3305 apply(erule ValOrd.cases)
 
       
  3306 apply(simp_all)[8]
 
       
  3307 apply(clarify)
 
       
  3308 apply(simp add: Values_def)
 
       
  3309 defer
 
       
  3310 apply(erule ValOrd.cases)
 
       
  3311 apply(simp_all)[8]
 
       
  3312 apply(clarify)
 
       
  3313 apply(rule ValOrd2.intros(1))
 
       
  3314 apply(rotate_tac 1)
 
       
  3315 apply(drule_tac x="v2" in meta_spec)
 
       
  3316 apply(rotate_tac 8)
 
       
  3317 apply(drule_tac x="v2'" in meta_spec)
 
       
  3318 apply(rotate_tac 8)
 
       
  3319 oops
 
       
  3320 
       
  3321 lemma POSIX_der:
 
       
  3322   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
       
  3323   shows "POSIX (injval r c v) r"
 
       
  3324 using assms
 
       
  3325 unfolding POSIX_def
 
       
  3326 apply(auto)
 
       
  3327 thm v3
 
       
  3328 apply (erule v3)
 
       
  3329 thm v4
 
       
  3330 apply(subst (asm) v4)
 
       
  3331 apply(assumption)
 
       
  3332 apply(drule_tac x="projval r c v'" in spec)
 
       
  3333 apply(drule mp)
 
       
  3334 apply(rule conjI)
 
       
  3335 thm v3_proj
 
       
  3336 apply(rule v3_proj)
 
       
  3337 apply(simp)
 
       
  3338 apply(rule_tac x="flat v" in exI)
 
       
  3339 apply(simp)
 
       
  3340 thm t
 
       
  3341 apply(rule_tac c="c" in  t)
 
       
  3342 apply(simp)
 
       
  3343 thm v4_proj
 
       
  3344 apply(subst v4_proj)
 
       
  3345 apply(simp)
 
       
  3346 apply(rule_tac x="flat v" in exI)
 
       
  3347 apply(simp)
 
       
  3348 apply(simp)
 
       
  3349 oops
 
       
  3350 
       
  3351 lemma POSIX_der:
 
       
  3352   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
       
  3353   shows "POSIX (injval r c v) r"
 
       
  3354 using assms
 
       
  3355 apply(induct c r arbitrary: v rule: der.induct)
 
       
  3356 (* null case*)
 
       
  3357 apply(simp add: POSIX_def)
 
       
  3358 apply(auto)[1]
 
       
  3359 apply(erule Prf.cases)
 
       
  3360 apply(simp_all)[5]
 
       
  3361 apply(erule Prf.cases)
 
       
  3362 apply(simp_all)[5]
 
       
  3363 (* empty case *)
 
       
  3364 apply(simp add: POSIX_def)
 
       
  3365 apply(auto)[1]
 
       
  3366 apply(erule Prf.cases)
 
       
  3367 apply(simp_all)[5]
 
       
  3368 apply(erule Prf.cases)
 
       
  3369 apply(simp_all)[5]
 
       
  3370 (* char case *)
 
       
  3371 apply(simp add: POSIX_def)
 
       
  3372 apply(case_tac "c = c'")
 
       
  3373 apply(auto)[1]
 
       
  3374 apply(erule Prf.cases)
 
       
  3375 apply(simp_all)[5]
 
       
  3376 apply (metis Prf.intros(5))
 
       
  3377 apply(erule Prf.cases)
 
       
  3378 apply(simp_all)[5]
 
       
  3379 apply(erule Prf.cases)
 
       
  3380 apply(simp_all)[5]
 
       
  3381 apply (metis ValOrd.intros(8))
 
       
  3382 apply(auto)[1]
 
       
  3383 apply(erule Prf.cases)
 
       
  3384 apply(simp_all)[5]
 
       
  3385 apply(erule Prf.cases)
 
       
  3386 apply(simp_all)[5]
 
       
  3387 (* alt case *)
 
       
  3388 apply(erule Prf.cases)
 
       
  3389 apply(simp_all)[5]
 
       
  3390 apply(clarify)
 
       
  3391 apply(simp (no_asm) add: POSIX_def)
 
       
  3392 apply(auto)[1]
 
       
  3393 apply (metis Prf.intros(2) v3)
 
       
  3394 apply(rotate_tac 4)
 
       
  3395 apply(erule Prf.cases)
 
       
  3396 apply(simp_all)[5]
 
       
  3397 apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
 
       
  3398 apply (metis ValOrd.intros(3) order_refl)
 
       
  3399 apply(simp (no_asm) add: POSIX_def)
 
       
  3400 apply(auto)[1]
 
       
  3401 apply (metis Prf.intros(3) v3)
 
       
  3402 apply(rotate_tac 4)
 
       
  3403 apply(erule Prf.cases)
 
       
  3404 apply(simp_all)[5]
 
       
  3405 defer
 
       
  3406 apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
 
       
  3407 prefer 2
 
       
  3408 apply(subst (asm) (5) POSIX_def)
 
       
  3409 apply(auto)[1]
 
       
  3410 apply(rotate_tac 5)
 
       
  3411 apply(erule Prf.cases)
 
       
  3412 apply(simp_all)[5]
 
       
  3413 apply(rule ValOrd.intros)
 
       
  3414 apply(subst (asm) v4)
 
       
  3415 apply(simp)
 
       
  3416 apply(drule_tac x="Left (projval r1a c v1)" in spec)
 
       
  3417 apply(clarify)
 
       
  3418 apply(drule mp)
 
       
  3419 apply(rule conjI)
 
       
  3420 apply (metis Prf.intros(2) v3_proj)
 
       
  3421 apply(simp)
 
       
  3422 apply (metis v4_proj2)
 
       
  3423 apply(erule ValOrd.cases)
 
       
  3424 apply(simp_all)[8]
 
       
  3425 apply (metis less_not_refl v4_proj2)
 
       
  3426 (* seq case *)
 
       
  3427 apply(case_tac "nullable r1")
 
       
  3428 defer
 
       
  3429 apply(simp add: POSIX_def)
 
       
  3430 apply(auto)[1]
 
       
  3431 apply(erule Prf.cases)
 
       
  3432 apply(simp_all)[5]
 
       
  3433 apply (metis Prf.intros(1) v3)
 
       
  3434 apply(erule Prf.cases)
 
       
  3435 apply(simp_all)[5]
 
       
  3436 apply(erule Prf.cases)
 
       
  3437 apply(simp_all)[5]
 
       
  3438 apply(clarify)
 
       
  3439 apply(subst (asm) (3) v4)
 
       
  3440 apply(simp)
 
       
  3441 apply(simp)
 
       
  3442 apply(subgoal_tac "flat v1a \<noteq> []")
 
       
  3443 prefer 2
 
       
  3444 apply (metis Prf_flat_L nullable_correctness)
 
       
  3445 apply(subgoal_tac "\<exists>s. flat v1a = c # s")
 
       
  3446 prefer 2
 
       
  3447 apply (metis append_eq_Cons_conv)
 
       
  3448 apply(auto)[1]
 
       
  3449 oops
 
       
  3450 
       
  3451 
       
  3452 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
 
       
  3453 apply(induct r arbitrary: v)
 
       
  3454 apply(erule Prf.cases)
 
       
  3455 apply(simp_all)[5]
 
       
  3456 apply(erule Prf.cases)
 
       
  3457 apply(simp_all)[5]
 
       
  3458 apply(rule_tac x="Void" in exI)
 
       
  3459 apply(simp add: POSIX_def)
 
       
  3460 apply(auto)[1]
 
       
  3461 apply (metis Prf.intros(4))
 
       
  3462 apply(erule Prf.cases)
 
       
  3463 apply(simp_all)[5]
 
       
  3464 apply (metis ValOrd.intros(7))
 
       
  3465 apply(erule Prf.cases)
 
       
  3466 apply(simp_all)[5]
 
       
  3467 apply(rule_tac x="Char c" in exI)
 
       
  3468 apply(simp add: POSIX_def)
 
       
  3469 apply(auto)[1]
 
       
  3470 apply (metis Prf.intros(5))
 
       
  3471 apply(erule Prf.cases)
 
       
  3472 apply(simp_all)[5]
 
       
  3473 apply (metis ValOrd.intros(8))
 
       
  3474 apply(erule Prf.cases)
 
       
  3475 apply(simp_all)[5]
 
       
  3476 apply(auto)[1]
 
       
  3477 apply(drule_tac x="v1" in meta_spec)
 
       
  3478 apply(drule_tac x="v2" in meta_spec)
 
       
  3479 apply(auto)[1]
 
       
  3480 defer
 
       
  3481 apply(erule Prf.cases)
 
       
  3482 apply(simp_all)[5]
 
       
  3483 apply(auto)[1]
 
       
  3484 apply (metis POSIX_ALT_I1)
 
       
  3485 apply (metis POSIX_ALT_I1 POSIX_ALT_I2)
 
       
  3486 apply(case_tac "nullable r1a")
 
       
  3487 apply(rule_tac x="Seq (mkeps r1a) va" in exI)
 
       
  3488 apply(auto simp add: POSIX_def)[1]
 
       
  3489 apply (metis Prf.intros(1) mkeps_nullable)
 
       
  3490 apply(simp add: mkeps_flat)
 
       
  3491 apply(rotate_tac 7)
 
       
  3492 apply(erule Prf.cases)
 
       
  3493 apply(simp_all)[5]
 
       
  3494 apply(case_tac "mkeps r1 = v1a")
 
       
  3495 apply(simp)
 
       
  3496 apply (rule ValOrd.intros(1))
 
       
  3497 apply (metis append_Nil mkeps_flat)
 
       
  3498 apply (rule ValOrd.intros(2))
 
       
  3499 apply(drule mkeps_POSIX)
 
       
  3500 apply(simp add: POSIX_def)
 
       
  3501 oops
 
       
  3502 
       
  3503 lemma POSIX_ex2: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r \<and> \<turnstile> v : r"
 
       
  3504 apply(induct r arbitrary: v)
 
       
  3505 apply(erule Prf.cases)
 
       
  3506 apply(simp_all)[5]
 
       
  3507 apply(erule Prf.cases)
 
       
  3508 apply(simp_all)[5]
 
       
  3509 apply(rule_tac x="Void" in exI)
 
       
  3510 apply(simp add: POSIX_def)
 
       
  3511 apply(auto)[1]
 
       
  3512 oops
 
       
  3513 
       
  3514 lemma POSIX_ALT_cases:
 
       
  3515   assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
 
       
  3516   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
 
       
  3517 using assms
 
       
  3518 apply(erule_tac Prf.cases)
 
       
  3519 apply(simp_all)
 
       
  3520 unfolding POSIX_def
 
       
  3521 apply(auto)
 
       
  3522 apply (metis POSIX_ALT2 POSIX_def assms(2))
 
       
  3523 by (metis POSIX_ALT1b assms(2))
 
       
  3524 
       
  3525 lemma POSIX_ALT_cases2:
 
       
  3526   assumes "POSIX v (ALT r1 r2)" "\<turnstile> v : (ALT r1 r2)" 
       
  3527   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
 
       
  3528 using assms POSIX_ALT_cases by auto
 
       
  3529 
       
  3530 lemma Prf_flat_empty:
 
       
  3531   assumes "\<turnstile> v : r" "flat v = []"
 
       
  3532   shows "nullable r"
 
       
  3533 using assms
 
       
  3534 apply(induct)
 
       
  3535 apply(auto)
 
       
  3536 done
 
       
  3537 
       
  3538 lemma POSIX_proj:
 
       
  3539   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
 
       
  3540   shows "POSIX (projval r c v) (der c r)"
 
       
  3541 using assms
 
       
  3542 apply(induct r c v arbitrary: rule: projval.induct)
 
       
  3543 defer
 
       
  3544 defer
 
       
  3545 defer
 
       
  3546 defer
 
       
  3547 apply(erule Prf.cases)
 
       
  3548 apply(simp_all)[5]
 
       
  3549 apply(erule Prf.cases)
 
       
  3550 apply(simp_all)[5]
 
       
  3551 apply(erule Prf.cases)
 
       
  3552 apply(simp_all)[5]
 
       
  3553 apply(erule Prf.cases)
 
       
  3554 apply(simp_all)[5]
 
       
  3555 apply(erule Prf.cases)
 
       
  3556 apply(simp_all)[5]
 
       
  3557 apply(erule Prf.cases)
 
       
  3558 apply(simp_all)[5]
 
       
  3559 apply(erule Prf.cases)
 
       
  3560 apply(simp_all)[5]
 
       
  3561 apply(erule Prf.cases)
 
       
  3562 apply(simp_all)[5]
 
       
  3563 apply(erule Prf.cases)
 
       
  3564 apply(simp_all)[5]
 
       
  3565 apply(erule Prf.cases)
 
       
  3566 apply(simp_all)[5]
 
       
  3567 apply(simp add: POSIX_def)
 
       
  3568 apply(auto)[1]
 
       
  3569 apply(erule Prf.cases)
 
       
  3570 apply(simp_all)[5]
 
       
  3571 oops
 
       
  3572 
       
  3573 lemma POSIX_proj:
 
       
  3574   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
 
       
  3575   shows "POSIX (projval r c v) (der c r)"
 
       
  3576 using assms
 
       
  3577 apply(induct r arbitrary: c v rule: rexp.induct)
 
       
  3578 apply(erule Prf.cases)
 
       
  3579 apply(simp_all)[5]
 
       
  3580 apply(erule Prf.cases)
 
       
  3581 apply(simp_all)[5]
 
       
  3582 apply(erule Prf.cases)
 
       
  3583 apply(simp_all)[5]
 
       
  3584 apply(simp add: POSIX_def)
 
       
  3585 apply(auto)[1]
 
       
  3586 apply(erule Prf.cases)
 
       
  3587 apply(simp_all)[5]
 
       
  3588 oops
 
       
  3589 
       
  3590 lemma POSIX_proj:
 
       
  3591   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
 
       
  3592   shows "POSIX (projval r c v) (der c r)"
 
       
  3593 using assms
 
       
  3594 apply(induct r c v arbitrary: rule: projval.induct)
 
       
  3595 defer
 
       
  3596 defer
 
       
  3597 defer
 
       
  3598 defer
 
       
  3599 apply(erule Prf.cases)
 
       
  3600 apply(simp_all)[5]
 
       
  3601 apply(erule Prf.cases)
 
       
  3602 apply(simp_all)[5]
 
       
  3603 apply(erule Prf.cases)
 
       
  3604 apply(simp_all)[5]
 
       
  3605 apply(erule Prf.cases)
 
       
  3606 apply(simp_all)[5]
 
       
  3607 apply(erule Prf.cases)
 
       
  3608 apply(simp_all)[5]
 
       
  3609 apply(erule Prf.cases)
 
       
  3610 apply(simp_all)[5]
 
       
  3611 apply(erule Prf.cases)
 
       
  3612 apply(simp_all)[5]
 
       
  3613 apply(erule Prf.cases)
 
       
  3614 apply(simp_all)[5]
 
       
  3615 apply(erule Prf.cases)
 
       
  3616 apply(simp_all)[5]
 
       
  3617 apply(erule Prf.cases)
 
       
  3618 apply(simp_all)[5]
 
       
  3619 apply(simp add: POSIX_def)
 
       
  3620 apply(auto)[1]
 
       
  3621 apply(erule Prf.cases)
 
       
  3622 apply(simp_all)[5]
 
       
  3623 oops
 
       
  3624 
       
  3625 lemma Prf_inj:
 
       
  3626   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
 
       
  3627   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
       
  3628 using assms
 
       
  3629 apply(induct arbitrary: v1 v2 rule: der.induct)
 
       
  3630 (* NULL case *)
 
       
  3631 apply(simp)
 
       
  3632 apply(erule ValOrd.cases)
 
       
  3633 apply(simp_all)[8]
 
       
  3634 (* EMPTY case *)
 
       
  3635 apply(erule ValOrd.cases)
 
       
  3636 apply(simp_all)[8]
 
       
  3637 (* CHAR case *)
 
       
  3638 apply(case_tac "c = c'")
 
       
  3639 apply(simp)
 
       
  3640 apply(erule ValOrd.cases)
 
       
  3641 apply(simp_all)[8]
 
       
  3642 apply(rule ValOrd.intros)
 
       
  3643 apply(simp)
 
       
  3644 apply(erule ValOrd.cases)
 
       
  3645 apply(simp_all)[8]
 
       
  3646 (* ALT case *)
 
       
  3647 apply(simp)
 
       
  3648 apply(erule ValOrd.cases)
 
       
  3649 apply(simp_all)[8]
 
       
  3650 apply(rule ValOrd.intros)
 
       
  3651 apply(subst v4)
 
       
  3652 apply(clarify)
 
       
  3653 apply(rotate_tac 3)
 
       
  3654 apply(erule Prf.cases)
 
       
  3655 apply(simp_all)[5]
 
       
  3656 apply(subst v4)
 
       
  3657 apply(clarify)
 
       
  3658 apply(rotate_tac 2)
 
       
  3659 apply(erule Prf.cases)
 
       
  3660 apply(simp_all)[5]
 
       
  3661 apply(simp)
 
       
  3662 apply(rule ValOrd.intros)
 
       
  3663 apply(clarify)
 
       
  3664 apply(rotate_tac 3)
 
       
  3665 apply(erule Prf.cases)
 
       
  3666 apply(simp_all)[5]
 
       
  3667 apply(clarify)
 
       
  3668 apply(erule Prf.cases)
 
       
  3669 apply(simp_all)[5]
 
       
  3670 apply(rule ValOrd.intros)
 
       
  3671 apply(clarify)
 
       
  3672 apply(erule Prf.cases)
 
       
  3673 apply(simp_all)[5]
 
       
  3674 apply(erule Prf.cases)
 
       
  3675 apply(simp_all)[5]
 
       
  3676 (* SEQ case*)
 
       
  3677 apply(simp)
 
       
  3678 apply(case_tac "nullable r1")
 
       
  3679 defer
 
       
  3680 apply(simp)
 
       
  3681 apply(erule ValOrd.cases)
 
       
  3682 apply(simp_all)[8]
 
       
  3683 apply(clarify)
 
       
  3684 apply(erule Prf.cases)
 
       
  3685 apply(simp_all)[5]
 
       
  3686 apply(erule Prf.cases)
 
       
  3687 apply(simp_all)[5]
 
       
  3688 apply(clarify)
 
       
  3689 apply(rule ValOrd.intros)
 
       
  3690 apply(simp)
 
       
  3691 oops
 
       
  3692 
       
  3693 
       
  3694 text {*
 
       
  3695   Injection followed by projection is the identity.
 
       
  3696 *}
 
       
  3697 
       
  3698 lemma proj_inj_id:
 
       
  3699   assumes "\<turnstile> v : der c r" 
       
  3700   shows "projval r c (injval r c v) = v"
 
       
  3701 using assms
 
       
  3702 apply(induct r arbitrary: c v rule: rexp.induct)
 
       
  3703 apply(simp)
 
       
  3704 apply(erule Prf.cases)
 
       
  3705 apply(simp_all)[5]
 
       
  3706 apply(simp)
 
       
  3707 apply(erule Prf.cases)
 
       
  3708 apply(simp_all)[5]
 
       
  3709 apply(simp)
 
       
  3710 apply(case_tac "c = char")
 
       
  3711 apply(simp)
 
       
  3712 apply(erule Prf.cases)
 
       
  3713 apply(simp_all)[5]
 
       
  3714 apply(simp)
 
       
  3715 apply(erule Prf.cases)
 
       
  3716 apply(simp_all)[5]
 
       
  3717 defer
 
       
  3718 apply(simp)
 
       
  3719 apply(erule Prf.cases)
 
       
  3720 apply(simp_all)[5]
 
       
  3721 apply(simp)
 
       
  3722 apply(case_tac "nullable rexp1")
 
       
  3723 apply(simp)
 
       
  3724 apply(erule Prf.cases)
 
       
  3725 apply(simp_all)[5]
 
       
  3726 apply(auto)[1]
 
       
  3727 apply(erule Prf.cases)
 
       
  3728 apply(simp_all)[5]
 
       
  3729 apply(auto)[1]
 
       
  3730 apply (metis list.distinct(1) v4)
 
       
  3731 apply(auto)[1]
 
       
  3732 apply (metis mkeps_flat)
 
       
  3733 apply(auto)
 
       
  3734 apply(erule Prf.cases)
 
       
  3735 apply(simp_all)[5]
 
       
  3736 apply(auto)[1]
 
       
  3737 apply(simp add: v4)
 
       
  3738 done
 
       
  3739 
       
  3740 text {* 
       
  3741 
       
  3742   HERE: Crucial lemma that does not go through in the sequence case. 
       
  3743 
       
  3744 *}
 
       
  3745 lemma v5:
 
       
  3746   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
 
       
  3747   shows "POSIX (injval r c v) r"
 
       
  3748 using assms
 
       
  3749 apply(induct arbitrary: v rule: der.induct)
 
       
  3750 (* NULL case *)
 
       
  3751 apply(simp)
 
       
  3752 apply(erule Prf.cases)
 
       
  3753 apply(simp_all)[5]
 
       
  3754 (* EMPTY case *)
 
       
  3755 apply(simp)
 
       
  3756 apply(erule Prf.cases)
 
       
  3757 apply(simp_all)[5]
 
       
  3758 (* CHAR case *)
 
       
  3759 apply(simp)
 
       
  3760 apply(case_tac "c = c'")
 
       
  3761 apply(auto simp add: POSIX_def)[1]
 
       
  3762 apply(erule Prf.cases)
 
       
  3763 apply(simp_all)[5]
 
       
  3764 oops
 
       
  3765 *)
 
       
  3766 
  1438 
  3767 
  1439 
  3768 end
 
  1440 end
lexing