equal
deleted
inserted
replaced
1 theory Correctness |
1 theory Correctness |
2 imports PIPBasics Implementation |
2 imports PIPBasics |
3 begin |
3 begin |
4 |
4 |
5 text {* |
5 text {* |
6 The following two auxiliary lemmas are used to reason about @{term Max}. |
6 The following two auxiliary lemmas are used to reason about @{term Max}. |
7 *} |
7 *} |
465 |
465 |
466 The following lemma shows that the counting controls whether |
466 The following lemma shows that the counting controls whether |
467 a thread is running or not. |
467 a thread is running or not. |
468 *} |
468 *} |
469 |
469 |
470 lemma pv_blocked_pre: |
470 lemma pv_blocked_pre: (* ddd *) |
471 assumes th'_in: "th' \<in> threads (t@s)" |
471 assumes th'_in: "th' \<in> threads (t@s)" |
472 and neq_th': "th' \<noteq> th" |
472 and neq_th': "th' \<noteq> th" |
473 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
473 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
474 shows "th' \<notin> runing (t@s)" |
474 shows "th' \<notin> runing (t@s)" |
475 proof |
475 proof |
494 qed |
494 qed |
495 qed |
495 qed |
496 |
496 |
497 lemmas pv_blocked = pv_blocked_pre[folded detached_eq] |
497 lemmas pv_blocked = pv_blocked_pre[folded detached_eq] |
498 |
498 |
499 lemma runing_precond_pre: |
499 lemma runing_precond_pre: (* ddd *) |
500 fixes th' |
500 fixes th' |
501 assumes th'_in: "th' \<in> threads s" |
501 assumes th'_in: "th' \<in> threads s" |
502 and eq_pv: "cntP s th' = cntV s th'" |
502 and eq_pv: "cntP s th' = cntV s th'" |
503 and neq_th': "th' \<noteq> th" |
503 and neq_th': "th' \<noteq> th" |
504 shows "th' \<in> threads (t@s) \<and> |
504 shows "th' \<in> threads (t@s) \<and> |
598 |
598 |
599 text {* Changing counting balance to detachedness *} |
599 text {* Changing counting balance to detachedness *} |
600 lemmas runing_precond_pre_dtc = runing_precond_pre |
600 lemmas runing_precond_pre_dtc = runing_precond_pre |
601 [folded vat_t.detached_eq vat_s.detached_eq] |
601 [folded vat_t.detached_eq vat_s.detached_eq] |
602 |
602 |
603 lemma runing_precond: |
603 lemma runing_precond: (* ddd *) |
604 fixes th' |
604 fixes th' |
605 assumes th'_in: "th' \<in> threads s" |
605 assumes th'_in: "th' \<in> threads s" |
606 and neq_th': "th' \<noteq> th" |
606 and neq_th': "th' \<noteq> th" |
607 and is_runing: "th' \<in> runing (t@s)" |
607 and is_runing: "th' \<in> runing (t@s)" |
608 shows "cntP s th' > cntV s th'" |
608 shows "cntP s th' > cntV s th'" |
658 show ?thesis |
658 show ?thesis |
659 by (metis add.commute append_assoc eq_pv h.runing_precond_pre |
659 by (metis add.commute append_assoc eq_pv h.runing_precond_pre |
660 moment_plus_split neq_th' th'_in) |
660 moment_plus_split neq_th' th'_in) |
661 qed |
661 qed |
662 |
662 |
663 lemma moment_blocked_eqpv: |
663 lemma moment_blocked_eqpv: (* ddd *) |
664 assumes neq_th': "th' \<noteq> th" |
664 assumes neq_th': "th' \<noteq> th" |
665 and th'_in: "th' \<in> threads ((moment i t)@s)" |
665 and th'_in: "th' \<in> threads ((moment i t)@s)" |
666 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
666 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
667 and le_ij: "i \<le> j" |
667 and le_ij: "i \<le> j" |
668 shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> |
668 shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> |
828 and "cp (t@s) th' = preced th s" |
828 and "cp (t@s) th' = preced th s" |
829 apply (metis neq_th runing' runing_inversion_2) |
829 apply (metis neq_th runing' runing_inversion_2) |
830 apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) |
830 apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) |
831 by (metis neq_th runing' runing_inversion_3) |
831 by (metis neq_th runing' runing_inversion_3) |
832 |
832 |
833 |
|
834 text {* |
833 text {* |
835 Suppose @{term th} is not running, it is first shown that |
834 Suppose @{term th} is not running, it is first shown that |
836 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
835 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
837 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
836 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
838 |
837 |