1354 (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)" |
1174 (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)" |
1355 hence "(n1, n2) \<in> RAG s" by simp |
1175 hence "(n1, n2) \<in> RAG s" by simp |
1356 thus ?thesis |
1176 thus ?thesis |
1357 proof(cases rule:in_RAG_E) |
1177 proof(cases rule:in_RAG_E) |
1358 case (waiting th' cs') |
1178 case (waiting th' cs') |
1359 thus ?thesis |
1179 from h and this(1,2) |
|
1180 have "th' \<noteq> h_n.taker \<or> cs' \<noteq> cs" by auto |
|
1181 hence "waiting (e#s) th' cs'" |
|
1182 proof |
|
1183 assume "cs' \<noteq> cs" |
|
1184 from waiting_esI1[OF waiting(3) this] |
|
1185 show ?thesis . |
|
1186 next |
|
1187 assume neq_th': "th' \<noteq> h_n.taker" |
|
1188 show ?thesis |
|
1189 proof(cases "cs' = cs") |
|
1190 case False |
|
1191 from waiting_esI1[OF waiting(3) this] |
|
1192 show ?thesis . |
|
1193 next |
|
1194 case True |
|
1195 from h_n.waiting_esI2[OF waiting(3)[unfolded True] neq_th', folded True] |
|
1196 show ?thesis . |
|
1197 qed |
|
1198 qed |
|
1199 thus ?thesis using waiting(1,2) |
|
1200 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
1201 next |
|
1202 case (holding th' cs') |
|
1203 from h this(1,2) |
|
1204 have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto |
|
1205 hence "holding (e#s) th' cs'" |
|
1206 proof |
|
1207 assume "cs' \<noteq> cs" |
|
1208 from holding_esI2[OF this holding(3)] |
|
1209 show ?thesis . |
|
1210 next |
|
1211 assume "th' \<noteq> th" |
|
1212 from holding_esI1[OF holding(3) this] |
|
1213 show ?thesis . |
|
1214 qed |
|
1215 thus ?thesis using holding(1,2) |
|
1216 by (unfold s_RAG_def, fold holding_eq, auto) |
1360 qed |
1217 qed |
1361 qed |
1218 qed |
1362 qed |
1219 next |
1363 qed |
1220 case True |
1364 |
1221 interpret h_e: valid_trace_v_e s e th cs |
1365 end |
1222 by (unfold_locales, insert True, simp) |
1366 |
1223 from h[unfolded h_e.waiting_set_eq h_e.holding_set_eq] |
1367 |
1224 have h_s: "(n1, n2) \<in> RAG s" "(n1, n2) \<noteq> (Cs cs, Th th)" |
1368 lemma step_RAG_v: (* ccc *) |
1225 by auto |
|
1226 from h_s(1) |
|
1227 show ?thesis |
|
1228 proof(cases rule:in_RAG_E) |
|
1229 case (waiting th' cs') |
|
1230 from h_e.waiting_esI2[OF this(3)] |
|
1231 show ?thesis using waiting(1,2) |
|
1232 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
1233 next |
|
1234 case (holding th' cs') |
|
1235 with h_s(2) |
|
1236 have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto |
|
1237 thus ?thesis |
|
1238 proof |
|
1239 assume neq_cs: "cs' \<noteq> cs" |
|
1240 from holding_esI2[OF this holding(3)] |
|
1241 show ?thesis using holding(1,2) |
|
1242 by (unfold s_RAG_def, fold holding_eq, auto) |
|
1243 next |
|
1244 assume "th' \<noteq> th" |
|
1245 from holding_esI1[OF holding(3) this] |
|
1246 show ?thesis using holding(1,2) |
|
1247 by (unfold s_RAG_def, fold holding_eq, auto) |
|
1248 qed |
|
1249 qed |
|
1250 qed |
|
1251 qed |
|
1252 |
|
1253 end |
|
1254 |
|
1255 lemma step_RAG_v: |
1369 assumes vt: |
1256 assumes vt: |
1370 "vt (V th cs#s)" |
1257 "vt (V th cs#s)" |
1371 shows " |
1258 shows " |
1372 RAG (V th cs # s) = |
1259 RAG (V th cs # s) = |
1373 RAG s - {(Cs cs, Th th)} - |
1260 RAG s - {(Cs cs, Th th)} - |
1374 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
1261 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
1375 {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") |
1262 {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") |
1376 proof(rule rel_eqI) |
1263 proof - |
1377 fix n1 n2 |
1264 interpret vt_v: valid_trace_v s "V th cs" |
1378 assume "(n1, n2) \<in> ?L" |
1265 using assms step_back_vt by (unfold_locales, auto) |
1379 show "(n1, n2) \<in> ?R" sorry |
1266 show ?thesis using vt_v.RAG_es . |
|
1267 qed |
|
1268 |
|
1269 lemma (in valid_trace_create) |
|
1270 th_not_in_threads: "th \<notin> threads s" |
|
1271 proof - |
|
1272 from pip_e[unfolded is_create] |
|
1273 show ?thesis by (cases, simp) |
|
1274 qed |
|
1275 |
|
1276 lemma (in valid_trace_create) |
|
1277 threads_es [simp]: "threads (e#s) = threads s \<union> {th}" |
|
1278 by (unfold is_create, simp) |
|
1279 |
|
1280 lemma (in valid_trace_exit) |
|
1281 threads_es [simp]: "threads (e#s) = threads s - {th}" |
|
1282 by (unfold is_exit, simp) |
|
1283 |
|
1284 lemma (in valid_trace_p) |
|
1285 threads_es [simp]: "threads (e#s) = threads s" |
|
1286 by (unfold is_p, simp) |
|
1287 |
|
1288 lemma (in valid_trace_v) |
|
1289 threads_es [simp]: "threads (e#s) = threads s" |
|
1290 by (unfold is_v, simp) |
|
1291 |
|
1292 lemma (in valid_trace_v) |
|
1293 th_not_in_rest[simp]: "th \<notin> set rest" |
|
1294 proof |
|
1295 assume otherwise: "th \<in> set rest" |
|
1296 have "distinct (wq s cs)" by (simp add: wq_distinct) |
|
1297 from this[unfolded wq_s_cs] and otherwise |
|
1298 show False by auto |
|
1299 qed |
|
1300 |
|
1301 lemma (in valid_trace_v) |
|
1302 set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}" |
|
1303 proof(unfold wq_es_cs wq'_def, rule someI2) |
|
1304 show "distinct rest \<and> set rest = set rest" |
|
1305 by (simp add: distinct_rest) |
1380 next |
1306 next |
1381 fix n1 n2 |
1307 fix x |
1382 assume "(n1, n2) \<in> ?R" |
1308 assume "distinct x \<and> set x = set rest" |
1383 show "(n1, n2) \<in> ?L" sorry |
1309 thus "set x = set (wq s cs) - {th}" |
1384 qed |
1310 by (unfold wq_s_cs, simp) |
1385 |
1311 qed |
1386 |
1312 |
1387 |
1313 lemma (in valid_trace_exit) |
1388 text {* (* ddd *) |
1314 th_not_in_wq: "th \<notin> set (wq s cs)" |
1389 The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed |
1315 proof - |
1390 with the happening of @{text "V"}-events: |
1316 from pip_e[unfolded is_exit] |
1391 *} |
1317 show ?thesis |
1392 lemma step_RAG_v: |
1318 by (cases, unfold holdents_def s_holding_def, fold wq_def, |
1393 assumes vt: |
1319 auto elim!:runing_wqE) |
1394 "vt (V th cs#s)" |
1320 qed |
1395 shows " |
1321 |
1396 RAG (V th cs # s) = |
1322 lemma (in valid_trace) wq_threads: |
1397 RAG s - {(Cs cs, Th th)} - |
1323 assumes "th \<in> set (wq s cs)" |
1398 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
1324 shows "th \<in> threads s" |
1399 {(Cs cs, Th th') |th'. next_th s th cs th'}" |
1325 using assms |
1400 apply (insert vt, unfold s_RAG_def) |
1326 proof(induct rule:ind) |
1401 apply (auto split:if_splits list.splits simp:Let_def) |
1327 case (Nil) |
1402 apply (auto elim: step_v_waiting_mono step_v_hold_inv |
1328 thus ?case by (auto simp:wq_def) |
1403 step_v_release step_v_wait_inv |
1329 next |
1404 step_v_get_hold step_v_release_inv) |
1330 case (Cons s e) |
1405 apply (erule_tac step_v_not_wait, auto) |
1331 interpret vt_e: valid_trace_e s e using Cons by simp |
1406 done |
|
1407 |
|
1408 text {* |
|
1409 The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed |
|
1410 with the happening of @{text "P"}-events: |
|
1411 *} |
|
1412 lemma step_RAG_p: |
|
1413 "vt (P th cs#s) \<Longrightarrow> |
|
1414 RAG (P th cs # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)} |
|
1415 else RAG s \<union> {(Th th, Cs cs)})" |
|
1416 apply(simp only: s_RAG_def wq_def) |
|
1417 apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def) |
|
1418 apply(case_tac "csa = cs", auto) |
|
1419 apply(fold wq_def) |
|
1420 apply(drule_tac step_back_step) |
|
1421 apply(ind_cases " step s (P (hd (wq s cs)) cs)") |
|
1422 apply(simp add:s_RAG_def wq_def cs_holding_def) |
|
1423 apply(auto) |
|
1424 done |
|
1425 |
|
1426 |
|
1427 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs" |
|
1428 by (unfold s_RAG_def, auto) |
|
1429 |
|
1430 context valid_trace |
|
1431 begin |
|
1432 |
|
1433 text {* |
|
1434 The following lemma shows that @{text "RAG"} is acyclic. |
|
1435 The overall structure is by induction on the formation of @{text "vt s"} |
|
1436 and then case analysis on event @{text "e"}, where the non-trivial cases |
|
1437 for those for @{text "V"} and @{text "P"} events. |
|
1438 *} |
|
1439 lemma acyclic_RAG: |
|
1440 shows "acyclic (RAG s)" |
|
1441 using vt |
|
1442 proof(induct) |
|
1443 case (vt_cons s e) |
|
1444 interpret vt_s: valid_trace s using vt_cons(1) |
|
1445 by (unfold_locales, simp) |
|
1446 assume ih: "acyclic (RAG s)" |
|
1447 and stp: "step s e" |
|
1448 and vt: "vt s" |
|
1449 show ?case |
1332 show ?case |
1450 proof(cases e) |
1333 proof(cases e) |
1451 case (Create th prio) |
1334 case (Create th' prio') |
1452 with ih |
1335 interpret vt: valid_trace_create s e th' prio' |
1453 show ?thesis by (simp add:RAG_create_unchanged) |
1336 using Create by (unfold_locales, simp) |
1454 next |
1337 show ?thesis |
1455 case (Exit th) |
1338 using Cons.hyps(2) Cons.prems by auto |
1456 with ih show ?thesis by (simp add:RAG_exit_unchanged) |
1339 next |
1457 next |
1340 case (Exit th') |
1458 case (V th cs) |
1341 interpret vt: valid_trace_exit s e th' |
1459 from V vt stp have vtt: "vt (V th cs#s)" by auto |
1342 using Exit by (unfold_locales, simp) |
1460 from step_RAG_v [OF this] |
1343 show ?thesis |
1461 have eq_de: |
1344 using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto |
1462 "RAG (e # s) = |
1345 next |
1463 RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
1346 case (P th' cs') |
1464 {(Cs cs, Th th') |th'. next_th s th cs th'}" |
1347 interpret vt: valid_trace_p s e th' cs' |
1465 (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V) |
1348 using P by (unfold_locales, simp) |
1466 from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset) |
1349 show ?thesis |
1467 from step_back_step [OF vtt] |
1350 using Cons.hyps(2) Cons.prems readys_threads |
1468 have "step s (V th cs)" . |
1351 runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv |
1469 thus ?thesis |
1352 by fastforce |
1470 proof(cases) |
1353 next |
1471 assume "holding s th cs" |
1354 case (V th' cs') |
1472 hence th_in: "th \<in> set (wq s cs)" and |
1355 interpret vt: valid_trace_v s e th' cs' |
1473 eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto |
1356 using V by (unfold_locales, simp) |
1474 then obtain rest where |
1357 show ?thesis using Cons |
1475 eq_wq: "wq s cs = th#rest" |
1358 using vt.is_v vt.threads_es vt_e.wq_in_inv by blast |
1476 by (cases "wq s cs", auto) |
1359 next |
1477 show ?thesis |
1360 case (Set th' prio) |
1478 proof(cases "rest = []") |
1361 interpret vt: valid_trace_set s e th' prio |
1479 case False |
1362 using Set by (unfold_locales, simp) |
1480 let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" |
1363 show ?thesis using Cons.hyps(2) Cons.prems vt.is_set |
1481 from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}" |
1364 by (auto simp:wq_def Let_def) |
1482 by (unfold next_th_def, auto) |
1365 qed |
1483 let ?E = "(?A - ?B - ?C)" |
1366 qed |
1484 have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*" |
|
1485 proof |
|
1486 assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*" |
|
1487 hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl) |
|
1488 from tranclD [OF this] |
|
1489 obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast |
|
1490 hence th_d: "(Th ?th', x) \<in> ?A" by simp |
|
1491 from RAG_target_th [OF this] |
|
1492 obtain cs' where eq_x: "x = Cs cs'" by auto |
|
1493 with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp |
|
1494 hence wt_th': "waiting s ?th' cs'" |
|
1495 unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp |
|
1496 hence "cs' = cs" |
|
1497 proof(rule vt_s.waiting_unique) |
|
1498 from eq_wq vt_s.wq_distinct[of cs] |
|
1499 show "waiting s ?th' cs" |
|
1500 apply (unfold s_waiting_def wq_def, auto) |
|
1501 proof - |
|
1502 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
1503 and eq_wq: "wq_fun (schs s) cs = th # rest" |
|
1504 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
1505 proof(rule someI2) |
|
1506 from vt_s.wq_distinct[of cs] and eq_wq |
|
1507 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto |
|
1508 next |
|
1509 fix x assume "distinct x \<and> set x = set rest" |
|
1510 with False show "x \<noteq> []" by auto |
|
1511 qed |
|
1512 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> |
|
1513 set (SOME q. distinct q \<and> set q = set rest)" by auto |
|
1514 moreover have "\<dots> = set rest" |
|
1515 proof(rule someI2) |
|
1516 from vt_s.wq_distinct[of cs] and eq_wq |
|
1517 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto |
|
1518 next |
|
1519 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
1520 qed |
|
1521 moreover note hd_in |
|
1522 ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto |
|
1523 next |
|
1524 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
1525 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest" |
|
1526 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
1527 proof(rule someI2) |
|
1528 from vt_s.wq_distinct[of cs] and eq_wq |
|
1529 show "distinct rest \<and> set rest = set rest" by auto |
|
1530 next |
|
1531 fix x assume "distinct x \<and> set x = set rest" |
|
1532 with False show "x \<noteq> []" by auto |
|
1533 qed |
|
1534 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> |
|
1535 set (SOME q. distinct q \<and> set q = set rest)" by auto |
|
1536 moreover have "\<dots> = set rest" |
|
1537 proof(rule someI2) |
|
1538 from vt_s.wq_distinct[of cs] and eq_wq |
|
1539 show "distinct rest \<and> set rest = set rest" by auto |
|
1540 next |
|
1541 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
1542 qed |
|
1543 moreover note hd_in |
|
1544 ultimately show False by auto |
|
1545 qed |
|
1546 qed |
|
1547 with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp |
|
1548 with False |
|
1549 show "False" by (auto simp: next_th_def eq_wq) |
|
1550 qed |
|
1551 with acyclic_insert[symmetric] and ac |
|
1552 and eq_de eq_D show ?thesis by auto |
|
1553 next |
|
1554 case True |
|
1555 with eq_wq |
|
1556 have eq_D: "?D = {}" |
|
1557 by (unfold next_th_def, auto) |
|
1558 with eq_de ac |
|
1559 show ?thesis by auto |
|
1560 qed |
|
1561 qed |
|
1562 next |
|
1563 case (P th cs) |
|
1564 from P vt stp have vtt: "vt (P th cs#s)" by auto |
|
1565 from step_RAG_p [OF this] P |
|
1566 have "RAG (e # s) = |
|
1567 (if wq s cs = [] then RAG s \<union> {(Cs cs, Th th)} else |
|
1568 RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R") |
|
1569 by simp |
|
1570 moreover have "acyclic ?R" |
|
1571 proof(cases "wq s cs = []") |
|
1572 case True |
|
1573 hence eq_r: "?R = RAG s \<union> {(Cs cs, Th th)}" by simp |
|
1574 have "(Th th, Cs cs) \<notin> (RAG s)\<^sup>*" |
|
1575 proof |
|
1576 assume "(Th th, Cs cs) \<in> (RAG s)\<^sup>*" |
|
1577 hence "(Th th, Cs cs) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) |
|
1578 from tranclD2 [OF this] |
|
1579 obtain x where "(x, Cs cs) \<in> RAG s" by auto |
|
1580 with True show False by (auto simp:s_RAG_def cs_waiting_def) |
|
1581 qed |
|
1582 with acyclic_insert ih eq_r show ?thesis by auto |
|
1583 next |
|
1584 case False |
|
1585 hence eq_r: "?R = RAG s \<union> {(Th th, Cs cs)}" by simp |
|
1586 have "(Cs cs, Th th) \<notin> (RAG s)\<^sup>*" |
|
1587 proof |
|
1588 assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*" |
|
1589 hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) |
|
1590 moreover from step_back_step [OF vtt] have "step s (P th cs)" . |
|
1591 ultimately show False |
|
1592 proof - |
|
1593 show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False" |
|
1594 by (ind_cases "step s (P th cs)", simp) |
|
1595 qed |
|
1596 qed |
|
1597 with acyclic_insert ih eq_r show ?thesis by auto |
|
1598 qed |
|
1599 ultimately show ?thesis by simp |
|
1600 next |
|
1601 case (Set thread prio) |
|
1602 with ih |
|
1603 thm RAG_set_unchanged |
|
1604 show ?thesis by (simp add:RAG_set_unchanged) |
|
1605 qed |
|
1606 next |
|
1607 case vt_nil |
|
1608 show "acyclic (RAG ([]::state))" |
|
1609 by (auto simp: s_RAG_def cs_waiting_def |
|
1610 cs_holding_def wq_def acyclic_def) |
|
1611 qed |
|
1612 |
|
1613 |
|
1614 lemma finite_RAG: |
|
1615 shows "finite (RAG s)" |
|
1616 proof - |
|
1617 from vt show ?thesis |
|
1618 proof(induct) |
|
1619 case (vt_cons s e) |
|
1620 interpret vt_s: valid_trace s using vt_cons(1) |
|
1621 by (unfold_locales, simp) |
|
1622 assume ih: "finite (RAG s)" |
|
1623 and stp: "step s e" |
|
1624 and vt: "vt s" |
|
1625 show ?case |
|
1626 proof(cases e) |
|
1627 case (Create th prio) |
|
1628 with ih |
|
1629 show ?thesis by (simp add:RAG_create_unchanged) |
|
1630 next |
|
1631 case (Exit th) |
|
1632 with ih show ?thesis by (simp add:RAG_exit_unchanged) |
|
1633 next |
|
1634 case (V th cs) |
|
1635 from V vt stp have vtt: "vt (V th cs#s)" by auto |
|
1636 from step_RAG_v [OF this] |
|
1637 have eq_de: "RAG (e # s) = |
|
1638 RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
|
1639 {(Cs cs, Th th') |th'. next_th s th cs th'} |
|
1640 " |
|
1641 (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V) |
|
1642 moreover from ih have ac: "finite (?A - ?B - ?C)" by simp |
|
1643 moreover have "finite ?D" |
|
1644 proof - |
|
1645 have "?D = {} \<or> (\<exists> a. ?D = {a})" |
|
1646 by (unfold next_th_def, auto) |
|
1647 thus ?thesis |
|
1648 proof |
|
1649 assume h: "?D = {}" |
|
1650 show ?thesis by (unfold h, simp) |
|
1651 next |
|
1652 assume "\<exists> a. ?D = {a}" |
|
1653 thus ?thesis |
|
1654 by (metis finite.simps) |
|
1655 qed |
|
1656 qed |
|
1657 ultimately show ?thesis by simp |
|
1658 next |
|
1659 case (P th cs) |
|
1660 from P vt stp have vtt: "vt (P th cs#s)" by auto |
|
1661 from step_RAG_p [OF this] P |
|
1662 have "RAG (e # s) = |
|
1663 (if wq s cs = [] then RAG s \<union> {(Cs cs, Th th)} else |
|
1664 RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R") |
|
1665 by simp |
|
1666 moreover have "finite ?R" |
|
1667 proof(cases "wq s cs = []") |
|
1668 case True |
|
1669 hence eq_r: "?R = RAG s \<union> {(Cs cs, Th th)}" by simp |
|
1670 with True and ih show ?thesis by auto |
|
1671 next |
|
1672 case False |
|
1673 hence "?R = RAG s \<union> {(Th th, Cs cs)}" by simp |
|
1674 with False and ih show ?thesis by auto |
|
1675 qed |
|
1676 ultimately show ?thesis by auto |
|
1677 next |
|
1678 case (Set thread prio) |
|
1679 with ih |
|
1680 show ?thesis by (simp add:RAG_set_unchanged) |
|
1681 qed |
|
1682 next |
|
1683 case vt_nil |
|
1684 show "finite (RAG ([]::state))" |
|
1685 by (auto simp: s_RAG_def cs_waiting_def |
|
1686 cs_holding_def wq_def acyclic_def) |
|
1687 qed |
|
1688 qed |
|
1689 |
|
1690 text {* Several useful lemmas *} |
|
1691 |
|
1692 lemma wf_dep_converse: |
|
1693 shows "wf ((RAG s)^-1)" |
|
1694 proof(rule finite_acyclic_wf_converse) |
|
1695 from finite_RAG |
|
1696 show "finite (RAG s)" . |
|
1697 next |
|
1698 from acyclic_RAG |
|
1699 show "acyclic (RAG s)" . |
|
1700 qed |
|
1701 |
|
1702 end |
|
1703 |
|
1704 lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l" |
|
1705 by (induct l, auto) |
|
1706 |
|
1707 lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s" |
|
1708 by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) |
|
1709 |
1367 |
1710 context valid_trace |
1368 context valid_trace |
1711 begin |
1369 begin |
1712 |
1370 |
1713 lemma wq_threads: |
1371 lemma dm_RAG_threads: |
1714 assumes h: "th \<in> set (wq s cs)" |
|
1715 shows "th \<in> threads s" |
|
1716 proof - |
|
1717 from vt and h show ?thesis |
|
1718 proof(induct arbitrary: th cs) |
|
1719 case (vt_cons s e) |
|
1720 interpret vt_s: valid_trace s |
|
1721 using vt_cons(1) by (unfold_locales, auto) |
|
1722 assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s" |
|
1723 and stp: "step s e" |
|
1724 and vt: "vt s" |
|
1725 and h: "th \<in> set (wq (e # s) cs)" |
|
1726 show ?case |
|
1727 proof(cases e) |
|
1728 case (Create th' prio) |
|
1729 with ih h show ?thesis |
|
1730 by (auto simp:wq_def Let_def) |
|
1731 next |
|
1732 case (Exit th') |
|
1733 with stp ih h show ?thesis |
|
1734 apply (auto simp:wq_def Let_def) |
|
1735 apply (ind_cases "step s (Exit th')") |
|
1736 apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def |
|
1737 s_RAG_def s_holding_def cs_holding_def) |
|
1738 done |
|
1739 next |
|
1740 case (V th' cs') |
|
1741 show ?thesis |
|
1742 proof(cases "cs' = cs") |
|
1743 case False |
|
1744 with h |
|
1745 show ?thesis |
|
1746 apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def) |
|
1747 by (drule_tac ih, simp) |
|
1748 next |
|
1749 case True |
|
1750 from h |
|
1751 show ?thesis |
|
1752 proof(unfold V wq_def) |
|
1753 assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l") |
|
1754 show "th \<in> threads (V th' cs' # s)" |
|
1755 proof(cases "cs = cs'") |
|
1756 case False |
|
1757 hence "?l = wq_fun (schs s) cs" by (simp add:Let_def) |
|
1758 with th_in have " th \<in> set (wq s cs)" |
|
1759 by (fold wq_def, simp) |
|
1760 from ih [OF this] show ?thesis by simp |
|
1761 next |
|
1762 case True |
|
1763 show ?thesis |
|
1764 proof(cases "wq_fun (schs s) cs'") |
|
1765 case Nil |
|
1766 with h V show ?thesis |
|
1767 apply (auto simp:wq_def Let_def split:if_splits) |
|
1768 by (fold wq_def, drule_tac ih, simp) |
|
1769 next |
|
1770 case (Cons a rest) |
|
1771 assume eq_wq: "wq_fun (schs s) cs' = a # rest" |
|
1772 with h V show ?thesis |
|
1773 apply (auto simp:Let_def wq_def split:if_splits) |
|
1774 proof - |
|
1775 assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
|
1776 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
1777 proof(rule someI2) |
|
1778 from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def] |
|
1779 show "distinct rest \<and> set rest = set rest" by auto |
|
1780 next |
|
1781 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" |
|
1782 by auto |
|
1783 qed |
|
1784 with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto |
|
1785 from ih[OF this[folded wq_def]] show "th \<in> threads s" . |
|
1786 next |
|
1787 assume th_in: "th \<in> set (wq_fun (schs s) cs)" |
|
1788 from ih[OF this[folded wq_def]] |
|
1789 show "th \<in> threads s" . |
|
1790 qed |
|
1791 qed |
|
1792 qed |
|
1793 qed |
|
1794 qed |
|
1795 next |
|
1796 case (P th' cs') |
|
1797 from h stp |
|
1798 show ?thesis |
|
1799 apply (unfold P wq_def) |
|
1800 apply (auto simp:Let_def split:if_splits, fold wq_def) |
|
1801 apply (auto intro:ih) |
|
1802 apply(ind_cases "step s (P th' cs')") |
|
1803 by (unfold runing_def readys_def, auto) |
|
1804 next |
|
1805 case (Set thread prio) |
|
1806 with ih h show ?thesis |
|
1807 by (auto simp:wq_def Let_def) |
|
1808 qed |
|
1809 next |
|
1810 case vt_nil |
|
1811 thus ?case by (auto simp:wq_def) |
|
1812 qed |
|
1813 qed |
|
1814 |
|
1815 lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s" |
|
1816 apply(unfold s_RAG_def cs_waiting_def cs_holding_def) |
|
1817 by (auto intro:wq_threads) |
|
1818 |
|
1819 lemma readys_v_eq: |
|
1820 assumes neq_th: "th \<noteq> thread" |
|
1821 and eq_wq: "wq s cs = thread#rest" |
|
1822 and not_in: "th \<notin> set rest" |
|
1823 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
|
1824 proof - |
|
1825 from assms show ?thesis |
|
1826 apply (auto simp:readys_def) |
|
1827 apply(simp add:s_waiting_def[folded wq_def]) |
|
1828 apply (erule_tac x = csa in allE) |
|
1829 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
|
1830 apply (case_tac "csa = cs", simp) |
|
1831 apply (erule_tac x = cs in allE) |
|
1832 apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) |
|
1833 apply(auto simp add: wq_def) |
|
1834 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
|
1835 proof - |
|
1836 assume th_nin: "th \<notin> set rest" |
|
1837 and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
|
1838 and eq_wq: "wq_fun (schs s) cs = thread # rest" |
|
1839 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
1840 proof(rule someI2) |
|
1841 from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def] |
|
1842 show "distinct rest \<and> set rest = set rest" by auto |
|
1843 next |
|
1844 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
1845 qed |
|
1846 with th_nin th_in show False by auto |
|
1847 qed |
|
1848 qed |
|
1849 |
|
1850 text {* \noindent |
|
1851 The following lemmas shows that: starting from any node in @{text "RAG"}, |
|
1852 by chasing out-going edges, it is always possible to reach a node representing a ready |
|
1853 thread. In this lemma, it is the @{text "th'"}. |
|
1854 *} |
|
1855 |
|
1856 lemma chain_building: |
|
1857 shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)" |
|
1858 proof - |
|
1859 from wf_dep_converse |
|
1860 have h: "wf ((RAG s)\<inverse>)" . |
|
1861 show ?thesis |
|
1862 proof(induct rule:wf_induct [OF h]) |
|
1863 fix x |
|
1864 assume ih [rule_format]: |
|
1865 "\<forall>y. (y, x) \<in> (RAG s)\<inverse> \<longrightarrow> |
|
1866 y \<in> Domain (RAG s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (y, Th th') \<in> (RAG s)\<^sup>+)" |
|
1867 show "x \<in> Domain (RAG s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (RAG s)\<^sup>+)" |
|
1868 proof |
|
1869 assume x_d: "x \<in> Domain (RAG s)" |
|
1870 show "\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (RAG s)\<^sup>+" |
|
1871 proof(cases x) |
|
1872 case (Th th) |
|
1873 from x_d Th obtain cs where x_in: "(Th th, Cs cs) \<in> RAG s" by (auto simp:s_RAG_def) |
|
1874 with Th have x_in_r: "(Cs cs, x) \<in> (RAG s)^-1" by simp |
|
1875 from th_chasing [OF x_in] obtain th' where "(Cs cs, Th th') \<in> RAG s" by blast |
|
1876 hence "Cs cs \<in> Domain (RAG s)" by auto |
|
1877 from ih [OF x_in_r this] obtain th' |
|
1878 where th'_ready: " th' \<in> readys s" and cs_in: "(Cs cs, Th th') \<in> (RAG s)\<^sup>+" by auto |
|
1879 have "(x, Th th') \<in> (RAG s)\<^sup>+" using Th x_in cs_in by auto |
|
1880 with th'_ready show ?thesis by auto |
|
1881 next |
|
1882 case (Cs cs) |
|
1883 from x_d Cs obtain th' where th'_d: "(Th th', x) \<in> (RAG s)^-1" by (auto simp:s_RAG_def) |
|
1884 show ?thesis |
|
1885 proof(cases "th' \<in> readys s") |
|
1886 case True |
|
1887 from True and th'_d show ?thesis by auto |
|
1888 next |
|
1889 case False |
|
1890 from th'_d and range_in have "th' \<in> threads s" by auto |
|
1891 with False have "Th th' \<in> Domain (RAG s)" |
|
1892 by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def) |
|
1893 from ih [OF th'_d this] |
|
1894 obtain th'' where |
|
1895 th''_r: "th'' \<in> readys s" and |
|
1896 th''_in: "(Th th', Th th'') \<in> (RAG s)\<^sup>+" by auto |
|
1897 from th'_d and th''_in |
|
1898 have "(x, Th th'') \<in> (RAG s)\<^sup>+" by auto |
|
1899 with th''_r show ?thesis by auto |
|
1900 qed |
|
1901 qed |
|
1902 qed |
|
1903 qed |
|
1904 qed |
|
1905 |
|
1906 text {* \noindent |
|
1907 The following is just an instance of @{text "chain_building"}. |
|
1908 *} |
|
1909 lemma th_chain_to_ready: |
|
1910 assumes th_in: "th \<in> threads s" |
|
1911 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)" |
|
1912 proof(cases "th \<in> readys s") |
|
1913 case True |
|
1914 thus ?thesis by auto |
|
1915 next |
|
1916 case False |
|
1917 from False and th_in have "Th th \<in> Domain (RAG s)" |
|
1918 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) |
|
1919 from chain_building [rule_format, OF this] |
|
1920 show ?thesis by auto |
|
1921 qed |
|
1922 |
|
1923 end |
|
1924 |
|
1925 |
|
1926 |
|
1927 lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2" |
|
1928 by (unfold s_holding_def cs_holding_def, auto) |
|
1929 |
|
1930 context valid_trace |
|
1931 begin |
|
1932 |
|
1933 lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2" |
|
1934 apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq) |
|
1935 by(auto elim:waiting_unique holding_unique) |
|
1936 |
|
1937 end |
|
1938 |
|
1939 |
|
1940 lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r" |
|
1941 by (induct rule:trancl_induct, auto) |
|
1942 |
|
1943 context valid_trace |
|
1944 begin |
|
1945 |
|
1946 lemma dchain_unique: |
|
1947 assumes th1_d: "(n, Th th1) \<in> (RAG s)^+" |
|
1948 and th1_r: "th1 \<in> readys s" |
|
1949 and th2_d: "(n, Th th2) \<in> (RAG s)^+" |
|
1950 and th2_r: "th2 \<in> readys s" |
|
1951 shows "th1 = th2" |
|
1952 proof - |
|
1953 { assume neq: "th1 \<noteq> th2" |
|
1954 hence "Th th1 \<noteq> Th th2" by simp |
|
1955 from unique_chain [OF _ th1_d th2_d this] and unique_RAG |
|
1956 have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto |
|
1957 hence "False" |
|
1958 proof |
|
1959 assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" |
|
1960 from trancl_split [OF this] |
|
1961 obtain n where dd: "(Th th1, n) \<in> RAG s" by auto |
|
1962 then obtain cs where eq_n: "n = Cs cs" |
|
1963 by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) |
|
1964 from dd eq_n have "th1 \<notin> readys s" |
|
1965 by (auto simp:readys_def s_RAG_def wq_def s_waiting_def cs_waiting_def) |
|
1966 with th1_r show ?thesis by auto |
|
1967 next |
|
1968 assume "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" |
|
1969 from trancl_split [OF this] |
|
1970 obtain n where dd: "(Th th2, n) \<in> RAG s" by auto |
|
1971 then obtain cs where eq_n: "n = Cs cs" |
|
1972 by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) |
|
1973 from dd eq_n have "th2 \<notin> readys s" |
|
1974 by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) |
|
1975 with th2_r show ?thesis by auto |
|
1976 qed |
|
1977 } thus ?thesis by auto |
|
1978 qed |
|
1979 |
|
1980 end |
|
1981 |
|
1982 |
|
1983 lemma step_holdents_p_add: |
|
1984 assumes vt: "vt (P th cs#s)" |
|
1985 and "wq s cs = []" |
|
1986 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
|
1987 proof - |
|
1988 from assms show ?thesis |
|
1989 unfolding holdents_test step_RAG_p[OF vt] by (auto) |
|
1990 qed |
|
1991 |
|
1992 lemma step_holdents_p_eq: |
|
1993 assumes vt: "vt (P th cs#s)" |
|
1994 and "wq s cs \<noteq> []" |
|
1995 shows "holdents (P th cs#s) th = holdents s th" |
|
1996 proof - |
|
1997 from assms show ?thesis |
|
1998 unfolding holdents_test step_RAG_p[OF vt] by auto |
|
1999 qed |
|
2000 |
|
2001 |
|
2002 lemma (in valid_trace) finite_holding : |
|
2003 shows "finite (holdents s th)" |
|
2004 proof - |
|
2005 let ?F = "\<lambda> (x, y). the_cs x" |
|
2006 from finite_RAG |
|
2007 have "finite (RAG s)" . |
|
2008 hence "finite (?F `(RAG s))" by simp |
|
2009 moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>" |
|
2010 proof - |
|
2011 { have h: "\<And> a A f. a \<in> A \<Longrightarrow> f a \<in> f ` A" by auto |
|
2012 fix x assume "(Cs x, Th th) \<in> RAG s" |
|
2013 hence "?F (Cs x, Th th) \<in> ?F `(RAG s)" by (rule h) |
|
2014 moreover have "?F (Cs x, Th th) = x" by simp |
|
2015 ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` RAG s" by simp |
|
2016 } thus ?thesis by auto |
|
2017 qed |
|
2018 ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset) |
|
2019 qed |
|
2020 |
|
2021 lemma cntCS_v_dec: |
|
2022 assumes vtv: "vt (V thread cs#s)" |
|
2023 shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" |
|
2024 proof - |
|
2025 from vtv interpret vt_s: valid_trace s |
|
2026 by (cases, unfold_locales, simp) |
|
2027 from vtv interpret vt_v: valid_trace "V thread cs#s" |
|
2028 by (unfold_locales, simp) |
|
2029 from step_back_step[OF vtv] |
|
2030 have cs_in: "cs \<in> holdents s thread" |
|
2031 apply (cases, unfold holdents_test s_RAG_def, simp) |
|
2032 by (unfold cs_holding_def s_holding_def wq_def, auto) |
|
2033 moreover have cs_not_in: |
|
2034 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
|
2035 apply (insert vt_s.wq_distinct[of cs]) |
|
2036 apply (unfold holdents_test, unfold step_RAG_v[OF vtv], |
|
2037 auto simp:next_th_def) |
|
2038 proof - |
|
2039 fix rest |
|
2040 assume dst: "distinct (rest::thread list)" |
|
2041 and ne: "rest \<noteq> []" |
|
2042 and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
2043 moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
2044 proof(rule someI2) |
|
2045 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
2046 next |
|
2047 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
2048 qed |
|
2049 ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> |
|
2050 set (SOME q. distinct q \<and> set q = set rest)" by simp |
|
2051 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
2052 proof(rule someI2) |
|
2053 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
2054 next |
|
2055 fix x assume " distinct x \<and> set x = set rest" with ne |
|
2056 show "x \<noteq> []" by auto |
|
2057 qed |
|
2058 ultimately |
|
2059 show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> RAG s" |
|
2060 by auto |
|
2061 next |
|
2062 fix rest |
|
2063 assume dst: "distinct (rest::thread list)" |
|
2064 and ne: "rest \<noteq> []" |
|
2065 and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
2066 moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
2067 proof(rule someI2) |
|
2068 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
2069 next |
|
2070 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
2071 qed |
|
2072 ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> |
|
2073 set (SOME q. distinct q \<and> set q = set rest)" by simp |
|
2074 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
2075 proof(rule someI2) |
|
2076 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
2077 next |
|
2078 fix x assume " distinct x \<and> set x = set rest" with ne |
|
2079 show "x \<noteq> []" by auto |
|
2080 qed |
|
2081 ultimately show "False" by auto |
|
2082 qed |
|
2083 ultimately |
|
2084 have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" |
|
2085 by auto |
|
2086 moreover have "card \<dots> = |
|
2087 Suc (card ((holdents (V thread cs#s) thread) - {cs}))" |
|
2088 proof(rule card_insert) |
|
2089 from vt_v.finite_holding |
|
2090 show " finite (holdents (V thread cs # s) thread)" . |
|
2091 qed |
|
2092 moreover from cs_not_in |
|
2093 have "cs \<notin> (holdents (V thread cs#s) thread)" by auto |
|
2094 ultimately show ?thesis by (simp add:cntCS_def) |
|
2095 qed |
|
2096 |
|
2097 lemma count_rec1 [simp]: |
|
2098 assumes "Q e" |
|
2099 shows "count Q (e#es) = Suc (count Q es)" |
|
2100 using assms |
|
2101 by (unfold count_def, auto) |
|
2102 |
|
2103 lemma count_rec2 [simp]: |
|
2104 assumes "\<not>Q e" |
|
2105 shows "count Q (e#es) = (count Q es)" |
|
2106 using assms |
|
2107 by (unfold count_def, auto) |
|
2108 |
|
2109 lemma count_rec3 [simp]: |
|
2110 shows "count Q [] = 0" |
|
2111 by (unfold count_def, auto) |
|
2112 |
|
2113 lemma cntP_diff_inv: |
|
2114 assumes "cntP (e#s) th \<noteq> cntP s th" |
|
2115 shows "isP e \<and> actor e = th" |
|
2116 proof(cases e) |
|
2117 case (P th' pty) |
|
2118 show ?thesis |
|
2119 by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", |
|
2120 insert assms P, auto simp:cntP_def) |
|
2121 qed (insert assms, auto simp:cntP_def) |
|
2122 |
|
2123 lemma cntV_diff_inv: |
|
2124 assumes "cntV (e#s) th \<noteq> cntV s th" |
|
2125 shows "isV e \<and> actor e = th" |
|
2126 proof(cases e) |
|
2127 case (V th' pty) |
|
2128 show ?thesis |
|
2129 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", |
|
2130 insert assms V, auto simp:cntV_def) |
|
2131 qed (insert assms, auto simp:cntV_def) |
|
2132 |
|
2133 context valid_trace |
|
2134 begin |
|
2135 |
|
2136 text {* (* ddd *) \noindent |
|
2137 The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} |
|
2138 of one particular thread. |
|
2139 *} |
|
2140 |
|
2141 lemma cnp_cnv_cncs: |
|
2142 shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s) |
|
2143 then cntCS s th else cntCS s th + 1)" |
|
2144 proof - |
|
2145 from vt show ?thesis |
|
2146 proof(induct arbitrary:th) |
|
2147 case (vt_cons s e) |
|
2148 interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) |
|
2149 assume vt: "vt s" |
|
2150 and ih: "\<And>th. cntP s th = cntV s th + |
|
2151 (if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)" |
|
2152 and stp: "step s e" |
|
2153 from stp show ?case |
|
2154 proof(cases) |
|
2155 case (thread_create thread prio) |
|
2156 assume eq_e: "e = Create thread prio" |
|
2157 and not_in: "thread \<notin> threads s" |
|
2158 show ?thesis |
|
2159 proof - |
|
2160 { fix cs |
|
2161 assume "thread \<in> set (wq s cs)" |
|
2162 from vt_s.wq_threads [OF this] have "thread \<in> threads s" . |
|
2163 with not_in have "False" by simp |
|
2164 } with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}" |
|
2165 by (auto simp:readys_def threads.simps s_waiting_def |
|
2166 wq_def cs_waiting_def Let_def) |
|
2167 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
|
2168 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
|
2169 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
|
2170 unfolding cntCS_def holdents_test |
|
2171 by (simp add:RAG_create_unchanged eq_e) |
|
2172 { assume "th \<noteq> thread" |
|
2173 with eq_readys eq_e |
|
2174 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
|
2175 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
|
2176 by (simp add:threads.simps) |
|
2177 with eq_cnp eq_cnv eq_cncs ih not_in |
|
2178 have ?thesis by simp |
|
2179 } moreover { |
|
2180 assume eq_th: "th = thread" |
|
2181 with not_in ih have " cntP s th = cntV s th + cntCS s th" by simp |
|
2182 moreover from eq_th and eq_readys have "th \<in> readys (e#s)" by simp |
|
2183 moreover note eq_cnp eq_cnv eq_cncs |
|
2184 ultimately have ?thesis by auto |
|
2185 } ultimately show ?thesis by blast |
|
2186 qed |
|
2187 next |
|
2188 case (thread_exit thread) |
|
2189 assume eq_e: "e = Exit thread" |
|
2190 and is_runing: "thread \<in> runing s" |
|
2191 and no_hold: "holdents s thread = {}" |
|
2192 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
|
2193 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
|
2194 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
|
2195 unfolding cntCS_def holdents_test |
|
2196 by (simp add:RAG_exit_unchanged eq_e) |
|
2197 { assume "th \<noteq> thread" |
|
2198 with eq_e |
|
2199 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
|
2200 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
|
2201 apply (simp add:threads.simps readys_def) |
|
2202 apply (subst s_waiting_def) |
|
2203 apply (simp add:Let_def) |
|
2204 apply (subst s_waiting_def, simp) |
|
2205 done |
|
2206 with eq_cnp eq_cnv eq_cncs ih |
|
2207 have ?thesis by simp |
|
2208 } moreover { |
|
2209 assume eq_th: "th = thread" |
|
2210 with ih is_runing have " cntP s th = cntV s th + cntCS s th" |
|
2211 by (simp add:runing_def) |
|
2212 moreover from eq_th eq_e have "th \<notin> threads (e#s)" |
|
2213 by simp |
|
2214 moreover note eq_cnp eq_cnv eq_cncs |
|
2215 ultimately have ?thesis by auto |
|
2216 } ultimately show ?thesis by blast |
|
2217 next |
|
2218 case (thread_P thread cs) |
|
2219 assume eq_e: "e = P thread cs" |
|
2220 and is_runing: "thread \<in> runing s" |
|
2221 and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+" |
|
2222 from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto |
|
2223 then interpret vt_p: valid_trace "(P thread cs#s)" |
|
2224 by (unfold_locales, simp) |
|
2225 show ?thesis |
|
2226 proof - |
|
2227 { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast |
|
2228 assume neq_th: "th \<noteq> thread" |
|
2229 with eq_e |
|
2230 have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))" |
|
2231 apply (simp add:readys_def s_waiting_def wq_def Let_def) |
|
2232 apply (rule_tac hh) |
|
2233 apply (intro iffI allI, clarify) |
|
2234 apply (erule_tac x = csa in allE, auto) |
|
2235 apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) |
|
2236 apply (erule_tac x = cs in allE, auto) |
|
2237 by (case_tac "(wq_fun (schs s) cs)", auto) |
|
2238 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
|
2239 apply (simp add:cntCS_def holdents_test) |
|
2240 by (unfold step_RAG_p [OF vtp], auto) |
|
2241 moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" |
|
2242 by (simp add:cntP_def count_def) |
|
2243 moreover from eq_e neq_th have "cntV (e#s) th = cntV s th" |
|
2244 by (simp add:cntV_def count_def) |
|
2245 moreover from eq_e neq_th have "threads (e#s) = threads s" by simp |
|
2246 moreover note ih [of th] |
|
2247 ultimately have ?thesis by simp |
|
2248 } moreover { |
|
2249 assume eq_th: "th = thread" |
|
2250 have ?thesis |
|
2251 proof - |
|
2252 from eq_e eq_th have eq_cnp: "cntP (e # s) th = 1 + (cntP s th)" |
|
2253 by (simp add:cntP_def count_def) |
|
2254 from eq_e eq_th have eq_cnv: "cntV (e#s) th = cntV s th" |
|
2255 by (simp add:cntV_def count_def) |
|
2256 show ?thesis |
|
2257 proof (cases "wq s cs = []") |
|
2258 case True |
|
2259 with is_runing |
|
2260 have "th \<in> readys (e#s)" |
|
2261 apply (unfold eq_e wq_def, unfold readys_def s_RAG_def) |
|
2262 apply (simp add: wq_def[symmetric] runing_def eq_th s_waiting_def) |
|
2263 by (auto simp:readys_def wq_def Let_def s_waiting_def wq_def) |
|
2264 moreover have "cntCS (e # s) th = 1 + cntCS s th" |
|
2265 proof - |
|
2266 have "card {csa. csa = cs \<or> (Cs csa, Th thread) \<in> RAG s} = |
|
2267 Suc (card {cs. (Cs cs, Th thread) \<in> RAG s})" (is "card ?L = Suc (card ?R)") |
|
2268 proof - |
|
2269 have "?L = insert cs ?R" by auto |
|
2270 moreover have "card \<dots> = Suc (card (?R - {cs}))" |
|
2271 proof(rule card_insert) |
|
2272 from vt_s.finite_holding [of thread] |
|
2273 show " finite {cs. (Cs cs, Th thread) \<in> RAG s}" |
|
2274 by (unfold holdents_test, simp) |
|
2275 qed |
|
2276 moreover have "?R - {cs} = ?R" |
|
2277 proof - |
|
2278 have "cs \<notin> ?R" |
|
2279 proof |
|
2280 assume "cs \<in> {cs. (Cs cs, Th thread) \<in> RAG s}" |
|
2281 with no_dep show False by auto |
|
2282 qed |
|
2283 thus ?thesis by auto |
|
2284 qed |
|
2285 ultimately show ?thesis by auto |
|
2286 qed |
|
2287 thus ?thesis |
|
2288 apply (unfold eq_e eq_th cntCS_def) |
|
2289 apply (simp add: holdents_test) |
|
2290 by (unfold step_RAG_p [OF vtp], auto simp:True) |
|
2291 qed |
|
2292 moreover from is_runing have "th \<in> readys s" |
|
2293 by (simp add:runing_def eq_th) |
|
2294 moreover note eq_cnp eq_cnv ih [of th] |
|
2295 ultimately show ?thesis by auto |
|
2296 next |
|
2297 case False |
|
2298 have eq_wq: "wq (e#s) cs = wq s cs @ [th]" |
|
2299 by (unfold eq_th eq_e wq_def, auto simp:Let_def) |
|
2300 have "th \<notin> readys (e#s)" |
|
2301 proof |
|
2302 assume "th \<in> readys (e#s)" |
|
2303 hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def) |
|
2304 from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" . |
|
2305 hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)" |
|
2306 by (simp add:s_waiting_def wq_def) |
|
2307 moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto |
|
2308 ultimately have "th = hd (wq (e#s) cs)" by blast |
|
2309 with eq_wq have "th = hd (wq s cs @ [th])" by simp |
|
2310 hence "th = hd (wq s cs)" using False by auto |
|
2311 with False eq_wq vt_p.wq_distinct [of cs] |
|
2312 show False by (fold eq_e, auto) |
|
2313 qed |
|
2314 moreover from is_runing have "th \<in> threads (e#s)" |
|
2315 by (unfold eq_e, auto simp:runing_def readys_def eq_th) |
|
2316 moreover have "cntCS (e # s) th = cntCS s th" |
|
2317 apply (unfold cntCS_def holdents_test eq_e step_RAG_p[OF vtp]) |
|
2318 by (auto simp:False) |
|
2319 moreover note eq_cnp eq_cnv ih[of th] |
|
2320 moreover from is_runing have "th \<in> readys s" |
|
2321 by (simp add:runing_def eq_th) |
|
2322 ultimately show ?thesis by auto |
|
2323 qed |
|
2324 qed |
|
2325 } ultimately show ?thesis by blast |
|
2326 qed |
|
2327 next |
|
2328 case (thread_V thread cs) |
|
2329 from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto |
|
2330 then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp) |
|
2331 assume eq_e: "e = V thread cs" |
|
2332 and is_runing: "thread \<in> runing s" |
|
2333 and hold: "holding s thread cs" |
|
2334 from hold obtain rest |
|
2335 where eq_wq: "wq s cs = thread # rest" |
|
2336 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
|
2337 have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e) |
|
2338 have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
2339 proof(rule someI2) |
|
2340 from vt_v.wq_distinct[of cs] and eq_wq |
|
2341 show "distinct rest \<and> set rest = set rest" |
|
2342 by (metis distinct.simps(2) vt_s.wq_distinct) |
|
2343 next |
|
2344 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" |
|
2345 by auto |
|
2346 qed |
|
2347 show ?thesis |
|
2348 proof - |
|
2349 { assume eq_th: "th = thread" |
|
2350 from eq_th have eq_cnp: "cntP (e # s) th = cntP s th" |
|
2351 by (unfold eq_e, simp add:cntP_def count_def) |
|
2352 moreover from eq_th have eq_cnv: "cntV (e#s) th = 1 + cntV s th" |
|
2353 by (unfold eq_e, simp add:cntV_def count_def) |
|
2354 moreover from cntCS_v_dec [OF vtv] |
|
2355 have "cntCS (e # s) thread + 1 = cntCS s thread" |
|
2356 by (simp add:eq_e) |
|
2357 moreover from is_runing have rd_before: "thread \<in> readys s" |
|
2358 by (unfold runing_def, simp) |
|
2359 moreover have "thread \<in> readys (e # s)" |
|
2360 proof - |
|
2361 from is_runing |
|
2362 have "thread \<in> threads (e#s)" |
|
2363 by (unfold eq_e, auto simp:runing_def readys_def) |
|
2364 moreover have "\<forall> cs1. \<not> waiting (e#s) thread cs1" |
|
2365 proof |
|
2366 fix cs1 |
|
2367 { assume eq_cs: "cs1 = cs" |
|
2368 have "\<not> waiting (e # s) thread cs1" |
|
2369 proof - |
|
2370 from eq_wq |
|
2371 have "thread \<notin> set (wq (e#s) cs1)" |
|
2372 apply(unfold eq_e wq_def eq_cs s_holding_def) |
|
2373 apply (auto simp:Let_def) |
|
2374 proof - |
|
2375 assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)" |
|
2376 with eq_set have "thread \<in> set rest" by simp |
|
2377 with vt_v.wq_distinct[of cs] |
|
2378 and eq_wq show False |
|
2379 by (metis distinct.simps(2) vt_s.wq_distinct) |
|
2380 qed |
|
2381 thus ?thesis by (simp add:wq_def s_waiting_def) |
|
2382 qed |
|
2383 } moreover { |
|
2384 assume neq_cs: "cs1 \<noteq> cs" |
|
2385 have "\<not> waiting (e # s) thread cs1" |
|
2386 proof - |
|
2387 from wq_v_neq [OF neq_cs[symmetric]] |
|
2388 have "wq (V thread cs # s) cs1 = wq s cs1" . |
|
2389 moreover have "\<not> waiting s thread cs1" |
|
2390 proof - |
|
2391 from runing_ready and is_runing |
|
2392 have "thread \<in> readys s" by auto |
|
2393 thus ?thesis by (simp add:readys_def) |
|
2394 qed |
|
2395 ultimately show ?thesis |
|
2396 by (auto simp:wq_def s_waiting_def eq_e) |
|
2397 qed |
|
2398 } ultimately show "\<not> waiting (e # s) thread cs1" by blast |
|
2399 qed |
|
2400 ultimately show ?thesis by (simp add:readys_def) |
|
2401 qed |
|
2402 moreover note eq_th ih |
|
2403 ultimately have ?thesis by auto |
|
2404 } moreover { |
|
2405 assume neq_th: "th \<noteq> thread" |
|
2406 from neq_th eq_e have eq_cnp: "cntP (e # s) th = cntP s th" |
|
2407 by (simp add:cntP_def count_def) |
|
2408 from neq_th eq_e have eq_cnv: "cntV (e # s) th = cntV s th" |
|
2409 by (simp add:cntV_def count_def) |
|
2410 have ?thesis |
|
2411 proof(cases "th \<in> set rest") |
|
2412 case False |
|
2413 have "(th \<in> readys (e # s)) = (th \<in> readys s)" |
|
2414 apply (insert step_back_vt[OF vtv]) |
|
2415 by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq) |
|
2416 moreover have "cntCS (e#s) th = cntCS s th" |
|
2417 apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) |
|
2418 proof - |
|
2419 have "{csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} = |
|
2420 {cs. (Cs cs, Th th) \<in> RAG s}" |
|
2421 proof - |
|
2422 from False eq_wq |
|
2423 have " next_th s thread cs th \<Longrightarrow> (Cs cs, Th th) \<in> RAG s" |
|
2424 apply (unfold next_th_def, auto) |
|
2425 proof - |
|
2426 assume ne: "rest \<noteq> []" |
|
2427 and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
2428 and eq_wq: "wq s cs = thread # rest" |
|
2429 from eq_set ni have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> |
|
2430 set (SOME q. distinct q \<and> set q = set rest) |
|
2431 " by simp |
|
2432 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
2433 proof(rule someI2) |
|
2434 from vt_s.wq_distinct[ of cs] and eq_wq |
|
2435 show "distinct rest \<and> set rest = set rest" by auto |
|
2436 next |
|
2437 fix x assume "distinct x \<and> set x = set rest" |
|
2438 with ne show "x \<noteq> []" by auto |
|
2439 qed |
|
2440 ultimately show |
|
2441 "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> RAG s" |
|
2442 by auto |
|
2443 qed |
|
2444 thus ?thesis by auto |
|
2445 qed |
|
2446 thus "card {csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} = |
|
2447 card {cs. (Cs cs, Th th) \<in> RAG s}" by simp |
|
2448 qed |
|
2449 moreover note ih eq_cnp eq_cnv eq_threads |
|
2450 ultimately show ?thesis by auto |
|
2451 next |
|
2452 case True |
|
2453 assume th_in: "th \<in> set rest" |
|
2454 show ?thesis |
|
2455 proof(cases "next_th s thread cs th") |
|
2456 case False |
|
2457 with eq_wq and th_in have |
|
2458 neq_hd: "th \<noteq> hd (SOME q. distinct q \<and> set q = set rest)" (is "th \<noteq> hd ?rest") |
|
2459 by (auto simp:next_th_def) |
|
2460 have "(th \<in> readys (e # s)) = (th \<in> readys s)" |
|
2461 proof - |
|
2462 from eq_wq and th_in |
|
2463 have "\<not> th \<in> readys s" |
|
2464 apply (auto simp:readys_def s_waiting_def) |
|
2465 apply (rule_tac x = cs in exI, auto) |
|
2466 by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def) |
|
2467 moreover |
|
2468 from eq_wq and th_in and neq_hd |
|
2469 have "\<not> (th \<in> readys (e # s))" |
|
2470 apply (auto simp:readys_def s_waiting_def eq_e wq_def Let_def split:list.splits) |
|
2471 by (rule_tac x = cs in exI, auto simp:eq_set) |
|
2472 ultimately show ?thesis by auto |
|
2473 qed |
|
2474 moreover have "cntCS (e#s) th = cntCS s th" |
|
2475 proof - |
|
2476 from eq_wq and th_in and neq_hd |
|
2477 have "(holdents (e # s) th) = (holdents s th)" |
|
2478 apply (unfold eq_e step_RAG_v[OF vtv], |
|
2479 auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def |
|
2480 Let_def cs_holding_def) |
|
2481 by (insert vt_s.wq_distinct[of cs], auto simp:wq_def) |
|
2482 thus ?thesis by (simp add:cntCS_def) |
|
2483 qed |
|
2484 moreover note ih eq_cnp eq_cnv eq_threads |
|
2485 ultimately show ?thesis by auto |
|
2486 next |
|
2487 case True |
|
2488 let ?rest = " (SOME q. distinct q \<and> set q = set rest)" |
|
2489 let ?t = "hd ?rest" |
|
2490 from True eq_wq th_in neq_th |
|
2491 have "th \<in> readys (e # s)" |
|
2492 apply (auto simp:eq_e readys_def s_waiting_def wq_def |
|
2493 Let_def next_th_def) |
|
2494 proof - |
|
2495 assume eq_wq: "wq_fun (schs s) cs = thread # rest" |
|
2496 and t_in: "?t \<in> set rest" |
|
2497 show "?t \<in> threads s" |
|
2498 proof(rule vt_s.wq_threads) |
|
2499 from eq_wq and t_in |
|
2500 show "?t \<in> set (wq s cs)" by (auto simp:wq_def) |
|
2501 qed |
|
2502 next |
|
2503 fix csa |
|
2504 assume eq_wq: "wq_fun (schs s) cs = thread # rest" |
|
2505 and t_in: "?t \<in> set rest" |
|
2506 and neq_cs: "csa \<noteq> cs" |
|
2507 and t_in': "?t \<in> set (wq_fun (schs s) csa)" |
|
2508 show "?t = hd (wq_fun (schs s) csa)" |
|
2509 proof - |
|
2510 { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)" |
|
2511 from vt_s.wq_distinct[of cs] and |
|
2512 eq_wq[folded wq_def] and t_in eq_wq |
|
2513 have "?t \<noteq> thread" by auto |
|
2514 with eq_wq and t_in |
|
2515 have w1: "waiting s ?t cs" |
|
2516 by (auto simp:s_waiting_def wq_def) |
|
2517 from t_in' neq_hd' |
|
2518 have w2: "waiting s ?t csa" |
|
2519 by (auto simp:s_waiting_def wq_def) |
|
2520 from vt_s.waiting_unique[OF w1 w2] |
|
2521 and neq_cs have "False" by auto |
|
2522 } thus ?thesis by auto |
|
2523 qed |
|
2524 qed |
|
2525 moreover have "cntP s th = cntV s th + cntCS s th + 1" |
|
2526 proof - |
|
2527 have "th \<notin> readys s" |
|
2528 proof - |
|
2529 from True eq_wq neq_th th_in |
|
2530 show ?thesis |
|
2531 apply (unfold readys_def s_waiting_def, auto) |
|
2532 by (rule_tac x = cs in exI, auto simp add: wq_def) |
|
2533 qed |
|
2534 moreover have "th \<in> threads s" |
|
2535 proof - |
|
2536 from th_in eq_wq |
|
2537 have "th \<in> set (wq s cs)" by simp |
|
2538 from vt_s.wq_threads [OF this] |
|
2539 show ?thesis . |
|
2540 qed |
|
2541 ultimately show ?thesis using ih by auto |
|
2542 qed |
|
2543 moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" |
|
2544 apply (unfold cntCS_def holdents_test eq_e step_RAG_v[OF vtv], auto) |
|
2545 proof - |
|
2546 show "card {csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs} = |
|
2547 Suc (card {cs. (Cs cs, Th th) \<in> RAG s})" |
|
2548 (is "card ?A = Suc (card ?B)") |
|
2549 proof - |
|
2550 have "?A = insert cs ?B" by auto |
|
2551 hence "card ?A = card (insert cs ?B)" by simp |
|
2552 also have "\<dots> = Suc (card ?B)" |
|
2553 proof(rule card_insert_disjoint) |
|
2554 have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)" |
|
2555 apply (auto simp:image_def) |
|
2556 by (rule_tac x = "(Cs x, Th th)" in bexI, auto) |
|
2557 with vt_s.finite_RAG |
|
2558 show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset) |
|
2559 next |
|
2560 show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}" |
|
2561 proof |
|
2562 assume "cs \<in> {cs. (Cs cs, Th th) \<in> RAG s}" |
|
2563 hence "(Cs cs, Th th) \<in> RAG s" by simp |
|
2564 with True neq_th eq_wq show False |
|
2565 by (auto simp:next_th_def s_RAG_def cs_holding_def) |
|
2566 qed |
|
2567 qed |
|
2568 finally show ?thesis . |
|
2569 qed |
|
2570 qed |
|
2571 moreover note eq_cnp eq_cnv |
|
2572 ultimately show ?thesis by simp |
|
2573 qed |
|
2574 qed |
|
2575 } ultimately show ?thesis by blast |
|
2576 qed |
|
2577 next |
|
2578 case (thread_set thread prio) |
|
2579 assume eq_e: "e = Set thread prio" |
|
2580 and is_runing: "thread \<in> runing s" |
|
2581 show ?thesis |
|
2582 proof - |
|
2583 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) |
|
2584 from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) |
|
2585 have eq_cncs: "cntCS (e#s) th = cntCS s th" |
|
2586 unfolding cntCS_def holdents_test |
|
2587 by (simp add:RAG_set_unchanged eq_e) |
|
2588 from eq_e have eq_readys: "readys (e#s) = readys s" |
|
2589 by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, |
|
2590 auto simp:Let_def) |
|
2591 { assume "th \<noteq> thread" |
|
2592 with eq_readys eq_e |
|
2593 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = |
|
2594 (th \<in> readys (s) \<or> th \<notin> threads (s))" |
|
2595 by (simp add:threads.simps) |
|
2596 with eq_cnp eq_cnv eq_cncs ih is_runing |
|
2597 have ?thesis by simp |
|
2598 } moreover { |
|
2599 assume eq_th: "th = thread" |
|
2600 with is_runing ih have " cntP s th = cntV s th + cntCS s th" |
|
2601 by (unfold runing_def, auto) |
|
2602 moreover from eq_th and eq_readys is_runing have "th \<in> readys (e#s)" |
|
2603 by (simp add:runing_def) |
|
2604 moreover note eq_cnp eq_cnv eq_cncs |
|
2605 ultimately have ?thesis by auto |
|
2606 } ultimately show ?thesis by blast |
|
2607 qed |
|
2608 qed |
|
2609 next |
|
2610 case vt_nil |
|
2611 show ?case |
|
2612 by (unfold cntP_def cntV_def cntCS_def, |
|
2613 auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) |
|
2614 qed |
|
2615 qed |
|
2616 |
|
2617 lemma not_thread_cncs: |
|
2618 assumes not_in: "th \<notin> threads s" |
|
2619 shows "cntCS s th = 0" |
|
2620 proof - |
|
2621 from vt not_in show ?thesis |
|
2622 proof(induct arbitrary:th) |
|
2623 case (vt_cons s e th) |
|
2624 interpret vt_s: valid_trace s using vt_cons(1) |
|
2625 by (unfold_locales, simp) |
|
2626 assume vt: "vt s" |
|
2627 and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0" |
|
2628 and stp: "step s e" |
|
2629 and not_in: "th \<notin> threads (e # s)" |
|
2630 from stp show ?case |
|
2631 proof(cases) |
|
2632 case (thread_create thread prio) |
|
2633 assume eq_e: "e = Create thread prio" |
|
2634 and not_in': "thread \<notin> threads s" |
|
2635 have "cntCS (e # s) th = cntCS s th" |
|
2636 apply (unfold eq_e cntCS_def holdents_test) |
|
2637 by (simp add:RAG_create_unchanged) |
|
2638 moreover have "th \<notin> threads s" |
|
2639 proof - |
|
2640 from not_in eq_e show ?thesis by simp |
|
2641 qed |
|
2642 moreover note ih ultimately show ?thesis by auto |
|
2643 next |
|
2644 case (thread_exit thread) |
|
2645 assume eq_e: "e = Exit thread" |
|
2646 and nh: "holdents s thread = {}" |
|
2647 have eq_cns: "cntCS (e # s) th = cntCS s th" |
|
2648 apply (unfold eq_e cntCS_def holdents_test) |
|
2649 by (simp add:RAG_exit_unchanged) |
|
2650 show ?thesis |
|
2651 proof(cases "th = thread") |
|
2652 case True |
|
2653 have "cntCS s th = 0" by (unfold cntCS_def, auto simp:nh True) |
|
2654 with eq_cns show ?thesis by simp |
|
2655 next |
|
2656 case False |
|
2657 with not_in and eq_e |
|
2658 have "th \<notin> threads s" by simp |
|
2659 from ih[OF this] and eq_cns show ?thesis by simp |
|
2660 qed |
|
2661 next |
|
2662 case (thread_P thread cs) |
|
2663 assume eq_e: "e = P thread cs" |
|
2664 and is_runing: "thread \<in> runing s" |
|
2665 from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto |
|
2666 have neq_th: "th \<noteq> thread" |
|
2667 proof - |
|
2668 from not_in eq_e have "th \<notin> threads s" by simp |
|
2669 moreover from is_runing have "thread \<in> threads s" |
|
2670 by (simp add:runing_def readys_def) |
|
2671 ultimately show ?thesis by auto |
|
2672 qed |
|
2673 hence "cntCS (e # s) th = cntCS s th " |
|
2674 apply (unfold cntCS_def holdents_test eq_e) |
|
2675 by (unfold step_RAG_p[OF vtp], auto) |
|
2676 moreover have "cntCS s th = 0" |
|
2677 proof(rule ih) |
|
2678 from not_in eq_e show "th \<notin> threads s" by simp |
|
2679 qed |
|
2680 ultimately show ?thesis by simp |
|
2681 next |
|
2682 case (thread_V thread cs) |
|
2683 assume eq_e: "e = V thread cs" |
|
2684 and is_runing: "thread \<in> runing s" |
|
2685 and hold: "holding s thread cs" |
|
2686 have neq_th: "th \<noteq> thread" |
|
2687 proof - |
|
2688 from not_in eq_e have "th \<notin> threads s" by simp |
|
2689 moreover from is_runing have "thread \<in> threads s" |
|
2690 by (simp add:runing_def readys_def) |
|
2691 ultimately show ?thesis by auto |
|
2692 qed |
|
2693 from assms thread_V vt stp ih |
|
2694 have vtv: "vt (V thread cs#s)" by auto |
|
2695 then interpret vt_v: valid_trace "(V thread cs#s)" |
|
2696 by (unfold_locales, simp) |
|
2697 from hold obtain rest |
|
2698 where eq_wq: "wq s cs = thread # rest" |
|
2699 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
|
2700 from not_in eq_e eq_wq |
|
2701 have "\<not> next_th s thread cs th" |
|
2702 apply (auto simp:next_th_def) |
|
2703 proof - |
|
2704 assume ne: "rest \<noteq> []" |
|
2705 and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s") |
|
2706 have "?t \<in> set rest" |
|
2707 proof(rule someI2) |
|
2708 from vt_v.wq_distinct[of cs] and eq_wq |
|
2709 show "distinct rest \<and> set rest = set rest" |
|
2710 by (metis distinct.simps(2) vt_s.wq_distinct) |
|
2711 next |
|
2712 fix x assume "distinct x \<and> set x = set rest" with ne |
|
2713 show "hd x \<in> set rest" by (cases x, auto) |
|
2714 qed |
|
2715 with eq_wq have "?t \<in> set (wq s cs)" by simp |
|
2716 from vt_s.wq_threads[OF this] and ni |
|
2717 show False |
|
2718 using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)` |
|
2719 ni vt_s.wq_threads by blast |
|
2720 qed |
|
2721 moreover note neq_th eq_wq |
|
2722 ultimately have "cntCS (e # s) th = cntCS s th" |
|
2723 by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) |
|
2724 moreover have "cntCS s th = 0" |
|
2725 proof(rule ih) |
|
2726 from not_in eq_e show "th \<notin> threads s" by simp |
|
2727 qed |
|
2728 ultimately show ?thesis by simp |
|
2729 next |
|
2730 case (thread_set thread prio) |
|
2731 print_facts |
|
2732 assume eq_e: "e = Set thread prio" |
|
2733 and is_runing: "thread \<in> runing s" |
|
2734 from not_in and eq_e have "th \<notin> threads s" by auto |
|
2735 from ih [OF this] and eq_e |
|
2736 show ?thesis |
|
2737 apply (unfold eq_e cntCS_def holdents_test) |
|
2738 by (simp add:RAG_set_unchanged) |
|
2739 qed |
|
2740 next |
|
2741 case vt_nil |
|
2742 show ?case |
|
2743 by (unfold cntCS_def, |
|
2744 auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) |
|
2745 qed |
|
2746 qed |
|
2747 |
|
2748 end |
|
2749 |
|
2750 |
|
2751 context valid_trace |
|
2752 begin |
|
2753 |
|
2754 lemma dm_RAG_threads: |
|
2755 assumes in_dom: "(Th th) \<in> Domain (RAG s)" |
1372 assumes in_dom: "(Th th) \<in> Domain (RAG s)" |
2756 shows "th \<in> threads s" |
1373 shows "th \<in> threads s" |
2757 proof - |
1374 proof - |
2758 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto |
1375 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto |
2759 moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto |
1376 moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto |
2761 hence "th \<in> set (wq s cs)" |
1378 hence "th \<in> set (wq s cs)" |
2762 by (unfold s_RAG_def, auto simp:cs_waiting_def) |
1379 by (unfold s_RAG_def, auto simp:cs_waiting_def) |
2763 from wq_threads [OF this] show ?thesis . |
1380 from wq_threads [OF this] show ?thesis . |
2764 qed |
1381 qed |
2765 |
1382 |
2766 end |
1383 lemma cp_le: |
2767 |
|
2768 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" |
|
2769 unfolding cp_def wq_def |
|
2770 apply(induct s rule: schs.induct) |
|
2771 thm cpreced_initial |
|
2772 apply(simp add: Let_def cpreced_initial) |
|
2773 apply(simp add: Let_def) |
|
2774 apply(simp add: Let_def) |
|
2775 apply(simp add: Let_def) |
|
2776 apply(subst (2) schs.simps) |
|
2777 apply(simp add: Let_def) |
|
2778 apply(subst (2) schs.simps) |
|
2779 apply(simp add: Let_def) |
|
2780 done |
|
2781 |
|
2782 context valid_trace |
|
2783 begin |
|
2784 |
|
2785 lemma runing_unique: |
|
2786 assumes runing_1: "th1 \<in> runing s" |
|
2787 and runing_2: "th2 \<in> runing s" |
|
2788 shows "th1 = th2" |
|
2789 proof - |
|
2790 from runing_1 and runing_2 have "cp s th1 = cp s th2" |
|
2791 unfolding runing_def |
|
2792 apply(simp) |
|
2793 done |
|
2794 hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) = |
|
2795 Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))" |
|
2796 (is "Max (?f ` ?A) = Max (?f ` ?B)") |
|
2797 unfolding cp_eq_cpreced |
|
2798 unfolding cpreced_def . |
|
2799 obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)" |
|
2800 proof - |
|
2801 have h1: "finite (?f ` ?A)" |
|
2802 proof - |
|
2803 have "finite ?A" |
|
2804 proof - |
|
2805 have "finite (dependants (wq s) th1)" |
|
2806 proof- |
|
2807 have "finite {th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+}" |
|
2808 proof - |
|
2809 let ?F = "\<lambda> (x, y). the_th x" |
|
2810 have "{th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)" |
|
2811 apply (auto simp:image_def) |
|
2812 by (rule_tac x = "(Th x, Th th1)" in bexI, auto) |
|
2813 moreover have "finite \<dots>" |
|
2814 proof - |
|
2815 from finite_RAG have "finite (RAG s)" . |
|
2816 hence "finite ((RAG (wq s))\<^sup>+)" |
|
2817 apply (unfold finite_trancl) |
|
2818 by (auto simp: s_RAG_def cs_RAG_def wq_def) |
|
2819 thus ?thesis by auto |
|
2820 qed |
|
2821 ultimately show ?thesis by (auto intro:finite_subset) |
|
2822 qed |
|
2823 thus ?thesis by (simp add:cs_dependants_def) |
|
2824 qed |
|
2825 thus ?thesis by simp |
|
2826 qed |
|
2827 thus ?thesis by auto |
|
2828 qed |
|
2829 moreover have h2: "(?f ` ?A) \<noteq> {}" |
|
2830 proof - |
|
2831 have "?A \<noteq> {}" by simp |
|
2832 thus ?thesis by simp |
|
2833 qed |
|
2834 from Max_in [OF h1 h2] |
|
2835 have "Max (?f ` ?A) \<in> (?f ` ?A)" . |
|
2836 thus ?thesis |
|
2837 thm cpreced_def |
|
2838 unfolding cpreced_def[symmetric] |
|
2839 unfolding cp_eq_cpreced[symmetric] |
|
2840 unfolding cpreced_def |
|
2841 using that[intro] by (auto) |
|
2842 qed |
|
2843 obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)" |
|
2844 proof - |
|
2845 have h1: "finite (?f ` ?B)" |
|
2846 proof - |
|
2847 have "finite ?B" |
|
2848 proof - |
|
2849 have "finite (dependants (wq s) th2)" |
|
2850 proof- |
|
2851 have "finite {th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+}" |
|
2852 proof - |
|
2853 let ?F = "\<lambda> (x, y). the_th x" |
|
2854 have "{th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)" |
|
2855 apply (auto simp:image_def) |
|
2856 by (rule_tac x = "(Th x, Th th2)" in bexI, auto) |
|
2857 moreover have "finite \<dots>" |
|
2858 proof - |
|
2859 from finite_RAG have "finite (RAG s)" . |
|
2860 hence "finite ((RAG (wq s))\<^sup>+)" |
|
2861 apply (unfold finite_trancl) |
|
2862 by (auto simp: s_RAG_def cs_RAG_def wq_def) |
|
2863 thus ?thesis by auto |
|
2864 qed |
|
2865 ultimately show ?thesis by (auto intro:finite_subset) |
|
2866 qed |
|
2867 thus ?thesis by (simp add:cs_dependants_def) |
|
2868 qed |
|
2869 thus ?thesis by simp |
|
2870 qed |
|
2871 thus ?thesis by auto |
|
2872 qed |
|
2873 moreover have h2: "(?f ` ?B) \<noteq> {}" |
|
2874 proof - |
|
2875 have "?B \<noteq> {}" by simp |
|
2876 thus ?thesis by simp |
|
2877 qed |
|
2878 from Max_in [OF h1 h2] |
|
2879 have "Max (?f ` ?B) \<in> (?f ` ?B)" . |
|
2880 thus ?thesis by (auto intro:that) |
|
2881 qed |
|
2882 from eq_f_th1 eq_f_th2 eq_max |
|
2883 have eq_preced: "preced th1' s = preced th2' s" by auto |
|
2884 hence eq_th12: "th1' = th2'" |
|
2885 proof (rule preced_unique) |
|
2886 from th1_in have "th1' = th1 \<or> (th1' \<in> dependants (wq s) th1)" by simp |
|
2887 thus "th1' \<in> threads s" |
|
2888 proof |
|
2889 assume "th1' \<in> dependants (wq s) th1" |
|
2890 hence "(Th th1') \<in> Domain ((RAG s)^+)" |
|
2891 apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) |
|
2892 by (auto simp:Domain_def) |
|
2893 hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain) |
|
2894 from dm_RAG_threads[OF this] show ?thesis . |
|
2895 next |
|
2896 assume "th1' = th1" |
|
2897 with runing_1 show ?thesis |
|
2898 by (unfold runing_def readys_def, auto) |
|
2899 qed |
|
2900 next |
|
2901 from th2_in have "th2' = th2 \<or> (th2' \<in> dependants (wq s) th2)" by simp |
|
2902 thus "th2' \<in> threads s" |
|
2903 proof |
|
2904 assume "th2' \<in> dependants (wq s) th2" |
|
2905 hence "(Th th2') \<in> Domain ((RAG s)^+)" |
|
2906 apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) |
|
2907 by (auto simp:Domain_def) |
|
2908 hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain) |
|
2909 from dm_RAG_threads[OF this] show ?thesis . |
|
2910 next |
|
2911 assume "th2' = th2" |
|
2912 with runing_2 show ?thesis |
|
2913 by (unfold runing_def readys_def, auto) |
|
2914 qed |
|
2915 qed |
|
2916 from th1_in have "th1' = th1 \<or> th1' \<in> dependants (wq s) th1" by simp |
|
2917 thus ?thesis |
|
2918 proof |
|
2919 assume eq_th': "th1' = th1" |
|
2920 from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp |
|
2921 thus ?thesis |
|
2922 proof |
|
2923 assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp |
|
2924 next |
|
2925 assume "th2' \<in> dependants (wq s) th2" |
|
2926 with eq_th12 eq_th' have "th1 \<in> dependants (wq s) th2" by simp |
|
2927 hence "(Th th1, Th th2) \<in> (RAG s)^+" |
|
2928 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) |
|
2929 hence "Th th1 \<in> Domain ((RAG s)^+)" |
|
2930 apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) |
|
2931 by (auto simp:Domain_def) |
|
2932 hence "Th th1 \<in> Domain (RAG s)" by (simp add:trancl_domain) |
|
2933 then obtain n where d: "(Th th1, n) \<in> RAG s" by (auto simp:Domain_def) |
|
2934 from RAG_target_th [OF this] |
|
2935 obtain cs' where "n = Cs cs'" by auto |
|
2936 with d have "(Th th1, Cs cs') \<in> RAG s" by simp |
|
2937 with runing_1 have "False" |
|
2938 apply (unfold runing_def readys_def s_RAG_def) |
|
2939 by (auto simp:waiting_eq) |
|
2940 thus ?thesis by simp |
|
2941 qed |
|
2942 next |
|
2943 assume th1'_in: "th1' \<in> dependants (wq s) th1" |
|
2944 from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp |
|
2945 thus ?thesis |
|
2946 proof |
|
2947 assume "th2' = th2" |
|
2948 with th1'_in eq_th12 have "th2 \<in> dependants (wq s) th1" by simp |
|
2949 hence "(Th th2, Th th1) \<in> (RAG s)^+" |
|
2950 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) |
|
2951 hence "Th th2 \<in> Domain ((RAG s)^+)" |
|
2952 apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) |
|
2953 by (auto simp:Domain_def) |
|
2954 hence "Th th2 \<in> Domain (RAG s)" by (simp add:trancl_domain) |
|
2955 then obtain n where d: "(Th th2, n) \<in> RAG s" by (auto simp:Domain_def) |
|
2956 from RAG_target_th [OF this] |
|
2957 obtain cs' where "n = Cs cs'" by auto |
|
2958 with d have "(Th th2, Cs cs') \<in> RAG s" by simp |
|
2959 with runing_2 have "False" |
|
2960 apply (unfold runing_def readys_def s_RAG_def) |
|
2961 by (auto simp:waiting_eq) |
|
2962 thus ?thesis by simp |
|
2963 next |
|
2964 assume "th2' \<in> dependants (wq s) th2" |
|
2965 with eq_th12 have "th1' \<in> dependants (wq s) th2" by simp |
|
2966 hence h1: "(Th th1', Th th2) \<in> (RAG s)^+" |
|
2967 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) |
|
2968 from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+" |
|
2969 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) |
|
2970 show ?thesis |
|
2971 proof(rule dchain_unique[OF h1 _ h2, symmetric]) |
|
2972 from runing_1 show "th1 \<in> readys s" by (simp add:runing_def) |
|
2973 from runing_2 show "th2 \<in> readys s" by (simp add:runing_def) |
|
2974 qed |
|
2975 qed |
|
2976 qed |
|
2977 qed |
|
2978 |
|
2979 |
|
2980 lemma "card (runing s) \<le> 1" |
|
2981 apply(subgoal_tac "finite (runing s)") |
|
2982 prefer 2 |
|
2983 apply (metis finite_nat_set_iff_bounded lessI runing_unique) |
|
2984 apply(rule ccontr) |
|
2985 apply(simp) |
|
2986 apply(case_tac "Suc (Suc 0) \<le> card (runing s)") |
|
2987 apply(subst (asm) card_le_Suc_iff) |
|
2988 apply(simp) |
|
2989 apply(auto)[1] |
|
2990 apply (metis insertCI runing_unique) |
|
2991 apply(auto) |
|
2992 done |
|
2993 |
|
2994 end |
|
2995 |
|
2996 |
|
2997 lemma create_pre: |
|
2998 assumes stp: "step s e" |
|
2999 and not_in: "th \<notin> threads s" |
|
3000 and is_in: "th \<in> threads (e#s)" |
|
3001 obtains prio where "e = Create th prio" |
|
3002 proof - |
|
3003 from assms |
|
3004 show ?thesis |
|
3005 proof(cases) |
|
3006 case (thread_create thread prio) |
|
3007 with is_in not_in have "e = Create th prio" by simp |
|
3008 from that[OF this] show ?thesis . |
|
3009 next |
|
3010 case (thread_exit thread) |
|
3011 with assms show ?thesis by (auto intro!:that) |
|
3012 next |
|
3013 case (thread_P thread) |
|
3014 with assms show ?thesis by (auto intro!:that) |
|
3015 next |
|
3016 case (thread_V thread) |
|
3017 with assms show ?thesis by (auto intro!:that) |
|
3018 next |
|
3019 case (thread_set thread) |
|
3020 with assms show ?thesis by (auto intro!:that) |
|
3021 qed |
|
3022 qed |
|
3023 |
|
3024 context valid_trace |
|
3025 begin |
|
3026 |
|
3027 lemma cnp_cnv_eq: |
|
3028 assumes "th \<notin> threads s" |
|
3029 shows "cntP s th = cntV s th" |
|
3030 using assms |
|
3031 using cnp_cnv_cncs not_thread_cncs by auto |
|
3032 |
|
3033 end |
|
3034 |
|
3035 |
|
3036 lemma eq_RAG: |
|
3037 "RAG (wq s) = RAG s" |
|
3038 by (unfold cs_RAG_def s_RAG_def, auto) |
|
3039 |
|
3040 context valid_trace |
|
3041 begin |
|
3042 |
|
3043 lemma count_eq_dependants: |
|
3044 assumes eq_pv: "cntP s th = cntV s th" |
|
3045 shows "dependants (wq s) th = {}" |
|
3046 proof - |
|
3047 from cnp_cnv_cncs and eq_pv |
|
3048 have "cntCS s th = 0" |
|
3049 by (auto split:if_splits) |
|
3050 moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}" |
|
3051 proof - |
|
3052 from finite_holding[of th] show ?thesis |
|
3053 by (simp add:holdents_test) |
|
3054 qed |
|
3055 ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}" |
|
3056 by (unfold cntCS_def holdents_test cs_dependants_def, auto) |
|
3057 show ?thesis |
|
3058 proof(unfold cs_dependants_def) |
|
3059 { assume "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" |
|
3060 then obtain th' where "(Th th', Th th) \<in> (RAG (wq s))\<^sup>+" by auto |
|
3061 hence "False" |
|
3062 proof(cases) |
|
3063 assume "(Th th', Th th) \<in> RAG (wq s)" |
|
3064 thus "False" by (auto simp:cs_RAG_def) |
|
3065 next |
|
3066 fix c |
|
3067 assume "(c, Th th) \<in> RAG (wq s)" |
|
3068 with h and eq_RAG show "False" |
|
3069 by (cases c, auto simp:cs_RAG_def) |
|
3070 qed |
|
3071 } thus "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} = {}" by auto |
|
3072 qed |
|
3073 qed |
|
3074 |
|
3075 lemma dependants_threads: |
|
3076 shows "dependants (wq s) th \<subseteq> threads s" |
|
3077 proof |
|
3078 { fix th th' |
|
3079 assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (RAG (wq s))\<^sup>+}" |
|
3080 have "Th th \<in> Domain (RAG s)" |
|
3081 proof - |
|
3082 from h obtain th' where "(Th th, Th th') \<in> (RAG (wq s))\<^sup>+" by auto |
|
3083 hence "(Th th) \<in> Domain ( (RAG (wq s))\<^sup>+)" by (auto simp:Domain_def) |
|
3084 with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp |
|
3085 thus ?thesis using eq_RAG by simp |
|
3086 qed |
|
3087 from dm_RAG_threads[OF this] |
|
3088 have "th \<in> threads s" . |
|
3089 } note hh = this |
|
3090 fix th1 |
|
3091 assume "th1 \<in> dependants (wq s) th" |
|
3092 hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (RAG (wq s))\<^sup>+}" |
|
3093 by (unfold cs_dependants_def, simp) |
|
3094 from hh [OF this] show "th1 \<in> threads s" . |
|
3095 qed |
|
3096 |
|
3097 lemma finite_threads: |
|
3098 shows "finite (threads s)" |
|
3099 using vt by (induct) (auto elim: step.cases) |
|
3100 |
|
3101 end |
|
3102 |
|
3103 lemma Max_f_mono: |
|
3104 assumes seq: "A \<subseteq> B" |
|
3105 and np: "A \<noteq> {}" |
|
3106 and fnt: "finite B" |
|
3107 shows "Max (f ` A) \<le> Max (f ` B)" |
|
3108 proof(rule Max_mono) |
|
3109 from seq show "f ` A \<subseteq> f ` B" by auto |
|
3110 next |
|
3111 from np show "f ` A \<noteq> {}" by auto |
|
3112 next |
|
3113 from fnt and seq show "finite (f ` B)" by auto |
|
3114 qed |
|
3115 |
|
3116 context valid_trace |
|
3117 begin |
|
3118 |
|
3119 lemma cp_le: |
|
3120 assumes th_in: "th \<in> threads s" |
1384 assumes th_in: "th \<in> threads s" |
3121 shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)" |
1385 shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)" |
3122 proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) |
1386 proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) |
3123 show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+})) |
1387 show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+})) |
3124 \<le> Max ((\<lambda>th. preced th s) ` threads s)" |
1388 \<le> Max ((\<lambda>th. preced th s) ` threads s)" |
3223 ultimately show ?thesis by auto |
1447 ultimately show ?thesis by auto |
3224 qed |
1448 qed |
3225 ultimately show ?thesis using eq_l by auto |
1449 ultimately show ?thesis using eq_l by auto |
3226 qed |
1450 qed |
3227 |
1451 |
3228 lemma max_cp_readys_threads_pre: |
1452 lemma max_cp_eq_the_preced: |
3229 assumes np: "threads s \<noteq> {}" |
1453 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" |
3230 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" |
1454 using max_cp_eq using the_preced_def by presburger |
3231 proof(unfold max_cp_eq) |
1455 |
3232 show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)" |
1456 end |
3233 proof - |
1457 |
3234 let ?p = "Max ((\<lambda>th. preced th s) ` threads s)" |
1458 lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s" |
3235 let ?f = "(\<lambda>th. preced th s)" |
1459 by (unfold preced_def, simp) |
3236 have "?p \<in> ((\<lambda>th. preced th s) ` threads s)" |
1460 |
3237 proof(rule Max_in) |
1461 lemma (in valid_trace_v) |
3238 from finite_threads show "finite (?f ` threads s)" by simp |
1462 preced_es: "preced th (e#s) = preced th s" |
3239 next |
1463 by (unfold is_v preced_def, simp) |
3240 from np show "?f ` threads s \<noteq> {}" by simp |
1464 |
3241 qed |
1465 lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s" |
3242 then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s" |
1466 proof |
3243 by (auto simp:Image_def) |
1467 fix th' |
3244 from th_chain_to_ready [OF tm_in] |
1468 show "the_preced (V th cs # s) th' = the_preced s th'" |
3245 have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" . |
1469 by (unfold the_preced_def preced_def, simp) |
3246 thus ?thesis |
1470 qed |
3247 proof |
1471 |
3248 assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+ " |
1472 lemma (in valid_trace_v) |
3249 then obtain th' where th'_in: "th' \<in> readys s" |
1473 the_preced_es: "the_preced (e#s) = the_preced s" |
3250 and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto |
1474 by (unfold is_v preced_def, simp) |
3251 have "cp s th' = ?f tm" |
1475 |
3252 proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) |
1476 context valid_trace_p |
3253 from dependants_threads finite_threads |
1477 begin |
3254 show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))" |
1478 |
3255 by (auto intro:finite_subset) |
1479 lemma not_holding_es_th_cs: "\<not> holding s th cs" |
3256 next |
1480 proof |
3257 fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')" |
1481 assume otherwise: "holding s th cs" |
3258 from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" . |
1482 from pip_e[unfolded is_p] |
3259 moreover have "p \<le> \<dots>" |
1483 show False |
3260 proof(rule Max_ge) |
1484 proof(cases) |
3261 from finite_threads |
1485 case (thread_P) |
3262 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp |
1486 moreover have "(Cs cs, Th th) \<in> RAG s" |
3263 next |
1487 using otherwise cs_holding_def |
3264 from p_in and th'_in and dependants_threads[of th'] |
1488 holding_eq th_not_in_wq by auto |
3265 show "p \<in> (\<lambda>th. preced th s) ` threads s" |
1489 ultimately show ?thesis by auto |
3266 by (auto simp:readys_def) |
1490 qed |
3267 qed |
1491 qed |
3268 ultimately show "p \<le> preced tm s" by auto |
1492 |
3269 next |
1493 end |
3270 show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')" |
1494 |
3271 proof - |
1495 locale valid_trace_p_h = valid_trace_p + |
3272 from tm_chain |
1496 assumes we: "wq s cs = []" |
3273 have "tm \<in> dependants (wq s) th'" |
1497 |
3274 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto) |
1498 locale valid_trace_p_w = valid_trace_p + |
3275 thus ?thesis by auto |
1499 assumes we: "wq s cs \<noteq> []" |
3276 qed |
1500 begin |
3277 qed |
1501 |
3278 with tm_max |
1502 definition "holder = hd (wq s cs)" |
3279 have h: "cp s th' = Max ((\<lambda>th. preced th s) ` threads s)" by simp |
1503 definition "waiters = tl (wq s cs)" |
3280 show ?thesis |
1504 definition "waiters' = waiters @ [th]" |
3281 proof (fold h, rule Max_eqI) |
1505 |
3282 fix q |
1506 lemma wq_s_cs: "wq s cs = holder#waiters" |
3283 assume "q \<in> cp s ` readys s" |
1507 by (simp add: holder_def waiters_def we) |
3284 then obtain th1 where th1_in: "th1 \<in> readys s" |
1508 |
3285 and eq_q: "q = cp s th1" by auto |
1509 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]" |
3286 show "q \<le> cp s th'" |
1510 by (simp add: wq_es_cs wq_s_cs) |
3287 apply (unfold h eq_q) |
1511 |
3288 apply (unfold cp_eq_cpreced cpreced_def) |
1512 lemma waiting_es_th_cs: "waiting (e#s) th cs" |
3289 apply (rule Max_mono) |
1513 using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto |
3290 proof - |
1514 |
3291 from dependants_threads [of th1] th1_in |
1515 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)" |
3292 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq> |
1516 by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) |
3293 (\<lambda>th. preced th s) ` threads s" |
1517 |
3294 by (auto simp:readys_def) |
1518 end |
3295 next |
1519 |
3296 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp |
1520 context valid_trace_p_h |
3297 next |
1521 begin |
3298 from finite_threads |
1522 |
3299 show " finite ((\<lambda>th. preced th s) ` threads s)" by simp |
1523 lemma wq_es_cs': "wq (e#s) cs = [th]" |
3300 qed |
1524 using wq_es_cs[unfolded we] by simp |
3301 next |
1525 |
3302 from finite_threads |
1526 lemma holding_es_th_cs: |
3303 show "finite (cp s ` readys s)" by (auto simp:readys_def) |
1527 shows "holding (e#s) th cs" |
3304 next |
1528 proof - |
3305 from th'_in |
1529 from wq_es_cs' |
3306 show "cp s th' \<in> cp s ` readys s" by simp |
1530 have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto |
3307 qed |
1531 thus ?thesis using cs_holding_def holding_eq by blast |
3308 next |
1532 qed |
3309 assume tm_ready: "tm \<in> readys s" |
1533 |
3310 show ?thesis |
1534 lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)" |
3311 proof(fold tm_max) |
1535 by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto) |
3312 have cp_eq_p: "cp s tm = preced tm s" |
1536 |
3313 proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) |
1537 lemma waiting_esE: |
3314 fix y |
1538 assumes "waiting (e#s) th' cs'" |
3315 assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)" |
1539 obtains "waiting s th' cs'" |
3316 show "y \<le> preced tm s" |
1540 using assms |
3317 proof - |
1541 by (metis cs_waiting_def event.distinct(15) is_p list.sel(1) |
3318 { fix y' |
1542 set_ConsD waiting_eq we wq_es_cs' wq_neq_simp wq_out_inv) |
3319 assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)" |
1543 |
3320 have "y' \<le> preced tm s" |
1544 lemma holding_esE: |
3321 proof(unfold tm_max, rule Max_ge) |
1545 assumes "holding (e#s) th' cs'" |
3322 from hy' dependants_threads[of tm] |
1546 obtains "cs' \<noteq> cs" "holding s th' cs'" |
3323 show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto |
1547 | "cs' = cs" "th' = th" |
3324 next |
1548 proof(cases "cs' = cs") |
3325 from finite_threads |
|
3326 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp |
|
3327 qed |
|
3328 } with hy show ?thesis by auto |
|
3329 qed |
|
3330 next |
|
3331 from dependants_threads[of tm] finite_threads |
|
3332 show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))" |
|
3333 by (auto intro:finite_subset) |
|
3334 next |
|
3335 show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)" |
|
3336 by simp |
|
3337 qed |
|
3338 moreover have "Max (cp s ` readys s) = cp s tm" |
|
3339 proof(rule Max_eqI) |
|
3340 from tm_ready show "cp s tm \<in> cp s ` readys s" by simp |
|
3341 next |
|
3342 from finite_threads |
|
3343 show "finite (cp s ` readys s)" by (auto simp:readys_def) |
|
3344 next |
|
3345 fix y assume "y \<in> cp s ` readys s" |
|
3346 then obtain th1 where th1_readys: "th1 \<in> readys s" |
|
3347 and h: "y = cp s th1" by auto |
|
3348 show "y \<le> cp s tm" |
|
3349 apply(unfold cp_eq_p h) |
|
3350 apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) |
|
3351 proof - |
|
3352 from finite_threads |
|
3353 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp |
|
3354 next |
|
3355 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" |
|
3356 by simp |
|
3357 next |
|
3358 from dependants_threads[of th1] th1_readys |
|
3359 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) |
|
3360 \<subseteq> (\<lambda>th. preced th s) ` threads s" |
|
3361 by (auto simp:readys_def) |
|
3362 qed |
|
3363 qed |
|
3364 ultimately show " Max (cp s ` readys s) = preced tm s" by simp |
|
3365 qed |
|
3366 qed |
|
3367 qed |
|
3368 qed |
|
3369 |
|
3370 text {* (* ccc *) \noindent |
|
3371 Since the current precedence of the threads in ready queue will always be boosted, |
|
3372 there must be one inside it has the maximum precedence of the whole system. |
|
3373 *} |
|
3374 lemma max_cp_readys_threads: |
|
3375 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" |
|
3376 proof(cases "threads s = {}") |
|
3377 case True |
1549 case True |
3378 thus ?thesis |
1550 from held_unique[OF holding_es_th_cs assms[unfolded True]] |
3379 by (auto simp:readys_def) |
1551 have "th' = th" by simp |
|
1552 from that(2)[OF True this] show ?thesis . |
3380 next |
1553 next |
3381 case False |
1554 case False |
3382 show ?thesis by (rule max_cp_readys_threads_pre[OF False]) |
1555 have "holding s th' cs'" using assms |
3383 qed |
1556 using False cs_holding_def holding_eq by auto |
3384 |
1557 from that(1)[OF False this] show ?thesis . |
3385 end |
1558 qed |
3386 |
1559 |
3387 lemma eq_holding: "holding (wq s) th cs = holding s th cs" |
1560 lemma waiting_kept: |
3388 apply (unfold s_holding_def cs_holding_def wq_def, simp) |
1561 assumes "waiting s th' cs'" |
3389 done |
1562 shows "waiting (e#s) th' cs'" |
3390 |
1563 using assms |
3391 lemma f_image_eq: |
1564 by (metis cs_waiting_def list.sel(1) list.set_intros(2) |
3392 assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a" |
1565 th_not_in_wq waiting_eq we wq_es_cs' wq_neq_simp) |
3393 shows "f ` A = g ` A" |
1566 |
3394 proof |
1567 |
3395 show "f ` A \<subseteq> g ` A" |
1568 lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R") |
3396 by(rule image_subsetI, auto intro:h) |
1569 proof(rule rel_eqI) |
3397 next |
1570 fix n1 n2 |
3398 show "g ` A \<subseteq> f ` A" |
1571 assume "(n1, n2) \<in> ?L" |
3399 by (rule image_subsetI, auto intro:h[symmetric]) |
1572 thus "(n1, n2) \<in> ?R" |
3400 qed |
1573 proof(cases rule:in_RAG_E) |
3401 |
1574 case (waiting th' cs') |
3402 |
1575 from this(3) |
3403 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
|
3404 where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))" |
|
3405 |
|
3406 lemma detached_test: |
|
3407 shows "detached s th = (Th th \<notin> Field (RAG s))" |
|
3408 apply(simp add: detached_def Field_def) |
|
3409 apply(simp add: s_RAG_def) |
|
3410 apply(simp add: s_holding_abv s_waiting_abv) |
|
3411 apply(simp add: Domain_iff Range_iff) |
|
3412 apply(simp add: wq_def) |
|
3413 apply(auto) |
|
3414 done |
|
3415 |
|
3416 context valid_trace |
|
3417 begin |
|
3418 |
|
3419 lemma detached_intro: |
|
3420 assumes eq_pv: "cntP s th = cntV s th" |
|
3421 shows "detached s th" |
|
3422 proof - |
|
3423 from cnp_cnv_cncs |
|
3424 have eq_cnt: "cntP s th = |
|
3425 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . |
|
3426 hence cncs_zero: "cntCS s th = 0" |
|
3427 by (auto simp:eq_pv split:if_splits) |
|
3428 with eq_cnt |
|
3429 have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:eq_pv) |
|
3430 thus ?thesis |
|
3431 proof |
|
3432 assume "th \<notin> threads s" |
|
3433 with range_in dm_RAG_threads |
|
3434 show ?thesis |
1576 show ?thesis |
3435 by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) |
1577 proof(cases rule:waiting_esE) |
3436 next |
1578 case 1 |
3437 assume "th \<in> readys s" |
1579 thus ?thesis using waiting(1,2) |
3438 moreover have "Th th \<notin> Range (RAG s)" |
1580 by (unfold s_RAG_def, fold waiting_eq, auto) |
3439 proof - |
|
3440 from card_0_eq [OF finite_holding] and cncs_zero |
|
3441 have "holdents s th = {}" |
|
3442 by (simp add:cntCS_def) |
|
3443 thus ?thesis |
|
3444 apply(auto simp:holdents_test) |
|
3445 apply(case_tac a) |
|
3446 apply(auto simp:holdents_test s_RAG_def) |
|
3447 done |
|
3448 qed |
1581 qed |
3449 ultimately show ?thesis |
1582 next |
3450 by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def readys_def) |
1583 case (holding th' cs') |
3451 qed |
1584 from this(3) |
3452 qed |
1585 show ?thesis |
3453 |
1586 proof(cases rule:holding_esE) |
3454 lemma detached_elim: |
|
3455 assumes dtc: "detached s th" |
|
3456 shows "cntP s th = cntV s th" |
|
3457 proof - |
|
3458 from cnp_cnv_cncs |
|
3459 have eq_pv: " cntP s th = |
|
3460 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . |
|
3461 have cncs_z: "cntCS s th = 0" |
|
3462 proof - |
|
3463 from dtc have "holdents s th = {}" |
|
3464 unfolding detached_def holdents_test s_RAG_def |
|
3465 by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) |
|
3466 thus ?thesis by (auto simp:cntCS_def) |
|
3467 qed |
|
3468 show ?thesis |
|
3469 proof(cases "th \<in> threads s") |
|
3470 case True |
|
3471 with dtc |
|
3472 have "th \<in> readys s" |
|
3473 by (unfold readys_def detached_def Field_def Domain_def Range_def, |
|
3474 auto simp:waiting_eq s_RAG_def) |
|
3475 with cncs_z and eq_pv show ?thesis by simp |
|
3476 next |
|
3477 case False |
|
3478 with cncs_z and eq_pv show ?thesis by simp |
|
3479 qed |
|
3480 qed |
|
3481 |
|
3482 lemma detached_eq: |
|
3483 shows "(detached s th) = (cntP s th = cntV s th)" |
|
3484 by (insert vt, auto intro:detached_intro detached_elim) |
|
3485 |
|
3486 end |
|
3487 |
|
3488 text {* |
|
3489 The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived |
|
3490 from the concise and miniature model of PIP given in PrioGDef.thy. |
|
3491 *} |
|
3492 |
|
3493 lemma eq_dependants: "dependants (wq s) = dependants s" |
|
3494 by (simp add: s_dependants_abv wq_def) |
|
3495 |
|
3496 lemma next_th_unique: |
|
3497 assumes nt1: "next_th s th cs th1" |
|
3498 and nt2: "next_th s th cs th2" |
|
3499 shows "th1 = th2" |
|
3500 using assms by (unfold next_th_def, auto) |
|
3501 |
|
3502 lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s" |
|
3503 apply (induct s, simp) |
|
3504 proof - |
|
3505 fix a s |
|
3506 assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s" |
|
3507 and eq_as: "a # s \<noteq> []" |
|
3508 show "last_set th (a # s) < length (a # s)" |
|
3509 proof(cases "s \<noteq> []") |
|
3510 case False |
|
3511 from False show ?thesis |
|
3512 by (cases a, auto simp:last_set.simps) |
|
3513 next |
|
3514 case True |
|
3515 from ih [OF True] show ?thesis |
|
3516 by (cases a, auto simp:last_set.simps) |
|
3517 qed |
|
3518 qed |
|
3519 |
|
3520 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []" |
|
3521 by (induct s, auto simp:threads.simps) |
|
3522 |
|
3523 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s" |
|
3524 apply (drule_tac th_in_ne) |
|
3525 by (unfold preced_def, auto intro: birth_time_lt) |
|
3526 |
|
3527 lemma inj_the_preced: |
|
3528 "inj_on (the_preced s) (threads s)" |
|
3529 by (metis inj_onI preced_unique the_preced_def) |
|
3530 |
|
3531 lemma tRAG_alt_def: |
|
3532 "tRAG s = {(Th th1, Th th2) | th1 th2. |
|
3533 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" |
|
3534 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
|
3535 |
|
3536 lemma tRAG_Field: |
|
3537 "Field (tRAG s) \<subseteq> Field (RAG s)" |
|
3538 by (unfold tRAG_alt_def Field_def, auto) |
|
3539 |
|
3540 lemma tRAG_ancestorsE: |
|
3541 assumes "x \<in> ancestors (tRAG s) u" |
|
3542 obtains th where "x = Th th" |
|
3543 proof - |
|
3544 from assms have "(u, x) \<in> (tRAG s)^+" |
|
3545 by (unfold ancestors_def, auto) |
|
3546 from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto |
|
3547 then obtain th where "x = Th th" |
|
3548 by (unfold tRAG_alt_def, auto) |
|
3549 from that[OF this] show ?thesis . |
|
3550 qed |
|
3551 |
|
3552 lemma tRAG_mono: |
|
3553 assumes "RAG s' \<subseteq> RAG s" |
|
3554 shows "tRAG s' \<subseteq> tRAG s" |
|
3555 using assms |
|
3556 by (unfold tRAG_alt_def, auto) |
|
3557 |
|
3558 lemma holding_next_thI: |
|
3559 assumes "holding s th cs" |
|
3560 and "length (wq s cs) > 1" |
|
3561 obtains th' where "next_th s th cs th'" |
|
3562 proof - |
|
3563 from assms(1)[folded eq_holding, unfolded cs_holding_def] |
|
3564 have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" . |
|
3565 then obtain rest where h1: "wq s cs = th#rest" |
|
3566 by (cases "wq s cs", auto) |
|
3567 with assms(2) have h2: "rest \<noteq> []" by auto |
|
3568 let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" |
|
3569 have "next_th s th cs ?th'" using h1(1) h2 |
|
3570 by (unfold next_th_def, auto) |
|
3571 from that[OF this] show ?thesis . |
|
3572 qed |
|
3573 |
|
3574 lemma RAG_tRAG_transfer: |
|
3575 assumes "vt s'" |
|
3576 assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
|
3577 and "(Cs cs, Th th'') \<in> RAG s'" |
|
3578 shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R") |
|
3579 proof - |
|
3580 interpret vt_s': valid_trace "s'" using assms(1) |
|
3581 by (unfold_locales, simp) |
|
3582 interpret rtree: rtree "RAG s'" |
|
3583 proof |
|
3584 show "single_valued (RAG s')" |
|
3585 apply (intro_locales) |
|
3586 by (unfold single_valued_def, |
|
3587 auto intro:vt_s'.unique_RAG) |
|
3588 |
|
3589 show "acyclic (RAG s')" |
|
3590 by (rule vt_s'.acyclic_RAG) |
|
3591 qed |
|
3592 { fix n1 n2 |
|
3593 assume "(n1, n2) \<in> ?L" |
|
3594 from this[unfolded tRAG_alt_def] |
|
3595 obtain th1 th2 cs' where |
|
3596 h: "n1 = Th th1" "n2 = Th th2" |
|
3597 "(Th th1, Cs cs') \<in> RAG s" |
|
3598 "(Cs cs', Th th2) \<in> RAG s" by auto |
|
3599 from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto |
|
3600 from h(3) and assms(2) |
|
3601 have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> |
|
3602 (Th th1, Cs cs') \<in> RAG s'" by auto |
|
3603 hence "(n1, n2) \<in> ?R" |
|
3604 proof |
|
3605 assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" |
|
3606 hence eq_th1: "th1 = th" by simp |
|
3607 moreover have "th2 = th''" |
|
3608 proof - |
|
3609 from h1 have "cs' = cs" by simp |
|
3610 from assms(3) cs_in[unfolded this] rtree.sgv |
|
3611 show ?thesis |
|
3612 by (unfold single_valued_def, auto) |
|
3613 qed |
|
3614 ultimately show ?thesis using h(1,2) by auto |
|
3615 next |
|
3616 assume "(Th th1, Cs cs') \<in> RAG s'" |
|
3617 with cs_in have "(Th th1, Th th2) \<in> tRAG s'" |
|
3618 by (unfold tRAG_alt_def, auto) |
|
3619 from this[folded h(1, 2)] show ?thesis by auto |
|
3620 qed |
|
3621 } moreover { |
|
3622 fix n1 n2 |
|
3623 assume "(n1, n2) \<in> ?R" |
|
3624 hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto |
|
3625 hence "(n1, n2) \<in> ?L" |
|
3626 proof |
|
3627 assume "(n1, n2) \<in> tRAG s'" |
|
3628 moreover have "... \<subseteq> ?L" |
|
3629 proof(rule tRAG_mono) |
|
3630 show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto) |
|
3631 qed |
|
3632 ultimately show ?thesis by auto |
|
3633 next |
|
3634 assume eq_n: "(n1, n2) = (Th th, Th th'')" |
|
3635 from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto |
|
3636 moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto |
|
3637 ultimately show ?thesis |
|
3638 by (unfold eq_n tRAG_alt_def, auto) |
|
3639 qed |
|
3640 } ultimately show ?thesis by auto |
|
3641 qed |
|
3642 |
|
3643 context valid_trace |
|
3644 begin |
|
3645 |
|
3646 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] |
|
3647 |
|
3648 end |
|
3649 |
|
3650 lemma cp_alt_def: |
|
3651 "cp s th = |
|
3652 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
|
3653 proof - |
|
3654 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = |
|
3655 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
3656 (is "Max (_ ` ?L) = Max (_ ` ?R)") |
|
3657 proof - |
|
3658 have "?L = ?R" |
|
3659 by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def) |
|
3660 thus ?thesis by simp |
|
3661 qed |
|
3662 thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) |
|
3663 qed |
|
3664 |
|
3665 lemma cp_gen_alt_def: |
|
3666 "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" |
|
3667 by (auto simp:cp_gen_def) |
|
3668 |
|
3669 lemma tRAG_nodeE: |
|
3670 assumes "(n1, n2) \<in> tRAG s" |
|
3671 obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" |
|
3672 using assms |
|
3673 by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) |
|
3674 |
|
3675 lemma subtree_nodeE: |
|
3676 assumes "n \<in> subtree (tRAG s) (Th th)" |
|
3677 obtains th1 where "n = Th th1" |
|
3678 proof - |
|
3679 show ?thesis |
|
3680 proof(rule subtreeE[OF assms]) |
|
3681 assume "n = Th th" |
|
3682 from that[OF this] show ?thesis . |
|
3683 next |
|
3684 assume "Th th \<in> ancestors (tRAG s) n" |
|
3685 hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
|
3686 hence "\<exists> th1. n = Th th1" |
|
3687 proof(induct) |
|
3688 case (base y) |
|
3689 from tRAG_nodeE[OF this] show ?case by metis |
|
3690 next |
|
3691 case (step y z) |
|
3692 thus ?case by auto |
|
3693 qed |
|
3694 with that show ?thesis by auto |
|
3695 qed |
|
3696 qed |
|
3697 |
|
3698 lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*" |
|
3699 proof - |
|
3700 have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" |
|
3701 by (rule rtrancl_mono, auto simp:RAG_split) |
|
3702 also have "... \<subseteq> ((RAG s)^*)^*" |
|
3703 by (rule rtrancl_mono, auto) |
|
3704 also have "... = (RAG s)^*" by simp |
|
3705 finally show ?thesis by (unfold tRAG_def, simp) |
|
3706 qed |
|
3707 |
|
3708 lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x" |
|
3709 proof - |
|
3710 { fix a |
|
3711 assume "a \<in> subtree (tRAG s) x" |
|
3712 hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def) |
|
3713 with tRAG_star_RAG[of s] |
|
3714 have "(a, x) \<in> (RAG s)^*" by auto |
|
3715 hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def) |
|
3716 } thus ?thesis by auto |
|
3717 qed |
|
3718 |
|
3719 lemma tRAG_trancl_eq: |
|
3720 "{th'. (Th th', Th th) \<in> (tRAG s)^+} = |
|
3721 {th'. (Th th', Th th) \<in> (RAG s)^+}" |
|
3722 (is "?L = ?R") |
|
3723 proof - |
|
3724 { fix th' |
|
3725 assume "th' \<in> ?L" |
|
3726 hence "(Th th', Th th) \<in> (tRAG s)^+" by auto |
|
3727 from tranclD[OF this] |
|
3728 obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto |
|
3729 from tRAG_subtree_RAG[of s] and this(2) |
|
3730 have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) |
|
3731 moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto |
|
3732 ultimately have "th' \<in> ?R" by auto |
|
3733 } moreover |
|
3734 { fix th' |
|
3735 assume "th' \<in> ?R" |
|
3736 hence "(Th th', Th th) \<in> (RAG s)^+" by (auto) |
|
3737 from plus_rpath[OF this] |
|
3738 obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto |
|
3739 hence "(Th th', Th th) \<in> (tRAG s)^+" |
|
3740 proof(induct xs arbitrary:th' th rule:length_induct) |
|
3741 case (1 xs th' th) |
|
3742 then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) |
|
3743 show ?case |
|
3744 proof(cases "xs1") |
|
3745 case Nil |
|
3746 from 1(2)[unfolded Cons1 Nil] |
|
3747 have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . |
|
3748 hence "(Th th', x1) \<in> (RAG s)" by (cases, simp) |
|
3749 then obtain cs where "x1 = Cs cs" |
|
3750 by (unfold s_RAG_def, auto) |
|
3751 from rpath_nnl_lastE[OF rp[unfolded this]] |
|
3752 show ?thesis by auto |
|
3753 next |
|
3754 case (Cons x2 xs2) |
|
3755 from 1(2)[unfolded Cons1[unfolded this]] |
|
3756 have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . |
|
3757 from rpath_edges_on[OF this] |
|
3758 have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" . |
|
3759 have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
3760 by (simp add: edges_on_unfold) |
|
3761 with eds have rg1: "(Th th', x1) \<in> RAG s" by auto |
|
3762 then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) |
|
3763 have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
3764 by (simp add: edges_on_unfold) |
|
3765 from this eds |
|
3766 have rg2: "(x1, x2) \<in> RAG s" by auto |
|
3767 from this[unfolded eq_x1] |
|
3768 obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) |
|
3769 from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] |
|
3770 have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto) |
|
3771 from rp have "rpath (RAG s) x2 xs2 (Th th)" |
|
3772 by (elim rpath_ConsE, simp) |
|
3773 from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . |
|
3774 show ?thesis |
|
3775 proof(cases "xs2 = []") |
|
3776 case True |
|
3777 from rpath_nilE[OF rp'[unfolded this]] |
|
3778 have "th1 = th" by auto |
|
3779 from rt1[unfolded this] show ?thesis by auto |
|
3780 next |
|
3781 case False |
|
3782 from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] |
|
3783 have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp |
|
3784 with rt1 show ?thesis by auto |
|
3785 qed |
|
3786 qed |
|
3787 qed |
|
3788 hence "th' \<in> ?L" by auto |
|
3789 } ultimately show ?thesis by blast |
|
3790 qed |
|
3791 |
|
3792 lemma tRAG_trancl_eq_Th: |
|
3793 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
|
3794 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
|
3795 using tRAG_trancl_eq by auto |
|
3796 |
|
3797 lemma dependants_alt_def: |
|
3798 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
|
3799 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
|
3800 |
|
3801 context valid_trace |
|
3802 begin |
|
3803 |
|
3804 lemma count_eq_tRAG_plus: |
|
3805 assumes "cntP s th = cntV s th" |
|
3806 shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
|
3807 using assms count_eq_dependants dependants_alt_def eq_dependants by auto |
|
3808 |
|
3809 lemma count_eq_RAG_plus: |
|
3810 assumes "cntP s th = cntV s th" |
|
3811 shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
|
3812 using assms count_eq_dependants cs_dependants_def eq_RAG by auto |
|
3813 |
|
3814 lemma count_eq_RAG_plus_Th: |
|
3815 assumes "cntP s th = cntV s th" |
|
3816 shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
|
3817 using count_eq_RAG_plus[OF assms] by auto |
|
3818 |
|
3819 lemma count_eq_tRAG_plus_Th: |
|
3820 assumes "cntP s th = cntV s th" |
|
3821 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
|
3822 using count_eq_tRAG_plus[OF assms] by auto |
|
3823 |
|
3824 end |
|
3825 |
|
3826 lemma tRAG_subtree_eq: |
|
3827 "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}" |
|
3828 (is "?L = ?R") |
|
3829 proof - |
|
3830 { fix n |
|
3831 assume h: "n \<in> ?L" |
|
3832 hence "n \<in> ?R" |
|
3833 by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) |
|
3834 } moreover { |
|
3835 fix n |
|
3836 assume "n \<in> ?R" |
|
3837 then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" |
|
3838 by (auto simp:subtree_def) |
|
3839 from rtranclD[OF this(2)] |
|
3840 have "n \<in> ?L" |
|
3841 proof |
|
3842 assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+" |
|
3843 with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto |
|
3844 thus ?thesis using subtree_def tRAG_trancl_eq by fastforce |
|
3845 qed (insert h, auto simp:subtree_def) |
|
3846 } ultimately show ?thesis by auto |
|
3847 qed |
|
3848 |
|
3849 lemma threads_set_eq: |
|
3850 "the_thread ` (subtree (tRAG s) (Th th)) = |
|
3851 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") |
|
3852 by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) |
|
3853 |
|
3854 lemma cp_alt_def1: |
|
3855 "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" |
|
3856 proof - |
|
3857 have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = |
|
3858 ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))" |
|
3859 by auto |
|
3860 thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) |
|
3861 qed |
|
3862 |
|
3863 lemma cp_gen_def_cond: |
|
3864 assumes "x = Th th" |
|
3865 shows "cp s th = cp_gen s (Th th)" |
|
3866 by (unfold cp_alt_def1 cp_gen_def, simp) |
|
3867 |
|
3868 lemma cp_gen_over_set: |
|
3869 assumes "\<forall> x \<in> A. \<exists> th. x = Th th" |
|
3870 shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A" |
|
3871 proof(rule f_image_eq) |
|
3872 fix a |
|
3873 assume "a \<in> A" |
|
3874 from assms[rule_format, OF this] |
|
3875 obtain th where eq_a: "a = Th th" by auto |
|
3876 show "cp_gen s a = (cp s \<circ> the_thread) a" |
|
3877 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
|
3878 qed |
|
3879 |
|
3880 |
|
3881 context valid_trace |
|
3882 begin |
|
3883 |
|
3884 lemma RAG_threads: |
|
3885 assumes "(Th th) \<in> Field (RAG s)" |
|
3886 shows "th \<in> threads s" |
|
3887 using assms |
|
3888 by (metis Field_def UnE dm_RAG_threads range_in vt) |
|
3889 |
|
3890 lemma subtree_tRAG_thread: |
|
3891 assumes "th \<in> threads s" |
|
3892 shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R") |
|
3893 proof - |
|
3894 have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
3895 by (unfold tRAG_subtree_eq, simp) |
|
3896 also have "... \<subseteq> ?R" |
|
3897 proof |
|
3898 fix x |
|
3899 assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
3900 then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto |
|
3901 from this(2) |
|
3902 show "x \<in> ?R" |
|
3903 proof(cases rule:subtreeE) |
|
3904 case 1 |
1587 case 1 |
3905 thus ?thesis by (simp add: assms h(1)) |
1588 with holding(1,2) |
|
1589 show ?thesis by (unfold s_RAG_def, fold holding_eq, auto) |
3906 next |
1590 next |
3907 case 2 |
1591 case 2 |
3908 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) |
1592 with holding(1,2) show ?thesis by auto |
3909 qed |
1593 qed |
3910 qed |
1594 qed |
3911 finally show ?thesis . |
|
3912 qed |
|
3913 |
|
3914 lemma readys_root: |
|
3915 assumes "th \<in> readys s" |
|
3916 shows "root (RAG s) (Th th)" |
|
3917 proof - |
|
3918 { fix x |
|
3919 assume "x \<in> ancestors (RAG s) (Th th)" |
|
3920 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
3921 from tranclD[OF this] |
|
3922 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
3923 with assms(1) have False |
|
3924 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
3925 by (fold wq_def, blast) |
|
3926 } thus ?thesis by (unfold root_def, auto) |
|
3927 qed |
|
3928 |
|
3929 lemma readys_in_no_subtree: |
|
3930 assumes "th \<in> readys s" |
|
3931 and "th' \<noteq> th" |
|
3932 shows "Th th \<notin> subtree (RAG s) (Th th')" |
|
3933 proof |
|
3934 assume "Th th \<in> subtree (RAG s) (Th th')" |
|
3935 thus False |
|
3936 proof(cases rule:subtreeE) |
|
3937 case 1 |
|
3938 with assms show ?thesis by auto |
|
3939 next |
|
3940 case 2 |
|
3941 with readys_root[OF assms(1)] |
|
3942 show ?thesis by (auto simp:root_def) |
|
3943 qed |
|
3944 qed |
|
3945 |
|
3946 lemma not_in_thread_isolated: |
|
3947 assumes "th \<notin> threads s" |
|
3948 shows "(Th th) \<notin> Field (RAG s)" |
|
3949 proof |
|
3950 assume "(Th th) \<in> Field (RAG s)" |
|
3951 with dm_RAG_threads and range_in assms |
|
3952 show False by (unfold Field_def, blast) |
|
3953 qed |
|
3954 |
|
3955 lemma wf_RAG: "wf (RAG s)" |
|
3956 proof(rule finite_acyclic_wf) |
|
3957 from finite_RAG show "finite (RAG s)" . |
|
3958 next |
1595 next |
3959 from acyclic_RAG show "acyclic (RAG s)" . |
1596 fix n1 n2 |
3960 qed |
1597 assume "(n1, n2) \<in> ?R" |
3961 |
1598 hence "(n1, n2) \<in> RAG s \<or> (n1 = Cs cs \<and> n2 = Th th)" by auto |
3962 lemma sgv_wRAG: "single_valued (wRAG s)" |
1599 thus "(n1, n2) \<in> ?L" |
3963 using waiting_unique |
1600 proof |
3964 by (unfold single_valued_def wRAG_def, auto) |
1601 assume "(n1, n2) \<in> RAG s" |
3965 |
1602 thus ?thesis |
3966 lemma sgv_hRAG: "single_valued (hRAG s)" |
1603 proof(cases rule:in_RAG_E) |
3967 using holding_unique |
1604 case (waiting th' cs') |
3968 by (unfold single_valued_def hRAG_def, auto) |
1605 find_theorems waiting e s |
3969 |
|
3970 lemma sgv_tRAG: "single_valued (tRAG s)" |
|
3971 by (unfold tRAG_def, rule single_valued_relcomp, |
|
3972 insert sgv_wRAG sgv_hRAG, auto) |
|
3973 |
|
3974 lemma acyclic_tRAG: "acyclic (tRAG s)" |
|
3975 proof(unfold tRAG_def, rule acyclic_compose) |
|
3976 show "acyclic (RAG s)" using acyclic_RAG . |
|
3977 next |
|
3978 show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
|
3979 next |
|
3980 show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
|
3981 qed |
|
3982 |
|
3983 lemma sgv_RAG: "single_valued (RAG s)" |
|
3984 using unique_RAG by (auto simp:single_valued_def) |
|
3985 |
|
3986 lemma rtree_RAG: "rtree (RAG s)" |
|
3987 using sgv_RAG acyclic_RAG |
|
3988 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
|
3989 |
|
3990 end |
|
3991 |
|
3992 sublocale valid_trace < rtree_RAG: rtree "RAG s" |
|
3993 proof |
|
3994 show "single_valued (RAG s)" |
|
3995 apply (intro_locales) |
|
3996 by (unfold single_valued_def, |
|
3997 auto intro:unique_RAG) |
|
3998 |
|
3999 show "acyclic (RAG s)" |
|
4000 by (rule acyclic_RAG) |
|
4001 qed |
|
4002 |
|
4003 sublocale valid_trace < rtree_s: rtree "tRAG s" |
|
4004 proof(unfold_locales) |
|
4005 from sgv_tRAG show "single_valued (tRAG s)" . |
|
4006 next |
|
4007 from acyclic_tRAG show "acyclic (tRAG s)" . |
|
4008 qed |
|
4009 |
|
4010 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" |
|
4011 proof - |
|
4012 show "fsubtree (RAG s)" |
|
4013 proof(intro_locales) |
|
4014 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . |
|
4015 next |
|
4016 show "fsubtree_axioms (RAG s)" |
|
4017 proof(unfold fsubtree_axioms_def) |
|
4018 from wf_RAG show "wf (RAG s)" . |
|
4019 qed |
1606 qed |
4020 qed |
1607 qed |
4021 qed |
1608 qed |
4022 |
1609 |
4023 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" |
1610 end |
4024 proof - |
1611 |
4025 have "fsubtree (tRAG s)" |
1612 |
4026 proof - |
1613 |
4027 have "fbranch (tRAG s)" |
1614 lemma "RAG (e # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)} |
4028 proof(unfold tRAG_def, rule fbranch_compose) |
1615 else RAG s \<union> {(Th th, Cs cs)})" |
4029 show "fbranch (wRAG s)" |
1616 proof(cases "wq s cs = []") |
4030 proof(rule finite_fbranchI) |
1617 case True |
4031 from finite_RAG show "finite (wRAG s)" |
1618 from wq_es_cs[unfolded this] |
4032 by (unfold RAG_split, auto) |
1619 have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto |
4033 qed |
1620 hence "holding (e#s) th cs" |
4034 next |
1621 using cs_holding_def holding_eq by blast |
4035 show "fbranch (hRAG s)" |
1622 thus |
4036 proof(rule finite_fbranchI) |
1623 qed |
4037 from finite_RAG |
1624 end |
4038 show "finite (hRAG s)" by (unfold RAG_split, auto) |
1625 |
4039 qed |
1626 text {* |
4040 qed |
1627 The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed |
4041 moreover have "wf (tRAG s)" |
1628 with the happening of @{text "P"}-events: |
4042 proof(rule wf_subset) |
1629 *} |
4043 show "wf (RAG s O RAG s)" using wf_RAG |
1630 lemma step_RAG_p: |
4044 by (fold wf_comp_self, simp) |
1631 "vt (P th cs#s) \<Longrightarrow> |
4045 next |
1632 RAG (P th cs # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)} |
4046 show "tRAG s \<subseteq> (RAG s O RAG s)" |
1633 else RAG s \<union> {(Th th, Cs cs)})" |
4047 by (unfold tRAG_alt_def, auto) |
1634 apply(simp only: s_RAG_def wq_def) |
4048 qed |
1635 apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def) |
4049 ultimately show ?thesis |
1636 apply(case_tac "csa = cs", auto) |
4050 by (unfold fsubtree_def fsubtree_axioms_def,auto) |
1637 apply(fold wq_def) |
4051 qed |
1638 apply(drule_tac step_back_step) |
4052 from this[folded tRAG_def] show "fsubtree (tRAG s)" . |
1639 apply(ind_cases " step s (P (hd (wq s cs)) cs)") |
4053 qed |
1640 apply(simp add:s_RAG_def wq_def cs_holding_def) |
4054 |
1641 apply(auto) |
4055 lemma Max_UNION: |
1642 done |
4056 assumes "finite A" |
1643 |
4057 and "A \<noteq> {}" |
1644 |
4058 and "\<forall> M \<in> f ` A. finite M" |
1645 |
4059 and "\<forall> M \<in> f ` A. M \<noteq> {}" |
1646 end |
4060 shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") |
|
4061 using assms[simp] |
|
4062 proof - |
|
4063 have "?L = Max (\<Union>(f ` A))" |
|
4064 by (fold Union_image_eq, simp) |
|
4065 also have "... = ?R" |
|
4066 by (subst Max_Union, simp+) |
|
4067 finally show ?thesis . |
|
4068 qed |
|
4069 |
|
4070 lemma max_Max_eq: |
|
4071 assumes "finite A" |
|
4072 and "A \<noteq> {}" |
|
4073 and "x = y" |
|
4074 shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R") |
|
4075 proof - |
|
4076 have "?R = Max (insert y A)" by simp |
|
4077 also from assms have "... = ?L" |
|
4078 by (subst Max.insert, simp+) |
|
4079 finally show ?thesis by simp |
|
4080 qed |
|
4081 |
|
4082 context valid_trace |
|
4083 begin |
|
4084 |
|
4085 (* ddd *) |
|
4086 lemma cp_gen_rec: |
|
4087 assumes "x = Th th" |
|
4088 shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)" |
|
4089 proof(cases "children (tRAG s) x = {}") |
|
4090 case True |
|
4091 show ?thesis |
|
4092 by (unfold True cp_gen_def subtree_children, simp add:assms) |
|
4093 next |
|
4094 case False |
|
4095 hence [simp]: "children (tRAG s) x \<noteq> {}" by auto |
|
4096 note fsbttRAGs.finite_subtree[simp] |
|
4097 have [simp]: "finite (children (tRAG s) x)" |
|
4098 by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], |
|
4099 rule children_subtree) |
|
4100 { fix r x |
|
4101 have "subtree r x \<noteq> {}" by (auto simp:subtree_def) |
|
4102 } note this[simp] |
|
4103 have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}" |
|
4104 proof - |
|
4105 from False obtain q where "q \<in> children (tRAG s) x" by blast |
|
4106 moreover have "subtree (tRAG s) q \<noteq> {}" by simp |
|
4107 ultimately show ?thesis by blast |
|
4108 qed |
|
4109 have h: "Max ((the_preced s \<circ> the_thread) ` |
|
4110 ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) = |
|
4111 Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)" |
|
4112 (is "?L = ?R") |
|
4113 proof - |
|
4114 let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L |
|
4115 let "Max (_ \<union> (?h ` ?B))" = ?R |
|
4116 let ?L1 = "?f ` \<Union>(?g ` ?B)" |
|
4117 have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" |
|
4118 proof - |
|
4119 have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp |
|
4120 also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto |
|
4121 finally have "Max ?L1 = Max ..." by simp |
|
4122 also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)" |
|
4123 by (subst Max_UNION, simp+) |
|
4124 also have "... = Max (cp_gen s ` children (tRAG s) x)" |
|
4125 by (unfold image_comp cp_gen_alt_def, simp) |
|
4126 finally show ?thesis . |
|
4127 qed |
|
4128 show ?thesis |
|
4129 proof - |
|
4130 have "?L = Max (?f ` ?A \<union> ?L1)" by simp |
|
4131 also have "... = max (the_preced s (the_thread x)) (Max ?L1)" |
|
4132 by (subst Max_Un, simp+) |
|
4133 also have "... = max (?f x) (Max (?h ` ?B))" |
|
4134 by (unfold eq_Max_L1, simp) |
|
4135 also have "... =?R" |
|
4136 by (rule max_Max_eq, (simp)+, unfold assms, simp) |
|
4137 finally show ?thesis . |
|
4138 qed |
|
4139 qed thus ?thesis |
|
4140 by (fold h subtree_children, unfold cp_gen_def, simp) |
|
4141 qed |
|
4142 |
|
4143 lemma cp_rec: |
|
4144 "cp s th = Max ({the_preced s th} \<union> |
|
4145 (cp s o the_thread) ` children (tRAG s) (Th th))" |
|
4146 proof - |
|
4147 have "Th th = Th th" by simp |
|
4148 note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] |
|
4149 show ?thesis |
|
4150 proof - |
|
4151 have "cp_gen s ` children (tRAG s) (Th th) = |
|
4152 (cp s \<circ> the_thread) ` children (tRAG s) (Th th)" |
|
4153 proof(rule cp_gen_over_set) |
|
4154 show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th" |
|
4155 by (unfold tRAG_alt_def, auto simp:children_def) |
|
4156 qed |
|
4157 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
|
4158 qed |
|
4159 qed |
|
4160 |
|
4161 end |
|
4162 |
|
4163 (* keep *) |
|
4164 lemma next_th_holding: |
|
4165 assumes vt: "vt s" |
|
4166 and nxt: "next_th s th cs th'" |
|
4167 shows "holding (wq s) th cs" |
|
4168 proof - |
|
4169 from nxt[unfolded next_th_def] |
|
4170 obtain rest where h: "wq s cs = th # rest" |
|
4171 "rest \<noteq> []" |
|
4172 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
|
4173 thus ?thesis |
|
4174 by (unfold cs_holding_def, auto) |
|
4175 qed |
|
4176 |
|
4177 context valid_trace |
|
4178 begin |
|
4179 |
|
4180 lemma next_th_waiting: |
|
4181 assumes nxt: "next_th s th cs th'" |
|
4182 shows "waiting (wq s) th' cs" |
|
4183 proof - |
|
4184 from nxt[unfolded next_th_def] |
|
4185 obtain rest where h: "wq s cs = th # rest" |
|
4186 "rest \<noteq> []" |
|
4187 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
|
4188 from wq_distinct[of cs, unfolded h] |
|
4189 have dst: "distinct (th # rest)" . |
|
4190 have in_rest: "th' \<in> set rest" |
|
4191 proof(unfold h, rule someI2) |
|
4192 show "distinct rest \<and> set rest = set rest" using dst by auto |
|
4193 next |
|
4194 fix x assume "distinct x \<and> set x = set rest" |
|
4195 with h(2) |
|
4196 show "hd x \<in> set (rest)" by (cases x, auto) |
|
4197 qed |
|
4198 hence "th' \<in> set (wq s cs)" by (unfold h(1), auto) |
|
4199 moreover have "th' \<noteq> hd (wq s cs)" |
|
4200 by (unfold h(1), insert in_rest dst, auto) |
|
4201 ultimately show ?thesis by (auto simp:cs_waiting_def) |
|
4202 qed |
|
4203 |
|
4204 lemma next_th_RAG: |
|
4205 assumes nxt: "next_th (s::event list) th cs th'" |
|
4206 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
|
4207 using vt assms next_th_holding next_th_waiting |
|
4208 by (unfold s_RAG_def, simp) |
|
4209 |
|
4210 end |
|
4211 |
|
4212 -- {* A useless definition *} |
|
4213 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
|
4214 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
|
4215 |
|
4216 find_theorems release |
|
4217 |
|
4218 lemma "wq (V th cs # s) cs1 = ttt" |
|
4219 apply (unfold wq_def, auto simp:Let_def) |
|
4220 |
|
4221 end |
|
4222 |
|