--- a/PrioG.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/PrioG.thy Tue May 06 14:36:40 2014 +0100
@@ -375,15 +375,15 @@
by auto
-lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"
+lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
apply (induct s, auto)
by (case_tac a, auto split:if_splits)
-lemma birthtime_unique:
- "\<lbrakk>birthtime th1 s = birthtime th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
+lemma last_set_unique:
+ "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
\<Longrightarrow> th1 = th2"
apply (induct s, auto)
- by (case_tac a, auto split:if_splits dest:birthtime_lt)
+ by (case_tac a, auto split:if_splits dest:last_set_lt)
lemma preced_unique :
assumes pcd_eq: "preced th1 s = preced th2 s"
@@ -391,8 +391,8 @@
and th_in2: " th2 \<in> threads s"
shows "th1 = th2"
proof -
- from pcd_eq have "birthtime th1 s = birthtime th2 s" by (simp add:preced_def)
- from birthtime_unique [OF this th_in1 th_in2]
+ from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
+ from last_set_unique [OF this th_in1 th_in2]
show ?thesis .
qed
@@ -2100,8 +2100,8 @@
proof -
from runing_1 and runing_2 have "cp s th1 = cp s th2"
by (unfold runing_def, simp)
- hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)) =
- Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependents (wq s) th2))"
+ hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
+ Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
(is "Max (?f ` ?A) = Max (?f ` ?B)")
by (unfold cp_eq_cpreced cpreced_def)
obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
@@ -2110,7 +2110,7 @@
proof -
have "finite ?A"
proof -
- have "finite (dependents (wq s) th1)"
+ have "finite (dependants (wq s) th1)"
proof-
have "finite {th'. (Th th', Th th1) \<in> (depend (wq s))\<^sup>+}"
proof -
@@ -2128,7 +2128,7 @@
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
- thus ?thesis by (simp add:cs_dependents_def)
+ thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
@@ -2149,7 +2149,7 @@
proof -
have "finite ?B"
proof -
- have "finite (dependents (wq s) th2)"
+ have "finite (dependants (wq s) th2)"
proof-
have "finite {th'. (Th th', Th th2) \<in> (depend (wq s))\<^sup>+}"
proof -
@@ -2167,7 +2167,7 @@
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
- thus ?thesis by (simp add:cs_dependents_def)
+ thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
@@ -2186,12 +2186,12 @@
have eq_preced: "preced th1' s = preced th2' s" by auto
hence eq_th12: "th1' = th2'"
proof (rule preced_unique)
- from th1_in have "th1' = th1 \<or> (th1' \<in> dependents (wq s) th1)" by simp
+ from th1_in have "th1' = th1 \<or> (th1' \<in> dependants (wq s) th1)" by simp
thus "th1' \<in> threads s"
proof
- assume "th1' \<in> dependents (wq s) th1"
+ assume "th1' \<in> dependants (wq s) th1"
hence "(Th th1') \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (depend s)" by (simp add:trancl_domain)
from dm_depend_threads[OF vt this] show ?thesis .
@@ -2201,12 +2201,12 @@
by (unfold runing_def readys_def, auto)
qed
next
- from th2_in have "th2' = th2 \<or> (th2' \<in> dependents (wq s) th2)" by simp
+ from th2_in have "th2' = th2 \<or> (th2' \<in> dependants (wq s) th2)" by simp
thus "th2' \<in> threads s"
proof
- assume "th2' \<in> dependents (wq s) th2"
+ assume "th2' \<in> dependants (wq s) th2"
hence "(Th th2') \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (depend s)" by (simp add:trancl_domain)
from dm_depend_threads[OF vt this] show ?thesis .
@@ -2216,21 +2216,21 @@
by (unfold runing_def readys_def, auto)
qed
qed
- from th1_in have "th1' = th1 \<or> th1' \<in> dependents (wq s) th1" by simp
+ from th1_in have "th1' = th1 \<or> th1' \<in> dependants (wq s) th1" by simp
thus ?thesis
proof
assume eq_th': "th1' = th1"
- from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
+ from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp
next
- assume "th2' \<in> dependents (wq s) th2"
- with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp
+ assume "th2' \<in> dependants (wq s) th2"
+ with eq_th12 eq_th' have "th1 \<in> dependants (wq s) th2" by simp
hence "(Th th1, Th th2) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
hence "Th th1 \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def)
@@ -2243,16 +2243,16 @@
thus ?thesis by simp
qed
next
- assume th1'_in: "th1' \<in> dependents (wq s) th1"
- from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
+ assume th1'_in: "th1' \<in> dependants (wq s) th1"
+ from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2"
- with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp
+ with th1'_in eq_th12 have "th2 \<in> dependants (wq s) th1" by simp
hence "(Th th2, Th th1) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
hence "Th th2 \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def)
@@ -2264,12 +2264,12 @@
by (auto simp:eq_waiting)
thus ?thesis by simp
next
- assume "th2' \<in> dependents (wq s) th2"
- with eq_th12 have "th1' \<in> dependents (wq s) th2" by simp
+ assume "th2' \<in> dependants (wq s) th2"
+ with eq_th12 have "th1' \<in> dependants (wq s) th2" by simp
hence h1: "(Th th1', Th th2) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
from th1'_in have h2: "(Th th1', Th th1) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
show ?thesis
proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
@@ -2415,10 +2415,10 @@
"depend (wq s) = depend s"
by (unfold cs_depend_def s_depend_def, auto)
-lemma count_eq_dependents:
+lemma count_eq_dependants:
assumes vt: "vt s"
and eq_pv: "cntP s th = cntV s th"
- shows "dependents (wq s) th = {}"
+ shows "dependants (wq s) th = {}"
proof -
from cnp_cnv_cncs[OF vt] and eq_pv
have "cntCS s th = 0"
@@ -2429,9 +2429,9 @@
by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
- by (unfold cntCS_def holdents_test cs_dependents_def, auto)
+ by (unfold cntCS_def holdents_test cs_dependants_def, auto)
show ?thesis
- proof(unfold cs_dependents_def)
+ proof(unfold cs_dependants_def)
{ assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
then obtain th' where "(Th th', Th th) \<in> (depend (wq s))\<^sup>+" by auto
hence "False"
@@ -2448,10 +2448,10 @@
qed
qed
-lemma dependents_threads:
+lemma dependants_threads:
fixes s th
assumes vt: "vt s"
- shows "dependents (wq s) th \<subseteq> threads s"
+ shows "dependants (wq s) th \<subseteq> threads s"
proof
{ fix th th'
assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (depend (wq s))\<^sup>+}"
@@ -2466,9 +2466,9 @@
have "th \<in> threads s" .
} note hh = this
fix th1
- assume "th1 \<in> dependents (wq s) th"
+ assume "th1 \<in> dependants (wq s) th"
hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (depend (wq s))\<^sup>+}"
- by (unfold cs_dependents_def, simp)
+ by (unfold cs_dependants_def, simp)
from hh [OF this] show "th1 \<in> threads s" .
qed
@@ -2495,7 +2495,7 @@
assumes vt: "vt s"
and th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
-proof(unfold cp_eq_cpreced cpreced_def cs_dependents_def)
+proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}))
\<le> Max ((\<lambda>th. preced th s) ` threads s)"
(is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
@@ -2518,9 +2518,9 @@
assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
- show "Prc (original_priority th s) (birthtime th s)
- \<le> Max (insert (Prc (original_priority th s) (birthtime th s))
- ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))"
+ show "Prc (priority th s) (last_set th s)
+ \<le> Max (insert (Prc (priority th s) (last_set th s))
+ ((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
(is "?l \<le> Max (insert ?l ?A)")
proof(cases "?A = {}")
case False
@@ -2544,7 +2544,7 @@
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
- thus ?thesis by (simp add:cs_dependents_def)
+ thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
@@ -2629,28 +2629,28 @@
and tm_chain:"(Th tm, Th th') \<in> (depend s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
- from dependents_threads[OF vt] finite_threads[OF vt]
- show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th'))"
+ from dependants_threads[OF vt] finite_threads[OF vt]
+ show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
by (auto intro:finite_subset)
next
- fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')"
+ fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
moreover have "p \<le> \<dots>"
proof(rule Max_ge)
from finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- from p_in and th'_in and dependents_threads[OF vt, of th']
+ from p_in and th'_in and dependants_threads[OF vt, of th']
show "p \<in> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
ultimately show "p \<le> preced tm s" by auto
next
- show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')"
+ show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
proof -
from tm_chain
- have "tm \<in> dependents (wq s) th'"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, auto)
+ have "tm \<in> dependants (wq s) th'"
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, auto)
thus ?thesis by auto
qed
qed
@@ -2667,12 +2667,12 @@
apply (unfold cp_eq_cpreced cpreced_def)
apply (rule Max_mono)
proof -
- from dependents_threads [OF vt, of th1] th1_in
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<subseteq>
+ from dependants_threads [OF vt, of th1] th1_in
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
(\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
next
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<noteq> {}" by simp
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
next
from finite_threads[OF vt]
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
@@ -2691,14 +2691,14 @@
have cp_eq_p: "cp s tm = preced tm s"
proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
fix y
- assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm)"
+ assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
show "y \<le> preced tm s"
proof -
{ fix y'
- assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependents (wq s) tm)"
+ assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
- from hy' dependents_threads[OF vt, of tm]
+ from hy' dependants_threads[OF vt, of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
from finite_threads[OF vt]
@@ -2707,11 +2707,11 @@
} with hy show ?thesis by auto
qed
next
- from dependents_threads[OF vt, of tm] finite_threads[OF vt]
- show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm))"
+ from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+ show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
by (auto intro:finite_subset)
next
- show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm)"
+ show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
by simp
qed
moreover have "Max (cp s ` readys s) = cp s tm"
@@ -2731,11 +2731,11 @@
from finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<noteq> {}"
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
by simp
next
- from dependents_threads[OF vt, of th1] th1_readys
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)
+ from dependants_threads[OF vt, of th1] th1_readys
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
\<subseteq> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed