--- a/prio/PrioG.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/PrioG.thy Sun Feb 12 04:45:20 2012 +0000
@@ -9,7 +9,7 @@
"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
by (auto simp:wq_def Let_def cp_def split:list.splits)
-lemma wq_distinct: "vt step s \<Longrightarrow> distinct (wq s cs)"
+lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
proof(erule_tac vt.induct, simp add:wq_def)
fix s e
assume h1: "step s e"
@@ -44,15 +44,15 @@
qed
qed
-lemma step_back_vt: "vt ccs (e#s) \<Longrightarrow> vt ccs s"
- by(ind_cases "vt ccs (e#s)", simp)
+lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
+ by(ind_cases "vt (e#s)", simp)
-lemma step_back_step: "vt ccs (e#s) \<Longrightarrow> ccs s e"
- by(ind_cases "vt ccs (e#s)", simp)
+lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
+ by(ind_cases "vt (e#s)", simp)
lemma block_pre:
fixes thread cs s
- assumes vt_e: "vt step (e#s)"
+ assumes vt_e: "vt (e#s)"
and s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
@@ -84,7 +84,7 @@
assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
and h2: "q # qs = wq_fun (schs s) cs"
and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
- and vt: "vt step (V th cs # s)"
+ and vt: "vt (V th cs # s)"
from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
moreover have "thread \<in> set qs"
proof -
@@ -104,9 +104,9 @@
qed
qed
-lemma p_pre: "\<lbrakk>vt step ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
+lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (depend s)^+"
-apply (ind_cases "vt step ((P thread cs)#s)")
+apply (ind_cases "vt ((P thread cs)#s)")
apply (ind_cases "step s (P thread cs)")
by auto
@@ -124,10 +124,10 @@
lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
by (cases es, auto)
-inductive_cases evt_cons: "vt cs (a#s)"
+inductive_cases evt_cons: "vt (a#s)"
lemma abs2:
- assumes vt: "vt step (e#s)"
+ assumes vt: "vt (e#s)"
and inq: "thread \<in> set (wq s cs)"
and nh: "thread = hd (wq s cs)"
and qt: "thread \<noteq> hd (wq (e#s) cs)"
@@ -141,7 +141,7 @@
apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)
proof -
fix th qs
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
@@ -166,13 +166,13 @@
qed
qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
+lemma vt_moment: "\<And> t. \<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
proof(induct s, simp)
fix a s t
- assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
- and vt_a: "vt cs (a # s)"
+ assume h: "\<And>t.\<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+ and vt_a: "vt (a # s)"
and le_t: "t \<le> length (a # s)"
- show "vt cs (moment t (a # s))"
+ show "vt (moment t (a # s))"
proof(cases "t = length (a#s)")
case True
from True have "moment t (a#s) = a#s" by simp
@@ -180,9 +180,9 @@
next
case False
with le_t have le_t1: "t \<le> length s" by simp
- from vt_a have "vt cs s"
+ from vt_a have "vt s"
by (erule_tac evt_cons, simp)
- from h [OF this le_t1] have "vt cs (moment t s)" .
+ from h [OF this le_t1] have "vt (moment t s)" .
moreover have "moment t (a#s) = moment t s"
proof -
from moment_app [OF le_t1, of "[a]"]
@@ -198,7 +198,7 @@
lemma waiting_unique_pre:
fixes cs1 cs2 s thread
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
@@ -235,10 +235,10 @@
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- have vt_e: "vt step (e#moment t2 s)"
+ have vt_e: "vt (e#moment t2 s)"
proof -
from vt_moment [OF vt le_t3]
- have "vt step (moment ?t3 s)" .
+ have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
@@ -252,11 +252,11 @@
case False
from block_pre [OF vt_e False h1]
have "e = P thread cs2" .
- with vt_e have "vt step ((P thread cs2)# moment t2 s)" by simp
+ with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
with runing_ready have "thread \<in> readys (moment t2 s)" by auto
with nn1 [rule_format, OF lt12]
- show ?thesis by (simp add:readys_def s_waiting_def, auto)
+ show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
qed
} moreover {
assume lt12: "t2 < t1"
@@ -268,10 +268,10 @@
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have vt_e: "vt step (e#moment t1 s)"
+ have vt_e: "vt (e#moment t1 s)"
proof -
from vt_moment [OF vt le_t3]
- have "vt step (moment ?t3 s)" .
+ have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
@@ -285,11 +285,11 @@
case False
from block_pre [OF vt_e False h1]
have "e = P thread cs1" .
- with vt_e have "vt step ((P thread cs1)# moment t1 s)" by simp
+ with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
with runing_ready have "thread \<in> readys (moment t1 s)" by auto
with nn2 [rule_format, OF lt12]
- show ?thesis by (simp add:readys_def s_waiting_def, auto)
+ show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
qed
} moreover {
assume eqt12: "t1 = t2"
@@ -301,10 +301,10 @@
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have vt_e: "vt step (e#moment t1 s)"
+ have vt_e: "vt (e#moment t1 s)"
proof -
from vt_moment [OF vt le_t3]
- have "vt step (moment ?t3 s)" .
+ have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
@@ -328,15 +328,15 @@
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
- from vt_e and eqt12 have "vt step (e#moment t2 s)" by simp
+ from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
from abs2 [OF this True eq_th h2 h1]
show ?thesis .
next
case False
- have vt_e: "vt step (e#moment t2 s)"
+ have vt_e: "vt (e#moment t2 s)"
proof -
from vt_moment [OF vt le_t3] eqt12
- have "vt step (moment (Suc t2) s)" by auto
+ have "vt (moment (Suc t2) s)" by auto
with eq_m eqt12 show ?thesis by simp
qed
from block_pre [OF vt_e False h1]
@@ -350,18 +350,18 @@
lemma waiting_unique:
fixes s cs1 cs2
- assumes "vt step s"
+ assumes "vt s"
and "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
proof -
from waiting_unique_pre and prems
show ?thesis
- by (auto simp add:s_waiting_def)
+ by (auto simp add: wq_def s_waiting_def)
qed
lemma held_unique:
- assumes "vt step s"
+ assumes "vt s"
and "holding s th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
@@ -512,11 +512,11 @@
lemma step_v_hold_inv[elim_format]:
- "\<And>c t. \<lbrakk>vt step (V th cs # s);
+ "\<And>c t. \<lbrakk>vt (V th cs # s);
\<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
proof -
fix c t
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and nhd: "\<not> holding (wq s) t c"
and hd: "holding (wq (V th cs # s)) t c"
show "next_th s th cs t \<and> c = cs"
@@ -561,12 +561,12 @@
qed
lemma step_v_wait_inv[elim_format]:
- "\<And>t c. \<lbrakk>vt step (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
+ "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
\<rbrakk>
\<Longrightarrow> (next_th s th cs t \<and> cs = c)"
proof -
fix t c
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and nw: "\<not> waiting (wq (V th cs # s)) t c"
and wt: "waiting (wq s) t c"
show "next_th s th cs t \<and> cs = c"
@@ -623,13 +623,13 @@
qed
lemma step_v_not_wait[consumes 3]:
- "\<lbrakk>vt step (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
+ "\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)
lemma step_v_release:
- "\<lbrakk>vt step (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
+ "\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
proof -
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and hd: "holding (wq (V th cs # s)) th cs"
from step_back_step [OF vt] and hd
show "False"
@@ -664,12 +664,12 @@
qed
lemma step_v_get_hold:
- "\<And>th'. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
+ "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
apply (unfold cs_holding_def next_th_def wq_def,
auto simp:Let_def)
proof -
fix rest
- assume vt: "vt step (V th cs # s)"
+ assume vt: "vt (V th cs # s)"
and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
and nrest: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest)
@@ -688,12 +688,12 @@
qed
lemma step_v_release_inv[elim_format]:
-"\<And>c t. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
+"\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
c = cs \<and> t = th"
apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)
proof -
fix a list
- assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+ assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step [OF vt] show "a = th"
proof(cases)
assume "holding s th cs" with eq_wq
@@ -702,7 +702,7 @@
qed
next
fix a list
- assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+ assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step [OF vt] show "a = th"
proof(cases)
assume "holding s th cs" with eq_wq
@@ -712,11 +712,11 @@
qed
lemma step_v_waiting_mono:
- "\<And>t c. \<lbrakk>vt step (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
+ "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
proof -
fix t c
let ?s' = "(V th cs # s)"
- assume vt: "vt step ?s'"
+ assume vt: "vt ?s'"
and wt: "waiting (wq ?s') t c"
show "waiting (wq s) t c"
proof(cases "c = cs")
@@ -772,7 +772,7 @@
lemma step_depend_v:
fixes th::thread
assumes vt:
- "vt step (V th cs#s)"
+ "vt (V th cs#s)"
shows "
depend (V th cs # s) =
depend s - {(Cs cs, Th th)} -
@@ -787,7 +787,7 @@
done
lemma step_depend_p:
- "vt step (P th cs#s) \<Longrightarrow>
+ "vt (P th cs#s) \<Longrightarrow>
depend (P th cs # s) = (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
else depend s \<union> {(Th th, Cs cs)})"
apply(simp only: s_depend_def wq_def)
@@ -816,7 +816,7 @@
lemma acyclic_depend:
fixes s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "acyclic (depend s)"
proof -
from vt show ?thesis
@@ -824,7 +824,7 @@
case (vt_cons s e)
assume ih: "acyclic (depend s)"
and stp: "step s e"
- and vt: "vt step s"
+ and vt: "vt s"
show ?case
proof(cases e)
case (Create th prio)
@@ -835,7 +835,7 @@
with ih show ?thesis by (simp add:depend_exit_unchanged)
next
case (V th cs)
- from V vt stp have vtt: "vt step (V th cs#s)" by auto
+ from V vt stp have vtt: "vt (V th cs#s)" by auto
from step_depend_v [OF this]
have eq_de:
"depend (e # s) =
@@ -849,7 +849,7 @@
proof(cases)
assume "holding s th cs"
hence th_in: "th \<in> set (wq s cs)" and
- eq_hd: "th = hd (wq s cs)" by (unfold s_holding_def, auto)
+ eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
then obtain rest where
eq_wq: "wq s cs = th#rest"
by (cases "wq s cs", auto)
@@ -871,19 +871,19 @@
obtain cs' where eq_x: "x = Cs cs'" by auto
with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
hence wt_th': "waiting s ?th' cs'"
- unfolding s_depend_def s_waiting_def cs_waiting_def by simp
+ unfolding s_depend_def s_waiting_def cs_waiting_def wq_def by simp
hence "cs' = cs"
proof(rule waiting_unique [OF vt])
from eq_wq wq_distinct[OF vt, of cs]
show "waiting s ?th' cs"
- apply (unfold s_waiting_def, auto)
+ apply (unfold s_waiting_def wq_def, auto)
proof -
assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
- and eq_wq: "wq s cs = th # rest"
+ and eq_wq: "wq_fun (schs s) cs = th # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from wq_distinct[OF vt, of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
+ show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
fix x assume "distinct x \<and> set x = set rest"
with False show "x \<noteq> []" by auto
@@ -893,7 +893,7 @@
moreover have "\<dots> = set rest"
proof(rule someI2)
from wq_distinct[OF vt, of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
+ show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
@@ -940,7 +940,7 @@
qed
next
case (P th cs)
- from P vt stp have vtt: "vt step (P th cs#s)" by auto
+ from P vt stp have vtt: "vt (P th cs#s)" by auto
from step_depend_p [OF this] P
have "depend (e # s) =
(if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
@@ -992,7 +992,7 @@
lemma finite_depend:
fixes s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "finite (depend s)"
proof -
from vt show ?thesis
@@ -1000,7 +1000,7 @@
case (vt_cons s e)
assume ih: "finite (depend s)"
and stp: "step s e"
- and vt: "vt step s"
+ and vt: "vt s"
show ?case
proof(cases e)
case (Create th prio)
@@ -1011,7 +1011,7 @@
with ih show ?thesis by (simp add:depend_exit_unchanged)
next
case (V th cs)
- from V vt stp have vtt: "vt step (V th cs#s)" by auto
+ from V vt stp have vtt: "vt (V th cs#s)" by auto
from step_depend_v [OF this]
have eq_de: "depend (e # s) =
depend s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
@@ -1035,7 +1035,7 @@
ultimately show ?thesis by simp
next
case (P th cs)
- from P vt stp have vtt: "vt step (P th cs#s)" by auto
+ from P vt stp have vtt: "vt (P th cs#s)" by auto
from step_depend_p [OF this] P
have "depend (e # s) =
(if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
@@ -1069,7 +1069,7 @@
lemma wf_dep_converse:
fixes s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "wf ((depend s)^-1)"
proof(rule finite_acyclic_wf_converse)
from finite_depend [OF vt]
@@ -1087,7 +1087,7 @@
lemma wq_threads:
fixes s cs
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
@@ -1096,7 +1096,7 @@
case (vt_cons s e)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
- and vt: "vt step s"
+ and vt: "vt s"
and h: "th \<in> set (wq (e # s) cs)"
show ?case
proof(cases e)
@@ -1187,13 +1187,13 @@
qed
qed
-lemma range_in: "\<lbrakk>vt step s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_depend_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
fixes th thread cs rest
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
@@ -1201,19 +1201,21 @@
proof -
from prems show ?thesis
apply (auto simp:readys_def)
- apply (case_tac "cs = csa", simp add:s_waiting_def)
+ apply(simp add:s_waiting_def[folded wq_def])
apply (erule_tac x = csa in allE)
apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
apply (case_tac "csa = cs", simp)
apply (erule_tac x = cs in allE)
+ apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
+ apply(auto simp add: wq_def)
apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
proof -
- assume th_nin: "th \<notin> set rest"
+ assume th_nin: "th \<notin> set rest"
and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
and eq_wq: "wq_fun (schs s) cs = thread # rest"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq[folded wq_def]
+ from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -1223,7 +1225,7 @@
qed
lemma chain_building:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)"
proof -
from wf_dep_converse [OF vt]
@@ -1259,7 +1261,7 @@
case False
from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
with False have "Th th' \<in> Domain (depend s)"
- by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+ by (auto simp:readys_def wq_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
from ih [OF th'_d this]
obtain th'' where
th''_r: "th'' \<in> readys s" and
@@ -1275,7 +1277,7 @@
lemma th_chain_to_ready:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (depend s)^+)"
proof(cases "th \<in> readys s")
@@ -1284,21 +1286,21 @@
next
case False
from False and th_in have "Th th \<in> Domain (depend s)"
- by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+ by (auto simp:readys_def s_waiting_def s_depend_def wq_def cs_waiting_def Domain_def)
from chain_building [rule_format, OF vt this]
show ?thesis by auto
qed
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
- by (unfold s_waiting_def cs_waiting_def, auto)
+ by (unfold s_waiting_def cs_waiting_def wq_def, auto)
lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
- by (unfold s_holding_def cs_holding_def, simp)
+ by (unfold s_holding_def wq_def cs_holding_def, simp)
lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
by (unfold s_holding_def cs_holding_def, auto)
-lemma unique_depend: "\<lbrakk>vt step s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
+lemma unique_depend: "\<lbrakk>vt s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_depend_def, auto, fold waiting_eq holding_eq)
by(auto elim:waiting_unique holding_unique)
@@ -1306,7 +1308,7 @@
by (induct rule:trancl_induct, auto)
lemma dchain_unique:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and th1_d: "(n, Th th1) \<in> (depend s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (depend s)^+"
@@ -1325,7 +1327,7 @@
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
from dd eq_n have "th1 \<notin> readys s"
- by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ by (auto simp:readys_def s_depend_def wq_def s_waiting_def cs_waiting_def)
with th1_r show ?thesis by auto
next
assume "(Th th2, Th th1) \<in> (depend s)\<^sup>+"
@@ -1334,7 +1336,7 @@
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
from dd eq_n have "th2 \<notin> readys s"
- by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
with th2_r show ?thesis by auto
qed
} thus ?thesis by auto
@@ -1343,7 +1345,7 @@
lemma step_holdents_p_add:
fixes th cs s
- assumes vt: "vt step (P th cs#s)"
+ assumes vt: "vt (P th cs#s)"
and "wq s cs = []"
shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
proof -
@@ -1353,7 +1355,7 @@
lemma step_holdents_p_eq:
fixes th cs s
- assumes vt: "vt step (P th cs#s)"
+ assumes vt: "vt (P th cs#s)"
and "wq s cs \<noteq> []"
shows "holdents (P th cs#s) th = holdents s th"
proof -
@@ -1364,7 +1366,7 @@
lemma finite_holding:
fixes s th cs
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
@@ -1385,13 +1387,13 @@
lemma cntCS_v_dec:
fixes s thread cs
- assumes vtv: "vt step (V thread cs#s)"
+ assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
apply (cases, unfold holdents_def s_depend_def, simp)
- by (unfold cs_holding_def s_holding_def, auto)
+ 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])
@@ -1458,14 +1460,14 @@
lemma cnp_cnv_cncs:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s)
then cntCS s th else cntCS s th + 1)"
proof -
from vt show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e)
- assume vt: "vt step s"
+ assume vt: "vt s"
and ih: "\<And>th. cntP s th = cntV s th +
(if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
and stp: "step s e"
@@ -1519,10 +1521,9 @@
(th \<in> readys (s) \<or> th \<notin> threads (s))"
apply (simp add:threads.simps readys_def)
apply (subst s_waiting_def)
- apply (subst (1 2) wq_def)
apply (simp add:Let_def)
apply (subst s_waiting_def, simp)
- by (fold wq_def, simp)
+ done
with eq_cnp eq_cnv eq_cncs ih
have ?thesis by simp
} moreover {
@@ -1539,7 +1540,7 @@
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
- from prems have vtp: "vt step (P thread cs#s)" by auto
+ from prems have vtp: "vt (P thread cs#s)" by auto
show ?thesis
proof -
{ have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1621,7 +1622,7 @@
hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def)
from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" .
hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)"
- by (simp add:s_waiting_def)
+ by (simp add:s_waiting_def wq_def)
moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto
ultimately have "th = hd (wq (e#s) cs)" by blast
with eq_wq have "th = hd (wq s cs @ [th])" by simp
@@ -1644,13 +1645,13 @@
qed
next
case (thread_V thread cs)
- from prems have vtv: "vt step (V thread cs # s)" by auto
+ from prems have vtv: "vt (V thread cs # s)" by auto
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp:s_holding_def)
+ by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
@@ -1693,7 +1694,7 @@
with wq_distinct[OF step_back_vt[OF vtv], of cs]
and eq_wq show False by auto
qed
- thus ?thesis by (simp add:s_waiting_def)
+ thus ?thesis by (simp add:wq_def s_waiting_def)
qed
} moreover {
assume neq_cs: "cs1 \<noteq> cs"
@@ -1708,7 +1709,7 @@
thus ?thesis by (simp add:readys_def)
qed
ultimately show ?thesis
- by (auto simp:s_waiting_def eq_e)
+ by (auto simp:wq_def s_waiting_def eq_e)
qed
} ultimately show "\<not> waiting (e # s) thread cs1" by blast
qed
@@ -1778,7 +1779,7 @@
have "\<not> th \<in> readys s"
apply (auto simp:readys_def s_waiting_def)
apply (rule_tac x = cs in exI, auto)
- by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto)
+ by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
moreover
from eq_wq and th_in and neq_hd
have "\<not> (th \<in> readys (e # s))"
@@ -1844,7 +1845,7 @@
from True eq_wq neq_th th_in
show ?thesis
apply (unfold readys_def s_waiting_def, auto)
- by (rule_tac x = cs in exI, auto)
+ by (rule_tac x = cs in exI, auto simp add: wq_def)
qed
moreover have "th \<in> threads s"
proof -
@@ -1931,14 +1932,14 @@
lemma not_thread_cncs:
fixes th s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and not_in: "th \<notin> threads s"
shows "cntCS s th = 0"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
- assume vt: "vt step s"
+ assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
and stp: "step s e"
and not_in: "th \<notin> threads (e # s)"
@@ -1977,7 +1978,7 @@
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
- from prems have vtp: "vt step (P thread cs#s)" by auto
+ from prems have vtp: "vt (P thread cs#s)" by auto
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
@@ -2005,10 +2006,10 @@
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
- from prems have vtv: "vt step (V thread cs#s)" by auto
+ from prems have vtv: "vt (V thread cs#s)" by auto
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp:s_holding_def)
+ by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
from not_in eq_e eq_wq
have "\<not> next_th s thread cs th"
apply (auto simp:next_th_def)
@@ -2055,11 +2056,11 @@
qed
lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
- by (auto simp:s_waiting_def cs_waiting_def)
+ by (auto simp:s_waiting_def cs_waiting_def wq_def)
lemma dm_depend_threads:
fixes th s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and in_dom: "(Th th) \<in> Domain (depend s)"
shows "th \<in> threads s"
proof -
@@ -2087,7 +2088,7 @@
lemma runing_unique:
fixes th1 th2 s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and runing_1: "th1 \<in> runing s"
and runing_2: "th2 \<in> runing s"
shows "th1 = th2"
@@ -2331,7 +2332,7 @@
lemma cnp_cnv_eq:
fixes th s
- assumes "vt step s"
+ assumes "vt s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
proof -
@@ -2352,7 +2353,7 @@
case (thread_exit thread)
assume eq_e: "e = Exit thread"
and not_holding: "holdents s thread = {}"
- have vt_s: "vt step s" by fact
+ have vt_s: "vt s" by fact
from finite_holding[OF vt_s] have "finite (holdents s thread)" .
with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
@@ -2408,7 +2409,7 @@
by (unfold cs_depend_def s_depend_def, auto)
lemma count_eq_dependents:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and eq_pv: "cntP s th = cntV s th"
shows "dependents (wq s) th = {}"
proof -
@@ -2442,7 +2443,7 @@
lemma dependents_threads:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "dependents (wq s) th \<subseteq> threads s"
proof
{ fix th th'
@@ -2465,13 +2466,13 @@
qed
lemma finite_threads:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "finite (threads s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
- assume vt: "vt step s"
+ assume vt: "vt s"
and step: "step s e"
and ih: "finite (threads s)"
from step
@@ -2518,7 +2519,7 @@
qed
lemma cp_le:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependents_def)
@@ -2541,7 +2542,7 @@
qed
lemma le_cp:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (original_priority th s) (birthtime th s)
@@ -2582,7 +2583,7 @@
qed
lemma max_cp_eq:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
(is "?l = ?r")
proof(cases "threads s = {}")
@@ -2630,7 +2631,7 @@
qed
lemma max_cp_readys_threads_pre:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(unfold max_cp_eq[OF vt])
@@ -2773,7 +2774,7 @@
qed
lemma max_cp_readys_threads:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(cases "threads s = {}")
case True
@@ -2794,7 +2795,7 @@
qed
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
- apply (unfold s_holding_def cs_holding_def, simp)
+ apply (unfold s_holding_def cs_holding_def wq_def, simp)
done
lemma f_image_eq: