--- a/CpsG.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/CpsG.thy Tue May 06 14:36:40 2014 +0100
@@ -255,8 +255,8 @@
"children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
unfolding child_def children_def by simp
-lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
- by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
+lemma children_dependants: "children s th \<subseteq> dependants (wq s) th"
+ by (unfold children_def child_def cs_dependants_def, auto simp:eq_depend)
lemma child_unique:
assumes vt: "vt s"
@@ -446,20 +446,20 @@
show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
qed
-lemma dependents_child_unique:
+lemma dependants_child_unique:
fixes s th th1 th2 th3
assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
- and dp1: "th3 \<in> dependents s th1"
- and dp2: "th3 \<in> dependents s th2"
+ and dp1: "th3 \<in> dependants s th1"
+ and dp2: "th3 \<in> dependants s th2"
shows "th1 = th2"
proof -
{ assume neq: "th1 \<noteq> th2"
from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+"
- by (simp add:s_dependents_def eq_depend)
+ by (simp add:s_dependants_def eq_depend)
from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+"
- by (simp add:s_dependents_def eq_depend)
+ by (simp add:s_dependants_def eq_depend)
from unique_depend_p[OF vt dp1 dp2] and neq
have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto
hence False
@@ -479,90 +479,90 @@
shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
proof(unfold cp_eq_cpreced_f cpreced_def)
let ?f = "(\<lambda>th. preced th s)"
- show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"
+ show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
+ Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th)"
proof(cases " children s th = {}")
case False
- have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th =
- {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+ have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th =
+ {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
(is "?L = ?R")
by auto
also have "\<dots> =
- Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+ Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
(is "_ = Max ` ?C")
by auto
finally have "Max ?L = Max (Max ` ?C)" by auto
also have "\<dots> = Max (\<Union> ?C)"
proof(rule Max_Union[symmetric])
- from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]
- show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ from children_dependants[of s th] finite_threads[OF vt] and dependants_threads[OF vt, of th]
+ show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
by (auto simp:finite_subset)
next
from False
- show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
+ show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
by simp
next
- show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
+ show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
finite A \<and> A \<noteq> {}"
apply (auto simp:finite_subset)
proof -
fix th'
- from finite_threads[OF vt] and dependents_threads[OF vt, of th']
- show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)
+ from finite_threads[OF vt] and dependants_threads[OF vt, of th']
+ show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th')" by (auto simp:finite_subset)
qed
qed
- also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"
+ also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependants (wq s) th)"
(is "Max ?A = Max ?B")
proof -
have "?A = ?B"
proof
- show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}
- \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}
+ \<subseteq> (\<lambda>th. preced th s) ` dependants (wq s) th"
proof
fix x
- assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
then obtain th' where
th'_in: "th' \<in> children s th"
- and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto
- hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto
- thus "x \<in> ?f ` dependents (wq s) th"
+ and x_in: "x \<in> ?f ` ({th'} \<union> dependants (wq s) th')" by auto
+ hence "x = ?f th' \<or> x \<in> (?f ` dependants (wq s) th')" by auto
+ thus "x \<in> ?f ` dependants (wq s) th"
proof
assume "x = preced th' s"
- with th'_in and children_dependents
- show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto
+ with th'_in and children_dependants
+ show "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th" by auto
next
- assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'"
+ assume "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th'"
moreover note th'_in
- ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
- by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)
+ ultimately show " x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
+ by (unfold cs_dependants_def children_def child_def, auto simp:eq_depend)
qed
qed
next
- show "?f ` dependents (wq s) th
- \<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ show "?f ` dependants (wq s) th
+ \<subseteq> \<Union>{?f ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
proof
fix x
- assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
then obtain th' where
eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+"
- by (auto simp:cs_dependents_def eq_depend)
+ by (auto simp:cs_dependants_def eq_depend)
from depend_children[OF dp]
have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .
- thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
proof
assume "th' \<in> children s th"
with eq_x
- show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
by auto
next
assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"
then obtain th3 where th3_in: "th3 \<in> children s th"
and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto
- show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
proof -
from dp3
- have "th' \<in> dependents (wq s) th3"
- by (auto simp:cs_dependents_def eq_depend)
+ have "th' \<in> dependants (wq s) th3"
+ by (auto simp:cs_dependants_def eq_depend)
with eq_x th3_in show ?thesis by auto
qed
qed
@@ -570,34 +570,34 @@
qed
thus ?thesis by simp
qed
- finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)"
+ finally have "Max ((\<lambda>th. preced th s) ` dependants (wq s) th) = Max (?L)"
(is "?X = ?Y") by auto
- moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
+ moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
max (?f th) ?X"
proof -
- have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp
- also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"
+ have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
+ Max ({?f th} \<union> ?f ` (dependants (wq s) th))" by simp
+ also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependants (wq s) th)))"
proof(rule Max_Un, auto)
- from finite_threads[OF vt] and dependents_threads[OF vt, of th]
- show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)
+ from finite_threads[OF vt] and dependants_threads[OF vt, of th]
+ show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th)" by (auto simp:finite_subset)
next
- assume "dependents (wq s) th = {}"
- with False and children_dependents show False by auto
+ assume "dependants (wq s) th = {}"
+ with False and children_dependants show False by auto
qed
also have "\<dots> = max (?f th) ?X" by simp
finally show ?thesis .
qed
moreover have "Max ({preced th s} \<union>
- (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
+ (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th) =
max (?f th) ?Y"
proof -
have "Max ({preced th s} \<union>
- (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
+ (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th) =
max (Max {preced th s}) ?Y"
proof(rule Max_Un, auto)
- from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th]
- show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) `
+ from finite_threads[OF vt] dependants_threads[OF vt, of th] children_dependants [of s th]
+ show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependants (wq s) th))) `
children s th)"
by (auto simp:finite_subset)
next
@@ -609,11 +609,11 @@
ultimately show ?thesis by auto
next
case True
- moreover have "dependents (wq s) th = {}"
+ moreover have "dependants (wq s) th = {}"
proof -
{ fix th'
- assume "th' \<in> dependents (wq s) th"
- hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)
+ assume "th' \<in> dependants (wq s) th"
+ hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependants_def eq_depend)
from depend_children[OF this] and True
have "False" by auto
} thus ?thesis by auto
@@ -648,46 +648,46 @@
lemma eq_cp_pre:
fixes th'
assumes neq_th: "th' \<noteq> th"
- and nd: "th \<notin> dependents s th'"
+ and nd: "th \<notin> dependants s th'"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with eq_preced[OF neq_th]
show "preced th1 s = preced th1 s'" by simp
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
-lemma no_dependents:
+lemma no_dependants:
assumes "th' \<noteq> th"
- shows "th \<notin> dependents s th'"
+ shows "th \<notin> dependants s th'"
proof
- assume h: "th \<in> dependents s th'"
+ assume h: "th \<in> dependants s th'"
from step_back_step [OF vt_s[unfolded s_def]]
have "step s' (Set th prio)" .
hence "th \<in> runing s'" by (cases, simp)
hence rd_th: "th \<in> readys s'"
by (simp add:readys_def runing_def)
from h have "(Th th, Th th') \<in> (depend s')\<^sup>+"
- by (unfold s_dependents_def, unfold eq_depend, unfold eq_dep, auto)
+ by (unfold s_dependants_def, unfold eq_depend, unfold eq_dep, auto)
from tranclD[OF this]
obtain z where "(Th th, z) \<in> depend s'" by auto
with rd_th show "False"
@@ -701,19 +701,19 @@
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
proof(rule eq_cp_pre [OF neq_th])
- from no_dependents[OF neq_th]
- show "th \<notin> dependents s th'" .
+ from no_dependants[OF neq_th]
+ show "th \<notin> dependants s th'" .
qed
lemma eq_up:
fixes th' th''
- assumes dp1: "th \<in> dependents s th'"
- and dp2: "th' \<in> dependents s th''"
+ assumes dp1: "th \<in> dependants s th'"
+ and dp2: "th' \<in> dependants s th''"
and eq_cps: "cp s th' = cp s' th'"
shows "cp s th'' = cp s' th''"
proof -
from dp2
- have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
from depend_child[OF vt_s this[unfolded eq_depend]]
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
moreover { fix n th''
@@ -726,7 +726,7 @@
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
moreover from child_depend_p[OF ch'] and eq_y
have "(Th th', Th thy) \<in> (depend s)^+" by simp
ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
@@ -761,11 +761,11 @@
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
- have "th \<notin> dependents s th1"
+ have "th \<notin> dependants s th1"
proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
+ assume h:"th \<in> dependants s th1"
+ from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+ from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
@@ -793,7 +793,7 @@
assume "th'' = th"
with dp1 dp'
have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def s_dependents_def eq_depend)
+ by (auto simp:child_def s_dependants_def eq_depend)
with wf_trancl[OF wf_depend[OF vt_s]]
show False by auto
qed
@@ -811,17 +811,17 @@
proof
assume eq_th1: "th1 = th"
with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from children_no_dep[OF vt_s _ _ this]
th1_in dp'
show False by (auto simp:children_def)
qed
thus ?thesis
proof(rule eq_cp_pre)
- show "th \<notin> dependents s th1"
+ show "th \<notin> dependants s th1"
proof
- assume "th \<in> dependents s th1"
- from dependents_child_unique[OF vt_s _ _ this dp1]
+ assume "th \<in> dependants s th1"
+ from dependants_child_unique[OF vt_s _ _ this dp1]
th1_in dp' have "th1 = th'"
by (auto simp:children_def)
with False show False by auto
@@ -843,12 +843,12 @@
lemma eq_up_self:
fixes th' th''
- assumes dp: "th \<in> dependents s th''"
+ assumes dp: "th \<in> dependants s th''"
and eq_cps: "cp s th = cp s' th"
shows "cp s th'' = cp s' th''"
proof -
from dp
- have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
from depend_child[OF vt_s this[unfolded eq_depend]]
have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
moreover { fix n th''
@@ -894,11 +894,11 @@
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
- have "th \<notin> dependents s th1"
+ have "th \<notin> dependants s th1"
proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
+ assume h:"th \<in> dependants s th1"
+ from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+ from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
@@ -926,7 +926,7 @@
assume "th'' = th"
with dp dp'
have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def s_dependents_def eq_depend)
+ by (auto simp:child_def s_dependants_def eq_depend)
with wf_trancl[OF wf_depend[OF vt_s]]
show False by auto
qed
@@ -943,10 +943,10 @@
assume neq_th1: "th1 \<noteq> th"
thus ?thesis
proof(rule eq_cp_pre)
- show "th \<notin> dependents s th1"
+ show "th \<notin> dependants s th1"
proof
- assume "th \<in> dependents s th1"
- hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ assume "th \<in> dependants s th1"
+ hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
from children_no_dep[OF vt_s _ _ this]
and th1_in dp' show False
by (auto simp:children_def)
@@ -1046,16 +1046,16 @@
and nt show ?thesis by (auto intro:next_th_unique)
qed
-lemma dependents_kept:
+lemma dependants_kept:
fixes th''
assumes neq1: "th'' \<noteq> th"
and neq2: "th'' \<noteq> th'"
- shows "dependents (wq s) th'' = dependents (wq s') th''"
+ shows "dependants (wq s) th'' = dependants (wq s') th''"
proof(auto)
fix x
- assume "x \<in> dependents (wq s) th''"
+ assume "x \<in> dependants (wq s) th''"
hence dp: "(Th x, Th th'') \<in> (depend s)^+"
- by (auto simp:cs_dependents_def eq_depend)
+ by (auto simp:cs_dependants_def eq_depend)
{ fix n
have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow> (n, Th th'') \<in> (depend s')^+"
proof(induct rule:converse_trancl_induct)
@@ -1120,13 +1120,13 @@
qed
}
from this[OF dp]
- show "x \<in> dependents (wq s') th''"
- by (auto simp:cs_dependents_def eq_depend)
+ show "x \<in> dependants (wq s') th''"
+ by (auto simp:cs_dependants_def eq_depend)
next
fix x
- assume "x \<in> dependents (wq s') th''"
+ assume "x \<in> dependants (wq s') th''"
hence dp: "(Th x, Th th'') \<in> (depend s')^+"
- by (auto simp:cs_dependents_def eq_depend)
+ by (auto simp:cs_dependants_def eq_depend)
{ fix n
have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow> (n, Th th'') \<in> (depend s)^+"
proof(induct rule:converse_trancl_induct)
@@ -1209,8 +1209,8 @@
qed
}
from this[OF dp]
- show "x \<in> dependents (wq s) th''"
- by (auto simp:cs_dependents_def eq_depend)
+ show "x \<in> dependants (wq s) th''"
+ by (auto simp:cs_dependants_def eq_depend)
qed
lemma cp_kept:
@@ -1219,18 +1219,18 @@
and neq2: "th'' \<noteq> th'"
shows "cp s th'' = cp s' th''"
proof -
- from dependents_kept[OF neq1 neq2]
- have "dependents (wq s) th'' = dependents (wq s') th''" .
+ from dependants_kept[OF neq1 neq2]
+ have "dependants (wq s) th'' = dependants (wq s') th''" .
moreover {
fix th1
- assume "th1 \<in> dependents (wq s) th''"
+ assume "th1 \<in> dependants (wq s) th''"
have "preced th1 s = preced th1 s'"
by (unfold s_def, auto simp:preced_def)
}
moreover have "preced th'' s = preced th'' s'"
by (unfold s_def, auto simp:preced_def)
- ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependents (wq s) th'')) =
- ((\<lambda>th. preced th s') ` ({th''} \<union> dependents (wq s') th''))"
+ ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) =
+ ((\<lambda>th. preced th s') ` ({th''} \<union> dependants (wq s') th''))"
by (auto simp:image_def)
thus ?thesis
by (unfold cp_eq_cpreced cpreced_def, simp)
@@ -1352,8 +1352,8 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- apply (unfold cs_dependents_def, unfold eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ apply (unfold cs_dependants_def, unfold eq_depend)
proof -
from eq_child
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
@@ -1364,21 +1364,21 @@
qed
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
@@ -1496,8 +1496,8 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- apply (unfold cs_dependents_def, unfold eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ apply (unfold cs_dependants_def, unfold eq_depend)
proof -
from eq_child
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
@@ -1508,21 +1508,21 @@
qed
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
@@ -1597,7 +1597,7 @@
lemma eq_cp:
fixes th'
- assumes nd: "th \<notin> dependents s th'"
+ assumes nd: "th \<notin> dependants s th'"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
@@ -1607,13 +1607,13 @@
with child_depend_eq[OF vt_s]
have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp
with nd show False
- by (simp add:s_dependents_def eq_depend)
+ by (simp add:s_dependants_def eq_depend)
qed
- have eq_dp: "dependents (wq s) th' = dependents (wq s') th'"
+ have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"
proof(auto)
- fix x assume " x \<in> dependents (wq s) th'"
- thus "x \<in> dependents (wq s') th'"
- apply (auto simp:cs_dependents_def eq_depend)
+ fix x assume " x \<in> dependants (wq s) th'"
+ thus "x \<in> dependants (wq s') th'"
+ apply (auto simp:cs_dependants_def eq_depend)
proof -
assume "(Th x, Th th') \<in> (depend s)\<^sup>+"
with child_depend_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
@@ -1622,9 +1622,9 @@
show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
qed
next
- fix x assume "x \<in> dependents (wq s') th'"
- thus "x \<in> dependents (wq s) th'"
- apply (auto simp:cs_dependents_def eq_depend)
+ fix x assume "x \<in> dependants (wq s') th'"
+ thus "x \<in> dependants (wq s) th'"
+ apply (auto simp:cs_dependants_def eq_depend)
proof -
assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
@@ -1636,22 +1636,22 @@
qed
moreover {
fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
lemma eq_up:
fixes th' th''
- assumes dp1: "th \<in> dependents s th'"
- and dp2: "th' \<in> dependents s th''"
+ assumes dp1: "th \<in> dependants s th'"
+ and dp2: "th' \<in> dependants s th''"
and eq_cps: "cp s th' = cp s' th'"
shows "cp s th'' = cp s' th''"
proof -
from dp2
- have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
from depend_child[OF vt_s this[unfolded eq_depend]]
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
moreover {
@@ -1665,7 +1665,7 @@
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
moreover from child_depend_p[OF ch'] and eq_y
have "(Th th', Th thy) \<in> (depend s)^+" by simp
ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
@@ -1690,11 +1690,11 @@
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
- have "th \<notin> dependents s th1"
+ have "th \<notin> dependants s th1"
proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
+ assume h:"th \<in> dependants s th1"
+ from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+ from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
@@ -1711,7 +1711,7 @@
assume "(Cs cs, Th th'') \<in> depend s'"
with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
from dp1 have "(Th th, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from converse_tranclE[OF this]
obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
@@ -1772,17 +1772,17 @@
proof
assume eq_th1: "th1 = th"
with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from children_no_dep[OF vt_s _ _ this]
th1_in dp'
show False by (auto simp:children_def)
qed
show ?thesis
proof(rule eq_cp)
- show "th \<notin> dependents s th1"
+ show "th \<notin> dependants s th1"
proof
- assume "th \<in> dependents s th1"
- from dependents_child_unique[OF vt_s _ _ this dp1]
+ assume "th \<in> dependants s th1"
+ from dependants_child_unique[OF vt_s _ _ this dp1]
th1_in dp' have "th1 = th'"
by (auto simp:children_def)
with False show False by auto
@@ -1799,7 +1799,7 @@
assume "(Cs cs, Th th'') \<in> depend s'"
with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
from dp1 have "(Th th, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from converse_tranclE[OF this]
obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
@@ -1863,10 +1863,10 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have nd: "th \<notin> dependents s th'"
+ have nd: "th \<notin> dependants s th'"
proof
- assume "th \<in> dependents s th'"
- hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+ assume "th \<in> dependants s th'"
+ hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependants_def eq_depend)
with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
from converse_tranclE[OF this]
obtain y where "(Th th, y) \<in> depend s'" by auto
@@ -1879,31 +1879,31 @@
with in_th show ?thesis by simp
qed
qed
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with neq_th
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
-lemma nil_dependents: "dependents s th = {}"
+lemma nil_dependants: "dependants s th = {}"
proof -
from step_back_step[OF vt_s[unfolded s_def]]
show ?thesis
@@ -1911,11 +1911,11 @@
assume "th \<notin> threads s'"
from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
have hdn: " holdents s' th = {}" .
- have "dependents s' th = {}"
+ have "dependants s' th = {}"
proof -
- { assume "dependents s' th \<noteq> {}"
+ { assume "dependants s' th \<noteq> {}"
then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from tranclE[OF this] obtain cs' where
"(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
with hdn
@@ -1923,13 +1923,13 @@
} thus ?thesis by auto
qed
thus ?thesis
- by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp)
+ by (unfold s_def s_dependants_def eq_depend depend_create_unchanged, simp)
qed
qed
lemma eq_cp_th: "cp s th = preced th s"
apply (unfold cp_eq_cpreced cpreced_def)
- by (insert nil_dependents, unfold s_dependents_def cs_dependents_def, auto)
+ by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)
end
@@ -1951,10 +1951,10 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have nd: "th \<notin> dependents s th'"
+ have nd: "th \<notin> dependants s th'"
proof
- assume "th \<in> dependents s th'"
- hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+ assume "th \<in> dependants s th'"
+ hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependants_def eq_depend)
with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
from converse_tranclE[OF this]
obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'"
@@ -1968,28 +1968,28 @@
by (auto simp:cs_waiting_def wq_def)
qed
qed
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with neq_th
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end