348 } |
348 } |
349 ultimately show "acyclic (RAG2 (V th cs # s))" by metis |
349 ultimately show "acyclic (RAG2 (V th cs # s))" by metis |
350 qed (simp_all) |
350 qed (simp_all) |
351 |
351 |
352 |
352 |
353 |
353 lemma finite_RAG: |
354 |
354 assumes "vt s" |
355 |
355 shows "finite (RAG2 s)" |
356 |
356 using assms |
|
357 apply(induct) |
|
358 apply(simp add: RAG2_def RAG_def waits_def holds_def) |
|
359 apply(erule step.cases) |
|
360 apply(auto) |
|
361 apply(case_tac "wq sa cs = []") |
|
362 apply(rule finite_subset) |
|
363 apply(rule RAG_p1) |
|
364 apply(simp) |
|
365 apply(simp) |
|
366 apply(rule finite_subset) |
|
367 apply(rule RAG_p2) |
|
368 apply(simp) |
|
369 apply(simp) |
|
370 apply(simp) |
|
371 apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts") |
|
372 apply(erule exE) |
|
373 apply(case_tac "wts = []") |
|
374 apply(rule finite_subset) |
|
375 apply(rule RAG_v1) |
|
376 apply(simp) |
|
377 apply(simp) |
|
378 apply(rule finite_subset) |
|
379 apply(rule RAG_v2) |
|
380 apply(simp) |
|
381 apply(simp) |
|
382 apply(simp) |
|
383 apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") |
|
384 apply(case_tac "wq sa cs") |
|
385 apply(auto)[2] |
|
386 apply(auto simp add: holds2_def holds_def wq_def) |
|
387 done |
|
388 |
|
389 lemma wq_threads: |
|
390 assumes vt: "vt s" |
|
391 and h: "th \<in> set (wq s cs)" |
|
392 shows "th \<in> threads s" |
|
393 using assms |
|
394 apply(induct) |
|
395 apply(simp add: wq_def) |
|
396 apply(erule step.cases) |
|
397 apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) |
|
398 apply(simp add: waits_def) |
|
399 apply(auto simp add: waits_def split: if_splits)[1] |
|
400 apply(auto split: if_splits) |
|
401 apply(simp only: waits_def) |
|
402 by (metis insert_iff set_simps(2)) |
|
403 |
|
404 lemma max_cpreceds_readys_threads: |
|
405 assumes vt: "vt s" |
|
406 shows "Max (cpreceds2 s (readys s)) = Max (cpreceds2 s (threads s))" |
|
407 apply(case_tac "threads s = {}") |
|
408 apply(simp add: readys_def) |
|
409 using vt |
|
410 apply(induct) |
|
411 apply(simp) |
|
412 apply(erule step.cases) |
|
413 apply(auto simp add: readys_def waits2_def waits_def Let_def holding_def runing_def holds2_def) |
|
414 defer |
|
415 defer |
|
416 oops |
|
417 |
|
418 |
|
419 end |