
diff -r fb3f52fe99d1 -r 785c0f6b8184 PIPBasics.thy
--- a/PIPBasics.thy	Tue Aug 16 11:49:37 2016 +0100
+++ b/PIPBasics.thy	Wed Aug 24 16:13:20 2016 +0200
@@ -920,6 +920,8 @@
   "dependants s th =  {th'. th \<in> ancestors (tG s) th'}"
   by (unfold dependants_alt_tG ancestors_def, simp)
 
+
+
 section {* Locales used to investigate the execution of PIP *}
 
 text {* 
@@ -3459,6 +3461,36 @@
   qed
 qed
 
+lemma root_readys:
+  assumes "th \<in> readys s"
+  shows "root (tRAG s) (Th th)"
+proof -
+  { assume "\<not> root (tRAG s) (Th th)"
+    then obtain n' where "(Th th, n') \<in> (tRAG s)^+"
+      unfolding root_def ancestors_def by auto
+    then obtain cs where "(Th th, Cs cs) \<in> RAG s"
+      unfolding tRAG_alt_def using tranclD by fastforce 
+    then have "th \<notin> readys s" 
+      unfolding readys_def using in_RAG_E by blast 
+    with assms have False by simp
+  } then show "root (tRAG s) (Th th)" by auto
+qed
+
+lemma root_readys_tG:
+  assumes "th \<in> readys s"
+  shows "root (tG s) th"
+proof -
+  { assume "\<not> root (tG s) th"
+    then obtain th' where "(th, th') \<in> (tG s)^+"
+      unfolding root_def ancestors_def by auto
+    then have "(Th th, Th th') \<in> (tRAG s)^+" 
+      using trancl_tG_tRAG by simp
+    with root_readys assms 
+    have False 
+      unfolding root_def ancestors_def by auto
+  } then show "root (tG s) th" by auto
+qed  
+
 lemma readys_indep:
   assumes "th1 \<in> readys s"
   and "th2 \<in> readys s"
@@ -3509,191 +3541,67 @@
   The following two lemmas shows there is at most one running thread 
   in the system.
 *}
+
+
 lemma running_unique:
   assumes running_1: "th1 \<in> running s"
   and running_2: "th2 \<in> running s"
   shows "th1 = th2"
 proof -
-  -- {* According to lemma @{thm thread_chain}, 
-        each living threads is chained to a thread in its subtree, and this
-        target thread holds the highest precedence of the subtree.
-
-        The chains for @{term th1} and @{term th2} are established 
-        first in the following in @{text "h1"} and @{text "h2"}:
-     *}
+  -- {* 
+
+  According to lemma @{thm thread_chain}, each live thread is chained to a
+  thread in its subtree, who holds the highest precedence of the subtree.
+
+  The chains for @{term th1} and @{term th2} are established first in the
+  following in @{text "chain1"} and @{text "chain2"}. These chains start
+  with the threads @{text "th1'"} and @{text "th2'"} respectively. *}
+  
   have "th1 \<in> threads s" using assms
     by (unfold running_def readys_def, auto)
-  from thread_chain[OF this]
+  with thread_chain
   obtain th1' where 
-      h1: "th1' \<in> subtree (tG s) th1" 
+      chain1: "th1' \<in> subtree (tG s) th1" 
           "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
           "th1' \<in> threads s"
       by auto
   have "th2 \<in> threads s" using assms
     by (unfold running_def readys_def, auto)
-  from thread_chain[OF this]
+  with thread_chain
   obtain th2' where 
-      h2: "th2' \<in> subtree (tG s) th2" 
+      chain2: "th2' \<in> subtree (tG s) th2" 
           "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
           "th2' \<in> threads s"
       by auto
-  -- {* It can be proved that the chained thread for @{term th1} and @{term th2}
-        must be equal:
+  -- {* From these two chains we can be prove that the threads 
+        @{term th1} and @{term th2} must be equal. For this we first
+        show that the starting points of the chains are equal.
      *}
   have eq_th': "th1' = th2'"
   proof -
-    have "the_preced s th1' = the_preced s th2'" 
-    proof -
-      from running_1 and running_2 have "cp s th1 = cp s th2"
-          unfolding running_def by auto
-      from this[unfolded cp_alt_def2]
-      have eq_max: "Max (the_preced s ` subtree (tG s) th1) = 
-                    Max (the_preced s ` subtree (tG s) th2)" .
-      with h1(2) h2(2)
-      show ?thesis by metis
-    qed
-    from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)]
-    show ?thesis .
-  qed
-  -- {* From this, it can be derived that the two sub-trees 
-        rooted by @{term th1} and @{term th2} must overlap: *}
-  have overlapping: "th1' \<in> subtree (tG s) th1 \<inter> subtree (tG s) th2" 
-     using  eq_th' h1(1) h2(1) by auto
-  -- {* However, this would be in contradiction with the fact
-        that two independent sub-trees can not overlap, 
-        if @{term "th1 \<noteq> th2"} (therefore, each roots an independent sub-trees).
-        Therefore, @{term th1} and @{term th2} must be equal.
-     *}
-  { assume neq: "th1 \<noteq> th2"
-    -- {* According to @{thm readys_indep_tG}, two different threads 
-          in ready queue must be independent with each other: *}
-    have "indep (tG s) th1 th2"
-      by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def)
-    -- {* Therefore, according to lemma @{thm subtree_disjoint},
-          the two sub-trees rooted by them can not overlap: 
-    *}
-    from subtree_disjoint[OF this]
-    have "subtree (tG s) th1 \<inter> subtree (tG s) th2 = {}" .
-    -- {* In contradiction with @{thm overlapping}: *}
-    with overlapping have False by auto
-  } thus ?thesis by auto
-qed
-
-text {*
-  The following two lemmas shows there is at most one running thread 
-  in the system.
-*}
-lemma running_unique_old:
-  assumes running_1: "th1 \<in> running s"
-  and running_2: "th2 \<in> running s"
-  shows "th1 = th2"
-proof -
-  from running_1 and running_2 have "cp s th1 = cp s th2"
-    unfolding running_def by auto
-  from this[unfolded cp_alt_def]
-  have eq_max: 
-    "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
-     Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})" 
-        (is "Max ?L = Max ?R") .
-  have "Max ?L \<in> ?L"
-  proof(rule Max_in)
-    show "finite ?L" by (simp add: finite_subtree_threads) 
-  next
-    show "?L \<noteq> {}" using subtree_def by fastforce 
-  qed
-  then obtain th1' where 
-    h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L"
-    by auto
-  have "Max ?R \<in> ?R"
-  proof(rule Max_in)
-    show "finite ?R" by (simp add: finite_subtree_threads)
-  next
-    show "?R \<noteq> {}" using subtree_def by fastforce 
+    -- {* from @{text th1} and @{text th2} running, we know their 
+          cp-value is the same *}
+    from running_1 and running_2 have "cp s th1 = cp s th2"
+      unfolding running_def by auto
+    -- {* that means the preced of @{text th1'} and @{text th2'} 
+          must be the same *}
+    then 
+    have eq_max: "Max (the_preced s ` subtree (tG s) th1) = 
+                  Max (the_preced s ` subtree (tG s) th2)" 
+      unfolding cp_alt_def2 .
+    with chain1(2) chain2(2)
+    have "the_preced s th1' = the_preced s th2'" by simp
+    -- {* since the precedences are the same, we can conclude
+          that  @{text th1'} and @{text th2'} are the same *}
+    with preced_unique chain1(3) chain2(3)
+    show "th1' = th2'" unfolding the_preced_def by auto
   qed
-  then obtain th2' where 
-    h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R"
-    by auto
-  have "th1' = th2'"
-  proof(rule preced_unique)
-    from h_1(1)
-    show "th1' \<in> threads s"
-    proof(cases rule:subtreeE)
-      case 1
-      hence "th1' = th1" by simp
-      with running_1 show ?thesis by (auto simp:running_def readys_def)
-    next
-      case 2
-      from this(2)
-      have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
-      from tranclD[OF this]
-      have "(Th th1') \<in> Domain (RAG s)" by auto
-      from dm_RAG_threads[OF this] show ?thesis .
-    qed
-  next
-    from h_2(1)
-    show "th2' \<in> threads s"
-    proof(cases rule:subtreeE)
-      case 1
-      hence "th2' = th2" by simp
-      with running_2 show ?thesis by (auto simp:running_def readys_def)
-    next
-      case 2
-      from this(2)
-      have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
-      from tranclD[OF this]
-      have "(Th th2') \<in> Domain (RAG s)" by auto
-      from dm_RAG_threads[OF this] show ?thesis .
-    qed
-  next
-    have "the_preced s th1' = the_preced s th2'" 
-     using eq_max h_1(2) h_2(2) by metis
-    thus "preced th1' s = preced th2' s" by (simp add:the_preced_def)
-  qed
-  from h_1(1)[unfolded this]
-  have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def)
-  from h_2(1)[unfolded this]
-  have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def)
-  from star_rpath[OF star1] obtain xs1 
-    where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)"
-    by auto
-  from star_rpath[OF star2] obtain xs2 
-    where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)"
-    by auto
-  from rp1 rp2
-  show ?thesis
-  proof(cases)
-    case (less_1 xs')
-    moreover have "xs' = []"
-    proof(rule ccontr)
-      assume otherwise: "xs' \<noteq> []"
-      from rpath_plus[OF less_1(3) this]
-      have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
-      from tranclD[OF this]
-      obtain cs where "waiting s th1 cs"
-        by (unfold s_RAG_def, fold s_waiting_abv, auto)
-      with running_1 show False
-        by (unfold running_def readys_def, auto)
-    qed
-    ultimately have "xs2 = xs1" by simp
-    from rpath_dest_eq[OF rp1 rp2[unfolded this]]
-    show ?thesis by simp
-  next
-    case (less_2 xs')
-    moreover have "xs' = []"
-    proof(rule ccontr)
-      assume otherwise: "xs' \<noteq> []"
-      from rpath_plus[OF less_2(3) this]
-      have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
-      from tranclD[OF this]
-      obtain cs where "waiting s th2 cs"
-        by (unfold s_RAG_def, fold s_waiting_abv, auto)
-      with running_2 show False
-        by (unfold running_def readys_def, auto)
-    qed
-    ultimately have "xs2 = xs1" by simp
-    from rpath_dest_eq[OF rp1 rp2[unfolded this]]
-    show ?thesis by simp
-  qed
+  moreover
+  have "root (tG s) th1" "root (tG s) th2" using assms
+    using assms root_readys_tG
+    unfolding running_def by auto
+  ultimately show "th1 = th2" using root_unique chain1(1) chain2(1)
+     by fastforce
 qed
 
 lemma card_running: 




