1257 finally show ?thesis . |
1257 finally show ?thesis . |
1258 qed |
1258 qed |
1259 |
1259 |
1260 end |
1260 end |
1261 |
1261 |
|
1262 fun postfixes where |
|
1263 "postfixes [] = []" | |
|
1264 "postfixes (x#xs) = (xs)#postfixes xs" |
|
1265 |
|
1266 definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)" |
|
1267 |
|
1268 definition "occs' Q tt = length (filter Q (postfixes tt))" |
|
1269 |
|
1270 lemma occs'_nil [simp]: "occs' Q [] = 0" |
|
1271 by (unfold occs'_def, simp) |
|
1272 |
|
1273 lemma occs'_cons [simp]: |
|
1274 shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)" |
|
1275 using assms |
|
1276 by (unfold occs'_def, simp) |
|
1277 |
|
1278 lemma occs_len': "occs' Q t + occs' (\<lambda>e. \<not> Q e) t = length t" |
|
1279 unfolding occs'_def |
|
1280 by (induct t, auto) |
|
1281 |
|
1282 lemma [simp]: "Q [] \<Longrightarrow> occs' Q [] + 1 = occs Q []" |
|
1283 by (unfold occs'_def, simp) |
|
1284 |
|
1285 lemma [simp]: "\<not> Q [] \<Longrightarrow> occs' Q [] = occs Q []" |
|
1286 by (unfold occs'_def, simp) |
|
1287 |
|
1288 lemma [simp]: "l \<noteq> [] \<Longrightarrow> Q l \<Longrightarrow> Suc (occs Q (tl l)) = occs Q l" |
|
1289 by (induct l, auto) |
|
1290 |
|
1291 lemma [simp]: "l \<noteq> [] \<Longrightarrow> \<not> Q l \<Longrightarrow> (occs Q (tl l)) = occs Q l" |
|
1292 by (induct l, auto) |
|
1293 |
|
1294 lemma "l \<noteq> [] \<Longrightarrow> occs' Q l = occs Q (tl l)" |
|
1295 proof(unfold occs'_def, induct l) |
|
1296 case (Cons a l) |
|
1297 show ?case |
|
1298 proof(cases "l = []") |
|
1299 case False |
|
1300 from Cons(1)[OF this] have "length (filter Q (postfixes l)) = occs Q (tl l)" . |
|
1301 with False |
|
1302 show ?thesis by auto |
|
1303 qed simp |
|
1304 qed auto |
|
1305 |
|
1306 |
|
1307 |
1262 text {* |
1308 text {* |
1263 As explained before, lemma @{text bound_priority_inversion} alone does not |
1309 As explained before, lemma @{text bound_priority_inversion} alone does not |
1264 ensure the correctness of PIP. For PIP to be correct, the number of blocking operations |
1310 ensure the correctness of PIP. For PIP to be correct, the number of blocking operations |
1265 (by {\em blocking operation}, we mean the @{term Create}-operations and |
1311 (by {\em blocking operation}, we mean the @{term Create}-operations and |
1266 operations taken by blockers) has to be bounded somehow. |
1312 operations taken by blockers) has to be bounded somehow. |