578 -- {* The nontrivial case is for the @{term Cons}: *} |
578 -- {* The nontrivial case is for the @{term Cons}: *} |
579 case (Cons e t) |
579 case (Cons e t) |
580 -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} |
580 -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} |
581 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
581 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
582 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
582 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
|
583 interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto) |
583 show ?case |
584 show ?case |
584 proof - |
585 proof - |
585 -- {* It can be proved that @{term cntP}-value of @{term th'} does not change |
586 -- {* It can be proved that @{term cntP}-value of @{term th'} does not change |
586 by the happening of event @{term e}: *} |
587 by the happening of event @{term e}: *} |
587 have "cntP ((e#t)@s) th' = cntP (t@s) th'" |
588 have "cntP ((e#t)@s) th' = cntP (t@s) th'" |
589 -- {* 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}: *} |
590 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'" |
591 -- {* Then the actor of @{term e} must be @{term th'} and @{term e} |
592 -- {* Then the actor of @{term e} must be @{term th'} and @{term e} |
592 must be a @{term P}-event: *} |
593 must be a @{term P}-event: *} |
593 hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) |
594 hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) |
594 with vat_t.actor_inv[OF Cons(2)] |
595 with vat_es.actor_inv |
595 -- {* According to @{thm actor_inv}, @{term th'} must be running at |
596 -- {* According to @{thm vat_es.actor_inv}, @{term th'} must be running at |
596 the moment @{term "t@s"}: *} |
597 the moment @{term "t@s"}: *} |
597 have "th' \<in> runing (t@s)" by (cases e, auto) |
598 have "th' \<in> runing (t@s)" by (cases e, auto) |
598 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis |
599 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis |
599 shows @{term th'} can not be running at moment @{term "t@s"}: *} |
600 shows @{term th'} can not be running at moment @{term "t@s"}: *} |
600 moreover have "th' \<notin> runing (t@s)" |
601 moreover have "th' \<notin> runing (t@s)" |
607 -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} |
608 -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} |
608 moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" |
609 moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" |
609 proof(rule ccontr) -- {* Proof by contradiction. *} |
610 proof(rule ccontr) -- {* Proof by contradiction. *} |
610 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'" |
611 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'" |
611 hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) |
612 hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) |
612 with vat_t.actor_inv[OF Cons(2)] |
613 with vat_es.actor_inv |
613 have "th' \<in> runing (t@s)" by (cases e, auto) |
614 have "th' \<in> runing (t@s)" by (cases e, auto) |
614 moreover have "th' \<notin> runing (t@s)" |
615 moreover have "th' \<notin> runing (t@s)" |
615 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
616 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
616 ultimately show False by simp |
617 ultimately show False by simp |
617 qed |
618 qed |