--- a/Graphs.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/Graphs.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -7,49 +7,55 @@
   shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+"
 using assms by (metis rtrancl_eq_or_trancl) 
 
+(* NOT NEEDED : FIXME *)
 lemma trancl_split: 
   "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
 by (induct rule:trancl_induct, auto)
 
-lemma unique_minus:
-  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
-  and xy: "(x, y) \<in> r"
-  and xz: "(x, z) \<in> r^+"
-  and neq: "y \<noteq> z"
-  shows "(y, z) \<in> r^+"
-by (metis converse_tranclE neq unique xy xz)
+
+section {* Single_Valuedness *}
+
+lemma single_valued_Collect:
+  assumes "single_valuedP r"
+  and "inj f"
+  shows "single_valued {(f x, g y) | x y. r x y}"
+using assms
+unfolding single_valued_def inj_on_def
+apply(auto)
+done
 
-lemma unique_base:
-  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
-  and xy: "(x, y) \<in> r"
-  and xz: "(x, z) \<in> r^+"
-  and neq_yz: "y \<noteq> z"
-  shows "(y, z) \<in> r^+"
-by (metis neq_yz unique unique_minus xy xz)
+lemma single_valued_union:
+  assumes "single_valued r" "single_valued q"
+  and "Domain r \<inter> Domain q = {}"
+  shows "single_valued (r \<union> q)"
+using assms
+unfolding single_valued_def
+by auto
 
-lemma unique_chain_star:
-  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
-  and xy: "(x, y) \<in> r^*"
-  and xz: "(x, z) \<in> r^*"
-  shows "(y, z) \<in> r^* \<or> (z, y) \<in> r^*"
-thm single_valued_confluent single_valued_def unique xy xz
-by (metis single_valued_confluent single_valued_def unique xy xz)
+lemma single_valuedP_update:
+  assumes "single_valuedP r"
+  shows "single_valuedP (r(x := y))"
+using assms
+oops
 
-lemma unique_chain:
-  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
+lemma single_valued_confluent2:
+  assumes unique: "single_valued r"
   and xy: "(x, y) \<in> r^+"
   and xz: "(x, z) \<in> r^+"
   and neq_yz: "y \<noteq> z"
   shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"
 proof -
-  have xy_star: "(x, y) \<in> r^*"
-  and  xz_star: "(x, z) \<in> r^*" using xy xz by simp_all
-  from unique_chain_star[OF unique xy_star xz_star]
+  have "(x, y) \<in> r^*" "(x, z) \<in> r^*" using xy xz by simp_all
+  with single_valued_confluent[OF unique]
   have "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" by auto
   with neq_yz
-  show ?thesis by(auto)
+  show "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" by simp
 qed
 
+lemmas unique_chain = single_valued_confluent2
+
+
+
 definition funof :: "[('a * 'b)set, 'a] => 'b" where
    "funof r == (\<lambda>x. THE y. (x, y) \<in> r)"
 
@@ -64,8 +70,7 @@
      "[|r `` {x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" 
 by (force simp add: funof_eq)
  
-lemma single_valuedP_update:
-  shows "single_valuedP r \<Longrightarrow> single_valuedP (r(x := y))"
-oops
+
+
 
 end
\ No newline at end of file

--- a/Journal/Paper.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/Journal/Paper.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -152,9 +152,12 @@
   \cite[Section 2.3.1]{book} which specifies for a process that 
   inherited a higher priority and exits a critical section ``{\it it resumes 
   the priority it had at the point of entry into the critical section}''.
+  The same error can also be found in the more recent textbook 
+  \cite[Page 119]{Laplante11} which states ``{\it when [the task] exits the critical 
+  section that caused the block, it reverts to the priority it had when 
+  it entered that section}''.
    
-  While \cite{book} and
-  \cite{Sha90} are the only formal publications we have 
+  While \cite{Laplante11,book,Sha90} are the only formal publications we have 
   found that describe the incorrect behaviour, not all, but many
   informal\footnote{informal as in ``found on the Web''} 
   descriptions of PIP overlook the possibility that another
@@ -1564,7 +1567,7 @@
   points out an error in a paper about Preemption 
   Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
   invaluable to us in order to be confident about the correctness of our reasoning 
-  (no case can be overlooked).   
+  (for example no corner case can be overlooked).   
   The most closely related work to ours is the formal verification in
   PVS of the Priority Ceiling Protocol done by Dutertre
   \cite{dutertre99b}---another solution to the Priority Inversion

--- a/Journal/document/root.bib	Tue Jun 03 15:00:12 2014 +0100
+++ b/Journal/document/root.bib	Mon Jun 09 16:01:28 2014 +0100
@@ -1,5 +1,13 @@
 
 
+@Book{Laplante11,
+  author = 	 {P.~A.~Laplante and S.~J.~Ovaska},
+  title = 	 {Real-Time Systems Design and Analysis: Tools for the Practitioner},
+  publisher = 	 {Wiley-IEEE Press},
+  year = 	 {2011},
+  edition = 	 {4th}
+}
+
 @TechReport{Xv6,
   author =    {R.~Cox and F.~Kaashoek and R.~Morris},
   title =        {{X}v6: {A} {S}imple, {U}nix-like {T}eaching {O}perating {S}ystem},

--- a/PrioG.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/PrioG.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -2269,6 +2269,20 @@
 qed
 
 
+lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+apply(subgoal_tac "finite (runing s)")
+prefer 2
+apply (metis finite_nat_set_iff_bounded lessI runing_unique)
+apply(case_tac "Suc (Suc 0) \<le> card (runing s)")
+apply(subst (asm) card_le_Suc_iff)
+apply(simp)
+apply(auto)[1]
+apply (metis insertCI runing_unique)
+apply(auto) 
+done
+  
+
+
 lemma create_pre:
   assumes stp: "step s e"
   and not_in: "th \<notin> threads s"

--- a/Test.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/Test.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -74,6 +74,20 @@
              [] => [] 
           |  (_ # qs) => SOME q. distinct q \<and> set q = set qs"
 
+lemma [simp]: 
+  "(SOME q. distinct q \<and> q = []) = []"
+by auto
+
+lemma [simp]: 
+  "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
+apply(auto)
+apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
+by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
+
+abbreviation
+  "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
+
+
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
   "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" 
@@ -127,8 +141,6 @@
 definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
   where "holding s th \<equiv> {cs . holds2 s th cs}"
 
-abbreviation
-  "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
 
 lemma exists_distinct:
   obtains ys where "distinct ys" "set ys = set xs"
@@ -169,12 +181,63 @@
   unfolding readys_def
   by auto
 
+lemma wq_threads: 
+  assumes vt: "vt s"
+  and h: "th \<in> set (wq s cs)"
+  shows "th \<in> threads s"
+using assms
+apply(induct)
+apply(simp add: wq_def)
+apply(erule step.cases)
+apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def)
+apply(simp add: waits_def)
+apply(auto simp add: waits_def split: if_splits)[1]
+apply(auto split: if_splits)
+apply(simp only: waits_def)
+by (metis insert_iff set_simps(2))
+
+
+
+lemma Domain_RAG_threads:
+  assumes vt: "vt s"
+  and in_dom: "(Th th) \<in> Domain (RAG2 s)"
+  shows "th \<in> threads s"
+proof -
+  from in_dom obtain n where "(Th th, n) \<in> RAG2 s" by auto
+  then obtain cs where "n = Cs cs" "(Th th, Cs cs) \<in> RAG2 s"  
+    unfolding RAG2_def RAG_def by auto
+  then have "th \<in> set (wq s cs)"
+    unfolding wq_def RAG_def RAG2_def waits_def by auto
+  with wq_threads [OF vt] show ?thesis .
+qed
+
+lemma dependants_threads:
+  assumes vt: "vt s"
+  shows "dependants2 s th \<subseteq> threads s"
+proof
+  fix th1 
+  assume "th1 \<in> dependants2 s th"
+  then have h: "(Th th1, Th th) \<in> (RAG2 s)\<^sup>+"
+    unfolding dependants2_def dependants_def RAG2_def by simp
+  then have "Th th1 \<in> Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto
+  then have "Th th1 \<in> Domain (RAG2 s)" using trancl_domain by simp
+  then show "th1 \<in> threads s" using vt by (rule_tac Domain_RAG_threads)
+qed
+
+lemma finite_threads:
+  assumes vt: "vt s"
+  shows "finite (threads s)"
+using vt by (induct) (auto elim: step.cases)
+
+
+section {* Distinctness of @{const wq} *}
+
 lemma wq_distinct_step: 
   assumes "step s e" "distinct (wq s cs)" 
   shows "distinct (wq (e # s) cs)"
 using assms
 unfolding wq_def
-apply(induct)
+apply(erule_tac step.cases)
 apply(auto simp add: RAG2_def RAG_def Let_def)[1]
 apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)
 apply(auto split: list.split)
@@ -191,72 +254,8 @@
 apply(simp add: wq_distinct_step)
 done
 
-lemma RAG_set_unchanged[simp]: 
-  shows "RAG2 (Set th prio # s) = RAG2 s"
-unfolding RAG2_def
-by (simp add: Let_def)
 
-lemma RAG_create_unchanged[simp]: 
-  "RAG2 (Create th prio # s) = RAG2 s"
-unfolding RAG2_def
-by (simp add: Let_def)
-
-lemma RAG_exit_unchanged[simp]: 
-  shows "RAG2 (Exit th # s) = RAG2 s"
-unfolding RAG2_def
-by (simp add: Let_def)
-
-lemma RAG_p1:
-  assumes "wq s cs = []"
-  shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}"
-using assms
-unfolding  RAG2_def RAG_def wq_def Let_def waits_def holds_def
-by (auto simp add: Let_def)
-
-
-lemma RAG_p2:
-  assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []"
-  shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}"
-using assms
-unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
-by (auto simp add: Let_def)
-
-lemma [simp]: "(SOME q. distinct q \<and> q = []) = []"
-by auto
-
-lemma [simp]: "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
-apply auto
-apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
-by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
-
-lemma RAG_v1:
-assumes vt: "wq s cs = [th]"
-shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}"
-using assms
-unfolding RAG2_def RAG_def waits_def holds_def wq_def
-by (auto simp add: Let_def)
-
-lemma RAG_v2:
-assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []"
-shows "RAG2 (V th cs # s) \<subseteq>
-  RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
-unfolding RAG2_def RAG_def waits_def holds_def
-using assms wq_distinct[OF vt(1), of"cs"]
-by (auto simp add: Let_def wq_def)
-
-(*
-lemma single_valued_waits2:
-  assumes "vt s"
-  shows "single_valuedP (waits2 s)"
-using assms
-apply(induct)
-apply(simp add: waits2_def waits_def)
-apply(erule step.cases)
-apply(auto simp add: Let_def waits2_def)
-unfolding single_valued_def waits2_def waits_def
-apply(auto)
-*)
-
+section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *}
 
 lemma waits2_unique:
   assumes "vt s"
@@ -274,34 +273,85 @@
 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
 
+lemma single_valued_waits2:
+  assumes "vt s"
+  shows "single_valuedP (waits2 s)"
+using assms
+unfolding single_valued_def
+by (metis Collect_splitD fst_eqD sndI waits2_unique)
+
 lemma single_valued_holds2:
   assumes "vt s"
   shows "single_valuedP (\<lambda>cs th. holds2 s th cs)"
 unfolding single_valued_def holds2_def holds_def by simp
 
-
-lemma holds2_unique: 
-  assumes "holds2 s th1 cs"
-  and      "holds2 s th2 cs"
-  shows "th1 = th2"
-using assms
-unfolding holds2_def holds_def by auto
-
-lemma single_valued_waits2:
-  assumes "vt s"
-  shows "single_valuedP (waits2 s)"
-by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique)
-
-
-(* was unique_RAG2 *)
 lemma single_valued_RAG2:
   assumes "vt s"
   shows "single_valued (RAG2 s)"
 using single_valued_waits2[OF assms] single_valued_holds2[OF assms] 
-unfolding RAG2_def RAG_def 
-unfolding single_valued_def
-unfolding holds2_def waits2_def 
-by auto 
+unfolding RAG2_def RAG_def
+apply(rule_tac single_valued_union)
+unfolding holds2_def[symmetric] waits2_def[symmetric]
+apply(rule single_valued_Collect)
+apply(simp)
+apply(simp add: inj_on_def)
+apply(rule single_valued_Collect)
+apply(simp)
+apply(simp add: inj_on_def)
+apply(auto)
+done
+
+
+section {* Properties of @{const RAG2} under events *}
+
+lemma RAG_Set [simp]: 
+  shows "RAG2 (Set th prio # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_Create [simp]: 
+  "RAG2 (Create th prio # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_Exit [simp]: 
+  shows "RAG2 (Exit th # s) = RAG2 s"
+unfolding RAG2_def
+by (simp add: Let_def)
+
+lemma RAG_P1:
+  assumes "wq s cs = []"
+  shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}"
+using assms
+unfolding  RAG2_def RAG_def wq_def Let_def waits_def holds_def
+by (auto simp add: Let_def)
+
+lemma RAG_P2:
+  assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []"
+  shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}"
+using assms
+unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
+by (auto simp add: Let_def)
+
+
+lemma RAG_V1:
+assumes vt: "wq s cs = [th]"
+shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}"
+using assms
+unfolding RAG2_def RAG_def waits_def holds_def wq_def
+by (auto simp add: Let_def)
+
+lemma RAG_V2:
+assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []"
+shows "RAG2 (V th cs # s) \<subseteq>
+  RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
+unfolding RAG2_def RAG_def waits_def holds_def
+using assms wq_distinct[OF vt(1), of"cs"]
+by (auto simp add: Let_def wq_def)
+
+
+
+section {* Acyclicity of @{const RAG2} *}
 
 lemma acyclic_RAG_step: 
   assumes vt: "vt s"
@@ -321,14 +371,14 @@
       with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
     qed
     with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
-    then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF wq_empty] 
+    then have "acyclic (RAG2 (P th cs # s))" using RAG_P1[OF wq_empty] 
       by (rule acyclic_subset)
   }
   moreover
   { assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
     from ac ds
     have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp
-    then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds wq_not_empty] 
+    then have "acyclic (RAG2 (P th cs # s))" using RAG_P2[OF ds wq_not_empty] 
       by (rule acyclic_subset)
   }
   ultimately show "acyclic (RAG2 (P th cs # s))" by metis
@@ -343,7 +393,7 @@
   -- "case no thread present in the waiting queue to take over"
   { assume "wts = []" 
     with eq_wq have "wq s cs = [th]" by simp
-    then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1)
+    then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_V1)
     moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset)
     ultimately 
     have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
@@ -352,11 +402,13 @@
   -- "at least one thread present to take over"
   { def nth \<equiv> "next_to_run wts"
     assume wq_not_empty: "wts \<noteq> []" 
-    have waits2_cs: "waits2 s nth cs" 
+    have "waits2 s nth cs" 
       using eq_wq wq_not_empty wq_distinct
       unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto
+    then have cs_in_RAG: "(Th nth, Cs cs) \<in> RAG2 s" 
+      unfolding RAG2_def RAG_def waits2_def by auto
     have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" 
-      unfolding nth_def using  vt wq_not_empty eq_wq by (rule_tac RAG_v2) (auto)
+      unfolding nth_def using  vt wq_not_empty eq_wq by (rule_tac RAG_V2) (auto)
     moreover 
     have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)})" 
     proof -
@@ -368,14 +420,9 @@
         then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})"
           by (metis converse_tranclE)
         then have "(Th nth, z) \<in> RAG2 s" by simp
-        then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
-          unfolding RAG2_def RAG_def by auto
-        moreover 
-        have "waits2 s nth cs'" 
-          using b(2) unfolding RAG2_def RAG_def waits2_def by simp
-        ultimately have "cs = cs'" 
-          by (rule_tac waits2_unique[OF vt waits2_cs])
-        then show "False" using a b(1) by simp
+        then have "z = Cs cs" using cs_in_RAG single_valued_RAG2[OF vt]
+          by (simp add: single_valued_def)
+        then show "False" using a by simp
       qed
       ultimately 
       show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp
@@ -397,11 +444,11 @@
 apply(auto)
 apply(case_tac "wq sa cs = []")
 apply(rule finite_subset)
-apply(rule RAG_p1)
+apply(rule RAG_P1)
 apply(simp)
 apply(simp)
 apply(rule finite_subset)
-apply(rule RAG_p2)
+apply(rule RAG_P2)
 apply(simp)
 apply(simp)
 apply(simp)
@@ -409,11 +456,11 @@
 apply(erule exE)
 apply(case_tac "wts = []")
 apply(rule finite_subset)
-apply(rule RAG_v1)
+apply(rule RAG_V1)
 apply(simp)
 apply(simp)
 apply(rule finite_subset)
-apply(rule RAG_v2)
+apply(rule RAG_V2)
 apply(simp)
 apply(simp)
 apply(simp)
@@ -423,20 +470,39 @@
 apply(auto simp add: holds2_def holds_def wq_def)
 done
 
-lemma wq_threads: 
+
+
+lemma dchain_unique:
   assumes vt: "vt s"
-  and h: "th \<in> set (wq s cs)"
-  shows "th \<in> threads s"
-using assms
-apply(induct)
-apply(simp add: wq_def)
-apply(erule step.cases)
-apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def)
-apply(simp add: waits_def)
-apply(auto simp add: waits_def split: if_splits)[1]
-apply(auto split: if_splits)
-apply(simp only: waits_def)
-by (metis insert_iff set_simps(2))
+  and th1_d: "(n, Th th1) \<in> (RAG2 s)^+"
+  and th1_r: "th1 \<in> readys s"
+  and th2_d: "(n, Th th2) \<in> (RAG2 s)^+"
+  and th2_r: "th2 \<in> readys s"
+  shows "th1 = th2"
+proof(rule ccontr)
+  assume neq: "th1 \<noteq> th2"
+   with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d
+  have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" by auto
+  moreover
+  { assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+"      
+    then obtain n where dd: "(Th th1, n) \<in> RAG2 s" by (metis converse_tranclE)
+    then obtain cs where eq_n: "n = Cs cs"
+      unfolding RAG2_def RAG_def by (case_tac n) (auto)
+    from dd eq_n have "th1 \<notin> readys s"
+      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)
+    with th1_r have "False" by auto
+  }
+  moreover
+  { assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+"
+    then obtain n where dd: "(Th th2, n) \<in> RAG2 s" by (metis converse_tranclE)
+    then obtain cs where eq_n: "n = Cs cs"
+      unfolding RAG2_def RAG_def by (case_tac n) (auto)
+    from dd eq_n have "th2 \<notin> readys s"
+      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)
+    with th2_r have "False" by auto
+  }
+  ultimately show "False" by metis
+qed
 
 lemma max_cpreceds_readys_threads:
   assumes vt: "vt s"
@@ -452,46 +518,51 @@
 defer
 oops
 
-
+lemma readys_Exit:
+  shows "readys (Exit th # s) \<subseteq> readys s"
+by (auto simp add: readys_def waits2_def Let_def)
 
+lemma readys_Create:
+  shows "readys (Create th prio # s) \<subseteq> {th} \<union> readys s"
+by (auto simp add: readys_def waits2_def Let_def)
 
+lemma readys_Set:
+  shows "readys (Set th prio # s) \<subseteq> readys s"
+by (auto simp add: readys_def waits2_def Let_def)
 
 
-lemma dchain_unique:
-  assumes vt: "vt s"
-  and th1_d: "(n, Th th1) \<in> (RAG2 s)^+"
-  and th1_r: "th1 \<in> readys s"
-  and th2_d: "(n, Th th2) \<in> (RAG2 s)^+"
-  and th2_r: "th2 \<in> readys s"
-  shows "th1 = th2"
-proof(rule ccontr)
-  assume neq: "th1 \<noteq> th2"
-  hence "Th th1 \<noteq> Th th2" by simp
-  from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt]
-  have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" 
-    unfolding single_valued_def by auto
-  then show "False"
-  proof
-    assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+"      
-    from trancl_split [OF this]
-    obtain n where dd: "(Th th1, n) \<in> RAG2 s" by auto
-    then obtain cs where eq_n: "n = Cs cs"
-      unfolding RAG2_def RAG_def by (case_tac n) (auto)
-    from dd eq_n have "th1 \<notin> readys s"
-      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)
-    with th1_r show ?thesis by auto
-  next
-    assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+"
-    from trancl_split [OF this]
-    obtain n where dd: "(Th th2, n) \<in> RAG2 s" by auto
-    then obtain cs where eq_n: "n = Cs cs"
-      unfolding RAG2_def RAG_def by (case_tac n) (auto)
-    from dd eq_n have "th2 \<notin> readys s"
-      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)
-    with th2_r show ?thesis by auto
-  qed
-qed
+lemma readys_P:
+  shows "readys (P th cs # s) \<subseteq> readys s"
+apply(auto simp add: readys_def waits2_def Let_def)
+apply(simp add: waits_def)
+apply(case_tac "csa = cs")
+apply(simp)
+apply(drule_tac x="cs" in spec)
+apply(simp)
+apply (metis hd_append2 in_set_insert insert_Nil list.sel(1))
+apply(drule_tac x="csa" in spec)
+apply(simp)
+done
 
+lemma readys_V:
+  shows "readys (V th cs # s) \<subseteq> readys s \<union> set (wq s cs)"
+apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def)
+done
+
+lemma 
+  assumes "vt s"
+  shows "card (runing s) \<le> 1"
+proof (rule ccontr)
+  assume "\<not> card (runing s) \<le> 1"
+  then have "2 \<le> card (runing s)" by auto
+  moreover 
+  have "finite (runing s)" sorry
+  ultimately obtain th1 th2 where "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s"
+    by (auto simp add: numerals card_le_Suc_iff) (blast)
+
+  show "False"
+apply(simp)
+oops  
 
 
 end
\ No newline at end of file

Binary file journal.pdf has changed