--- a/Journal/Paper.thy	Wed Jan 13 13:20:45 2016 +0000
+++ b/Journal/Paper.thy	Wed Jan 13 14:20:58 2016 +0000
@@ -890,10 +890,10 @@
   programs that contain for every looking request also a corresponding
   unlocking request for a resource. Second, we would need to specify a
   kind of global clock that tracks the time how long a thread locks a
-  resource. But this seems difficult, because how do we conveninet
+  resource. But this seems difficult, because how do we conveniently
   distinguish between a thread that ``just'' lock a resource for a
   very long time and one that locks it forever.  Therefore we decided
-  to leave it out this property and let the programmer assume the
+  to leave out this property and let the programmer assume the
   responsibility to program threads in such a benign manner (in
   addition to causing no circularity in the RAG). In this detail, we
   do not make any progress in comparison with the work by Sha et al.
@@ -936,7 +936,7 @@
 
   THENTHEN
 
-  @{thm [source] runing_inversion_4} @{thm runing_inversion_4}
+  (here) %@ {thm [source] runing_inversion_4} @  {thm runing_inversion_4}
 
   which explains what the @{term "th'"} looks like. Now, we have found the 
   @{term "th'"} which blocks @{term th}, we need to know more about it.
@@ -1166,6 +1166,20 @@
   %if every such thread can release all its resources in finite duration, then after finite
   %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
   %then.
+
+  NOTE: about bounds in sha et al and ours:
+
+  There are low priority threads, 
+  which do not hold any resources, 
+  such thread will not block th. 
+  Their Theorem 3 does not exclude such threads.
+
+  There are resources, which are not held by any low prioirty threads,
+  such resources can not cause blockage of th neither. And similiary, 
+  theorem 6 does not exlude them.
+
+  Our one bound excudle them by using a different formaulation. "
+
   *}
 (*<*)
 end

--- a/Moment.thy	Wed Jan 13 13:20:45 2016 +0000
+++ b/Moment.thy	Wed Jan 13 14:20:58 2016 +0000
@@ -5,36 +5,18 @@
 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where "moment n s = rev (take n (rev s))"
 
-value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
-
 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where "restm n s = rev (drop n (rev s))"
 
-value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
-
-definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where "from_to i j s = take (j - i) (drop i s)"
+value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
+value "moment 2 [5, 4, 3, 2, 1, 0::int]"
 
-definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where "down_to j i s = rev (from_to i j (rev s))"
-
-value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]"
-value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]"
-
-value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ 
-       from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]"
-
+value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
 
 lemma moment_restm_s: "(restm n s) @ (moment n s) = s"
   unfolding restm_def moment_def
 by (metis append_take_drop_id rev_append rev_rev_ident)
 
-declare drop.simps [simp del] 
-
-lemma length_take_le: 
-  "n \<le> length s \<Longrightarrow> length (take n s) = n"
-by (metis length_take min.absorb2)
-
 lemma length_moment_le:
   assumes le_k: "k \<le> length s"
   shows "length (moment k s) = k"
@@ -45,29 +27,12 @@
   shows "length (moment k s) = (length s)"
 using assms unfolding moment_def by simp
 
-lemma length_take: 
-  "(length (take n s) = length s) \<or> (length (take n s) = n)"
-by (metis length_take min_def)
-
-lemma take_conc: 
-  assumes le_mn: "m \<le> n"
-  shows "take m s = take m (take n  s)"
-using assms by (metis min.absorb1 take_take) 
-
-(*
-value "down_to 2 0 [5, 4, 3, 2, 1, 0]"
-value "moment 2 [5, 4, 3, 2, 1, 0]"
-*)
-
-lemma from_to_take: "from_to 0 k s = take k s"
-by (simp add:from_to_def drop.simps)
-
 lemma moment_app [simp]:
   assumes ile: "i \<le> length s"
-  shows "moment i (s'@s) = moment i s"
+  shows "moment i (s' @ s) = moment i s"
 using assms unfolding moment_def by simp
 
-lemma moment_eq [simp]: "moment (length s) (s'@s) = s"
+lemma moment_eq [simp]: "moment (length s) (s' @ s) = s"
   unfolding moment_def by simp
 
 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"
@@ -172,7 +137,7 @@
 qed
 
 lemma p_split: 
-  "\<And> s Q. \<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> 
        (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
 proof -
   fix s Q
@@ -183,20 +148,6 @@
     by auto
 qed
 
-(*
-value "from_to 2 5 [0, 1, 2, 3, 4]"
-value "drop 2  [0, 1, 2, 3, 4]"
-*)
-
-(*
-lemma down_to_moment: "down_to k 0 s = moment k s"
-proof -
-  have "rev (from_to 0 k (rev s)) = rev (take k (rev s))" 
-    using from_to_take by metis
-  thus ?thesis by (simp add:down_to_def moment_def)
-qed
-*)
-
 lemma moment_plus_split:
   shows "moment (m + i) s = moment m (restm i s) @ moment i s"
 unfolding moment_def restm_def
@@ -213,32 +164,6 @@
   with moment_app show ?thesis by auto
 qed
 
-lemma length_down_to_in: 
-  assumes le_ij: "i \<le> j"
-    and le_js: "j \<le> length s"
-  shows "length (down_to j i s) = j - i"
-using assms
-unfolding down_to_def from_to_def
-by (simp)
-
-lemma moment_head: 
-  assumes le_it: "Suc i \<le> length t"
-  obtains e where "moment (Suc i) t = e#moment i t"
-proof -
-  have "i \<le> Suc i" by simp
-  from length_down_to_in [OF this le_it]
-  have a: "length (down_to (Suc i) i t) = 1" by auto
-  then obtain e where "down_to (Suc i) i t = [e]"
-    apply (cases "(down_to (Suc i) i t)") by auto
-  moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
-    unfolding down_to_def from_to_def rev_append[symmetric]
-    apply(simp del: rev_append)
-    by (metis One_nat_def Suc_eq_plus1_left add.commute take_add)
-  ultimately have eq_me: "moment (Suc i) t = e # (moment i t)"
-    by(simp add: moment_def down_to_def from_to_def)
-  from that [OF this] show ?thesis .
-qed
-
 lemma moment_plus: 
   "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)"
 proof(induct s, simp+)
@@ -276,3 +201,4 @@
 qed
 
 end
+