740 |
740 |
741 text {* |
741 text {* |
742 Because @{term "e#s"} is also a valid trace, properties |
742 Because @{term "e#s"} is also a valid trace, properties |
743 derived for valid trace @{term s} also hold on @{term "e#s"}. |
743 derived for valid trace @{term s} also hold on @{term "e#s"}. |
744 *} |
744 *} |
745 sublocale valid_trace_e < vat_es!: valid_trace "e#s" |
745 sublocale valid_trace_e < vat_es: valid_trace "e#s" |
746 using vt_e |
746 using vt_e |
747 by (unfold_locales, simp) |
747 by (unfold_locales, simp) |
748 |
748 |
749 text {* |
749 text {* |
750 For each specific event (or operation), there is a sublocale |
750 For each specific event (or operation), there is a sublocale |
975 derived on any valid state to the prefix of it, with length @{text "i"}. |
975 derived on any valid state to the prefix of it, with length @{text "i"}. |
976 *} |
976 *} |
977 locale valid_moment = valid_trace + |
977 locale valid_moment = valid_trace + |
978 fixes i :: nat |
978 fixes i :: nat |
979 |
979 |
980 sublocale valid_moment < vat_moment!: valid_trace "(moment i s)" |
980 sublocale valid_moment < vat_moment: valid_trace "(moment i s)" |
981 by (unfold_locales, insert vt_moment, auto) |
981 by (unfold_locales, insert vt_moment, auto) |
982 |
982 |
983 locale valid_moment_e = valid_moment + |
983 locale valid_moment_e = valid_moment + |
984 assumes less_i: "i < length s" |
984 assumes less_i: "i < length s" |
985 begin |
985 begin |
993 show ?thesis . |
993 show ?thesis . |
994 qed |
994 qed |
995 |
995 |
996 end |
996 end |
997 |
997 |
998 sublocale valid_moment_e < vat_moment_e!: valid_trace_e "moment i s" "next_e" |
998 sublocale valid_moment_e < vat_moment_e: valid_trace_e "moment i s" "next_e" |
999 using vt_moment[of "Suc i", unfolded trace_e] |
999 using vt_moment[of "Suc i", unfolded trace_e] |
1000 by (unfold_locales, simp) |
1000 by (unfold_locales, simp) |
1001 |
1001 |
1002 section {* Waiting queues are distinct *} |
1002 section {* Waiting queues are distinct *} |
1003 |
1003 |
1466 proof - |
1466 proof - |
1467 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto |
1467 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto |
1468 moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto) |
1468 moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto) |
1469 ultimately have "(Th th, Cs cs) \<in> RAG s" by simp |
1469 ultimately have "(Th th, Cs cs) \<in> RAG s" by simp |
1470 hence "th \<in> set (wq s cs)" |
1470 hence "th \<in> set (wq s cs)" |
1471 by (unfold s_RAG_def, auto simp:cs_waiting_def) |
1471 by (unfold s_RAG_def, auto simp:cs_waiting_raw) |
1472 from wq_threads [OF this] show ?thesis . |
1472 from wq_threads [OF this] show ?thesis . |
1473 qed |
1473 qed |
1474 |
1474 |
1475 lemma rg_RAG_threads: |
1475 lemma rg_RAG_threads: |
1476 assumes "(Th th) \<in> Range (RAG s)" |
1476 assumes "(Th th) \<in> Range (RAG s)" |
1477 shows "th \<in> threads s" |
1477 shows "th \<in> threads s" |
1478 using assms |
1478 using assms |
1479 by (unfold s_RAG_def cs_waiting_def cs_holding_def, |
1479 by (unfold s_RAG_def cs_waiting_raw cs_holding_raw, |
1480 auto intro:wq_threads) |
1480 auto intro:wq_threads) |
1481 |
1481 |
1482 lemma RAG_threads: |
1482 lemma RAG_threads: |
1483 assumes "(Th th) \<in> Field (RAG s)" |
1483 assumes "(Th th) \<in> Field (RAG s)" |
1484 shows "th \<in> threads s" |
1484 shows "th \<in> threads s" |
1611 next |
1611 next |
1612 case False |
1612 case False |
1613 have "wq (e#s) c = wq s c" using False |
1613 have "wq (e#s) c = wq s c" using False |
1614 by simp |
1614 by simp |
1615 hence "waiting s t c" using assms |
1615 hence "waiting s t c" using assms |
1616 by (simp add: cs_waiting_def waiting_eq) |
1616 by (simp add: cs_waiting_raw waiting_eq) |
1617 hence "t \<notin> readys s" by (unfold readys_def, auto) |
1617 hence "t \<notin> readys s" by (unfold readys_def, auto) |
1618 hence "t \<notin> runing s" using runing_ready by auto |
1618 hence "t \<notin> runing s" using runing_ready by auto |
1619 with runing_th_s[folded otherwise] show ?thesis by auto |
1619 with runing_th_s[folded otherwise] show ?thesis by auto |
1620 qed |
1620 qed |
1621 qed |
1621 qed |
1626 shows "waiting (e#s) t c" |
1626 shows "waiting (e#s) t c" |
1627 proof - |
1627 proof - |
1628 have "wq (e#s) c = wq s c" |
1628 have "wq (e#s) c = wq s c" |
1629 using assms(2) by auto |
1629 using assms(2) by auto |
1630 with assms(1) show ?thesis |
1630 with assms(1) show ?thesis |
1631 using cs_waiting_def waiting_eq by auto |
1631 unfolding cs_waiting_raw waiting_eq by auto |
1632 qed |
1632 qed |
1633 |
1633 |
1634 lemma holding_esI2: |
1634 lemma holding_esI2: |
1635 assumes "c \<noteq> cs" |
1635 assumes "c \<noteq> cs" |
1636 and "holding s t c" |
1636 and "holding s t c" |
1714 by (simp add: distinct_rest) |
1714 by (simp add: distinct_rest) |
1715 next |
1715 next |
1716 fix x |
1716 fix x |
1717 assume "distinct x \<and> set x = set rest" |
1717 assume "distinct x \<and> set x = set rest" |
1718 moreover have "t \<in> set rest" |
1718 moreover have "t \<in> set rest" |
1719 using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto |
1719 using assms(1) unfolding cs_waiting_raw waiting_eq wq_s_cs by auto |
1720 ultimately show "t \<in> set x" by simp |
1720 ultimately show "t \<in> set x" by simp |
1721 qed |
1721 qed |
1722 moreover have "t \<noteq> hd wq'" |
1722 moreover have "t \<noteq> hd wq'" |
1723 using assms(2) taker_def by auto |
1723 using assms(2) taker_def by auto |
1724 ultimately show ?thesis |
1724 ultimately show ?thesis |
1730 obtains "c \<noteq> cs" "waiting s t c" |
1730 obtains "c \<noteq> cs" "waiting s t c" |
1731 | "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'" |
1731 | "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'" |
1732 proof(cases "c = cs") |
1732 proof(cases "c = cs") |
1733 case False |
1733 case False |
1734 hence "wq (e#s) c = wq s c" by auto |
1734 hence "wq (e#s) c = wq s c" by auto |
1735 with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto |
1735 with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto |
1736 from that(1)[OF False this] show ?thesis . |
1736 from that(1)[OF False this] show ?thesis . |
1737 next |
1737 next |
1738 case True |
1738 case True |
1739 from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs] |
1739 from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs] |
1740 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto |
1740 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto |
1741 hence "t \<noteq> taker" by (simp add: taker_def) |
1741 hence "t \<noteq> taker" by (simp add: taker_def) |
1742 moreover hence "t \<noteq> th" using assms neq_t_th by blast |
1742 moreover hence "t \<noteq> th" using assms neq_t_th by blast |
1743 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) |
1743 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) |
1744 ultimately have "waiting s t cs" |
1744 ultimately have "waiting s t cs" |
1745 by (metis cs_waiting_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs) |
1745 by (metis cs_waiting_raw insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs) |
1746 show ?thesis using that(2) |
1746 show ?thesis using that(2) |
1747 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto |
1747 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto |
1748 qed |
1748 qed |
1749 |
1749 |
1750 lemma holding_esI1: |
1750 lemma holding_esI1: |
1837 lemma waiting_esI2: |
1837 lemma waiting_esI2: |
1838 assumes "waiting s t c" |
1838 assumes "waiting s t c" |
1839 shows "waiting (e#s) t c" |
1839 shows "waiting (e#s) t c" |
1840 proof - |
1840 proof - |
1841 have "c \<noteq> cs" using assms |
1841 have "c \<noteq> cs" using assms |
1842 using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto |
1842 using rest_nil wq_s_cs unfolding cs_waiting_raw waiting_eq by auto |
1843 from waiting_esI1[OF assms this] |
1843 from waiting_esI1[OF assms this] |
1844 show ?thesis . |
1844 show ?thesis . |
1845 qed |
1845 qed |
1846 |
1846 |
1847 lemma waiting_esE: |
1847 lemma waiting_esE: |
1848 assumes "waiting (e#s) t c" |
1848 assumes "waiting (e#s) t c" |
1849 obtains "c \<noteq> cs" "waiting s t c" |
1849 obtains "c \<noteq> cs" "waiting s t c" |
1850 proof(cases "c = cs") |
1850 proof(cases "c = cs") |
1851 case False |
1851 case False |
1852 hence "wq (e#s) c = wq s c" by auto |
1852 hence "wq (e#s) c = wq s c" by auto |
1853 with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto |
1853 with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto |
1854 from that(1)[OF False this] show ?thesis . |
1854 from that(1)[OF False this] show ?thesis . |
1855 next |
1855 next |
1856 case True |
1856 case True |
1857 from no_waiter_after[OF assms[unfolded True]] |
1857 from no_waiter_after[OF assms[unfolded True]] |
1858 show ?thesis by auto |
1858 show ?thesis by auto |
2069 |
2069 |
2070 lemma waiting_kept: |
2070 lemma waiting_kept: |
2071 assumes "waiting s th' cs'" |
2071 assumes "waiting s th' cs'" |
2072 shows "waiting (e#s) th' cs'" |
2072 shows "waiting (e#s) th' cs'" |
2073 using assms |
2073 using assms |
2074 unfolding th_not_in_wq waiting_eq cs_waiting_def |
2074 unfolding th_not_in_wq waiting_eq cs_waiting_raw |
2075 by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD |
2075 by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD |
2076 list.distinct(1) split_list wq_es_cs wq_neq_simp) |
2076 list.distinct(1) split_list wq_es_cs wq_neq_simp) |
2077 |
2077 |
2078 lemma holding_kept: |
2078 lemma holding_kept: |
2079 assumes "holding s th' cs'" |
2079 assumes "holding s th' cs'" |
2080 shows "holding (e#s) th' cs'" |
2080 shows "holding (e#s) th' cs'" |
2081 proof(cases "cs' = cs") |
2081 proof(cases "cs' = cs") |
2082 case False |
2082 case False |
2083 hence "wq (e#s) cs' = wq s cs'" by simp |
2083 hence "wq (e#s) cs' = wq s cs'" by simp |
2084 with assms show ?thesis using cs_holding_def holding_eq by auto |
2084 with assms show ?thesis unfolding cs_holding_raw holding_eq by auto |
2085 next |
2085 next |
2086 case True |
2086 case True |
2087 from assms[unfolded s_holding_def, folded wq_def] |
2087 from assms[unfolded s_holding_def, folded wq_def] |
2088 obtain rest where eq_wq: "wq s cs' = th'#rest" |
2088 obtain rest where eq_wq: "wq s cs' = th'#rest" |
2089 by (metis empty_iff list.collapse list.set(1)) |
2089 by (metis empty_iff list.collapse list.set(1)) |
2090 hence "wq (e#s) cs' = th'#(rest@[th])" |
2090 hence "wq (e#s) cs' = th'#(rest@[th])" |
2091 by (simp add: True wq_es_cs) |
2091 by (simp add: True wq_es_cs) |
2092 thus ?thesis |
2092 thus ?thesis |
2093 by (simp add: cs_holding_def holding_eq) |
2093 by (simp add: cs_holding_raw holding_eq) |
2094 qed |
2094 qed |
2095 end |
2095 end |
2096 |
2096 |
2097 lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c" |
2097 lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c" |
2098 proof - |
2098 proof - |
2111 lemma holding_es_th_cs: |
2111 lemma holding_es_th_cs: |
2112 shows "holding (e#s) th cs" |
2112 shows "holding (e#s) th cs" |
2113 proof - |
2113 proof - |
2114 from wq_es_cs' |
2114 from wq_es_cs' |
2115 have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto |
2115 have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto |
2116 thus ?thesis using cs_holding_def holding_eq by blast |
2116 thus ?thesis unfolding cs_holding_raw holding_eq by blast |
2117 qed |
2117 qed |
2118 |
2118 |
2119 lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)" |
2119 lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)" |
2120 by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto) |
2120 by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto) |
2121 |
2121 |
2136 have "th' = th" by simp |
2136 have "th' = th" by simp |
2137 from that(2)[OF True this] show ?thesis . |
2137 from that(2)[OF True this] show ?thesis . |
2138 next |
2138 next |
2139 case False |
2139 case False |
2140 have "holding s th' cs'" using assms |
2140 have "holding s th' cs'" using assms |
2141 using False cs_holding_def holding_eq by auto |
2141 using False unfolding cs_holding_raw holding_eq by auto |
2142 from that(1)[OF False this] show ?thesis . |
2142 from that(1)[OF False this] show ?thesis . |
2143 qed |
2143 qed |
2144 |
2144 |
2145 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R") |
2145 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R") |
2146 proof(rule rel_eqI) |
2146 proof(rule rel_eqI) |
2206 |
2206 |
2207 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]" |
2207 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]" |
2208 by (simp add: wq_es_cs wq_s_cs) |
2208 by (simp add: wq_es_cs wq_s_cs) |
2209 |
2209 |
2210 lemma waiting_es_th_cs: "waiting (e#s) th cs" |
2210 lemma waiting_es_th_cs: "waiting (e#s) th cs" |
2211 using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto |
2211 using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding cs_waiting_raw by auto |
2212 |
2212 |
2213 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)" |
2213 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)" |
2214 by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) |
2214 by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) |
2215 |
2215 |
2216 lemma holding_esE: |
2216 lemma holding_esE: |
2218 obtains "holding s th' cs'" |
2218 obtains "holding s th' cs'" |
2219 using assms |
2219 using assms |
2220 proof(cases "cs' = cs") |
2220 proof(cases "cs' = cs") |
2221 case False |
2221 case False |
2222 hence "wq (e#s) cs' = wq s cs'" by simp |
2222 hence "wq (e#s) cs' = wq s cs'" by simp |
2223 with assms show ?thesis |
2223 with assms show ?thesis using that |
2224 using cs_holding_def holding_eq that by auto |
2224 unfolding cs_holding_raw holding_eq by auto |
2225 next |
2225 next |
2226 case True |
2226 case True |
2227 with assms show ?thesis |
2227 with assms show ?thesis |
2228 using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto |
2228 using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto |
2229 qed |
2229 qed |
2242 qed |
2242 qed |
2243 from that(1)[OF this True] show ?thesis . |
2243 from that(1)[OF this True] show ?thesis . |
2244 next |
2244 next |
2245 case False |
2245 case False |
2246 hence "th' = th \<and> cs' = cs" |
2246 hence "th' = th \<and> cs' = cs" |
2247 by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2) |
2247 by (metis assms cs_waiting_raw holder_def list.sel(1) rotate1.simps(2) |
2248 set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp) |
2248 set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp) |
2249 with that(2) show ?thesis by metis |
2249 with that(2) show ?thesis by metis |
2250 qed |
2250 qed |
2251 |
2251 |
2252 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R") |
2252 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R") |
2353 lemma finite_RAG: |
2353 lemma finite_RAG: |
2354 shows "finite (RAG s)" |
2354 shows "finite (RAG s)" |
2355 proof(induct rule:ind) |
2355 proof(induct rule:ind) |
2356 case Nil |
2356 case Nil |
2357 show ?case |
2357 show ?case |
2358 by (auto simp: s_RAG_def cs_waiting_def |
2358 by (auto simp: s_RAG_def cs_waiting_raw |
2359 cs_holding_def wq_def acyclic_def) |
2359 cs_holding_raw wq_def acyclic_def) |
2360 next |
2360 next |
2361 case (Cons s e) |
2361 case (Cons s e) |
2362 interpret vt_e: valid_trace_e s e using Cons by simp |
2362 interpret vt_e: valid_trace_e s e using Cons by simp |
2363 show ?case |
2363 show ?case |
2364 proof(cases e) |
2364 proof(cases e) |
2786 lemma acyclic_RAG: |
2786 lemma acyclic_RAG: |
2787 shows "acyclic (RAG s)" |
2787 shows "acyclic (RAG s)" |
2788 proof(induct rule:ind) |
2788 proof(induct rule:ind) |
2789 case Nil |
2789 case Nil |
2790 show ?case |
2790 show ?case |
2791 by (auto simp: s_RAG_def cs_waiting_def |
2791 by (auto simp: s_RAG_def cs_waiting_raw |
2792 cs_holding_def wq_def acyclic_def) |
2792 cs_holding_raw wq_def acyclic_def) |
2793 next |
2793 next |
2794 case (Cons s e) |
2794 case (Cons s e) |
2795 interpret vt_e: valid_trace_e s e using Cons by simp |
2795 interpret vt_e: valid_trace_e s e using Cons by simp |
2796 show ?case |
2796 show ?case |
2797 proof(cases e) |
2797 proof(cases e) |
3076 case True |
3076 case True |
3077 thus ?thesis by auto |
3077 thus ?thesis by auto |
3078 next |
3078 next |
3079 case False |
3079 case False |
3080 from False and th_in have "Th th \<in> Domain (RAG s)" |
3080 from False and th_in have "Th th \<in> Domain (RAG s)" |
3081 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) |
3081 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_raw Domain_def) |
3082 from chain_building [rule_format, OF this] |
3082 from chain_building [rule_format, OF this] |
3083 show ?thesis by auto |
3083 show ?thesis by auto |
3084 qed |
3084 qed |
3085 |
3085 |
3086 text {* |
3086 text {* |
3626 from pip_e[unfolded is_p] |
3626 from pip_e[unfolded is_p] |
3627 show False |
3627 show False |
3628 proof(cases) |
3628 proof(cases) |
3629 case (thread_P) |
3629 case (thread_P) |
3630 moreover have "(Cs cs, Th th) \<in> RAG s" |
3630 moreover have "(Cs cs, Th th) \<in> RAG s" |
3631 using otherwise cs_holding_def |
3631 using otherwise th_not_in_wq |
3632 holding_eq th_not_in_wq by auto |
3632 unfolding cs_holding_raw holding_eq by auto |
3633 ultimately show ?thesis by auto |
3633 ultimately show ?thesis by auto |
3634 qed |
3634 qed |
3635 qed |
3635 qed |
3636 |
3636 |
3637 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" |
3637 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" |