pip: comparison Correctness.thy~

equal deleted inserted replaced

-:3fa70b12c117
+:b0054fb0d1ce
 theory Correctness
 imports PIPBasics
 begin
 text {*
 The following two auxiliary lemmas are used to reason about @{term Max}.
 *}
 lemma image_Max_eqI:
 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
-lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
+lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)"
-by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)
+using eq_cp_s_th highest max_cp_eq the_preced_def by presburger
-lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"
+lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)"
 by (fold eq_cp_s_th, unfold highest_cp_preced, simp)
 lemma highest': "cp s th = Max (cp s ` threads s)"
-proof -
+by (simp add: eq_cp_s_th highest)
-from highest_cp_preced max_cp_eq[symmetric]
-show ?thesis by simp
-qed
 end
 locale extend_highest_gen = highest_gen +
 fixes t
 from vt_et show "vt (e # t @ s)" by simp
 qed
 qed
 qed
 qed
 locale red_extend_highest_gen = extend_highest_gen +
 fixes i::nat
 sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
 The proof goes by induction over @{text "t"} using the specialized
 induction rule @{thm ind}, followed by case analysis of each possible
 operations of PIP. All cases follow the same pattern rendered by the
 generalized introduction rule @{thm "image_Max_eqI"}.
-The very essence is to show that precedences, no matter whether they are newly introduced
+The very essence is to show that precedences, no matter whether they
-or modified, are always lower than the one held by @{term "th"},
+are newly introduced or modified, are always lower than the one held
-which by @{thm th_kept} is preserved along the way.
+by @{term "th"}, which by @{thm th_kept} is preserved along the way.
 *}
 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
 proof(induct rule:ind)
 case Nil
 from highest_preced_thread
-show ?case
+show ?case by simp
-by (unfold the_preced_def, simp)
 next
 case (Cons e t)
 interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
 interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
 show ?case
 thus "?f x \<le> ?f th"
 proof
 assume "x = thread"
 thus ?thesis
 apply (simp add:Create the_preced_def preced_def, fold preced_def)
-using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force
+using Create h_e.create_low h_t.th_kept lt_tm preced_leI2
+preced_th by force
 next
 assume h: "x \<in> threads (t @ s)"
 from Cons(2)[unfolded Create]
 have "x \<noteq> thread" using h by (cases, auto)
 hence "?f x = the_preced (t@s) x"
 qed
 also have "... = ?R" by (simp add: max_preced the_preced_def)
 finally show ?thesis .
 qed
-lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"
+lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th"
 using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger
-lemma th_cp_preced: "cp (t@s) th = preced th s"
+lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))"
+by (simp add: th_cp_max_preced)
+lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th"
+using max_kept th_kept the_preced_def by auto
+lemma [simp]: "the_preced (t@s) th = preced th (t@s)"
+using the_preced_def by auto
+lemma [simp]: "preced th (t@s) = preced th s"
+by (simp add: th_kept)
+lemma [simp]: "cp s th = preced th s"
+by (simp add: eq_cp_s_th)
+lemma th_cp_preced [simp]: "cp (t@s) th = preced th s"
 by (fold max_kept, unfold th_cp_max_preced, simp)
 lemma preced_less:
 assumes th'_in: "th' \<in> threads s"
 and neq_th': "th' \<noteq> th"
 using assms
 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)
+section {* The `blocking thread` *}
+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.
+In this section, we are going to derive a series of lemmas
+with finally give rise to a picture of the blocking thread.
+By `blocking thread`, we mean a thread in running state but
+different from thread @{term th}.
+*}
 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.
 *}
 also have "\<dots> = ?R"
 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
 finally show ?thesis .
 qed
-section {* The `blocking thread` *}
+text {*
+The following lemma shows how the counting of
-text {*
+@{term "P"} and @{term "V"} operations affects
-Counting of the number of @{term "P"} and @{term "V"} operations
+the running state of threads in @{term t}.
-is the cornerstone of a large number of the following proofs.
-The reason is that this counting is quite easy to calculate and
+The lemma shows that if a thread's @{term "P"}-count equals
-convenient to use in the reasoning.
+its @{term "V"}-count (which means it no longer has any
+resource in its possession), it can not be in running thread.
-The following lemma shows that the counting controls whether
-a thread is running or not.
+The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
-*} (* ccc *)
+The key is the use of @{thm count_eq_dependants}
+to derive the emptiness of @{text th'}s @{term dependants}-set
+from the balance of its @{term P} @{term V} counts.
+From this, it can be shown @{text th'}s @{term cp}-value
+equals to its own precedence.
+On the other hand, since @{text th'} is running, by
+@{thm runing_preced_inversion}, its @{term cp}-value
+equals to the precedence of @{term th}.
+Combining the above two we have that @{text th'} and
+@{term th} have the same precedence. By uniqueness of precedence, we
+have @{text "th' = th"}, which is in contradiction with the
+assumption @{text "th' \<noteq> th"}.
+*}
 lemma eq_pv_blocked: (* ddd *)
 assumes neq_th': "th' \<noteq> th"
 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
 shows "th' \<notin> runing (t@s)"
 -- {* 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)
--- {* Since @{term "th'"} is running by @{thm otherwise},
+-- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
-it has the highest @{term cp}-value, by definition,
+its @{term cp}-value equals @{term "preced th s"},
-which in turn equals to the @{term cp}-value of @{term th}. *}
+which equals to @{term "?R"} by simplification: *}
 also have "... = ?R"
-using runing_preced_inversion[OF otherwise] th_kept by simp
+thm runing_preced_inversion
+using runing_preced_inversion[OF otherwise] by simp
 finally show ?thesis .
 qed
 qed (auto simp: th'_in th_kept)
-moreover have "th' \<noteq> th" using neq_th' .
+with `th' \<noteq> th` show ?thesis by simp
-ultimately show ?thesis by simp
 qed
 qed
 text {*
 The following lemma is the extrapolation of @{thm eq_pv_blocked}.
 and eq_pv: "cntP s th' = cntV s th'"
 shows "th' \<notin> runing (t@s)"
 using assms
 by (simp add: eq_pv_blocked eq_pv_persist)
-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:
-*}
 text {*
 The following lemma shows the blocking thread @{term th'}
 must hold some resource in the very beginning.
 *}
 lemma runing_cntP_cntV_inv: (* ddd *)
 next
 case False
 thus ?thesis using th_blockedE by auto
 qed
 end
 end

changeset 73	b0054fb0d1ce
parent 68	db196b066b97