1575 lemma rtree_RAGs: "rtree (RAG s)"

  1600 lemma readys_th: "th \<in> readys s'"

  1601 proof -

  1602     from step_back_step [OF vt_s[unfolded s_def]]

  1603     have "PIP s' (P th cs)" .

  1604     hence "th \<in> runing s'" by (cases, simp)

  1605     thus ?thesis by (simp add:readys_def runing_def)

  1606 qed

  1607 

  1608 lemma root_th: "root (RAG s') (Th th)"

  1609   using readys_root[OF vat_s'.vt readys_th] .

  1610 

  1611 lemma in_no_others_subtree:

  1612   assumes "th' \<noteq> th"

  1613   shows "Th th \<notin> subtree (RAG s') (Th th')"

  1577   show "single_valued (RAG s)"

  1615   assume "Th th \<in> subtree (RAG s') (Th th')"

  1578   apply (intro_locales)

  1616   thus False

  1579     by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])

  1617   proof(cases rule:subtreeE)

  1580 

  1618     case 1

  1581   show "acyclic (RAG s)"

  1619     with assms show ?thesis by auto

  1582      by (rule acyclic_RAG[OF vt_s])

  1620   next

  1583 qed

  1621     case 2

  1584 

  1622     with root_th show ?thesis by (auto simp:root_def)

  1585 lemma rtree_RAGs': "rtree (RAG s')"

  1623   qed

  1586 proof

  1587   show "single_valued (RAG s')"

  1588   apply (intro_locales)

  1589     by (unfold single_valued_def, 

  1590         auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])

  1591 

  1592   show "acyclic (RAG s')"

  1593      by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])

  1618 lemma child_kept_left:

  1648 lemma subtree_kept:

  1619   assumes 

  1649   assumes "th' \<noteq> th"

  1620   "(n1, n2) \<in> (child s')^+"

  1650   shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')"

  1621   shows "(n1, n2) \<in> (child s)^+"

  1651 proof(unfold RAG_s, rule subtree_insert_next)

  1622 proof -

  1652   from in_no_others_subtree[OF assms] 

  1623   from assms show ?thesis 

  1653   show "Th th \<notin> subtree (RAG s') (Th th')" .

  1624   proof(induct rule: converse_trancl_induct)

  1654 qed

  1625     case (base y)

  1655 

  1626     from base obtain th1 cs1 th2

  1656 lemma cp_kept: 

  1627       where h1: "(Th th1, Cs cs1) \<in> RAG s'"

  1657   assumes "th' \<noteq> th"

  1628       and h2: "(Cs cs1, Th th2) \<in> RAG s'"

  1629       and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)

  1630     have "cs1 \<noteq> cs"

  1631     proof

  1632       assume eq_cs: "cs1 = cs"

  1633       with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp

  1634       with ee show False

  1635         by (auto simp:s_RAG_def cs_waiting_def)

  1636     qed

  1637     with h1 h2 RAG_s have 

  1638       h1': "(Th th1, Cs cs1) \<in> RAG s" and

  1639       h2': "(Cs cs1, Th th2) \<in> RAG s" by auto

  1640     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)

  1641     with eq_y eq_n2 have "(y, n2) \<in> child s" by simp

  1642     thus ?case by auto

  1643   next

  1644     case (step y z)

  1645     have "(y, z) \<in> child s'" by fact

  1646     then obtain th1 cs1 th2

  1647       where h1: "(Th th1, Cs cs1) \<in> RAG s'"

  1648       and h2: "(Cs cs1, Th th2) \<in> RAG s'"

  1649       and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)

  1650     have "cs1 \<noteq> cs"

  1651     proof

  1652       assume eq_cs: "cs1 = cs"

  1653       with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp

  1654       with ee show False 

  1655         by (auto simp:s_RAG_def cs_waiting_def)

  1656     qed

  1657     with h1 h2 RAG_s have 

  1658       h1': "(Th th1, Cs cs1) \<in> RAG s" and

  1659       h2': "(Cs cs1, Th th2) \<in> RAG s" by auto

  1660     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)

  1661     with eq_y eq_z have "(y, z) \<in> child s" by simp

  1662     moreover have "(z, n2) \<in> (child s)^+" by fact

  1663     ultimately show ?case by auto

  1664   qed

  1665 qed

  1666 

  1667 lemma  child_kept_right:

  1668   assumes

  1669   "(n1, n2) \<in> (child s)^+"

  1670   shows "(n1, n2) \<in> (child s')^+"

  1671 proof -

  1672   from assms show ?thesis

  1673   proof(induct)

  1674     case (base y)

  1675     from base and RAG_s

  1676     have "(n1, y) \<in> child s'"

  1677       apply (auto simp:child_def)

  1678       proof -

  1679         fix th'

  1680         assume "(Th th', Cs cs) \<in> RAG s'"

  1681         with ee have "False"

  1682           by (auto simp:s_RAG_def cs_waiting_def)

  1683         thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto 

  1684       qed

  1685     thus ?case by auto

  1686   next

  1687     case (step y z)

  1688     have "(y, z) \<in> child s" by fact

  1689     with RAG_s have "(y, z) \<in> child s'"

  1690       apply (auto simp:child_def)

  1691       proof -

  1692         fix th'

  1693         assume "(Th th', Cs cs) \<in> RAG s'"

  1694         with ee have "False"

  1695           by (auto simp:s_RAG_def cs_waiting_def)

  1696         thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto 

  1697       qed

  1698     moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact

  1699     ultimately show ?case by auto

  1700   qed

  1701 qed

  1702 

  1703 lemma eq_child: "(child s)^+ = (child s')^+"

  1704   by (insert child_kept_left child_kept_right, auto)

  1705 

  1706 lemma eq_cp:

  1707   fixes th' 

  1709   apply (unfold cp_eq_cpreced cpreced_def)

  1659 proof -

  1710 proof -

  1660   have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =

  1711   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"

  1661         (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"

  1712     apply (unfold cs_dependants_def, unfold eq_RAG)

  1662         by (unfold preced_kept subtree_kept[OF assms], simp)

  1713   proof -

  1663   thus ?thesis by (unfold cp_alt_def, simp)

  1714     from eq_child

  1715     have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"

  1716       by auto

  1717     with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]

  1718     show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"

  1719       by simp

  1720   qed

  1721   moreover {

  1722     fix th1 

  1723     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"

  1724     hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto

  1725     hence "preced th1 s = preced th1 s'"

  1726     proof

  1727       assume "th1 = th'"

  1728       show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)

  1729     next

  1730       assume "th1 \<in> dependants (wq s') th'"

  1731       show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)

  1732     qed

  1733   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 

  1734                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 

  1735     by (auto simp:image_def)

  1736   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

  1737         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp

  1816 lemma set_prop_split:

  1729 lemma cp_gen_update_stop: (* ddd *)

  1817   "A = {x. x \<in> A \<and> PP x} \<union> {x. x \<in> A \<and> \<not> PP x}"

  1818   by auto

  1819 

  1820 lemma f_image_union_eq:

  1821   assumes "f ` A = g ` A"

  1822   and "f ` B = g ` B"

  1823   shows "f ` (A \<union> B) = g ` (A \<union> B)"

  1824   using assms by auto

  1825 

  1826 (* ccc *)

  1827 

  1828 lemma cp_gen_update_stop:

  1921               have "a \<notin> ancestors (tRAG s) (Th th)" sorry

  1823               have "a \<notin> ancestors (tRAG s) (Th th)"

  1824               proof

  1825                 assume a_in': "a \<in> ancestors (tRAG s) (Th th)"

  1826                 have "a = z"

  1827                 proof(rule vat_s.rtree_s.ancestors_children_unique)

  1828                   from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)"

  1829                       by (auto simp:ancestors_def)

  1830                   with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter> 

  1831                                        RTree.children (tRAG s) x" by auto

  1832                 next

  1833                   from a_in a_in'

  1834                   show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x"

  1835                     by auto

  1836                 qed

  1837                 with False show False by auto

  1838               qed

  1939 

  1856 lemma cp_up:

  1940 

  1857   assumes "(Th th') \<in> ancestors (tRAG s) (Th th)"

  1941 (* ccc *)

  1858   and "cp s th' = cp s' th'"

  1942 

  1859   and "(Th th'') \<in> ancestors (tRAG s) (Th th')"

  1943 lemma eq_child_left:

  1944   assumes nd: "(Th th, Th th') \<notin> (child s)^+"

  1945   shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"

  1946 proof(induct rule:converse_trancl_induct)

  1947   case (base y)

  1948   from base obtain th1 cs1

  1949     where h1: "(Th th1, Cs cs1) \<in> RAG s"

  1950     and h2: "(Cs cs1, Th th') \<in> RAG s"

  1951     and eq_y: "y = Th th1"   by (auto simp:child_def)

  1952   have "th1 \<noteq> th"

  1953   proof

  1954     assume "th1 = th"

  1955     with base eq_y have "(Th th, Th th') \<in> child s" by simp

  1956     with nd show False by auto

  1957   qed

  1958   with h1 h2 RAG_s 

  1959   have h1': "(Th th1, Cs cs1) \<in> RAG s'" and 

  1960        h2': "(Cs cs1, Th th') \<in> RAG s'" by auto

  1961   with eq_y show ?case by (auto simp:child_def)

  1962 next

  1963   case (step y z)

  1964   have yz: "(y, z) \<in> child s" by fact

  1965   then obtain th1 cs1 th2

  1966     where h1: "(Th th1, Cs cs1) \<in> RAG s"

  1967     and h2: "(Cs cs1, Th th2) \<in> RAG s"

  1968     and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)

  1969   have "th1 \<noteq> th"

  1970   proof

  1971     assume "th1 = th"

  1972     with yz eq_y have "(Th th, z) \<in> child s" by simp

  1973     moreover have "(z, Th th') \<in> (child s)^+" by fact

  1974     ultimately have "(Th th, Th th') \<in> (child s)^+" by auto

  1975     with nd show False by auto

  1976   qed

  1977   with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"

  1978                        and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto

  1979   with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)

  1980   moreover have "(z, Th th') \<in> (child s')^+" by fact

  1981   ultimately show ?case by auto

  1982 qed

  1983 

  1984 lemma eq_child_right:

  1985   shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"

  1986 proof(induct rule:converse_trancl_induct)

  1987   case (base y)

  1988   with RAG_s show ?case by (auto simp:child_def)

  1989 next

  1990   case (step y z)

  1991   have "(y, z) \<in> child s'" by fact

  1992   with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def)

  1993   moreover have "(z, Th th') \<in> (child s)^+" by fact

  1994   ultimately show ?case by auto

  1995 qed

  1996 

  1997 lemma eq_child:

  1998   assumes nd: "(Th th, Th th') \<notin> (child s)^+"

  1999   shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"

  2000   by (insert eq_child_left[OF nd] eq_child_right, auto)

  2001 

  2002 lemma eq_cp:

  2003   fixes th' 

  2004   assumes nd: "th \<notin> dependants s th'"

  2005   shows "cp s th' = cp s' th'"

  2006   apply (unfold cp_eq_cpreced cpreced_def)

  2007 proof -

  2008   have nd': "(Th th, Th th') \<notin> (child s)^+"

  2009   proof

  2010     assume "(Th th, Th th') \<in> (child s)\<^sup>+"

  2011     with child_RAG_eq[OF vt_s]

  2012     have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp

  2013     with nd show False 

  2014       by (simp add:s_dependants_def eq_RAG)

  2015   qed

  2016   have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"

  2017   proof(auto)

  2018     fix x assume " x \<in> dependants (wq s) th'"

  2019     thus "x \<in> dependants (wq s') th'"

  2020       apply (auto simp:cs_dependants_def eq_RAG)

  2021     proof -

  2022       assume "(Th x, Th th') \<in> (RAG s)\<^sup>+"

  2023       with  child_RAG_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp

  2024       with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp

  2025       with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]

  2026       show "(Th x, Th th') \<in> (RAG s')\<^sup>+" by simp

  2027     qed

  2028   next

  2029     fix x assume "x \<in> dependants (wq s') th'"

  2030     thus "x \<in> dependants (wq s) th'"

  2031       apply (auto simp:cs_dependants_def eq_RAG)

  2032     proof -

  2033       assume "(Th x, Th th') \<in> (RAG s')\<^sup>+"

  2034       with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] 

  2035       have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp

  2036       with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp

  2037       with  child_RAG_eq[OF vt_s]

  2038       show "(Th x, Th th') \<in> (RAG s)\<^sup>+" by simp

  2039     qed

  2040   qed

  2041   moreover {

  2042     fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)

  2043   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 

  2044                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 

  2045     by (auto simp:image_def)

  2046   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

  2047         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp

  2048 qed

  2049 

  2050 lemma eq_up:

  2051   fixes th' th''

  2052   assumes dp1: "th \<in> dependants s th'"

  2053   and dp2: "th' \<in> dependants s th''"

  2054   and eq_cps: "cp s th' = cp s' th'"

  2057   from dp2

  1862   have "cp_gen s (Th th'') = cp_gen s' (Th th'')"

  2058   have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)

  1863   proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])

  2059   from RAG_child[OF vt_s this[unfolded eq_RAG]]

  1864     from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]

  2060   have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .

  1865     show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis

  2061   moreover {

  1866   qed

  2062     fix n th''

  1867   with cp_gen_def_cond[OF refl[of "Th th''"]]

  2063     have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>

  1868   show ?thesis by metis

  2064                    (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"

  2065     proof(erule trancl_induct, auto)

  2066       fix y th''

  2067       assume y_ch: "(y, Th th'') \<in> child s"

  2068         and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"

  2069         and ch': "(Th th', y) \<in> (child s)\<^sup>+"

  2070       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)

  2071       with ih have eq_cpy:"cp s thy = cp s' thy" by blast

  2072       from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)

  2073       moreover from child_RAG_p[OF ch'] and eq_y

  2074       have "(Th th', Th thy) \<in> (RAG s)^+" by simp

  2075       ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto

  2076       show "cp s th'' = cp s' th''"

  2077         apply (subst cp_rec[OF vt_s])

  2078       proof -

  2079         have "preced th'' s = preced th'' s'"

  2080           by (simp add:s_def preced_def)

  2081         moreover { 

  2082           fix th1

  2083           assume th1_in: "th1 \<in> children s th''"

  2084           have "cp s th1 = cp s' th1"

  2085           proof(cases "th1 = thy")

  2086             case True

  2087             with eq_cpy show ?thesis by simp

  2088           next

  2089             case False

  2090             have neq_th1: "th1 \<noteq> th"

  2091             proof

  2092               assume eq_th1: "th1 = th"

  2093               with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp

  2094               from children_no_dep[OF vt_s _ _ this] and 

  2095               th1_in y_ch eq_y show False by (auto simp:children_def)

  2096             qed

  2097             have "th \<notin> dependants s th1"

  2098             proof

  2099               assume h:"th \<in> dependants s th1"

  2100               from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)

  2101               from dependants_child_unique[OF vt_s _ _ h this]

  2102               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)

  2103               with False show False by auto

  2104             qed

  2105             from eq_cp[OF this]

  2106             show ?thesis .

  2107           qed

  2108         }

  2109         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 

  2110           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)

  2111         moreover have "children s th'' = children s' th''"

  2112           apply (unfold children_def child_def s_def RAG_set_unchanged, simp)

  2113           apply (fold s_def, auto simp:RAG_s)

  2114           proof -

  2115             assume "(Cs cs, Th th'') \<in> RAG s'"

  2116             with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto

  2117             from dp1 have "(Th th, Th th') \<in> (RAG s)^+"

  2118               by (auto simp:s_dependants_def eq_RAG)

  2119             from converse_tranclE[OF this]

  2120             obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"

  2121               and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"

  2122               by (auto simp:s_RAG_def)

  2123             have eq_cs: "cs1 = cs" 

  2124             proof -

  2125               from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp

  2126               from unique_RAG[OF vt_s this h1]

  2127               show ?thesis by simp

  2128             qed

  2129             have False

  2130             proof(rule converse_tranclE[OF h2])

  2131               assume "(Cs cs1, Th th') \<in> RAG s"

  2132               with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp

  2133               from unique_RAG[OF vt_s this cs_th']

  2134               have "th' = th''" by simp

  2135               with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto

  2136               with wf_trancl[OF wf_child[OF vt_s]] 

  2137               show False by auto

  2138             next

  2139               fix y

  2140               assume "(Cs cs1, y) \<in> RAG s"

  2141                 and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"

  2142               with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp

  2143               from unique_RAG[OF vt_s this cs_th']

  2144               have "y = Th th''" .

  2145               with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp

  2146               from RAG_child[OF vt_s this]

  2147               have "(Th th'', Th th') \<in> (child s)\<^sup>+" .

  2148               moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto

  2149               ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto 

  2150               with wf_trancl[OF wf_child[OF vt_s]] 

  2151               show False by auto

  2152             qed

  2153             thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto

  2154           qed

  2155           ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"

  2156           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])

  2157       qed

  2158     next

  2159       fix th''

  2160       assume dp': "(Th th', Th th'') \<in> child s"

  2161       show "cp s th'' = cp s' th''"

  2162         apply (subst cp_rec[OF vt_s])

  2163       proof -

  2164         have "preced th'' s = preced th'' s'"

  2165           by (simp add:s_def preced_def)

  2166         moreover { 

  2167           fix th1

  2168           assume th1_in: "th1 \<in> children s th''"

  2169           have "cp s th1 = cp s' th1"

  2170           proof(cases "th1 = th'")

  2171             case True

  2172             with eq_cps show ?thesis by simp

  2173           next

  2174             case False

  2175             have neq_th1: "th1 \<noteq> th"

  2176             proof

  2177               assume eq_th1: "th1 = th"

  2178               with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 

  2179                 by (auto simp:s_dependants_def eq_RAG)

  2180               from children_no_dep[OF vt_s _ _ this]

  2181               th1_in dp'

  2182               show False by (auto simp:children_def)

  2183             qed

  2184             show ?thesis

  2185             proof(rule eq_cp)

  2186               show "th \<notin> dependants s th1"

  2187               proof

  2188                 assume "th \<in> dependants s th1"

  2189                 from dependants_child_unique[OF vt_s _ _ this dp1]

  2190                 th1_in dp' have "th1 = th'"

  2191                   by (auto simp:children_def)

  2192                 with False show False by auto

  2193               qed

  2194             qed

  2195           qed

  2196         }

  2197         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 

  2198           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)

  2199         moreover have "children s th'' = children s' th''"

  2200           apply (unfold children_def child_def s_def RAG_set_unchanged, simp)

  2201           apply (fold s_def, auto simp:RAG_s)

  2202           proof -

  2203             assume "(Cs cs, Th th'') \<in> RAG s'"

  2204             with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto

  2205             from dp1 have "(Th th, Th th') \<in> (RAG s)^+"

  2206               by (auto simp:s_dependants_def eq_RAG)

  2207             from converse_tranclE[OF this]

  2208             obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"

  2209               and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"

  2210               by (auto simp:s_RAG_def)

  2211             have eq_cs: "cs1 = cs" 

  2212             proof -

  2213               from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp

  2214               from unique_RAG[OF vt_s this h1]

  2215               show ?thesis by simp

  2216             qed

  2217             have False

  2218             proof(rule converse_tranclE[OF h2])

  2219               assume "(Cs cs1, Th th') \<in> RAG s"

  2220               with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp

  2221               from unique_RAG[OF vt_s this cs_th']

  2222               have "th' = th''" by simp

  2223               with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto

  2224               with wf_trancl[OF wf_child[OF vt_s]] 

  2225               show False by auto

  2226             next

  2227               fix y

  2228               assume "(Cs cs1, y) \<in> RAG s"

  2229                 and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"

  2230               with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp

  2231               from unique_RAG[OF vt_s this cs_th']

  2232               have "y = Th th''" .

  2233               with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp

  2234               from RAG_child[OF vt_s this]

  2235               have "(Th th'', Th th') \<in> (child s)\<^sup>+" .

  2236               moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto

  2237               ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto 

  2238               with wf_trancl[OF wf_child[OF vt_s]] 

  2239               show False by auto

  2240             qed

  2241             thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto

  2242           qed

  2243         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"

  2244           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])

  2245       qed     

  2246     qed

  2247   }

  2248   ultimately show ?thesis by auto

  2261 lemma eq_dep: "RAG s = RAG s'"

  1887 lemma RAG_kept: "RAG s = RAG s'"

  2268   apply (unfold cp_eq_cpreced cpreced_def)

  1911 proof -

  2269 proof -

  1912   have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =

  2270   have nd: "th \<notin> dependants s th'"

  1913         (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"

  2271   proof

  1914   proof(unfold tRAG_kept, rule f_image_eq)

  2272     assume "th \<in> dependants s th'"

  1915     fix a

  2273     hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)

  1916     assume a_in: "a \<in> subtree (tRAG s') (Th th')"

  2274     with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp

  1917     then obtain th_a where eq_a: "a = Th th_a" 

  2275     from converse_tranclE[OF this]

  1918     proof(cases rule:subtreeE)

  2276     obtain y where "(Th th, y) \<in> RAG s'" by auto

  1919       case 2

  2277     with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]

  1920       from ancestors_Field[OF 2(2)]

  2278     have in_th: "th \<in> threads s'" by auto

  1921       and that show ?thesis by (unfold tRAG_alt_def, auto)

  2279     from step_back_step[OF vt_s[unfolded s_def]]

  1922     qed auto

  2280     show False

  1923     have neq_th_a: "th_a \<noteq> th"

  2281     proof(cases)

  2282       assume "th \<notin> threads s'" 

  2283       with in_th show ?thesis by simp

  2284     qed

  2285   qed

  2286   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"

  2287     by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)

  2288   moreover {

  2289     fix th1 

  2290     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"

  2291     hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto

  2292     hence "preced th1 s = preced th1 s'"

  2293     proof

  2294       assume "th1 = th'"

  2295       with neq_th

  2296       show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)

  2297     next

  2298       assume "th1 \<in> dependants (wq s') th'"

  2299       with nd and eq_dp have "th1 \<noteq> th"

  2300         by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)

  2301       thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)

  2302     qed

  2303   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 

  2304                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 

  2305     by (auto simp:image_def)

  2306   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

  2307         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp

  2308 qed

  2309 

  2310 lemma nil_dependants: "dependants s th = {}"

  2311 proof -

  2312   from step_back_step[OF vt_s[unfolded s_def]]

  2313   show ?thesis

  2314   proof(cases)

  2315     assume "th \<notin> threads s'"

  2316     from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]

  2317     have hdn: " holdents s' th = {}" .

  2318     have "dependants s' th = {}"

  2320       { assume "dependants s' th \<noteq> {}"

  1925       have "(Th th) \<notin> subtree (tRAG s') (Th th')"

  2321         then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+"

  1926       proof

  2322           by (auto simp:s_dependants_def eq_RAG)

  1927         assume "Th th \<in> subtree (tRAG s') (Th th')"

  2323         from tranclE[OF this] obtain cs' where 

  1928         thus False

  2324           "(Cs cs', Th th) \<in> RAG s'" by (auto simp:s_RAG_def)

  1929         proof(cases rule:subtreeE)

  2325         with hdn

  1930           case 2

  2326         have False by (auto simp:holdents_test)

  1931           from ancestors_Field[OF this(2)]

  2327       } thus ?thesis by auto

  1932           and th_not_in[unfolded Field_def]

  2328     qed

  1933           show ?thesis by auto

  2329     thus ?thesis 

  1934         qed (insert assms, auto)

  2330       by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp)

  1935       qed

  2331   qed

  1936       with a_in[unfolded eq_a] show ?thesis by auto

  1937     qed

  1938     from preced_kept[OF this]

  1939     show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"

  1940       by (unfold eq_a, simp)

  1941   qed

  1942   thus ?thesis by (unfold cp_alt_def1, simp)

  1943 qed

  1944 

  1945 lemma children_of_th: "RTree.children (tRAG s) (Th th) = {}"

  1946 proof -

  1947   { fix a

  1948     assume "a \<in> RTree.children (tRAG s) (Th th)"

  1949     hence "(a, Th th) \<in> tRAG s" by (auto simp:RTree.children_def)

  1950     with th_not_in have False 

  1951      by (unfold Field_def tRAG_kept, auto)

  1952   } thus ?thesis by auto

  2335   apply (unfold cp_eq_cpreced cpreced_def)

  1956  by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def)

  2336   by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)

  2349 lemma eq_dep: "RAG s = RAG s'"

  1974 lemma preced_kept:

  1975   assumes "th' \<noteq> th"

  1976   shows "the_preced s th' = the_preced s' th'"

  1977   by (unfold s_def the_preced_def preced_def, insert assms, auto)

  1978 

  1979 lemma RAG_kept: "RAG s = RAG s'"

  2356   apply (unfold cp_eq_cpreced cpreced_def)

  2026 proof -

  2357 proof -

  2027   have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =

  2358   have nd: "th \<notin> dependants s th'"

  2028         (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"

  2359   proof

  2029   proof(unfold tRAG_kept, rule f_image_eq)

  2360     assume "th \<in> dependants s th'"

  2030     fix a

  2361     hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)

  2031     assume a_in: "a \<in> subtree (tRAG s') (Th th')"

  2362     with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp

  2032     then obtain th_a where eq_a: "a = Th th_a" 

  2363     from converse_tranclE[OF this]

  2033     proof(cases rule:subtreeE)

  2364     obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'"

  2034       case 2

  2365       by (auto simp:s_RAG_def)

  2035       from ancestors_Field[OF 2(2)]

  2366     from step_back_step[OF vt_s[unfolded s_def]]

  2036       and that show ?thesis by (unfold tRAG_alt_def, auto)

  2367     show False

  2037     qed auto

  2368     proof(cases)

  2038     have neq_th_a: "th_a \<noteq> th"

  2369       assume "th \<in> runing s'"

  2039     proof -

  2370       with bk show ?thesis

  2040       from readys_in_no_subtree[OF vat_s'.vt th_ready assms]

  2371         apply (unfold runing_def readys_def s_waiting_def s_RAG_def)

  2041       have "(Th th) \<notin> subtree (RAG s') (Th th')" .

  2372         by (auto simp:cs_waiting_def wq_def)

  2042       find_theorems subtree tRAG RAG (* ccc *)

  2373     qed

  2043       proof

  2374   qed

  2044         assume "Th th \<in> subtree (tRAG s') (Th th')"

  2375   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"

  2045         thus False

  2376     by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)

  2046         proof(cases rule:subtreeE)

  2377   moreover {

  2047           case 2

  2378     fix th1 

  2048           from ancestors_Field[OF this(2)]

  2379     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"

  2049           and th_tRAG[unfolded Field_def]

  2380     hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto

  2050           show ?thesis by auto

  2381     hence "preced th1 s = preced th1 s'"

  2051         qed (insert assms, auto)

  2382     proof

  2052       qed

  2383       assume "th1 = th'"

  2053       with a_in[unfolded eq_a] show ?thesis by auto

  2384       with neq_th

  2054     qed

  2385       show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)

  2055     from preced_kept[OF this]

  2386     next

  2056     show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"

  2387       assume "th1 \<in> dependants (wq s') th'"

  2057       by (unfold eq_a, simp)

  2388       with nd and eq_dp have "th1 \<noteq> th"

  2058   qed

  2389         by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)

  2059   thus ?thesis by (unfold cp_alt_def1, simp)

  2390       thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)

  2391     qed

  2392   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 

  2393                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 

  2394     by (auto simp:image_def)

  2395   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

  2396         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp