--- a/CpsG.thy~ Thu Jan 14 00:55:54 2016 +0800
+++ b/CpsG.thy~ Sat Jan 16 10:59:03 2016 +0800
@@ -2,6 +2,19 @@
imports PIPDefs
begin
+lemma Max_f_mono:
+ assumes seq: "A \<subseteq> B"
+ and np: "A \<noteq> {}"
+ and fnt: "finite B"
+ shows "Max (f ` A) \<le> Max (f ` B)"
+proof(rule Max_mono)
+ from seq show "f ` A \<subseteq> f ` B" by auto
+next
+ from np show "f ` A \<noteq> {}" by auto
+next
+ from fnt and seq show "finite (f ` B)" by auto
+qed
+
(* I am going to use this file as a start point to retrofiting
PIPBasics.thy, which is originally called CpsG.ghy *)
@@ -9,6 +22,14 @@
fixes s
assumes vt : "vt s"
+lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
+ 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 wq_def cs_holding_def, simp)
+
+thm s_waiting_def cs_waiting_def wq_def
+
locale valid_trace_e = valid_trace +
fixes e
assumes vt_e: "vt (e#s)"
@@ -224,78 +245,6 @@
end
-text {*
- The following lemmas is also obvious and shallow. It says
- that only running thread can request for a critical resource
- and that the requested resource must be one which is
- not current held by the thread.
-*}
-
-lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
- thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (RAG s)^+"
-apply (ind_cases "vt ((P thread cs)#s)")
-apply (ind_cases "step s (P thread cs)")
-by auto
-
-lemma abs1:
- assumes ein: "e \<in> set es"
- and neq: "hd es \<noteq> hd (es @ [x])"
- shows "False"
-proof -
- from ein have "es \<noteq> []" by auto
- then obtain e ess where "es = e # ess" by (cases es, auto)
- with neq show ?thesis by auto
-qed
-
-lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
- by (cases es, auto)
-
-inductive_cases evt_cons: "vt (a#s)"
-
-context valid_trace_e
-begin
-
-lemma abs2:
- 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 vt_e assms show "False"
- apply (cases e)
- apply ((simp split:if_splits add:Let_def wq_def)[1])+
- apply (insert abs1, fast)[1]
- apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)
- proof -
- fix th qs
- 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"
- proof -
- 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 cs]
- and eq_wq [folded wq_def]
- show "distinct qs \<and> set qs = set qs" by auto
- next
- fix x assume "distinct x \<and> set x = set qs"
- thus "set x = set qs" by auto
- qed
- with th_in show ?thesis by auto
- qed
- ultimately show ?thesis by auto
- qed
- qed
-qed
-
-end
-
context valid_trace
begin
@@ -369,7 +318,7 @@
make any request and get blocked the second time: Contradiction.
*}
-lemma waiting_unique_pre: (* ccc *)
+lemma waiting_unique_pre: (* ddd *)
assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
@@ -402,55 +351,76 @@
show False by (simp add: wq_def)
qed
} note q_not_runing = this
- { fix i1 i2
- let ?i3 = "Suc i2"
- assume lt12: "i1 < i2"
- and "i1 < length s" "i2 < length s"
- hence le_i3: "?i3 \<le> length s" by auto
- from moment_plus [OF this]
- obtain e where eq_m: "moment ?i3 s = e#moment i2 s" by auto
- have "i2 < ?i3" by simp
+ { fix t1 t2 cs1 cs2
+ assume lt1: "t1 < length s"
+ and np1: "\<not> ?Q cs1 (moment t1 s)"
+ and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
+ and lt2: "t2 < length s"
+ and np2: "\<not> ?Q cs2 (moment t2 s)"
+ and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))"
+ and lt12: "t1 < t2"
+ let ?t3 = "Suc t2"
+ from lt2 have le_t3: "?t3 \<le> length s" by auto
+ from moment_plus [OF this]
+ obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
+ have "t2 < ?t3" by simp
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#moment t2 s)"
- proof -
- 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"
+ 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#moment t2 s)"
+ proof -
+ 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
+ have ?thesis
+ proof -
+ have "thread \<in> runing (moment t2 s)"
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
- from vt_e.abs2 [OF True eq_th h2 h1]
- show ?thesis by auto
+ have "e = V thread cs2"
+ proof -
+ have eq_th: "thread = hd (wq (moment t2 s) cs2)"
+ using True and np2 by auto
+ from vt_e.wq_out_inv[OF True this h2]
+ show ?thesis .
+ qed
+ thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto
next
case False
- from vt_e.block_pre[OF False h1]
- have "e = P thread cs2" .
- 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]
- show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
+ have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
+ with vt_e.actor_inv[OF vt_e.pip_e]
+ show ?thesis by auto
qed
- }
+ moreover have "thread \<notin> runing (moment t2 s)"
+ by (rule q_not_runing[OF nn1[rule_format, OF lt12]])
+ ultimately show ?thesis by simp
+ qed
+ } note lt_case = this
show ?thesis
proof -
- {
- assume lt12: "t1 < t2"
+ { assume "t1 < t2"
+ from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]
+ have ?thesis .
+ } moreover {
+ assume "t2 < t1"
+ from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]
+ have ?thesis .
+ } moreover {
+ assume eq_12: "t1 = t2"
let ?t3 = "Suc t2"
from lt2 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
- have "t2 < ?t3" by simp
+ have lt_2: "t2 < ?t3" by simp
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
+ from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12]
+ have g1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
+ g2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have "vt (e#moment t2 s)"
proof -
from vt_moment
@@ -458,119 +428,38 @@
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
+ by (unfold_locales, auto, cases, simp)
+ have "e = V thread cs2 \<or> e = P thread cs2"
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
- from vt_e.abs2 [OF True eq_th h2 h1]
- show ?thesis by auto
- next
- case False
- from vt_e.block_pre[OF False h1]
- have "e = P thread cs2" .
- 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]
- show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
- qed
- } moreover {
- assume lt12: "t2 < t1"
- let ?t3 = "Suc t1"
- from lt1 have le_t3: "?t3 \<le> length s" by auto
- from moment_plus [OF this]
- obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto
- have lt_t3: "t1 < ?t3" by simp
- 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#moment t1 s)"
- proof -
- 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 vt_e.abs2 True eq_th h2 h1
- show ?thesis by auto
+ have "e = V thread cs2"
+ proof -
+ have eq_th: "thread = hd (wq (moment t2 s) cs2)"
+ using True and np2 by auto
+ from vt_e.wq_out_inv[OF True this h2]
+ show ?thesis .
+ qed
+ thus ?thesis by auto
next
case False
- from vt_e.block_pre [OF False h1]
- have "e = P thread cs1" .
- 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]
- show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
+ have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
+ thus ?thesis by auto
qed
- } moreover {
- assume eqt12: "t1 = t2"
- let ?t3 = "Suc t1"
- from lt1 have le_t3: "?t3 \<le> length s" by auto
- from moment_plus [OF this]
- obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto
- have lt_t3: "t1 < ?t3" by simp
- 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)"
- proof -
- 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
+ moreover have "e = V thread cs1 \<or> e = P thread cs1"
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 vt_e.abs2 [OF True eq_th h2 h1]
- show ?thesis by auto
+ have eq_th: "thread = hd (wq (moment t1 s) cs1)"
+ using True and np1 by auto
+ from vt_e.wq_out_inv[folded eq_12, OF True this g2]
+ have "e = V thread cs1" .
+ thus ?thesis by auto
next
case False
- 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
- from nn2 [rule_format, OF this] and eq_m and eqt12
- have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
- h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- show ?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
- from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
- 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#moment t2 s)"
- proof -
- from vt_moment eqt12
- have "vt (moment (Suc t2) s)" by auto
- with eq_m eqt12 show ?thesis by simp
- qed
- 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
+ have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] .
+ thus ?thesis by auto
qed
- } ultimately show ?thesis by arith
+ ultimately have ?thesis using neq12 by auto
+ } ultimately show ?thesis using nat_neq_iff by blast
qed
qed
@@ -582,9 +471,9 @@
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
+ using waiting_unique_pre assms
+ unfolding wq_def s_waiting_def
+ by auto
end
@@ -621,7 +510,7 @@
from last_set_unique [OF this th_in1 th_in2]
show ?thesis .
qed
-
+
lemma preced_linorder:
assumes neq_12: "th1 \<noteq> th2"
and th_in1: "th1 \<in> threads s"
@@ -633,7 +522,7 @@
thus ?thesis by auto
qed
-(* An aux lemma used later *)
+(* An aux lemma used later *)
lemma unique_minus:
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r"
@@ -743,284 +632,758 @@
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)
-
-text {*
- The following lemmas are used in the proof of
- lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed
- by @{text "V"}-events.
- However, since our model is very concise, such seemingly obvious lemmas need to be derived from scratch,
- starting from the model definitions.
-*}
-lemma step_v_hold_inv[elim_format]:
- "\<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"
+context valid_trace
+begin
+
+lemma finite_threads:
+ shows "finite (threads s)"
+using vt by (induct) (auto elim: step.cases)
+
+lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
+unfolding cp_def wq_def
+apply(induct s rule: schs.induct)
+thm cpreced_initial
+apply(simp add: Let_def cpreced_initial)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+done
+
+lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
+ by (unfold s_RAG_def, auto)
+
+lemma wq_threads:
+ assumes h: "th \<in> set (wq s cs)"
+ shows "th \<in> threads s"
proof -
- fix c t
- 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"
- proof(cases "c = cs")
- case False
- with nhd hd show ?thesis
- by (unfold cs_holding_def wq_def, auto simp:Let_def)
+ 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"
+ and h: "th \<in> set (wq (e # s) cs)"
+ show ?case
+ proof(cases e)
+ case (Create th' prio)
+ with ih h show ?thesis
+ by (auto simp:wq_def Let_def)
+ next
+ case (Exit th')
+ with stp ih h show ?thesis
+ apply (auto simp:wq_def Let_def)
+ apply (ind_cases "step s (Exit th')")
+ apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def
+ s_RAG_def s_holding_def cs_holding_def)
+ done
+ next
+ case (V th' cs')
+ show ?thesis
+ proof(cases "cs' = cs")
+ case False
+ with h
+ show ?thesis
+ apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def)
+ by (drule_tac ih, simp)
+ next
+ case True
+ from h
+ show ?thesis
+ proof(unfold V wq_def)
+ assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
+ show "th \<in> threads (V th' cs' # s)"
+ proof(cases "cs = cs'")
+ case False
+ hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)
+ with th_in have " th \<in> set (wq s cs)"
+ by (fold wq_def, simp)
+ from ih [OF this] show ?thesis by simp
+ next
+ case True
+ show ?thesis
+ proof(cases "wq_fun (schs s) cs'")
+ case Nil
+ with h V show ?thesis
+ apply (auto simp:wq_def Let_def split:if_splits)
+ by (fold wq_def, drule_tac ih, simp)
+ next
+ case (Cons a rest)
+ assume eq_wq: "wq_fun (schs s) cs' = a # rest"
+ with h V show ?thesis
+ apply (auto simp:Let_def wq_def split:if_splits)
+ proof -
+ 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 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"
+ by auto
+ qed
+ with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto
+ from ih[OF this[folded wq_def]] show "th \<in> threads s" .
+ next
+ assume th_in: "th \<in> set (wq_fun (schs s) cs)"
+ from ih[OF this[folded wq_def]]
+ show "th \<in> threads s" .
+ qed
+ qed
+ qed
+ qed
+ qed
+ next
+ case (P th' cs')
+ from h stp
+ show ?thesis
+ apply (unfold P wq_def)
+ apply (auto simp:Let_def split:if_splits, fold wq_def)
+ apply (auto intro:ih)
+ apply(ind_cases "step s (P th' cs')")
+ by (unfold runing_def readys_def, auto)
+ next
+ case (Set thread prio)
+ with ih h show ?thesis
+ by (auto simp:wq_def Let_def)
+ qed
next
- case True
- with step_back_step [OF vt]
- have "step s (V th c)" by simp
- hence "next_th s th cs t"
- proof(cases)
- assume "holding s th c"
- with nhd hd show ?thesis
- apply (unfold s_holding_def cs_holding_def wq_def next_th_def,
- auto simp:Let_def split:list.splits if_splits)
- proof -
- assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"
- moreover have "\<dots> = set []"
- proof(rule someI2)
- show "distinct [] \<and> [] = []" by auto
- next
- fix x assume "distinct x \<and> x = []"
- thus "set x = set []" by auto
- qed
- ultimately show False by auto
- next
- assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"
- moreover have "\<dots> = set []"
- proof(rule someI2)
- show "distinct [] \<and> [] = []" by auto
- next
- fix x assume "distinct x \<and> x = []"
- thus "set x = set []" by auto
- qed
- ultimately show False by auto
- qed
- qed
- with True show ?thesis by auto
+ case vt_nil
+ thus ?case by (auto simp:wq_def)
+ qed
+qed
+
+lemma dm_RAG_threads:
+ 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
+ moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
+ 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 this] show ?thesis .
+qed
+
+
+lemma cp_le:
+ 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>+}))
+ \<le> Max ((\<lambda>th. preced th s) ` threads s)"
+ (is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
+ 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
+ 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)
+ apply (unfold trancl_domain [of "RAG s", symmetric])
+ by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
qed
qed
-text {*
- The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be
- derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.
-*}
-lemma step_v_wait_inv[elim_format]:
- "\<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 (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")
+lemma le_cp:
+ 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)
+ \<le> Max (insert (Prc (priority th s) (last_set th s))
+ ((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
+ (is "?l \<le> Max (insert ?l ?A)")
+ proof(cases "?A = {}")
case False
- with nw wt show ?thesis
- by (auto simp:cs_waiting_def wq_def Let_def)
+ have "finite ?A" (is "finite (?f ` ?B)")
+ proof -
+ have "finite ?B"
+ proof-
+ have "finite {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}"
+ proof -
+ let ?F = "\<lambda> (x, y). the_th x"
+ have "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
+ apply (auto simp:image_def)
+ by (rule_tac x = "(Th x, Th th)" in bexI, auto)
+ moreover have "finite \<dots>"
+ proof -
+ 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)
+ thus ?thesis by auto
+ qed
+ ultimately show ?thesis by (auto intro:finite_subset)
+ qed
+ thus ?thesis by (simp add:cs_dependants_def)
+ qed
+ thus ?thesis by simp
+ qed
+ from Max_insert [OF this False, of ?l] show ?thesis by auto
next
case True
- from nw[folded True] wt[folded True]
- have "next_th s th cs t"
- apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits)
- proof -
- fix a list
- assume t_in: "t \<in> set list"
- and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
- 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 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"
- by auto
- qed
- with t_ni and t_in show "a = th" by auto
+ thus ?thesis by auto
+ qed
+qed
+
+lemma max_cp_eq:
+ shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
+ (is "?l = ?r")
+proof(cases "threads s = {}")
+ case True
+ thus ?thesis by auto
+next
+ case False
+ have "?l \<in> ((cp s) ` threads s)"
+ proof(rule Max_in)
+ 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 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
+ show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
next
- fix a list
- assume t_in: "t \<in> set list"
- and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
- 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 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"
+ 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 th'] eq_r
+ have "?r \<le> cp s th'" by auto
+ moreover have "\<dots> \<le> cp s th"
+ proof(fold eq_l)
+ show " cp s th' \<le> Max (cp s ` threads s)"
+ proof(rule Max_ge)
+ from th_in' show "cp s th' \<in> cp s ` threads s"
by auto
- qed
- with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto
- next
- fix a list
- assume 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 show ?thesis
- by (unfold s_holding_def wq_def, auto)
+ next
+ from finite_threads
+ show "finite (cp s ` threads s)" by auto
qed
qed
- with True show ?thesis by simp
+ ultimately show ?thesis by auto
+ qed
+ ultimately show ?thesis using eq_l by auto
+qed
+
+lemma max_cp_eq_the_preced:
+ shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
+ using max_cp_eq using the_preced_def by presburger
+
+end
+
+lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s"
+ by (unfold preced_def, simp)
+
+lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"
+proof
+ fix th'
+ show "the_preced (V th cs # s) th' = the_preced s th'"
+ by (unfold the_preced_def preced_def, simp)
+qed
+
+locale valid_trace_v = valid_trace_e +
+ fixes th cs
+ assumes is_v: "e = V th cs"
+
+context valid_trace_v
+begin
+
+definition "rest = tl (wq s cs)"
+
+definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
+
+lemma distinct_rest: "distinct rest"
+ by (simp add: distinct_tl rest_def wq_distinct)
+
+lemma runing_th_s:
+ shows "th \<in> runing s"
+proof -
+ from pip_e[unfolded is_v]
+ show ?thesis by (cases, simp)
+qed
+
+lemma holding_cs_eq_th:
+ assumes "holding s t cs"
+ shows "t = th"
+proof -
+ from pip_e[unfolded is_v]
+ show ?thesis
+ proof(cases)
+ case (thread_V)
+ from held_unique[OF this(2) assms]
+ show ?thesis by simp
+ qed
+qed
+
+lemma th_not_waiting:
+ "\<not> waiting s th c"
+proof -
+ have "th \<in> readys s"
+ using runing_ready runing_th_s by blast
+ thus ?thesis
+ by (unfold readys_def, auto)
+qed
+
+lemma waiting_neq_th:
+ assumes "waiting s t c"
+ shows "t \<noteq> th"
+ using assms using th_not_waiting by blast
+
+lemma wq_s_cs:
+ "wq s cs = th#rest"
+proof -
+ from pip_e[unfolded is_v]
+ show ?thesis
+ proof(cases)
+ case (thread_V)
+ from this(2) show ?thesis
+ by (unfold rest_def s_holding_def, fold wq_def,
+ metis empty_iff list.collapse list.set(1))
+ qed
+qed
+
+lemma wq_es_cs:
+ "wq (e#s) cs = wq'"
+ using wq_s_cs[unfolded wq_def]
+ by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp)
+
+lemma distinct_wq': "distinct wq'"
+ by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def)
+
+lemma th'_in_inv:
+ assumes "th' \<in> set wq'"
+ shows "th' \<in> set rest"
+ using assms
+ by (metis (mono_tags, lifting) distinct.simps(2)
+ rest_def some_eq_ex wq'_def wq_distinct wq_s_cs)
+
+lemma neq_t_th:
+ assumes "waiting (e#s) t c"
+ shows "t \<noteq> th"
+proof
+ assume otherwise: "t = th"
+ show False
+ proof(cases "c = cs")
+ case True
+ have "t \<in> set wq'"
+ using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs]
+ by simp
+ from th'_in_inv[OF this] have "t \<in> set rest" .
+ with wq_s_cs[folded otherwise] wq_distinct[of cs]
+ show ?thesis by simp
+ next
+ case False
+ have "wq (e#s) c = wq s c" using False
+ by (unfold is_v, simp)
+ hence "waiting s t c" using assms
+ by (simp add: cs_waiting_def waiting_eq)
+ hence "t \<notin> readys s" by (unfold readys_def, auto)
+ hence "t \<notin> runing s" using runing_ready by auto
+ with runing_th_s[folded otherwise] show ?thesis by auto
qed
qed
-lemma step_v_not_wait[consumes 3]:
- "\<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 (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
+lemma waiting_esI1:
+ assumes "waiting s t c"
+ and "c \<noteq> cs"
+ shows "waiting (e#s) t c"
+proof -
+ have "wq (e#s) c = wq s c"
+ using assms(2) is_v by auto
+ with assms(1) show ?thesis
+ using cs_waiting_def waiting_eq by auto
+qed
+
+lemma holding_esI2:
+ assumes "c \<noteq> cs"
+ and "holding s t c"
+ shows "holding (e#s) t c"
+proof -
+ from assms(1) have "wq (e#s) c = wq s c" using is_v by auto
+ from assms(2)[unfolded s_holding_def, folded wq_def,
+ folded this, unfolded wq_def, folded s_holding_def]
+ show ?thesis .
+qed
+
+end
+
+locale valid_trace_v_n = valid_trace_v +
+ assumes rest_nnl: "rest \<noteq> []"
+begin
+
+lemma neq_wq': "wq' \<noteq> []"
+proof (unfold wq'_def, rule someI2)
+ show "distinct rest \<and> set rest = set rest"
+ by (simp add: distinct_rest)
+next
+ fix x
+ assume " distinct x \<and> set x = set rest"
+ thus "x \<noteq> []" using rest_nnl by auto
+qed
+
+definition "taker = hd wq'"
+
+definition "rest' = tl wq'"
+
+lemma eq_wq': "wq' = taker # rest'"
+ by (simp add: neq_wq' rest'_def taker_def)
+
+lemma next_th_taker:
+ shows "next_th s th cs taker"
+ using rest_nnl taker_def wq'_def wq_s_cs
+ by (auto simp:next_th_def)
+
+lemma taker_unique:
+ assumes "next_th s th cs taker'"
+ shows "taker' = taker"
+proof -
+ from assms
+ obtain rest' where
+ h: "wq s cs = th # rest'"
+ "taker' = hd (SOME q. distinct q \<and> set q = set rest')"
+ by (unfold next_th_def, auto)
+ with wq_s_cs have "rest' = rest" by auto
+ thus ?thesis using h(2) taker_def wq'_def by auto
+qed
+
+lemma waiting_set_eq:
+ "{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}"
+ by (smt all_not_in_conv bot.extremum insertI1 insert_subset
+ mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)
+
+lemma holding_set_eq:
+ "{(Cs cs, Th th') |th'. next_th s th cs th'} = {(Cs cs, Th taker)}"
+ using next_th_taker taker_def waiting_set_eq
+ by fastforce
+
+lemma holding_taker:
+ shows "holding (e#s) taker cs"
+ by (unfold s_holding_def, fold wq_def, unfold wq_es_cs,
+ auto simp:neq_wq' taker_def)
+
+lemma waiting_esI2:
+ assumes "waiting s t cs"
+ and "t \<noteq> taker"
+ shows "waiting (e#s) t cs"
+proof -
+ have "t \<in> set wq'"
+ proof(unfold wq'_def, rule someI2)
+ show "distinct rest \<and> set rest = set rest"
+ by (simp add: distinct_rest)
+ next
+ fix x
+ assume "distinct x \<and> set x = set rest"
+ moreover have "t \<in> set rest"
+ using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto
+ ultimately show "t \<in> set x" by simp
+ qed
+ moreover have "t \<noteq> hd wq'"
+ using assms(2) taker_def by auto
+ ultimately show ?thesis
+ by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp)
+qed
+
+lemma waiting_esE:
+ assumes "waiting (e#s) t c"
+ obtains "c \<noteq> cs" "waiting s t c"
+ | "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"
+proof(cases "c = cs")
+ case False
+ hence "wq (e#s) c = wq s c" using is_v by auto
+ with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
+ from that(1)[OF False this] show ?thesis .
+next
+ case True
+ from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]
+ have "t \<noteq> hd wq'" "t \<in> set wq'" by auto
+ hence "t \<noteq> taker" by (simp add: taker_def)
+ moreover hence "t \<noteq> th" using assms neq_t_th by blast
+ moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv)
+ ultimately have "waiting s t cs"
+ by (metis cs_waiting_def list.distinct(2) list.sel(1)
+ list.set_sel(2) rest_def waiting_eq wq_s_cs)
+ show ?thesis using that(2)
+ using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto
+qed
+
+lemma holding_esI1:
+ assumes "c = cs"
+ and "t = taker"
+ shows "holding (e#s) t c"
+ by (unfold assms, simp add: holding_taker)
+
+lemma holding_esE:
+ assumes "holding (e#s) t c"
+ obtains "c = cs" "t = taker"
+ | "c \<noteq> cs" "holding s t c"
+proof(cases "c = cs")
+ case True
+ from assms[unfolded True, unfolded s_holding_def,
+ folded wq_def, unfolded wq_es_cs]
+ have "t = taker" by (simp add: taker_def)
+ from that(1)[OF True this] show ?thesis .
+next
+ case False
+ hence "wq (e#s) c = wq s c" using is_v by auto
+ from assms[unfolded s_holding_def, folded wq_def,
+ unfolded this, unfolded wq_def, folded s_holding_def]
+ have "holding s t c" .
+ from that(2)[OF False this] show ?thesis .
+qed
+
+end
+
+locale valid_trace_v_e = valid_trace_v +
+ assumes rest_nil: "rest = []"
+begin
+
+lemma nil_wq': "wq' = []"
+proof (unfold wq'_def, rule someI2)
+ show "distinct rest \<and> set rest = set rest"
+ by (simp add: distinct_rest)
+next
+ fix x
+ assume " distinct x \<and> set x = set rest"
+ thus "x = []" using rest_nil by auto
+qed
+
+lemma no_taker:
+ assumes "next_th s th cs taker"
+ shows "False"
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)
- assume "holding (wq (V th cs # s)) th cs" and "holding s th cs"
+ from assms[unfolded next_th_def]
+ obtain rest' where "wq s cs = th # rest'" "rest' \<noteq> []"
+ by auto
+ thus ?thesis using rest_def rest_nil by auto
+qed
+
+lemma waiting_set_eq:
+ "{(Th th', Cs cs) |th'. next_th s th cs th'} = {}"
+ using no_taker by auto
+
+lemma holding_set_eq:
+ "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}"
+ using no_taker by auto
+
+lemma no_holding:
+ assumes "holding (e#s) taker cs"
+ shows False
+proof -
+ from wq_es_cs[unfolded nil_wq']
+ have " wq (e # s) cs = []" .
+ from assms[unfolded s_holding_def, folded wq_def, unfolded this]
+ show ?thesis by auto
+qed
+
+lemma no_waiting:
+ assumes "waiting (e#s) t cs"
+ shows False
+proof -
+ from wq_es_cs[unfolded nil_wq']
+ have " wq (e # s) cs = []" .
+ from assms[unfolded s_waiting_def, folded wq_def, unfolded this]
+ show ?thesis by auto
+qed
+
+lemma waiting_esE:
+ assumes "waiting (e#s) t c"
+ obtains "c \<noteq> cs" "waiting s t c"
+proof(cases "c = cs")
+ case False
+ hence "wq (e#s) c = wq s c" using is_v by auto
+ with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
+ from that(1)[OF False this] show ?thesis .
+next
+ case True
+ from no_waiting[OF assms[unfolded True]]
+ show ?thesis by auto
+qed
+
+lemma holding_esE:
+ assumes "holding (e#s) t c"
+ obtains "c \<noteq> cs" "holding s t c"
+proof(cases "c = cs")
+ case True
+ from no_holding[OF assms[unfolded True]]
+ show ?thesis by auto
+next
+ case False
+ hence "wq (e#s) c = wq s c" using is_v by auto
+ from assms[unfolded s_holding_def, folded wq_def,
+ unfolded this, unfolded wq_def, folded s_holding_def]
+ have "holding s t c" .
+ from that[OF False this] show ?thesis .
+qed
+
+end (* ccc *)
+
+lemma rel_eqI:
+ assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
+ and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
+ shows "A = B"
+ using assms by auto
+
+lemma in_RAG_E:
+ assumes "(n1, n2) \<in> RAG (s::state)"
+ obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
+ | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
+ using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
+ by auto
+
+context valid_trace_v
+begin
+
+lemma
+ "RAG (e # s) =
+ RAG s - {(Cs cs, Th th)} -
+ {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
+ {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")
+proof(rule rel_eqI)
+ fix n1 n2
+ assume "(n1, n2) \<in> ?L"
+ thus "(n1, n2) \<in> ?R"
+ proof(cases rule:in_RAG_E)
+ case (waiting th' cs')
+ show ?thesis
+ proof(cases "rest = []")
+ case False
+ interpret h_n: valid_trace_v_n s e th cs
+ by (unfold_locales, insert False, simp)
+ from waiting(3)
+ show ?thesis
+ proof(cases rule:h_n.waiting_esE)
+ case 1
+ with waiting(1,2)
+ show ?thesis
+ by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
+ fold waiting_eq, auto)
+ next
+ case 2
+ with waiting(1,2)
+ show ?thesis
+ by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
+ fold waiting_eq, auto)
+ qed
+ next
+ case True
+ interpret h_e: valid_trace_v_e s e th cs
+ by (unfold_locales, insert True, simp)
+ from waiting(3)
+ show ?thesis
+ proof(cases rule:h_e.waiting_esE)
+ case 1
+ with waiting(1,2)
+ show ?thesis
+ by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
+ fold waiting_eq, auto)
+ qed
+ qed
+ next
+ case (holding th' cs')
+ show ?thesis
+ proof(cases "rest = []")
+ case False
+ interpret h_n: valid_trace_v_n s e th cs
+ by (unfold_locales, insert False, simp)
+ from holding(3)
+ show ?thesis
+ proof(cases rule:h_n.holding_esE)
+ case 1
+ with holding(1,2)
+ show ?thesis
+ by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
+ fold waiting_eq, auto)
+ next
+ case 2
+ with holding(1,2)
+ show ?thesis
+ by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
+ fold holding_eq, auto)
+ qed
+ next
+ case True
+ interpret h_e: valid_trace_v_e s e th cs
+ by (unfold_locales, insert True, simp)
+ from holding(3)
+ show ?thesis
+ proof(cases rule:h_e.holding_esE)
+ case 1
+ with holding(1,2)
+ show ?thesis
+ by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
+ fold holding_eq, auto)
+ qed
+ qed
+ qed
+next
+ fix n1 n2
+ assume h: "(n1, n2) \<in> ?R"
+ show "(n1, n2) \<in> ?L"
+ proof(cases "rest = []")
+ case False
+ interpret h_n: valid_trace_v_n s e th cs
+ by (unfold_locales, insert False, simp)
+ from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq]
+ have "((n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th)
+ \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)) \<or>
+ (n2 = Th h_n.taker \<and> n1 = Cs cs)"
+ by auto
+ thus ?thesis
+ proof
+ assume "n2 = Th h_n.taker \<and> n1 = Cs cs"
+ with h_n.holding_taker
+ show ?thesis
+ by (unfold s_RAG_def, fold holding_eq, auto)
+ next
+ assume h: "(n1, n2) \<in> RAG s \<and>
+ (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"
+ hence "(n1, n2) \<in> RAG s" by simp
thus ?thesis
- apply (unfold s_holding_def wq_def cs_holding_def)
- apply (auto simp:Let_def split:list.splits)
- proof -
- fix list
- assume eq_wq[folded wq_def]:
- "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
- and hd_in: "hd (SOME q. distinct q \<and> set q = set list)
- \<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 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"
- by auto
- qed
- moreover have "distinct (hd (SOME q. distinct q \<and> set q = set list) # list)"
- proof -
- from vt_v.wq_distinct[of cs] and eq_wq
- show ?thesis by auto
- qed
- moreover note eq_wq and hd_in
- ultimately show "False" by auto
+ proof(cases rule:in_RAG_E)
+ case (waiting th' cs')
+ thus ?thesis
qed
+ qed
qed
qed
-lemma step_v_get_hold:
- "\<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 (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)
- \<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 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"
- hence "set x = set rest" by auto
- with nrest
- show "x \<noteq> []" by (case_tac x, auto)
- qed
- with ni show "False" by auto
+end
+
+
+lemma step_RAG_v: (* ccc *)
+assumes vt:
+ "vt (V th cs#s)"
+shows "
+ RAG (V th cs # s) =
+ RAG s - {(Cs cs, Th th)} -
+ {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
+ {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")
+proof(rule rel_eqI)
+ fix n1 n2
+ assume "(n1, n2) \<in> ?L"
+ show "(n1, n2) \<in> ?R" sorry
+next
+ fix n1 n2
+ assume "(n1, n2) \<in> ?R"
+ show "(n1, n2) \<in> ?L" sorry
qed
-lemma step_v_release_inv[elim_format]:
-"\<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 (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
- show ?thesis
- by (unfold s_holding_def wq_def, auto)
- qed
- next
- fix 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
- show ?thesis
- by (unfold s_holding_def wq_def, auto)
- qed
- qed
-
-lemma step_v_waiting_mono:
- "\<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 ?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
- assume neq_cs: "c \<noteq> cs"
- hence "waiting (wq ?s') t c = waiting (wq s) t c"
- by (unfold cs_waiting_def wq_def, auto simp:Let_def)
- with wt show ?thesis by simp
- next
- case True
- with wt show ?thesis
- apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits)
- proof -
- fix a list
- assume not_in: "t \<notin> set list"
- and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"
- 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 vt_v.wq_distinct [of cs]
- and eq_wq[folded wq_def]
- show "distinct list \<and> set list = set list" by auto
- next
- fix x assume "distinct x \<and> set x = set list"
- thus "set x = set list" by auto
- qed
- with not_in is_in show "t = a" by auto
- next
- fix list
- assume is_waiting: "waiting (wq (V th cs # s)) t cs"
- and eq_wq: "wq_fun (schs s) cs = t # list"
- hence "t \<in> set list"
- apply (unfold wq_def, auto simp:Let_def cs_waiting_def)
- proof -
- assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
- moreover have "\<dots> = set list"
- proof(rule someI2)
- from vt_v.wq_distinct [of cs]
- and eq_wq[folded wq_def]
- show "distinct list \<and> set list = set list" by auto
- next
- fix x assume "distinct x \<and> set x = set list"
- thus "set x = set list" by auto
- qed
- ultimately show "t \<in> set list" by simp
- qed
- with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]
- show False by auto
- qed
- qed
-qed
+
text {* (* ddd *)
The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
@@ -1036,7 +1399,7 @@
{(Cs cs, Th th') |th'. next_th s th cs th'}"
apply (insert vt, unfold s_RAG_def)
apply (auto split:if_splits list.splits simp:Let_def)
- apply (auto elim: step_v_waiting_mono step_v_hold_inv
+ apply (auto elim: step_v_waiting_mono step_v_hold_inv
step_v_release step_v_wait_inv
step_v_get_hold step_v_release_inv)
apply (erule_tac step_v_not_wait, auto)
@@ -1559,11 +1922,7 @@
end
-lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
- 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 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)
@@ -2388,8 +2747,6 @@
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
@@ -2579,7 +2936,7 @@
with d have "(Th th1, Cs cs') \<in> RAG s" by simp
with runing_1 have "False"
apply (unfold runing_def readys_def s_RAG_def)
- by (auto simp:eq_waiting)
+ by (auto simp:waiting_eq)
thus ?thesis by simp
qed
next
@@ -2601,7 +2958,7 @@
with d have "(Th th2, Cs cs') \<in> RAG s" by simp
with runing_2 have "False"
apply (unfold runing_def readys_def s_RAG_def)
- by (auto simp:eq_waiting)
+ by (auto simp:waiting_eq)
thus ?thesis by simp
next
assume "th2' \<in> dependants (wq s) th2"
@@ -2664,37 +3021,6 @@
qed
qed
-lemma length_down_to_in:
- assumes le_ij: "i \<le> j"
- and le_js: "j \<le> length s"
- shows "length (down_to j i s) = j - i"
-proof -
- have "length (down_to j i s) = length (from_to i j (rev s))"
- by (unfold down_to_def, auto)
- also have "\<dots> = j - i"
- proof(rule length_from_to_in[OF le_ij])
- from le_js show "j \<le> length (rev s)" by simp
- qed
- finally show ?thesis .
-qed
-
-
-lemma moment_head:
- assumes le_it: "Suc i \<le> length t"
- obtains e where "moment (Suc i) t = e#moment i t"
-proof -
- have "i \<le> Suc i" by simp
- from length_down_to_in [OF this le_it]
- have "length (down_to (Suc i) i t) = 1" by auto
- then obtain e where "down_to (Suc i) i t = [e]"
- apply (cases "(down_to (Suc i) i t)") by auto
- moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
- by (rule down_to_conc[symmetric], auto)
- ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
- by (auto simp:down_to_moment)
- from that [OF this] show ?thesis .
-qed
-
context valid_trace
begin
@@ -3077,7 +3403,6 @@
definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
-
lemma detached_test:
shows "detached s th = (Th th \<notin> Field (RAG s))"
apply(simp add: detached_def Field_def)
@@ -3146,7 +3471,7 @@
with dtc
have "th \<in> readys s"
by (unfold readys_def detached_def Field_def Domain_def Range_def,
- auto simp:eq_waiting s_RAG_def)
+ auto simp:waiting_eq s_RAG_def)
with cncs_z and eq_pv show ?thesis by simp
next
case False
@@ -3888,4 +4213,10 @@
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
+find_theorems release
+
+lemma "wq (V th cs # s) cs1 = ttt"
+ apply (unfold wq_def, auto simp:Let_def)
+
end
+
--- a/PIPBasics.thy~ Thu Jan 14 00:55:54 2016 +0800
+++ b/PIPBasics.thy~ Sat Jan 16 10:59:03 2016 +0800
@@ -30,6 +30,13 @@
"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 runing_head:
+ assumes "th \<in> runing s"
+ and "th \<in> set (wq_fun (schs s) cs)"
+ shows "th = hd (wq_fun (schs s) cs)"
+ using assms
+ by (simp add:runing_def readys_def s_waiting_def wq_def)
+
context valid_trace
begin
@@ -60,39 +67,70 @@
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)"
- thus "distinct (wq (e # s) cs)"
- proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
- fix thread s
- assume h1: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
- and h2: "thread \<in> set (wq_fun (schs s) cs)"
- and h3: "thread \<in> runing s"
- show "False"
- proof -
- from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow>
- thread = hd ((wq_fun (schs s) cs))"
- by (simp add:runing_def readys_def s_waiting_def wq_def)
- from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .
- with h2
- have "(Cs cs, Th thread) \<in> (RAG s)"
- by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)
- with h1 show False by auto
+proof(induct rule:ind)
+ case (Cons s e)
+ from Cons(4,3)
+ show ?case
+ proof(induct)
+ case (thread_P th s cs1)
+ show ?case
+ proof(cases "cs = cs1")
+ case True
+ thus ?thesis (is "distinct ?L")
+ proof -
+ have "?L = wq_fun (schs s) cs1 @ [th]" using True
+ by (simp add:wq_def wf_def Let_def split:list.splits)
+ moreover have "distinct ..."
+ proof -
+ have "th \<notin> set (wq_fun (schs s) cs1)"
+ proof
+ assume otherwise: "th \<in> set (wq_fun (schs s) cs1)"
+ from runing_head[OF thread_P(1) this]
+ have "th = hd (wq_fun (schs s) cs1)" .
+ hence "(Cs cs1, Th th) \<in> (RAG s)" using otherwise
+ by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)
+ with thread_P(2) show False by auto
+ qed
+ moreover have "distinct (wq_fun (schs s) cs1)"
+ using True thread_P wq_def by auto
+ ultimately show ?thesis by auto
+ qed
+ ultimately show ?thesis by simp
+ qed
+ next
+ case False
+ with thread_P(3)
+ show ?thesis
+ by (auto simp:wq_def wf_def Let_def split:list.splits)
qed
next
- fix thread s a list
- assume dst: "distinct list"
- show "distinct (SOME q. distinct q \<and> set q = set list)"
- proof(rule someI2)
- from dst show "distinct list \<and> set list = set list" by auto
+ case (thread_V th s cs1)
+ thus ?case
+ proof(cases "cs = cs1")
+ case True
+ show ?thesis (is "distinct ?L")
+ proof(cases "(wq s cs)")
+ case Nil
+ thus ?thesis
+ by (auto simp:wq_def wf_def Let_def split:list.splits)
+ next
+ case (Cons w_hd w_tl)
+ moreover have "distinct (SOME q. distinct q \<and> set q = set w_tl)"
+ proof(rule someI2)
+ from thread_V(3)[unfolded Cons]
+ show "distinct w_tl \<and> set w_tl = set w_tl" by auto
+ qed auto
+ ultimately show ?thesis
+ by (auto simp:wq_def wf_def Let_def True split:list.splits)
+ qed
next
- fix q assume "distinct q \<and> set q = set list"
- thus "distinct q" by auto
+ case False
+ with thread_V(3)
+ show ?thesis
+ by (auto simp:wq_def wf_def Let_def split:list.splits)
qed
- qed
-qed
+ qed (insert Cons, auto simp: wq_def Let_def split:list.splits)
+qed (unfold wq_def Let_def, simp)
end
@@ -108,56 +146,34 @@
*}
lemma block_pre:
- assumes 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 -
- show ?thesis
- proof(cases e)
- case (P th cs)
- with assms
+proof(cases e)
+ -- {* This is the only non-trivial case: *}
+ case (V th cs1)
+ have False
+ proof(cases "cs1 = cs")
+ case True
show ?thesis
- by (auto simp:wq_def Let_def split:if_splits)
- next
- case (Create th prio)
- with assms show ?thesis
- by (auto simp:wq_def Let_def split:if_splits)
- next
- case (Exit th)
- with assms show ?thesis
- by (auto simp:wq_def Let_def split:if_splits)
- next
- case (Set th prio)
- with assms show ?thesis
- by (auto simp:wq_def Let_def split:if_splits)
- next
- case (V th cs)
- with vt_e assms show ?thesis
- apply (auto simp:wq_def Let_def split:if_splits)
- proof -
- fix q qs
- 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 (V th cs # s)"
- from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
- moreover have "thread \<in> set qs"
+ proof(cases "(wq s cs1)")
+ case (Cons w_hd w_tl)
+ have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"
proof -
- have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
+ have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"
+ using Cons V by (auto simp:wq_def Let_def True split:if_splits)
+ moreover have "set ... \<subseteq> set (wq s cs)"
proof(rule someI2)
- from wq_distinct [of cs]
- and h2[symmetric, folded wq_def]
- show "distinct qs \<and> set qs = set qs" by auto
- next
- fix x assume "distinct x \<and> set x = set qs"
- thus "set x = set qs" by auto
- qed
- with h3 show ?thesis by simp
+ show "distinct w_tl \<and> set w_tl = set w_tl"
+ by (metis distinct.simps(2) local.Cons wq_distinct)
+ qed (insert Cons True, auto)
+ ultimately show ?thesis by simp
qed
- ultimately show "False" by auto
- qed
- qed
-qed
+ with assms show ?thesis by auto
+ qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)
+ qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
+ thus ?thesis by auto
+qed (insert assms, auto simp:wq_def Let_def split:if_splits)
end
@@ -233,10 +249,10 @@
end
+
context valid_trace
begin
-
-lemma vt_moment: "\<And> t. vt (moment t s)"
+lemma vt_moment: "\<And> t. vt (moment t s)"
proof(induct rule:ind)
case Nil
thus ?case by (simp add:vt_nil)
@@ -260,10 +276,17 @@
ultimately show ?thesis by simp
qed
qed
+end
-(* Wrong:
- lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
-*)
+locale valid_moment = valid_trace +
+ fixes i :: nat
+
+sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
+ by (unfold_locales, insert vt_moment, auto)
+
+context valid_trace
+begin
+
text {* (* ddd *)
The nature of the work is like this: since it starts from a very simple and basic
@@ -292,13 +315,13 @@
@{text "th"} got blocked on @{text "cs1"} and @{text "cs2"}
and kept on blocked on them respectively ever since.
- Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
+ Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still
in blocked state at moment @{text "t2"} and could not
make any request and get blocked the second time: Contradiction.
*}
-lemma waiting_unique_pre:
+lemma waiting_unique_pre: (* ccc *)
assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
@@ -519,7 +542,6 @@
(* An aux lemma used later *)
lemma unique_minus:
- fixes x y z r
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r"
and xz: "(x, z) \<in> r^+"
@@ -547,7 +569,6 @@
qed
lemma unique_base:
- fixes r x y z
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r"
and xz: "(x, z) \<in> r^+"
@@ -574,7 +595,6 @@
qed
lemma unique_chain:
- fixes r x y z
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r^+"
and xz: "(x, z) \<in> r^+"
@@ -914,7 +934,6 @@
with the happening of @{text "V"}-events:
*}
lemma step_RAG_v:
-fixes th::thread
assumes vt:
"vt (V th cs#s)"
shows "
@@ -1342,7 +1361,6 @@
by (auto intro:wq_threads)
lemma readys_v_eq:
- fixes th thread cs rest
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
@@ -1511,7 +1529,6 @@
lemma step_holdents_p_add:
- fixes 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}"
@@ -1521,7 +1538,6 @@
qed
lemma step_holdents_p_eq:
- fixes 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"
@@ -1551,7 +1567,6 @@
qed
lemma cntCS_v_dec:
- fixes s thread cs
assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
@@ -2566,36 +2581,6 @@
qed
qed
-lemma length_down_to_in:
- assumes le_ij: "i \<le> j"
- and le_js: "j \<le> length s"
- shows "length (down_to j i s) = j - i"
-proof -
- have "length (down_to j i s) = length (from_to i j (rev s))"
- by (unfold down_to_def, auto)
- also have "\<dots> = j - i"
- proof(rule length_from_to_in[OF le_ij])
- from le_js show "j \<le> length (rev s)" by simp
- qed
- finally show ?thesis .
-qed
-
-
-lemma moment_head:
- assumes le_it: "Suc i \<le> length t"
- obtains e where "moment (Suc i) t = e#moment i t"
-proof -
- have "i \<le> Suc i" by simp
- from length_down_to_in [OF this le_it]
- have "length (down_to (Suc i) i t) = 1" by auto
- then obtain e where "down_to (Suc i) i t = [e]"
- apply (cases "(down_to (Suc i) i t)") by auto
- moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
- by (rule down_to_conc[symmetric], auto)
- ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
- by (auto simp:down_to_moment)
- from that [OF this] show ?thesis .
-qed
context valid_trace
begin
@@ -3790,4 +3775,6 @@
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
+find_theorems readys runing
+
end