pip: comparison Correctness.thy~

equal deleted inserted replaced

-:2af87bb52fca
+:25fd656667a7
 by (unfold vat_s.cp_rec, rule Max_ge,
 auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
 ultimately show ?thesis by auto
 qed
-(* ccc *)
 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
 by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)
 lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"
 by (fold eq_cp_s_th, unfold highest_cp_preced, simp)
 sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
 by (unfold highest_gen_def, auto dest:step_back_vt_app)
 context extend_highest_gen
 begin
 lemma ind [consumes 0, case_names Nil Cons, induct type]:
 by (metis Max.coboundedI finite_imageI highest not_le order.trans
 preced_linorder rev_image_eqI threads_s vat_s.finite_threads
 vat_s.le_cp)
 text {*
+The following lemmas shows that the @{term cp}-value
+of the blocking thread @{text th'} equals to the highest
+precedence in the whole system.
+*}
+lemma runing_preced_inversion:
+assumes runing': "th' \<in> runing (t@s)"
+shows "cp (t@s) th' = preced th s" (is "?L = ?R")
+proof -
+have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
+by (unfold runing_def, auto)
+also have "\<dots> = ?R"
+by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
+finally show ?thesis .
+qed
+text {*
 Counting of the number of @{term "P"} and @{term "V"} operations
 is the cornerstone of a large number of the following proofs.
 The reason is that this counting is quite easy to calculate and
 convenient to use in the reasoning.
 The following lemma shows that the counting controls whether
 a thread is running or not.
-*}
+*} (* ccc *)
-lemma pv_blocked_pre: (* ddd *)
+lemma eq_pv_blocked: (* ddd *)
-assumes th'_in: "th' \<in> threads (t@s)"
+assumes neq_th': "th' \<noteq> th"
-and neq_th': "th' \<noteq> th"
 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
 shows "th' \<notin> runing (t@s)"
 proof
 assume otherwise: "th' \<in> runing (t@s)"
 show False
 proof -
+have th'_in: "th' \<in> threads (t@s)"
+using otherwise readys_threads runing_def by auto
 have "th' = th"
 proof(rule preced_unique)
+-- {* The proof goes like this:
+it is first shown that the @{term preced}-value of @{term th'}
+equals to that of @{term th}, then by uniqueness
+of @{term preced}-values (given by lemma @{thm preced_unique}),
+@{term th'} equals to @{term th}: *}
 show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
 proof -
+-- {* Since the counts of @{term th'} are balanced, the subtree
+of it contains only itself, so, its @{term cp}-value
+equals its @{term preced}-value: *}
 have "?L = cp (t@s) th'"
 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
-also have "... = cp (t @ s) th" using otherwise
+-- {* Since @{term "th'"} is running by @{thm otherwise},
-by (metis (mono_tags, lifting) mem_Collect_eq
+it has the highest @{term cp}-value, by definition,
-runing_def th_cp_max vat_t.max_cp_readys_threads)
+which in turn equals to the @{term cp}-value of @{term th}. *}
-also have "... = ?R" by (metis th_cp_preced th_kept)
+also have "... = ?R"
+using runing_preced_inversion[OF otherwise] th_kept by simp
 finally show ?thesis .
 qed
 qed (auto simp: th'_in th_kept)
 moreover have "th' \<noteq> th" using neq_th' .
 ultimately show ?thesis by simp
 qed
 qed
-lemmas pv_blocked = pv_blocked_pre[folded detached_eq]
+lemmas eq_pv_blocked_dtc = eq_pv_blocked[folded detached_eq]
-lemma runing_precond_pre: (* ddd *)
-fixes th'
+lemma eq_pv_kept: (* ddd *)
 assumes th'_in: "th' \<in> threads s"
 and eq_pv: "cntP s th' = cntV s th'"
 and neq_th': "th' \<noteq> th"
 shows "th' \<in> threads (t@s) \<and>
 cntP (t@s) th' = cntV (t@s) th'"
 have "step (t@s) (P thread cs)" using Cons P by auto
 thus ?thesis
 proof(cases)
 assume "thread \<in> runing (t@s)"
 moreover have "th' \<notin> runing (t@s)" using Cons(5)
-by (metis neq_th' vat_t.pv_blocked_pre)
+by (metis neq_th' vat_t.eq_pv_blocked)
 ultimately show ?thesis by auto
 qed
 qed with Cons show ?thesis
 by (unfold P, simp add:cntP_def cntV_def count_def)
 qed
 have "step (t@s) (V thread cs)" using Cons V by auto
 thus ?thesis
 proof(cases)
 assume "thread \<in> runing (t@s)"
 moreover have "th' \<notin> runing (t@s)" using Cons(5)
-by (metis neq_th' vat_t.pv_blocked_pre)
+by (metis neq_th' vat_t.eq_pv_blocked)
 ultimately show ?thesis by auto
 qed
 qed with Cons show ?thesis
 by (unfold V, simp add:cntP_def cntV_def count_def)
 qed
 proof -
 have neq_thread: "thread \<noteq> th'"
 proof -
 have "step (t@s) (Exit thread)" using Cons Exit by auto
 thus ?thesis apply (cases) using Cons(5)
-by (metis neq_th' vat_t.pv_blocked_pre)
+by (metis neq_th' vat_t.eq_pv_blocked)
 qed
 hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons
 by (unfold Exit, simp add:cntP_def cntV_def count_def)
 moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread
 by (unfold Exit, simp)
 case Nil
 with assms
 show ?case by auto
 qed
+(* runing_precond has changed to eq_pv_kept *)
 text {* Changing counting balance to detachedness *}
-lemmas runing_precond_pre_dtc = runing_precond_pre
+lemmas eq_pv_kept_dtc = eq_pv_kept
 [folded vat_t.detached_eq vat_s.detached_eq]
-lemma runing_precond: (* ddd *)
+section {* The blocking thread *}
-fixes th'
+text {*
+The purpose of PIP is to ensure that the most
+urgent thread @{term th} is not blocked unreasonably.
+Therefore, a clear picture of the blocking thread is essential
+to assure people that the purpose is fulfilled.
+The following lemmas will give us such a picture:
+*}
+(* ccc *)
+text {*
+The following lemma shows the blocking thread @{term th'}
+must hold some resource in the very beginning.
+*}
+lemma runing_cntP_cntV_inv: (* ddd *)
 assumes th'_in: "th' \<in> threads s"
 and neq_th': "th' \<noteq> th"
 and is_runing: "th' \<in> runing (t@s)"
 shows "cntP s th' > cntV s th'"
 using assms
-proof -
+proof - (* ccc *)
+-- {* First, it can be shown that the number of @{term P} and
+@{term V} operations can not be equal for thred @{term th'} *}
 have "cntP s th' \<noteq> cntV s th'"
-by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in)
+proof
+assume otherwise: "cntP s th' = cntV s th'"
+-- {* The proof goes by contradiction. *}
+-- {* We can show that @{term th'} can not be running at moment @{term "t@s"}: *}
+have "th' \<notin> runing (t@s)"
+proof(rule eq_pv_blocked)
+show "th' \<noteq> th" using neq_th' by simp
+next
+show "cntP (t @ s) th' = cntV (t @ s) th'"
+using eq_pv_kept[OF th'_in otherwise neq_th'] by simp
+qed
+-- {* This is obvious in contradiction with assumption @{thm is_runing}  *}
+thus False using is_runing by simp
+qed
 moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
 ultimately show ?thesis by auto
 qed
 lemma moment_blocked_pre:
 assume "Exit th' \<in> set (moment j (restm i t))"
 thus "th' \<noteq> th"
 by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append)
 qed
 show ?thesis
-by (metis add.commute append_assoc eq_pv h.runing_precond_pre
+by (metis add.commute append_assoc eq_pv h.eq_pv_kept
 moment_plus_split neq_th' th'_in)
 qed
 lemma moment_blocked_eqpv: (* ddd *)
 assumes neq_th': "th' \<noteq> th"
 and h2: "th' \<in> threads ((moment j t)@s)" by auto
 moreover have "th' \<notin> runing ((moment j t)@s)"
 proof -
 interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
 show ?thesis
-using h.pv_blocked_pre h1 h2 neq_th' by auto
+using h.eq_pv_blocked h1 h2 neq_th' by auto
 qed
 ultimately show ?thesis by auto
 qed
 (* The foregoing two lemmas are preparation for this one, but
 in long run can be combined. Maybe I am wrong.
+This one is useless (* XY *)
 *)
 lemma moment_blocked:
 assumes neq_th': "th' \<noteq> th"
 and th'_in: "th' \<in> threads ((moment i t)@s)"
 and dtc: "detached (moment i t @ s) th'"
 by (metis dtc h_i.detached_elim)
 from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij]
 show ?thesis by (metis h_j.detached_intro)
 qed
-lemma runing_preced_inversion:
+text {*
+The following lemmas shows the blocking thread @{text th'} must be live
+at the very beginning, i.e. the moment (or state) @{term s}.
+*}
+lemma runing_threads_inv: (* ddd *) (* ccc *)
 assumes runing': "th' \<in> runing (t@s)"
-shows "cp (t@s) th' = preced th s" (is "?L = ?R")
+and neq_th': "th' \<noteq> th"
-proof -
-have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
-by (unfold runing_def, auto)
-also have "\<dots> = ?R"
-by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
-finally show ?thesis .
-qed
-text {*
-The situation when @{term "th"} is blocked is analyzed by the following lemmas.
-*}
-text {*
-The following lemmas shows the running thread @{text "th'"}, if it is different from
-@{term th}, must be live at the very beginning. By the term {\em the very beginning},
-we mean the moment where the formal investigation starts, i.e. the moment (or state)
-@{term s}.
-*}
-lemma runing_inversion_0:
-assumes neq_th': "th' \<noteq> th"
-and runing': "th' \<in> runing (t@s)"
 shows "th' \<in> threads s"
 proof -
 -- {* The proof is by contradiction: *}
 { assume otherwise: "\<not> ?thesis"
 have "th' \<notin> runing (t @ s)"
 with `th' \<in> runing (t@s)`
 have False by simp
 } thus ?thesis by auto
 qed
 text {*
-The second lemma says, if the running thread @{text th'} is different from
+The following lemma summarizes several foregoing
-@{term th}, then this @{text th'} must in the possession of some resources
+lemmas to give an overall picture of the blocking thread @{text "th'"}:
-at the very beginning.
+*}
+lemma runing_inversion:
-To ease the reasoning of resource possession of one particular thread,
-we used two auxiliary functions @{term cntV} and @{term cntP},
-which are the counters of @{term P}-operations and
-@{term V}-operations respectively.
-If the number of @{term V}-operation is less than the number of
-@{term "P"}-operations, the thread must have some unreleased resource.
-*}
-lemma runing_inversion_1: (* ddd *)
-assumes neq_th': "th' \<noteq> th"
-and runing': "th' \<in> runing (t@s)"
--- {* thread @{term "th'"} is a live on in state @{term "s"} and
-it has some unreleased resource. *}
-shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
-proof -
--- {* The proof is a simple composition of @{thm runing_inversion_0} and
-@{thm runing_precond}: *}
--- {* By applying @{thm runing_inversion_0} to assumptions,
-it can be shown that @{term th'} is live in state @{term s}: *}
-have "th' \<in> threads s"  using runing_inversion_0[OF assms(1,2)] .
--- {* Then the thesis is derived easily by applying @{thm runing_precond}: *}
-with runing_precond [OF this neq_th' runing'] show ?thesis by simp
-qed
-text {*
-The following lemma is just a rephrasing of @{thm runing_inversion_1}:
-*}
-lemma runing_inversion_2:
-assumes runing': "th' \<in> runing (t@s)"
-shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
-proof -
-from runing_inversion_1[OF _ runing']
-show ?thesis by auto
-qed
-lemma runing_inversion_3:
-assumes runing': "th' \<in> runing (t@s)"
-and neq_th: "th' \<noteq> th"
-shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
-by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)
-lemma runing_inversion_4:
 assumes runing': "th' \<in> runing (t@s)"
 and neq_th: "th' \<noteq> th"
 shows "th' \<in> threads s"
 and    "\<not>detached s th'"
 and    "cp (t@s) th' = preced th s"
-apply (metis neq_th runing' runing_inversion_2)
+proof -
-apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)
+from runing_threads_inv[OF assms]
-by (metis neq_th runing' runing_inversion_3)
+show "th' \<in> threads s" .
+next
+from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing']
+show "\<not>detached s th'" using vat_s.detached_eq by simp
+next
+from runing_preced_inversion[OF runing']
+show "cp (t@s) th' = preced th s" .
+qed
 text {*
 Suppose @{term th} is not running, it is first shown that
 there is a path in RAG leading from node @{term th} to another thread @{text "th'"}
 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).

changeset 67	25fd656667a7
parent 66	2af87bb52fca
child 68	db196b066b97