pip: comparison CpsG.thy

equal deleted inserted replaced

-:8f026b608378
+:e861aff29655
 lemma children_def2:
 "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"
+lemma children_dependants: "children s th \<subseteq> dependants (wq s) th"
-by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
+by (unfold children_def child_def cs_dependants_def, auto simp:eq_depend)
 lemma child_unique:
 assumes vt: "vt s"
 and ch1: "(Th th, Th th1) \<in> child s"
 and ch2: "(Th th, Th th2) \<in> child s"
 proof(rule unique_chain [OF _ dp1 dp2 neq])
 from unique_depend[OF vt]
 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 dp1: "th3 \<in> dependants s th1"
-and dp2: "th3 \<in> dependents s th2"
+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
 proof
 assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "
 fixes s th
 assumes vt: "vt s"
 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)) =
+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> dependents (wq s) th))) ` children 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 =
+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> 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 "?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]
+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> dependents (wq s) th') |th'. th' \<in> children s 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']
+from finite_threads[OF vt] and dependants_threads[OF vt, of th']
-show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)
+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}
+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) ` dependents (wq 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
+and x_in: "x \<in> ?f ` ({th'} \<union> dependants (wq s) th')" by auto
-hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto
+hence "x = ?f th' \<or> x \<in> (?f ` dependants (wq s) th')" by auto
-thus "x \<in> ?f ` dependents (wq s) th"
+thus "x \<in> ?f ` dependants (wq s) th"
 proof
 assume "x = preced th' s"
-with th'_in and children_dependents
+with th'_in and children_dependants
-show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto
+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"
+ultimately show " x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
-by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)
+by (unfold cs_dependants_def children_def child_def, auto simp:eq_depend)
 qed
 qed
 next
-show "?f ` dependents (wq s) th
+show "?f ` dependants (wq s) th
-\<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children 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"
+have "th' \<in> dependants (wq s) th3"
-by (auto simp:cs_dependents_def eq_depend)
+by (auto simp:cs_dependants_def eq_depend)
 with eq_x th3_in show ?thesis by auto
 qed
 qed
 qed
 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)) =
+have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
-Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp
+Max ({?f th} \<union> ?f ` (dependants (wq s) th))" by simp
-also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"
+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]
+from finite_threads[OF vt] and dependants_threads[OF vt, of th]
-show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)
+show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th)" by (auto simp:finite_subset)
 next
-assume "dependents (wq s) th = {}"
+assume "dependants (wq s) th = {}"
-with False and children_dependents show False by auto
+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]
+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) ` dependents (wq 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
 assume "children s th = {}"
 with False show False by auto
 thus ?thesis by simp
 qed
 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"
+assume "th' \<in> dependants (wq s) th"
-hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)
+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
 qed
 ultimately show ?thesis by auto
 by (unfold s_def depend_set_unchanged, auto)
 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"
+have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
 moreover {
 fix th1
-assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
-hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+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')) =
+} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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')) =
+thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+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"
 apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def)
 by (fold wq_def, blast)
 lemma eq_cp:
 fixes th'
 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]
+from no_dependants[OF neq_th]
-show "th \<notin> dependents s th'" .
+show "th \<notin> dependants s th'" .
 qed
 lemma eq_up:
 fixes th' th''
-assumes dp1: "th \<in> dependents s th'"
+assumes dp1: "th \<in> dependants s th'"
-and dp2: "th' \<in> dependents 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''
 have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
 (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
 assume y_ch: "(y, Th th'') \<in> child s"
 and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
 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
 show "cp s th'' = cp s' th''"
 apply (subst cp_rec[OF vt_s])
 assume eq_th1: "th1 = th"
 with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
 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"
+assume h:"th \<in> dependants s th1"
-from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
-from dependents_child_unique[OF vt_s _ _ h this]
+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
 from eq_cp_pre[OF neq_th1 this]
 show ?thesis .
 show "th'' \<noteq> th"
 proof
 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
 qed
 moreover {
 case False
 have neq_th1: "th1 \<noteq> th"
 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"
+assume "th \<in> dependants s th1"
-from dependents_child_unique[OF vt_s _ _ this dp1]
+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
 qed
 qed
 ultimately show ?thesis by auto
 qed
 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''
 have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
 (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
 assume eq_th1: "th1 = th"
 with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
 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"
+assume h:"th \<in> dependants s th1"
-from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
-from dependents_child_unique[OF vt_s _ _ h this]
+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
 from eq_cp_pre[OF neq_th1 this]
 show ?thesis .
 show "th'' \<noteq> th"
 proof
 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
 qed
 moreover {
 next
 case False
 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"
+assume "th \<in> dependants s th1"
-hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+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)
 qed
 qed
 proof -
 from step_depend_v[OF vt_s[unfolded s_def], folded s_def]
 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)
 fix y
 assume "(y, Th th'') \<in> depend s"
 with ztp'
 show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
 qed
 }
 from this[OF dp]
-show "x \<in> dependents (wq s') th''"
+show "x \<in> dependants (wq s') th''"
-by (auto simp:cs_dependents_def eq_depend)
+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)
 fix y
 assume "(y, Th th'') \<in> depend s'"
 with ztp'
 show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
 qed
 }
 from this[OF dp]
-show "x \<in> dependents (wq s) th''"
+show "x \<in> dependants (wq s) th''"
-by (auto simp:cs_dependents_def eq_depend)
+by (auto simp:cs_dependants_def eq_depend)
 qed
 lemma cp_kept:
 fixes th''
 assumes neq1: "th'' \<noteq> th"
 and neq2: "th'' \<noteq> th'"
 shows "cp s th'' = cp s' th''"
 proof -
-from dependents_kept[OF neq1 neq2]
+from dependants_kept[OF neq1 neq2]
-have "dependents (wq s) th'' = dependents (wq s') th''" .
+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'')) =
+ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) =
-((\<lambda>th. preced th s') ` ({th''} \<union> dependents (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)
 qed
 lemma eq_cp:
 fixes 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"
+have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-apply (unfold cs_dependents_def, unfold eq_depend)
+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>+}"
 by simp
 with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
 show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
 by simp
 qed
 moreover {
 fix th1
-assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
-hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+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')) =
+} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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')) =
+thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
 qed
 end
 locale step_P_cps =
 lemma eq_cp:
 fixes 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"
+have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-apply (unfold cs_dependents_def, unfold eq_depend)
+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>+}"
 by auto
 with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
 show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
 by simp
 qed
 moreover {
 fix th1
-assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
-hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+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')) =
+} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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')) =
+thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
 qed
 end
 context step_P_cps_ne
 shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
 by (insert eq_child_left[OF nd] eq_child_right, auto)
 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 -
 have nd': "(Th th, Th th') \<notin> (child s)^+"
 proof
 assume "(Th th, Th th') \<in> (child s)\<^sup>+"
 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'"
+fix x assume " x \<in> dependants (wq s) th'"
-thus "x \<in> dependents (wq s') th'"
+thus "x \<in> dependants (wq s') th'"
-apply (auto simp:cs_dependents_def eq_depend)
+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
 with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp
 with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
 show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
 qed
 next
-fix x assume "x \<in> dependents (wq s') th'"
+fix x assume "x \<in> dependants (wq s') th'"
-thus "x \<in> dependents (wq s) th'"
+thus "x \<in> dependants (wq s) th'"
-apply (auto simp:cs_dependents_def eq_depend)
+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]]]
 have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp
 with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp
 show "(Th x, Th th') \<in> (depend s)\<^sup>+" by simp
 qed
 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')) =
+} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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')) =
+thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+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'"
+assumes dp1: "th \<in> dependants s th'"
-and dp2: "th' \<in> dependents 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''
 have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
 assume y_ch: "(y, Th th'') \<in> child s"
 and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
 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
 show "cp s th'' = cp s' th''"
 apply (subst cp_rec[OF vt_s])
 assume eq_th1: "th1 = th"
 with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
 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"
+assume h:"th \<in> dependants s th1"
-from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
-from dependents_child_unique[OF vt_s _ _ h this]
+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
 from eq_cp[OF this]
 show ?thesis .
 apply (fold s_def, auto simp:depend_s)
 proof -
 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>+"
 by (auto simp:s_depend_def)
 have eq_cs: "cs1 = cs"
 case False
 have neq_th1: "th1 \<noteq> th"
 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"
+assume "th \<in> dependants s th1"
-from dependents_child_unique[OF vt_s _ _ this dp1]
+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
 qed
 qed
 apply (fold s_def, auto simp:depend_s)
 proof -
 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>+"
 by (auto simp:s_depend_def)
 have eq_cs: "cs1 = cs"
 fixes th'
 assumes neq_th: "th' \<noteq> th"
 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'"
+assume "th \<in> dependants s th'"
-hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+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
 with dm_depend_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
 have in_th: "th \<in> threads s'" by auto
 proof(cases)
 assume "th \<notin> threads s'"
 with in_th show ?thesis by simp
 qed
 qed
-have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
 moreover {
 fix th1
-assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
-hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+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')) =
+} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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')) =
+thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+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
 proof(cases)
 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
 have False by (auto simp:holdents_test)
 } 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
 locale step_exit_cps =
 fixes th'
 assumes neq_th: "th' \<noteq> th"
 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'"
+assume "th \<in> dependants s th'"
-hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+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'"
 by (auto simp:s_depend_def)
 from step_back_step[OF vt_s[unfolded s_def]]
 with bk show ?thesis
 apply (unfold runing_def readys_def s_waiting_def s_depend_def)
 by (auto simp:cs_waiting_def wq_def)
 qed
 qed
-have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
 moreover {
 fix th1
-assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
-hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+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')) =
+} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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')) =
+thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
 qed
 end
 end

changeset 32	e861aff29655
parent 0	110247f9d47e
child 33	9b9f2117561f