--- a/Implementation.thy Fri Feb 12 12:32:57 2016 +0800
+++ b/Implementation.thy Fri Feb 12 17:50:24 2016 +0800
@@ -2,118 +2,49 @@
imports PIPBasics
begin
+
+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
+
+end
+
section {*
This file contains lemmas used to guide the recalculation of current precedence
after every system call (or system operation)
*}
-section {* Recursive calculation of @{term "cp"} *}
-
-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
-(* 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 cp_rec:
- "cp s th = Max ({the_preced s th} \<union>
- (cp s o the_thread) ` children (tRAG s) (Th th))"
-proof -
- 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
-qed
-
-end
-
text {* (* ddd *)
One beauty of our modelling is that we follow the definitional extension tradition of HOL.
The benefit of such a concise and miniature model is that large number of intuitively
@@ -235,7 +166,6 @@
The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
*}
-
context valid_trace_v
begin
@@ -283,7 +213,8 @@
lemma sub_RAGs':
"{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"
- using next_th_RAG[OF next_th_taker] .
+ using waiting_taker holding_th_cs_s
+ by (unfold s_RAG_def, fold waiting_eq holding_eq, auto)
lemma ancestors_th':
"ancestors (RAG s) (Th taker) = {Th th, Cs cs}"