1432 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1445 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
1433 using assms |
1446 using assms |
1434 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
1447 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
1435 val_ord_ex1_def val_ord_ex_def val_ord_ex_trans) |
1448 val_ord_ex1_def val_ord_ex_def val_ord_ex_trans) |
1436 |
1449 |
1437 (* |
1450 thm Posix.intros(6) |
1438 lemma CPrf_Stars: |
1451 |
1439 assumes "\<forall>v \<in> set vs. \<Turnstile> v : r" |
1452 inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool" |
1440 shows "\<Turnstile> Stars vs : STAR r" |
1453 where |
1441 using assms |
1454 "Prop r []" |
1442 apply(induct vs) |
1455 | "\<lbrakk>Prop r vs; |
1443 apply(auto intro: CPrf.intros) |
1456 \<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
1444 a |
1457 \<Longrightarrow> Prop r (v # vs)" |
1445 |
1458 |
1446 lemma L_flat_CPrf: |
1459 lemma STAR_val_ord_ex: |
1447 assumes "s \<in> L r" |
1460 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
1448 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
1461 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
1449 using assms |
1462 using assms |
1450 apply(induct r arbitrary: s) |
1463 apply(subst (asm) val_ord_ex_def) |
1451 apply(auto simp add: Sequ_def intro: CPrf.intros) |
1464 apply(erule exE) |
1452 using CPrf.intros(1) flat.simps(5) apply blast |
1465 apply(case_tac p) |
1453 using CPrf.intros(2) flat.simps(3) apply blast |
1466 apply(simp) |
1454 using CPrf.intros(3) flat.simps(4) apply blast |
1467 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
1455 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<Turnstile> v : r)") |
1468 apply(subst val_ord_ex_def) |
1456 apply(auto)[1] |
1469 apply(rule_tac x="[]" in exI) |
1457 apply(rule_tac x="Stars vs" in exI) |
1470 apply(simp add: val_ord_def pflat_len_simps Pos_empty) |
1458 apply(simp) |
1471 apply(simp) |
1459 (* HERE *) |
1472 apply(case_tac a) |
1460 apply (simp add: Prf_Stars) |
1473 apply(clarify) |
1461 apply(drule Star_string) |
1474 prefer 2 |
1462 apply(auto) |
1475 using STAR_val_ord val_ord_ex_def apply blast |
1463 apply(rule Star_val) |
1476 apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1] |
1464 apply(auto) |
1477 done |
1465 done |
1478 |
1466 *) |
1479 lemma STAR_val_ord_exI: |
|
1480 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
|
1481 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
1482 using assms |
|
1483 apply(induct vs) |
|
1484 apply(simp) |
|
1485 apply(simp) |
|
1486 apply(simp add: val_ord_ex_def) |
|
1487 apply(erule exE) |
|
1488 apply(case_tac p) |
|
1489 apply(simp) |
|
1490 apply(rule_tac x="[]" in exI) |
|
1491 apply(simp add: val_ord_def) |
|
1492 apply(auto simp add: pflat_len_simps intlen_append)[1] |
|
1493 apply(simp) |
|
1494 apply(rule_tac x="Suc aa#list" in exI) |
|
1495 apply(rule val_ord_STARI2) |
|
1496 apply(simp) |
|
1497 apply(simp) |
|
1498 done |
|
1499 |
|
1500 lemma STAR_val_ord_ex_append: |
|
1501 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
1502 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
1503 using assms |
|
1504 apply(induct vs) |
|
1505 apply(simp) |
|
1506 apply(simp) |
|
1507 apply(drule STAR_val_ord_ex) |
|
1508 apply(simp) |
|
1509 done |
|
1510 |
|
1511 lemma STAR_val_ord_ex_append_eq: |
|
1512 assumes "flat (Stars vs1) = flat (Stars vs2)" |
|
1513 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
1514 using assms |
|
1515 apply(rule_tac iffI) |
|
1516 apply(erule STAR_val_ord_ex_append) |
|
1517 apply(rule STAR_val_ord_exI) |
|
1518 apply(auto) |
|
1519 done |
|
1520 |
|
1521 lemma Posix_STARI: |
|
1522 assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs" |
|
1523 shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
1524 using assms |
|
1525 apply(induct vs arbitrary: r) |
|
1526 apply(simp) |
|
1527 apply(rule Posix.intros) |
|
1528 apply(simp) |
|
1529 apply(rule Posix.intros) |
|
1530 apply(simp) |
|
1531 apply(auto)[1] |
|
1532 apply(erule Prop.cases) |
|
1533 apply(simp) |
|
1534 apply(simp) |
|
1535 apply(simp) |
|
1536 apply(erule Prop.cases) |
|
1537 apply(simp) |
|
1538 apply(auto)[1] |
|
1539 done |
|
1540 |
|
1541 lemma CPrf_stars: |
|
1542 assumes "\<Turnstile> Stars vs : STAR r" |
|
1543 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
1544 using assms |
|
1545 apply(induct vs) |
|
1546 apply(auto) |
|
1547 apply(erule CPrf.cases) |
|
1548 apply(simp_all) |
|
1549 apply(erule CPrf.cases) |
|
1550 apply(simp_all) |
|
1551 apply(erule CPrf.cases) |
|
1552 apply(simp_all) |
|
1553 apply(erule CPrf.cases) |
|
1554 apply(simp_all) |
|
1555 done |
1467 |
1556 |
1468 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
1557 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
1469 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
1558 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
|
1559 |
|
1560 lemma exists: |
|
1561 assumes "s \<in> (L r)\<star>" |
|
1562 shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r" |
|
1563 using assms |
|
1564 apply(drule_tac Star_string) |
|
1565 apply(auto) |
|
1566 by (metis L_flat_Prf2 Prf_Stars Star_val) |
|
1567 |
|
1568 |
|
1569 lemma val_ord_Posix_Stars: |
|
1570 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
|
1571 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
|
1572 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
|
1573 using assms |
|
1574 apply(induct vs) |
|
1575 apply(simp) |
|
1576 apply(rule Posix.intros) |
|
1577 apply(simp (no_asm)) |
|
1578 apply(rule Posix.intros) |
|
1579 apply(auto)[1] |
|
1580 apply(auto simp add: CPT_def PT_def)[1] |
|
1581 defer |
|
1582 apply(simp) |
|
1583 apply(drule meta_mp) |
|
1584 apply(auto simp add: CPT_def PT_def)[1] |
|
1585 apply(erule CPrf.cases) |
|
1586 apply(simp_all) |
|
1587 apply(drule meta_mp) |
|
1588 apply(auto simp add: CPT_def PT_def)[1] |
|
1589 apply(erule Prf.cases) |
|
1590 apply(simp_all) |
|
1591 apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25)) |
|
1592 apply(clarify) |
|
1593 apply(drule_tac x="Stars (a#v#vsa)" in spec) |
|
1594 apply(simp) |
|
1595 apply(drule mp) |
|
1596 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
|
1597 apply(subst (asm) (2) val_ord_ex_def) |
|
1598 apply(simp) |
|
1599 apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def) |
|
1600 apply(auto simp add: CPT_def PT_def)[1] |
|
1601 using CPrf_stars apply auto[1] |
|
1602 apply(auto)[1] |
|
1603 apply(auto simp add: CPT_def PT_def)[1] |
|
1604 apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r") |
|
1605 prefer 2 |
|
1606 apply (meson L_flat_Prf2) |
|
1607 apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)") |
|
1608 apply(clarify) |
|
1609 apply(drule_tac x="Stars (vA # vB)" in spec) |
|
1610 apply(simp) |
|
1611 apply(drule mp) |
|
1612 using Prf.intros(7) apply blast |
|
1613 apply(subst (asm) (2) val_ord_ex_def) |
|
1614 apply(simp) |
|
1615 prefer 2 |
|
1616 apply(simp) |
|
1617 using exists apply blast |
|
1618 prefer 2 |
|
1619 apply(drule meta_mp) |
|
1620 apply(erule CPrf.cases) |
|
1621 apply(simp_all) |
|
1622 apply(drule meta_mp) |
|
1623 apply(auto)[1] |
|
1624 prefer 2 |
|
1625 apply(simp) |
|
1626 apply(erule CPrf.cases) |
|
1627 apply(simp_all) |
|
1628 apply(clarify) |
|
1629 apply(rotate_tac 3) |
|
1630 apply(erule Prf.cases) |
|
1631 apply(simp_all) |
|
1632 apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def) |
|
1633 apply(drule_tac x="Stars (v#va#vsb)" in spec) |
|
1634 apply(drule mp) |
|
1635 apply (simp add: Posix1a Prf.intros(7)) |
|
1636 apply(simp) |
|
1637 apply(subst (asm) (2) val_ord_ex_def) |
|
1638 apply(simp) |
|
1639 apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def) |
|
1640 proof - |
|
1641 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
|
1642 assume a1: "s\<^sub>3 \<noteq> []" |
|
1643 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
|
1644 assume a3: "flat vA = flat a @ s\<^sub>3" |
|
1645 assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)" |
|
1646 have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs" |
|
1647 by (meson drop_eq_Nil not_less) |
|
1648 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
|
1649 using a3 a1 by simp |
|
1650 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
|
1651 using a3 a2 by simp |
|
1652 then show False |
|
1653 using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_STARI val_ord_ex_def val_ord_shorterI) |
|
1654 qed |
|
1655 |
|
1656 lemma Prf_Stars_append: |
|
1657 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
|
1658 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
|
1659 using assms |
|
1660 apply(induct vs1 arbitrary: vs2) |
|
1661 apply(auto intro: Prf.intros) |
|
1662 apply(erule Prf.cases) |
|
1663 apply(simp_all) |
|
1664 apply(auto intro: Prf.intros) |
|
1665 done |
|
1666 |
|
1667 lemma CPrf_Stars_appendE: |
|
1668 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
1669 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
1670 using assms |
|
1671 apply(induct vs1 arbitrary: vs2) |
|
1672 apply(auto intro: CPrf.intros)[1] |
|
1673 apply(erule CPrf.cases) |
|
1674 apply(simp_all) |
|
1675 apply(auto intro: CPrf.intros) |
|
1676 done |
1470 |
1677 |
1471 lemma val_ord_Posix: |
1678 lemma val_ord_Posix: |
1472 assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)" |
1679 assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)" |
1473 shows "s \<in> r \<rightarrow> v1" |
1680 shows "s \<in> r \<rightarrow> v1" |
1474 using assms |
1681 using assms |
1592 apply(drule mp) |
1799 apply(drule mp) |
1593 apply (simp add: Prf.intros(1)) |
1800 apply (simp add: Prf.intros(1)) |
1594 apply(subst (asm) (3) val_ord_ex_def) |
1801 apply(subst (asm) (3) val_ord_ex_def) |
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) |
1802 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) |
1596 (* STAR *) |
1803 (* STAR *) |
1597 |
1804 apply(auto simp add: CPT_def)[1] |
1598 |
1805 apply(erule CPrf.cases) |
1599 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" |
1806 apply(simp_all)[6] |
1600 where |
1807 using Posix_STAR2 apply blast |
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')" |
1808 apply(clarify) |
1602 |
1809 apply(rule val_ord_Posix_Stars) |
1603 lemma |
1810 apply(auto simp add: CPT_def)[1] |
1604 assumes "s \<in> L(r)" |
1811 apply (simp add: CPrf.intros(7)) |
1605 shows "\<exists>v. Minval r s v" |
1812 apply(auto)[1] |
1606 using assms |
1813 apply(drule_tac x="flat v" in meta_spec) |
1607 apply(induct r arbitrary: s) |
1814 apply(drule_tac x="v" in meta_spec) |
1608 apply(simp) |
1815 apply(simp) |
1609 apply(simp) |
1816 apply(drule meta_mp) |
1610 apply(rule_tac x="Void" in exI) |
1817 apply(auto)[1] |
1611 apply(simp add: Minval_def) |
1818 apply(drule_tac x="Stars (v2#vs)" in spec) |
1612 apply(rule conjI) |
1819 apply(simp) |
1613 apply (simp add: CPrf.intros(4)) |
1820 apply(drule mp) |
1614 apply(clarify) |
1821 using Prf.intros(7) Prf_CPrf apply blast |
1615 apply(simp add: CPT_def) |
1822 apply(subst (asm) (2) val_ord_ex_def) |
1616 apply(auto)[1] |
1823 apply(simp) |
1617 apply(erule CPrf.cases) |
1824 using val_ord_STARI val_ord_ex_def apply fastforce |
1618 apply(simp_all) |
1825 apply(assumption) |
1619 apply(rule_tac x="Char x" in exI) |
1826 apply(drule_tac x="flat va" in meta_spec) |
1620 apply(simp add: Minval_def) |
1827 apply(drule_tac x="va" in meta_spec) |
1621 apply(rule conjI) |
1828 apply(simp) |
1622 apply (simp add: CPrf.intros) |
1829 apply(drule meta_mp) |
1623 apply(clarify) |
1830 using CPrf_stars apply blast |
1624 apply(simp add: CPT_def) |
1831 apply(drule meta_mp) |
1625 apply(auto)[1] |
1832 apply(auto)[1] |
1626 apply(erule CPrf.cases) |
1833 apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post") |
1627 apply(simp_all) |
1834 prefer 2 |
1628 prefer 2 |
1835 apply (metis append_Cons append_Nil in_set_conv_decomp_first) |
1629 apply(auto)[1] |
1836 apply(clarify) |
1630 apply(drule_tac x="s" in meta_spec) |
1837 apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec) |
1631 apply(simp) |
1838 apply(simp) |
1632 apply(clarify) |
1839 apply(drule mp) |
1633 apply(rule_tac x="Left x" in exI) |
1840 apply(rule Prf.intros) |
1634 apply(simp (no_asm) add: Minval_def) |
1841 apply (simp add: Prf_CPrf) |
1635 apply(rule conjI) |
1842 apply(rule Prf_Stars_append) |
1636 apply (simp add: CPrf.intros(2) Minval_def) |
1843 apply(drule CPrf_Stars_appendE) |
1637 apply(rule conjI) |
1844 apply(auto simp add: Prf_CPrf)[1] |
1638 apply(simp add: Minval_def) |
1845 apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD) |
1639 apply(clarify) |
1846 apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)") |
1640 apply(simp add: CPT_def) |
1847 apply(subst (asm) STAR_val_ord_ex_append_eq) |
1641 apply(auto)[1] |
1848 apply(simp) |
1642 apply(erule CPrf.cases) |
1849 apply(subst (asm) STAR_val_ord_ex_append_eq) |
1643 apply(simp_all) |
1850 apply(simp) |
|
1851 prefer 2 |
|
1852 apply(simp) |
|
1853 prefer 2 |
|
1854 apply(simp) |
1644 apply(simp add: val_ord_ex_def) |
1855 apply(simp add: val_ord_ex_def) |
1645 apply(simp only: val_ord_def) |
1856 apply(erule exE) |
1646 oops |
1857 apply(rotate_tac 6) |
1647 |
1858 apply(drule_tac x="0#p" in spec) |
1648 lemma |
1859 apply (simp add: val_ord_STARI) |
1649 "wf {(v1, v2). v1 \<in> CPT r s \<and> v2 \<in> CPT r s \<and> (v1 :\<sqsubset>val v2)}" |
1860 apply(auto simp add: PT_def) |
1650 apply(rule wfI) |
1861 done |
1651 oops |
|
1652 |
1862 |
1653 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
1863 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
1654 where |
1864 where |
1655 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
1865 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
1656 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |
1866 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |
1681 apply(rule ValOrd.intros) |
1893 apply(rule ValOrd.intros) |
1682 apply(rule ValOrd.intros) |
1894 apply(rule ValOrd.intros) |
1683 apply(rule ValOrd.intros) |
1895 apply(rule ValOrd.intros) |
1684 apply(simp) |
1896 apply(simp) |
1685 done |
1897 done |
|
1898 *) |
|
1899 |
|
1900 lemma ValOrd_irrefl: |
|
1901 assumes "\<turnstile> v : r" "v \<preceq>r v" |
|
1902 shows "False" |
|
1903 using assms |
|
1904 apply(induct v r rule: Prf.induct) |
|
1905 apply(erule ValOrd.cases) |
|
1906 apply(simp_all) |
|
1907 apply(erule ValOrd.cases) |
|
1908 apply(simp_all) |
|
1909 apply(erule ValOrd.cases) |
|
1910 apply(simp_all) |
|
1911 apply(erule ValOrd.cases) |
|
1912 apply(simp_all) |
|
1913 apply(erule ValOrd.cases) |
|
1914 apply(simp_all) |
|
1915 apply(erule ValOrd.cases) |
|
1916 apply(simp_all) |
|
1917 apply(erule ValOrd.cases) |
|
1918 apply(simp_all) |
|
1919 done |
|
1920 |
|
1921 lemma prefix_sprefix: |
|
1922 shows "xs \<sqsubseteq>pre ys \<longleftrightarrow> (xs = ys \<or> xs \<sqsubset>spre ys)" |
|
1923 apply(auto simp add: sprefix_list_def prefix_list_def) |
|
1924 done |
|
1925 |
|
1926 |
1686 |
1927 |
1687 lemma Posix_CPT2: |
1928 lemma Posix_CPT2: |
1688 assumes "v1 \<preceq>r v2" "flat v1 = flat v2" |
1929 assumes "v1 \<preceq>r v2" "flat v2 \<sqsubseteq>pre flat v1" |
1689 shows "v2 :\<sqsubset>val v1 \<or> v1 = v2" |
1930 shows "v1 :\<sqsubset>val v2" |
1690 using assms |
1931 using assms |
1691 apply(induct r arbitrary: v1 v2 rule: rexp.induct) |
1932 apply(induct v1 r v2 arbitrary: rule: ValOrd.induct) |
|
1933 prefer 3 |
|
1934 apply(simp) |
|
1935 apply(auto simp add: prefix_sprefix)[1] |
|
1936 apply(rule val_ord_spre) |
|
1937 apply(simp) |
|
1938 prefer 3 |
|
1939 apply(simp) |
|
1940 apply(auto simp add: prefix_sprefix)[1] |
|
1941 apply(auto simp add: val_ord_ex_def)[1] |
|
1942 apply(rule_tac x="[0]" in exI) |
|
1943 apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1] |
|
1944 apply (smt inlen_bigger) |
|
1945 apply(rule val_ord_spre) |
|
1946 apply(simp) |
|
1947 prefer 3 |
|
1948 apply(simp) |
|
1949 apply(auto simp add: prefix_sprefix)[1] |
|
1950 using val_ord_ALTI2 val_ord_ex_def apply fastforce |
|
1951 apply(rule val_ord_spre) |
|
1952 apply(simp) |
|
1953 prefer 3 |
|
1954 apply(simp) |
|
1955 apply(auto simp add: prefix_sprefix)[1] |
|
1956 using val_ord_ALTI val_ord_ex_def apply fastforce |
|
1957 apply(rule val_ord_spre) |
|
1958 apply(simp) |
|
1959 (* SEQ case *) |
|
1960 apply(simp) |
|
1961 apply(auto simp add: prefix_sprefix)[1] |
|
1962 apply(auto simp add: append_eq_append_conv2)[1] |
|
1963 apply(case_tac "us = []") |
|
1964 apply(simp) |
|
1965 apply(auto simp add: val_ord_ex1_def)[1] |
|
1966 apply (metis flat.simps(5) val_ord_SEQI val_ord_ex_def) |
|
1967 apply(simp) |
|
1968 prefer 2 |
|
1969 apply(case_tac "us = []") |
|
1970 apply(simp) |
|
1971 apply (metis flat.simps(5) val_ord_SEQI val_ord_ex_def) |
|
1972 apply(drule meta_mp) |
|
1973 apply(rule disjI2) |
|
1974 apply (metis append_self_conv prefix_list_def sprefix_list_def) |
|
1975 apply(auto simp add: val_ord_ex_def)[1] |
|
1976 apply (metis append_assoc flat.simps(5) val_ord_SEQI) |
|
1977 |
|
1978 apply(sugoal_ tac "") |
|
1979 thm val_ord_SEQI |
|
1980 apply(rule val_ord_SEQI) |
|
1981 thm val_ord_SEQI |
|
1982 prefer 2 |
|
1983 apply(case_tac "us |
|
1984 apply(case_tac "v1 = v1'") |
|
1985 apply(simp) |
|
1986 |
|
1987 apply(auto simp add: val_ord_ex1_def)[1] |
|
1988 apply(auto simp add: val_ord_ex_def)[1] |
|
1989 apply(rule_tac x="[0]" in exI) |
|
1990 |
|
1991 prefer 2 |
|
1992 apply(rule val_ord_spre) |
|
1993 apply(simp) |
|
1994 prefer 3 |
|
1995 apply(simp) |
|
1996 using val_ord_ex1_def val_ord_spre apply auto[1] |
|
1997 |
|
1998 apply(erule disjE) |
|
1999 prefer 2 |
|
2000 apply(subst val_ord_ex1_def) |
|
2001 apply(rule disjI1) |
|
2002 apply(rule val_ord_spre) |
|
2003 apply(simp) |
|
2004 apply(simp) |
|
2005 apply(simp add: append_eq_append_conv2) |
|
2006 apply(auto)[1] |
|
2007 apply(case_tac "us = []") |
|
2008 apply(simp) |
|
2009 apply(drule meta_mp) |
|
2010 apply(auto simp add: prefix_sprefix)[1] |
|
2011 apply(subst (asm) val_ord_ex1_def) |
|
2012 apply(erule disjE) |
|
2013 apply(subst val_ord_ex1_def) |
|
2014 apply(rule disjI1) |
|
2015 apply (metis flat.simps(5) val_ord_SEQI val_ord_ex_def) |
|
2016 apply(clarify) |
|
2017 prefer 2 |
|
2018 apply(subgoal_tac "flat v1' \<sqsubset>spre flat v1") |
|
2019 prefer 2 |
|
2020 apply (simp add: prefix_list_def sprefix_list_def) |
|
2021 apply(drule val_ord_spre) |
|
2022 apply(auto)[1] |
|
2023 apply(rule val_ord_sprefixI) |
1692 apply(erule ValOrd.cases) |
2024 apply(erule ValOrd.cases) |
1693 apply(simp_all) |
2025 apply(simp_all) |
1694 apply(erule ValOrd.cases) |
2026 apply(erule ValOrd.cases) |
1695 apply(simp_all) |
2027 apply(simp_all) |
1696 apply(erule ValOrd.cases) |
2028 apply(erule ValOrd.cases) |