diff -r 2056d9f481e2 -r ed938e2246b9 CpsG.thy
--- a/CpsG.thy	Thu Jan 28 16:36:46 2016 +0800
+++ b/CpsG.thy	Thu Jan 28 21:14:17 2016 +0800
@@ -84,6 +84,30 @@
   finally show ?thesis by simp
 qed
 
+lemma birth_time_lt:  
+  assumes "s \<noteq> []"
+  shows "last_set th s < length s"
+  using assms
+proof(induct s)
+  case (Cons a s)
+  show ?case
+  proof(cases "s \<noteq> []")
+    case False
+    thus ?thesis
+      by (cases a, auto)
+  next
+    case True
+    show ?thesis using Cons(1)[OF True]
+      by (cases a, auto)
+  qed
+qed simp
+
+lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
+  by (induct s, auto)
+
+lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
+  by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
+
 lemma eq_RAG: 
   "RAG (wq s) = RAG s"
   by (unfold cs_RAG_def s_RAG_def, auto)
@@ -2245,10 +2269,6 @@
   ultimately show ?thesis by auto
 qed
 
-lemma max_cp_eq_the_preced:
-  shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
-  using max_cp_eq using the_preced_def by presburger 
-
 lemma wf_RAG_converse: 
   shows "wf ((RAG s)^-1)"
 proof(rule finite_acyclic_wf_converse)
@@ -4444,5 +4464,85 @@
   shows "th1 = th2"
 using assms by (unfold next_th_def, auto)
 
+context valid_trace
+begin
+
+thm th_chain_to_ready
+
+find_theorems subtree Th RAG
+
+lemma threads_alt_def:
+  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+    (is "?L = ?R")
+proof -
+  { fix th1
+    assume "th1 \<in> ?L"
+    from th_chain_to_ready[OF this]
+    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .
+    hence "th1 \<in> ?R" by (auto simp:subtree_def)
+  } moreover 
+  { fix th'
+    assume "th' \<in> ?R"
+    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"
+      by auto
+    from this(2)
+    have "th' \<in> ?L" 
+    proof(cases rule:subtreeE)
+      case 1
+      with h(1) show ?thesis by (auto simp:readys_def)
+    next
+      case 2
+      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]
+      have "Th th' \<in> Domain (RAG s)" by auto
+      from dm_RAG_threads[OF this]
+      show ?thesis .
+    qed
+  } ultimately show ?thesis by auto
+qed
+
+lemma finite_readys [simp]: "finite (readys s)"
+  using finite_threads readys_threads rev_finite_subset by blast
+
+text {* (* ccc *) \noindent
+  Since the current precedence of the threads in ready queue will always be boosted,
+  there must be one inside it has the maximum precedence of the whole system. 
+*}
+lemma max_cp_readys_threads:
+  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
+proof(cases "readys s = {}")
+  case False
+  have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
+  also have "... = 
+    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" 
+         by (unfold threads_alt_def, simp)
+  also have "... = 
+    Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
+          by (unfold image_UN, simp)
+  also have "... = 
+    Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" 
+  proof(rule Max_UNION)
+    show "\<forall>M\<in>(\<lambda>x. the_preced s ` 
+                    {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
+                        using finite_subtree_threads by auto
+  qed (auto simp:False subtree_def)
+  also have "... =  
+    Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" 
+      by (unfold image_comp, simp)
+  also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
+  proof -
+    have "(?f ` ?A) = (?g ` ?A)"
+    proof(rule f_image_eq)
+      fix th1 
+      assume "th1 \<in> ?A"
+      thus "?f th1 = ?g th1"
+        by (unfold cp_alt_def, simp)
+    qed
+    thus ?thesis by simp
+  qed
+  finally show ?thesis by simp
+qed (auto simp:threads_alt_def)
+
 end
 
+end
+