equal
deleted
inserted
replaced
359 fixes s cs1 cs2 |
359 fixes s cs1 cs2 |
360 assumes "vt s" |
360 assumes "vt s" |
361 and "waiting s th cs1" |
361 and "waiting s th cs1" |
362 and "waiting s th cs2" |
362 and "waiting s th cs2" |
363 shows "cs1 = cs2" |
363 shows "cs1 = cs2" |
364 using waiting_unique_pre prems |
364 using waiting_unique_pre assms |
365 unfolding wq_def s_waiting_def |
365 unfolding wq_def s_waiting_def |
366 by auto |
366 by auto |
367 |
367 |
368 (* not used *) |
368 (* not used *) |
369 lemma held_unique: |
369 lemma held_unique: |
370 fixes s::"state" |
370 fixes s::"state" |
371 assumes "holding s th1 cs" |
371 assumes "holding s th1 cs" |
372 and "holding s th2 cs" |
372 and "holding s th2 cs" |
373 shows "th1 = th2" |
373 shows "th1 = th2" |
374 using prems |
374 using assms |
375 unfolding s_holding_def |
375 unfolding s_holding_def |
376 by auto |
376 by auto |
377 |
377 |
378 |
378 |
379 lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s" |
379 lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s" |
1202 and neq_th: "th \<noteq> thread" |
1202 and neq_th: "th \<noteq> thread" |
1203 and eq_wq: "wq s cs = thread#rest" |
1203 and eq_wq: "wq s cs = thread#rest" |
1204 and not_in: "th \<notin> set rest" |
1204 and not_in: "th \<notin> set rest" |
1205 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1205 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1206 proof - |
1206 proof - |
1207 from prems show ?thesis |
1207 from assms show ?thesis |
1208 apply (auto simp:readys_def) |
1208 apply (auto simp:readys_def) |
1209 apply(simp add:s_waiting_def[folded wq_def]) |
1209 apply(simp add:s_waiting_def[folded wq_def]) |
1210 apply (erule_tac x = csa in allE) |
1210 apply (erule_tac x = csa in allE) |
1211 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
1211 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
1212 apply (case_tac "csa = cs", simp) |
1212 apply (case_tac "csa = cs", simp) |
1352 fixes th cs s |
1352 fixes th cs s |
1353 assumes vt: "vt (P th cs#s)" |
1353 assumes vt: "vt (P th cs#s)" |
1354 and "wq s cs = []" |
1354 and "wq s cs = []" |
1355 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
1355 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
1356 proof - |
1356 proof - |
1357 from prems show ?thesis |
1357 from assms show ?thesis |
1358 unfolding holdents_def step_depend_p[OF vt] by auto |
1358 unfolding holdents_def step_depend_p[OF vt] by auto |
1359 qed |
1359 qed |
1360 |
1360 |
1361 lemma step_holdents_p_eq: |
1361 lemma step_holdents_p_eq: |
1362 fixes th cs s |
1362 fixes th cs s |
1363 assumes vt: "vt (P th cs#s)" |
1363 assumes vt: "vt (P th cs#s)" |
1364 and "wq s cs \<noteq> []" |
1364 and "wq s cs \<noteq> []" |
1365 shows "holdents (P th cs#s) th = holdents s th" |
1365 shows "holdents (P th cs#s) th = holdents s th" |
1366 proof - |
1366 proof - |
1367 from prems show ?thesis |
1367 from assms show ?thesis |
1368 unfolding holdents_def step_depend_p[OF vt] by auto |
1368 unfolding holdents_def step_depend_p[OF vt] by auto |
1369 qed |
1369 qed |
1370 |
1370 |
1371 |
1371 |
1372 lemma finite_holding: |
1372 lemma finite_holding: |
1543 next |
1543 next |
1544 case (thread_P thread cs) |
1544 case (thread_P thread cs) |
1545 assume eq_e: "e = P thread cs" |
1545 assume eq_e: "e = P thread cs" |
1546 and is_runing: "thread \<in> runing s" |
1546 and is_runing: "thread \<in> runing s" |
1547 and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+" |
1547 and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+" |
1548 from prems have vtp: "vt (P thread cs#s)" by auto |
1548 from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto |
1549 show ?thesis |
1549 show ?thesis |
1550 proof - |
1550 proof - |
1551 { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast |
1551 { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast |
1552 assume neq_th: "th \<noteq> thread" |
1552 assume neq_th: "th \<noteq> thread" |
1553 with eq_e |
1553 with eq_e |
1648 qed |
1648 qed |
1649 } ultimately show ?thesis by blast |
1649 } ultimately show ?thesis by blast |
1650 qed |
1650 qed |
1651 next |
1651 next |
1652 case (thread_V thread cs) |
1652 case (thread_V thread cs) |
1653 from prems have vtv: "vt (V thread cs # s)" by auto |
1653 from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto |
1654 assume eq_e: "e = V thread cs" |
1654 assume eq_e: "e = V thread cs" |
1655 and is_runing: "thread \<in> runing s" |
1655 and is_runing: "thread \<in> runing s" |
1656 and hold: "holding s thread cs" |
1656 and hold: "holding s thread cs" |
1657 from hold obtain rest |
1657 from hold obtain rest |
1658 where eq_wq: "wq s cs = thread # rest" |
1658 where eq_wq: "wq s cs = thread # rest" |
1981 qed |
1981 qed |
1982 next |
1982 next |
1983 case (thread_P thread cs) |
1983 case (thread_P thread cs) |
1984 assume eq_e: "e = P thread cs" |
1984 assume eq_e: "e = P thread cs" |
1985 and is_runing: "thread \<in> runing s" |
1985 and is_runing: "thread \<in> runing s" |
1986 from prems have vtp: "vt (P thread cs#s)" by auto |
1986 from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto |
1987 have neq_th: "th \<noteq> thread" |
1987 have neq_th: "th \<noteq> thread" |
1988 proof - |
1988 proof - |
1989 from not_in eq_e have "th \<notin> threads s" by simp |
1989 from not_in eq_e have "th \<notin> threads s" by simp |
1990 moreover from is_runing have "thread \<in> threads s" |
1990 moreover from is_runing have "thread \<in> threads s" |
1991 by (simp add:runing_def readys_def) |
1991 by (simp add:runing_def readys_def) |
2009 from not_in eq_e have "th \<notin> threads s" by simp |
2009 from not_in eq_e have "th \<notin> threads s" by simp |
2010 moreover from is_runing have "thread \<in> threads s" |
2010 moreover from is_runing have "thread \<in> threads s" |
2011 by (simp add:runing_def readys_def) |
2011 by (simp add:runing_def readys_def) |
2012 ultimately show ?thesis by auto |
2012 ultimately show ?thesis by auto |
2013 qed |
2013 qed |
2014 from prems have vtv: "vt (V thread cs#s)" by auto |
2014 from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto |
2015 from hold obtain rest |
2015 from hold obtain rest |
2016 where eq_wq: "wq s cs = thread # rest" |
2016 where eq_wq: "wq s cs = thread # rest" |
2017 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
2017 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
2018 from not_in eq_e eq_wq |
2018 from not_in eq_e eq_wq |
2019 have "\<not> next_th s thread cs th" |
2019 have "\<not> next_th s thread cs th" |