1238           1 + (length (actions_of blockers t) + length (filter (isCreate) t))"

  1238           1 + (length (actions_of blockers t) + length (filter (isCreate) t))"

  1239    (is "?L \<le> ?R")

  1239    (is "?L \<le> ?R")

  1240 proof - 

  1240 proof - 

  1241   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"

  1241   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"

  1242   from occs_le[of ?Q t] 

  1242   from occs_le[of ?Q t] 

  1243   have "?L \<le> (1 + length t) - occs ?Q t" by simp

  1244   have "?L \<le> (1 + length t) - occs ?Q t" by simp

  1244   also have "... \<le> ?R"

  1245   also have "... \<le> ?R"

  1245   proof -

  1246   proof -

  1246     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))

  1248     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))

  1247               \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")

  1249               \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")

  1248     proof -

  1250     proof -

  1250       also have "... \<le> ?R1" using actions_th_occs by simp

  1252       also have "... \<le> ?R1" using actions_th_occs by simp

  1251       finally show ?thesis .

  1253       finally show ?thesis .

  1252     qed            

  1254     qed            

  1253     thus ?thesis by simp

  1255     thus ?thesis by simp

  1254   qed

  1256   qed

  1278     the total number of operations take by any standalone thread (or process) 

  1280     the total number of operations take by any standalone thread (or process) 

  1279     is only determined by its own input, and should not be affected by 

  1281     is only determined by its own input, and should not be affected by 

  1280     the particular environment in which it operates. In this particular case,

  1282     the particular environment in which it operates. In this particular case,

  1281     we regard the @{term t} as the environment of thread @{term th}.

  1283     we regard the @{term t} as the environment of thread @{term th}.

  1282   *}

  1284   *}

  1284           "th' \<in> blockers \<Longrightarrow>

  1286           "th' \<in> blockers \<Longrightarrow>

  1285                  (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 

  1287                  (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 

  1286                                   \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"

  1288                                   \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"

  1287 

  1289 

  1288   -- {*

  1290   -- {*

  1427 *}

  1429 *}

  1428 theorem enough_actions_for_the_highest:

  1430 theorem enough_actions_for_the_highest:

  1429   "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"

  1431   "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"

  1430   using actions_split create_bc len_action_blockers by linarith

  1432   using actions_split create_bc len_action_blockers by linarith

  1431 

  1433 

  1432 end

  1436 end

  1433 

  1437 

  1434 

  1438 

  1435 

  1439 

  1436 

  1440