Theory AWN_Invariants

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

section "Generic invariants on sequential AWN processes"

theory AWN_Invariants
imports Invariants AWN_SOS AWN_Labels
begin

subsection "Invariants via labelled control terms"

text ‹
  Used to state that the initial control-state of an automaton appears within a process
  specification ‹Γ›, meaning that its transitions, and those of its subterms, are
  subsumed by those of ‹Γ›.
›

definition
  control_within :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('z × ('s, 'm, 'p, 'l) seqp) set ⇒ bool"
where
  "control_within Γ σ ≡ ∀(ξ, p)∈σ. ∃pn. p ∈ subterms (Γ pn)"

lemma control_withinI [intro]:
  assumes "⋀p. p ∈ Range σ ⟹ ∃pn. p ∈ subterms (Γ pn)"
    shows "control_within Γ σ"
  using assms unfolding control_within_def by auto

lemma control_withinD [dest]:
  assumes "control_within Γ σ"
      and "(ξ, p) ∈ σ"
    shows "∃pn. p ∈ subterms (Γ pn)"
  using assms unfolding control_within_def by blast

lemma control_within_topI [intro]:
  assumes "⋀p. p ∈ Range σ ⟹ ∃pn. p = Γ pn"
    shows "control_within Γ σ"
  using assms unfolding control_within_def
  by clarsimp (metis Range.RangeI subterms_refl)

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

lemma reachable_subterms:
  assumes "wellformed Γ"
      and "control_within Γ (init A)"
      and "trans A = seqp_sos Γ"
      and "(ξ, p) ∈ reachable A I"
    shows "∃pn. p ∈ subterms (Γ pn)"
  using assms(4)
  proof (induct rule: reachable_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) ∈ reachable A I"
       and "∃pn. p ∈ subterms (Γ pn)"
       and *: "((ξ, p), a, (ξ', p')) ∈ trans A"
       and "I a"
    moreover from * and assms(3) have "((ξ, p), a, (ξ', p')) ∈ seqp_sos Γ" by simp
    ultimately show "∃pn. p' ∈ subterms (Γ pn)"
    using ‹wellformed Γ›
      by (auto elim: seqp_sos_subterms)
  qed

definition
  onl :: "('s, 'm, 'p, 'l) seqp_env
           ⇒ ('z × 'l ⇒ bool)
           ⇒ 'z × ('s, 'm, 'p, 'l) seqp
           ⇒ bool"
where
  "onl Γ P ≡ (λ(ξ, p). ∀l∈labels Γ p. P (ξ, l))"

lemma onlI [intro]:
  assumes "⋀l. l∈labels Γ p ⟹ P (ξ, l)"
    shows "onl Γ P (ξ, p)"
  using assms unfolding onl_def by simp

lemmas onlI' [intro] = onlI [simplified atomize_ball]

lemma onlD [dest]:
  assumes "onl Γ P (ξ, p)"
    shows "∀l∈labels Γ p. P (ξ, l)"
  using assms unfolding onl_def by simp

lemma onl_invariantI [intro]:
  assumes init: "⋀ξ p l. ⟦ (ξ, p) ∈ init A; l ∈ labels Γ p ⟧ ⟹ P (ξ, l)"
      and step: "⋀ξ p a ξ' p' l'.
                   ⟦ (ξ, p) ∈ reachable A I;
                     ∀l∈labels Γ p. P (ξ, l);
                     ((ξ, p), a, (ξ', p')) ∈ trans A;
                     l' ∈ labels Γ p';
                     I a ⟧ ⟹ P (ξ', l')"
    shows "A ⊫ (I →) onl Γ P"
  proof (rule invariant_pairI)
    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) ∈ reachable A I"
       and "onl Γ P (ξ, p)"
       and tr: "((ξ, p), a, (ξ', p')) ∈ trans A"
       and "I a"
    from ‹onl Γ P (ξ, p)› have "∀l∈labels Γ p. P (ξ, l)" ..
    with rp tr ‹I a› have "∀l'∈labels Γ p'. P (ξ', l')" by (auto elim: step)
    thus "onl Γ P (ξ', p')" ..
  qed

lemma onl_invariantD [dest]:
  assumes "A ⊫ (I →) onl Γ P"
      and "(ξ, p) ∈ reachable A I"
      and "l ∈ labels Γ p"
    shows "P (ξ, l)"
  using assms unfolding onl_def by auto

lemma onl_invariant_initD [dest]:
  assumes invP: "A ⊫ (I →) onl Γ P"
      and init: "(ξ, p) ∈ init A"
      and pnl:  "l ∈ labels Γ p"
    shows "P (ξ, l)"
  proof -
    from init have "(ξ, p) ∈ reachable A I" ..
    with invP show ?thesis using pnl ..
  qed

lemma onl_invariant_sterms:
  assumes wf: "wellformed Γ"
      and il: "A ⊫ (I →) onl Γ P"
      and rp: "(ξ, p) ∈ reachable A I"
      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_invariant_sterms_weaken:
  assumes wf: "wellformed Γ"
      and il: "A ⊫ (I →) onl Γ P"
      and rp: "(ξ, p) ∈ reachable A I'"
      and "p'∈sterms Γ p"
      and "l∈labels Γ p'"
      and weaken: "⋀a. I' a ⟹ I a"
    shows "P (ξ, l)"
  proof -
    from ‹(ξ, p) ∈ reachable A I'› have "(ξ, p) ∈ reachable A I"
      by (rule reachable_weakenE)
         (erule weaken)
    with assms(1-2) show ?thesis using assms(4-5) by (rule onl_invariant_sterms)
  qed

lemma onl_invariant_sterms_TT:
  assumes wf: "wellformed Γ"
      and il: "A ⊫ onl Γ P"
      and rp: "(ξ, p) ∈ reachable A I"
      and "p'∈sterms Γ p"
      and "l∈labels Γ p'"
    shows "P (ξ, l)"
  using assms by (rule onl_invariant_sterms_weaken) simp

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

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

lemma trans_to_dterms:
  assumes "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ"
      and "wellformed Γ"
   shows "∀r∈sterms Γ q. r ∈ dterms Γ p"
  using assms by (induction q) auto

theorem cterms_includes_sterms_of_seq_reachable:
  assumes "wellformed Γ"
      and "control_within Γ (init A)"
      and "trans A = seqp_sos Γ"
    shows "⋃(sterms Γ ` snd ` reachable A I) ⊆ cterms Γ"
  proof
    fix qs
    assume "qs ∈ ⋃(sterms Γ ` snd ` reachable A I)"
    then obtain ξ and q where  *: "(ξ, q) ∈ reachable A I"
                          and **: "qs ∈ sterms Γ q" by auto
    from * have "⋀x. x ∈ sterms Γ q ⟹ x ∈ cterms Γ"
    proof (induction rule: reachable_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) ∈ reachable A I"
         and IH: "⋀x. x ∈ sterms Γ p ⟹ x ∈ cterms Γ"
         and "((ξ, p), a, (ξ', q)) ∈ trans A"
         and "x ∈ sterms Γ q"
      from this(3) and ‹trans A = seqp_sos Γ› have "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ" by simp
      from this and ‹wellformed Γ› obtain ps
        where ps: "ps ∈ sterms Γ p"
          and step: "((ξ, ps), a, (ξ', q)) ∈ seqp_sos Γ"
        by (rule trans_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 trans_to_dterms [rule_format])
      ultimately show "x ∈ cterms Γ" by (rule ctermsDI)
    qed
    thus "qs ∈ cterms Γ" using ** .
  qed

corollary seq_reachable_in_cterms:
  assumes "wellformed Γ"
      and "control_within Γ (init A)"
      and "trans A = seqp_sos Γ"
      and "(ξ, p) ∈ reachable A I"
      and "p' ∈ sterms Γ p"
    shows "p' ∈ cterms Γ"
  using assms(1-3)
  proof (rule cterms_includes_sterms_of_seq_reachable [THEN subsetD])
    from assms(4-5) show "p' ∈ ⋃(sterms Γ ` snd ` reachable A I)"
      by (auto elim!: rev_bexI)
  qed

lemma seq_invariant_ctermI:
  assumes wf: "wellformed Γ"
      and cw: "control_within Γ (init A)"
      and sl: "simple_labels Γ"
      and sp: "trans A = seqp_sos Γ"
      and init: "⋀ξ p l. ⟦
                   (ξ, p) ∈ init A;
                   l∈labels Γ p
                 ⟧ ⟹ P (ξ, l)"
      and step: "⋀p l ξ a q l' ξ' pp. ⟦
                 p∈cterms Γ;
                 l∈labels Γ p;
                 P (ξ, l);
                 ((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ;
                 ((ξ, p), a, (ξ', q)) ∈ trans A;
                 l'∈labels Γ q;
                 (ξ, pp)∈reachable A I;
                 p∈sterms Γ pp;
                 (ξ', q)∈reachable A I;
                 I a
               ⟧ ⟹ P (ξ', l')"
    shows "A ⊫ (I →) 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) ∈ reachable A I"
       and pl: "∀l∈labels Γ p. P (ξ, l)"
       and tr: "((ξ, p), a, (ξ', q)) ∈ trans A"
       and A6: "l' ∈ labels Γ q"
       and "I a"
     from this(3) and ‹trans A = seqp_sos Γ› have tr': "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ" by simp
     show "P (ξ', l')"
    proof -
      from sr and tr and ‹I a› have A7: "(ξ', q) ∈ reachable A I" ..
      from tr' obtain p' where "p' ∈ sterms Γ p"
                           and "((ξ, p'), a, (ξ', q)) ∈ seqp_sos Γ"
        by (blast dest: trans_from_sterms [OF _ wf])
      from wf cw sp sr this(1) have A1: "p'∈cterms Γ"
        by (rule seq_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 ‹((ξ, p'), a, (ξ', q)) ∈ seqp_sos Γ› and sp
        have A5: "((ξ, p'), a, (ξ', q)) ∈ trans A" by simp
      with sp have A4: "((ξ, p'), a, (ξ', q)) ∈ seqp_sos Γ" by simp
      from sr ‹p'∈sterms Γ p›
        obtain pp where A7: "(ξ, pp)∈reachable A I"
                    and A8: "p'∈sterms Γ pp"
        by auto
      from sr tr ‹I a› have A9: "(ξ', q) ∈ reachable A I" ..
      from A1 A2 A3 A4 A5 A6 A7 A8 A9 ‹I a› show ?thesis by (rule step)
    qed
  qed

lemma seq_invariant_ctermsI:
  assumes wf: "wellformed Γ"
      and "control_within Γ (init A)"
      and "simple_labels Γ"
      and "trans A = seqp_sos Γ"
      and init: "⋀ξ p l. ⟦
                   (ξ, p) ∈ init A;
                   l∈labels Γ p
                 ⟧ ⟹ P (ξ, l)"
      and step: "⋀p l ξ a q l' ξ' pp pn. ⟦
                 wellformed Γ;
                 p∈ctermsl (Γ pn);
                 not_call p;
                 l∈labels Γ p;
                 P (ξ, l);
                 ((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ;
                 ((ξ, p), a, (ξ', q)) ∈ trans A;
                 l'∈labels Γ q;
                 (ξ, pp)∈reachable A I;
                 p∈sterms Γ pp;
                 (ξ', q)∈reachable A I;
                 I a
               ⟧ ⟹ P (ξ', l')"
    shows "A ⊫ (I →) onl Γ P"
  using assms(1-4) proof (rule seq_invariant_ctermI)
    fix ξ p l
    assume "(ξ, p) ∈ init A"
       and "l ∈ labels Γ p"
    thus "P (ξ, l)" by (rule init)
  next
    fix p l ξ a q l' ξ' pp
    assume "p ∈ cterms Γ"
       and otherassms: "l ∈ labels Γ p"
           "P (ξ, l)"
           "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ"
           "((ξ, p), a, (ξ', q)) ∈ trans A"
           "l' ∈ labels Γ q"
           "(ξ, pp) ∈ reachable A I"
           "p ∈ sterms Γ pp"
           "(ξ', q) ∈ reachable A I"
           "I 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 step)
  qed

subsection "Step invariants via labelled control terms"

definition
  onll :: "('s, 'm, 'p, 'l) seqp_env
           ⇒ (('z × 'l, 'a) transition ⇒ bool)
           ⇒ ('z × ('s, 'm, 'p, 'l) seqp, 'a) transition ⇒ bool"
where
  "onll Γ P ≡ (λ((ξ, p), a, (ξ', p')). ∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((ξ, l), a, (ξ', l')))"

lemma onllI [intro]:
  assumes "⋀l l'. ⟦ l∈labels Γ p; l'∈labels Γ p' ⟧ ⟹ P ((ξ, l), a, (ξ', l'))"
    shows "onll Γ P ((ξ, p), a, (ξ', p'))"
  using assms unfolding onll_def by simp

lemma onllIl [intro]:
  assumes "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
    shows "onll Γ P ((ξ, p), a, (ξ', p'))"
  using assms by auto

lemma onllD [dest]:
  assumes "onll Γ P ((ξ, p), a, (ξ', p'))"
    shows "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
  using assms unfolding onll_def by simp

lemma onl_weaken [elim!]: "⋀Γ P Q s. ⟦ onl Γ P s; ⋀s. P s ⟹ Q s ⟧ ⟹ onl Γ Q s"
  by (clarsimp dest!: onlD intro!: onlI)

lemma onll_weaken [elim!]: "⋀Γ P Q s. ⟦ onll Γ P s; ⋀s. P s ⟹ Q s ⟧ ⟹ onll Γ Q s"
  by (clarsimp dest!: onllD intro!: onllI)

lemma onll_weaken' [elim!]: "⋀Γ P Q s. ⟦ onll Γ P ((ξ, p), a, (ξ', p'));
                                        ⋀l l'. P ((ξ, l), a, (ξ', l')) ⟹ Q ((ξ, l), a, (ξ', l')) ⟧
                                      ⟹ onll Γ Q ((ξ, p), a, (ξ', p'))"
  by (clarsimp dest!: onllD intro!: onllI)

lemma onll_step_invariantI [intro]:
  assumes *: "⋀ξ p l a ξ' p' l'. ⟦ (ξ, p)∈reachable A I;
                                   ((ξ, p), a, (ξ', p')) ∈ trans A;
                                   I a;
                                   l ∈labels Γ p;
                                   l'∈labels Γ p' ⟧
                                 ⟹ P ((ξ, l), a, (ξ', l'))"
    shows "A ⊫⇩A (I →) onll Γ P"
  proof
    fix ξ p ξ' p' a
    assume "(ξ, p) ∈ reachable A I"
       and "((ξ, p), a, (ξ', p')) ∈ trans A"
       and "I a"
    hence "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((ξ, l), a, (ξ', l'))" by (auto elim!: *)
    thus "onll Γ P ((ξ, p), a, (ξ', p'))" ..
  qed

lemma onll_step_invariantE [elim]:
  assumes "A ⊫⇩A (I →) onll Γ P"
      and "(ξ, p) ∈ reachable A I"
      and "((ξ, p), a, (ξ', p')) ∈ trans A"
      and "I 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_step_invariantD [dest]:
  assumes "A ⊫⇩A (I →) onll Γ P"
      and "(ξ, p) ∈ reachable A I"
      and "((ξ, p), a, (ξ', p')) ∈ trans A"
      and "I a"
    shows "∀l∈labels Γ p. ∀l'∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
  using assms by auto

lemma onll_step_to_invariantI [intro]:
  assumes sinv: "A ⊫⇩A (I →) onll Γ Q"
      and wf: "wellformed Γ"
      and init: "⋀ξ l p. ⟦ (ξ, p) ∈ init A; l∈labels Γ p ⟧ ⟹ P (ξ, l)"
      and step: "⋀ξ p l ξ' l' a.
                   ⟦ (ξ, p) ∈ reachable A I;
                     l∈labels Γ p;
                     P (ξ, l);
                     Q ((ξ, l), a, (ξ', l'));
                     I a⟧ ⟹ P (ξ', l')"
    shows "A ⊫ (I →) 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) ∈ reachable A I"
       and lp: "∀l∈labels Γ p. P (ξ, l)"
       and tr: "((ξ, p), a, (ξ', p')) ∈ trans A"
       and "I 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 ‹I a› this(1) lp' have "Q ((ξ, l), a, (ξ', l'))" ..
      with sr ‹l∈labels Γ p› ‹P (ξ, l)› show "P (ξ', l')" using ‹I a› by (rule step)
    qed
  qed

lemma onll_step_invariant_sterms:
  assumes wf: "wellformed Γ"
      and si: "A ⊫⇩A (I →) onll Γ P"
      and sr: "(ξ, p) ∈ reachable A I"
      and sos: "((ξ, p), a, (ξ', q)) ∈ trans A"
      and "I 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 ‹I a› show "P ((ξ, l), a, (ξ', l'))" using ‹l'∈labels Γ q› ..
  qed

lemma seq_step_invariant_sterms:
  assumes inv: "A ⊫⇩A (I →) onll Γ P"
      and wf: "wellformed Γ"
      and sp: "trans A = seqp_sos Γ"
      and "l'∈labels Γ q"
      and sr: "(ξ, p) ∈ reachable A I"
      and tr: "((ξ, p'), a, (ξ', q)) ∈ trans A"
      and "I a"
      and "p'∈sterms Γ p"
    shows "∀l∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
  proof
    from tr and sp have "((ξ, p'), a, (ξ', q)) ∈ seqp_sos Γ" by simp
    hence "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ"
      using wf ‹p'∈sterms Γ p› by  (rule trans_from_sterms')
    with sp have trp: "((ξ, p), a, (ξ', q)) ∈ trans A" by simp
    fix l assume "l ∈ labels Γ p'"
    with wf inv sr trp ‹I a› ‹l'∈labels Γ q› ‹p'∈sterms Γ p›
      show "P ((ξ, l), a, (ξ', l'))" by (rule onll_step_invariant_sterms)
  qed

lemma seq_step_invariant_sterms_weaken:
  assumes "A ⊫⇩A (I →) onll Γ P"
      and "wellformed Γ"
      and "trans A = seqp_sos Γ"
      and "l'∈labels Γ q"
      and "(ξ, p) ∈ reachable A I'"
      and "((ξ, p'), a, (ξ', q)) ∈ trans A"
      and "I' a"
      and "p'∈sterms Γ p"
      and weaken: "⋀a. I' a ⟹ I a"
    shows "∀l∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
  proof -
    from ‹I' a› have "I a" by (rule weaken)
    from ‹(ξ, p) ∈ reachable A I'› have Ir: "(ξ, p) ∈ reachable A I"
        by (rule reachable_weakenE) (erule weaken)
    with assms(1-4) show ?thesis
      using ‹((ξ, p'), a, (ξ', q)) ∈ trans A› ‹I a› and ‹p'∈sterms Γ p›
      by (rule seq_step_invariant_sterms)
  qed

lemma seq_step_invariant_sterms_TT:
  assumes "A ⊫⇩A onll Γ P"
      and "wellformed Γ"
      and "trans A = seqp_sos Γ"
      and "l'∈labels Γ q"
      and "(ξ, p) ∈ reachable A I"
      and "((ξ, p'), a, (ξ', q)) ∈ trans A"
      and "I a"
      and "p'∈sterms Γ p"
    shows "∀l∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
  using assms by (rule seq_step_invariant_sterms_weaken) simp

lemma onll_step_invariant_any_sterms:
  assumes "wellformed Γ"
      and "A ⊫⇩A (I →) onll Γ P"
      and "(ξ, p) ∈ reachable A I"
      and "((ξ, p), a, (ξ', q)) ∈ trans A"
      and "I a"
      and "l'∈labels Γ q"
    shows "∀p'∈sterms Γ p. ∀l∈labels Γ p'. P ((ξ, l), a, (ξ', l'))"
  by (intro ballI) (rule onll_step_invariant_sterms [OF assms])

lemma seq_step_invariant_ctermI [intro]:
  assumes wf: "wellformed Γ"
      and cw: "control_within Γ (init A)"
      and sl: "simple_labels Γ"
      and sp: "trans A = seqp_sos Γ"
      and step: "⋀p pp l ξ a q l' ξ'. ⟦
                 p∈cterms Γ;
                 l∈labels Γ p;
                 ((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ;
                 ((ξ, p), a, (ξ', q)) ∈ trans A;
                 l'∈labels Γ q;
                 (ξ, pp) ∈ reachable A I;
                 p∈sterms Γ pp;
                 (ξ', q) ∈ reachable A I;
                 I a
               ⟧ ⟹ P ((ξ, l), a, (ξ', l'))"
    shows "A ⊫⇩A (I →) onll Γ P"
  proof
       fix ξ p l a ξ' q l'
    assume sr: "(ξ, p) ∈ reachable A I"
       and tr: "((ξ, p), a, (ξ', q)) ∈ trans A"
       and "I a"
       and pl: "l ∈ labels Γ p"
       and A5: "l' ∈ labels Γ q"
    from this(2) and sp have tr': "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ" by simp
    then obtain p' where "p' ∈ sterms Γ p"
                     and A3: "((ξ, p'), a, (ξ', q)) ∈ seqp_sos Γ"
      by (blast dest: trans_from_sterms [OF _ wf])
    from wf cw sp sr this(1) have A1: "p'∈cterms Γ"
      by (rule seq_reachable_in_cterms)
    from ‹((ξ, p'), a, (ξ', q)) ∈ seqp_sos Γ› and sp
      have A4: "((ξ, p'), a, (ξ', q)) ∈ trans A" by simp
    from sr ‹p'∈sterms Γ p› obtain pp where A6: "(ξ, pp)∈reachable A I"
                                        and A7: "p'∈sterms Γ pp"
      by auto
    from sr tr ‹I a› have A8: "(ξ', q)∈reachable A I" ..
    from wf cw sp sr have "∃pn. p ∈ subterms (Γ pn)"
      by (rule reachable_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 ‹I a›
      by (rule step)
  qed

lemma seq_step_invariant_ctermsI [intro]:
  assumes wf: "wellformed Γ"
      and cw: "control_within Γ (init A)"
      and sl: "simple_labels Γ"
      and sp: "trans A = seqp_sos Γ"
      and step: "⋀p l ξ a q l' ξ' pp pn. ⟦
                 wellformed Γ;
                 p∈ctermsl (Γ pn);
                 not_call p;
                 l∈labels Γ p;
                 ((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ;
                 ((ξ, p), a, (ξ', q)) ∈ trans A;
                 l'∈labels Γ q;
                 (ξ, pp) ∈ reachable A I;
                 p∈sterms Γ pp;
                 (ξ', q) ∈ reachable A I;
                 I a
               ⟧ ⟹ P ((ξ, l), a, (ξ', l'))"
    shows "A ⊫⇩A (I →) onll Γ P"
  using assms(1-4) proof (rule seq_step_invariant_ctermI)
    fix p pp l ξ a q l' ξ'
    assume "p ∈ cterms Γ"
       and otherassms: "l ∈ labels Γ p"
           "((ξ, p), a, (ξ', q)) ∈ seqp_sos Γ"
           "((ξ, p), a, (ξ', q)) ∈ trans A"
           "l' ∈ labels Γ q"
           "(ξ, pp) ∈ reachable A I"
           "p ∈ sterms Γ pp"
           "(ξ', q) ∈ reachable A I"
           "I 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 step)
  qed

end