1275 the particular environment in which it operates. In this particular case, |
1280 the particular environment in which it operates. In this particular case, |
1276 we regard the @{term t} as the environment of thread @{term th}. |
1281 we regard the @{term t} as the environment of thread @{term th}. |
1277 *} |
1282 *} |
1278 assumes finite_span: |
1283 assumes finite_span: |
1279 "th' \<in> blockers \<Longrightarrow> |
1284 "th' \<in> blockers \<Longrightarrow> |
1280 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> |
1285 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> |
1281 length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')" |
1286 \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)" |
1282 -- {* The following @{text BC} is bound of @{term Create}-operations *} |
1287 |
|
1288 -- {* |
|
1289 The difference between this @{text finite_span} and the former one is to allow the number |
|
1290 of action steps to change with execution paths (i.e. different value of @{term "t'@s"}}). |
|
1291 The @{term span} is a upper bound on these step numbers. |
|
1292 *} |
|
1293 |
1283 fixes BC |
1294 fixes BC |
1284 -- {* |
1295 -- {* |
1285 The following assumption requires the number of @{term Create}-operations is |
1296 The following assumption requires the number of @{term Create}-operations is |
1286 less or equal to @{term BC} regardless of any particular extension of @{term t}. |
1297 less or equal to @{term BC} regardless of any particular extension of @{term t}. |
1287 |
1298 |
1314 text {* |
1325 text {* |
1315 The following @{term span}-function gives the upper bound of |
1326 The following @{term span}-function gives the upper bound of |
1316 operations take by each particular blocker. |
1327 operations take by each particular blocker. |
1317 *} |
1328 *} |
1318 definition "span th' = (SOME span. |
1329 definition "span th' = (SOME span. |
1319 \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow> |
1330 \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> |
1320 length (actions_of {th'} t') = span \<longrightarrow> detached (t' @ s) th')" |
1331 \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)" |
1321 |
1332 |
1322 text {* |
1333 text {* |
1323 The following lemmas shows the correctness of @{term span}, i.e. |
1334 The following lemmas shows the correctness of @{term span}, i.e. |
1324 the number of operations of taken by @{term th'} is given by |
1335 the number of operations of taken by @{term th'} is given by |
1325 @{term "span th"}. |
1336 @{term "span th"}. |
1331 lemma le_span: |
1342 lemma le_span: |
1332 assumes "th' \<in> blockers" |
1343 assumes "th' \<in> blockers" |
1333 shows "length (actions_of {th'} t) \<le> span th'" |
1344 shows "length (actions_of {th'} t) \<le> span th'" |
1334 proof - |
1345 proof - |
1335 from finite_span[OF assms(1)] obtain span' |
1346 from finite_span[OF assms(1)] obtain span' |
1336 where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow> |
1347 where span': "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> |
1337 length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'") |
1348 \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span'" (is "?P span'") |
1338 by auto |
1349 by auto |
1339 have "length (actions_of {th'} t) \<le> (SOME span. ?P span)" |
1350 have "length (actions_of {th'} t) \<le> (SOME span. ?P span)" |
1340 proof(rule someI2[where a = span']) |
1351 proof(rule someI2[where a = span']) |
1341 fix span |
1352 fix span |
1342 assume fs: "?P span" |
1353 assume fs: "?P span" |
1343 show "length (actions_of {th'} t) \<le> span" |
1354 show "length (actions_of {th'} t) \<le> span" |
1344 proof(induct rule:ind) |
1355 proof(induct rule:ind) |
1345 case h: (Cons e t) |
1356 case h: (Cons e t) |
1346 interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp |
1357 interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp |
1347 show ?case |
1358 show ?case |
1348 proof(cases "length (actions_of {th'} t) < span") |
1359 proof(cases "detached (t@s) th'") |
1349 case True |
1360 case True |
1350 thus ?thesis by (simp add:actions_of_def) |
|
1351 next |
|
1352 case False |
|
1353 have "actor e \<noteq> th'" |
1361 have "actor e \<noteq> th'" |
1354 proof |
1362 proof |
1355 assume otherwise: "actor e = th'" |
1363 assume otherwise: "actor e = th'" |
1356 from ve'.blockers_no_create [OF assms _ this] |
1364 from ve'.blockers_no_create [OF assms _ this] |
1357 have "\<not> isCreate e" by auto |
1365 have "\<not> isCreate e" by auto |
1358 from PIP_actorE[OF h(2) otherwise this] |
1366 from PIP_actorE[OF h(2) otherwise this] |
1359 have "th' \<in> running (t @ s)" . |
1367 have "th' \<in> running (t @ s)" . |
1360 moreover have "th' \<notin> running (t @ s)" |
1368 moreover have "th' \<notin> running (t @ s)" |
1361 proof - |
1369 proof - |
1362 from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp |
1370 from extend_highest_gen.detached_not_running[OF h(3) True] assms |
1363 from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" . |
|
1364 from extend_highest_gen.detached_not_running[OF h(3) this] assms |
|
1365 show ?thesis by (auto simp:blockers_def) |
1371 show ?thesis by (auto simp:blockers_def) |
1366 qed |
1372 qed |
1367 ultimately show False by simp |
1373 ultimately show False by simp |
1368 qed |
1374 qed |
1369 with h show ?thesis by (auto simp:actions_of_def) |
1375 with h show ?thesis by (auto simp:actions_of_def) |
|
1376 next |
|
1377 case False |
|
1378 from fs[rule_format, OF h(3) this] and actions_of_len_cons |
|
1379 show ?thesis by (meson discrete order.trans) |
1370 qed |
1380 qed |
1371 qed (simp add: actions_of_def) |
1381 qed (simp add: actions_of_def) |
1372 next |
1382 next |
1373 from span' |
1383 from span' |
1374 show "?P span'" . |
1384 show "?P span'" . |