1 theory PrioG |
1 theory PrioG |
2 imports PrioGDef |
2 imports PrioGDef |
3 begin |
3 begin |
4 |
4 |
5 lemma runing_ready: "runing s \<subseteq> readys s" |
5 lemma runing_ready: |
6 by (auto simp only:runing_def readys_def) |
6 shows "runing s \<subseteq> readys s" |
|
7 unfolding runing_def readys_def |
|
8 by auto |
|
9 |
|
10 lemma readys_threads: |
|
11 shows "readys s \<subseteq> threads s" |
|
12 unfolding readys_def |
|
13 by auto |
7 |
14 |
8 lemma wq_v_neq: |
15 lemma wq_v_neq: |
9 "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'" |
16 "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'" |
10 by (auto simp:wq_def Let_def cp_def split:list.splits) |
17 by (auto simp:wq_def Let_def cp_def split:list.splits) |
11 |
18 |
352 fixes s cs1 cs2 |
359 fixes s cs1 cs2 |
353 assumes "vt s" |
360 assumes "vt s" |
354 and "waiting s th cs1" |
361 and "waiting s th cs1" |
355 and "waiting s th cs2" |
362 and "waiting s th cs2" |
356 shows "cs1 = cs2" |
363 shows "cs1 = cs2" |
357 proof - |
364 using waiting_unique_pre prems |
358 from waiting_unique_pre and prems |
365 unfolding wq_def s_waiting_def |
359 show ?thesis |
366 by auto |
360 by (auto simp add: wq_def s_waiting_def) |
367 |
361 qed |
368 (* not used *) |
362 |
|
363 lemma held_unique: |
369 lemma held_unique: |
364 assumes "vt s" |
370 fixes s::"state" |
365 and "holding s th1 cs" |
371 assumes "holding s th1 cs" |
366 and "holding s th2 cs" |
372 and "holding s th2 cs" |
367 shows "th1 = th2" |
373 shows "th1 = th2" |
368 proof - |
374 using prems |
369 from prems show ?thesis |
375 unfolding s_holding_def |
370 unfolding s_holding_def |
376 by auto |
371 by auto |
377 |
372 qed |
|
373 |
378 |
374 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" |
375 apply (induct s, auto) |
380 apply (induct s, auto) |
376 by (case_tac a, auto split:if_splits) |
381 by (case_tac a, auto split:if_splits) |
377 |
382 |
2466 qed |
2471 qed |
2467 |
2472 |
2468 lemma finite_threads: |
2473 lemma finite_threads: |
2469 assumes vt: "vt s" |
2474 assumes vt: "vt s" |
2470 shows "finite (threads s)" |
2475 shows "finite (threads s)" |
2471 proof - |
2476 using vt |
2472 from vt show ?thesis |
2477 by (induct) (auto elim: step.cases) |
2473 proof(induct) |
|
2474 case (vt_cons s e) |
|
2475 assume vt: "vt s" |
|
2476 and step: "step s e" |
|
2477 and ih: "finite (threads s)" |
|
2478 from step |
|
2479 show ?case |
|
2480 proof(cases) |
|
2481 case (thread_create thread prio) |
|
2482 assume eq_e: "e = Create thread prio" |
|
2483 with ih |
|
2484 show ?thesis by (unfold eq_e, auto) |
|
2485 next |
|
2486 case (thread_exit thread) |
|
2487 assume eq_e: "e = Exit thread" |
|
2488 with ih show ?thesis |
|
2489 by (unfold eq_e, auto) |
|
2490 next |
|
2491 case (thread_P thread cs) |
|
2492 assume eq_e: "e = P thread cs" |
|
2493 with ih show ?thesis by (unfold eq_e, auto) |
|
2494 next |
|
2495 case (thread_V thread cs) |
|
2496 assume eq_e: "e = V thread cs" |
|
2497 with ih show ?thesis by (unfold eq_e, auto) |
|
2498 next |
|
2499 case (thread_set thread prio) |
|
2500 from vt_cons thread_set show ?thesis by simp |
|
2501 qed |
|
2502 next |
|
2503 case vt_nil |
|
2504 show ?case by (auto) |
|
2505 qed |
|
2506 qed |
|
2507 |
2478 |
2508 lemma Max_f_mono: |
2479 lemma Max_f_mono: |
2509 assumes seq: "A \<subseteq> B" |
2480 assumes seq: "A \<subseteq> B" |
2510 and np: "A \<noteq> {}" |
2481 and np: "A \<noteq> {}" |
2511 and fnt: "finite B" |
2482 and fnt: "finite B" |
2783 next |
2754 next |
2784 case False |
2755 case False |
2785 show ?thesis by (rule max_cp_readys_threads_pre[OF vt False]) |
2756 show ?thesis by (rule max_cp_readys_threads_pre[OF vt False]) |
2786 qed |
2757 qed |
2787 |
2758 |
2788 lemma readys_threads: |
|
2789 shows "readys s \<subseteq> threads s" |
|
2790 proof |
|
2791 fix th |
|
2792 assume "th \<in> readys s" |
|
2793 thus "th \<in> threads s" |
|
2794 by (unfold readys_def, auto) |
|
2795 qed |
|
2796 |
2759 |
2797 lemma eq_holding: "holding (wq s) th cs = holding s th cs" |
2760 lemma eq_holding: "holding (wq s) th cs = holding s th cs" |
2798 apply (unfold s_holding_def cs_holding_def wq_def, simp) |
2761 apply (unfold s_holding_def cs_holding_def wq_def, simp) |
2799 done |
2762 done |
2800 |
2763 |