1358 

  1359 locale step_P_cps_e =step_P_cps +

  1360   assumes ee: "wq s' cs = []"

  1361 

  1362 context step_P_cps_e

  1363 begin

  1364 

  1365 lemma depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"

  1366 proof -

  1367   from ee and  step_depend_p[OF vt_s[unfolded s_def], folded s_def]

  1368   show ?thesis by auto

  1369 qed

  1370 

  1371 lemma child_kept_left:

  1372   assumes 

  1373   "(n1, n2) \<in> (child s')^+"

  1374   shows "(n1, n2) \<in> (child s)^+"

  1375 proof -

  1376   from assms show ?thesis 

  1377   proof(induct rule: converse_trancl_induct)

  1378     case (base y)

  1379     from base obtain th1 cs1 th2

  1380       where h1: "(Th th1, Cs cs1) \<in> depend s'"

  1381       and h2: "(Cs cs1, Th th2) \<in> depend s'"

  1382       and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)

  1383     have "cs1 \<noteq> cs"

  1384     proof

  1385       assume eq_cs: "cs1 = cs"

  1386       with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp

  1387       with ee show False

  1388         by (auto simp:s_depend_def cs_waiting_def)

  1389     qed

  1390     with h1 h2 depend_s have 

  1391       h1': "(Th th1, Cs cs1) \<in> depend s" and

  1392       h2': "(Cs cs1, Th th2) \<in> depend s" by auto

  1393     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)

  1394     with eq_y eq_n2 have "(y, n2) \<in> child s" by simp

  1395     thus ?case by auto

  1396   next

  1397     case (step y z)

  1398     have "(y, z) \<in> child s'" by fact

  1399     then obtain th1 cs1 th2

  1400       where h1: "(Th th1, Cs cs1) \<in> depend s'"

  1401       and h2: "(Cs cs1, Th th2) \<in> depend s'"

  1402       and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)

  1403     have "cs1 \<noteq> cs"

  1404     proof

  1405       assume eq_cs: "cs1 = cs"

  1406       with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp

  1407       with ee show False 

  1408         by (auto simp:s_depend_def cs_waiting_def)

  1409     qed

  1410     with h1 h2 depend_s have 

  1411       h1': "(Th th1, Cs cs1) \<in> depend s" and

  1412       h2': "(Cs cs1, Th th2) \<in> depend s" by auto

  1413     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)

  1414     with eq_y eq_z have "(y, z) \<in> child s" by simp

  1415     moreover have "(z, n2) \<in> (child s)^+" by fact

  1416     ultimately show ?case by auto

  1417   qed

  1418 qed

  1419 

  1420 lemma  child_kept_right:

  1421   assumes

  1422   "(n1, n2) \<in> (child s)^+"

  1423   shows "(n1, n2) \<in> (child s')^+"

  1424 proof -

  1425   from assms show ?thesis

  1426   proof(induct)

  1427     case (base y)

  1428     from base and depend_s

  1429     have "(n1, y) \<in> child s'"

  1430       apply (auto simp:child_def)

  1431       proof -

  1432         fix th'

  1433         assume "(Th th', Cs cs) \<in> depend s'"

  1434         with ee have "False"

  1435           by (auto simp:s_depend_def cs_waiting_def)

  1436         thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto 

  1437       qed

  1438     thus ?case by auto

  1439   next

  1440     case (step y z)

  1441     have "(y, z) \<in> child s" by fact

  1442     with depend_s have "(y, z) \<in> child s'"

  1443       apply (auto simp:child_def)

  1444       proof -

  1445         fix th'

  1446         assume "(Th th', Cs cs) \<in> depend s'"

  1447         with ee have "False"

  1448           by (auto simp:s_depend_def cs_waiting_def)

  1449         thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto 

  1450       qed

  1451     moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact

  1452     ultimately show ?case by auto

  1453   qed

  1454 qed

  1455 

  1456 lemma eq_child: "(child s)^+ = (child s')^+"

  1457   by (insert child_kept_left child_kept_right, auto)

  1458 

  1459 lemma eq_cp:

  1460   fixes th' 

  1461   shows "cp s th' = cp s' th'"

  1462   apply (unfold cp_eq_cpreced cpreced_def)

  1463 proof -

  1464   have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"

  1465     apply (unfold cs_dependents_def, unfold eq_depend)

  1466   proof -

  1467     from eq_child

  1468     have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"

  1469       by auto

  1470     with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]

  1471     show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"

  1472       by simp

  1473   qed

  1474   moreover {

  1475     fix th1 

  1476     assume "th1 \<in> {th'} \<union> dependents (wq s') th'"

  1477     hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto

  1478     hence "preced th1 s = preced th1 s'"

  1479     proof

  1480       assume "th1 = th'"

  1481       show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)

  1482     next

  1483       assume "th1 \<in> dependents (wq s') th'"

  1484       show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)

  1485     qed

  1486   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = 

  1487                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 

  1488     by (auto simp:image_def)

  1489   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =

  1490         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp

  1491 qed

  1492 

  1493 end