--- a/Implementation.thy Tue Feb 09 22:30:43 2016 +0800
+++ b/Implementation.thy Fri Feb 12 12:32:57 2016 +0800
@@ -7,6 +7,113 @@
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