diff -r 8f026b608378 -r e861aff29655 CpsG.thy
--- 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