--- a/Correctness.thy Sat Jan 09 22:19:27 2016 +0800
+++ b/Correctness.thy Tue Jan 12 08:35:36 2016 +0800
@@ -79,17 +79,15 @@
ultimately show ?thesis by auto
qed
-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_cp_preced: "cp s th = Max (the_preced s ` threads s)"
+ 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 -
- from highest_cp_preced max_cp_eq[symmetric]
- show ?thesis by simp
-qed
+ by (simp add: eq_cp_s_th highest)
end
@@ -125,7 +123,6 @@
qed
qed
-
locale red_extend_highest_gen = extend_highest_gen +
fixes i::nat
@@ -248,16 +245,15 @@
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
- or modified, are always lower than the one held by @{term "th"},
- which by @{thm th_kept} is preserved along the way.
+ The very essence is to show that precedences, no matter whether they
+ are newly introduced or modified, are always lower than the one held
+ 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
- by (unfold the_preced_def, simp)
+ show ?case by simp
next
case (Cons e t)
interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
@@ -285,7 +281,8 @@
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]
@@ -440,10 +437,25 @@
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:
@@ -455,6 +467,21 @@
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
@@ -471,17 +498,31 @@
finally show ?thesis .
qed
-section {* The `blocking thread` *}
+text {*
+ The following lemma shows how the counting of
+ @{term "P"} and @{term "V"} operations affects
+ the running state of threads in @{term t}.
+
+ The lemma shows that if a thread's @{term "P"}-count equals
+ its @{term "V"}-count (which means it no longer has any
+ resource in its possession), it can not be in running thread.
-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 proof is by contraction with the assumption @{text "th' \<noteq> th"}.
+ 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.
- The following lemma shows that the counting controls whether
- a thread is running or not.
-*} (* ccc *)
+ 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"
@@ -507,16 +548,16 @@
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},
- it has the highest @{term cp}-value, by definition,
- which in turn equals to the @{term cp}-value of @{term th}. *}
+ -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
+ its @{term cp}-value equals @{term "preced th s"},
+ 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' .
- ultimately show ?thesis by simp
+ with `th' \<noteq> th` show ?thesis by simp
qed
qed
@@ -589,15 +630,6 @@
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.