189 unfolding RAG2_def |
192 unfolding RAG2_def |
190 by (simp add: Let_def) |
193 by (simp add: Let_def) |
191 |
194 |
192 lemma RAG_p1: |
195 lemma RAG_p1: |
193 assumes "wq s cs = []" |
196 assumes "wq s cs = []" |
194 shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}" |
197 shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}" |
195 using assms |
198 using assms |
196 apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def) |
199 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def |
197 apply (metis in_set_insert insert_Nil list.distinct(1)) |
200 by (auto simp add: Let_def) |
198 done |
201 |
199 |
202 |
200 lemma RAG_p2: |
203 lemma RAG_p2: |
201 assumes "vt (P th cs#s)" "wq s cs \<noteq> []" |
204 assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []" |
202 shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}" |
205 shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}" |
203 using assms |
206 using assms |
204 apply(simp add: RAG2_def Let_def) |
207 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def |
205 apply(erule_tac vt.cases) |
208 by (auto simp add: Let_def) |
206 apply(simp) |
209 |
207 apply(clarify) |
210 lemma [simp]: "(SOME q. distinct q \<and> q = []) = []" |
208 apply(simp) |
211 by auto |
209 apply(erule_tac step.cases) |
212 |
210 apply(simp_all) |
213 lemma [simp]: "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)" |
211 apply(simp add: wq_def RAG_def RAG2_def) |
214 apply auto |
212 apply(simp add: waits_def holds_def) |
215 apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
213 apply(auto) |
216 by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
214 done |
217 |
215 |
218 lemma RAG_v1: |
216 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool" |
219 assumes vt: "wq s cs = [th]" |
217 where "next_th s th cs t = |
220 shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" |
218 (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))" |
221 using assms |
219 |
222 unfolding RAG2_def RAG_def waits_def holds_def wq_def |
220 lemma RAG_v: |
223 by (auto simp add: Let_def) |
221 assumes vt:"vt (V th cs#s)" |
224 |
222 shows " |
225 lemma RAG_v2: |
223 RAG2 (V th cs # s) = |
226 assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []" |
224 RAG2 s - {(Cs cs, Th th)} - |
227 shows "RAG2 (V th cs # s) \<subseteq> |
225 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
228 RAG2 s - {(Cs cs, Th th)} - {(Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}" |
226 {(Cs cs, Th th') |th'. next_th s th cs th'}" |
229 unfolding RAG2_def RAG_def waits_def holds_def |
227 apply (insert vt, unfold RAG2_def RAG_def) |
230 using assms wq_distinct[OF vt(1), of"cs"] |
228 sorry |
231 by (auto simp add: Let_def wq_def) |
229 |
232 |
230 lemma waiting_unique: |
233 lemma waiting_unique: |
231 assumes "vt s" |
234 assumes "vt s" |
232 and "waits2 s th cs1" |
235 and "waits2 s th cs1" |
233 and "waits2 s th cs2" |
236 and "waits2 s th cs2" |
234 shows "cs1 = cs2" |
237 shows "cs1 = cs2" |
235 sorry |
238 sorry |
236 |
|
237 lemma singleton_Un: |
|
238 shows "A \<union> {x} = insert x A" |
|
239 by simp |
|
240 |
|
241 |
239 |
242 lemma acyclic_RAG_step: |
240 lemma acyclic_RAG_step: |
243 assumes vt: "vt s" |
241 assumes vt: "vt s" |
244 and stp: "step s e" |
242 and stp: "step s e" |
245 and ac: "acyclic (RAG2 s)" |
243 and ac: "acyclic (RAG2 s)" |
246 shows "acyclic (RAG2 (e # s))" |
244 shows "acyclic (RAG2 (e # s))" |
247 using stp vt ac |
245 using stp vt ac |
248 proof (induct) |
246 proof (induct) |
249 case (step_P th s cs) |
247 case (step_P th s cs) |
250 have vt: "vt s" by fact |
|
251 have ac: "acyclic (RAG2 s)" by fact |
248 have ac: "acyclic (RAG2 s)" by fact |
252 have rn: "th \<in> runing s" by fact |
|
253 have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact |
249 have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact |
254 have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons) |
|
255 { assume a: "wq s cs = []" -- "case waiting queue is empty" |
250 { assume a: "wq s cs = []" -- "case waiting queue is empty" |
256 have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*" |
251 have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*" |
257 proof |
252 proof |
258 assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*" |
253 assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*" |
259 then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) |
254 then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) |
260 then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis |
255 then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis |
261 with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def) |
256 with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def) |
262 qed |
257 qed |
263 with acyclic_insert ac |
258 with acyclic_insert ac |
264 have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp |
259 have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp |
265 then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] by simp |
260 then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] |
|
261 by (rule acyclic_subset) |
266 } |
262 } |
267 moreover |
263 moreover |
268 { assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty" |
264 { assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty" |
269 from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD) |
265 from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD) |
270 with acyclic_insert ac |
266 with acyclic_insert ac |
271 have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto |
267 have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto |
272 then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF vtt a] by simp |
268 then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds a] |
|
269 by (rule acyclic_subset) |
273 } |
270 } |
274 ultimately show "acyclic (RAG2 (P th cs # s))" by metis |
271 ultimately show "acyclic (RAG2 (P th cs # s))" by metis |
275 next |
272 next |
276 case (step_V th s cs) |
273 case (step_V th s cs) |
277 have vt: "vt s" by fact |
274 have vt: "vt s" by fact |
278 have ac: "acyclic (RAG2 s)" by fact |
275 have ac: "acyclic (RAG2 s)" by fact |
279 have rn: "th \<in> runing s" by fact |
276 have rn: "th \<in> runing s" by fact |
280 have hd: "holds2 s th cs" by fact |
277 have hd: "holds2 s th cs" by fact |
281 from hd |
278 from hd have th_in: "th \<in> set (wq s cs)" and |
282 have th_in: "th \<in> set (wq s cs)" and |
279 eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto |
283 eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto |
280 then obtain wts where |
284 then obtain rest where |
281 eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto) |
285 eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto) |
282 { assume "wts = []" -- "case no thread present to take over" |
286 show ?case |
283 with eq_wq have "wq s cs = [th]" by simp |
287 apply(subst RAG_v) |
284 then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1) |
288 apply(rule vt_cons) |
285 moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset) |
289 apply(rule vt) |
286 ultimately |
290 apply(rule step.step_V) |
287 have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) |
291 apply(rule rn) |
288 } |
292 apply(rule hd) |
289 moreover |
293 using eq_wq |
290 { def nth \<equiv> "next_to_run wts" |
294 apply(cases "rest = []") |
291 assume aa: "wts \<noteq> []" -- "at least one thread present to take over" |
295 apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}") |
292 with vt eq_wq |
296 apply(simp) |
293 have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" |
297 apply(rule acyclic_subset) |
294 unfolding nth_def by (rule_tac RAG_v2) (auto) |
298 apply(rule ac) |
295 moreover |
299 apply(auto)[1] |
296 have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" |
300 apply(auto simp add: next_th_def)[1] |
297 proof - |
301 -- "case wq more than a singleton" |
298 have "acyclic (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset) |
302 apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} = |
299 moreover |
303 {(Cs cs, Th th') |th'. next_th s th cs th'}") |
300 have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+" |
304 apply(rotate_tac 2) |
301 proof |
305 apply(drule sym) |
302 assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+" |
306 apply(simp only: singleton_Un) |
303 then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" |
307 apply(simp only: acyclic_insert) |
304 by (metis converse_tranclE) |
308 apply(rule conjI) |
305 then have "(Th nth, z) \<in> RAG2 s" by simp |
309 apply(rule acyclic_subset) |
306 then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s" |
310 apply(rule ac) |
307 unfolding RAG2_def RAG_def by auto |
311 apply(auto)[1] |
308 then have "cs = cs'" |
312 apply(rotate_tac 2) |
309 apply(rule_tac waiting_unique[OF vt]) |
313 apply(thin_tac "?X") |
310 using eq_wq aa |
314 defer |
311 apply(auto simp add: nth_def RAG2_def RAG_def waits2_def waits_def wq_def) |
315 apply(simp add: next_th_def) |
312 apply (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.inject set_empty2 tfl_some vt wq_def wq_distinct) |
316 apply(clarify) |
313 by (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.sel(1) set_empty2 tfl_some vt wq_def wq_distinct) |
317 apply(simp add: rtrancl_eq_or_trancl) |
314 then show "False" using a b by simp |
318 apply(drule tranclD) |
315 qed |
319 apply(erule exE) |
316 then have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>*" |
320 apply(drule conjunct1) |
317 by (metis node.distinct(1) rtranclD) |
321 apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s") |
318 ultimately |
322 prefer 2 |
319 show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))" |
323 apply(simp) |
320 by (simp add: acyclic_insert) |
324 apply(case_tac z) |
321 qed |
325 apply(simp add: RAG2_def RAG_def) |
322 ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) |
326 apply(clarify) |
323 } |
327 apply(simp) |
324 ultimately show "acyclic (RAG2 (V th cs # s))" by metis |
328 apply(simp add: next_th_def) |
|
329 apply(rule waiting_unique) |
|
330 apply(rule vt) |
|
331 apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def) |
|
332 apply(rotate_tac 2) |
|
333 apply(thin_tac "?X") |
|
334 apply(subgoal_tac "distinct (wq s cs)") |
|
335 prefer 2 |
|
336 apply(rule wq_distinct) |
|
337 apply(rule vt) |
|
338 apply (unfold waits2_def waits_def wq_def, auto) |
|
339 apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []") |
|
340 prefer 2 |
|
341 apply (metis (mono_tags) set_empty tfl_some) |
|
342 apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> |
|
343 set (SOME q. distinct q \<and> set q = set rest)") |
|
344 prefer 2 |
|
345 apply(auto)[1] |
|
346 apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") |
|
347 prefer 2 |
|
348 apply(rule someI2) |
|
349 apply(auto)[2] |
|
350 apply(auto)[1] |
|
351 apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []") |
|
352 prefer 2 |
|
353 apply (metis (mono_tags) set_empty tfl_some) |
|
354 apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> |
|
355 set (SOME q. distinct q \<and> set q = set rest)") |
|
356 prefer 2 |
|
357 apply(auto)[1] |
|
358 apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") |
|
359 prefer 2 |
|
360 apply(rule someI2) |
|
361 apply(auto)[2] |
|
362 apply(auto)[1] |
|
363 done |
|
364 qed (simp_all) |
325 qed (simp_all) |
365 |
326 |
366 |
327 |
367 |
328 |
368 |
329 |