1446 shows "th \<in> threads s" |
1446 shows "th \<in> threads s" |
1447 proof - |
1447 proof - |
1448 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto |
1448 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto |
1449 moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto) |
1449 moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto) |
1450 ultimately have "(Th th, Cs cs) \<in> RAG s" by simp |
1450 ultimately have "(Th th, Cs cs) \<in> RAG s" by simp |
1451 hence "th \<in> set (wq s cs)" |
1451 then have "th \<in> set (wq s cs)" |
1452 by (unfold s_RAG_def, auto simp: waiting_raw_def) |
1452 using in_RAG_E s_waiting_def wq_def by auto |
1453 from wq_threads [OF this] show ?thesis . |
1453 then show ?thesis using wq_threads by simp |
1454 qed |
1454 qed |
1455 |
1455 |
1456 lemma rg_RAG_threads: |
1456 lemma rg_RAG_threads: |
1457 assumes "(Th th) \<in> Range (RAG s)" |
1457 assumes "(Th th) \<in> Range (RAG s)" |
1458 shows "th \<in> threads s" |
1458 shows "th \<in> threads s" |
1459 using assms |
1459 using assms |
1460 unfolding s_RAG_def waiting_raw_def holding_raw_def |
1460 apply(erule_tac RangeE) |
1461 using wq_threads by auto |
1461 apply(erule_tac in_RAG_E) |
|
1462 apply(auto) |
|
1463 using s_holding_def wq_def wq_threads by auto |
1462 |
1464 |
1463 lemma RAG_threads: |
1465 lemma RAG_threads: |
1464 assumes "(Th th) \<in> Field (RAG s)" |
1466 assumes "(Th th) \<in> Field (RAG s)" |
1465 shows "th \<in> threads s" |
1467 shows "th \<in> threads s" |
1466 using assms |
1468 using assms |
1591 show ?thesis by simp |
1593 show ?thesis by simp |
1592 next |
1594 next |
1593 case False |
1595 case False |
1594 have "wq (e#s) c = wq s c" using False |
1596 have "wq (e#s) c = wq s c" using False |
1595 by simp |
1597 by simp |
1596 hence "waiting s t c" using assms |
1598 hence "waiting s t c" using assms |
1597 by (simp add: waiting_raw_def waiting_eq) |
1599 by (simp add: s_waiting_def wq_def) |
1598 hence "t \<notin> readys s" by (unfold readys_def, auto) |
1600 hence "t \<notin> readys s" by (unfold readys_def, auto) |
1599 hence "t \<notin> running s" using running_ready by auto |
1601 hence "t \<notin> running s" using running_ready by auto |
1600 with running_th_s[folded otherwise] show ?thesis by auto |
1602 with running_th_s[folded otherwise] show ?thesis by auto |
1601 qed |
1603 qed |
1602 qed |
1604 qed |
1606 and "c \<noteq> cs" |
1608 and "c \<noteq> cs" |
1607 shows "waiting (e#s) t c" |
1609 shows "waiting (e#s) t c" |
1608 proof - |
1610 proof - |
1609 have "wq (e#s) c = wq s c" |
1611 have "wq (e#s) c = wq s c" |
1610 using assms(2) by auto |
1612 using assms(2) by auto |
1611 with assms(1) show ?thesis |
1613 with assms(1) show ?thesis |
1612 unfolding waiting_raw_def waiting_eq by auto |
1614 by (simp add: s_waiting_def wq_def) |
1613 qed |
1615 qed |
1614 |
1616 |
1615 lemma holding_esI2: |
1617 lemma holding_esI2: |
1616 assumes "c \<noteq> cs" |
1618 assumes "c \<noteq> cs" |
1617 and "holding s t c" |
1619 and "holding s t c" |
1695 by (simp add: distinct_rest) |
1697 by (simp add: distinct_rest) |
1696 next |
1698 next |
1697 fix x |
1699 fix x |
1698 assume "distinct x \<and> set x = set rest" |
1700 assume "distinct x \<and> set x = set rest" |
1699 moreover have "t \<in> set rest" |
1701 moreover have "t \<in> set rest" |
1700 using assms(1) unfolding waiting_raw_def waiting_eq wq_s_cs by auto |
1702 using assms(1) s_waiting_def set_ConsD wq_def wq_s_cs by auto |
1701 ultimately show "t \<in> set x" by simp |
1703 ultimately show "t \<in> set x" by simp |
1702 qed |
1704 qed |
1703 moreover have "t \<noteq> hd wq'" |
1705 moreover have "t \<noteq> hd wq'" |
1704 using assms(2) taker_def by auto |
1706 using assms(2) taker_def by auto |
1705 ultimately show ?thesis |
1707 ultimately show ?thesis |
1711 obtains "c \<noteq> cs" "waiting s t c" |
1713 obtains "c \<noteq> cs" "waiting s t c" |
1712 | "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'" |
1714 | "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'" |
1713 proof(cases "c = cs") |
1715 proof(cases "c = cs") |
1714 case False |
1716 case False |
1715 hence "wq (e#s) c = wq s c" by auto |
1717 hence "wq (e#s) c = wq s c" by auto |
1716 with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto |
1718 with assms have "waiting s t c" |
|
1719 by (simp add: s_waiting_def wq_def) |
1717 from that(1)[OF False this] show ?thesis . |
1720 from that(1)[OF False this] show ?thesis . |
1718 next |
1721 next |
1719 case True |
1722 case True |
1720 from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs] |
1723 from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs] |
1721 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto |
1724 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto |
1722 hence "t \<noteq> taker" by (simp add: taker_def) |
1725 hence "t \<noteq> taker" by (simp add: taker_def) |
1723 moreover hence "t \<noteq> th" using assms neq_t_th by blast |
1726 moreover hence "t \<noteq> th" using assms neq_t_th by blast |
1724 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) |
1727 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) |
1725 ultimately have "waiting s t cs" |
1728 ultimately have "waiting s t cs" |
1726 by (metis waiting_raw_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs) |
1729 by (metis list.sel(1) list.set_sel(2) list.simps(3) rest_def s_waiting_def wq_def wq_s_cs) |
1727 show ?thesis using that(2) |
1730 show ?thesis using that(2) |
1728 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto |
1731 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto |
1729 qed |
1732 qed |
1730 |
1733 |
1731 lemma holding_esI1: |
1734 lemma holding_esI1: |
1815 show ?thesis by auto |
1818 show ?thesis by auto |
1816 qed |
1819 qed |
1817 |
1820 |
1818 lemma waiting_esI2: |
1821 lemma waiting_esI2: |
1819 assumes "waiting s t c" |
1822 assumes "waiting s t c" |
1820 shows "waiting (e#s) t c" |
1823 shows "waiting (e # s) t c" |
1821 proof - |
1824 proof - |
1822 have "c \<noteq> cs" using assms |
1825 have "c \<noteq> cs" using assms |
1823 using rest_nil wq_s_cs unfolding waiting_raw_def waiting_eq by auto |
1826 using no_waiter_before by blast |
1824 from waiting_esI1[OF assms this] |
1827 from waiting_esI1[OF assms this] |
1825 show ?thesis . |
1828 show ?thesis . |
1826 qed |
1829 qed |
1827 |
1830 |
1828 lemma waiting_esE: |
1831 lemma waiting_esE: |
1829 assumes "waiting (e#s) t c" |
1832 assumes "waiting (e#s) t c" |
1830 obtains "c \<noteq> cs" "waiting s t c" |
1833 obtains "c \<noteq> cs" "waiting s t c" |
1831 proof(cases "c = cs") |
1834 proof(cases "c = cs") |
1832 case False |
1835 case False |
1833 hence "wq (e#s) c = wq s c" by auto |
1836 hence "wq (e#s) c = wq s c" by auto |
1834 with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto |
1837 with assms have "waiting s t c" |
|
1838 by (simp add: s_waiting_def wq_def) |
1835 from that(1)[OF False this] show ?thesis . |
1839 from that(1)[OF False this] show ?thesis . |
1836 next |
1840 next |
1837 case True |
1841 case True |
1838 from no_waiter_after[OF assms[unfolded True]] |
1842 from no_waiter_after[OF assms[unfolded True]] |
1839 show ?thesis by auto |
1843 show ?thesis by auto |
2050 |
2054 |
2051 lemma waiting_kept: |
2055 lemma waiting_kept: |
2052 assumes "waiting s th' cs'" |
2056 assumes "waiting s th' cs'" |
2053 shows "waiting (e#s) th' cs'" |
2057 shows "waiting (e#s) th' cs'" |
2054 using assms |
2058 using assms |
2055 unfolding th_not_in_wq waiting_eq waiting_raw_def |
2059 by (metis butlast_snoc distinct.simps(2) distinct_singleton hd_append2 |
2056 by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD |
2060 in_set_butlastD s_waiting_def wq_def wq_es_cs wq_neq_simp) |
2057 list.distinct(1) split_list wq_es_cs wq_neq_simp) |
|
2058 |
2061 |
2059 lemma holding_kept: |
2062 lemma holding_kept: |
2060 assumes "holding s th' cs'" |
2063 assumes "holding s th' cs'" |
2061 shows "holding (e#s) th' cs'" |
2064 shows "holding (e#s) th' cs'" |
2062 proof(cases "cs' = cs") |
2065 proof(cases "cs' = cs") |
2187 |
2190 |
2188 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]" |
2191 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]" |
2189 by (simp add: wq_es_cs wq_s_cs) |
2192 by (simp add: wq_es_cs wq_s_cs) |
2190 |
2193 |
2191 lemma waiting_es_th_cs: "waiting (e#s) th cs" |
2194 lemma waiting_es_th_cs: "waiting (e#s) th cs" |
2192 using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding waiting_raw_def by auto |
2195 using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs |
|
2196 by (simp add: s_waiting_def wq_def wq_es_cs) |
2193 |
2197 |
2194 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)" |
2198 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)" |
2195 by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) |
2199 by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) |
2196 |
2200 |
2197 lemma holding_esE: |
2201 lemma holding_esE: |
2200 using assms |
2204 using assms |
2201 proof(cases "cs' = cs") |
2205 proof(cases "cs' = cs") |
2202 case False |
2206 case False |
2203 hence "wq (e#s) cs' = wq s cs'" by simp |
2207 hence "wq (e#s) cs' = wq s cs'" by simp |
2204 with assms show ?thesis using that |
2208 with assms show ?thesis using that |
2205 unfolding holding_raw_def holding_eq by auto |
2209 using s_holding_def wq_def by auto |
2206 next |
2210 next |
2207 case True |
2211 case True |
2208 with assms show ?thesis |
2212 with assms show ?thesis |
2209 using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto |
2213 using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto |
2210 qed |
2214 qed |
2223 qed |
2227 qed |
2224 from that(1)[OF this True] show ?thesis . |
2228 from that(1)[OF this True] show ?thesis . |
2225 next |
2229 next |
2226 case False |
2230 case False |
2227 hence "th' = th \<and> cs' = cs" |
2231 hence "th' = th \<and> cs' = cs" |
2228 by (metis assms waiting_raw_def holder_def list.sel(1) rotate1.simps(2) |
2232 by (metis assms hd_append2 insert_iff list.simps(15) rotate1.simps(2) |
2229 set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp) |
2233 s_waiting_def set_rotate1 wne wq_def wq_es_cs wq_neq_simp) |
2230 with that(2) show ?thesis by metis |
2234 with that(2) show ?thesis by metis |
2231 qed |
2235 qed |
2232 |
2236 |
2233 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R") |
2237 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R") |
2234 proof(rule rel_eqI) |
2238 proof(rule rel_eqI) |
3609 show False |
3613 show False |
3610 proof(cases) |
3614 proof(cases) |
3611 case (thread_P) |
3615 case (thread_P) |
3612 moreover have "(Cs cs, Th th) \<in> RAG s" |
3616 moreover have "(Cs cs, Th th) \<in> RAG s" |
3613 using otherwise th_not_in_wq |
3617 using otherwise th_not_in_wq |
3614 unfolding holding_raw_def holding_eq by auto |
3618 using s_holding_def wq_def by auto |
3615 ultimately show ?thesis by auto |
3619 ultimately show ?thesis by auto |
3616 qed |
3620 qed |
3617 qed |
3621 qed |
3618 |
3622 |
3619 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" |
3623 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" |
5116 proof(rule DomainE) |
5120 proof(rule DomainE) |
5117 fix b |
5121 fix b |
5118 assume "(Th th, b) \<in> RAG s" |
5122 assume "(Th th, b) \<in> RAG s" |
5119 with assms[unfolded readys_def s_waiting_def] |
5123 with assms[unfolded readys_def s_waiting_def] |
5120 show False |
5124 show False |
5121 by (cases b, auto simp: RAG_raw_def s_RAG_abv waiting_raw_def) |
5125 using Collect_disj_eq s_RAG_def s_waiting_abv s_waiting_def wq_def by fastforce |
5122 qed |
5126 qed |
5123 qed |
5127 qed |
5124 |
5128 |
5125 lemma readys_holdents_detached: |
5129 lemma readys_holdents_detached: |
5126 assumes "th \<in> readys s" |
5130 assumes "th \<in> readys s" |