2 imports PIPDefs 

     2 imports PIPDefs

     3 begin

     3 begin

     4 

     5 lemma Max_fg_mono:

     6   assumes "finite A"

     7   and "\<forall> a \<in> A. f a \<le> g a"

     8   shows "Max (f ` A) \<le> Max (g ` A)"

     9 proof(cases "A = {}")

    10   case True

    11   thus ?thesis by auto

    12 next

    13   case False

    14   show ?thesis

    15   proof(rule Max.boundedI)

    16     from assms show "finite (f ` A)" by auto

    17   next

    18     from False show "f ` A \<noteq> {}" by auto

    19   next

    20     fix fa

    21     assume "fa \<in> f ` A"

    22     then obtain a where h_fa: "a \<in> A" "fa = f a" by auto

    23     show "fa \<le> Max (g ` A)"

    24     proof(rule Max_ge_iff[THEN iffD2])

    25       from assms show "finite (g ` A)" by auto

    26     next

    27       from False show "g ` A \<noteq> {}" by auto

    28     next

    29       from h_fa have "g a \<in> g ` A" by auto

    30       moreover have "fa \<le> g a" using h_fa assms(2) by auto

    31       ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto

    32     qed

    33   qed

    34 qed 

   772   using assms

   862   using assms set_wq' by simp

   773   by (metis (mono_tags, lifting) distinct.simps(2) 

   774         rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) 

  1383 lemma  cp_le:

  1471 lemma rg_RAG_threads: 

  1384   assumes th_in: "th \<in> threads s"

  1472   assumes "(Th th) \<in> Range (RAG s)"

  1385   shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"

  1473   shows "th \<in> threads s"

  1386 proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)

  1474   using assms

  1387   show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))

  1475   by (unfold s_RAG_def cs_waiting_def cs_holding_def, 

  1388          \<le> Max ((\<lambda>th. preced th s) ` threads s)"

  1476        auto intro:wq_threads)

  1389     (is "Max (?f ` ?A) \<le> Max (?f ` ?B)")

  1477 

  1390   proof(rule Max_f_mono)

  1478 end

  1391     show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp

  1479 

  1392   next

  1480 

  1393     from finite_threads

  1481 

  1394     show "finite (threads s)" .

  1395   next

  1396     from th_in

  1397     show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"

  1398       apply (auto simp:Domain_def)

  1399       apply (rule_tac dm_RAG_threads)

  1400       apply (unfold trancl_domain [of "RAG s", symmetric])

  1401       by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)

  1402   qed

  1403 qed

  1404 

  1405 lemma max_cp_eq: 

  1406   shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"

  1407   (is "?l = ?r")

  1408 proof(cases "threads s = {}")

  1409   case True

  1410   thus ?thesis by auto

  1411 next

  1412   case False

  1413   have "?l \<in> ((cp s) ` threads s)"

  1414   proof(rule Max_in)

  1415     from finite_threads

  1416     show "finite (cp s ` threads s)" by auto

  1417   next

  1418     from False show "cp s ` threads s \<noteq> {}" by auto

  1419   qed

  1420   then obtain th 

  1421     where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto

  1422   have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])

  1423   moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")

  1424   proof -

  1425     have "?r \<in> (?f ` ?A)"

  1426     proof(rule Max_in)

  1427       from finite_threads

  1428       show " finite ((\<lambda>th. preced th s) ` threads s)" by auto

  1429     next

  1430       from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto

  1431     qed

  1432     then obtain th' where 

  1433       th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto

  1434     from le_cp [of th']  eq_r

  1435     have "?r \<le> cp s th'" by auto

  1436     moreover have "\<dots> \<le> cp s th"

  1437     proof(fold eq_l)

  1438       show " cp s th' \<le> Max (cp s ` threads s)"

  1439       proof(rule Max_ge)

  1440         from th_in' show "cp s th' \<in> cp s ` threads s"

  1441           by auto

  1442       next

  1443         from finite_threads

  1444         show "finite (cp s ` threads s)" by auto

  1445       qed

  1446     qed

  1447     ultimately show ?thesis by auto

  1448   qed

  1449   ultimately show ?thesis using eq_l by auto

  1450 qed

  1451 

  1452 lemma max_cp_eq_the_preced:

  1453   shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"

  1454   using max_cp_eq using the_preced_def by presburger 

  1455 

  1456 end

  1479 lemma not_holding_es_th_cs: "\<not> holding s th cs"

  1504 lemma not_holding_s_th_cs: "\<not> holding s th cs"

  1499   assumes we: "wq s cs \<noteq> []"

  1550   assumes wne: "wq s cs \<noteq> []"

  1507     by (simp add: holder_def waiters_def we)

  1558     by (simp add: holder_def waiters_def wne)

  1605       find_theorems waiting e s

  1737       from waiting_kept[OF this(3)]

  1606     qed

  1738       show ?thesis using waiting(1,2)

  1607   qed

  1739          by (unfold s_RAG_def, fold waiting_eq, auto)

  1608 qed

  1740     next

  1609 

  1741       case (holding th' cs')

  1610 end

  1742       from holding_kept[OF this(3)]

  1611 

  1743       show ?thesis using holding(1,2)

  1612 

  1744          by (unfold s_RAG_def, fold holding_eq, auto)

  1613 

  1745     qed

  1614 lemma "RAG (e # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}

  1746   next

  1615                                          else RAG s \<union> {(Th th, Cs cs)})"

  1747     assume "n1 = Cs cs \<and> n2 = Th th"

  1748     with holding_es_th_cs

  1749     show ?thesis 

  1750       by (unfold s_RAG_def, fold holding_eq, auto)

  1751   qed

  1752 qed

  1753 

  1754 end

  1755 

  1756 context valid_trace_p

  1757 begin

  1758 

  1759 lemma RAG_es': "RAG (e # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}

  1760                                                   else RAG s \<union> {(Th th, Cs cs)})"

  1761 proof(cases "wq s cs = []")

  1762   case True

  1763   interpret vt_p: valid_trace_p_h using True

  1764     by (unfold_locales, simp)

  1765   show ?thesis by (simp add: vt_p.RAG_es vt_p.we) 

  1766 next

  1767   case False

  1768   interpret vt_p: valid_trace_p_w using False

  1769     by (unfold_locales, simp)

  1770   show ?thesis by (simp add: vt_p.RAG_es vt_p.wne) 

  1771 qed

  1772 

  1773 end

  1774 

  1775 lemma (in valid_trace_v_n) finite_waiting_set:

  1776   "finite {(Th th', Cs cs) |th'. next_th s th cs th'}"

  1777     by (simp add: waiting_set_eq)

  1778 

  1779 lemma (in valid_trace_v_n) finite_holding_set:

  1780   "finite {(Cs cs, Th th') |th'. next_th s th cs th'}"

  1781     by (simp add: holding_set_eq)

  1782 

  1783 lemma (in valid_trace_v_e) finite_waiting_set:

  1784   "finite {(Th th', Cs cs) |th'. next_th s th cs th'}"

  1785     by (simp add: waiting_set_eq)

  1786 

  1787 lemma (in valid_trace_v_e) finite_holding_set:

  1788   "finite {(Cs cs, Th th') |th'. next_th s th cs th'}"

  1789     by (simp add: holding_set_eq)

  1790 

  1791 context valid_trace_v

  1792 begin

  1793 

  1794 lemma 

  1795   finite_RAG_kept:

  1796   assumes "finite (RAG s)"

  1797   shows "finite (RAG (e#s))"

  1798 proof(cases "rest = []")

  1799   case True

  1800   interpret vt: valid_trace_v_e using True

  1801     by (unfold_locales, simp)

  1802   show ?thesis using assms

  1803     by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)

  1804 next

  1805   case False

  1806   interpret vt: valid_trace_v_n using False

  1807     by (unfold_locales, simp)

  1808   show ?thesis using assms

  1809     by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)

  1810 qed

  1811 

  1812 end

  1813 

  1814 context valid_trace_v_e

  1815 begin 

  1816 

  1817 lemma 

  1818   acylic_RAG_kept:

  1819   assumes "acyclic (RAG s)"

  1820   shows "acyclic (RAG (e#s))"

  1821 proof(rule acyclic_subset[OF assms])

  1822   show "RAG (e # s) \<subseteq> RAG s"

  1823       by (unfold RAG_es waiting_set_eq holding_set_eq, auto)

  1824 qed

  1825 

  1826 end

  1827 

  1828 context valid_trace_v_n

  1829 begin 

  1830 

  1831 lemma waiting_taker: "waiting s taker cs"

  1832   apply (unfold s_waiting_def, fold wq_def, unfold wq_s_cs taker_def)

  1833   using eq_wq' th'_in_inv wq'_def by fastforce

  1834 

  1835 lemma 

  1836   acylic_RAG_kept:

  1837   assumes "acyclic (RAG s)"

  1838   shows "acyclic (RAG (e#s))"

  1839 proof -

  1840   have "acyclic ((RAG s - {(Cs cs, Th th)} - {(Th taker, Cs cs)}) \<union> 

  1841                  {(Cs cs, Th taker)})" (is "acyclic (?A \<union> _)")

  1842   proof -

  1843     from assms

  1844     have "acyclic ?A"

  1845        by (rule acyclic_subset, auto)

  1846     moreover have "(Th taker, Cs cs) \<notin> ?A^*"

  1847     proof

  1848       assume otherwise: "(Th taker, Cs cs) \<in> ?A^*"

  1849       hence "(Th taker, Cs cs) \<in> ?A^+"

  1850         by (unfold rtrancl_eq_or_trancl, auto)

  1851       from tranclD[OF this]

  1852       obtain cs' where h: "(Th taker, Cs cs') \<in> ?A" 

  1853                           "(Th taker, Cs cs') \<in> RAG s"

  1854         by (unfold s_RAG_def, auto)

  1855       from this(2) have "waiting s taker cs'" 

  1856         by (unfold s_RAG_def, fold waiting_eq, auto)

  1857       from waiting_unique[OF this waiting_taker]

  1858       have "cs' = cs" .

  1859       from h(1)[unfolded this] show False by auto

  1860     qed

  1861     ultimately show ?thesis by auto

  1862   qed

  1863   thus ?thesis 

  1864     by (unfold RAG_es waiting_set_eq holding_set_eq, simp)

  1865 qed

  1866 

  1867 end

  1868 

  1869 context valid_trace_p_h

  1870 begin

  1871 

  1872 lemma 

  1873   acylic_RAG_kept:

  1874   assumes "acyclic (RAG s)"

  1875   shows "acyclic (RAG (e#s))"

  1876 proof -

  1877   have "acyclic (RAG s \<union> {(Cs cs, Th th)})" (is "acyclic (?A \<union> _)") 

  1878   proof -

  1879     from assms

  1880     have "acyclic ?A"

  1881        by (rule acyclic_subset, auto)

  1882     moreover have "(Th th, Cs cs) \<notin> ?A^*"

  1883     proof

  1884       assume otherwise: "(Th th, Cs cs) \<in> ?A^*"

  1885       hence "(Th th, Cs cs) \<in> ?A^+"

  1886         by (unfold rtrancl_eq_or_trancl, auto)

  1887       from tranclD[OF this]

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

  1889         by (unfold s_RAG_def, auto)

  1890       hence "waiting s th cs'" 

  1891         by (unfold s_RAG_def, fold waiting_eq, auto)

  1892       with th_not_waiting show False by auto

  1893     qed

  1894     ultimately show ?thesis by auto

  1895   qed

  1896   thus ?thesis by (unfold RAG_es, simp)

  1897 qed

  1898 

  1899 end

  1900 

  1901 context valid_trace_p_w

  1902 begin

  1903 

  1904 lemma 

  1905   acylic_RAG_kept:

  1906   assumes "acyclic (RAG s)"

  1907   shows "acyclic (RAG (e#s))"

  1908 proof -

  1909   have "acyclic (RAG s \<union> {(Th th, Cs cs)})" (is "acyclic (?A \<union> _)") 

  1910   proof -

  1911     from assms

  1912     have "acyclic ?A"

  1913        by (rule acyclic_subset, auto)

  1914     moreover have "(Cs cs, Th th) \<notin> ?A^*"

  1915     proof

  1916       assume otherwise: "(Cs cs, Th th) \<in> ?A^*"

  1917       from pip_e[unfolded is_p]

  1918       show False

  1919       proof(cases)

  1920         case (thread_P)

  1921         moreover from otherwise have "(Cs cs, Th th) \<in> ?A^+"

  1922             by (unfold rtrancl_eq_or_trancl, auto)

  1923         ultimately show ?thesis by auto

  1924       qed

  1925     qed

  1926     ultimately show ?thesis by auto

  1927   qed

  1928   thus ?thesis by (unfold RAG_es, simp)

  1929 qed

  1930 

  1931 end

  1932 

  1933 context valid_trace

  1934 begin

  1935 

  1936 lemma finite_RAG:

  1937   shows "finite (RAG s)"

  1938 proof(induct rule:ind)

  1939   case Nil

  1940   show ?case 

  1941   by (auto simp: s_RAG_def cs_waiting_def 

  1942                    cs_holding_def wq_def acyclic_def)

  1943 next

  1944   case (Cons s e)

  1945   interpret vt_e: valid_trace_e s e using Cons by simp

  1946   show ?case

  1947   proof(cases e)

  1948     case (Create th prio)

  1949     interpret vt: valid_trace_create s e th prio using Create

  1950       by (unfold_locales, simp)

  1951     show ?thesis using Cons by (simp add: vt.RAG_unchanged) 

  1952   next

  1953     case (Exit th)

  1954     interpret vt: valid_trace_exit s e th using Exit

  1955       by (unfold_locales, simp)

  1956     show ?thesis using Cons by (simp add: vt.RAG_unchanged)

  1957   next

  1958     case (P th cs)

  1959     interpret vt: valid_trace_p s e th cs using P

  1960       by (unfold_locales, simp)

  1961     show ?thesis using Cons using vt.RAG_es' by auto 

  1962   next

  1963     case (V th cs)

  1964     interpret vt: valid_trace_v s e th cs using V

  1965       by (unfold_locales, simp)

  1966     show ?thesis using Cons by (simp add: vt.finite_RAG_kept) 

  1967   next

  1968     case (Set th prio)

  1969     interpret vt: valid_trace_set s e th prio using Set

  1970       by (unfold_locales, simp)

  1971     show ?thesis using Cons by (simp add: vt.RAG_unchanged) 

  1972   qed

  1973 qed

  1974 

  1975 lemma acyclic_RAG:

  1976   shows "acyclic (RAG s)"

  1977 proof(induct rule:ind)

  1978   case Nil

  1979   show ?case 

  1980   by (auto simp: s_RAG_def cs_waiting_def 

  1981                    cs_holding_def wq_def acyclic_def)

  1982 next

  1983   case (Cons s e)

  1984   interpret vt_e: valid_trace_e s e using Cons by simp

  1985   show ?case

  1986   proof(cases e)

  1987     case (Create th prio)

  1988     interpret vt: valid_trace_create s e th prio using Create

  1989       by (unfold_locales, simp)

  1990     show ?thesis using Cons by (simp add: vt.RAG_unchanged) 

  1991   next

  1992     case (Exit th)

  1993     interpret vt: valid_trace_exit s e th using Exit

  1994       by (unfold_locales, simp)

  1995     show ?thesis using Cons by (simp add: vt.RAG_unchanged)

  1996   next

  1997     case (P th cs)

  1998     interpret vt: valid_trace_p s e th cs using P

  1999       by (unfold_locales, simp)

  2000     show ?thesis

  2001     proof(cases "wq s cs = []")

  2002       case True

  2003       then interpret vt_h: valid_trace_p_h s e th cs

  2004         by (unfold_locales, simp)

  2005       show ?thesis using Cons by (simp add: vt_h.acylic_RAG_kept) 

  2006     next

  2007       case False

  2008       then interpret vt_w: valid_trace_p_w s e th cs

  2009         by (unfold_locales, simp)

  2010       show ?thesis using Cons by (simp add: vt_w.acylic_RAG_kept) 

  2011     qed

  2012   next

  2013     case (V th cs)

  2014     interpret vt: valid_trace_v s e th cs using V

  2015       by (unfold_locales, simp)

  2016     show ?thesis

  2017     proof(cases "vt.rest = []")

  2018       case True

  2019       then interpret vt_e: valid_trace_v_e s e th cs

  2020         by (unfold_locales, simp)

  2021       show ?thesis by (simp add: Cons.hyps(2) vt_e.acylic_RAG_kept) 

  2022     next

  2023       case False

  2024       then interpret vt_n: valid_trace_v_n s e th cs

  2025         by (unfold_locales, simp)

  2026       show ?thesis by (simp add: Cons.hyps(2) vt_n.acylic_RAG_kept) 

  2027     qed

  2028   next

  2029     case (Set th prio)

  2030     interpret vt: valid_trace_set s e th prio using Set

  2031       by (unfold_locales, simp)

  2032     show ?thesis using Cons by (simp add: vt.RAG_unchanged) 

  2033   qed

  2034 qed

  2035 

  2036 lemma wf_RAG: "wf (RAG s)"

  2037 proof(rule finite_acyclic_wf)

  2038   from finite_RAG show "finite (RAG s)" .

  2039 next

  2040   from acyclic_RAG show "acyclic (RAG s)" .

  2041 qed

  2042 

  2043 lemma sgv_wRAG: "single_valued (wRAG s)"

  2044   using waiting_unique

  2045   by (unfold single_valued_def wRAG_def, auto)

  2046 

  2047 lemma sgv_hRAG: "single_valued (hRAG s)"

  2048   using held_unique 

  2049   by (unfold single_valued_def hRAG_def, auto)

  2050 

  2051 lemma sgv_tRAG: "single_valued (tRAG s)"

  2052   by (unfold tRAG_def, rule single_valued_relcomp, 

  2053               insert sgv_wRAG sgv_hRAG, auto)

  2054 

  2055 lemma acyclic_tRAG: "acyclic (tRAG s)"

  2056 proof(unfold tRAG_def, rule acyclic_compose)

  2057   show "acyclic (RAG s)" using acyclic_RAG .

  2058 next

  2059   show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto

  2060 next

  2061   show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto

  2062 qed

  2063 

  2064 lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"

  2065   apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)

  2066   by(auto elim:waiting_unique held_unique)

  2067 

  2068 lemma sgv_RAG: "single_valued (RAG s)"

  2069   using unique_RAG by (auto simp:single_valued_def)

  2070 

  2071 lemma rtree_RAG: "rtree (RAG s)"

  2072   using sgv_RAG acyclic_RAG

  2073   by (unfold rtree_def rtree_axioms_def sgv_def, auto)

  2074 

  2075 end

  2076 

  2077 sublocale valid_trace < rtree_RAG: rtree "RAG s"

  2078 proof

  2079   show "single_valued (RAG s)"

  2080   apply (intro_locales)

  2081     by (unfold single_valued_def, 

  2082         auto intro:unique_RAG)

  2083 

  2084   show "acyclic (RAG s)"

  2085      by (rule acyclic_RAG)

  2086 qed

  2087 

  2088 sublocale valid_trace < rtree_s: rtree "tRAG s"

  2089 proof(unfold_locales)

  2090   from sgv_tRAG show "single_valued (tRAG s)" .

  2091 next

  2092   from acyclic_tRAG show "acyclic (tRAG s)" .

  2093 qed

  2094 

  2095 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"

  2096 proof -

  2097   show "fsubtree (RAG s)"

  2098   proof(intro_locales)

  2099     show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .

  2100   next

  2101     show "fsubtree_axioms (RAG s)"

  2102     proof(unfold fsubtree_axioms_def)

  2103       from wf_RAG show "wf (RAG s)" .

  2104     qed

  2105   qed

  2106 qed

  2107 

  2108 context valid_trace

  2109 begin

  2110 

  2111 lemma finite_subtree_threads:

  2112     "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A")

  2113 proof -

  2114   have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"

  2115         by (auto, insert image_iff, fastforce)

  2116   moreover have "finite {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"

  2117         (is "finite ?B")

  2118   proof -

  2119      have "?B = (subtree (RAG s) (Th th)) \<inter> {Th th' | th'. True}"

  2120       by auto

  2121      moreover have "... \<subseteq> (subtree (RAG s) (Th th))" by auto

  2122      moreover have "finite ..." by (simp add: finite_subtree) 

  2123      ultimately show ?thesis by auto

  2124   qed

  2125   ultimately show ?thesis by auto

  2126 qed

  2127 

  2128 lemma le_cp:

  2129   shows "preced th s \<le> cp s th"

  2130   proof(unfold cp_alt_def, rule Max_ge)

  2131     show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"

  2132       by (simp add: finite_subtree_threads)

  2133   next

  2134     show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}"

  2135       by (simp add: subtree_def the_preced_def)   

  2136   qed

  2137 

  2138 lemma cp_le:

  2139   assumes th_in: "th \<in> threads s"

  2140   shows "cp s th \<le> Max (the_preced s ` threads s)"

  2141 proof(unfold cp_alt_def, rule Max_f_mono)

  2142   show "finite (threads s)" by (simp add: finite_threads) 

  2143 next

  2144   show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}"

  2145     using subtree_def by fastforce

  2146 next

  2147   show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s"

  2148     using assms

  2149     by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq 

  2150         node.inject(1) rtranclD subsetI subtree_def trancl_domain) 

  2151 qed

  2152 

  2153 lemma max_cp_eq: 

  2154   shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"

  2155   (is "?L = ?R")

  2156 proof -

  2157   have "?L \<le> ?R" 

  2158   proof(cases "threads s = {}")

  2159     case False

  2160     show ?thesis 

  2161       by (rule Max.boundedI, 

  2162           insert cp_le, 

  2163           auto simp:finite_threads False)

  2164   qed auto

  2165   moreover have "?R \<le> ?L"

  2166     by (rule Max_fg_mono, 

  2167         simp add: finite_threads,

  2168         simp add: le_cp the_preced_def)

  2169   ultimately show ?thesis by auto

  2170 qed

  2171 

  2172 lemma max_cp_eq_the_preced:

  2173   shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"

  2174   using max_cp_eq using the_preced_def by presburger 

  2175 

  2176 lemma wf_RAG_converse: 

  2177   shows "wf ((RAG s)^-1)"

  2178 proof(rule finite_acyclic_wf_converse)

  2179   from finite_RAG 

  2180   show "finite (RAG s)" .

  2181 next

  2182   from acyclic_RAG

  2183   show "acyclic (RAG s)" .

  2184 qed

  2185 

  2186 lemma chain_building:

  2187   assumes "node \<in> Domain (RAG s)"

  2188   obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"

  2189 proof -

  2190   from assms have "node \<in> Range ((RAG s)^-1)" by auto

  2191   from wf_base[OF wf_RAG_converse this]

  2192   obtain b where h_b: "(b, node) \<in> ((RAG s)\<inverse>)\<^sup>+" "\<forall>c. (c, b) \<notin> (RAG s)\<inverse>" by auto

  2193   obtain th' where eq_b: "b = Th th'"

  2194   proof(cases b)

  2195     case (Cs cs)

  2196     from h_b(1)[unfolded trancl_converse] 

  2197     have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto

  2198     from tranclE[OF this]

  2199     obtain n where "(n, b) \<in> RAG s" by auto

  2200     from this[unfolded Cs]

  2201     obtain th1 where "waiting s th1 cs"

  2202       by (unfold s_RAG_def, fold waiting_eq, auto)

  2203     from waiting_holding[OF this]

  2204     obtain th2 where "holding s th2 cs" .

  2205     hence "(Cs cs, Th th2) \<in> RAG s"

  2206       by (unfold s_RAG_def, fold holding_eq, auto)

  2207     with h_b(2)[unfolded Cs, rule_format]

  2208     have False by auto

  2209     thus ?thesis by auto

  2210   qed auto

  2211   have "th' \<in> readys s" 

  2212   proof -

  2213     from h_b(2)[unfolded eq_b]

  2214     have "\<forall>cs. \<not> waiting s th' cs"

  2215       by (unfold s_RAG_def, fold waiting_eq, auto)

  2216     moreover have "th' \<in> threads s"

  2217     proof(rule rg_RAG_threads)

  2218       from tranclD[OF h_b(1), unfolded eq_b]

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

  2220       thus "Th th' \<in> Range (RAG s)" by auto

  2221     qed

  2222     ultimately show ?thesis by (auto simp:readys_def)

  2223   qed

  2224   moreover have "(node, Th th') \<in> (RAG s)^+" 

  2225     using h_b(1)[unfolded trancl_converse] eq_b by auto

  2226   ultimately show ?thesis using that by metis

  2227 qed

  2228 

  2229 text {* \noindent

  2230   The following is just an instance of @{text "chain_building"}.

  2231 *}

  2232 lemma th_chain_to_ready:

  2233   assumes th_in: "th \<in> threads s"

  2234   shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"

  2235 proof(cases "th \<in> readys s")

  2236   case True

  2237   thus ?thesis by auto

  2238 next

  2239   case False

  2240   from False and th_in have "Th th \<in> Domain (RAG s)" 

  2241     by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)

  2242   from chain_building [rule_format, OF this]

  2243   show ?thesis by auto

  2244 qed

  2245 

  2246 end

  2247 

  2248 lemma count_rec1 [simp]: 

  2249   assumes "Q e"

  2250   shows "count Q (e#es) = Suc (count Q es)"

  2251   using assms

  2252   by (unfold count_def, auto)

  2253 

  2254 lemma count_rec2 [simp]: 

  2255   assumes "\<not>Q e"

  2256   shows "count Q (e#es) = (count Q es)"

  2257   using assms

  2258   by (unfold count_def, auto)

  2259 

  2260 lemma count_rec3 [simp]: 

  2261   shows "count Q [] =  0"

  2262   by (unfold count_def, auto)

  2263 

  2264 lemma cntP_simp1[simp]:

  2265   "cntP (P th cs'#s) th = cntP s th + 1"

  2266   by (unfold cntP_def, simp)

  2267 

  2268 lemma cntP_simp2[simp]:

  2269   assumes "th' \<noteq> th"

  2270   shows "cntP (P th cs'#s) th' = cntP s th'"

  2271   using assms

  2272   by (unfold cntP_def, simp)

  2273 

  2274 lemma cntP_simp3[simp]:

  2275   assumes "\<not> isP e"

  2276   shows "cntP (e#s) th' = cntP s th'"

  2277   using assms

  2278   by (unfold cntP_def, cases e, simp+)

  2279 

  2280 lemma cntV_simp1[simp]:

  2281   "cntV (V th cs'#s) th = cntV s th + 1"

  2282   by (unfold cntV_def, simp)

  2283 

  2284 lemma cntV_simp2[simp]:

  2285   assumes "th' \<noteq> th"

  2286   shows "cntV (V th cs'#s) th' = cntV s th'"

  2287   using assms

  2288   by (unfold cntV_def, simp)

  2289 

  2290 lemma cntV_simp3[simp]:

  2291   assumes "\<not> isV e"

  2292   shows "cntV (e#s) th' = cntV s th'"

  2293   using assms

  2294   by (unfold cntV_def, cases e, simp+)

  2295 

  2296 lemma cntP_diff_inv:

  2297   assumes "cntP (e#s) th \<noteq> cntP s th"

  2298   shows "isP e \<and> actor e = th"

  2299 proof(cases e)

  2300   case (P th' pty)

  2301   show ?thesis

  2302   by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", 

  2303         insert assms P, auto simp:cntP_def)

  2304 qed (insert assms, auto simp:cntP_def)

  2305   

  2306 lemma cntV_diff_inv:

  2307   assumes "cntV (e#s) th \<noteq> cntV s th"

  2308   shows "isV e \<and> actor e = th"

  2309 proof(cases e)

  2310   case (V th' pty)

  2311   show ?thesis

  2312   by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", 

  2313         insert assms V, auto simp:cntV_def)

  2314 qed (insert assms, auto simp:cntV_def)

  2315 

  2316 lemma children_RAG_alt_def:

  2317   "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"

  2318   by (unfold s_RAG_def, auto simp:children_def holding_eq)

  2319 

  2320 fun the_cs :: "node \<Rightarrow> cs" where

  2321   "the_cs (Cs cs) = cs"

  2322 

  2323 lemma holdents_alt_def:

  2324   "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"

  2325   by (unfold children_RAG_alt_def holdents_def, simp add: image_image)

  2326 

  2327 lemma cntCS_alt_def:

  2328   "cntCS s th = card (children (RAG s) (Th th))"

  2329   apply (unfold children_RAG_alt_def cntCS_def holdents_def)

  2330   by (rule card_image[symmetric], auto simp:inj_on_def)

  2331 

  2332 context valid_trace

  2333 begin

  2334 

  2335 lemma finite_holdents: "finite (holdents s th)"

  2336   by (unfold holdents_alt_def, insert finite_children, auto)

  2337   

  2338 end

  2339 

  2340 context valid_trace_p_w

  2341 begin

  2342 

  2343 lemma holding_s_holder: "holding s holder cs"

  2344   by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)

  2345 

  2346 lemma holding_es_holder: "holding (e#s) holder cs"

  2347   by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto)

  2348 

  2349 lemma holdents_es:

  2350   shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") 

  2351 proof -

  2352   { fix cs'

  2353     assume "cs' \<in> ?L"

  2354     hence h: "holding (e#s) th' cs'" by (auto simp:holdents_def)

  2355     have "holding s th' cs'"

  2356     proof(cases "cs' = cs")

  2357       case True

  2358       from held_unique[OF h[unfolded True] holding_es_holder]

  2359       have "th' = holder" .

  2360       thus ?thesis 

  2361         by (unfold True holdents_def, insert holding_s_holder, simp)

  2362     next

  2363       case False

  2364       hence "wq (e#s) cs' = wq s cs'" by simp

  2365       from h[unfolded s_holding_def, folded wq_def, unfolded this]

  2366       show ?thesis

  2367        by (unfold s_holding_def, fold wq_def, auto)

  2368     qed 

  2369     hence "cs' \<in> ?R" by (auto simp:holdents_def)

  2370   } moreover {

  2371     fix cs'

  2372     assume "cs' \<in> ?R"

  2373     hence h: "holding s th' cs'" by (auto simp:holdents_def)

  2374     have "holding (e#s) th' cs'"

  2375     proof(cases "cs' = cs")

  2376       case True

  2377       from held_unique[OF h[unfolded True] holding_s_holder]

  2378       have "th' = holder" .

  2379       thus ?thesis 

  2380         by (unfold True holdents_def, insert holding_es_holder, simp)

  2381     next

  2382       case False

  2383       hence "wq s cs' = wq (e#s) cs'" by simp

  2384       from h[unfolded s_holding_def, folded wq_def, unfolded this]

  2385       show ?thesis

  2386        by (unfold s_holding_def, fold wq_def, auto)

  2387     qed 

  2388     hence "cs' \<in> ?L" by (auto simp:holdents_def)

  2389   } ultimately show ?thesis by auto

  2390 qed

  2391 

  2392 lemma cntCS_es_th[simp]: "cntCS (e#s) th' = cntCS s th'"

  2393  by (unfold cntCS_def holdents_es, simp)

  2394 

  2395 lemma th_not_ready_es: 

  2396   shows "th \<notin> readys (e#s)"

  2397   using waiting_es_th_cs 

  2398   by (unfold readys_def, auto)

  2399 

  2400 end

  2401   

  2402 context valid_trace_p_h

  2403 begin

  2404 

  2405 lemma th_not_waiting':

  2406   "\<not> waiting (e#s) th cs'"

  2407 proof(cases "cs' = cs")

  2408   case True

  2409   show ?thesis

  2410     by (unfold True s_waiting_def, fold wq_def, unfold wq_es_cs', auto)

  2411 next

  2412   case False

  2413   from th_not_waiting[of cs', unfolded s_waiting_def, folded wq_def]

  2414   show ?thesis