840 done |
840 done |
841 |
841 |
842 |
842 |
843 section {* Sulzmann's Ordering of values *} |
843 section {* Sulzmann's Ordering of values *} |
844 |
844 |
845 thm PMatch.intros |
|
846 |
|
847 inductive ValOrds :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100] 100) |
|
848 where |
|
849 "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
|
850 | "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = s2; (flat v1' @ flat v2') \<sqsubseteq> (s1 @ s2)\<rbrakk> |
|
851 \<Longrightarrow> s1 @ s2 \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
852 | "\<lbrakk>(flat v2) \<sqsubseteq> (flat v1); flat v1 = s\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
|
853 | "\<lbrakk>(flat v1) \<sqsubset> (flat v2); flat v2 = s\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
|
854 | "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
|
855 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
|
856 | "[] \<turnstile> Void \<succ>EMPTY Void" |
|
857 | "[c] \<turnstile> (Char c) \<succ>(CHAR c) (Char c)" |
|
858 |
|
859 lemma valord_prefix: |
|
860 assumes "s \<turnstile> v1 \<succ>r v2" |
|
861 shows "flat v1 \<sqsubseteq> s" and "flat v2 \<sqsubseteq> s" |
|
862 using assms |
|
863 apply(induct) |
|
864 apply(auto) |
|
865 apply(simp add: prefix_def rest_def) |
|
866 apply(auto)[1] |
|
867 apply(simp add: prefix_def rest_def) |
|
868 apply(auto)[1] |
|
869 apply(auto simp add: prefix_def rest_def) |
|
870 done |
|
871 |
|
872 lemma valord_prefix2: |
|
873 assumes "s \<turnstile> v1 \<succ>r v2" |
|
874 shows "flat v2 \<sqsubseteq> flat v1" |
|
875 using assms |
|
876 apply(induct) |
|
877 apply(auto) |
|
878 apply(simp add: prefix_def rest_def) |
|
879 apply(simp add: prefix_def rest_def) |
|
880 apply(auto)[1] |
|
881 defer |
|
882 apply(simp add: prefix_def rest_def) |
|
883 apply(auto)[1] |
|
884 apply (metis append_eq_append_conv_if append_eq_conv_conj) |
|
885 apply(simp add: prefix_def rest_def) |
|
886 apply(auto)[1] |
|
887 apply (metis append_eq_append_conv_if append_take_drop_id le_eq_less_or_eq) |
|
888 apply(simp add: prefix_def rest_def) |
|
889 apply(simp add: prefix_def rest_def) |
|
890 |
|
891 |
845 |
892 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
846 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
893 where |
847 where |
894 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
848 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
895 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
849 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
1071 apply metis |
1025 apply metis |
1072 apply(rule ValOrd.intros) |
1026 apply(rule ValOrd.intros) |
1073 apply metis |
1027 apply metis |
1074 done |
1028 done |
1075 |
1029 |
|
1030 section (* tryout with all-mkeps *) |
|
1031 |
|
1032 fun |
|
1033 alleps :: "rexp \<Rightarrow> val set" |
|
1034 where |
|
1035 "alleps(NULL) = {}" |
|
1036 | "alleps(EMPTY) = {Void}" |
|
1037 | "alleps(CHAR c) = {}" |
|
1038 | "alleps(SEQ r1 r2) = {Seq v1 v2 | v1 v2. v1 \<in> alleps r1 \<and> v2 \<in> alleps r2}" |
|
1039 | "alleps(ALT r1 r2) = {Left v1 | v1. v1 \<in> alleps r1} \<union> {Right v2 | v2. v2 \<in> alleps r2}" |
|
1040 |
|
1041 fun |
|
1042 allvals :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
1043 where |
|
1044 "allvals r [] = alleps r" |
|
1045 | "allvals r (c#s) = {injval r c v | v. v \<in> allvals (der c r) s}" |
|
1046 |
|
1047 |
|
1048 lemma q1: |
|
1049 assumes "v \<in> alleps r" |
|
1050 shows "\<turnstile> v : r \<and> flat v = []" |
|
1051 using assms |
|
1052 apply(induct r arbitrary: v) |
|
1053 apply(auto intro: Prf.intros) |
|
1054 done |
|
1055 |
|
1056 lemma q11: |
|
1057 assumes "nullable r" "\<turnstile> v : r" "flat v = []" |
|
1058 shows "v \<in> alleps r" |
|
1059 using assms |
|
1060 apply(induct r arbitrary: v) |
|
1061 apply(auto) |
|
1062 apply(erule Prf.cases) |
|
1063 apply(simp_all) |
|
1064 apply(erule Prf.cases) |
|
1065 apply(simp_all) |
|
1066 apply(erule Prf.cases) |
|
1067 apply(simp_all) |
|
1068 apply(auto) |
|
1069 apply(subgoal_tac "nullable r2a") |
|
1070 apply(auto) |
|
1071 using not_nullable_flat apply auto[1] |
|
1072 apply(erule Prf.cases) |
|
1073 apply(simp_all) |
|
1074 apply(auto) |
|
1075 apply(subgoal_tac "nullable r1a") |
|
1076 apply(auto) |
|
1077 using not_nullable_flat apply auto[1] |
|
1078 done |
|
1079 |
|
1080 lemma q33: |
|
1081 assumes "nullable r" |
|
1082 shows "alleps r = {v. \<turnstile> v : r \<and> flat v = []}" |
|
1083 using assms |
|
1084 apply(auto) |
|
1085 apply (simp_all add: q1) |
|
1086 by (simp add: q11) |
|
1087 |
|
1088 lemma q22: |
|
1089 assumes "v \<in> allvals r s" |
|
1090 shows "\<turnstile> v : r \<and> s \<in> L (r) \<and> flat v = s" |
|
1091 using assms |
|
1092 apply(induct s arbitrary: v r) |
|
1093 apply(auto) |
|
1094 apply(simp_all add: q1) |
|
1095 using Prf_flat_L q1 apply fastforce |
|
1096 apply (simp add: v3) |
|
1097 apply (metis Prf_flat_L v3 v4) |
|
1098 by (simp add: v4) |
|
1099 |
|
1100 |
|
1101 lemma qa_oops: |
|
1102 assumes "\<turnstile> v : r" "\<exists>s. flat v = a # s \<and> a # s \<in> L r" "\<turnstile> projval r a v : der a r" |
|
1103 shows "injval r a (projval r a v) = v" |
|
1104 using assms |
|
1105 apply(induct v r arbitrary: ) |
|
1106 defer |
|
1107 defer |
|
1108 apply(simp) |
|
1109 apply(erule Prf.cases) |
|
1110 apply(simp_all)[4] |
|
1111 apply(auto simp only:) |
|
1112 apply(simp) |
|
1113 apply(erule Prf.cases) |
|
1114 apply(simp_all)[5] |
|
1115 |
|
1116 done |
|
1117 apply(erule Prf.cases) |
|
1118 apply(simp_all) |
|
1119 apply(erule Prf.cases) |
|
1120 apply(simp_all) |
|
1121 apply(erule Prf.cases) |
|
1122 apply(simp_all) |
|
1123 apply(erule Prf.cases) |
|
1124 apply(simp_all) |
|
1125 apply(erule Prf.cases) |
|
1126 apply(simp_all) |
|
1127 apply(auto) |
|
1128 using Prf_flat_L apply fastforce |
|
1129 apply(erule Prf.cases) |
|
1130 apply(simp_all) |
|
1131 apply(erule Prf.cases) |
|
1132 apply(simp_all) |
|
1133 using Prf_flat_L apply force |
|
1134 apply(erule Prf.cases) |
|
1135 apply(simp_all) |
|
1136 apply(erule Prf.cases) |
|
1137 apply(simp_all) |
|
1138 apply(erule Prf.cases) |
|
1139 apply(simp_all) |
|
1140 apply(auto)[1] |
|
1141 apply(case_tac "nullable r1a") |
|
1142 apply(simp) |
|
1143 apply(erule Prf.cases) |
|
1144 apply(simp_all) |
|
1145 apply(auto simp add: Sequ_def)[1] |
|
1146 apply(simp add: Cons_eq_append_conv) |
|
1147 apply(auto) |
|
1148 |
|
1149 |
|
1150 using Prf_flat_L |
|
1151 apply(erule Prf.cases) |
|
1152 apply(simp_all) |
|
1153 using Prf_flat_L |
|
1154 apply(erule Prf.cases) |
|
1155 apply(simp_all) |
|
1156 apply(erule Prf.cases) |
|
1157 apply(simp_all) |
|
1158 apply(simp add: Sequ_def) |
|
1159 apply(auto)[1] |
|
1160 apply(simp add: Cons_eq_append_conv) |
|
1161 apply(auto)[1] |
|
1162 sorry |
|
1163 |
|
1164 |
|
1165 lemma q2: |
|
1166 assumes "s \<in> L(r)" |
|
1167 shows "allvals r s = {v. \<turnstile> v : r \<and> s \<in> L (r) \<and> flat v = s}" |
|
1168 using assms |
|
1169 apply(induct s arbitrary: r) |
|
1170 apply(simp) |
|
1171 apply(subst q33) |
|
1172 using nullable_correctness apply blast |
|
1173 apply(simp) |
|
1174 apply(simp) |
|
1175 apply(drule_tac x="der a r" in meta_spec) |
|
1176 apply(drule meta_mp) |
|
1177 using lex_correct1 lex_correct3 apply fastforce |
|
1178 apply(simp) |
|
1179 apply(auto) |
|
1180 using v3 apply blast |
|
1181 apply (simp add: v4) |
|
1182 apply(rule_tac x="projval r a x" in exI) |
|
1183 apply(rule conjI) |
|
1184 defer |
|
1185 apply(rule conjI) |
|
1186 apply (simp add: v3_proj) |
|
1187 apply (simp add: v4_proj2) |
|
1188 apply(subgoal_tac "projval r a x \<in> allvals (der a r) s") |
|
1189 apply(simp) |
|
1190 apply(subst qa_oops) |
|
1191 apply(simp) |
|
1192 apply(blast) |
|
1193 |
|
1194 lemma q2: |
|
1195 assumes "\<turnstile> v : r" "s \<in> L (r)" "flat v = s" |
|
1196 shows "v \<in> allvals r s" |
|
1197 using assms |
|
1198 apply(induct s arbitrary: r v) |
|
1199 apply(auto) |
|
1200 apply(subgoal_tac "nullable r") |
|
1201 apply(simp add: q11) |
|
1202 using not_nullable_flat apply fastforce |
|
1203 apply(drule sym) |
|
1204 apply(simp) |
|
1205 apply(case_tac s) |
|
1206 apply(simp) |
|
1207 |
|
1208 apply(drule_tac x="projval r a v" in meta_spec) |
|
1209 apply(drule_tac x="der a r" in meta_spec) |
|
1210 apply(drule meta_mp) |
|
1211 defer |
|
1212 apply(drule meta_mp) |
|
1213 using v3_proj apply blast |
|
1214 apply(rule_tac x="projval r a v" in exI) |
|
1215 apply(auto) |
|
1216 defer |
|
1217 apply(subst (asm) v4_proj2) |
|
1218 apply(assumption) |
|
1219 apply(assumption) |
|
1220 apply(simp) |
|
1221 apply(subst v4_proj2) |
|
1222 apply(assumption) |
|
1223 apply(assumption) |
|
1224 apply(simp) |
|
1225 apply(subst (asm) v4_proj2) |
|
1226 apply(assumption) |
|
1227 apply(assumption) |
|
1228 sorry |
|
1229 |
|
1230 |
|
1231 |
|
1232 lemma |
|
1233 "{v. \<turnstile> v : r \<and> flat v = s} = allvals r s" |
|
1234 apply(auto) |
|
1235 apply(rule q2) |
|
1236 apply(simp) |
|
1237 |
|
1238 |
|
1239 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> string \<Rightarrow> bool" |
|
1240 where |
|
1241 "POSIX2 v r s \<equiv> (\<turnstile> v : r \<and> (\<forall>v'\<in>allvals r s. v \<succ>r v'))" |
|
1242 |
|
1243 lemma k1: |
|
1244 shows "POSIX2 v r [] \<Longrightarrow> \<forall>v' \<in> alleps r. v \<succ>r v'" |
|
1245 using assms |
|
1246 apply(induct r arbitrary: v) |
|
1247 apply(simp_all) |
|
1248 apply(simp add: POSIX2_def) |
|
1249 apply(auto) |
|
1250 apply(simp add: POSIX2_def) |
|
1251 apply(simp add: POSIX2_def) |
|
1252 apply(simp add: POSIX2_def) |
|
1253 apply(simp add: POSIX2_def) |
|
1254 apply(simp add: POSIX2_def) |
|
1255 done |
|
1256 |
|
1257 lemma k2: |
|
1258 shows "POSIX2 v r s \<Longrightarrow> \<forall>v' \<in> allvals r s. v \<succ>r v'" |
|
1259 using assms |
|
1260 apply(induct s arbitrary: r v) |
|
1261 apply(simp add: k1) |
|
1262 apply(auto) |
|
1263 apply(simp only: POSIX2_def) |
|
1264 apply(simp) |
|
1265 apply(clarify) |
|
1266 apply(drule_tac x="injval r a va" in spec) |
|
1267 apply(drule mp) |
|
1268 defer |
|
1269 apply(auto) |
|
1270 done |
|
1271 done |
|
1272 |
|
1273 lemma "s \<in> L(r) \<Longrightarrow> \<exists>v. POSIX2 v r s" |
|
1274 apply(induct r arbitrary: s) |
|
1275 apply(auto) |
|
1276 apply(rule_tac x="Void" in exI) |
|
1277 apply(simp add: POSIX2_def) |
|
1278 apply (simp add: Prf.intros(4) ValOrd.intros(7)) |
|
1279 apply(rule_tac x="Char x" in exI) |
|
1280 apply(simp add: POSIX2_def) |
|
1281 apply (simp add: Prf.intros(5) ValOrd.intros(8)) |
|
1282 defer |
|
1283 apply(drule_tac x="s" in meta_spec) |
|
1284 apply(auto)[1] |
|
1285 apply(rule_tac x="Left v" in exI) |
|
1286 apply(simp add: POSIX2_def) |
|
1287 apply(auto)[1] |
|
1288 using Prf.intros(2) apply blast |
|
1289 apply(case_tac s) |
|
1290 apply(simp) |
|
1291 apply(auto)[1] |
|
1292 apply (simp add: ValOrd.intros(6)) |
|
1293 apply(rule ValOrd.intros) |
|
1294 |
1076 thm PMatch.intros[no_vars] |
1295 thm PMatch.intros[no_vars] |
1077 |
1296 |
1078 lemma POSIX_PMatch: |
1297 lemma POSIX_PMatch: |
1079 assumes "s \<in> r \<rightarrow> v" "v' \<in> Values r s" |
1298 assumes "s \<in> r \<rightarrow> v" "v' \<in> Values r s" |
1080 shows "v \<succ>r v' \<or> length (flat v') < length (flat v)" |
1299 shows "v \<succ>r v' \<or> length (flat v') < length (flat v)" |