--- a/PIPBasics.thy Fri Feb 12 12:32:57 2016 +0800
+++ b/PIPBasics.thy Fri Feb 12 17:50:24 2016 +0800
@@ -361,20 +361,20 @@
*}
lemma cntP_diff_inv:
assumes "cntP (e#s) th \<noteq> cntP s th"
- shows "isP e \<and> actor e = th"
+ obtains cs where "e = P th cs"
proof(cases e)
case (P th' pty)
- show ?thesis
+ show ?thesis using that
by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)",
insert assms P, auto simp:cntP_def)
qed (insert assms, auto simp:cntP_def)
lemma cntV_diff_inv:
assumes "cntV (e#s) th \<noteq> cntV s th"
- shows "isV e \<and> actor e = th"
+ obtains cs' where "e = V th cs'"
proof(cases e)
case (V th' pty)
- show ?thesis
+ show ?thesis using that
by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)",
insert assms V, auto simp:cntV_def)
qed (insert assms, auto simp:cntV_def)
@@ -1473,6 +1473,11 @@
using assms
by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)
+lemma not_in_thread_isolated:
+ assumes "th \<notin> threads s"
+ shows "(Th th) \<notin> Field (RAG s)"
+ using RAG_threads assms by auto
+
text {*
As a corollary, this lemma shows that @{term tRAG}
is also covered by the @{term threads}-set.
@@ -4919,104 +4924,139 @@
end
-section {* Other properties useful in Implementation.thy or Correctness.thy *}
-
-context valid_trace_e
-begin
-
-lemma actor_inv:
- assumes "\<not> isCreate e"
- shows "actor e \<in> runing s"
- using pip_e assms
- by (induct, auto)
-end
+section {* Recursive calculation of @{term "cp"} *}
+
+text {*
+ According to the normal definitions, such as @{thm cp_def}, @{thm cp_alt_def}
+ and @{thm cp_alt_def1}, the @{term cp}-value of a thread depends
+ on the @{term preced}-values of all threads in its subtree. To calculate
+ a @{term cp}-value, one needs to traverse a whole subtree.
+
+ However, in this section, we are going to show that @{term cp}-value
+ can be calculate locally (given by the lemma @{text "cp_rec"} in the following).
+ According to this lemma, the @{term cp}-value of a thread can be calculated only from
+ the @{term cp}-values of its children in @{term RAG}.
+ Therefore, if the @{term cp}-values of one thread's children are not
+ changed by an execution step, there is no need to recalculate. This
+ is particularly useful to in Implementation.thy to speed up the
+ recalculation of @{term cp}-values.
+*}
+
+text {*
+ The following function @{text "cp_gen"} is a generalization
+ of @{term cp}. Unlike @{term cp} which returns a precedence
+ for a thread, @{text "cp_gen"} returns precedence for a node
+ in @{term RAG}. When the node represent a thread, @{text cp_gen} is
+ coincident with @{term cp} (to be shown in lemma @{text "cp_gen_def_cond"}),
+ and this is the only meaningful use of @{text cp_gen}.
+
+ The introduction of @{text cp_gen} is purely technical to easy some
+ of the proofs leading to the finally lemma @{text cp_rec}.
+*}
+
+definition "cp_gen s x =
+ Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
+
+lemma cp_gen_alt_def:
+ "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
+ by (auto simp:cp_gen_def)
+
+lemma cp_gen_def_cond:
+ assumes "x = Th th"
+ shows "cp s th = cp_gen s (Th th)"
+by (unfold cp_alt_def1 cp_gen_def, simp)
+
+lemma cp_gen_over_set:
+ assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
+ shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
+proof(rule f_image_eq)
+ fix a
+ assume "a \<in> A"
+ from assms[rule_format, OF this]
+ obtain th where eq_a: "a = Th th" by auto
+ show "cp_gen s a = (cp s \<circ> the_thread) a"
+ by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
+qed
+
context valid_trace
begin
-
-lemma readys_root:
- assumes "th \<in> readys s"
- shows "root (RAG s) (Th th)"
-proof -
- { fix x
- assume "x \<in> ancestors (RAG s) (Th th)"
- hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- obtain z where "(Th th, z) \<in> RAG s" by auto
- with assms(1) have False
- apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
- by (fold wq_def, blast)
- } thus ?thesis by (unfold root_def, auto)
-qed
-
-lemma readys_in_no_subtree:
- assumes "th \<in> readys s"
- and "th' \<noteq> th"
- shows "Th th \<notin> subtree (RAG s) (Th th')"
-proof
- assume "Th th \<in> subtree (RAG s) (Th th')"
- thus False
- proof(cases rule:subtreeE)
- case 1
- with assms show ?thesis by auto
- next
- case 2
- with readys_root[OF assms(1)]
- show ?thesis by (auto simp:root_def)
- qed
-qed
-
-lemma not_in_thread_isolated:
- assumes "th \<notin> threads s"
- shows "(Th th) \<notin> Field (RAG s)"
-proof
- assume "(Th th) \<in> Field (RAG s)"
- with dm_RAG_threads and rg_RAG_threads assms
- show False by (unfold Field_def, blast)
+(* ddd *)
+lemma cp_gen_rec:
+ assumes "x = Th th"
+ shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"
+proof(cases "children (tRAG s) x = {}")
+ case True
+ show ?thesis
+ by (unfold True cp_gen_def subtree_children, simp add:assms)
+next
+ case False
+ hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
+ note fsbttRAGs.finite_subtree[simp]
+ have [simp]: "finite (children (tRAG s) x)"
+ by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree],
+ rule children_subtree)
+ { fix r x
+ have "subtree r x \<noteq> {}" by (auto simp:subtree_def)
+ } note this[simp]
+ have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"
+ proof -
+ from False obtain q where "q \<in> children (tRAG s) x" by blast
+ moreover have "subtree (tRAG s) q \<noteq> {}" by simp
+ ultimately show ?thesis by blast
+ qed
+ have h: "Max ((the_preced s \<circ> the_thread) `
+ ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =
+ Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"
+ (is "?L = ?R")
+ proof -
+ let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L
+ let "Max (_ \<union> (?h ` ?B))" = ?R
+ let ?L1 = "?f ` \<Union>(?g ` ?B)"
+ have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"
+ proof -
+ have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
+ also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
+ finally have "Max ?L1 = Max ..." by simp
+ also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
+ by (subst Max_UNION, simp+)
+ also have "... = Max (cp_gen s ` children (tRAG s) x)"
+ by (unfold image_comp cp_gen_alt_def, simp)
+ finally show ?thesis .
+ qed
+ show ?thesis
+ proof -
+ have "?L = Max (?f ` ?A \<union> ?L1)" by simp
+ also have "... = max (the_preced s (the_thread x)) (Max ?L1)"
+ by (subst Max_Un, simp+)
+ also have "... = max (?f x) (Max (?h ` ?B))"
+ by (unfold eq_Max_L1, simp)
+ also have "... =?R"
+ by (rule max_Max_eq, (simp)+, unfold assms, simp)
+ finally show ?thesis .
+ qed
+ qed thus ?thesis
+ by (fold h subtree_children, unfold cp_gen_def, simp)
qed
-lemma next_th_holding:
- assumes nxt: "next_th s th cs th'"
- shows "holding (wq s) th cs"
-proof -
- from nxt[unfolded next_th_def]
- obtain rest where h: "wq s cs = th # rest"
- "rest \<noteq> []"
- "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
- thus ?thesis
- by (unfold cs_holding_def, auto)
-qed
-
-lemma next_th_waiting:
- assumes nxt: "next_th s th cs th'"
- shows "waiting (wq s) th' cs"
+lemma cp_rec:
+ "cp s th = Max ({the_preced s th} \<union>
+ (cp s o the_thread) ` children (tRAG s) (Th th))"
proof -
- from nxt[unfolded next_th_def]
- obtain rest where h: "wq s cs = th # rest"
- "rest \<noteq> []"
- "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
- from wq_distinct[of cs, unfolded h]
- have dst: "distinct (th # rest)" .
- have in_rest: "th' \<in> set rest"
- proof(unfold h, rule someI2)
- show "distinct rest \<and> set rest = set rest" using dst by auto
- next
- fix x assume "distinct x \<and> set x = set rest"
- with h(2)
- show "hd x \<in> set (rest)" by (cases x, auto)
+ have "Th th = Th th" by simp
+ note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this]
+ show ?thesis
+ proof -
+ have "cp_gen s ` children (tRAG s) (Th th) =
+ (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"
+ proof(rule cp_gen_over_set)
+ show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"
+ by (unfold tRAG_alt_def, auto simp:children_def)
+ qed
+ thus ?thesis by (subst (1) h(1), unfold h(2), simp)
qed
- hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
- moreover have "th' \<noteq> hd (wq s cs)"
- by (unfold h(1), insert in_rest dst, auto)
- ultimately show ?thesis by (auto simp:cs_waiting_def)
qed
-lemma next_th_RAG:
- assumes nxt: "next_th (s::event list) th cs th'"
- shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
- using vt assms next_th_holding next_th_waiting
- by (unfold s_RAG_def, simp)
-
end
end