1171 | Posix_FROMNTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
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> |
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)" |
1173 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (v # vs)" |
1174 | 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> |
1175 \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs" |
1175 \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs" |
1176 | 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 - 1) (m - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; n \<le> m; |
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> |
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 - 1) (m - 1)))\<rbrakk> |
1178 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
1178 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (v # vs)" |
|
1179 | Posix_NMTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < m; |
|
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 r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))\<rbrakk> |
|
1181 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (v # vs)" |
1179 |
1182 |
1180 inductive_cases Posix_elims: |
1183 inductive_cases Posix_elims: |
1181 "s \<in> ZERO \<rightarrow> v" |
1184 "s \<in> ZERO \<rightarrow> v" |
1182 "s \<in> ONE \<rightarrow> v" |
1185 "s \<in> ONE \<rightarrow> v" |
1183 "s \<in> CHAR c \<rightarrow> v" |
1186 "s \<in> CHAR c \<rightarrow> v" |
1394 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1402 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+ |
1403 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1396 ultimately show "Stars (v # vs) = v2" by auto |
1404 ultimately show "Stars (v # vs) = v2" by auto |
1397 next |
1405 next |
1398 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
1406 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
1399 then show "Stars (v # vs) = v2" |
1407 have "(s1 @ s2) \<in> NMTIMES r n m \<rightarrow> v2" |
1400 sorry |
1408 "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1409 "0 < n" "n \<le> m" |
|
1410 "\<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 - 1) (m - 1)))" by fact+ |
|
1411 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" |
|
1412 "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs')" |
|
1413 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1414 using Posix1(1) Posix1(2) apply blast |
|
1415 apply(case_tac n) |
|
1416 apply(simp) |
|
1417 apply(simp) |
|
1418 apply(case_tac m) |
|
1419 apply(simp) |
|
1420 apply(simp) |
|
1421 apply(drule_tac x="va" in meta_spec) |
|
1422 apply(drule_tac x="vs" in meta_spec) |
|
1423 apply(simp) |
|
1424 apply(drule meta_mp) |
|
1425 apply (smt L.simps(10) Posix1(1) Posix1(2) Posix_NMTIMES1.hyps(4) UN_E append.right_neutral |
|
1426 append_eq_append_conv2 diff_Suc_1 val.inject(5)) |
|
1427 apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2) |
|
1428 by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil) |
|
1429 moreover |
|
1430 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1431 "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1432 ultimately show "Stars (v # vs) = v2" by auto |
1401 next |
1433 next |
1402 case (Posix_NMTIMES2 vs r n m v2) |
1434 case (Posix_NMTIMES2 vs r n m v2) |
1403 then show "Stars vs = v2" |
1435 then show "Stars vs = v2" |
1404 sorry |
1436 apply(erule_tac Posix_elims) |
|
1437 apply(simp) |
|
1438 apply(rule List_eq_zipI) |
|
1439 apply(auto) |
|
1440 apply (meson in_set_zipE) |
|
1441 apply (simp add: Posix1(2)) |
|
1442 apply(erule_tac Posix_elims) |
|
1443 apply(auto) |
|
1444 apply (simp add: Posix1(2))+ |
|
1445 done |
|
1446 next |
|
1447 case (Posix_NMTIMES3 s1 r v s2 m vs v2) |
|
1448 have "(s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> v2" |
|
1449 "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" "0 < m" |
|
1450 "\<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 (UPNTIMES r (m - 1 )))" by fact+ |
|
1451 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs')" |
|
1452 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1453 using Posix1(2) apply blast |
|
1454 apply (smt L.simps(7) Posix1(1) UN_E append_eq_append_conv2) |
|
1455 by (metis One_nat_def Posix1(1) Posix_NMTIMES3.hyps(7) append.right_neutral append_Nil) |
|
1456 moreover |
|
1457 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1458 "\<And>v2. s2 \<in> UPNTIMES r (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1459 ultimately show "Stars (v # vs) = v2" by auto |
1405 qed |
1460 qed |
1406 |
1461 |
1407 |
1462 |
1408 text {* |
1463 text {* |
1409 Our POSIX value is a lexical value. |
1464 Our POSIX value is a lexical value. |
1439 apply(clarify) |
1494 apply(clarify) |
1440 apply(erule Prf_elims) |
1495 apply(erule Prf_elims) |
1441 apply(simp) |
1496 apply(simp) |
1442 apply(rule Prf.intros) |
1497 apply(rule Prf.intros) |
1443 apply(simp) |
1498 apply(simp) |
|
1499 apply(simp) |
|
1500 (* NTIMES *) |
|
1501 prefer 4 |
|
1502 apply(simp) |
|
1503 apply(case_tac n) |
1444 apply(simp) |
1504 apply(simp) |
|
1505 apply(simp) |
|
1506 apply(clarify) |
|
1507 apply(rotate_tac 5) |
|
1508 apply(erule Prf_elims) |
|
1509 apply(simp) |
|
1510 apply(subst append.simps(2)[symmetric]) |
|
1511 apply(rule Prf.intros) |
|
1512 apply(simp) |
|
1513 apply(simp) |
|
1514 apply(simp) |
|
1515 prefer 4 |
|
1516 apply(simp) |
|
1517 apply (metis Prf.intros(8) length_removeAll_less less_irrefl_nat removeAll.simps(1) self_append_conv2) |
1445 (* NMTIMES *) |
1518 (* NMTIMES *) |
1446 sorry |
1519 apply(simp) |
1447 |
1520 apply (metis Prf.intros(11) append_Nil empty_iff list.set(1)) |
|
1521 apply(simp) |
|
1522 apply(clarify) |
|
1523 apply(rotate_tac 6) |
|
1524 apply(erule Prf_elims) |
|
1525 apply(simp) |
|
1526 apply(subst append.simps(2)[symmetric]) |
|
1527 apply(rule Prf.intros) |
|
1528 apply(simp) |
|
1529 apply(simp) |
|
1530 apply(simp) |
|
1531 apply(simp) |
|
1532 apply(rule Prf.intros) |
|
1533 apply(simp) |
|
1534 apply(simp) |
|
1535 apply(simp) |
|
1536 apply(simp) |
|
1537 apply(clarify) |
|
1538 apply(rotate_tac 6) |
|
1539 apply(erule Prf_elims) |
|
1540 apply(simp) |
|
1541 apply(rule Prf.intros) |
|
1542 apply(simp) |
|
1543 apply(simp) |
|
1544 apply(simp) |
|
1545 done |
1448 |
1546 |
1449 end |
1547 end |