--- 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