Quelle  OAWN_Invariants.thy

(*  Title:       OAWN_Invariants.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Generic open invariants on sequential AWN processes"

theory OAWN_Invariants
imports Invariants OInvariants
        AWN_Cterms AWN_Labels AWN_Invariants
        OAWN_SOS
begin

subsection "Open invariants via labelled control terms"

lemma oseqp_sos_subterms:
  assumes "wellformed Γ"
      and "∃pn. p ∈ subterms (Γ pn)"
      and "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
    shows "∃pn. p' ∈ subterms (Γ pn)"
  using assms
  proof (induct p)
    fix p1 p2
    assume IH1: "∃pn. p1 ∈ subterms (Γ pn) ==>
                      ((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i ==>
                      ∃pn. p' ∈ subterms (Γ pn)"
       and IH2: "∃pn. p2 ∈ subterms (Γ pn) ==>
                      ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i ==>
                      ∃pn. p' ∈ subterms (Γ pn)"
       and "∃pn. p1 ⊕ p2 ∈ subterms (Γ pn)"
       and "((σ, p1 ⊕ p2), a, (σ', p')) ∈ oseqp_sos Γ i"
    from ‹∃pn. p1 ⊕ p2 ∈ subterms (Γ pn)› obtain pn
                                            where "p1 ∈ subterms (Γ pn)"
                                              and "p2 ∈ subterms (Γ pn)" by auto
    from ‹((σ, p1 ⊕ p2), a, (σ', p')) ∈ oseqp_sos Γ i›
      have "((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i
            ∨ ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i" by auto
    thus "∃pn. p' ∈ subterms (Γ pn)"
    proof
      assume "((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i"
      with ‹p1 ∈ subterms (Γ pn)› show ?thesis by (auto intro: IH1)
    next
      assume "((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i"
      with ‹p2 ∈ subterms (Γ pn)› show ?thesis by (auto intro: IH2)
    qed
  qed auto

lemma oreachable_subterms:
  assumes "wellformed Γ"
      and "control_within Γ (init A)"
      and "trans A = oseqp_sos Γ i"
      and "(σ, p) ∈ oreachable A S U"
    shows "∃pn. p ∈ subterms (Γ pn)"
  using assms(4)
  proof (induct rule: oreachable_pair_induct)
    fix σ p
    assume "(σ, p) ∈ init A"
    with ‹control_within Γ (init A)› show "∃pn. p ∈ subterms (Γ pn)" ..
  next
    fix σ p a σ' p'
    assume "(σ, p) ∈ oreachable A S U"
       and "∃pn. p ∈ subterms (Γ pn)"
       and 3: "((σ, p), a, (σ', p')) ∈ trans A"
       and "S σ σ' a"
    moreover from 3 and ‹trans A = oseqp_sos Γ i›
      have "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i" by simp
    ultimately show "∃pn. p' ∈ subterms (Γ pn)"
    using ‹wellformed Γ›
      by (auto elim: oseqp_sos_subterms)
  qed

lemma onl_oinvariantI [intro]:
  assumes init: "∧σ p l. [ (σ, p) ∈ init A; l ∈ labels Γ p ] ==> P (σ, l)"
      and other: "∧σ σ' p l. [ (σ, p) ∈ oreachable A S U;
                                ∀l∈labels Γ p. P (σ, l);
                                U σ σ' ] ==> ∀l∈labels Γ p. P (σ', l)"
      and step: "∧σ p a σ' p' l'.
                   [ (σ, p) ∈ oreachable A S U;
                     ∀l∈labels Γ p. P (σ, l);
                     ((σ, p), a, (σ', p')) ∈ trans A;
                     l' ∈ labels Γ p';
                     S σ σ' a ] ==> P (σ', l')"
    shows "A ⊨ (S, U →) onl Γ P"
  proof
    fix σ p
    assume "(σ, p) ∈ init A"
    hence "∀l∈labels Γ p. P (σ, l)" using init by simp
    thus "onl Γ P (σ, p)" ..
  next
    fix σ p a σ' p'
    assume rp: "(σ, p) ∈ oreachable A S U"
       and "onl Γ P (σ, p)"
       and tr: "((σ, p), a, (σ', p')) ∈ trans A"
       and "S σ σ' a"
    from ‹onl Γ P (σ, p)› have "∀l∈labels Γ p. P (σ, l)" ..
    with rp tr ‹S σ σ' a› have "∀l'∈labels Γ p'. P (σ', l')" by (auto elim: step)
    thus "onl Γ P (σ', p')" ..
  next
    fix σ σ' p
    assume "(σ, p) ∈ oreachable A S U"
       and "onl Γ P (σ, p)"
       and "U σ σ'"
    from ‹onl Γ P (σ, p)› have "∀l∈labels Γ p. P (σ, l)" by auto
    with ‹(σ, p) ∈ oreachable A S U› have "∀l∈labels Γ p. P (σ', l)"
        using ‹U σ σ'› by (rule other)
    thus "onl Γ P (σ', p)" by auto
  qed

lemma global_oinvariantI [intro]:
  assumes init: "∧σ p. (σ, p) ∈ init A ==> P σ"
      and other: "∧σ σ' p l. [ (σ, p) ∈ oreachable A S U; P σ; U σ σ' ] ==> P σ'"
      and step: "∧σ p a σ' p'.
                   [ (σ, p) ∈ oreachable A S U;
                     P σ;
                     ((σ, p), a, (σ', p')) ∈ trans A;
                     S σ σ' a ] ==> P σ'"
    shows "A ⊨ (S, U →) (λ(σ, _). P σ)"
  proof
    fix σ p
    assume "(σ, p) ∈ init A"
    thus "(λ(σ, _). P σ) (σ, p)"
      by simp (erule init)
  next
    fix σ p a σ' p'
    assume rp: "(σ, p) ∈ oreachable A S U"
       and "(λ(σ, _). P σ) (σ, p)"
       and tr: "((σ, p), a, (σ', p')) ∈ trans A"
       and "S σ σ' a"
    from ‹(λ(σ, _). P σ) (σ, p)› have "P σ" by simp
    with rp have "P σ'"
      using tr ‹S σ σ' a› by (rule step)
    thus "(λ(σ, _). P σ) (σ', p')" by simp
  next
    fix σ σ' p
    assume "(σ, p) ∈ oreachable A S U"
       and "(λ(σ, _). P σ) (σ, p)"
       and "U σ σ'"
    hence "P σ'" by simp (erule other)
    thus "(λ(σ, _). P σ) (σ', p)" by simp
  qed

lemma onl_oinvariantD [dest]:
  assumes "A ⊨ (S, U →) onl Γ P"
      and "(σ, p) ∈ oreachable A S U"
      and "l ∈ labels Γ p"
    shows "P (σ, l)"
  using assms unfolding onl_def by auto

lemma onl_oinvariant_weakenD [dest]:
  assumes "A ⊨ (S', U' →) onl Γ P"
      and "(σ, p) ∈ oreachable A S U"
      and "l ∈ labels Γ p"
      and weakenS: "∧s s' a. S s s' a ==> S' s s' a"
      and weakenU: "∧s s'. U s s' ==> U' s s'"
    shows "P (σ, l)"
  proof -
    from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
      by (rule oreachable_weakenE)
         (erule weakenS, erule weakenU)
    with ‹A ⊨ (S', U' →) onl Γ P› show "P (σ, l)"
      using ‹l ∈ labels Γ p› ..
  qed

lemma onl_oinvariant_initD [dest]:
  assumes invP: "A ⊨ (S, U →) onl Γ P"
      and init: "(σ, p) ∈ init A"
      and pnl:  "l ∈ labels Γ p"
    shows "P (σ, l)"
  proof -
    from init have "(σ, p) ∈ oreachable A S U" ..
    with invP show ?thesis using pnl ..
  qed

lemma onl_oinvariant_sterms:
  assumes wf: "wellformed Γ"
      and il: "A ⊨ (S, U →) onl Γ P"
      and rp: "(σ, p) ∈ oreachable A S U"
      and "p'∈sterms Γ p"
      and "l∈labels Γ p'"
    shows "P (σ, l)"
  proof -
    from wf ‹p'∈sterms Γ p› ‹l∈labels Γ p'› have "l∈labels Γ p"
      by (rule labels_sterms_labels)
    with il rp show "P (σ, l)" ..
  qed

lemma onl_oinvariant_sterms_weaken:
  assumes wf: "wellformed Γ"
      and il: "A ⊨ (S', U' →) onl Γ P"
      and rp: "(σ, p) ∈ oreachable A S U"
      and "p'∈sterms Γ p"
      and "l∈labels Γ p'"
      and weakenS: "∧σ σ' a. S σ σ' a ==> S' σ σ' a"
      and weakenU: "∧σ σ'. U σ σ' ==> U' σ σ'"
    shows "P (σ, l)"
  proof -
    from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
      by (rule oreachable_weakenE)
         (erule weakenS, erule weakenU)
    with assms(1-2) show ?thesis using assms(4-5)
      by (rule onl_oinvariant_sterms)
  qed

lemma otrans_from_sterms:
  assumes "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
      and "wellformed Γ"
    shows "∃p'∈sterms Γ p. ((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
  using assms by (induction p rule: sterms_pinduct [OF ‹wellformed Γ›]) auto

lemma otrans_from_sterms':
  assumes "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
      and "wellformed Γ"
      and "p' ∈ sterms Γ p"
    shows "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
  using assms by (induction p rule: sterms_pinduct [OF ‹wellformed Γ›]) auto

lemma otrans_to_dterms:
  assumes "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
      and "wellformed Γ"
   shows "∀r∈sterms Γ q. r ∈ dterms Γ p"
  using assms by (induction q) auto

theorem cterms_includes_sterms_of_oseq_reachable:
  assumes "wellformed Γ"
      and "control_within Γ (init A)"
      and "trans A = oseqp_sos Γ i"
    shows "∪(sterms Γ ` snd ` oreachable A S U) ⊆ cterms Γ"
  proof
    fix qs
    assume "qs ∈ ∪(sterms Γ ` snd ` oreachable A S U)"
    then obtain ξ and q where  *: "(ξ, q) ∈ oreachable A S U"
                          and **: "qs ∈ sterms Γ q" by auto
    from * have "∧x. x ∈ sterms Γ q ==> x ∈ cterms Γ"
    proof (induction rule: oreachable_pair_induct)
      fix σ p q
      assume "(σ, p) ∈ init A"
         and "q ∈ sterms Γ p"
      from ‹control_within Γ (init A)› and ‹(σ, p) ∈ init A›
        obtain pn where "p ∈ subterms (Γ pn)" by auto
      with ‹wellformed Γ› show "q ∈ cterms Γ" using ‹q∈sterms Γ p›
        by (rule subterms_sterms_in_cterms)
    next
      fix p σ a σ' q x
      assume "(σ, p) ∈ oreachable A S U"
         and IH: "∧x. x ∈ sterms Γ p ==> x ∈ cterms Γ"
         and "((σ, p), a, (σ', q)) ∈ trans A"
         and "x ∈ sterms Γ q"
      from this(3) and ‹trans A = oseqp_sos Γ i›
        have step: "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
      from step ‹wellformed Γ› obtain ps
        where ps: "ps ∈ sterms Γ p"
          and step': "((σ, ps), a, (σ', q)) ∈ oseqp_sos Γ i"
        by (rule otrans_from_sterms [THEN bexE])
      from ps have "ps ∈ cterms Γ" by (rule IH)
      moreover from step' ‹wellformed Γ› ‹x ∈ sterms Γ q› have "x ∈ dterms Γ ps"
        by (rule otrans_to_dterms [rule_format])
      ultimately show "x ∈ cterms Γ" by (rule ctermsDI)
    qed
    thus "qs ∈ cterms Γ" using ** .
  qed

corollary oseq_reachable_in_cterms:
  assumes "wellformed Γ"
      and "control_within Γ (init A)"
      and "trans A = oseqp_sos Γ i"
      and "(σ, p) ∈ oreachable A S U"
      and "p' ∈ sterms Γ p"
    shows "p' ∈ cterms Γ"
  using assms(1-3)
  proof (rule cterms_includes_sterms_of_oseq_reachable [THEN subsetD])
    from assms(4-5) show "p' ∈ ∪(sterms Γ ` snd ` oreachable A S U)"
      by (auto elim!: rev_bexI)
  qed

lemma oseq_invariant_ctermI:
  assumes wf: "wellformed Γ"
      and cw: "control_within Γ (init A)"
      and sl: "simple_labels Γ"
      and sp: "trans A = oseqp_sos Γ i"
      and init: "∧σ p l. [
                   (σ, p) ∈ init A;
                   l∈labels Γ p
                 ] ==> P (σ, l)"
      and other: "∧σ σ' p l. [
                   (σ, p) ∈ oreachable A S U;
                   l∈labels Γ p;
                   P (σ, l);
                   U σ σ' ] ==> P (σ', l)"
      and local: "∧p l σ a q l' σ' pp. [
                 p∈cterms Γ;
                 l∈labels Γ p;
                 P (σ, l);
                 ((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
                 ((σ, p), a, (σ', q)) ∈ trans A;
                 l'∈labels Γ q;
                 (σ, pp)∈oreachable A S U;
                 p∈sterms Γ pp;
                 (σ', q)∈oreachable A S U;
                 S σ σ' a
               ] ==> P (σ', l')"
    shows "A ⊨ (S, U →) onl Γ P"
  proof
       fix σ p l
    assume "(σ, p) ∈ init A"
       and *: "l ∈ labels Γ p"
      with init show "P (σ, l)" by auto
  next
       fix σ p a σ' q l'
    assume sr: "(σ, p) ∈ oreachable A S U"
       and pl: "∀l∈labels Γ p. P (σ, l)"
       and tr: "((σ, p), a, (σ', q)) ∈ trans A"
       and A6: "l' ∈ labels Γ q"
       and "S σ σ' a"
      thus "P (σ', l')"
    proof -
      from sr and tr and ‹S σ σ' a› have A7: "(σ', q) ∈ oreachable A S U"
        by - (rule oreachable_local')
      from tr and sp have tr': "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
      then obtain p' where "p' ∈ sterms Γ p"
                       and A4: "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
        by (blast dest: otrans_from_sterms [OF _ wf])
      from wf cw sp sr this(1) have A1: "p'∈cterms Γ"
        by (rule oseq_reachable_in_cterms)
      from labels_not_empty [OF wf] obtain ll where A2: "ll∈labels Γ p'"
          by blast
      with ‹p'∈sterms Γ p› have "ll∈labels Γ p"
        by (rule labels_sterms_labels [OF wf])
      with pl have A3: "P (σ, ll)" by simp
      from sr ‹p'∈sterms Γ p›
        obtain pp where A7: "(σ, pp)∈oreachable A S U"
                    and A8: "p'∈sterms Γ pp"
        by auto
      from sr tr ‹S σ σ' a› have A9: "(σ', q)∈oreachable A S U"
        by - (rule oreachable_local')
      from sp and ‹((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i›
        have A5: "((σ, p'), a, (σ', q)) ∈ trans A" by simp
      from A1 A2 A3 A4 A5 A6 A7 A8 A9 ‹S σ σ' a› show ?thesis by (rule local)
    qed
  next
    fix σ σ' p l
    assume sr: "(σ, p) ∈ oreachable A S U"
       and "∀l∈labels Γ p. P (σ, l)"
       and "U σ σ'"
    show "∀l∈labels Γ p. P (σ', l)"
    proof
      fix l
      assume "l∈labels Γ p"
      with ‹∀l∈labels Γ p. P (σ, l)› have "P (σ, l)" ..
      with sr and ‹l∈labels Γ p›
        show "P (σ', l)" using ‹U σ σ'› by (rule other)
    qed
  qed

lemma oseq_invariant_ctermsI:
  assumes wf: "wellformed Γ"
      and cw: "control_within Γ (init A)"
      and sl: "simple_labels Γ"
      and sp: "trans A = oseqp_sos Γ i"
      and init: "∧σ p l. [
                   (σ, p) ∈ init A;
                   l∈labels Γ p
                 ] ==> P (σ, l)"
      and other: "∧σ σ' p l. [
                   wellformed Γ;
                   (σ, p) ∈ oreachable A S U;
                   l∈labels Γ p;
                   P (σ, l);
                   U σ σ' ] ==> P (σ', l)"
      and local: "∧p l σ a q l' σ' pp pn. [
                 wellformed Γ;
                 p∈ctermsl (Γ pn);
                 not_call p;
                 l∈labels Γ p;
                 P (σ, l);
                 ((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
                 ((σ, p), a, (σ', q)) ∈ trans A;
                 l'∈labels Γ q;
                 (σ, pp)∈oreachable A S U;
                 p∈sterms Γ pp;
                 (σ', q)∈oreachable A S U;
                 S σ σ' a
               ] ==> P (σ', l')"
    shows "A ⊨ (S, U →) onl Γ P"
  proof (rule oseq_invariant_ctermI [OF wf cw sl sp])
    fix σ p l
    assume "(σ, p) ∈ init A"
       and "l ∈ labels Γ p"
    thus "P (σ, l)" by (rule init)
  next
    fix σ σ' p l
    assume "(σ, p) ∈ oreachable A S U"
       and "l ∈ labels Γ p"
       and "P (σ, l)"
       and "U σ σ'"
    with wf show "P (σ', l)" by (rule other)
  next
    fix p l σ a q l' σ' pp
    assume "p ∈ cterms Γ"
       and otherassms: "l ∈ labels Γ p"
           "P (σ, l)"
           "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
           "((σ, p), a, (σ', q)) ∈ trans A"
           "l' ∈ labels Γ q"
           "(σ, pp) ∈ oreachable A S U"
           "p ∈ sterms Γ pp"
           "(σ', q) ∈ oreachable A S U"
           "S σ σ' a"
    from this(1) obtain pn where "p ∈ ctermsl(Γ pn)"
                             and "not_call p"
      unfolding cterms_def' [OF wf] by auto
    with wf show "P (σ', l')"
      using otherassms by (rule local)
  qed

subsection "Open step invariants via labelled control terms"

lemma onll_ostep_invariantI [intro]:
  assumes *: "∧σ p l a σ' p' l'. [ (σ, p)∈oreachable A S U;
                                   ((σ, p), a, (σ', p')) ∈ trans A;
                                   S σ σ' a;
                                   l ∈labels Γ p;
                                   l'∈labels Γ p' ]
                                 ==> P ((σ, l), a, (σ', l'))"
    shows "A ⊨_A (S, U →) onll Γ P"
  proof
    fix σ p σ' p' a
    assume "(σ, p) ∈ oreachable A S U"
       and "((σ, p), a, (σ', p')) ∈ trans A"
       and "S σ σ' a"
    hence "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((σ, l), a, (σ', l'))" by (auto elim!: *)
    thus "onll Γ P ((σ, p), a, (σ', p'))" ..
  qed

lemma onll_ostep_invariantE [elim]:
  assumes "A ⊨_A (S, U →) onll Γ P"
      and "(σ, p) ∈ oreachable A S U"
      and "((σ, p), a, (σ', p')) ∈ trans A"
      and "S σ σ' a"
      and lp:  "l ∈labels Γ p"
      and lp': "l'∈labels Γ p'"
    shows "P ((σ, l), a, (σ', l'))"
  proof -
    from assms(1-4) have "onll Γ P ((σ, p), a, (σ', p'))" ..
    with lp lp' show "P ((σ, l), a, (σ', l'))" by auto
  qed

lemma onll_ostep_invariantD [dest]:
  assumes "A ⊨_A (S, U →) onll Γ P"
      and "(σ, p) ∈ oreachable A S U"
      and "((σ, p), a, (σ', p')) ∈ trans A"
      and "S σ σ' a"
    shows "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((σ, l), a, (σ', l'))"
  using assms by auto

lemma onll_ostep_invariant_weakenD [dest]:
  assumes "A ⊨_A (S', U' →) onll Γ P"
      and "(σ, p) ∈ oreachable A S U"
      and "((σ, p), a, (σ', p')) ∈ trans A"
      and "S' σ σ' a"
      and weakenS: "∧s s' a. S s s' a ==> S' s s' a"
      and weakenU: "∧s s'. U s s' ==> U' s s'"
    shows "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((σ, l), a, (σ', l'))"
  proof -
    from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
      by (rule oreachable_weakenE)
         (erule weakenS, erule weakenU)
    with ‹A ⊨_A (S', U' →) onll Γ P› show ?thesis
      using ‹((σ, p), a, (σ', p')) ∈ trans A› and ‹S' σ σ' a› ..
  qed

lemma onll_ostep_to_invariantI [intro]:
  assumes sinv: "A ⊨_A (S, U →) onll Γ Q"
      and wf: "wellformed Γ"
      and init: "∧σ l p. [ (σ, p) ∈ init A; l∈labels Γ p ] ==> P (σ, l)"
      and other: "∧σ σ' p l.
                    [ (σ, p) ∈ oreachable A S U;
                      l∈labels Γ p;
                      P (σ, l);
                      U σ σ' ] ==> P (σ', l)"
      and local: "∧σ p l σ' l' a.
                    [ (σ, p) ∈ oreachable A S U;
                      l∈labels Γ p;
                      P (σ, l);
                      Q ((σ, l), a, (σ', l'));
                      S σ σ' a] ==> P (σ', l')"
    shows "A ⊨ (S, U →) onl Γ P"
  proof
    fix σ p l
    assume "(σ, p) ∈ init A" and "l∈labels Γ p"
      thus "P (σ, l)" by (rule init)
  next
    fix σ p a σ' p' l'
    assume sr: "(σ, p) ∈ oreachable A S U"
       and lp: "∀l∈labels Γ p. P (σ, l)"
       and tr: "((σ, p), a, (σ', p')) ∈ trans A"
       and "S σ σ' a"
       and lp': "l' ∈ labels Γ p'"
      show "P (σ', l')"
    proof -
      from lp obtain l where "l∈labels Γ p" and "P (σ, l)"
        using labels_not_empty [OF wf] by auto
      from sinv sr tr ‹S σ σ' a› this(1) lp' have "Q ((σ, l), a, (σ', l'))" ..
      with sr ‹l∈labels Γ p› ‹P (σ, l)› show "P (σ', l')" using ‹S σ σ' a› by (rule local)
    qed
  next
    fix σ σ' p l
    assume "(σ, p) ∈ oreachable A S U"
       and "∀l∈labels Γ p. P (σ, l)"
       and "U σ σ'"
      show "∀l∈labels Γ p. P (σ', l)"
    proof
      fix l
      assume "l∈labels Γ p"
      with ‹∀l∈labels Γ p. P (σ, l)› have "P (σ, l)" ..
      with ‹(σ, p) ∈ oreachable A S U› and ‹l∈labels Γ p›
      show "P (σ', l)" using ‹U σ σ'› by (rule other)
    qed
  qed

lemma onll_ostep_invariant_sterms:
  assumes wf: "wellformed Γ"
      and si: "A ⊨_A (S, U →) onll Γ P"
      and sr: "(σ, p) ∈ oreachable A S U"
      and sos: "((σ, p), a, (σ', q)) ∈ trans A"
      and "S σ σ' a"
      and "l'∈labels Γ q"
      and "p'∈sterms Γ p"
      and "l∈labels Γ p'"
    shows "P ((σ, l), a, (σ', l'))"
  proof -
    from wf ‹p'∈sterms Γ p› ‹l∈labels Γ p'› have "l∈labels Γ p"
      by (rule labels_sterms_labels)
    with si sr sos ‹S σ σ' a› show "P ((σ, l), a, (σ', l'))" using ‹l'∈labels Γ q› ..
  qed

lemma oseq_step_invariant_sterms:
  assumes inv: "A ⊨_A (S, U →) onll Γ P"
      and wf: "wellformed Γ"
      and sp: "trans A = oseqp_sos Γ i"
      and "l'∈labels Γ q"
      and sr: "(σ, p) ∈ oreachable A S U"
      and tr: "((σ, p'), a, (σ', q)) ∈ trans A"
      and "S σ σ' a"
      and "p'∈sterms Γ p"
    shows "∀l∈labels Γ p'. P ((σ, l), a, (σ', l'))"
  proof
    from assms(3, 6) have "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
    hence "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
      using wf ‹p'∈sterms Γ p›  by (rule otrans_from_sterms')
    with assms(3) have trp: "((σ, p), a, (σ', q)) ∈ trans A" by simp
    fix l assume "l ∈ labels Γ p'"
    with wf inv sr trp ‹S σ σ' a› ‹l'∈labels Γ q› ‹p'∈sterms Γ p›
      show "P ((σ, l), a, (σ', l'))"
        by - (erule(7) onll_ostep_invariant_sterms)
  qed

lemma oseq_step_invariant_sterms_weaken:
  assumes inv: "A ⊨_A (S, U →) onll Γ P"
      and wf: "wellformed Γ"
      and sp: "trans A = oseqp_sos Γ i"
      and "l'∈labels Γ q"
      and sr: "(σ, p) ∈ oreachable A S' U'"
      and tr: "((σ, p'), a, (σ', q)) ∈ trans A"
      and "S' σ σ' a"
      and "p'∈sterms Γ p"
      and weakenS: "∧σ σ' a. S' σ σ' a ==> S σ σ' a"
      and weakenU: "∧σ σ'. U' σ σ' ==> U σ σ'"
    shows "∀l∈labels Γ p'. P ((σ, l), a, (σ', l'))"
  proof -
    from ‹S' σ σ' a› have "S σ σ' a" by (rule weakenS)
    from ‹(σ, p) ∈ oreachable A S' U'›
      have Ir: "(σ, p) ∈ oreachable A S U"
        by (rule oreachable_weakenE)
           (erule weakenS, erule weakenU)
    with assms(1-4) show ?thesis
      using tr ‹S σ σ' a› ‹p'∈sterms Γ p›
      by (rule oseq_step_invariant_sterms)
  qed

lemma onll_ostep_invariant_any_sterms:
  assumes wf: "wellformed Γ"
      and si: "A ⊨_A (S, U →) onll Γ P"
      and sr: "(σ, p) ∈ oreachable A S U"
      and sos: "((σ, p), a, (σ', q)) ∈ trans A"
      and "S σ σ' a"
      and "l'∈labels Γ q"
    shows "∀p'∈sterms Γ p. ∀l∈labels Γ p'. P ((σ, l), a, (σ', l'))"
  by (intro ballI) (rule onll_ostep_invariant_sterms [OF assms])

lemma oseq_step_invariant_ctermI [intro]:
  assumes wf: "wellformed Γ"
      and cw: "control_within Γ (init A)"
      and sl: "simple_labels Γ"
      and sp: "trans A = oseqp_sos Γ i"
      and local: "∧p l σ a q l' σ' pp. [
                   p∈cterms Γ;
                   l∈labels Γ p;
                   ((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
                   ((σ, p), a, (σ', q)) ∈ trans A;
                   l'∈labels Γ q;
                   (σ, pp) ∈ oreachable A S U;
                   p∈sterms Γ pp;
                   (σ', q) ∈ oreachable A S U;
                   S σ σ' a
                 ] ==> P ((σ, l), a, (σ', l'))"
    shows "A ⊨_A (S, U →) onll Γ P"
  proof
       fix σ p l a σ' q l'
    assume sr: "(σ, p) ∈ oreachable A S U"
       and tr: "((σ, p), a, (σ', q)) ∈ trans A"
       and "S σ σ' a"
       and pl: "l ∈ labels Γ p"
       and A5: "l' ∈ labels Γ q"
    from this(2) and sp have "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i" by simp
    then obtain p' where "p' ∈ sterms Γ p"
                     and A3: "((σ, p'), a, (σ', q)) ∈ oseqp_sos Γ i"
      by (blast dest: otrans_from_sterms [OF _ wf])
    from this(2) and sp have A4: "((σ, p'), a, (σ', q)) ∈ trans A" by simp
    from wf cw sp sr ‹p'∈sterms Γ p› have A1: "p'∈cterms Γ"
      by (rule oseq_reachable_in_cterms)
    from sr ‹p'∈sterms Γ p›
      obtain pp where A6: "(σ, pp)∈oreachable A S U"
                  and A7: "p'∈sterms Γ pp"
      by auto
    from sr tr ‹S σ σ' a› have A8: "(σ', q)∈oreachable A S U"
      by - (erule(2) oreachable_local')
    from wf cw sp sr have "∃pn. p ∈ subterms (Γ pn)"
      by (rule oreachable_subterms)           
    with sl wf have "∀p'∈sterms Γ p. l ∈ labels Γ p'"
      using pl by (rule simple_labels_in_sterms)
    with ‹p' ∈ sterms Γ p› have "l ∈ labels Γ p'" by simp
    with A1 show "P ((σ, l), a, (σ', l'))" using A3 A4 A5 A6 A7 A8 ‹S σ σ' a›
      by (rule local)
  qed

lemma oseq_step_invariant_ctermsI [intro]:
  assumes wf: "wellformed Γ"
      and "control_within Γ (init A)"
      and "simple_labels Γ"
      and "trans A = oseqp_sos Γ i"
      and local: "∧p l σ a q l' σ' pp pn. [
                   wellformed Γ;
                   p∈ctermsl (Γ pn);
                   not_call p;
                   l∈labels Γ p;
                   ((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i;
                   ((σ, p), a, (σ', q)) ∈ trans A;
                   l'∈labels Γ q;
                   (σ, pp) ∈ oreachable A S U;
                   p∈sterms Γ pp;
                   (σ', q) ∈ oreachable A S U;
                   S σ σ' a
                 ] ==> P ((σ, l), a, (σ', l'))"
    shows "A ⊨_A (S, U →) onll Γ P"
  using assms(1-4) proof (rule oseq_step_invariant_ctermI)
    fix p l σ a q l' σ' pp
    assume "p ∈ cterms Γ"
       and otherassms: "l ∈ labels Γ p"
           "((σ, p), a, (σ', q)) ∈ oseqp_sos Γ i"
           "((σ, p), a, (σ', q)) ∈ trans A"
           "l' ∈ labels Γ q"
           "(σ, pp) ∈ oreachable A S U"
           "p ∈ sterms Γ pp"
           "(σ', q) ∈ oreachable A S U"
           "S σ σ' a"
    from this(1) obtain pn where "p ∈ ctermsl(Γ pn)"
                             and "not_call p"
      unfolding cterms_def' [OF wf] by auto
    with wf show "P ((σ, l), a, (σ', l'))"
      using otherassms by (rule local)
 qed

lemma open_seqp_action [elim]:
  assumes "wellformed Γ"
      and "((σ i, p), a, (σ' i, p')) ∈ seqp_sos Γ"
    shows "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
  proof -
    from assms obtain ps where "ps∈sterms Γ p"
                           and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
      by - (drule trans_from_sterms, auto)
    thus ?thesis
    proof (induction p)
      fix p1 p2
      assume "[ ps ∈ sterms Γ p1; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ]
              ==> ((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i"
         and "[ ps ∈ sterms Γ p2; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ]
              ==> ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i"
         and "ps ∈ sterms Γ (p1 ⊕ p2)"
         and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
      with assms(1) show "((σ, p1 ⊕ p2), a, (σ', p')) ∈ oseqp_sos Γ i"
        by simp (metis oseqp_sos.ochoiceT1 oseqp_sos.ochoiceT2)
    next
      fix l fip fmsg p1 p2
      assume IH1: "[ ps ∈ sterms Γ p1; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ]
                    ==> ((σ, p1), a, (σ', p')) ∈ oseqp_sos Γ i"
         and IH2: "[ ps ∈ sterms Γ p2; ((σ i, ps), a, σ' i, p') ∈ seqp_sos Γ ]
                    ==> ((σ, p2), a, (σ', p')) ∈ oseqp_sos Γ i"
         and "ps ∈ sterms Γ ({l}unicast(fip, fmsg). p1 ▹ p2)"
         and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
      from this(3-4) have "((σ i, {l}unicast(fip, fmsg). p1 ▹ p2), a, (σ' i, p')) ∈ seqp_sos Γ"
        by simp
      thus "((σ, {l}unicast(fip, fmsg). p1 ▹ p2), a, (σ', p')) ∈ oseqp_sos Γ i"
      proof (rule seqp_unicastTE)
        assume "a = unicast (fip (σ i)) (fmsg (σ i))"
           and "σ' i = σ i"
           and "p' = p1"
        thus ?thesis by auto
      next
        assume "a = ¬unicast (fip (σ i))"
           and "σ' i = σ i"
           and "p' = p2"
        thus ?thesis by auto
      qed
    next
      fix p
      assume "ps ∈ sterms Γ (call(p))"
         and "((σ i, ps), a, (σ' i, p')) ∈ seqp_sos Γ"
      with assms(1) have "((σ, ps), a, (σ', p')) ∈ oseqp_sos Γ i"
        by (cases ps) auto
      with assms(1) ‹ps ∈ sterms Γ (call(p))› have "((σ, Γ p), a, (σ', p')) ∈ oseqp_sos Γ i"
        by - (rule otrans_from_sterms', simp_all)
      thus "((σ, call(p)), a, (σ', p')) ∈ oseqp_sos Γ i" by auto
    qed auto
  qed

end