--- a/PIPBasics.thy Thu Feb 04 00:43:05 2016 +0000
+++ b/PIPBasics.thy Thu Feb 04 14:45:30 2016 +0800
@@ -4,6 +4,12 @@
section {* Generic aulxiliary lemmas *}
+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 f_image_eq:
assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
shows "f ` A = g ` A"
@@ -86,14 +92,10 @@
finally show ?thesis by simp
qed
-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
-
section {* Lemmas do not depend on trace validity *}
+text {* The following lemma serves to proof @{text "preced_tm_lt"} *}
+
lemma birth_time_lt:
assumes "s \<noteq> []"
shows "last_set th s < length s"
@@ -112,16 +114,18 @@
qed
qed simp
+text {* The following lemma also serves to proof @{text "preced_tm_lt"} *}
lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
by (induct s, auto)
+text {* The following lemma is used in Correctness.thy *}
lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
-lemma eq_RAG:
- "RAG (wq s) = RAG s"
- by (unfold cs_RAG_def s_RAG_def, auto)
-
+text {*
+ The follow lemma says if a resource is waited for, it must be held
+ by someone else.
+*}
lemma waiting_holding:
assumes "waiting (s::state) th cs"
obtains th' where "holding s th' cs"
@@ -134,7 +138,22 @@
from that[OF this] show ?thesis .
qed
-lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
+text {*
+ The following four lemmas relate the @{term wq}
+ and non-@{term wq} versions of @{term waiting}, @{term holding},
+ @{term dependants} and @{term cp}.
+*}
+
+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 eq_dependants: "dependants (wq s) = dependants s"
+ by (simp add: s_dependants_abv wq_def)
+
+lemma cp_eq: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
apply(simp add: Let_def cpreced_initial)
@@ -147,6 +166,13 @@
apply(simp add: Let_def)
done
+text {*
+ The following lemmas is an alternative definition of @{term cp},
+ which is based on the notion of subtrees in @{term RAG} and
+ is handy to use once the abstract theory of {\em relational graph}
+ (and specifically {\em relational tree} and {\em relational forest})
+ are in place.
+*}
lemma cp_alt_def:
"cp s th =
Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
@@ -159,22 +185,25 @@
by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
thus ?thesis by simp
qed
- thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
+ thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
qed
-lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
- by (unfold s_RAG_def, auto)
-
-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)
-
+text {*
+ The following @{text "children_RAG_alt_def"} relates
+ @{term children} in @{term RAG} to the notion of @{term holding}.
+ It is a technical lemmas used to prove the two following lemmas.
+*}
lemma children_RAG_alt_def:
"children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
by (unfold s_RAG_def, auto simp:children_def holding_eq)
+text {*
+ The following two lemmas relate @{term holdents} and @{term cntCS}
+ to @{term children} in @{term RAG}, so that proofs about
+ @{term holdents} and @{term cntCS} can be carried out under
+ the support of the abstract theory of {\em relational graph}
+ (and specifically {\em relational tree} and {\em relational forest}).
+*}
lemma holdents_alt_def:
"holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"
by (unfold children_RAG_alt_def holdents_def, simp add: image_image)
@@ -184,6 +213,11 @@
apply (unfold children_RAG_alt_def cntCS_def holdents_def)
by (rule card_image[symmetric], auto simp:inj_on_def)
+text {*
+ The following two lemmas show the inclusion relations
+ among three key sets, namely @{term runing}, @{term readys}
+ and @{term threads}.
+*}
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
@@ -194,17 +228,12 @@
unfolding readys_def
by auto
-lemma wq_v_neq [simp]:
- "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)
-
+text {*
+ The following lemma says that if a thread is running,
+ it must be the head of every waiting queue it is in.
+ In other words, a running thread must have got every
+ resource it has requested.
+*}
lemma runing_wqE:
assumes "th \<in> runing s"
and "th \<in> set (wq s cs)"
@@ -225,17 +254,6 @@
with eq_wq that show ?thesis by metis
qed
-lemma isP_E:
- assumes "isP e"
- obtains cs where "e = P (actor e) cs"
- using assms by (cases e, auto)
-
-lemma isV_E:
- assumes "isV e"
- obtains cs where "e = V (actor e) cs"
- using assms by (cases e, auto)
-
-
text {*
Every thread can only be blocked on one critical resource,
symmetrically, every critical resource can only be held by one thread.
@@ -247,6 +265,12 @@
shows "th1 = th2"
by (insert assms, unfold s_holding_def, auto)
+text {*
+ The following three lemmas establishes the uniqueness of
+ precedence, a key property about precedence.
+ The first two are just technical lemmas to assist the proof
+ of the third.
+*}
lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
apply (induct s, auto)
by (case_tac a, auto split:if_splits)
@@ -267,7 +291,12 @@
from last_set_unique [OF this th_in1 th_in2]
show ?thesis .
qed
-
+
+text {*
+ The following lemma shows that there exits a linear order
+ on precedences, which is crucial for the notion of
+ @{term Max} to be applicable.
+*}
lemma preced_linorder:
assumes neq_12: "th1 \<noteq> th2"
and th_in1: "th1 \<in> threads s"
@@ -279,6 +308,10 @@
thus ?thesis by auto
qed
+text {*
+ The following lemma case analysis the situations when
+ two nodes are in @{term RAG}.
+*}
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"
@@ -286,6 +319,13 @@
using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
by auto
+text {*
+ The following lemmas are the simplification rules
+ for @{term count}, @{term cntP}, @{term cntV}.
+ It is a major technical in this development to use
+ the counter of @{term "P"} and @{term "V"} (* ccc *)
+*}
+
lemma count_rec1 [simp]:
assumes "Q e"
shows "count Q (e#es) = Suc (count Q es)"
@@ -354,30 +394,6 @@
insert assms V, auto simp:cntV_def)
qed (insert assms, auto simp:cntV_def)
-lemma eq_dependants: "dependants (wq s) = dependants s"
- by (simp add: s_dependants_abv wq_def)
-
-lemma inj_the_preced:
- "inj_on (the_preced s) (threads s)"
- by (metis inj_onI preced_unique the_preced_def)
-
-lemma holding_next_thI:
- assumes "holding s th cs"
- and "length (wq s cs) > 1"
- obtains th' where "next_th s th cs th'"
-proof -
- from assms(1)[folded holding_eq, unfolded cs_holding_def]
- have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)"
- by (unfold s_holding_def, fold wq_def, auto)
- then obtain rest where h1: "wq s cs = th#rest"
- by (cases "wq s cs", auto)
- with assms(2) have h2: "rest \<noteq> []" by auto
- let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
- have "next_th s th cs ?th'" using h1(1) h2
- by (unfold next_th_def, auto)
- from that[OF this] show ?thesis .
-qed
-
(* ccc *)
section {* Locales used to investigate the execution of PIP *}
@@ -675,6 +691,13 @@
section {* Distinctiveness of waiting queues *}
+lemma (in valid_trace) finite_threads:
+ shows "finite (threads s)"
+ using vt by (induct) (auto elim: step.cases)
+
+lemma (in valid_trace) finite_readys [simp]: "finite (readys s)"
+ using finite_threads readys_threads rev_finite_subset by blast
+
context valid_trace_create
begin
@@ -811,13 +834,6 @@
context valid_trace
begin
-lemma finite_threads:
- shows "finite (threads s)"
- using vt by (induct) (auto elim: step.cases)
-
-lemma finite_readys [simp]: "finite (readys s)"
- using finite_threads readys_threads rev_finite_subset by blast
-
lemma wq_distinct: "distinct (wq s cs)"
proof(induct rule:ind)
case (Cons s e)
@@ -1033,7 +1049,7 @@
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
+ moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, 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)
@@ -1123,7 +1139,7 @@
next
case False
have "wq (e#s) c = wq s c" using False
- by (unfold is_v, simp)
+ by 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)
@@ -1138,7 +1154,7 @@
shows "waiting (e#s) t c"
proof -
have "wq (e#s) c = wq s c"
- using assms(2) is_v by auto
+ using assms(2) by auto
with assms(1) show ?thesis
using cs_waiting_def waiting_eq by auto
qed
@@ -1148,7 +1164,7 @@
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(1) have "wq (e#s) c = wq s c" by auto
from assms(2)[unfolded s_holding_def, folded wq_def,
folded this, unfolded wq_def, folded s_holding_def]
show ?thesis .
@@ -1243,7 +1259,7 @@
| "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
+ hence "wq (e#s) c = wq s c" 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
@@ -1277,7 +1293,7 @@
from that(1)[OF True this] show ?thesis .
next
case False
- hence "wq (e#s) c = wq s c" using is_v by auto
+ hence "wq (e#s) c = wq s c" 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" .
@@ -1328,7 +1344,15 @@
show ?thesis by auto
qed
-lemma no_waiting:
+lemma no_waiter_before: "\<not> waiting s t cs"
+proof
+ assume otherwise: "waiting s t cs"
+ from this[unfolded s_waiting_def, folded wq_def,
+ unfolded wq_s_cs rest_nil]
+ show False by simp
+qed
+
+lemma no_waiter_after:
assumes "waiting (e#s) t cs"
shows False
proof -
@@ -1353,12 +1377,12 @@
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
+ hence "wq (e#s) c = wq s c" 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]]
+ from no_waiter_after[OF assms[unfolded True]]
show ?thesis by auto
qed
@@ -1371,7 +1395,7 @@
show ?thesis by auto
next
case False
- hence "wq (e#s) c = wq s c" using is_v by auto
+ hence "wq (e#s) c = wq s c" 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" .
@@ -2689,6 +2713,10 @@
finally show ?thesis .
qed
+lemma eq_RAG:
+ "RAG (wq s) = RAG s"
+ by (unfold cs_RAG_def s_RAG_def, auto)
+
lemma dependants_alt_def:
"dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
@@ -4659,4 +4687,4 @@
end
-end
\ No newline at end of file
+end