807 shows "L (der c r) = Der c (L r)" |
812 shows "L (der c r) = Der c (L r)" |
808 apply(induct r) |
813 apply(induct r) |
809 apply(simp_all add: nullable_correctness) |
814 apply(simp_all add: nullable_correctness) |
810 done |
815 done |
811 |
816 |
|
817 lemma ders_correctness: |
|
818 shows "L (ders s r) = Ders s (L r)" |
|
819 apply(induct s arbitrary: r) |
|
820 apply(simp add: Ders_def) |
|
821 apply(simp) |
|
822 apply(subst der_correctness) |
|
823 apply(simp add: Ders_def Der_def) |
|
824 done |
|
825 |
812 section {* Injection function *} |
826 section {* Injection function *} |
813 |
827 |
814 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
828 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
815 where |
829 where |
816 "injval (EMPTY) c Void = Char c" |
830 "injval (CHAR d) c Void = Char d" |
817 | "injval (CHAR d) c Void = Char d" |
|
818 | "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')" |
|
819 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
831 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
820 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
832 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
821 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
833 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
822 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
834 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
823 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
835 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
1025 assumes "\<Turnstile> v : r" and "(flat v) = c # s" |
1038 assumes "\<Turnstile> v : r" and "(flat v) = c # s" |
1026 shows "flat (projval r c v) = s" |
1039 shows "flat (projval r c v) = s" |
1027 using assms |
1040 using assms |
1028 by (metis list.inject v4_proj) |
1041 by (metis list.inject v4_proj) |
1029 |
1042 |
|
1043 |
|
1044 section {* Roy's 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 |
1030 |
1150 |
1031 section {* Alternative Posix definition *} |
1151 section {* Alternative Posix definition *} |
1032 |
1152 |
1033 inductive |
1153 inductive |
1034 PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
1154 PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
1043 | "\<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> []; |
1044 \<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> |
1045 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1165 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1046 | "[] \<in> STAR r \<rightarrow> Stars []" |
1166 | "[] \<in> STAR r \<rightarrow> Stars []" |
1047 |
1167 |
1048 lemma PMatch_mkeps: |
|
1049 assumes "nullable r" |
|
1050 shows "[] \<in> r \<rightarrow> mkeps r" |
|
1051 using assms |
|
1052 apply(induct r) |
|
1053 apply(auto) |
|
1054 apply (metis PMatch.intros(1)) |
|
1055 apply(subst append.simps(1)[symmetric]) |
|
1056 apply (rule PMatch.intros) |
|
1057 apply(simp) |
|
1058 apply(simp) |
|
1059 apply(auto)[1] |
|
1060 apply (rule PMatch.intros) |
|
1061 apply(simp) |
|
1062 apply (rule PMatch.intros) |
|
1063 apply(simp) |
|
1064 apply (rule PMatch.intros) |
|
1065 apply(simp) |
|
1066 apply (metis nullable_correctness) |
|
1067 apply(metis PMatch.intros(7)) |
|
1068 done |
|
1069 |
|
1070 lemma PMatch1: |
1168 lemma PMatch1: |
1071 assumes "s \<in> r \<rightarrow> v" |
1169 assumes "s \<in> r \<rightarrow> v" |
1072 shows "\<turnstile> v : r" "flat v = s" |
1170 shows "\<turnstile> v : r" "flat v = s" |
1073 using assms |
1171 using assms |
1074 apply(induct s r v rule: PMatch.induct) |
1172 apply(induct s r v rule: PMatch.induct) |
1078 apply (metis Prf.intros(2)) |
1176 apply (metis Prf.intros(2)) |
1079 apply (metis Prf.intros(3)) |
1177 apply (metis Prf.intros(3)) |
1080 apply (metis Prf.intros(1)) |
1178 apply (metis Prf.intros(1)) |
1081 apply (metis Prf.intros(7)) |
1179 apply (metis Prf.intros(7)) |
1082 by (metis Prf.intros(6)) |
1180 by (metis Prf.intros(6)) |
|
1181 |
|
1182 |
|
1183 lemma |
|
1184 assumes "\<rhd> v : r" |
|
1185 shows "(flat v) \<in> r \<rightarrow> v" |
|
1186 using assms |
|
1187 apply(induct) |
|
1188 apply(auto intro: PMatch.intros) |
|
1189 apply(rule PMatch.intros) |
|
1190 apply(simp) |
|
1191 apply(simp) |
|
1192 apply(simp) |
|
1193 apply(auto)[1] |
|
1194 done |
|
1195 |
|
1196 lemma |
|
1197 assumes "s \<in> r \<rightarrow> v" |
|
1198 shows "\<rhd> v : r" |
|
1199 using assms |
|
1200 apply(induct) |
|
1201 apply(auto intro: Roy.intros) |
|
1202 apply (metis PMatch1(2) Roy.intros(4)) |
|
1203 apply (metis PMatch1(2) Roy.intros(5)) |
|
1204 by (metis L.simps(6) PMatch1(2) Roy.intros(6)) |
|
1205 |
|
1206 |
|
1207 lemma PMatch_mkeps: |
|
1208 assumes "nullable r" |
|
1209 shows "[] \<in> r \<rightarrow> mkeps r" |
|
1210 using assms |
|
1211 apply(induct r) |
|
1212 apply(auto) |
|
1213 apply (metis PMatch.intros(1)) |
|
1214 apply(subst append.simps(1)[symmetric]) |
|
1215 apply (rule PMatch.intros) |
|
1216 apply(simp) |
|
1217 apply(simp) |
|
1218 apply(auto)[1] |
|
1219 apply (rule PMatch.intros) |
|
1220 apply(simp) |
|
1221 apply (rule PMatch.intros) |
|
1222 apply(simp) |
|
1223 apply (rule PMatch.intros) |
|
1224 apply(simp) |
|
1225 apply (metis nullable_correctness) |
|
1226 apply(metis PMatch.intros(7)) |
|
1227 done |
|
1228 |
1083 |
1229 |
1084 lemma PMatch1N: |
1230 lemma PMatch1N: |
1085 assumes "s \<in> r \<rightarrow> v" |
1231 assumes "s \<in> r \<rightarrow> v" |
1086 shows "\<Turnstile> v : r" |
1232 shows "\<Turnstile> v : r" |
1087 using assms |
1233 using assms |
1339 apply (metis Nil_is_append_conv) |
1485 apply (metis Nil_is_append_conv) |
1340 apply(simp) |
1486 apply(simp) |
1341 apply(subst der_correctness) |
1487 apply(subst der_correctness) |
1342 apply(simp add: Der_def) |
1488 apply(simp add: Der_def) |
1343 done |
1489 done |
|
1490 |
|
1491 lemma PMatch_Roy2: |
|
1492 assumes "2\<rhd> v : (der c r)" |
|
1493 shows "2\<rhd> (injval r c v) : r" |
|
1494 using assms |
|
1495 apply(induct c r arbitrary: v rule: der.induct) |
|
1496 apply(auto) |
|
1497 apply(erule Roy2.cases) |
|
1498 apply(simp_all) |
|
1499 apply(erule Roy2.cases) |
|
1500 apply(simp_all) |
|
1501 apply(case_tac "c = c'") |
|
1502 apply(simp) |
|
1503 apply(erule Roy2.cases) |
|
1504 apply(simp_all) |
|
1505 apply (metis Roy2.intros(2)) |
|
1506 apply(erule Roy2.cases) |
|
1507 apply(simp_all) |
|
1508 apply(erule Roy2.cases) |
|
1509 apply(simp_all) |
|
1510 apply(clarify) |
|
1511 apply (metis Roy2.intros(3)) |
|
1512 apply(clarify) |
|
1513 apply(rule Roy2.intros(4)) |
|
1514 apply(metis) |
|
1515 apply(simp add: der_correctness Der_def) |
|
1516 apply(subst v4) |
|
1517 apply (metis Roy2_props) |
|
1518 apply(simp) |
|
1519 apply(case_tac "nullable r1") |
|
1520 apply(simp) |
|
1521 apply(erule Roy2.cases) |
|
1522 apply(simp_all) |
|
1523 apply(clarify) |
|
1524 apply(erule Roy2.cases) |
|
1525 apply(simp_all) |
|
1526 apply(clarify) |
|
1527 apply(rule Roy2.intros) |
|
1528 apply metis |
|
1529 apply(simp) |
|
1530 apply(auto)[1] |
|
1531 apply(simp add: ders_correctness Ders_def) |
|
1532 apply(simp add: der_correctness Der_def) |
|
1533 apply(drule_tac x="s" in spec) |
|
1534 apply(drule mp) |
|
1535 apply(rule conjI) |
|
1536 apply(subst (asm) v4) |
|
1537 apply (metis Roy2_props) |
|
1538 apply(simp) |
|
1539 apply(rule_tac x="t" in exI) |
|
1540 apply(simp) |
|
1541 apply(simp) |
|
1542 apply(rule Roy2.intros) |
|
1543 apply (metis Roy_mkeps_nullable) |
|
1544 apply metis |
|
1545 apply(auto)[1] |
|
1546 apply(simp add: ders_correctness Ders_def) |
|
1547 apply(subst (asm) mkeps_flat) |
|
1548 apply(simp) |
|
1549 apply(simp) |
|
1550 apply(subst (asm) v4) |
|
1551 apply (metis Roy2_props) |
|
1552 apply(subst (asm) v4) |
|
1553 apply (metis Roy2_props) |
|
1554 apply(simp add: Sequ_def prefix_def) |
|
1555 apply(auto)[1] |
|
1556 apply(simp add: append_eq_Cons_conv) |
|
1557 apply(auto) |
|
1558 apply(drule_tac x="ys'" in spec) |
|
1559 apply(drule mp) |
|
1560 apply(simp add: der_correctness Der_def) |
|
1561 apply(simp add: append_eq_append_conv2) |
|
1562 apply(auto)[1] |
|
1563 prefer 2 |
|
1564 apply(erule Roy2.cases) |
|
1565 apply(simp_all) |
|
1566 apply(rule Roy2.intros) |
|
1567 apply metis |
|
1568 apply(simp) |
|
1569 apply(auto)[1] |
|
1570 apply(simp add: ders_correctness Ders_def) |
|
1571 apply(subst (asm) v4) |
|
1572 apply (metis Roy2_props) |
|
1573 apply(drule_tac x="s" in spec) |
|
1574 apply(drule mp) |
|
1575 apply(rule conjI) |
|
1576 apply(simp add: der_correctness Der_def) |
|
1577 apply(auto)[1] |
|
1578 oops |
|
1579 |
1344 |
1580 |
1345 lemma lex_correct1: |
1581 lemma lex_correct1: |
1346 assumes "s \<notin> L r" |
1582 assumes "s \<notin> L r" |
1347 shows "lex r s = None" |
1583 shows "lex r s = None" |
1348 using assms |
1584 using assms |
1434 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
1670 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
1435 | "Void \<succ>EMPTY Void" |
1671 | "Void \<succ>EMPTY Void" |
1436 | "(Char c) \<succ>(CHAR c) (Char c)" |
1672 | "(Char c) \<succ>(CHAR c) (Char c)" |
1437 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))" |
1673 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))" |
1438 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])" |
1674 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])" |
1439 | "v1 \<succ>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))" |
1675 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))" |
1440 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))" |
1676 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))" |
1441 | "(Stars []) \<succ>(STAR r) (Stars [])" |
1677 | "(Stars []) \<succ>(STAR r) (Stars [])" |
|
1678 |
|
1679 inductive ValOrd2 :: "val \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ>_ _" [100, 100, 100] 100) |
|
1680 where |
|
1681 "v2 2\<succ>s v2' \<Longrightarrow> (Seq v1 v2) 2\<succ>(flat v1 @ s) (Seq v1 v2')" |
|
1682 | "\<lbrakk>v1 2\<succ>s v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ>s (Seq v1' v2')" |
|
1683 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ>(flat v1) (Right v2)" |
|
1684 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ>(flat v2) (Left v1)" |
|
1685 | "v2 2\<succ>s v2' \<Longrightarrow> (Right v2) 2\<succ>s (Right v2')" |
|
1686 | "v1 2\<succ>s v1' \<Longrightarrow> (Left v1) 2\<succ>s (Left v1')" |
|
1687 | "Void 2\<succ>[] Void" |
|
1688 | "(Char c) 2\<succ>[c] (Char c)" |
|
1689 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) 2\<succ>[] (Stars (v # vs))" |
|
1690 | "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))" |
|
1692 | "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))" |
|
1693 | "(Stars []) 2\<succ>[] (Stars [])" |
|
1694 |
|
1695 |
|
1696 lemma admissibility: |
|
1697 assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v" |
|
1698 shows "v \<succ>r v'" |
|
1699 using assms |
|
1700 apply(induct arbitrary: v') |
|
1701 apply(erule Prf.cases) |
|
1702 apply(simp_all)[7] |
|
1703 apply (metis ValOrd.intros(7)) |
|
1704 apply(erule Prf.cases) |
|
1705 apply(simp_all)[7] |
|
1706 apply (metis ValOrd.intros(8)) |
|
1707 apply(erule Prf.cases) |
|
1708 apply(simp_all)[7] |
|
1709 apply (metis ValOrd.intros(6)) |
|
1710 apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def) |
|
1711 apply(erule Prf.cases) |
|
1712 apply(simp_all)[7] |
|
1713 apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def) |
|
1714 apply (metis ValOrd.intros(5)) |
|
1715 (* Seq case *) |
|
1716 apply(erule Prf.cases) |
|
1717 apply(clarify)+ |
|
1718 prefer 2 |
|
1719 apply(clarify) |
|
1720 prefer 2 |
|
1721 apply(clarify) |
|
1722 prefer 2 |
|
1723 apply(clarify) |
|
1724 prefer 2 |
|
1725 apply(clarify) |
|
1726 prefer 2 |
|
1727 apply(clarify) |
|
1728 prefer 2 |
|
1729 apply(clarify) |
|
1730 apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1") |
|
1731 prefer 2 |
|
1732 apply(simp add: prefix_def sprefix_def) |
|
1733 apply (metis append_eq_append_conv2) |
|
1734 apply(erule disjE) |
|
1735 apply(subst (asm) sprefix_def) |
|
1736 apply(subst (asm) (5) prefix_def) |
|
1737 apply(clarify) |
|
1738 apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2") |
|
1739 prefer 2 |
|
1740 apply(simp) |
|
1741 apply (metis append_assoc prefix_append) |
|
1742 apply(subgoal_tac "s3 \<noteq> []") |
|
1743 prefer 2 |
|
1744 apply (metis append_Nil2) |
|
1745 apply(subst (asm) (5) prefix_def) |
|
1746 apply(erule exE) |
|
1747 apply(drule_tac x="s3" in spec) |
|
1748 apply(drule_tac x="s3a" in spec) |
|
1749 apply(drule mp) |
|
1750 apply(rule conjI) |
|
1751 apply(simp add: ders_correctness Ders_def) |
|
1752 apply (metis Prf_flat_L) |
|
1753 apply(rule conjI) |
|
1754 apply(simp) |
|
1755 apply (metis append_assoc prefix_def) |
|
1756 apply(simp) |
|
1757 apply(subgoal_tac "drop (length s3) (flat v2) = flat v2a @ s3a") |
|
1758 apply(simp add: Sequ_def) |
|
1759 apply (metis Prf_flat_L) |
|
1760 thm drop_append |
|
1761 apply (metis append_eq_conv_conj) |
|
1762 apply(simp) |
|
1763 apply (metis ValOrd.intros(1) ValOrd.intros(2) flat.simps(5) prefix_append) |
|
1764 (* star cases *) |
|
1765 oops |
|
1766 |
|
1767 |
|
1768 lemma admisibility: |
|
1769 assumes "\<rhd> v : r" "\<turnstile> v' : r" |
|
1770 shows "v \<succ>r v'" |
|
1771 using assms |
|
1772 apply(induct arbitrary: v') |
|
1773 prefer 5 |
|
1774 apply(drule royA) |
|
1775 apply(erule Prf.cases) |
|
1776 apply(simp_all)[7] |
|
1777 apply(clarify) |
|
1778 apply(case_tac "v1 = v1a") |
|
1779 apply(simp) |
|
1780 apply(rule ValOrd.intros) |
|
1781 apply metis |
|
1782 apply (metis ValOrd.intros(2)) |
|
1783 apply(erule Prf.cases) |
|
1784 apply(simp_all)[7] |
|
1785 apply (metis ValOrd.intros(7)) |
|
1786 apply(erule Prf.cases) |
|
1787 apply(simp_all)[7] |
|
1788 apply (metis ValOrd.intros(8)) |
|
1789 apply(erule Prf.cases) |
|
1790 apply(simp_all)[7] |
|
1791 apply (metis ValOrd.intros(6)) |
|
1792 apply(rule ValOrd.intros) |
|
1793 defer |
|
1794 apply(erule Prf.cases) |
|
1795 apply(simp_all)[7] |
|
1796 apply(clarify) |
|
1797 apply(rule ValOrd.intros) |
|
1798 (* seq case goes through *) |
|
1799 oops |
|
1800 |
|
1801 |
|
1802 lemma admisibility: |
|
1803 assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v" |
|
1804 shows "v \<succ>r v'" |
|
1805 using assms |
|
1806 apply(induct arbitrary: v') |
|
1807 prefer 5 |
|
1808 apply(drule royA) |
|
1809 apply(erule Prf.cases) |
|
1810 apply(simp_all)[7] |
|
1811 apply(clarify) |
|
1812 apply(case_tac "v1 = v1a") |
|
1813 apply(simp) |
|
1814 apply(rule ValOrd.intros) |
|
1815 apply(subst (asm) (3) prefix_def) |
|
1816 apply(erule exE) |
|
1817 apply(simp) |
|
1818 apply (metis prefix_def) |
|
1819 (* the unequal case *) |
|
1820 apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1") |
|
1821 prefer 2 |
|
1822 apply(simp add: prefix_def sprefix_def) |
|
1823 apply (metis append_eq_append_conv2) |
|
1824 apply(erule disjE) |
|
1825 (* first case flat v1 \<sqsubset> flat v1a *) |
|
1826 apply(subst (asm) sprefix_def) |
|
1827 apply(subst (asm) (5) prefix_def) |
|
1828 apply(clarify) |
|
1829 apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2") |
|
1830 prefer 2 |
|
1831 apply(simp) |
|
1832 apply (metis append_assoc prefix_append) |
|
1833 apply(subgoal_tac "s3 \<noteq> []") |
|
1834 prefer 2 |
|
1835 apply (metis append_Nil2) |
|
1836 (* HERE *) |
|
1837 apply(subst (asm) (5) prefix_def) |
|
1838 apply(erule exE) |
|
1839 apply(simp add: ders_correctness Ders_def) |
|
1840 apply(simp add: prefix_def) |
|
1841 apply(clarify) |
|
1842 apply(subst (asm) append_eq_append_conv2) |
|
1843 apply(erule exE) |
|
1844 apply(erule disjE) |
|
1845 apply(clarify) |
|
1846 oops |
|
1847 |
|
1848 |
1442 |
1849 |
1443 lemma ValOrd_refl: |
1850 lemma ValOrd_refl: |
1444 assumes "\<turnstile> v : r" |
1851 assumes "\<turnstile> v : r" |
1445 shows "v \<succ>r v" |
1852 shows "v \<succ>r v" |
1446 using assms |
1853 using assms |
1507 apply (metis ValOrd.intros(10) ValOrd.intros(9)) |
1914 apply (metis ValOrd.intros(10) ValOrd.intros(9)) |
1508 apply(erule Prf.cases) |
1915 apply(erule Prf.cases) |
1509 apply(simp_all)[7] |
1916 apply(simp_all)[7] |
1510 apply(auto) |
1917 apply(auto) |
1511 apply (metis ValOrd.intros(10) ValOrd.intros(9)) |
1918 apply (metis ValOrd.intros(10) ValOrd.intros(9)) |
1512 by (metis ValOrd.intros(11)) |
1919 apply(case_tac "v = va") |
|
1920 prefer 2 |
|
1921 apply (metis ValOrd.intros(11)) |
|
1922 apply(simp) |
|
1923 apply(rule ValOrd.intros(12)) |
|
1924 apply(erule contrapos_np) |
|
1925 apply(rule ValOrd.intros(12)) |
|
1926 oops |
|
1927 |
|
1928 lemma Roy_posix: |
|
1929 assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v" |
|
1930 shows "v \<succ>r v'" |
|
1931 using assms |
|
1932 apply(induct r arbitrary: v v' rule: rexp.induct) |
|
1933 apply(erule Prf.cases) |
|
1934 apply(simp_all)[7] |
|
1935 apply(erule Prf.cases) |
|
1936 apply(simp_all)[7] |
|
1937 apply(erule Roy.cases) |
|
1938 apply(simp_all) |
|
1939 apply (metis ValOrd.intros(7)) |
|
1940 apply(erule Prf.cases) |
|
1941 apply(simp_all)[7] |
|
1942 apply(erule Roy.cases) |
|
1943 apply(simp_all) |
|
1944 apply (metis ValOrd.intros(8)) |
|
1945 prefer 2 |
|
1946 apply(erule Prf.cases) |
|
1947 apply(simp_all)[7] |
|
1948 apply(erule Roy.cases) |
|
1949 apply(simp_all) |
|
1950 apply(clarify) |
|
1951 apply (metis ValOrd.intros(6)) |
|
1952 apply(clarify) |
|
1953 apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def) |
|
1954 apply(erule Roy.cases) |
|
1955 apply(simp_all) |
|
1956 apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def) |
|
1957 apply(clarify) |
|
1958 apply (metis ValOrd.intros(5)) |
|
1959 apply(erule Prf.cases) |
|
1960 apply(simp_all)[7] |
|
1961 apply(erule Roy.cases) |
|
1962 apply(simp_all) |
|
1963 apply(clarify) |
|
1964 apply(case_tac "v1a = v1") |
|
1965 apply(simp) |
|
1966 apply(rule ValOrd.intros) |
|
1967 apply (metis prefix_append) |
|
1968 apply(rule ValOrd.intros) |
|
1969 prefer 2 |
|
1970 apply(simp) |
|
1971 apply(simp add: prefix_def) |
|
1972 apply(auto)[1] |
|
1973 apply(simp add: append_eq_append_conv2) |
|
1974 apply(auto)[1] |
|
1975 apply(drule_tac x="v1a" in meta_spec) |
|
1976 apply(rotate_tac 9) |
|
1977 apply(drule_tac x="v1" in meta_spec) |
|
1978 apply(drule_tac meta_mp) |
|
1979 apply(simp) |
|
1980 apply(drule_tac meta_mp) |
|
1981 apply(simp) |
|
1982 apply(drule_tac meta_mp) |
|
1983 apply(simp) |
|
1984 apply(drule_tac x="us" in spec) |
|
1985 apply(drule_tac mp) |
|
1986 apply (metis Prf_flat_L) |
|
1987 apply(auto)[1] |
|
1988 oops |
|
1989 |
1513 |
1990 |
1514 lemma ValOrd_anti: |
1991 lemma ValOrd_anti: |
1515 shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2" |
1992 shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2" |
1516 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" |
1993 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" |
1517 apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts) |
1994 apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts) |