1429 |
1429 |
1430 lemma Posix_val_ord_reverse: |
1430 lemma Posix_val_ord_reverse: |
1431 assumes "s \<in> r \<rightarrow> v1" |
1431 assumes "s \<in> r \<rightarrow> v1" |
1432 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1432 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1433 using assms |
1433 using assms |
1434 apply(induct) |
1434 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
1435 apply(auto)[1] |
1435 val_ord_ex1_def val_ord_ex_def val_ord_ex_trans) |
1436 apply(simp add: CPT_def) |
1436 |
|
1437 (* |
|
1438 lemma CPrf_Stars: |
|
1439 assumes "\<forall>v \<in> set vs. \<Turnstile> v : r" |
|
1440 shows "\<Turnstile> Stars vs : STAR r" |
|
1441 using assms |
|
1442 apply(induct vs) |
|
1443 apply(auto intro: CPrf.intros) |
|
1444 a |
|
1445 |
|
1446 lemma L_flat_CPrf: |
|
1447 assumes "s \<in> L r" |
|
1448 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
|
1449 using assms |
|
1450 apply(induct r arbitrary: s) |
|
1451 apply(auto simp add: Sequ_def intro: CPrf.intros) |
|
1452 using CPrf.intros(1) flat.simps(5) apply blast |
|
1453 using CPrf.intros(2) flat.simps(3) apply blast |
|
1454 using CPrf.intros(3) flat.simps(4) apply blast |
|
1455 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<Turnstile> v : r)") |
|
1456 apply(auto)[1] |
|
1457 apply(rule_tac x="Stars vs" in exI) |
|
1458 apply(simp) |
|
1459 (* HERE *) |
|
1460 apply (simp add: Prf_Stars) |
|
1461 apply(drule Star_string) |
|
1462 apply(auto) |
|
1463 apply(rule Star_val) |
|
1464 apply(auto) |
|
1465 done |
|
1466 *) |
|
1467 |
|
1468 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
1469 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
|
1470 |
|
1471 lemma val_ord_Posix: |
|
1472 assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)" |
|
1473 shows "s \<in> r \<rightarrow> v1" |
|
1474 using assms |
|
1475 apply(induct r arbitrary: s v1) |
|
1476 apply(auto simp add: CPT_def PT_def)[1] |
|
1477 apply(erule CPrf.cases) |
|
1478 apply(simp_all) |
|
1479 (* ONE *) |
|
1480 apply(auto simp add: CPT_def)[1] |
|
1481 apply(erule CPrf.cases) |
|
1482 apply(simp_all) |
|
1483 apply(rule Posix.intros) |
|
1484 (* CHAR *) |
|
1485 apply(auto simp add: CPT_def)[1] |
|
1486 apply(erule CPrf.cases) |
|
1487 apply(simp_all) |
|
1488 apply(rule Posix.intros) |
|
1489 prefer 2 |
|
1490 (* ALT *) |
|
1491 apply(auto simp add: CPT_def PT_def)[1] |
|
1492 apply(erule CPrf.cases) |
|
1493 apply(simp_all) |
|
1494 apply(rule Posix.intros) |
|
1495 apply(drule_tac x="flat v1a" in meta_spec) |
|
1496 apply(drule_tac x="v1a" in meta_spec) |
|
1497 apply(drule meta_mp) |
|
1498 apply(simp) |
|
1499 apply(drule meta_mp) |
|
1500 apply(auto)[1] |
|
1501 apply(drule_tac x="Left v2" in spec) |
|
1502 apply(simp) |
|
1503 apply(drule mp) |
|
1504 apply(rule Prf.intros) |
|
1505 apply(simp) |
|
1506 apply (meson val_ord_ALTI val_ord_ex_def) |
|
1507 apply(assumption) |
|
1508 (* ALT Right *) |
|
1509 apply(auto simp add: CPT_def)[1] |
|
1510 apply(rule Posix.intros) |
|
1511 apply(rotate_tac 1) |
|
1512 apply(drule_tac x="flat v2" in meta_spec) |
|
1513 apply(drule_tac x="v2" in meta_spec) |
|
1514 apply(drule meta_mp) |
|
1515 apply(simp) |
|
1516 apply(drule meta_mp) |
|
1517 apply(auto)[1] |
|
1518 apply(drule_tac x="Right v2a" in spec) |
|
1519 apply(simp) |
|
1520 apply(drule mp) |
|
1521 apply(rule Prf.intros) |
|
1522 apply(simp) |
|
1523 apply(subst (asm) (2) val_ord_ex_def) |
|
1524 apply(erule exE) |
|
1525 apply(drule val_ord_ALTI2) |
|
1526 apply(assumption) |
|
1527 apply(auto simp add: val_ord_ex_def)[1] |
|
1528 apply(assumption) |
|
1529 apply(auto)[1] |
|
1530 apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a") |
|
1531 apply(clarify) |
|
1532 apply(drule_tac x="Left v2'" in spec) |
|
1533 apply(simp) |
|
1534 apply(drule mp) |
|
1535 apply(rule Prf.intros) |
|
1536 apply(assumption) |
1437 apply(simp add: val_ord_ex_def) |
1537 apply(simp add: val_ord_ex_def) |
1438 apply(erule exE) |
1538 apply(subst (asm) (3) val_ord_def) |
1439 apply(simp add: val_ord_def) |
1539 apply(simp) |
1440 apply(auto simp add: pflat_len_simps)[1] |
|
1441 using Prf_CPrf Prf_elims(4) apply blast |
|
1442 (* CHAR *) |
|
1443 apply(auto)[1] |
|
1444 apply(simp add: CPT_def) |
|
1445 apply(simp add: val_ord_ex_def) |
|
1446 apply(clarify) |
|
1447 apply(erule CPrf.cases) |
|
1448 apply(simp_all) |
|
1449 apply(simp add: val_ord_def) |
|
1450 (* ALT *) |
|
1451 apply(auto)[1] |
|
1452 apply(simp add: CPT_def) |
|
1453 apply(clarify) |
|
1454 apply(erule CPrf.cases) |
|
1455 apply(simp_all) |
|
1456 apply(simp add: val_ord_ex_def) |
|
1457 apply(clarify) |
|
1458 apply(case_tac p) |
|
1459 apply(simp) |
|
1460 apply(simp add: val_ord_def) |
|
1461 apply(auto)[1] |
|
1462 apply(auto simp add: pflat_len_simps)[1] |
|
1463 using Posix1(2) apply auto[1] |
|
1464 apply(clarify) |
|
1465 using val_ord_ALTE apply blast |
|
1466 apply(simp add: val_ord_ex_def) |
|
1467 apply(clarify) |
|
1468 apply(simp add: val_ord_def) |
|
1469 apply(auto simp add: pflat_len_simps)[1] |
|
1470 using Posix1(2) apply auto[1] |
|
1471 apply (metis (mono_tags, lifting) One_nat_def Pos_empty Sulzmann.lexordp_simps(3) Un_iff inlen_bigger less_minus_one_simps(1) mem_Collect_eq not_less pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(7) zero_less_one) |
|
1472 (* ALT RIGHT case *) |
|
1473 apply(auto)[1] |
|
1474 apply(simp add: CPT_def) |
|
1475 apply(clarify) |
|
1476 apply(erule CPrf.cases) |
|
1477 apply(simp_all) |
|
1478 apply(simp add: val_ord_ex_def) |
|
1479 apply(clarify) |
|
1480 apply (simp add: L_flat_Prf1 Prf_CPrf) |
|
1481 apply(simp add: val_ord_ex_def) |
|
1482 apply(clarify) |
|
1483 apply(case_tac p) |
|
1484 apply (simp add: Posix1(2) pflat_len_simps(7) val_ord_def) |
|
1485 using val_ord_ALTE2 apply blast |
|
1486 (* SEQ case *) |
|
1487 apply(clarify) |
|
1488 apply(simp add: CPT_def) |
|
1489 apply(clarify) |
|
1490 apply(erule CPrf.cases) |
|
1491 apply(simp_all) |
|
1492 apply(drule_tac r="r1a" in val_ord_SEQ) |
|
1493 apply(simp) |
|
1494 using Posix1(2) apply auto[1] |
|
1495 apply (simp add: Prf_CPrf) |
|
1496 apply (simp add: Posix1a) |
|
1497 apply(auto)[1] |
|
1498 apply(subgoal_tac "length (flat v1a) \<le> length s1") |
|
1499 prefer 2 |
|
1500 apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_eq_conv_conj drop_eq_Nil) |
|
1501 apply(subst (asm) append_eq_append_conv_if) |
|
1502 apply(simp) |
|
1503 apply (metis (mono_tags, lifting) CPT_def Posix_CPT le_less_linear mem_Collect_eq take_all val_ord_ex_trans val_ord_shorterI) |
|
1504 using Posix1(2) apply auto[1] |
|
1505 (* STAR case *) |
|
1506 apply(clarify) |
|
1507 apply(simp add: CPT_def) |
|
1508 apply(clarify) |
|
1509 apply(erule CPrf.cases) |
|
1510 apply(simp_all) |
|
1511 apply (simp add: Posix1(2)) |
|
1512 apply(subgoal_tac "length (flat va) \<le> length s1") |
|
1513 prefer 2 |
|
1514 apply (metis L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_eq_conv_conj drop_eq_Nil flat_Stars) |
|
1515 apply(subst (asm) append_eq_append_conv_if) |
|
1516 apply(simp) |
|
1517 (* HERE *) |
|
1518 apply(case_tac "flat va = s1") |
|
1519 prefer 2 |
|
1520 apply(subgoal_tac "v :\<sqsubset>val va") |
|
1521 prefer 2 |
|
1522 apply (metis Posix1(2) le_less_linear take_all val_ord_shorterI) |
|
1523 apply(rotate_tac 3) |
|
1524 apply(simp add: val_ord_ex_def) |
|
1525 apply(clarify) |
|
1526 apply(case_tac p) |
|
1527 apply(simp add: val_ord_def pflat_len_simps) |
|
1528 apply (smt Posix1(2) append_take_drop_id flat_Stars intlen_append) |
|
1529 apply(simp) |
|
1530 prefer 2 |
|
1531 apply(simp) |
|
1532 apply(drule_tac x="va" in spec) |
|
1533 apply(simp) |
|
1534 apply(subst (asm) (2) val_ord_ex_def) |
|
1535 apply(subst (asm) (2) val_ord_ex_def) |
|
1536 apply(clarify) |
|
1537 apply(simp) |
|
1538 apply(drule_tac x="Stars vsa" in spec) |
|
1539 apply(simp) |
|
1540 apply(case_tac p) |
|
1541 apply(simp) |
|
1542 apply (metis Posix1(2) flat.simps(7) flat_Stars less_irrefl pflat_len_simps(7) val_ord_def) |
|
1543 apply(clarify) |
|
1544 apply(case_tac a) |
|
1545 apply(simp) |
|
1546 apply(subst (asm) val_ord_ex_def) |
|
1547 apply(simp) |
|
1548 apply(subst (asm) (2) val_ord_def) |
|
1549 apply(clarify) |
|
1550 apply(simp add: pflat_len_Stars_simps) |
|
1551 apply(simp add: pflat_len_simps) |
1540 apply(simp add: pflat_len_simps) |
1552 prefer 3 |
1541 apply(drule_tac x="[0]" in spec) |
1553 proof - |
1542 apply(simp add: pflat_len_simps Pos_empty) |
1554 fix s1 :: "char list" and v :: val and s2 :: "char list" and vs :: "val list" and va :: val and ra :: rexp and vsa :: "val list" and p :: "nat list" and pa :: "nat list" and a :: nat and list :: "nat list" |
1543 apply(drule mp) |
1555 assume a1: "length (flat va) \<le> length s1" |
1544 apply (smt inlen_bigger) |
1556 assume a2: "s1 \<in> ra \<rightarrow> v" |
1545 apply(erule disjE) |
1557 assume a3: "s2 \<in> STAR ra \<rightarrow> Stars vs" |
1546 apply blast |
1558 assume a4: "Stars (va # vsa) \<sqsubset>val a # list Stars (v # vs)" |
1547 apply auto[1] |
1559 assume a5: "v \<sqsubset>val pa va" |
1548 apply (meson L_flat_Prf2) |
1560 assume a6: "flat va = take (length (flat va)) s1" |
1549 (* SEQ *) |
1561 assume a7: "concat (map flat vsa) = drop (length (flat va)) s1 @ s2" |
1550 apply(auto simp add: CPT_def)[1] |
1562 assume "p = a # list" |
1551 apply(erule CPrf.cases) |
1563 obtain nns :: "val \<Rightarrow> val \<Rightarrow> nat list" where |
1552 apply(simp_all) |
1564 f8: "(\<forall>v va. \<not> v :\<sqsubset>val va \<or> v \<sqsubset>val nns v va va) \<and> (\<forall>v va. (\<forall>ns. \<not> v \<sqsubset>val ns va) \<or> v :\<sqsubset>val va)" |
1553 apply(rule Posix.intros) |
1565 using val_ord_ex_def by moura |
1554 apply(drule_tac x="flat v1a" in meta_spec) |
1566 then have "Stars (v # vs) :\<sqsubset>val Stars (va # vsa)" |
1555 apply(drule_tac x="v1a" in meta_spec) |
1567 using a7 a6 a5 a3 a2 a1 by (metis Posix1(2) append_eq_append_conv_if flat.simps(7) flat_Stars val_ord_STARI) |
1556 apply(drule meta_mp) |
1568 then show False |
1557 apply(simp) |
1569 using f8 a4 by (meson less_irrefl val_ord_def val_ord_ex_trans) |
1558 apply(drule meta_mp) |
1570 next |
1559 apply(auto)[1] |
1571 fix v :: val and vs :: "val list" and va :: val and ra :: rexp and vsa :: "val list" and list :: "nat list" |
1560 apply(auto simp add: PT_def)[1] |
1572 assume a1: "intlen (flat va @ concat (map flat vsa)) = intlen (flat v @ concat (map flat vs)) \<and> (\<forall>q\<in>{0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)} \<union> ({0 # ps |ps. ps \<in> Pos v} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vs)}). q \<sqsubset>lex 0 # list \<longrightarrow> pflat_len (Stars (va # vsa)) q = pflat_len (Stars (v # vs)) q)" |
1561 apply(drule_tac x="Seq v2a v2" in spec) |
1573 assume a2: "pflat_len v list < pflat_len va list" |
1562 apply(simp) |
1574 assume a3: "list \<in> Pos va" |
1563 apply(drule mp) |
1575 assume a4: "\<forall>p. \<not> va \<sqsubset>val p v" |
1564 apply (simp add: Prf.intros(1) Prf_CPrf) |
1576 have f5: "\<And>ns. pflat_len (Stars (v # vs)) ns = pflat_len (Stars (va # vsa)) ns \<or> \<not> ns \<sqsubset>lex 0 # list \<or> (\<forall>nsa. ns \<noteq> 0 # nsa \<or> nsa \<notin> Pos v)" |
1565 using val_ord_SEQI val_ord_ex_def apply fastforce |
1577 using a1 by fastforce |
1566 apply(assumption) |
1578 have "\<And>ns. pflat_len (Stars (v # vs)) ns = pflat_len (Stars (va # vsa)) ns \<or> \<not> ns \<sqsubset>lex 0 # list \<or> (\<forall>nsa. ns \<noteq> 0 # nsa \<or> nsa \<notin> Pos va)" |
1567 apply(rotate_tac 1) |
1579 using a1 by fastforce |
1568 apply(drule_tac x="flat v2" in meta_spec) |
1580 then show False |
1569 apply(drule_tac x="v2" in meta_spec) |
1581 using f5 a4 a3 a2 by (metis (no_types) Sulzmann.lexordp_simps(3) Un_iff pflat_len_Stars_simps2(2) val_ord_def) |
1570 apply(simp) |
1582 next |
1571 apply(auto)[1] |
1583 fix v abd vs and va and ra and vsa and p a and list and nat |
1572 apply(drule meta_mp) |
1584 assume "flat va \<in> ra \<rightarrow> v" |
1573 apply(auto)[1] |
1585 "concat (map flat vsa) \<in> STAR ra \<rightarrow> Stars vs" "flat v \<noteq> []" |
1574 apply(auto simp add: PT_def)[1] |
1586 "\<forall>s\<^sub>3. flat va @ s\<^sub>3 \<in> L ra \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s\<^sub>3 @ s\<^sub>4 = concat (map flat vsa) \<longrightarrow> s\<^sub>4 \<notin> L ra\<star>)" |
1575 apply(drule_tac x="Seq v1a v2a" in spec) |
1587 "\<Turnstile> va : ra" "flat va \<noteq> []" |
1576 apply(simp) |
1588 "\<Turnstile> Stars vsa : STAR ra" |
1577 apply(drule mp) |
1589 "\<forall>p. \<not> va \<sqsubset>val p v" "Stars (va # vsa) \<sqsubset>val a # list Stars (v # vs)" |
1578 apply (simp add: Prf.intros(1) Prf_CPrf) |
1590 "\<not> Stars vsa :\<sqsubset>val Stars vs" "a = Suc nat" |
1579 apply (meson val_ord_SEQI2 val_ord_ex_def) |
1591 then show "False" |
1580 apply(assumption) |
1592 apply - |
1581 (* SEQ side condition *) |
1593 apply(subst (asm) val_ord_ex_def) |
1582 apply(auto simp add: PT_def) |
1594 apply(simp) |
1583 apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a") |
1595 apply(drule STAR_val_ord) |
1584 prefer 2 |
1596 using Posix1(2) apply auto[1] |
1585 apply (meson L_flat_Prf2) |
1597 apply blast |
1586 apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a") |
1598 done |
1587 prefer 2 |
1599 next |
1588 apply (meson L_flat_Prf2) |
1600 fix r |
1589 apply(clarify) |
1601 show " \<forall>v2\<in>CPT (STAR r) []. \<not> v2 :\<sqsubset>val Stars []" |
1590 apply(drule_tac x="Seq vA vB" in spec) |
1602 apply - |
1591 apply(simp) |
1603 apply(rule ballI) |
1592 apply(drule mp) |
1604 apply(simp add: CPT_def) |
1593 apply (simp add: Prf.intros(1)) |
1605 apply(auto) |
1594 apply(subst (asm) (3) val_ord_ex_def) |
1606 apply(erule CPrf.cases) |
1595 apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SEQI val_ord_ex_def val_ord_shorterI) |
1607 apply(simp_all) |
1596 (* STAR *) |
1608 apply(simp add: val_ord_ex_def) |
|
1609 apply(clarify) |
|
1610 apply(simp add: val_ord_def) |
|
1611 done |
|
1612 qed |
|
1613 |
1597 |
1614 |
1598 |
1615 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" |
1599 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" |
1616 where |
1600 where |
1617 "Minval r s v \<equiv> \<Turnstile> v : r \<and> flat v = s \<and> (\<forall>v' \<in> CPT r s. v :\<sqsubset>val v' \<or> v = v')" |
1601 "Minval r s v \<equiv> \<Turnstile> v : r \<and> flat v = s \<and> (\<forall>v' \<in> CPT r s. v :\<sqsubset>val v' \<or> v = v')" |