--- a/PrioG.thy Tue Dec 22 23:13:31 2015 +0800
+++ b/PrioG.thy Wed Jan 06 20:46:14 2016 +0800
@@ -2,6 +2,20 @@
imports PrioGDef
begin
+locale valid_trace =
+ fixes s
+ assumes vt : "vt s"
+
+locale valid_trace_e = valid_trace +
+ fixes e
+ assumes vt_e: "vt (e#s)"
+begin
+
+lemma pip_e: "PIP s e"
+ using vt_e by (cases, simp)
+
+end
+
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
@@ -16,8 +30,30 @@
"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 s \<Longrightarrow> distinct (wq s cs)"
-proof(erule_tac vt.induct, simp add:wq_def)
+context valid_trace
+begin
+
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+ assumes "PP []"
+ and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
+ PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+ shows "PP s"
+proof(rule vt.induct[OF vt])
+ from assms(1) show "PP []" .
+next
+ fix s e
+ assume h: "vt s" "PP s" "PIP s e"
+ show "PP (e # s)"
+ proof(cases rule:assms(2))
+ from h(1) show v1: "valid_trace s" by (unfold_locales, simp)
+ next
+ from h(1,3) have "vt (e#s)" by auto
+ thus "valid_trace (e # s)" by (unfold_locales, simp)
+ qed (insert h, auto)
+qed
+
+lemma wq_distinct: "distinct (wq s cs)"
+proof(rule ind, simp add:wq_def)
fix s e
assume h1: "step s e"
and h2: "distinct (wq s cs)"
@@ -51,6 +87,12 @@
qed
qed
+end
+
+
+context valid_trace_e
+begin
+
text {*
The following lemma shows that only the @{text "P"}
operation can add new thread into waiting queues.
@@ -59,9 +101,7 @@
*}
lemma block_pre:
- fixes thread cs s
- assumes vt_e: "vt (e#s)"
- and s_ni: "thread \<notin> set (wq s cs)"
+ assumes s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
proof -
@@ -85,7 +125,7 @@
by (auto simp:wq_def Let_def split:if_splits)
next
case (V th cs)
- with assms show ?thesis
+ with vt_e assms show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
proof -
fix q qs
@@ -98,7 +138,7 @@
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from wq_distinct [of cs]
and h2[symmetric, folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
@@ -112,6 +152,8 @@
qed
qed
+end
+
text {*
The following lemmas is also obvious and shallow. It says
that only running thread can request for a critical resource
@@ -126,7 +168,6 @@
by auto
lemma abs1:
- fixes e es
assumes ein: "e \<in> set es"
and neq: "hd es \<noteq> hd (es @ [x])"
shows "False"
@@ -141,15 +182,17 @@
inductive_cases evt_cons: "vt (a#s)"
+context valid_trace_e
+begin
+
lemma abs2:
- assumes vt: "vt (e#s)"
- and inq: "thread \<in> set (wq s cs)"
+ assumes inq: "thread \<in> set (wq s cs)"
and nh: "thread = hd (wq s cs)"
and qt: "thread \<noteq> hd (wq (e#s) cs)"
and inq': "thread \<in> set (wq (e#s) cs)"
shows "False"
proof -
- from assms show "False"
+ from vt_e assms show "False"
apply (cases e)
apply ((simp split:if_splits add:Let_def wq_def)[1])+
apply (insert abs1, fast)[1]
@@ -161,13 +204,13 @@
and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
proof -
- from wq_distinct[OF step_back_vt[OF vt], of cs]
+ from wq_distinct[of cs]
and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp
moreover have "thread \<in> set qs"
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from wq_distinct [of cs]
and eq_wq [folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
@@ -181,28 +224,33 @@
qed
qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
-proof(induct s, simp)
- fix a s t
- assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
- and vt_a: "vt (a # s)"
- show "vt (moment t (a # s))"
- proof(cases "t \<ge> length (a#s)")
+end
+
+context valid_trace
+begin
+
+lemma vt_moment: "\<And> t. vt (moment t s)"
+proof(induct rule:ind)
+ case Nil
+ thus ?case by (simp add:vt_nil)
+next
+ case (Cons s e t)
+ show ?case
+ proof(cases "t \<ge> length (e#s)")
case True
- from True have "moment t (a#s) = a#s" by simp
- with vt_a show ?thesis by simp
+ from True have "moment t (e#s) = e#s" by simp
+ thus ?thesis using Cons
+ by (simp add:valid_trace_def)
next
case False
- hence le_t1: "t \<le> length s" by simp
- from vt_a have "vt s"
- by (erule_tac evt_cons, simp)
- from h [OF this] have "vt (moment t s)" .
- moreover have "moment t (a#s) = moment t s"
+ from Cons have "vt (moment t s)" by simp
+ moreover have "moment t (e#s) = moment t s"
proof -
- from moment_app [OF le_t1, of "[a]"]
+ from False have "t \<le> length s" by simp
+ from moment_app [OF this, of "[e]"]
show ?thesis by simp
qed
- ultimately show ?thesis by auto
+ ultimately show ?thesis by simp
qed
qed
@@ -244,9 +292,7 @@
*}
lemma waiting_unique_pre:
- fixes cs1 cs2 s thread
- assumes vt: "vt s"
- and h11: "thread \<in> set (wq s cs1)"
+ assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
and h22: "thread \<noteq> hd (wq s cs2)"
@@ -282,25 +328,26 @@
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 (e#moment t2 s)"
+ have "vt (e#moment t2 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t2 s" "e"
+ by (unfold_locales, auto, cases, simp)
have ?thesis
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
- by auto
- thm abs2
- from abs2 [OF vt_e True eq_th h2 h1]
+ by auto
+ from vt_e.abs2 [OF True eq_th h2 h1]
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre[OF False h1]
have "e = P thread cs2" .
- with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
+ with vt_e.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]
@@ -316,24 +363,26 @@
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 (e#moment t1 s)"
+ have "vt (e#moment t1 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t1 s" e
+ by (unfold_locales, auto, cases, auto)
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
- from abs2 [OF vt_e True eq_th h2 h1]
+ from vt_e.abs2 True eq_th h2 h1
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre [OF False h1]
have "e = P thread cs1" .
- with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
+ with vt_e.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]
@@ -351,20 +400,22 @@
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have vt_e: "vt (e#moment t1 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t1 s" e
+ by (unfold_locales, auto, cases, auto)
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
- from abs2 [OF vt_e True eq_th h2 h1]
+ from vt_e.abs2 [OF True eq_th h2 h1]
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre [OF False h1]
have eq_e1: "e = P thread cs1" .
have lt_t3: "t1 < ?t3" by simp
with eqt12 have "t2 < ?t3" by simp
@@ -377,17 +428,21 @@
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
- from abs2 [OF this True eq_th h2 h1]
+ then interpret vt_e2: valid_trace_e "moment t2 s" e
+ by (unfold_locales, auto, cases, auto)
+ from vt_e2.abs2 [OF True eq_th h2 h1]
show ?thesis .
next
case False
- have vt_e: "vt (e#moment t2 s)"
+ have "vt (e#moment t2 s)"
proof -
- from vt_moment [OF vt] eqt12
+ from vt_moment eqt12
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]
+ then interpret vt_e2: valid_trace_e "moment t2 s" e
+ by (unfold_locales, auto, cases, auto)
+ from vt_e2.block_pre [OF False h1]
have "e = P thread cs2" .
with eq_e1 neq12 show ?thesis by auto
qed
@@ -401,15 +456,15 @@
*}
lemma waiting_unique:
- fixes s cs1 cs2
- assumes "vt s"
- and "waiting s th cs1"
+ assumes "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
using waiting_unique_pre assms
unfolding wq_def s_waiting_def
by auto
+end
+
(* not used *)
text {*
Every thread can only be blocked on one critical resource,
@@ -417,13 +472,10 @@
This fact is much more easier according to our definition.
*}
lemma held_unique:
- fixes s::"state"
- assumes "holding s th1 cs"
+ assumes "holding (s::event list) th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
-using assms
-unfolding s_holding_def
-by auto
+ by (insert assms, unfold s_holding_def, auto)
lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
@@ -642,6 +694,8 @@
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"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp)
show "next_th s th cs t \<and> cs = c"
proof(cases "cs = c")
case False
@@ -659,7 +713,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+ from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -673,7 +727,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+ from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -704,6 +758,8 @@
proof -
assume vt: "vt (V th cs # s)"
and hd: "holding (wq (V th cs # s)) th cs"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
from step_back_step [OF vt] and hd
show "False"
proof(cases)
@@ -719,7 +775,7 @@
\<in> set (SOME q. distinct q \<and> set q = set list)"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -727,7 +783,7 @@
qed
moreover have "distinct (hd (SOME q. distinct q \<and> set q = set list) # list)"
proof -
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show ?thesis by auto
qed
moreover note eq_wq and hd_in
@@ -747,9 +803,11 @@
and nrest: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest)
\<notin> set (SOME q. distinct q \<and> set q = set rest)"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume "distinct x \<and> set x = set rest"
@@ -791,6 +849,8 @@
let ?s' = "(V th cs # s)"
assume vt: "vt ?s'"
and wt: "waiting (wq ?s') t c"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
show "waiting (wq s) t c"
proof(cases "c = cs")
case False
@@ -809,7 +869,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from vt_v.wq_distinct [of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
@@ -827,7 +887,7 @@
assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
moreover have "\<dots> = set list"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from vt_v.wq_distinct [of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
@@ -836,7 +896,7 @@
qed
ultimately show "t \<in> set list" by simp
qed
- with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+ with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]
show False by auto
qed
qed
@@ -885,19 +945,22 @@
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
+context valid_trace
+begin
+
text {*
The following lemma shows that @{text "RAG"} is acyclic.
The overall structure is by induction on the formation of @{text "vt s"}
and then case analysis on event @{text "e"}, where the non-trivial cases
for those for @{text "V"} and @{text "P"} events.
*}
-lemma acyclic_RAG:
- fixes s
- assumes vt: "vt s"
+lemma acyclic_RAG:
shows "acyclic (RAG s)"
-using assms
+using vt
proof(induct)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume ih: "acyclic (RAG s)"
and stp: "step s e"
and vt: "vt s"
@@ -949,8 +1012,8 @@
hence wt_th': "waiting s ?th' cs'"
unfolding s_RAG_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]
+ proof(rule vt_s.waiting_unique)
+ from eq_wq vt_s.wq_distinct[of cs]
show "waiting s ?th' cs"
apply (unfold s_waiting_def wq_def, auto)
proof -
@@ -958,7 +1021,7 @@
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
+ from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
fix x assume "distinct x \<and> set x = set rest"
@@ -968,7 +1031,7 @@
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and eq_wq
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
@@ -980,7 +1043,7 @@
and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # 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
+ from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume "distinct x \<and> set x = set rest"
@@ -990,7 +1053,7 @@
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and eq_wq
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
@@ -1066,14 +1129,14 @@
qed
-lemma finite_RAG:
- fixes s
- assumes vt: "vt s"
+lemma finite_RAG:
shows "finite (RAG s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume ih: "finite (RAG s)"
and stp: "step s e"
and vt: "vt s"
@@ -1145,32 +1208,35 @@
text {* Several useful lemmas *}
lemma wf_dep_converse:
- fixes s
- assumes vt: "vt s"
shows "wf ((RAG s)^-1)"
proof(rule finite_acyclic_wf_converse)
- from finite_RAG [OF vt]
+ from finite_RAG
show "finite (RAG s)" .
next
- from acyclic_RAG[OF vt]
+ from acyclic_RAG
show "acyclic (RAG s)" .
qed
+end
+
lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
-by (induct l, auto)
+ by (induct l, auto)
lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s"
by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
+context valid_trace
+begin
+
lemma wq_threads:
- fixes s cs
- assumes vt: "vt s"
- and h: "th \<in> set (wq s cs)"
+ assumes h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
from vt and h show ?thesis
proof(induct arbitrary: th cs)
case (vt_cons s e)
+ interpret vt_s: valid_trace s
+ using vt_cons(1) by (unfold_locales, auto)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
and vt: "vt s"
@@ -1227,7 +1293,7 @@
assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set 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 vt_s.wq_distinct[of cs'] and eq_wq[folded 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"
@@ -1264,14 +1330,13 @@
qed
qed
-lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_RAG_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
fixes th thread cs rest
- assumes vt: "vt s"
- and neq_th: "th \<noteq> thread"
+ assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
@@ -1292,7 +1357,7 @@
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, unfolded wq_def] and eq_wq[unfolded wq_def]
+ from wq_distinct[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
@@ -1308,10 +1373,9 @@
*}
lemma chain_building:
- assumes vt: "vt s"
shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
proof -
- from wf_dep_converse [OF vt]
+ from wf_dep_converse
have h: "wf ((RAG s)\<inverse>)" .
show ?thesis
proof(induct rule:wf_induct [OF h])
@@ -1342,7 +1406,7 @@
from True and th'_d show ?thesis by auto
next
case False
- from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
+ from th'_d and range_in have "th' \<in> threads s" by auto
with False have "Th th' \<in> Domain (RAG s)"
by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def)
from ih [OF th'_d this]
@@ -1362,9 +1426,7 @@
The following is just an instance of @{text "chain_building"}.
*}
lemma th_chain_to_ready:
- fixes s th
- assumes vt: "vt s"
- and th_in: "th \<in> threads s"
+ assumes th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
proof(cases "th \<in> readys s")
case True
@@ -1373,10 +1435,12 @@
case False
from False and th_in have "Th th \<in> Domain (RAG s)"
by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)
- from chain_building [rule_format, OF vt this]
+ from chain_building [rule_format, OF this]
show ?thesis by auto
qed
+end
+
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
by (unfold s_waiting_def cs_waiting_def wq_def, auto)
@@ -1386,16 +1450,24 @@
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_RAG: "\<lbrakk>vt s; (n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
+context valid_trace
+begin
+
+lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
by(auto elim:waiting_unique holding_unique)
+end
+
+
lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
by (induct rule:trancl_induct, auto)
+context valid_trace
+begin
+
lemma dchain_unique:
- assumes vt: "vt s"
- and th1_d: "(n, Th th1) \<in> (RAG s)^+"
+ assumes th1_d: "(n, Th th1) \<in> (RAG s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (RAG s)^+"
and th2_r: "th2 \<in> readys s"
@@ -1403,7 +1475,7 @@
proof -
{ assume neq: "th1 \<noteq> th2"
hence "Th th1 \<noteq> Th th2" by simp
- from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt]
+ from unique_chain [OF _ th1_d th2_d this] and unique_RAG
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
hence "False"
proof
@@ -1427,6 +1499,8 @@
qed
} thus ?thesis by auto
qed
+
+end
lemma step_holdents_p_add:
@@ -1450,13 +1524,11 @@
qed
-lemma finite_holding:
- fixes s th cs
- assumes vt: "vt s"
+lemma (in valid_trace) finite_holding :
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
- from finite_RAG [OF vt]
+ from finite_RAG
have "finite (RAG s)" .
hence "finite (?F `(RAG s))" by simp
moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>"
@@ -1476,13 +1548,17 @@
assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
+ from vtv interpret vt_s: valid_trace s
+ by (cases, unfold_locales, simp)
+ from vtv interpret vt_v: valid_trace "V thread cs#s"
+ by (unfold_locales, simp)
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
apply (cases, unfold holdents_test s_RAG_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 (insert vt_s.wq_distinct[of cs])
apply (unfold holdents_test, unfold step_RAG_v[OF vtv],
auto simp:next_th_def)
proof -
@@ -1536,7 +1612,7 @@
moreover have "card \<dots> =
Suc (card ((holdents (V thread cs#s) thread) - {cs}))"
proof(rule card_insert)
- from finite_holding [OF vtv]
+ from vt_v.finite_holding
show " finite (holdents (V thread cs # s) thread)" .
qed
moreover from cs_not_in
@@ -1544,20 +1620,22 @@
ultimately show ?thesis by (simp add:cntCS_def)
qed
+context valid_trace
+begin
+
text {* (* ddd *) \noindent
The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
of one particular thread.
*}
lemma cnp_cnv_cncs:
- fixes s th
- 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)
+ interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp)
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)"
@@ -1571,7 +1649,7 @@
proof -
{ fix cs
assume "thread \<in> set (wq s cs)"
- from wq_threads [OF vt this] have "thread \<in> threads s" .
+ from vt_s.wq_threads [OF this] have "thread \<in> threads s" .
with not_in have "False" by simp
} with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}"
by (auto simp:readys_def threads.simps s_waiting_def
@@ -1632,6 +1710,8 @@
and is_runing: "thread \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
+ then interpret vt_p: valid_trace "(P thread cs#s)"
+ by (unfold_locales, simp)
show ?thesis
proof -
{ have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1679,7 +1759,7 @@
have "?L = insert cs ?R" by auto
moreover have "card \<dots> = Suc (card (?R - {cs}))"
proof(rule card_insert)
- from finite_holding [OF vt, of thread]
+ from vt_s.finite_holding [of thread]
show " finite {cs. (Cs cs, Th thread) \<in> RAG s}"
by (unfold holdents_test, simp)
qed
@@ -1718,7 +1798,7 @@
ultimately have "th = hd (wq (e#s) cs)" by blast
with eq_wq have "th = hd (wq s cs @ [th])" by simp
hence "th = hd (wq s cs)" using False by auto
- with False eq_wq wq_distinct [OF vtp, of cs]
+ with False eq_wq vt_p.wq_distinct [of cs]
show False by (fold eq_e, auto)
qed
moreover from is_runing have "th \<in> threads (e#s)"
@@ -1737,6 +1817,7 @@
next
case (thread_V thread cs)
from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
+ then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp)
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
@@ -1746,8 +1827,9 @@
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)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
+ from vt_v.wq_distinct[of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest"
+ by (metis distinct.simps(2) vt_s.wq_distinct)
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
@@ -1782,8 +1864,9 @@
proof -
assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)"
with eq_set have "thread \<in> set rest" by simp
- with wq_distinct[OF step_back_vt[OF vtv], of cs]
- and eq_wq show False by auto
+ with vt_v.wq_distinct[of cs]
+ and eq_wq show False
+ by (metis distinct.simps(2) vt_s.wq_distinct)
qed
thus ?thesis by (simp add:wq_def s_waiting_def)
qed
@@ -1819,7 +1902,7 @@
case False
have "(th \<in> readys (e # s)) = (th \<in> readys s)"
apply (insert step_back_vt[OF vtv])
- by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
+ by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq)
moreover have "cntCS (e#s) th = cntCS s th"
apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
proof -
@@ -1838,7 +1921,7 @@
" by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+ from vt_s.wq_distinct[ of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume "distinct x \<and> set x = set rest"
@@ -1870,7 +1953,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 simp add: wq_def)
+ by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def)
moreover
from eq_wq and th_in and neq_hd
have "\<not> (th \<in> readys (e # s))"
@@ -1885,7 +1968,7 @@
apply (unfold eq_e step_RAG_v[OF vtv],
auto simp:next_th_def eq_set s_RAG_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)
+ by (insert vt_s.wq_distinct[of cs], auto simp:wq_def)
thus ?thesis by (simp add:cntCS_def)
qed
moreover note ih eq_cnp eq_cnv eq_threads
@@ -1902,7 +1985,7 @@
assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
show "?t \<in> threads s"
- proof(rule wq_threads[OF step_back_vt[OF vtv]])
+ proof(rule vt_s.wq_threads)
from eq_wq and t_in
show "?t \<in> set (wq s cs)" by (auto simp:wq_def)
qed
@@ -1915,7 +1998,7 @@
show "?t = hd (wq_fun (schs s) csa)"
proof -
{ assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and
+ from vt_s.wq_distinct[of cs] and
eq_wq[folded wq_def] and t_in eq_wq
have "?t \<noteq> thread" by auto
with eq_wq and t_in
@@ -1924,7 +2007,7 @@
from t_in' neq_hd'
have w2: "waiting s ?t csa"
by (auto simp:s_waiting_def wq_def)
- from waiting_unique[OF step_back_vt[OF vtv] w1 w2]
+ from vt_s.waiting_unique[OF w1 w2]
and neq_cs have "False" by auto
} thus ?thesis by auto
qed
@@ -1942,7 +2025,7 @@
proof -
from th_in eq_wq
have "th \<in> set (wq s cs)" by simp
- from wq_threads [OF step_back_vt[OF vtv] this]
+ from vt_s.wq_threads [OF this]
show ?thesis .
qed
ultimately show ?thesis using ih by auto
@@ -1961,7 +2044,7 @@
have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)"
apply (auto simp:image_def)
by (rule_tac x = "(Cs x, Th th)" in bexI, auto)
- with finite_RAG[OF step_back_vt[OF vtv]]
+ with vt_s.finite_RAG
show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset)
next
show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}"
@@ -2022,14 +2105,14 @@
qed
lemma not_thread_cncs:
- fixes th s
- assumes vt: "vt s"
- and not_in: "th \<notin> threads s"
+ assumes 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)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
and stp: "step s e"
@@ -2097,7 +2180,10 @@
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
- from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto
+ from assms thread_V vt stp ih
+ have vtv: "vt (V thread cs#s)" by auto
+ then interpret vt_v: valid_trace "(V thread cs#s)"
+ by (unfold_locales, simp)
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
@@ -2109,15 +2195,18 @@
and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
have "?t \<in> set rest"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
+ from vt_v.wq_distinct[of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest"
+ by (metis distinct.simps(2) vt_s.wq_distinct)
next
fix x assume "distinct x \<and> set x = set rest" with ne
show "hd x \<in> set rest" by (cases x, auto)
qed
with eq_wq have "?t \<in> set (wq s cs)" by simp
- from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
- show False by auto
+ from vt_s.wq_threads[OF this] and ni
+ show False
+ using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)`
+ ni vt_s.wq_threads by blast
qed
moreover note neq_th eq_wq
ultimately have "cntCS (e # s) th = cntCS s th"
@@ -2146,13 +2235,16 @@
qed
qed
+end
+
lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
by (auto simp:s_waiting_def cs_waiting_def wq_def)
+context valid_trace
+begin
+
lemma dm_RAG_threads:
- fixes th s
- assumes vt: "vt s"
- and in_dom: "(Th th) \<in> Domain (RAG s)"
+ assumes in_dom: "(Th th) \<in> Domain (RAG s)"
shows "th \<in> threads s"
proof -
from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
@@ -2160,9 +2252,11 @@
ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
hence "th \<in> set (wq s cs)"
by (unfold s_RAG_def, auto simp:cs_waiting_def)
- from wq_threads [OF vt this] show ?thesis .
+ from wq_threads [OF this] show ?thesis .
qed
+end
+
lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
@@ -2177,11 +2271,11 @@
apply(simp add: Let_def)
done
-(* FIXME: NOT NEEDED *)
+context valid_trace
+begin
+
lemma runing_unique:
- fixes th1 th2 s
- assumes vt: "vt s"
- and runing_1: "th1 \<in> runing s"
+ assumes runing_1: "th1 \<in> runing s"
and runing_2: "th2 \<in> runing s"
shows "th1 = th2"
proof -
@@ -2210,7 +2304,7 @@
by (rule_tac x = "(Th x, Th th1)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2254,7 +2348,7 @@
by (rule_tac x = "(Th x, Th th2)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2289,7 +2383,7 @@
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain)
- from dm_RAG_threads[OF vt this] show ?thesis .
+ from dm_RAG_threads[OF this] show ?thesis .
next
assume "th1' = th1"
with runing_1 show ?thesis
@@ -2304,7 +2398,7 @@
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain)
- from dm_RAG_threads[OF vt this] show ?thesis .
+ from dm_RAG_threads[OF this] show ?thesis .
next
assume "th2' = th2"
with runing_2 show ?thesis
@@ -2366,7 +2460,7 @@
from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
show ?thesis
- proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
+ proof(rule dchain_unique[OF h1 _ h2, symmetric])
from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
from runing_2 show "th2 \<in> readys s" by (simp add:runing_def)
qed
@@ -2375,7 +2469,7 @@
qed
-lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+lemma "card (runing s) \<le> 1"
apply(subgoal_tac "finite (runing s)")
prefer 2
apply (metis finite_nat_set_iff_bounded lessI runing_unique)
@@ -2389,6 +2483,9 @@
apply(auto)
done
+end
+
+
lemma create_pre:
assumes stp: "step s e"
and not_in: "th \<notin> threads s"
@@ -2447,28 +2544,35 @@
from that [OF this] show ?thesis .
qed
+context valid_trace
+begin
+
lemma cnp_cnv_eq:
- fixes th s
- assumes "vt s"
- and "th \<notin> threads s"
+ assumes "th \<notin> threads s"
shows "cntP s th = cntV s th"
- by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+ using assms
+ using cnp_cnv_cncs not_thread_cncs by auto
+
+end
+
lemma eq_RAG:
"RAG (wq s) = RAG s"
by (unfold cs_RAG_def s_RAG_def, auto)
+context valid_trace
+begin
+
lemma count_eq_dependants:
- assumes vt: "vt s"
- and eq_pv: "cntP s th = cntV s th"
+ assumes eq_pv: "cntP s th = cntV s th"
shows "dependants (wq s) th = {}"
proof -
- from cnp_cnv_cncs[OF vt] and eq_pv
+ from cnp_cnv_cncs and eq_pv
have "cntCS s th = 0"
by (auto split:if_splits)
moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}"
proof -
- from finite_holding[OF vt, of th] show ?thesis
+ from finite_holding[of th] show ?thesis
by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}"
@@ -2492,8 +2596,6 @@
qed
lemma dependants_threads:
- fixes s th
- assumes vt: "vt s"
shows "dependants (wq s) th \<subseteq> threads s"
proof
{ fix th th'
@@ -2505,7 +2607,7 @@
with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp
thus ?thesis using eq_RAG by simp
qed
- from dm_RAG_threads[OF vt this]
+ from dm_RAG_threads[OF this]
have "th \<in> threads s" .
} note hh = this
fix th1
@@ -2516,10 +2618,10 @@
qed
lemma finite_threads:
- assumes vt: "vt s"
shows "finite (threads s)"
-using vt
-by (induct) (auto elim: step.cases)
+using vt by (induct) (auto elim: step.cases)
+
+end
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
@@ -2534,9 +2636,11 @@
from fnt and seq show "finite (f ` B)" by auto
qed
+context valid_trace
+begin
+
lemma cp_le:
- assumes vt: "vt s"
- and th_in: "th \<in> threads s"
+ assumes 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_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
@@ -2545,20 +2649,19 @@
proof(rule Max_f_mono)
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
next
- from finite_threads [OF vt]
+ from finite_threads
show "finite (threads s)" .
next
from th_in
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
apply (auto simp:Domain_def)
- apply (rule_tac dm_RAG_threads[OF vt])
+ apply (rule_tac dm_RAG_threads)
apply (unfold trancl_domain [of "RAG s", symmetric])
by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
qed
qed
lemma le_cp:
- assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (priority th s) (last_set th s)
@@ -2579,7 +2682,7 @@
by (rule_tac x = "(Th x, Th th)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2599,7 +2702,6 @@
qed
lemma max_cp_eq:
- 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 = {}")
@@ -2609,26 +2711,26 @@
case False
have "?l \<in> ((cp s) ` threads s)"
proof(rule Max_in)
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` threads s)" by auto
next
from False show "cp s ` threads s \<noteq> {}" by auto
qed
then obtain th
where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
- have "\<dots> \<le> ?r" by (rule cp_le[OF vt th_in])
+ have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
proof -
have "?r \<in> (?f ` ?A)"
proof(rule Max_in)
- from finite_threads[OF vt]
+ from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
next
from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
qed
then obtain th' where
th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
- from le_cp [OF vt, of th'] eq_r
+ from le_cp [of th'] eq_r
have "?r \<le> cp s th'" by auto
moreover have "\<dots> \<le> cp s th"
proof(fold eq_l)
@@ -2637,7 +2739,7 @@
from th_in' show "cp s th' \<in> cp s ` threads s"
by auto
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` threads s)" by auto
qed
qed
@@ -2647,23 +2749,22 @@
qed
lemma max_cp_readys_threads_pre:
- assumes vt: "vt s"
- and np: "threads s \<noteq> {}"
+ assumes np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
-proof(unfold max_cp_eq[OF vt])
+proof(unfold max_cp_eq)
show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
proof -
let ?p = "Max ((\<lambda>th. preced th s) ` threads s)"
let ?f = "(\<lambda>th. preced th s)"
have "?p \<in> ((\<lambda>th. preced th s) ` threads s)"
proof(rule Max_in)
- from finite_threads[OF vt] show "finite (?f ` threads s)" by simp
+ from finite_threads show "finite (?f ` threads s)" by simp
next
from np show "?f ` threads s \<noteq> {}" by simp
qed
then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"
by (auto simp:Image_def)
- from th_chain_to_ready [OF vt tm_in]
+ from th_chain_to_ready [OF tm_in]
have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .
thus ?thesis
proof
@@ -2672,7 +2773,7 @@
and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
- from dependants_threads[OF vt] finite_threads[OF vt]
+ from dependants_threads finite_threads
show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
by (auto intro:finite_subset)
next
@@ -2680,10 +2781,10 @@
from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
moreover have "p \<le> \<dots>"
proof(rule Max_ge)
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- from p_in and th'_in and dependants_threads[OF vt, of th']
+ from p_in and th'_in and dependants_threads[of th']
show "p \<in> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
@@ -2710,18 +2811,18 @@
apply (unfold cp_eq_cpreced cpreced_def)
apply (rule Max_mono)
proof -
- from dependants_threads [OF vt, of th1] th1_in
+ from dependants_threads [of th1] th1_in
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
(\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
next
- from finite_threads[OF vt]
+ from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
from th'_in
@@ -2741,16 +2842,16 @@
assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
- from hy' dependants_threads[OF vt, of tm]
+ from hy' dependants_threads[of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
} with hy show ?thesis by auto
qed
next
- from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+ from dependants_threads[of tm] finite_threads
show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
by (auto intro:finite_subset)
next
@@ -2761,7 +2862,7 @@
proof(rule Max_eqI)
from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
fix y assume "y \<in> cp s ` readys s"
@@ -2771,13 +2872,13 @@
apply(unfold cp_eq_p h)
apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
proof -
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
by simp
next
- from dependants_threads[OF vt, of th1] th1_readys
+ from dependants_threads[of th1] th1_readys
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
\<subseteq> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
@@ -2794,7 +2895,6 @@
there must be one inside it has the maximum precedence of the whole system.
*}
lemma max_cp_readys_threads:
- assumes vt: "vt s"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(cases "threads s = {}")
case True
@@ -2802,9 +2902,10 @@
by (auto simp:readys_def)
next
case False
- show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
+ show ?thesis by (rule max_cp_readys_threads_pre[OF False])
qed
+end
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
apply (unfold s_holding_def cs_holding_def wq_def, simp)
@@ -2836,13 +2937,14 @@
apply(auto)
done
+context valid_trace
+begin
+
lemma detached_intro:
- fixes s th
- assumes vt: "vt s"
- and eq_pv: "cntP s th = cntV s th"
+ assumes eq_pv: "cntP s th = cntV s th"
shows "detached s th"
proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
have eq_cnt: "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)" .
hence cncs_zero: "cntCS s th = 0"
@@ -2852,14 +2954,14 @@
thus ?thesis
proof
assume "th \<notin> threads s"
- with range_in[OF vt] dm_RAG_threads[OF vt]
+ with range_in dm_RAG_threads
show ?thesis
by (auto simp add: detached_def s_RAG_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 (RAG s)"
proof -
- from card_0_eq [OF finite_holding [OF vt]] and cncs_zero
+ from card_0_eq [OF finite_holding] and cncs_zero
have "holdents s th = {}"
by (simp add:cntCS_def)
thus ?thesis
@@ -2874,12 +2976,10 @@
qed
lemma detached_elim:
- fixes s th
- assumes vt: "vt s"
- and dtc: "detached s th"
+ assumes dtc: "detached s th"
shows "cntP s th = cntV s th"
proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
have eq_pv: " 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)" .
have cncs_z: "cntCS s th = 0"
@@ -2904,11 +3004,11 @@
qed
lemma detached_eq:
- fixes s th
- assumes vt: "vt s"
shows "(detached s th) = (cntP s th = cntV s th)"
by (insert vt, auto intro:detached_intro detached_elim)
+end
+
text {*
The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
from the concise and miniature model of PIP given in PrioGDef.thy.
@@ -2923,5 +3023,29 @@
shows "th1 = th2"
using assms by (unfold next_th_def, auto)
-
+lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+ apply (induct s, simp)
+proof -
+ fix a s
+ assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+ and eq_as: "a # s \<noteq> []"
+ show "last_set th (a # s) < length (a # s)"
+ proof(cases "s \<noteq> []")
+ case False
+ from False show ?thesis
+ by (cases a, auto simp:last_set.simps)
+ next
+ case True
+ from ih [OF True] show ?thesis
+ by (cases a, auto simp:last_set.simps)
+ qed
+qed
+
+lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
+ by (induct s, auto simp:threads.simps)
+
+lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
+ apply (drule_tac th_in_ne)
+ by (unfold preced_def, auto intro: birth_time_lt)
+
end