587 by the happening of event @{term e}: *} |
587 by the happening of event @{term e}: *} |
588 have "cntP ((e#t)@s) th' = cntP (t@s) th'" |
588 have "cntP ((e#t)@s) th' = cntP (t@s) th'" |
589 proof(rule ccontr) -- {* Proof by contradiction. *} |
589 proof(rule ccontr) -- {* Proof by contradiction. *} |
590 -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} |
590 -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} |
591 assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'" |
591 assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'" |
592 -- {* Then the actor of @{term e} must be @{term th'} and @{term e} |
592 from cntP_diff_inv[OF this[simplified]] |
593 must be a @{term P}-event: *} |
593 obtain cs' where "e = P th' cs'" by auto |
594 hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) |
594 from vat_es.pip_e[unfolded this] |
595 with vat_es.actor_inv |
595 have "th' \<in> runing (t@s)" |
596 -- {* According to @{thm vat_es.actor_inv}, @{term th'} must be running at |
596 by (cases, simp) |
597 the moment @{term "t@s"}: *} |
|
598 have "th' \<in> runing (t@s)" by (cases e, auto) |
|
599 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis |
597 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis |
600 shows @{term th'} can not be running at moment @{term "t@s"}: *} |
598 shows @{term th'} can not be running at moment @{term "t@s"}: *} |
601 moreover have "th' \<notin> runing (t@s)" |
599 moreover have "th' \<notin> runing (t@s)" |
602 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
600 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
603 -- {* Contradiction is finally derived: *} |
601 -- {* Contradiction is finally derived: *} |
607 by the happening of event @{term e}: *} |
605 by the happening of event @{term e}: *} |
608 -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} |
606 -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} |
609 moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" |
607 moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" |
610 proof(rule ccontr) -- {* Proof by contradiction. *} |
608 proof(rule ccontr) -- {* Proof by contradiction. *} |
611 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'" |
609 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'" |
612 hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) |
610 from cntV_diff_inv[OF this[simplified]] |
613 with vat_es.actor_inv |
611 obtain cs' where "e = V th' cs'" by auto |
614 have "th' \<in> runing (t@s)" by (cases e, auto) |
612 from vat_es.pip_e[unfolded this] |
|
613 have "th' \<in> runing (t@s)" by (cases, auto) |
615 moreover have "th' \<notin> runing (t@s)" |
614 moreover have "th' \<notin> runing (t@s)" |
616 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
615 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
617 ultimately show False by simp |
616 ultimately show False by simp |
618 qed |
617 qed |
619 -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} |
618 -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} |