--- a/ExtGG.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/ExtGG.thy Tue May 06 14:36:40 2014 +0100
@@ -2,21 +2,21 @@
imports PrioG
begin
-lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> birthtime th s < length s"
+lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
apply (induct s, simp)
proof -
fix a s
- assume ih: "s \<noteq> [] \<Longrightarrow> birthtime th s < length s"
+ assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
and eq_as: "a # s \<noteq> []"
- show "birthtime th (a # s) < length (a # s)"
+ show "last_set th (a # s) < length (a # s)"
proof(cases "s \<noteq> []")
case False
from False show ?thesis
- by (cases a, auto simp:birthtime.simps)
+ by (cases a, auto simp:last_set.simps)
next
case True
from ih [OF True] show ?thesis
- by (cases a, auto simp:birthtime.simps)
+ by (cases a, auto simp:last_set.simps)
qed
qed
@@ -46,18 +46,18 @@
proof -
from highest and max_cp_eq[OF vt_s]
have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp
- have sbs: "({th} \<union> dependents (wq s) th) \<subseteq> threads s"
+ have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s"
proof -
- from threads_s and dependents_threads[OF vt_s, of th]
+ from threads_s and dependants_threads[OF vt_s, of th]
show ?thesis by auto
qed
show ?thesis
proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
- show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)" by simp
+ show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp
next
fix y
- assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)"
- then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependents (wq s) th)"
+ assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)"
+ then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)"
and eq_y: "y = preced th1 s" by auto
show "y \<le> preced th s"
proof(unfold is_max, rule Max_ge)
@@ -69,7 +69,7 @@
qed
next
from sbs and finite_threads[OF vt_s]
- show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))"
+ show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))"
by (auto intro:finite_subset)
qed
qed
@@ -469,7 +469,7 @@
by (unfold cp_eq_cpreced, simp)
also have "\<dots> = ?R"
proof(unfold cpreced_def)
- show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependents (wq (t @ s)) th)) =
+ show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependants (wq (t @ s)) th)) =
Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
(is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)")
proof(cases "?A = {}")
@@ -479,7 +479,7 @@
proof(rule Max_insert)
show "finite (?f ` ?A)"
proof -
- from dependents_threads[OF vt_t]
+ from dependants_threads[OF vt_t]
have "?A \<subseteq> threads (t@s)" .
moreover from finite_threads[OF vt_t] have "finite \<dots>" .
ultimately show ?thesis
@@ -497,7 +497,7 @@
next
show "?f ` ?A \<subseteq> ?f ` ?B"
proof -
- have "?A \<subseteq> ?B" by (rule dependents_threads[OF vt_t])
+ have "?A \<subseteq> ?B" by (rule dependants_threads[OF vt_t])
thus ?thesis by auto
qed
next
@@ -566,8 +566,8 @@
finally have h: "cp (t @ s) th' = preced th (t @ s)" .
show False
proof -
- have "dependents (wq (t @ s)) th' = {}"
- by (rule count_eq_dependents [OF vt_t eq_pv])
+ have "dependants (wq (t @ s)) th' = {}"
+ by (rule count_eq_dependants [OF vt_t eq_pv])
moreover have "preced th' (t @ s) \<noteq> preced th (t @ s)"
proof
assume "preced th' (t @ s) = preced th (t @ s)"
@@ -983,13 +983,13 @@
proof -
have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"
proof -
- have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')) =
+ have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')) =
preced th (t@s)"
proof(rule Max_eqI)
fix y
- assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')"
+ assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
then obtain th1 where
- h1: "th1 = th' \<or> th1 \<in> dependents (wq (t @ s)) th'"
+ h1: "th1 = th' \<or> th1 \<in> dependants (wq (t @ s)) th'"
and eq_y: "y = preced th1 (t@s)" by auto
show "y \<le> preced th (t @ s)"
proof -
@@ -1003,8 +1003,8 @@
assume "th1 = th'"
with th'_in show ?thesis by (simp add:readys_def)
next
- assume "th1 \<in> dependents (wq (t @ s)) th'"
- with dependents_threads [OF vt_t]
+ assume "th1 \<in> dependants (wq (t @ s)) th'"
+ with dependants_threads [OF vt_t]
show "th1 \<in> threads (t @ s)" by auto
qed
with eq_y show " y \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" by simp
@@ -1015,15 +1015,15 @@
ultimately show ?thesis by auto
qed
next
- from finite_threads[OF vt_t] dependents_threads [OF vt_t, of th']
- show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th'))"
+ from finite_threads[OF vt_t] dependants_threads [OF vt_t, of th']
+ show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th'))"
by (auto intro:finite_subset)
next
from dp
- have "th \<in> dependents (wq (t @ s)) th'"
- by (unfold cs_dependents_def, auto simp:eq_depend)
+ have "th \<in> dependants (wq (t @ s)) th'"
+ by (unfold cs_dependants_def, auto simp:eq_depend)
thus "preced th (t @ s) \<in>
- (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')"
+ (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
by auto
qed
moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))"