equal
deleted
inserted
replaced
47 qed |
47 qed |
48 next |
48 next |
49 case (thread_P thread cs) |
49 case (thread_P thread cs) |
50 assume eq_e: "e = P thread cs" |
50 assume eq_e: "e = P thread cs" |
51 and is_runing: "thread \<in> runing s" |
51 and is_runing: "thread \<in> runing s" |
52 from prems have vtp: "vt (P thread cs#s)" by auto |
52 from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto |
53 have neq_th: "th \<noteq> thread" |
53 have neq_th: "th \<noteq> thread" |
54 proof - |
54 proof - |
55 from not_in eq_e have "th \<notin> threads s" by simp |
55 from not_in eq_e have "th \<notin> threads s" by simp |
56 moreover from is_runing have "thread \<in> threads s" |
56 moreover from is_runing have "thread \<in> threads s" |
57 by (simp add:runing_def readys_def) |
57 by (simp add:runing_def readys_def) |
75 from not_in eq_e have "th \<notin> threads s" by simp |
75 from not_in eq_e have "th \<notin> threads s" by simp |
76 moreover from is_runing have "thread \<in> threads s" |
76 moreover from is_runing have "thread \<in> threads s" |
77 by (simp add:runing_def readys_def) |
77 by (simp add:runing_def readys_def) |
78 ultimately show ?thesis by auto |
78 ultimately show ?thesis by auto |
79 qed |
79 qed |
80 from prems have vtv: "vt (V thread cs#s)" by auto |
80 from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto |
81 from hold obtain rest |
81 from hold obtain rest |
82 where eq_wq: "wq s cs = thread # rest" |
82 where eq_wq: "wq s cs = thread # rest" |
83 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
83 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
84 from not_in eq_e eq_wq |
84 from not_in eq_e eq_wq |
85 have "\<not> next_th s thread cs th" |
85 have "\<not> next_th s thread cs th" |