--- a/prio/PrioG.thy Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/PrioG.thy Mon Apr 30 15:32:34 2012 +0000
@@ -1114,7 +1114,7 @@
apply (ind_cases "step s (Exit th')")
apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def
s_depend_def s_holding_def cs_holding_def)
- by (fold wq_def, auto)
+ done
next
case (V th' cs')
show ?thesis
@@ -1354,7 +1354,7 @@
shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
proof -
from assms show ?thesis
- unfolding holdents_def step_depend_p[OF vt] by auto
+ unfolding holdents_test step_depend_p[OF vt] by (auto)
qed
lemma step_holdents_p_eq:
@@ -1364,7 +1364,7 @@
shows "holdents (P th cs#s) th = holdents s th"
proof -
from assms show ?thesis
- unfolding holdents_def step_depend_p[OF vt] by auto
+ unfolding holdents_test step_depend_p[OF vt] by auto
qed
@@ -1386,7 +1386,7 @@
ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` depend s" by simp
} thus ?thesis by auto
qed
- ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset)
+ ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset)
qed
lemma cntCS_v_dec:
@@ -1396,12 +1396,12 @@
proof -
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
- apply (cases, unfold holdents_def s_depend_def, simp)
+ apply (cases, unfold holdents_test s_depend_def, simp)
by (unfold cs_holding_def s_holding_def wq_def, auto)
moreover have cs_not_in:
"(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
- apply (unfold holdents_def, unfold step_depend_v[OF vtv],
+ apply (unfold holdents_test, unfold step_depend_v[OF vtv],
auto simp:next_th_def)
proof -
fix rest
@@ -1492,7 +1492,7 @@
from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
have eq_cncs: "cntCS (e#s) th = cntCS s th"
- unfolding cntCS_def holdents_def
+ unfolding cntCS_def holdents_test
by (simp add:depend_create_unchanged eq_e)
{ assume "th \<noteq> thread"
with eq_readys eq_e
@@ -1517,7 +1517,7 @@
from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
have eq_cncs: "cntCS (e#s) th = cntCS s th"
- unfolding cntCS_def holdents_def
+ unfolding cntCS_def holdents_test
by (simp add:depend_exit_unchanged eq_e)
{ assume "th \<noteq> thread"
with eq_e
@@ -1559,7 +1559,7 @@
apply (erule_tac x = cs in allE, auto)
by (case_tac "(wq_fun (schs s) cs)", auto)
moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
- apply (simp add:cntCS_def holdents_def)
+ apply (simp add:cntCS_def holdents_test)
by (unfold step_depend_p [OF vtp], auto)
moreover from eq_e neq_th have "cntP (e # s) th = cntP s th"
by (simp add:cntP_def count_def)
@@ -1594,7 +1594,7 @@
proof(rule card_insert)
from finite_holding [OF vt, of thread]
show " finite {cs. (Cs cs, Th thread) \<in> depend s}"
- by (unfold holdents_def, simp)
+ by (unfold holdents_test, simp)
qed
moreover have "?R - {cs} = ?R"
proof -
@@ -1609,7 +1609,7 @@
qed
thus ?thesis
apply (unfold eq_e eq_th cntCS_def)
- apply (simp add: holdents_def)
+ apply (simp add: holdents_test)
by (unfold step_depend_p [OF vtp], auto simp:True)
qed
moreover from is_runing have "th \<in> readys s"
@@ -1637,7 +1637,7 @@
moreover from is_runing have "th \<in> threads (e#s)"
by (unfold eq_e, auto simp:runing_def readys_def eq_th)
moreover have "cntCS (e # s) th = cntCS s th"
- apply (unfold cntCS_def holdents_def eq_e step_depend_p[OF vtp])
+ apply (unfold cntCS_def holdents_test eq_e step_depend_p[OF vtp])
by (auto simp:False)
moreover note eq_cnp eq_cnv ih[of th]
moreover from is_runing have "th \<in> readys s"
@@ -1734,7 +1734,7 @@
apply (insert step_back_vt[OF vtv])
by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
moreover have "cntCS (e#s) th = cntCS s th"
- apply (insert neq_th, unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+ apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
proof -
have "{csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs \<and> next_th s thread cs th} =
{cs. (Cs cs, Th th) \<in> depend s}"
@@ -1796,7 +1796,7 @@
from eq_wq and th_in and neq_hd
have "(holdents (e # s) th) = (holdents s th)"
apply (unfold eq_e step_depend_v[OF vtv],
- auto simp:next_th_def eq_set s_depend_def holdents_def wq_def
+ auto simp:next_th_def eq_set s_depend_def holdents_test wq_def
Let_def cs_holding_def)
by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def)
thus ?thesis by (simp add:cntCS_def)
@@ -1861,7 +1861,7 @@
ultimately show ?thesis using ih by auto
qed
moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th"
- apply (unfold cntCS_def holdents_def eq_e step_depend_v[OF vtv], auto)
+ apply (unfold cntCS_def holdents_test eq_e step_depend_v[OF vtv], auto)
proof -
show "card {csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs} =
Suc (card {cs. (Cs cs, Th th) \<in> depend s})"
@@ -1903,7 +1903,7 @@
from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
have eq_cncs: "cntCS (e#s) th = cntCS s th"
- unfolding cntCS_def holdents_def
+ unfolding cntCS_def holdents_test
by (simp add:depend_set_unchanged eq_e)
from eq_e have eq_readys: "readys (e#s) = readys s"
by (simp add:readys_def cs_waiting_def s_waiting_def wq_def,
@@ -1930,7 +1930,7 @@
case vt_nil
show ?case
by (unfold cntP_def cntV_def cntCS_def,
- auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+ auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
qed
qed
@@ -1953,7 +1953,7 @@
assume eq_e: "e = Create thread prio"
and not_in': "thread \<notin> threads s"
have "cntCS (e # s) th = cntCS s th"
- apply (unfold eq_e cntCS_def holdents_def)
+ apply (unfold eq_e cntCS_def holdents_test)
by (simp add:depend_create_unchanged)
moreover have "th \<notin> threads s"
proof -
@@ -1965,7 +1965,7 @@
assume eq_e: "e = Exit thread"
and nh: "holdents s thread = {}"
have eq_cns: "cntCS (e # s) th = cntCS s th"
- apply (unfold eq_e cntCS_def holdents_def)
+ apply (unfold eq_e cntCS_def holdents_test)
by (simp add:depend_exit_unchanged)
show ?thesis
proof(cases "th = thread")
@@ -1991,7 +1991,7 @@
ultimately show ?thesis by auto
qed
hence "cntCS (e # s) th = cntCS s th "
- apply (unfold cntCS_def holdents_def eq_e)
+ apply (unfold cntCS_def holdents_test eq_e)
by (unfold step_depend_p[OF vtp], auto)
moreover have "cntCS s th = 0"
proof(rule ih)
@@ -2034,7 +2034,7 @@
qed
moreover note neq_th eq_wq
ultimately have "cntCS (e # s) th = cntCS s th"
- by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+ by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
moreover have "cntCS s th = 0"
proof(rule ih)
from not_in eq_e show "th \<notin> threads s" by simp
@@ -2048,14 +2048,14 @@
from not_in and eq_e have "th \<notin> threads s" by auto
from ih [OF this] and eq_e
show ?thesis
- apply (unfold eq_e cntCS_def holdents_def)
+ apply (unfold eq_e cntCS_def holdents_test)
by (simp add:depend_set_unchanged)
qed
next
case vt_nil
show ?case
by (unfold cntCS_def,
- auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+ auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
qed
qed
@@ -2425,10 +2425,10 @@
moreover have "finite {cs. (Cs cs, Th th) \<in> depend s}"
proof -
from finite_holding[OF vt, of th] show ?thesis
- by (simp add:holdents_def)
+ by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
- by (unfold cntCS_def holdents_def cs_dependents_def, auto)
+ by (unfold cntCS_def holdents_test cs_dependents_def, auto)
show ?thesis
proof(unfold cs_dependents_def)
{ assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
@@ -2773,10 +2773,20 @@
by (rule image_subsetI, auto intro:h[symmetric])
qed
+
definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
- where "detached s th \<equiv> (Th th \<notin> Field (depend s))"
+ where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
+
-thm Field_def
+lemma detached_test:
+ shows "detached s th = (Th th \<notin> Field (depend s))"
+apply(simp add: detached_def Field_def)
+apply(simp add: s_depend_def)
+apply(simp add: s_holding_abv s_waiting_abv)
+apply(simp add: Domain_iff Range_iff)
+apply(simp add: wq_def)
+apply(auto)
+done
lemma detached_intro:
fixes s th
@@ -2796,7 +2806,7 @@
assume "th \<notin> threads s"
with range_in[OF vt] dm_depend_threads[OF vt]
show ?thesis
- by (auto simp:detached_def Field_def Domain_def Range_def)
+ by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff)
next
assume "th \<in> readys s"
moreover have "Th th \<notin> Range (depend s)"
@@ -2805,15 +2815,13 @@
have "holdents s th = {}"
by (simp add:cntCS_def)
thus ?thesis
- apply(auto simp:holdents_def)
+ apply(auto simp:holdents_test)
apply(case_tac a)
- apply(auto simp:holdents_def s_depend_def)
+ apply(auto simp:holdents_test s_depend_def)
done
qed
ultimately show ?thesis
- apply (auto simp:detached_def Field_def Domain_def readys_def)
- apply (case_tac b, auto simp:s_depend_def)
- by (erule_tac x = "nat" in allE, simp add: eq_waiting)
+ by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def readys_def)
qed
qed
@@ -2829,7 +2837,8 @@
have cncs_z: "cntCS s th = 0"
proof -
from dtc have "holdents s th = {}"
- by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def)
+ unfolding detached_def holdents_test s_depend_def
+ by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff)
thus ?thesis by (auto simp:cntCS_def)
qed
show ?thesis