208 lemma threads_set_eq: 

   224 lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"

   209    "the_thread ` (subtree (tRAG s) (Th th)) = 

   225 proof -

   210                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")

   226   have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" 

   211 proof -

   227     by (rule rtrancl_mono, auto simp:RAG_split)

   212   { fix th'

   228   also have "... \<subseteq> ((RAG s)^*)^*"

   213     assume "th' \<in> ?L"

   229     by (rule rtrancl_mono, auto)

   214     then obtain n where h: "th' = the_thread n" "n \<in>  subtree (tRAG s) (Th th)" by auto

   230   also have "... = (RAG s)^*" by simp

   215     from subtree_nodeE[OF this(2)]

   231   finally show ?thesis by (unfold tRAG_def, simp)

   216     obtain th1 where "n = Th th1" by auto

   232 qed

   217     with h have "Th th' \<in>  subtree (tRAG s) (Th th)" by auto

   233 

   218     hence "Th th' \<in>  subtree (RAG s) (Th th)"

   234 lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"

   219     proof(cases rule:subtreeE[consumes 1])

   235 proof -

   220       case 1

   236   { fix a

   221       thus ?thesis by (auto simp:subtree_def)

   237     assume "a \<in> subtree (tRAG s) x"

   222     next

   238     hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)

   223       case 2

   239     with tRAG_star_RAG[of s]

   224       hence "(Th th', Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)

   240     have "(a, x) \<in> (RAG s)^*" by auto

   225       thus ?thesis

   241     hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)

   226       proof(induct)

   242   } thus ?thesis by auto

   227         case (step y z)

   243 qed

   228         from this(2)[unfolded tRAG_alt_def]

   244 

   229         obtain u where 

   245 lemma tRAG_subtree_eq: 

   230          h: "(y, u) \<in> RAG s" "(u, z) \<in> RAG s"

   246    "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"

   231           by auto

   247    (is "?L = ?R")

   232         hence "y \<in> subtree (RAG s) z" by (auto simp:subtree_def)

   248 proof -

   233         with step(3)

   249   { fix n

   234         show ?case by (auto simp:subtree_def)

   250     assume "n \<in> ?L"

   235       next

   251     with subtree_nodeE[OF this]

   236         case (base y)

   252     obtain th' where "n = Th th'" "Th th' \<in>  subtree (tRAG s) (Th th)" by auto

   237         from this[unfolded tRAG_alt_def]

   253     with tRAG_subtree_RAG[of s "Th th"]

   238         show ?case by (auto simp:subtree_def)

   254     have "n \<in> ?R" by auto

   239       qed

   240     qed

   241     hence "th' \<in> ?R" by auto

   243     fix th'

   256     fix n

   244     assume "th' \<in> ?R"

   257     assume "n \<in> ?R"

   245     hence "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def)

   258     then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" 

   246     from star_rpath[OF this]

   259       by (auto simp:subtree_def)

   260     from star_rpath[OF this(2)]

   300     from imageI[OF this, of the_thread]

   313     from this[folded h(1)]

   301     have "th' \<in> ?L" by simp

   314     have "n \<in> ?L" .

   304                   

   317 

   318 lemma threads_set_eq: 

   319    "the_thread ` (subtree (tRAG s) (Th th)) = 

   320                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")

   321    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

   322 

  1575 lemma rtree_RAGs: "rtree (RAG s)"

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

  1603 proof -

  1604     from step_back_step [OF vt_s[unfolded s_def]]

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

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

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

  1608 qed

  1609 

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

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

  1612 

  1613 lemma in_no_others_subtree:

  1614   assumes "th' \<noteq> th"

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

  1577   show "single_valued (RAG s)"

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

  1578   apply (intro_locales)

  1618   thus False

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

  1619   proof(cases rule:subtreeE)

  1580 

  1620     case 1

  1581   show "acyclic (RAG s)"

  1621     with assms show ?thesis by auto

  1582      by (rule acyclic_RAG[OF vt_s])

  1622   next

  1583 qed

  1623     case 2

  1584 

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

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

  1625   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:

  1650 lemma subtree_kept:

  1619   assumes 

  1651   assumes "th' \<noteq> th"

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

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

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

  1653 proof(unfold RAG_s, rule subtree_insert_next)

  1622 proof -

  1654   from in_no_others_subtree[OF assms] 

  1623   from assms show ?thesis 

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

  1624   proof(induct rule: converse_trancl_induct)

  1656 qed

  1625     case (base y)

  1657 

  1626     from base obtain th1 cs1 th2

  1658 lemma cp_kept: 

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

  1659   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)

  1661 proof -

  1710 proof -

  1662   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"

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

  1712     apply (unfold cs_dependants_def, unfold eq_RAG)

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

  1713   proof -

  1665   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:

  1731 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:

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

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

  1826               proof

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

  1828                 have "a = z"

  1829                 proof(rule vat_s.rtree_s.ancestors_children_unique)

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

  1831                       by (auto simp:ancestors_def)

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

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

  1834                 next

  1835                   from a_in a_in'

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

  1837                     by auto

  1838                 qed

  1839                 with False show False by auto

  1840               qed

  1940 

  1858 lemma cp_up:

  1941 

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

  1942 (* ccc *)

  1860   and "cp s th' = cp s' th'"

  1943 

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

  1944 lemma eq_child_left:

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

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

  1947 proof(induct rule:converse_trancl_induct)

  1948   case (base y)

  1949   from base obtain th1 cs1

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

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

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

  1953   have "th1 \<noteq> th"

  1954   proof

  1955     assume "th1 = th"

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

  1957     with nd show False by auto

  1958   qed

  1959   with h1 h2 RAG_s 

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

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

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

  1963 next

  1964   case (step y z)

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

  1966   then obtain th1 cs1 th2

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

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

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

  1970   have "th1 \<noteq> th"

  1971   proof

  1972     assume "th1 = th"

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

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

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

  1976     with nd show False by auto

  1977   qed

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

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

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

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

  1982   ultimately show ?case by auto

  1983 qed

  1984 

  1985 lemma eq_child_right:

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

  1987 proof(induct rule:converse_trancl_induct)

  1988   case (base y)

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

  1990 next

  1991   case (step y z)

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

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

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

  1995   ultimately show ?case by auto

  1996 qed

  1997 

  1998 lemma eq_child:

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

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

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

  2002 

  2003 lemma eq_cp:

  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   assumes dp1: "th \<in> dependants s th'"

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

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

  2056   from dp2

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

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

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

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

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

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

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

  2060   moreover {

  1868   qed

  2061     fix n th''

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

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

  1870   show ?thesis by metis

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

  2064     proof(erule trancl_induct, auto)

  2065       fix y th''

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

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

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

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

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

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

  2072       moreover from child_RAG_p[OF ch'] and eq_y

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

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

  2075       show "cp s th'' = cp s' th''"

  2076         apply (subst cp_rec[OF vt_s])

  2077       proof -

  2078         have "preced th'' s = preced th'' s'"

  2079           by (simp add:s_def preced_def)

  2080         moreover { 

  2081           fix th1

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

  2083           have "cp s th1 = cp s' th1"

  2084           proof(cases "th1 = thy")

  2085             case True

  2086             with eq_cpy show ?thesis by simp

  2087           next

  2088             case False

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

  2090             proof

  2091               assume eq_th1: "th1 = th"

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

  2093               from children_no_dep[OF vt_s _ _ this] and 

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

  2095             qed

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

  2097             proof

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

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

  2100               from dependants_child_unique[OF vt_s _ _ h this]

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

  2102               with False show False by auto

  2103             qed

  2104             from eq_cp[OF this]

  2105             show ?thesis .

  2106           qed

  2107         }

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

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

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

  2111           apply (unfold children_def child_def s_def RAG_set_unchanged, simp)

  2112           apply (fold s_def, auto simp:RAG_s)

  2113           proof -

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

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

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

  2117               by (auto simp:s_dependants_def eq_RAG)

  2118             from converse_tranclE[OF this]

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

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

  2121               by (auto simp:s_RAG_def)

  2122             have eq_cs: "cs1 = cs" 

  2123             proof -

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

  2125               from unique_RAG[OF vt_s this h1]

  2126               show ?thesis by simp

  2127             qed

  2128             have False

  2129             proof(rule converse_tranclE[OF h2])

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

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

  2132               from unique_RAG[OF vt_s this cs_th']

  2133               have "th' = th''" by simp

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

  2135               with wf_trancl[OF wf_child[OF vt_s]] 

  2136               show False by auto

  2137             next

  2138               fix y

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

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

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

  2142               from unique_RAG[OF vt_s this cs_th']

  2143               have "y = Th th''" .

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

  2145               from RAG_child[OF vt_s this]

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

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

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

  2149               with wf_trancl[OF wf_child[OF vt_s]] 

  2150               show False by auto

  2151             qed

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

  2153           qed

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

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

  2156       qed

  2157     next

  2158       fix th''

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

  2160       show "cp s th'' = cp s' th''"

  2161         apply (subst cp_rec[OF vt_s])

  2162       proof -

  2163         have "preced th'' s = preced th'' s'"

  2164           by (simp add:s_def preced_def)

  2165         moreover { 

  2166           fix th1

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

  2168           have "cp s th1 = cp s' th1"

  2169           proof(cases "th1 = th'")

  2170             case True

  2171             with eq_cps show ?thesis by simp

  2172           next

  2173             case False

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

  2175             proof

  2176               assume eq_th1: "th1 = th"

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

  2178                 by (auto simp:s_dependants_def eq_RAG)

  2179               from children_no_dep[OF vt_s _ _ this]

  2180               th1_in dp'

  2181               show False by (auto simp:children_def)

  2182             qed

  2183             show ?thesis

  2184             proof(rule eq_cp)

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

  2186               proof

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

  2188                 from dependants_child_unique[OF vt_s _ _ this dp1]

  2189                 th1_in dp' have "th1 = th'"

  2190                   by (auto simp:children_def)

  2191                 with False show False by auto

  2192               qed

  2193             qed

  2194           qed

  2195         }

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

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

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

  2199           apply (unfold children_def child_def s_def RAG_set_unchanged, simp)

  2200           apply (fold s_def, auto simp:RAG_s)

  2201           proof -

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

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

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

  2205               by (auto simp:s_dependants_def eq_RAG)

  2206             from converse_tranclE[OF this]

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

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

  2209               by (auto simp:s_RAG_def)

  2210             have eq_cs: "cs1 = cs" 

  2211             proof -

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

  2213               from unique_RAG[OF vt_s this h1]

  2214               show ?thesis by simp

  2215             qed

  2216             have False

  2217             proof(rule converse_tranclE[OF h2])

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

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

  2220               from unique_RAG[OF vt_s this cs_th']

  2221               have "th' = th''" by simp

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

  2223               with wf_trancl[OF wf_child[OF vt_s]] 

  2224               show False by auto

  2225             next

  2226               fix y

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

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

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

  2230               from unique_RAG[OF vt_s this cs_th']

  2231               have "y = Th th''" .

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

  2233               from RAG_child[OF vt_s this]

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

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

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

  2237               with wf_trancl[OF wf_child[OF vt_s]] 

  2238               show False by auto

  2239             qed

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

  2241           qed

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

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

  2244       qed     

  2245     qed

  2246   }

  2247   ultimately show ?thesis by auto

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

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

  2267   apply (unfold cp_eq_cpreced cpreced_def)

  1913 proof -

  2268 proof -

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

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

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

  2270   proof

  1916   proof(unfold tRAG_kept, rule f_image_eq)

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

  1917     fix a

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

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

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

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

  2274     from converse_tranclE[OF this]

  1920     proof(cases rule:subtreeE)

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

  1921       case 2

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

  1922       from ancestors_Field[OF 2(2)]

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

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

  2278     from step_back_step[OF vt_s[unfolded s_def]]

  1924     qed auto

  2279     show False

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

  2280     proof(cases)

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

  2282       with in_th show ?thesis by simp

  2283     qed

  2284   qed

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

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

  2287   moreover {

  2288     fix th1 

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

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

  2291     hence "preced th1 s = preced th1 s'"

  2292     proof

  2293       assume "th1 = th'"

  2294       with neq_th

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

  2296     next

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

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

  2299         by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)

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

  2301     qed

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

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

  2304     by (auto simp:image_def)

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

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

  2307 qed

  2308 

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

  2310 proof -

  2311   from step_back_step[OF vt_s[unfolded s_def]]

  2312   show ?thesis

  2313   proof(cases)

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

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

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

  2317     have "dependants s' th = {}"

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

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

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

  1928       proof

  2321           by (auto simp:s_dependants_def eq_RAG)

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

  2322         from tranclE[OF this] obtain cs' where 

  1930         thus False

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

  1931         proof(cases rule:subtreeE)

  2324         with hdn

  1932           case 2

  2325         have False by (auto simp:holdents_test)

  1933           from ancestors_Field[OF this(2)]

  2326       } thus ?thesis by auto

  1934           and th_not_in[unfolded Field_def]

  2327     qed

  1935           show ?thesis by auto

  2328     thus ?thesis 

  1936         qed (insert assms, auto)

  2329       by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp)

  1937       qed

  2330   qed

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

  1939     qed

  1940     from preced_kept[OF this]

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

  1942       by (unfold eq_a, simp)

  1943   qed

  1944   thus ?thesis by (unfold cp_alt_def1, simp)

  1945 qed

  1946 

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

  1948 proof -

  1949   { fix a

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

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

  1952     with th_not_in have False 

  1953      by (unfold Field_def tRAG_kept, auto)

  1954   } thus ?thesis by auto

  2334   apply (unfold cp_eq_cpreced cpreced_def)

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

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

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

  1976 lemma preced_kept:

  1977   assumes "th' \<noteq> th"

  1978   shows "the_preced s th' = the_preced s' th'"

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

  1980 

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

  2355   apply (unfold cp_eq_cpreced cpreced_def)

  2028 proof -

  2356 proof -

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

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

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

  2358   proof

  2031   proof(unfold tRAG_kept, rule f_image_eq)

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

  2032     fix a

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

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

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

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

  2362     from converse_tranclE[OF this]

  2035     proof(cases rule:subtreeE)

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

  2036       case 2

  2364       by (auto simp:s_RAG_def)

  2037       from ancestors_Field[OF 2(2)]

  2365     from step_back_step[OF vt_s[unfolded s_def]]

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

  2366     show False

  2039     qed auto

  2367     proof(cases)

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

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

  2041     proof -

  2369       with bk show ?thesis

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

  2370         apply (unfold runing_def readys_def s_waiting_def s_RAG_def)

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

  2371         by (auto simp:cs_waiting_def wq_def)

  2044       with tRAG_subtree_RAG[of s' "Th th'"]

  2372     qed

  2045       have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto

  2373   qed

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

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

  2047     qed

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

  2048     from preced_kept[OF this]

  2376   moreover {

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

  2377     fix th1 

  2050       by (unfold eq_a, simp)

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

  2051   qed

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

  2052   thus ?thesis by (unfold cp_alt_def1, simp)

  2380     hence "preced th1 s = preced th1 s'"

  2381     proof

  2382       assume "th1 = th'"

  2383       with neq_th

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

  2385     next

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

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

  2388         by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)

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

  2390     qed

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

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

  2393     by (auto simp:image_def)

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

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