1163 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
1163 | "\<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> |
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> |
1165 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1165 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1166 | "[] \<in> STAR r \<rightarrow> Stars []" |
1166 | "[] \<in> STAR r \<rightarrow> Stars []" |
1167 |
1167 |
|
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 |
1168 lemma PMatch1: |
1183 lemma PMatch1: |
1169 assumes "s \<in> r \<rightarrow> v" |
1184 assumes "s \<in> r \<rightarrow> v" |
1170 shows "\<turnstile> v : r" "flat v = s" |
1185 shows "\<turnstile> v : r" "flat v = s" |
1171 using assms |
1186 using assms |
1172 apply(induct s r v rule: PMatch.induct) |
1187 apply(induct s r v rule: PMatch.induct) |
1177 apply (metis Prf.intros(3)) |
1192 apply (metis Prf.intros(3)) |
1178 apply (metis Prf.intros(1)) |
1193 apply (metis Prf.intros(1)) |
1179 apply (metis Prf.intros(7)) |
1194 apply (metis Prf.intros(7)) |
1180 by (metis Prf.intros(6)) |
1195 by (metis Prf.intros(6)) |
1181 |
1196 |
|
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 |
1182 |
1244 |
1183 lemma |
1245 lemma |
1184 assumes "\<rhd> v : r" |
1246 assumes "\<rhd> v : r" |
1185 shows "(flat v) \<in> r \<rightarrow> v" |
1247 shows "(flat v) \<in> r \<rightarrow> v" |
1186 using assms |
1248 using assms |
1408 (* nullable case *) |
1470 (* nullable case *) |
1409 apply(erule PMatch.cases) |
1471 apply(erule PMatch.cases) |
1410 apply(simp_all)[7] |
1472 apply(simp_all)[7] |
1411 apply(clarify) |
1473 apply(clarify) |
1412 apply(erule PMatch.cases) |
1474 apply(erule PMatch.cases) |
1413 apply(simp_all)[7] |
1475 apply(simp_all)[4] |
1414 apply(clarify) |
1476 apply(clarify) |
|
1477 apply(simp (no_asm)) |
1415 apply(subst append.simps(2)[symmetric]) |
1478 apply(subst append.simps(2)[symmetric]) |
1416 apply(rule PMatch.intros) |
1479 apply(rule PMatch.intros) |
1417 apply metis |
1480 apply metis |
1418 apply metis |
1481 apply metis |
|
1482 apply(erule contrapos_nn) |
|
1483 apply(erule exE)+ |
1419 apply(auto)[1] |
1484 apply(auto)[1] |
1420 apply(simp add: L_flat_NPrf) |
1485 apply(simp add: L_flat_NPrf) |
1421 apply(auto)[1] |
1486 apply(auto)[1] |
|
1487 thm v3_proj |
1422 apply(frule_tac c="c" in v3_proj) |
1488 apply(frule_tac c="c" in v3_proj) |
1423 apply metis |
1489 apply metis |
1424 apply(drule_tac x="s\<^sub>3" in spec) |
1490 apply(rule_tac x="s\<^sub>3" in exI) |
1425 apply(drule mp) |
1491 apply(simp) |
1426 apply (metis NPrf_imp_Prf v4_proj2) |
1492 apply (metis NPrf_imp_Prf v4_proj2) |
1427 apply(simp) |
1493 apply(simp) |
1428 (* interesting case *) |
1494 (* interesting case *) |
|
1495 apply(clarify) |
1429 apply(clarify) |
1496 apply(clarify) |
1430 apply(simp) |
1497 apply(simp) |
1431 apply(subst (asm) L.simps(4)[symmetric]) |
1498 apply(subst (asm) L.simps(4)[symmetric]) |
1432 apply(simp only: L_flat_Prf) |
1499 apply(simp only: L_flat_Prf) |
1433 apply(simp) |
1500 apply(simp) |
1690 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) 2\<succ>(flat (Stars (v # vs))) (Stars [])" |
1757 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) 2\<succ>(flat (Stars (v # vs))) (Stars [])" |
1691 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) 2\<succ>(flat v1) (Stars (v2 # vs2))" |
1758 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) 2\<succ>(flat v1) (Stars (v2 # vs2))" |
1692 | "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))" |
1759 | "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))" |
1693 | "(Stars []) 2\<succ>[] (Stars [])" |
1760 | "(Stars []) 2\<succ>[] (Stars [])" |
1694 |
1761 |
|
1762 lemma admissibility: |
|
1763 assumes "\<turnstile> s \<in> r \<rightarrow> v" "\<turnstile> v' : r" |
|
1764 shows "v \<succ>r v'" |
|
1765 using assms |
|
1766 apply(induct arbitrary: v') |
|
1767 apply(erule Prf.cases) |
|
1768 apply(simp_all)[7] |
|
1769 apply (metis ValOrd.intros(7)) |
|
1770 apply(erule Prf.cases) |
|
1771 apply(simp_all)[7] |
|
1772 apply (metis ValOrd.intros(8)) |
|
1773 apply(erule Prf.cases) |
|
1774 apply(simp_all)[7] |
|
1775 apply (metis ValOrd.intros(6)) |
|
1776 oops |
1695 |
1777 |
1696 lemma admissibility: |
1778 lemma admissibility: |
1697 assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v" |
1779 assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v" |
1698 shows "v \<succ>r v'" |
1780 shows "v \<succ>r v'" |
1699 using assms |
1781 using assms |