equal
deleted
inserted
replaced
1173 case (FROMNTIMES r n) |
1173 case (FROMNTIMES r n) |
1174 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1174 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1175 have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact |
1175 have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact |
1176 then consider |
1176 then consider |
1177 (null) v1 vs s1 s2 where |
1177 (null) v1 vs s1 s2 where |
|
1178 "n = 0" |
1178 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1179 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1179 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)" |
1180 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
1180 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))" |
1181 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))" |
1181 | (cons) m v1 vs s1 s2 where |
1182 | (cons) m v1 vs s1 s2 where |
1182 "n = Suc m" |
1183 "n = Suc m" |
1183 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1184 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1184 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
1185 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
1198 apply(drule_tac x="s1" in meta_spec) |
1199 apply(drule_tac x="s1" in meta_spec) |
1199 apply(simp) |
1200 apply(simp) |
1200 apply(drule_tac x="s1a @ s2a" in meta_spec) |
1201 apply(drule_tac x="s1a @ s2a" in meta_spec) |
1201 apply(simp) |
1202 apply(simp) |
1202 apply(drule meta_mp) |
1203 apply(drule meta_mp) |
1203 defer |
1204 apply(rule Posix.intros) |
|
1205 apply(simp) |
|
1206 apply(simp) |
|
1207 apply(simp) |
|
1208 apply(simp) |
1204 using Pow_in_Star apply blast |
1209 using Pow_in_Star apply blast |
1205 apply (meson Posix_FROMNTIMES2 append_is_Nil_conv self_append_conv) |
1210 by (meson Posix_STAR2 append_is_Nil_conv self_append_conv) |
1206 sorry |
|
1207 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" |
1211 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" |
1208 proof (cases) |
1212 proof (cases) |
1209 case cons |
1213 case cons |
1210 have "n = Suc m" by fact |
1214 have "n = Suc m" by fact |
1211 moreover |
1215 moreover |
1221 have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
1225 have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
1222 apply(rule_tac Posix.intros(12)) |
1226 apply(rule_tac Posix.intros(12)) |
1223 apply(simp_all) |
1227 apply(simp_all) |
1224 done |
1228 done |
1225 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
1229 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
|
1230 next |
|
1231 case null |
|
1232 then show ?thesis |
|
1233 apply(simp) |
|
1234 sorry |
1226 qed |
1235 qed |
1227 qed |
1236 qed |
1228 |
1237 |
1229 |
1238 |
1230 section {* The Lexer by Sulzmann and Lu *} |
1239 section {* The Lexer by Sulzmann and Lu *} |