equal
deleted
inserted
replaced
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: "runing s \<subseteq> readys s" |
6 by (auto simp only:runing_def readys_def) |
6 by (auto simp only:runing_def readys_def) |
7 |
7 |
347 } ultimately show ?thesis by arith |
347 } ultimately show ?thesis by arith |
348 qed |
348 qed |
349 qed |
349 qed |
350 |
350 |
351 lemma waiting_unique: |
351 lemma waiting_unique: |
|
352 fixes s cs1 cs2 |
352 assumes "vt step s" |
353 assumes "vt step s" |
353 and "waiting s th cs1" |
354 and "waiting s th cs1" |
354 and "waiting s th cs2" |
355 and "waiting s th cs2" |
355 shows "cs1 = cs2" |
356 shows "cs1 = cs2" |
356 proof - |
357 proof - |
357 from waiting_unique_pre and prems |
358 from waiting_unique_pre and prems |
358 show ?thesis |
359 show ?thesis |
359 by (auto simp add:s_waiting_def) |
360 by (auto simp add:s_waiting_def) |
360 qed |
361 qed |
361 |
362 |
362 lemma holded_unique: |
363 lemma held_unique: |
363 assumes "vt step s" |
364 assumes "vt step s" |
364 and "holding s th1 cs" |
365 and "holding s th1 cs" |
365 and "holding s th2 cs" |
366 and "holding s th2 cs" |
366 shows "th1 = th2" |
367 shows "th1 = th2" |
367 proof - |
368 proof - |