--- a/Correctness.thy	Mon Feb 20 13:08:04 2017 +0000
+++ b/Correctness.thy	Mon Feb 20 15:53:22 2017 +0000
@@ -2,6 +2,11 @@
 imports PIPBasics
 begin
 
+lemma actions_of_len_cons [iff]: 
+    "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1"
+      by  (unfold actions_of_def, simp)
+
+
 text {* 
   The following two auxiliary lemmas are used to reason about @{term Max}.
 *}
@@ -1277,9 +1282,15 @@
   *}
   assumes finite_span: 
           "th' \<in> blockers \<Longrightarrow>
-                 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
-                                length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')"
-  -- {* The following @{text BC} is bound of @{term Create}-operations *}
+                 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
+                                  \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"
+
+  -- {*
+    The difference between this @{text finite_span} and the former one is to allow the number
+    of action steps to change with execution paths (i.e. different value of @{term "t'@s"}}).
+    The @{term span} is a upper bound on these step numbers. 
+  *}
+
   fixes BC
   -- {* 
   The following assumption requires the number of @{term Create}-operations is 
@@ -1316,8 +1327,8 @@
   operations take by each particular blocker.
 *}
 definition "span th' = (SOME span.
-         \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
-              length (actions_of {th'} t') = span \<longrightarrow> detached (t' @ s) th')"
+         \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
+                  \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"
 
 text {*
   The following lemmas shows the correctness of @{term span}, i.e. 
@@ -1333,8 +1344,8 @@
   shows "length (actions_of {th'} t) \<le> span th'"
 proof -
   from finite_span[OF assms(1)] obtain span' 
-  where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
-                     length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'")
+  where span': "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
+                       \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span'" (is "?P span'")
                      by auto
   have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"
   proof(rule someI2[where a = span'])
@@ -1345,11 +1356,8 @@
       case h: (Cons e t)
         interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
       show ?case
-      proof(cases "length (actions_of {th'} t) < span")
+      proof(cases "detached (t@s) th'")
         case True
-        thus ?thesis by (simp add:actions_of_def)
-      next
-        case False
         have "actor e \<noteq> th'"
         proof
           assume otherwise: "actor e = th'"
@@ -1359,14 +1367,16 @@
           have "th' \<in> running (t @ s)" .
           moreover have "th' \<notin> running (t @ s)"
           proof -
-            from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
-            from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
-            from extend_highest_gen.detached_not_running[OF h(3) this] assms
+            from extend_highest_gen.detached_not_running[OF h(3) True] assms
             show ?thesis by (auto simp:blockers_def)
           qed
           ultimately show False by simp
         qed
         with h show ?thesis by (auto simp:actions_of_def)
+      next
+        case False
+        from fs[rule_format, OF h(3) this] and actions_of_len_cons
+        show ?thesis by (meson discrete order.trans) 
       qed
     qed (simp add: actions_of_def)
   next
@@ -1422,6 +1432,6 @@
 end
 
 
-unused_thms
+
 
 end