--- a/Correctness.thy	Tue Apr 11 03:03:33 2017 +0800
+++ b/Correctness.thy	Thu Apr 20 14:22:01 2017 +0100
@@ -1259,6 +1259,52 @@
 
 end
 
+fun postfixes where 
+  "postfixes [] = []" |
+  "postfixes (x#xs) = (xs)#postfixes xs" 
+
+definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)"
+
+definition "occs' Q tt = length (filter Q (postfixes tt))"
+
+lemma occs'_nil [simp]: "occs' Q [] = 0"
+        by (unfold occs'_def, simp)
+
+lemma occs'_cons [simp]: 
+  shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)"
+  using assms   
+  by (unfold occs'_def, simp)
+
+lemma occs_len': "occs' Q t + occs' (\<lambda>e. \<not> Q e) t = length t"
+  unfolding occs'_def
+  by (induct t, auto)
+
+lemma [simp]: "Q [] \<Longrightarrow> occs' Q [] + 1 = occs Q []"
+  by (unfold occs'_def, simp)
+
+lemma [simp]: "\<not> Q [] \<Longrightarrow> occs' Q [] = occs Q []"
+  by (unfold occs'_def, simp)
+
+lemma [simp]: "l \<noteq> [] \<Longrightarrow> Q l \<Longrightarrow> Suc (occs Q (tl l)) = occs Q l"
+  by (induct l, auto)
+
+lemma [simp]: "l \<noteq> [] \<Longrightarrow> \<not> Q l \<Longrightarrow> (occs Q (tl l)) = occs Q l"
+  by (induct l, auto)
+
+lemma "l \<noteq> [] \<Longrightarrow> occs' Q l = occs Q (tl l)"
+proof(unfold occs'_def, induct l)
+  case (Cons a l)
+  show ?case
+  proof(cases "l = []")
+    case False
+    from Cons(1)[OF this] have "length (filter Q (postfixes l)) = occs Q (tl l)" .
+    with False
+    show ?thesis by auto
+  qed simp
+qed auto
+
+
+
 text {*
   As explained before, lemma @{text bound_priority_inversion} alone does not
   ensure the correctness of PIP. For PIP to be correct, the number of blocking operations 

Binary file journal.pdf has changed