1112 with stp ih h show ?thesis |
1112 with stp ih h show ?thesis |
1113 apply (auto simp:wq_def Let_def) |
1113 apply (auto simp:wq_def Let_def) |
1114 apply (ind_cases "step s (Exit th')") |
1114 apply (ind_cases "step s (Exit th')") |
1115 apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def |
1115 apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def |
1116 s_depend_def s_holding_def cs_holding_def) |
1116 s_depend_def s_holding_def cs_holding_def) |
1117 by (fold wq_def, auto) |
1117 done |
1118 next |
1118 next |
1119 case (V th' cs') |
1119 case (V th' cs') |
1120 show ?thesis |
1120 show ?thesis |
1121 proof(cases "cs' = cs") |
1121 proof(cases "cs' = cs") |
1122 case False |
1122 case False |
1352 assumes vt: "vt (P th cs#s)" |
1352 assumes vt: "vt (P th cs#s)" |
1353 and "wq s cs = []" |
1353 and "wq s cs = []" |
1354 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
1354 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
1355 proof - |
1355 proof - |
1356 from assms show ?thesis |
1356 from assms show ?thesis |
1357 unfolding holdents_def step_depend_p[OF vt] by auto |
1357 unfolding holdents_test step_depend_p[OF vt] by (auto) |
1358 qed |
1358 qed |
1359 |
1359 |
1360 lemma step_holdents_p_eq: |
1360 lemma step_holdents_p_eq: |
1361 fixes th cs s |
1361 fixes th cs s |
1362 assumes vt: "vt (P th cs#s)" |
1362 assumes vt: "vt (P th cs#s)" |
1363 and "wq s cs \<noteq> []" |
1363 and "wq s cs \<noteq> []" |
1364 shows "holdents (P th cs#s) th = holdents s th" |
1364 shows "holdents (P th cs#s) th = holdents s th" |
1365 proof - |
1365 proof - |
1366 from assms show ?thesis |
1366 from assms show ?thesis |
1367 unfolding holdents_def step_depend_p[OF vt] by auto |
1367 unfolding holdents_test step_depend_p[OF vt] by auto |
1368 qed |
1368 qed |
1369 |
1369 |
1370 |
1370 |
1371 lemma finite_holding: |
1371 lemma finite_holding: |
1372 fixes s th cs |
1372 fixes s th cs |
1384 hence "?F (Cs x, Th th) \<in> ?F `(depend s)" by (rule h) |
1384 hence "?F (Cs x, Th th) \<in> ?F `(depend s)" by (rule h) |
1385 moreover have "?F (Cs x, Th th) = x" by simp |
1385 moreover have "?F (Cs x, Th th) = x" by simp |
1386 ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` depend s" by simp |
1386 ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` depend s" by simp |
1387 } thus ?thesis by auto |
1387 } thus ?thesis by auto |
1388 qed |
1388 qed |
1389 ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset) |
1389 ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset) |
1390 qed |
1390 qed |
1391 |
1391 |
1392 lemma cntCS_v_dec: |
1392 lemma cntCS_v_dec: |
1393 fixes s thread cs |
1393 fixes s thread cs |
1394 assumes vtv: "vt (V thread cs#s)" |
1394 assumes vtv: "vt (V thread cs#s)" |
1395 shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" |
1395 shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" |
1396 proof - |
1396 proof - |
1397 from step_back_step[OF vtv] |
1397 from step_back_step[OF vtv] |
1398 have cs_in: "cs \<in> holdents s thread" |
1398 have cs_in: "cs \<in> holdents s thread" |
1399 apply (cases, unfold holdents_def s_depend_def, simp) |
1399 apply (cases, unfold holdents_test s_depend_def, simp) |
1400 by (unfold cs_holding_def s_holding_def wq_def, auto) |
1400 by (unfold cs_holding_def s_holding_def wq_def, auto) |
1401 moreover have cs_not_in: |
1401 moreover have cs_not_in: |
1402 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
1402 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
1403 apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) |
1403 apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) |
1404 apply (unfold holdents_def, unfold step_depend_v[OF vtv], |
1404 apply (unfold holdents_test, unfold step_depend_v[OF vtv], |
1405 auto simp:next_th_def) |
1405 auto simp:next_th_def) |
1406 proof - |
1406 proof - |
1407 fix rest |
1407 fix rest |
1408 assume dst: "distinct (rest::thread list)" |
1408 assume dst: "distinct (rest::thread list)" |
1409 and ne: "rest \<noteq> []" |
1409 and ne: "rest \<noteq> []" |
1490 by (auto simp:readys_def threads.simps s_waiting_def |
1490 by (auto simp:readys_def threads.simps s_waiting_def |
1491 wq_def cs_waiting_def Let_def) |
1491 wq_def cs_waiting_def Let_def) |
1492 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
1492 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
1493 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
1493 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
1494 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
1494 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
1495 unfolding cntCS_def holdents_def |
1495 unfolding cntCS_def holdents_test |
1496 by (simp add:depend_create_unchanged eq_e) |
1496 by (simp add:depend_create_unchanged eq_e) |
1497 { assume "th \<noteq> thread" |
1497 { assume "th \<noteq> thread" |
1498 with eq_readys eq_e |
1498 with eq_readys eq_e |
1499 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
1499 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
1500 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
1500 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
1515 and is_runing: "thread \<in> runing s" |
1515 and is_runing: "thread \<in> runing s" |
1516 and no_hold: "holdents s thread = {}" |
1516 and no_hold: "holdents s thread = {}" |
1517 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
1517 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
1518 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
1518 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
1519 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
1519 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
1520 unfolding cntCS_def holdents_def |
1520 unfolding cntCS_def holdents_test |
1521 by (simp add:depend_exit_unchanged eq_e) |
1521 by (simp add:depend_exit_unchanged eq_e) |
1522 { assume "th \<noteq> thread" |
1522 { assume "th \<noteq> thread" |
1523 with eq_e |
1523 with eq_e |
1524 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
1524 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
1525 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
1525 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
1557 apply (erule_tac x = csa in allE, auto) |
1557 apply (erule_tac x = csa in allE, auto) |
1558 apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) |
1558 apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) |
1559 apply (erule_tac x = cs in allE, auto) |
1559 apply (erule_tac x = cs in allE, auto) |
1560 by (case_tac "(wq_fun (schs s) cs)", auto) |
1560 by (case_tac "(wq_fun (schs s) cs)", auto) |
1561 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
1561 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
1562 apply (simp add:cntCS_def holdents_def) |
1562 apply (simp add:cntCS_def holdents_test) |
1563 by (unfold step_depend_p [OF vtp], auto) |
1563 by (unfold step_depend_p [OF vtp], auto) |
1564 moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" |
1564 moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" |
1565 by (simp add:cntP_def count_def) |
1565 by (simp add:cntP_def count_def) |
1566 moreover from eq_e neq_th have "cntV (e#s) th = cntV s th" |
1566 moreover from eq_e neq_th have "cntV (e#s) th = cntV s th" |
1567 by (simp add:cntV_def count_def) |
1567 by (simp add:cntV_def count_def) |
1592 have "?L = insert cs ?R" by auto |
1592 have "?L = insert cs ?R" by auto |
1593 moreover have "card \<dots> = Suc (card (?R - {cs}))" |
1593 moreover have "card \<dots> = Suc (card (?R - {cs}))" |
1594 proof(rule card_insert) |
1594 proof(rule card_insert) |
1595 from finite_holding [OF vt, of thread] |
1595 from finite_holding [OF vt, of thread] |
1596 show " finite {cs. (Cs cs, Th thread) \<in> depend s}" |
1596 show " finite {cs. (Cs cs, Th thread) \<in> depend s}" |
1597 by (unfold holdents_def, simp) |
1597 by (unfold holdents_test, simp) |
1598 qed |
1598 qed |
1599 moreover have "?R - {cs} = ?R" |
1599 moreover have "?R - {cs} = ?R" |
1600 proof - |
1600 proof - |
1601 have "cs \<notin> ?R" |
1601 have "cs \<notin> ?R" |
1602 proof |
1602 proof |
1607 qed |
1607 qed |
1608 ultimately show ?thesis by auto |
1608 ultimately show ?thesis by auto |
1609 qed |
1609 qed |
1610 thus ?thesis |
1610 thus ?thesis |
1611 apply (unfold eq_e eq_th cntCS_def) |
1611 apply (unfold eq_e eq_th cntCS_def) |
1612 apply (simp add: holdents_def) |
1612 apply (simp add: holdents_test) |
1613 by (unfold step_depend_p [OF vtp], auto simp:True) |
1613 by (unfold step_depend_p [OF vtp], auto simp:True) |
1614 qed |
1614 qed |
1615 moreover from is_runing have "th \<in> readys s" |
1615 moreover from is_runing have "th \<in> readys s" |
1616 by (simp add:runing_def eq_th) |
1616 by (simp add:runing_def eq_th) |
1617 moreover note eq_cnp eq_cnv ih [of th] |
1617 moreover note eq_cnp eq_cnv ih [of th] |
1635 show False by (fold eq_e, auto) |
1635 show False by (fold eq_e, auto) |
1636 qed |
1636 qed |
1637 moreover from is_runing have "th \<in> threads (e#s)" |
1637 moreover from is_runing have "th \<in> threads (e#s)" |
1638 by (unfold eq_e, auto simp:runing_def readys_def eq_th) |
1638 by (unfold eq_e, auto simp:runing_def readys_def eq_th) |
1639 moreover have "cntCS (e # s) th = cntCS s th" |
1639 moreover have "cntCS (e # s) th = cntCS s th" |
1640 apply (unfold cntCS_def holdents_def eq_e step_depend_p[OF vtp]) |
1640 apply (unfold cntCS_def holdents_test eq_e step_depend_p[OF vtp]) |
1641 by (auto simp:False) |
1641 by (auto simp:False) |
1642 moreover note eq_cnp eq_cnv ih[of th] |
1642 moreover note eq_cnp eq_cnv ih[of th] |
1643 moreover from is_runing have "th \<in> readys s" |
1643 moreover from is_runing have "th \<in> readys s" |
1644 by (simp add:runing_def eq_th) |
1644 by (simp add:runing_def eq_th) |
1645 ultimately show ?thesis by auto |
1645 ultimately show ?thesis by auto |
1732 case False |
1732 case False |
1733 have "(th \<in> readys (e # s)) = (th \<in> readys s)" |
1733 have "(th \<in> readys (e # s)) = (th \<in> readys s)" |
1734 apply (insert step_back_vt[OF vtv]) |
1734 apply (insert step_back_vt[OF vtv]) |
1735 by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) |
1735 by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) |
1736 moreover have "cntCS (e#s) th = cntCS s th" |
1736 moreover have "cntCS (e#s) th = cntCS s th" |
1737 apply (insert neq_th, unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) |
1737 apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) |
1738 proof - |
1738 proof - |
1739 have "{csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs \<and> next_th s thread cs th} = |
1739 have "{csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs \<and> next_th s thread cs th} = |
1740 {cs. (Cs cs, Th th) \<in> depend s}" |
1740 {cs. (Cs cs, Th th) \<in> depend s}" |
1741 proof - |
1741 proof - |
1742 from False eq_wq |
1742 from False eq_wq |
1794 moreover have "cntCS (e#s) th = cntCS s th" |
1794 moreover have "cntCS (e#s) th = cntCS s th" |
1795 proof - |
1795 proof - |
1796 from eq_wq and th_in and neq_hd |
1796 from eq_wq and th_in and neq_hd |
1797 have "(holdents (e # s) th) = (holdents s th)" |
1797 have "(holdents (e # s) th) = (holdents s th)" |
1798 apply (unfold eq_e step_depend_v[OF vtv], |
1798 apply (unfold eq_e step_depend_v[OF vtv], |
1799 auto simp:next_th_def eq_set s_depend_def holdents_def wq_def |
1799 auto simp:next_th_def eq_set s_depend_def holdents_test wq_def |
1800 Let_def cs_holding_def) |
1800 Let_def cs_holding_def) |
1801 by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) |
1801 by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) |
1802 thus ?thesis by (simp add:cntCS_def) |
1802 thus ?thesis by (simp add:cntCS_def) |
1803 qed |
1803 qed |
1804 moreover note ih eq_cnp eq_cnv eq_threads |
1804 moreover note ih eq_cnp eq_cnv eq_threads |
1859 show ?thesis . |
1859 show ?thesis . |
1860 qed |
1860 qed |
1861 ultimately show ?thesis using ih by auto |
1861 ultimately show ?thesis using ih by auto |
1862 qed |
1862 qed |
1863 moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" |
1863 moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" |
1864 apply (unfold cntCS_def holdents_def eq_e step_depend_v[OF vtv], auto) |
1864 apply (unfold cntCS_def holdents_test eq_e step_depend_v[OF vtv], auto) |
1865 proof - |
1865 proof - |
1866 show "card {csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs} = |
1866 show "card {csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs} = |
1867 Suc (card {cs. (Cs cs, Th th) \<in> depend s})" |
1867 Suc (card {cs. (Cs cs, Th th) \<in> depend s})" |
1868 (is "card ?A = Suc (card ?B)") |
1868 (is "card ?A = Suc (card ?B)") |
1869 proof - |
1869 proof - |
1901 show ?thesis |
1901 show ?thesis |
1902 proof - |
1902 proof - |
1903 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
1903 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
1904 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
1904 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
1905 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
1905 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
1906 unfolding cntCS_def holdents_def |
1906 unfolding cntCS_def holdents_test |
1907 by (simp add:depend_set_unchanged eq_e) |
1907 by (simp add:depend_set_unchanged eq_e) |
1908 from eq_e have eq_readys: "readys (e#s) = readys s" |
1908 from eq_e have eq_readys: "readys (e#s) = readys s" |
1909 by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, |
1909 by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, |
1910 auto simp:Let_def) |
1910 auto simp:Let_def) |
1911 { assume "th \<noteq> thread" |
1911 { assume "th \<noteq> thread" |
1951 proof(cases) |
1951 proof(cases) |
1952 case (thread_create thread prio) |
1952 case (thread_create thread prio) |
1953 assume eq_e: "e = Create thread prio" |
1953 assume eq_e: "e = Create thread prio" |
1954 and not_in': "thread \<notin> threads s" |
1954 and not_in': "thread \<notin> threads s" |
1955 have "cntCS (e # s) th = cntCS s th" |
1955 have "cntCS (e # s) th = cntCS s th" |
1956 apply (unfold eq_e cntCS_def holdents_def) |
1956 apply (unfold eq_e cntCS_def holdents_test) |
1957 by (simp add:depend_create_unchanged) |
1957 by (simp add:depend_create_unchanged) |
1958 moreover have "th \<notin> threads s" |
1958 moreover have "th \<notin> threads s" |
1959 proof - |
1959 proof - |
1960 from not_in eq_e show ?thesis by simp |
1960 from not_in eq_e show ?thesis by simp |
1961 qed |
1961 qed |
1963 next |
1963 next |
1964 case (thread_exit thread) |
1964 case (thread_exit thread) |
1965 assume eq_e: "e = Exit thread" |
1965 assume eq_e: "e = Exit thread" |
1966 and nh: "holdents s thread = {}" |
1966 and nh: "holdents s thread = {}" |
1967 have eq_cns: "cntCS (e # s) th = cntCS s th" |
1967 have eq_cns: "cntCS (e # s) th = cntCS s th" |
1968 apply (unfold eq_e cntCS_def holdents_def) |
1968 apply (unfold eq_e cntCS_def holdents_test) |
1969 by (simp add:depend_exit_unchanged) |
1969 by (simp add:depend_exit_unchanged) |
1970 show ?thesis |
1970 show ?thesis |
1971 proof(cases "th = thread") |
1971 proof(cases "th = thread") |
1972 case True |
1972 case True |
1973 have "cntCS s th = 0" by (unfold cntCS_def, auto simp:nh True) |
1973 have "cntCS s th = 0" by (unfold cntCS_def, auto simp:nh True) |
1989 moreover from is_runing have "thread \<in> threads s" |
1989 moreover from is_runing have "thread \<in> threads s" |
1990 by (simp add:runing_def readys_def) |
1990 by (simp add:runing_def readys_def) |
1991 ultimately show ?thesis by auto |
1991 ultimately show ?thesis by auto |
1992 qed |
1992 qed |
1993 hence "cntCS (e # s) th = cntCS s th " |
1993 hence "cntCS (e # s) th = cntCS s th " |
1994 apply (unfold cntCS_def holdents_def eq_e) |
1994 apply (unfold cntCS_def holdents_test eq_e) |
1995 by (unfold step_depend_p[OF vtp], auto) |
1995 by (unfold step_depend_p[OF vtp], auto) |
1996 moreover have "cntCS s th = 0" |
1996 moreover have "cntCS s th = 0" |
1997 proof(rule ih) |
1997 proof(rule ih) |
1998 from not_in eq_e show "th \<notin> threads s" by simp |
1998 from not_in eq_e show "th \<notin> threads s" by simp |
1999 qed |
1999 qed |
2032 from wq_threads[OF step_back_vt[OF vtv], OF this] and ni |
2032 from wq_threads[OF step_back_vt[OF vtv], OF this] and ni |
2033 show False by auto |
2033 show False by auto |
2034 qed |
2034 qed |
2035 moreover note neq_th eq_wq |
2035 moreover note neq_th eq_wq |
2036 ultimately have "cntCS (e # s) th = cntCS s th" |
2036 ultimately have "cntCS (e # s) th = cntCS s th" |
2037 by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) |
2037 by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) |
2038 moreover have "cntCS s th = 0" |
2038 moreover have "cntCS s th = 0" |
2039 proof(rule ih) |
2039 proof(rule ih) |
2040 from not_in eq_e show "th \<notin> threads s" by simp |
2040 from not_in eq_e show "th \<notin> threads s" by simp |
2041 qed |
2041 qed |
2042 ultimately show ?thesis by simp |
2042 ultimately show ?thesis by simp |
2046 assume eq_e: "e = Set thread prio" |
2046 assume eq_e: "e = Set thread prio" |
2047 and is_runing: "thread \<in> runing s" |
2047 and is_runing: "thread \<in> runing s" |
2048 from not_in and eq_e have "th \<notin> threads s" by auto |
2048 from not_in and eq_e have "th \<notin> threads s" by auto |
2049 from ih [OF this] and eq_e |
2049 from ih [OF this] and eq_e |
2050 show ?thesis |
2050 show ?thesis |
2051 apply (unfold eq_e cntCS_def holdents_def) |
2051 apply (unfold eq_e cntCS_def holdents_test) |
2052 by (simp add:depend_set_unchanged) |
2052 by (simp add:depend_set_unchanged) |
2053 qed |
2053 qed |
2054 next |
2054 next |
2055 case vt_nil |
2055 case vt_nil |
2056 show ?case |
2056 show ?case |
2057 by (unfold cntCS_def, |
2057 by (unfold cntCS_def, |
2058 auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) |
2058 auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) |
2059 qed |
2059 qed |
2060 qed |
2060 qed |
2061 |
2061 |
2062 lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" |
2062 lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" |
2063 by (auto simp:s_waiting_def cs_waiting_def wq_def) |
2063 by (auto simp:s_waiting_def cs_waiting_def wq_def) |
2423 have "cntCS s th = 0" |
2423 have "cntCS s th = 0" |
2424 by (auto split:if_splits) |
2424 by (auto split:if_splits) |
2425 moreover have "finite {cs. (Cs cs, Th th) \<in> depend s}" |
2425 moreover have "finite {cs. (Cs cs, Th th) \<in> depend s}" |
2426 proof - |
2426 proof - |
2427 from finite_holding[OF vt, of th] show ?thesis |
2427 from finite_holding[OF vt, of th] show ?thesis |
2428 by (simp add:holdents_def) |
2428 by (simp add:holdents_test) |
2429 qed |
2429 qed |
2430 ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}" |
2430 ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}" |
2431 by (unfold cntCS_def holdents_def cs_dependents_def, auto) |
2431 by (unfold cntCS_def holdents_test cs_dependents_def, auto) |
2432 show ?thesis |
2432 show ?thesis |
2433 proof(unfold cs_dependents_def) |
2433 proof(unfold cs_dependents_def) |
2434 { assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}" |
2434 { assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}" |
2435 then obtain th' where "(Th th', Th th) \<in> (depend (wq s))\<^sup>+" by auto |
2435 then obtain th' where "(Th th', Th th) \<in> (depend (wq s))\<^sup>+" by auto |
2436 hence "False" |
2436 hence "False" |
2771 next |
2771 next |
2772 show "g ` A \<subseteq> f ` A" |
2772 show "g ` A \<subseteq> f ` A" |
2773 by (rule image_subsetI, auto intro:h[symmetric]) |
2773 by (rule image_subsetI, auto intro:h[symmetric]) |
2774 qed |
2774 qed |
2775 |
2775 |
|
2776 |
2776 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
2777 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
2777 where "detached s th \<equiv> (Th th \<notin> Field (depend s))" |
2778 where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))" |
2778 |
2779 |
2779 thm Field_def |
2780 |
|
2781 lemma detached_test: |
|
2782 shows "detached s th = (Th th \<notin> Field (depend s))" |
|
2783 apply(simp add: detached_def Field_def) |
|
2784 apply(simp add: s_depend_def) |
|
2785 apply(simp add: s_holding_abv s_waiting_abv) |
|
2786 apply(simp add: Domain_iff Range_iff) |
|
2787 apply(simp add: wq_def) |
|
2788 apply(auto) |
|
2789 done |
2780 |
2790 |
2781 lemma detached_intro: |
2791 lemma detached_intro: |
2782 fixes s th |
2792 fixes s th |
2783 assumes vt: "vt s" |
2793 assumes vt: "vt s" |
2784 and eq_pv: "cntP s th = cntV s th" |
2794 and eq_pv: "cntP s th = cntV s th" |
2794 thus ?thesis |
2804 thus ?thesis |
2795 proof |
2805 proof |
2796 assume "th \<notin> threads s" |
2806 assume "th \<notin> threads s" |
2797 with range_in[OF vt] dm_depend_threads[OF vt] |
2807 with range_in[OF vt] dm_depend_threads[OF vt] |
2798 show ?thesis |
2808 show ?thesis |
2799 by (auto simp:detached_def Field_def Domain_def Range_def) |
2809 by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) |
2800 next |
2810 next |
2801 assume "th \<in> readys s" |
2811 assume "th \<in> readys s" |
2802 moreover have "Th th \<notin> Range (depend s)" |
2812 moreover have "Th th \<notin> Range (depend s)" |
2803 proof - |
2813 proof - |
2804 from card_0_eq [OF finite_holding [OF vt]] and cncs_zero |
2814 from card_0_eq [OF finite_holding [OF vt]] and cncs_zero |
2805 have "holdents s th = {}" |
2815 have "holdents s th = {}" |
2806 by (simp add:cntCS_def) |
2816 by (simp add:cntCS_def) |
2807 thus ?thesis |
2817 thus ?thesis |
2808 apply(auto simp:holdents_def) |
2818 apply(auto simp:holdents_test) |
2809 apply(case_tac a) |
2819 apply(case_tac a) |
2810 apply(auto simp:holdents_def s_depend_def) |
2820 apply(auto simp:holdents_test s_depend_def) |
2811 done |
2821 done |
2812 qed |
2822 qed |
2813 ultimately show ?thesis |
2823 ultimately show ?thesis |
2814 apply (auto simp:detached_def Field_def Domain_def readys_def) |
2824 by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def readys_def) |
2815 apply (case_tac b, auto simp:s_depend_def) |
|
2816 by (erule_tac x = "nat" in allE, simp add: eq_waiting) |
|
2817 qed |
2825 qed |
2818 qed |
2826 qed |
2819 |
2827 |
2820 lemma detached_elim: |
2828 lemma detached_elim: |
2821 fixes s th |
2829 fixes s th |
2827 have eq_pv: " cntP s th = |
2835 have eq_pv: " cntP s th = |
2828 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . |
2836 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . |
2829 have cncs_z: "cntCS s th = 0" |
2837 have cncs_z: "cntCS s th = 0" |
2830 proof - |
2838 proof - |
2831 from dtc have "holdents s th = {}" |
2839 from dtc have "holdents s th = {}" |
2832 by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def) |
2840 unfolding detached_def holdents_test s_depend_def |
|
2841 by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) |
2833 thus ?thesis by (auto simp:cntCS_def) |
2842 thus ?thesis by (auto simp:cntCS_def) |
2834 qed |
2843 qed |
2835 show ?thesis |
2844 show ?thesis |
2836 proof(cases "th \<in> threads s") |
2845 proof(cases "th \<in> threads s") |
2837 case True |
2846 case True |