270 then ALT (SEQ (der c r1) r2) (der c r2) |
270 then ALT (SEQ (der c r1) r2) (der c r2) |
271 else SEQ (der c r1) r2)" |
271 else SEQ (der c r1) r2)" |
272 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
272 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
273 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))" |
273 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))" |
274 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))" |
274 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))" |
275 | "der c (FROMNTIMES r n) = SEQ (der c r) (FROMNTIMES r (n - 1))" |
275 | "der c (FROMNTIMES r n) = |
|
276 (if n = 0 |
|
277 then SEQ (der c r) (STAR r) |
|
278 else SEQ (der c r) (FROMNTIMES r (n - 1)))" |
276 | "der c (NMTIMES r n m) = |
279 | "der c (NMTIMES r n m) = |
277 (if m < n then ZERO |
280 (if m < n then ZERO |
278 else (if n = 0 then (if m = 0 then ZERO else |
281 else (if n = 0 then (if m = 0 then ZERO else |
279 SEQ (der c r) (UPNTIMES r (m - 1))) else |
282 SEQ (der c r) (UPNTIMES r (m - 1))) else |
280 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
283 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
312 apply(simp) |
315 apply(simp) |
313 apply(simp only: Der_union Der_empty) |
316 apply(simp only: Der_union Der_empty) |
314 apply(simp) |
317 apply(simp) |
315 (* FROMNTIMES *) |
318 (* FROMNTIMES *) |
316 apply(simp add: nullable_correctness del: Der_UNION) |
319 apply(simp add: nullable_correctness del: Der_UNION) |
|
320 apply(rule conjI) |
|
321 prefer 2 |
317 apply(subst Sequ_Union_in) |
322 apply(subst Sequ_Union_in) |
318 apply(subst Der_Pow_Sequ[symmetric]) |
323 apply(subst Der_Pow_Sequ[symmetric]) |
319 apply(subst Pow.simps[symmetric]) |
324 apply(subst Pow.simps[symmetric]) |
320 apply(case_tac x2) |
325 apply(case_tac x2) |
321 prefer 2 |
326 prefer 2 |
322 apply(subst Pow_Sequ_Un2) |
327 apply(subst Pow_Sequ_Un2) |
323 apply(simp) |
328 apply(simp) |
324 apply(simp) |
329 apply(simp) |
325 apply(auto simp add: Sequ_def Der_def)[1] |
330 apply(auto simp add: Sequ_def Der_def)[1] |
326 apply(rule_tac x="Suc xa" in exI) |
331 apply(auto simp add: Sequ_def split: if_splits)[1] |
327 apply(auto simp add: Sequ_def)[1] |
332 using Star_Pow apply fastforce |
328 apply(drule Pow_decomp) |
333 using Pow_Star apply blast |
329 apply(auto)[1] |
|
330 apply (metis append_Cons) |
|
331 (* NMTIMES *) |
334 (* NMTIMES *) |
332 apply(simp add: nullable_correctness del: Der_UNION) |
335 apply(simp add: nullable_correctness del: Der_UNION) |
333 apply(rule impI) |
336 apply(rule impI) |
334 apply(rule conjI) |
337 apply(rule conjI) |
335 apply(rule impI) |
338 apply(rule impI) |
1163 | Posix_FROMNTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
1166 | Posix_FROMNTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
1164 \<Longrightarrow> [] \<in> FROMNTIMES r n \<rightarrow> Stars vs" |
1167 \<Longrightarrow> [] \<in> FROMNTIMES r n \<rightarrow> Stars vs" |
1165 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
1168 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
1166 \<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 (FROMNTIMES r (n - 1)))\<rbrakk> |
1169 \<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 (FROMNTIMES r (n - 1)))\<rbrakk> |
1167 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (v # vs)" |
1170 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (v # vs)" |
|
1171 | Posix_FROMNTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
1172 \<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> |
|
1173 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (v # vs)" |
1168 | Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk> |
1174 | Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk> |
1169 \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs" |
1175 \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs" |
1170 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; n \<le> m; |
1176 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; n \<le> m; |
1171 \<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 (NMTIMES r n m))\<rbrakk> |
1177 \<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 (NMTIMES r n m))\<rbrakk> |
1172 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
1178 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
1203 apply(simp) |
1209 apply(simp) |
1204 apply(clarify) |
1210 apply(clarify) |
1205 apply(rule_tac x="Suc x" in bexI) |
1211 apply(rule_tac x="Suc x" in bexI) |
1206 apply(simp add: Sequ_def) |
1212 apply(simp add: Sequ_def) |
1207 apply(auto)[3] |
1213 apply(auto)[3] |
|
1214 defer |
1208 apply(simp) |
1215 apply(simp) |
1209 apply fastforce |
1216 apply fastforce |
1210 apply(simp) |
1217 apply(simp) |
1211 apply(simp) |
1218 apply(simp) |
1212 apply(clarify) |
1219 apply(clarify) |
1213 apply(rule_tac x="Suc x" in bexI) |
1220 apply(rule_tac x="Suc x" in bexI) |
1214 apply(auto simp add: Sequ_def)[2] |
1221 apply(auto simp add: Sequ_def)[2] |
1215 apply(simp) |
1222 apply(simp) |
1216 done |
1223 apply(simp) |
|
1224 by (simp add: Star.step Star_Pow) |
1217 |
1225 |
1218 text {* |
1226 text {* |
1219 Our Posix definition determines a unique value. |
1227 Our Posix definition determines a unique value. |
1220 *} |
1228 *} |
1221 |
1229 |
1341 apply(auto) |
1349 apply(auto) |
1342 by (simp add: Posix1(2)) |
1350 by (simp add: Posix1(2)) |
1343 next |
1351 next |
1344 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
1352 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
1345 have "(s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> v2" |
1353 have "(s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> v2" |
1346 "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
1354 "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" "0 < n" |
1347 "\<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 (FROMNTIMES r (n - 1 )))" by fact+ |
1355 "\<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 (FROMNTIMES r (n - 1 )))" by fact+ |
1348 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
1356 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
1349 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1357 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1350 using Posix1(1) Posix1(2) apply blast |
1358 using Posix1(1) Posix1(2) apply blast |
1351 apply(drule_tac x="v" in meta_spec) |
1359 apply(case_tac n) |
|
1360 apply(simp) |
|
1361 apply(simp) |
|
1362 apply(drule_tac x="va" in meta_spec) |
1352 apply(drule_tac x="vs" in meta_spec) |
1363 apply(drule_tac x="vs" in meta_spec) |
1353 apply(simp) |
1364 apply(simp) |
1354 apply(drule meta_mp) |
1365 apply(drule meta_mp) |
1355 apply(case_tac n) |
1366 apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5)) |
1356 apply(simp) |
1367 apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil) |
1357 apply(rule conjI) |
1368 by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2) |
1358 apply (smt L.simps(9) One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps Suc_mono Suc_pred UN_E append.right_neutral append_Nil lessI less_antisym list.size(3) nat.simps(3) neq0_conv not_less_eq val.inject(5)) |
|
1359 apply(rule List_eq_zipI) |
|
1360 apply(auto)[1] |
|
1361 sorry |
|
1362 moreover |
1369 moreover |
1363 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1370 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1364 "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1371 "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1365 ultimately show "Stars (v # vs) = v2" by auto |
1372 ultimately show "Stars (v # vs) = v2" by auto |
1366 next |
1373 next |
1368 then show "Stars vs = v2" |
1375 then show "Stars vs = v2" |
1369 apply(erule_tac Posix_elims) |
1376 apply(erule_tac Posix_elims) |
1370 apply(auto) |
1377 apply(auto) |
1371 apply(rule List_eq_zipI) |
1378 apply(rule List_eq_zipI) |
1372 apply(auto) |
1379 apply(auto) |
1373 apply(meson in_set_zipE) |
1380 apply(meson in_set_zipE) |
1374 by (simp add: Posix1(2)) |
1381 apply (simp add: Posix1(2)) |
1375 next |
1382 using Posix1(2) by blast |
|
1383 next |
|
1384 case (Posix_FROMNTIMES3 s1 r v s2 vs v2) |
|
1385 have "(s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> v2" |
|
1386 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1387 "\<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))" by fact+ |
|
1388 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
1389 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1390 using Posix1(2) apply fastforce |
|
1391 using Posix1(1) apply fastforce |
|
1392 by (metis Posix1(1) Posix_FROMNTIMES3.hyps(6) append.right_neutral append_Nil) |
|
1393 moreover |
|
1394 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1395 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1396 ultimately show "Stars (v # vs) = v2" by auto |
|
1397 next |
1376 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
1398 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
1377 then show "Stars (v # vs) = v2" |
1399 then show "Stars (v # vs) = v2" |
1378 sorry |
1400 sorry |
1379 next |
1401 next |
1380 case (Posix_NMTIMES2 vs r n m v2) |
1402 case (Posix_NMTIMES2 vs r n m v2) |
1395 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[7] |
1417 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[7] |
1396 defer |
1418 defer |
1397 defer |
1419 defer |
1398 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2] |
1420 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2] |
1399 apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq) |
1421 apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq) |
1400 prefer 4 |
1422 apply(simp) |
1401 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[1] |
1423 apply(clarify) |
1402 apply(subst append.simps(2)[symmetric]) |
1424 apply(case_tac n) |
1403 apply(rule Prf.intros) |
1425 apply(simp) |
1404 apply(auto) |
1426 apply(simp) |
1405 prefer 4 |
1427 apply(erule Prf_elims) |
1406 apply (metis Prf.intros(8) append_Nil empty_iff list.set(1)) |
1428 apply(simp) |
1407 apply(erule Posix_elims) |
|
1408 apply(auto) |
|
1409 apply(rule_tac t="v # vsa" and s = "[v] @ vsa" in subst) |
|
1410 apply(simp) |
|
1411 apply(rule Prf.intros) |
|
1412 apply(simp) |
|
1413 apply(auto)[1] |
|
1414 apply(auto simp add: Sequ_def intro: Prf.intros elim: Prf_elims)[1] |
|
1415 apply(simp) |
|
1416 apply(rotate_tac 4) |
|
1417 apply(erule Prf_elims) |
|
1418 apply(auto) |
|
1419 apply(case_tac n) |
|
1420 apply(simp) |
|
1421 |
|
1422 apply(subst append.simps(2)[symmetric]) |
1429 apply(subst append.simps(2)[symmetric]) |
1423 apply(rule Prf.intros) |
1430 apply(rule Prf.intros) |
1424 apply(auto) |
1431 apply(simp) |
1425 apply(rule Prf.intros(10)) |
1432 apply(simp) |
1426 apply(auto) |
1433 apply(simp) |
1427 apply (metis Prf.intros(11) append_Nil empty_iff list.set(1)) |
1434 apply(simp) |
1428 apply(rotate_tac 6) |
1435 apply(rule Prf.intros) |
1429 apply(erule Prf_elims) |
1436 apply(simp) |
1430 apply(simp) |
1437 apply(simp) |
1431 apply(subst append.simps(2)[symmetric]) |
1438 apply(simp) |
1432 apply(rule Prf.intros) |
1439 apply(clarify) |
1433 apply(auto) |
1440 apply(erule Prf_elims) |
1434 apply(rule_tac t="v # vsa" and s = "(v # vsa) @ []" in subst) |
1441 apply(simp) |
1435 apply(simp) |
1442 apply(rule Prf.intros) |
1436 apply(simp add: Prf.intros(12)) |
1443 apply(simp) |
1437 done |
1444 apply(simp) |
|
1445 (* NMTIMES *) |
|
1446 sorry |
1438 |
1447 |
1439 lemma FROMNTIMES_0: |
|
1440 assumes "s \<in> FROMNTIMES r 0 \<rightarrow> v" |
|
1441 shows "s = [] \<and> v = Stars []" |
|
1442 using assms |
|
1443 apply(erule_tac Posix_elims) |
|
1444 apply(auto) |
|
1445 done |
|
1446 |
|
1447 lemma FROMNTIMES_der_0: |
|
1448 shows "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)" |
|
1449 by(simp) |
|
1450 |
1448 |
1451 end |
1449 end |