pip: comparison PIPBasics.thy

equal deleted inserted replaced

-:81c6ede5cd11
+:74fc1eae4605
 apply(subst (2) schs.simps)
 apply(simp add: Let_def)
 apply(subst (2) schs.simps)
 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))})"
-proof -
-have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
-Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
-(is "Max (_ ` ?L) = Max (_ ` ?R)")
-proof -
-have "?L = ?R"
-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_def, fold the_preced_def, simp)
-qed
 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 threads_set_eq:
 "the_thread ` (subtree (tRAG s) (Th th)) =
 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
 by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
+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))})"
+proof -
+have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
+Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+(is "Max (_ ` ?L) = Max (_ ` ?R)")
+proof -
+have "?L = ?R"
+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_def, fold the_preced_def, simp)
+qed
+text {*
+The following is another definition of @{term cp}.
+*}
+lemma cp_alt_def1:
+"cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
+proof -
+have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
+((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
+by auto
+thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
+qed
 lemma RAG_tRAG_transfer:
 assumes  "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
 and "(Cs cs, Th th'') \<in> RAG s"
 shows "tRAG s' = tRAG s \<union> {(Th th, Th th'')}" (is "?L = ?R")
 proof -
 show ?thesis by simp
 qed
 ultimately show ?thesis by simp
 qed
 qed
+text {*
+The following two lemmas are fundamental, because they assure
+that the numbers of both living and ready threads are finite.
+*}
+lemma finite_threads:
+shows "finite (threads s)"
+using vt by (induct) (auto elim: step.cases)
+lemma  finite_readys: "finite (readys s)"
+using finite_threads readys_threads rev_finite_subset by blast
 end
 text {*
 The following locale @{text "valid_moment"} is to inherit the properties
 derived on any valid state to the prefix of it, with length @{text "i"}.
 by (unfold_locales, simp)
 section {* Waiting queues are distinct *}
 text {*
-This section proofs that every waiting queue in the system
+This section proves that every waiting queue in the system
 is distinct, given in lemma @{text wq_distinct}.
 The proof is split into the locales for events (or operations),
 all contain a lemma named @{text "wq_distinct_kept"} to show that
 the distinctiveness is preserved by the respective operation. All lemmas
 finally show ?thesis .
 qed
 end
-section {* The change of @{term RAG} *}
+section {* The formation of @{term RAG} *}
 text {*
 The whole of PIP resides on the understanding of the formation
-of @{term RAG}. In this section, we are going to investigate how
+of @{term RAG}. We are going to show that @{term RAG}
-@{term RAG} is changed with the execution of every event (or operation).
+forms a finite branching forest. The formalization is divided
-The effect of every event on @{text RAG} is derived in its respective
+into a series of subsections.
+*}
+subsection {* The change of @{term RAG} with each step of execution *}
+text {*
+The very essence to prove that @{term RAG} has a certain property is to
+show that this property is preserved as an invariant by the execution
+of the system, and the basis for such kind of invariant proofs is to
+show how @{term RAG} is changed with the execution of every execution step
+(or event, or system operation). In this subsection,
+the effect of every event on @{text RAG} is derived in its respective
 locale named @{text "RAG_es"} with all lemmas before auxiliary.
-The derivation of these @{text "RAG_es"}s forms the very basis
+These derived @{text "RAG_es"}s constitute the foundation
-to show the well-formedness of @{term RAG},
+to show the various well-formed properties of @{term RAG},
 for example, @{term RAG} is finite, acyclic, and single-valued, etc.
 *}
 text {*
 The following three lemmas show that @{text "RAG"} does not change
 by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}
 show ?thesis by (simp add: vt_p.RAG_es vt_p.wne)
 qed
 end
-section {* RAG is finite *}
+subsection {* RAG is finite *}
 context valid_trace_v
 begin
 lemma
 by (unfold_locales, simp)
 show ?thesis using Cons by simp
 qed
 qed
 end
-section {* RAG is acyclic *}
 subsection {* Uniqueness of waiting *}
 text {*
 {\em Uniqueness of waiting} means that
 thus ?thesis by (unfold RAG_es, simp)
 qed
 end
+subsection {* RAG is acyclic *}
 context valid_trace
 begin
 text {*
 With these @{text "acylic_RAG_kept"}-lemmas proved,
 qed
 qed
 end
-section {* RAG is single-valued *}
+subsection {* RAG is single-valued *}
 text {*
 The proof that @{term RAG} is single-valued makes use of
 @{text "unique_waiting"} and @{thm held_unique} and the
 proof itself is very simple:
 lemma sgv_RAG: "single_valued (RAG s)"
 using unique_RAG by (auto simp:single_valued_def)
 end
-section {* RAG is well-founded *}
+subsection {* RAG is well-founded *}
 text {*
 In this section, it is proved that both @{term RAG} and
 its converse @{term "(RAG s)^-1"} are well-founded.
 The proof is very simple with the help of
 show "acyclic (RAG s)" .
 qed
 end
-section {* RAG forms a finite-branching forest (or tree) *}
+subsection {* RAG forms a finite-branching forest (or tree) *}
 text {*
 With all the well-formedness proofs about @{term RAG} in place,
 it is easy to show.
 *}
 from wf_RAG show "wf (RAG s)" .
 qed
 qed
 qed
+subsection {* Derived properties for sub-graphs of RAG *}
-section {* Derived properties for sub-graphs of RAG *}
 context valid_trace
 begin
 lemma acyclic_tRAG: "acyclic (tRAG s)"
 qed
 section {* Chain to readys *}
 text {*
-In this section, a more complete view of @{term RAG} and @{term threads}
+In this section, based on the just derived
-are given.
+properties about the shape of @{term RAG},
+a more complete view of the relationship
+between threads is established.
 *}
 context valid_trace
 begin
 text {*
-The first lemma is technical, which says out of any node in the domain
+The first lemma is technical, which says out of any node
-of @{term RAG}, there is a path leading to a ready thread.
+in the domain of @{term RAG},
+(no matter whether it is thread node or resource node)
+there is a path leading to a ready thread.
 *}
 lemma chain_building:
 assumes "node \<in> Domain (RAG s)"
 obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"
 } thus ?thesis by auto
 qed
 end
-(* ccc *)
 section {* Relating @{term cp} and @{term the_preced} and @{term preced} *}
+text {*
+@{term cp} of a thread is defined to be the maximum of
+the @{term preced}-values (precedences) of all threads in
+its subtree given by @{term RAG}. Therefore, there exits
+a relationship between @{term cp} and @{term preced} (and
+also its variation @{term "the_preced"}) to be explored,
+and this is the target of this section.
+*}
 context valid_trace
 begin
-lemma finite_threads:
+text {*
-shows "finite (threads s)"
+Since @{term cp} is the maximum of all @{term preced}s in its subtree,
-using vt by (induct) (auto elim: step.cases)
+which includes itself, it is not difficult to show
+that the one thread's precedence is less or equal to its
-lemma  finite_readys: "finite (readys s)"
+@{text cp}-value:
-using finite_threads readys_threads rev_finite_subset by blast
+*}
 lemma le_cp:
 shows "preced th s \<le> cp s th"
 proof(unfold cp_alt_def, rule Max_ge)
 show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
 by (simp add: finite_subtree_threads)
 next
 show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}"
 by (simp add: subtree_def the_preced_def)
 qed
+text {*
+Since @{term cp} is the maximum precedence of its subtree,
+and the subtree is only a subset of the set of all threads,
+it can be shown that @{text cp} is less or equal to the maximum of
+all threads:
+*}
 lemma cp_le:
 assumes th_in: "th \<in> threads s"
 shows "cp s th \<le> Max (the_preced s ` threads s)"
 proof(unfold cp_alt_def, rule Max_f_mono)
 using assms
 by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq
 node.inject(1) rtranclD subsetI subtree_def trancl_domain)
 qed
+text {*
+Since the @{term cp}-value of each individual thread is less or equal to the
+maximum precedence value of all threads (shown in lemma @{thm cp_le}),
+it is easy to derive further that maximum @{term "cp"}-value of
+all threads is also less or equal to the latter.
+On the other hand, since the precedence value of each individual
+thread is less of equal to its own @{term cp}-value (shown in lemma @{thm le_cp}),
+it is easy to show that the maximum of the former is less or equal to the
+maximum of the latter.
+By combining these two perspectives, we get the following equality
+between the two maximums:
+*}
 lemma max_cp_eq:
 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
 (is "?L = ?R")
 proof -
 have "?L \<le> ?R"
 simp add: le_cp the_preced_def)
 ultimately show ?thesis by auto
 qed
 text {* (* ddd *) \noindent
-Since the current precedence of the threads in ready queue will always be boosted,
+According to @{thm threads_alt_def} and @{thm readys_subtree_disjoint} ,
-there must be one inside it has the maximum precedence of the whole system.
+the set of @{term threads} can be partitioned into subtrees of the
-*}
+threads in @{term readys}, and also because  @{term cp}-value of a thread is
-lemma max_cp_readys_threads:
+the maximum precedence of its own subtree, by applying
-shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
+the absorbing property of @{term Max} (lemma @{thm Max_UNION})
+over the union of subtrees, the following equation can be derived:
+*}
+lemma max_cp_readys_max_preced:
+shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
 proof(cases "readys s = {}")
 case False
-have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
+have "?R =
-also have "... =
+Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
-Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
+by (simp add: threads_alt_def)
-by (unfold threads_alt_def, simp)
 also have "... =
 Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
 by (unfold image_UN, simp)
 also have "... =
 Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)"
 proof(rule Max_UNION)
 show "\<forall>M\<in>(\<lambda>x. the_preced s `
 {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
 using finite_subtree_threads by auto
 qed (auto simp:False subtree_def finite_readys)
 also have "... =
-Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)"
+Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) `
-by (unfold image_comp, simp)
+readys s)"
+by (simp add: image_comp)
 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
 proof -
 have "(?f ` ?A) = (?g ` ?A)"
 proof(rule f_image_eq)
 fix th1
 thus ?thesis by simp
 qed
 finally show ?thesis by simp
 qed (auto simp:threads_alt_def)
-end
+text {*
+The following lemma is simply a corollary of @{thm max_cp_readys_max_preced}
+and @{thm max_cp_eq}:
+*}
+lemma max_cp_readys_threads:
+shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
+using max_cp_readys_max_preced max_cp_eq by auto
+end
 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}
+text {*
+As explained in the section where @{term "cntP"},
+@{term "cntV"} and @{term "cntCS"} are defined,
+we need to establish a equation (in lemma @{text "cnp_cnv_cncs"})
+so that the last can be calculated out of the first two.
+While the calculation of @{term "cntV"} and @{term "cntCS"}
+are relatively simple, the calculation of @{term "cntCS"} and
+@{term "pvD"} are complicated, because their definitions
+involve a number of other functions such as @{term holdents}, @{term readys},
+and @{term threads}. To prove  @{text "cnp_cnv_cncs"},
+we need to investigate how the values of these functions
+are changed with the execution of each kind of system operation.
+Following conventions, such investigation are divided into
+locales corresponding to system operations.
+*}
 context valid_trace_p_w
 begin
 lemma holding_s_holder: "holding s holder cs"
 section {* Corollaries of @{thm valid_trace.cnp_cnv_cncs} *}
 context valid_trace
 begin
+text {*
+The following two lemmas are purely technical, which says
+a non-living thread can not hold any resource.
+*}
 lemma not_thread_holdents:
 assumes not_in: "th \<notin> threads s"
 shows "holdents s th = {}"
 proof -
 { fix cs
 lemma not_thread_cncs:
 assumes not_in: "th \<notin> threads s"
 shows "cntCS s th = 0"
 using not_thread_holdents[OF assms]
 by (simp add:cntCS_def)
+text {*
+Starting from the following @{text cnp_cnv_eq}, all
+lemmas in this section concern the meaning of
+condition @{prop "cntP s th = cntV s th"}, i.e.
+when the numbers of resource requesting and resource releasing
+are equal.
+*}
 lemma cnp_cnv_eq:
 assumes "th \<notin> threads s"
 shows "cntP s th = cntV s th"
 using assms cnp_cnv_cncs not_thread_cncs pvD_def
 by (auto simp:children_def)
 with eq_pv_children[OF assms]
 show False by simp
 qed
+lemma count_eq_RAG_plus_Th:
+assumes "cntP s th = cntV s th"
+shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+using count_eq_RAG_plus[OF assms] by auto
 lemma eq_pv_dependants:
 assumes eq_pv: "cntP s th = cntV s th"
 shows "dependants s th = {}"
 proof -
 from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
 lemma count_eq_tRAG_plus:
 assumes "cntP s th = cntV s th"
 shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
 using assms eq_pv_dependants dependants_alt_def eq_dependants by auto
-lemma count_eq_RAG_plus_Th:
-assumes "cntP s th = cntV s th"
-shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
-using count_eq_RAG_plus[OF assms] by auto
 lemma count_eq_tRAG_plus_Th:
 assumes "cntP s th = cntV s th"
 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
 using count_eq_tRAG_plus[OF assms] by auto
 end
+subsection {* A notion @{text detached} and its relation with @{term cntP}
+and @{term cntV} *}
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
 where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
+text {*
+The following lemma shows that a thread is detached means
+it is isolated from @{term RAG}:
+*}
 lemma detached_test:
 shows "detached s th = (Th th \<notin> Field (RAG s))"
 apply(simp add: detached_def Field_def)
 apply(simp add: s_RAG_def)
 shows "(detached s th) = (cntP s th = cntV s th)"
 by (insert vt, auto intro:detached_intro detached_elim)
 end
-section {* Recursive definition of @{term "cp"} *}
-lemma cp_alt_def1:
-"cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
-proof -
-have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
-((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
-by auto
-thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
-qed
-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
 section {* Other properties useful in Implementation.thy or Correctness.thy *}
 context valid_trace_e
 begin

changeset 115	74fc1eae4605
parent 114	81c6ede5cd11
child 116	a7441db6f4e1