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