PIPBasics.thy
changeset 128 5d8ec128518b
parent 127 38c6acf03f68
child 129 e3cf792db636
equal deleted inserted replaced
127:38c6acf03f68 128:5d8ec128518b
  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"
  5101   proof(rule RangeE)
  5105   proof(rule RangeE)
  5102     fix a
  5106     fix a
  5103     assume "(a, Th th) \<in> RAG s"
  5107     assume "(a, Th th) \<in> RAG s"
  5104     with assms[unfolded holdents_test]
  5108     with assms[unfolded holdents_test]
  5105     show False
  5109     show False
  5106       by (cases a, auto simp:RAG_raw_def s_RAG_abv)
  5110     using assms children_def holdents_alt_def by fastforce
  5107   qed
  5111   qed
  5108 qed
  5112 qed
  5109 
  5113 
  5110 lemma readys_RAG:
  5114 lemma readys_RAG:
  5111   assumes "th \<in> readys s"
  5115   assumes "th \<in> readys s"
  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"