Quelle  ONode_Lifting.thy

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

section "Lifting rules for (open) nodes"

theory ONode_Lifting
imports AWN OAWN_SOS OInvariants
begin

lemma node_net_state':
  assumes "s ∈ oreachable (⟨i : T : R_i⟩_o) S U"
    shows "∃σ ζ R. s = (σ, NodeS i ζ R)"
  using assms proof induction
    fix s
    assume "s ∈ init (⟨i : T : R_i⟩_o)"
    then obtain σ ζ where "s = (σ, NodeS i ζ R_i)"
      by (auto simp: onode_comps)
    thus "∃σ ζ R. s = (σ, NodeS i ζ R)" by auto
  next
    fix s a σ'
    assume rt: "s ∈ oreachable (⟨i : T : R_i⟩_o) S U"
       and ih: "∃σ ζ R. s = (σ, NodeS i ζ R)"
       and "U (fst s) σ'"
    then obtain σ ζ R
      where "(σ, NodeS i ζ R) ∈ oreachable (⟨i : T : R_i⟩_o) S U"
        and "U σ σ'" and "snd s = NodeS i ζ R" by auto
    from this(1-2)
      have "(σ', NodeS i ζ R) ∈ oreachable (⟨i : T : R_i⟩_o) S U"
        by - (erule(1) oreachable_other')
    with ‹snd s = NodeS i ζ R› show "∃σ ζ R. (σ', snd s) = (σ, NodeS i ζ R)" by simp
  next
    fix s a s'
    assume rt: "s ∈ oreachable (⟨i : T : R_i⟩_o) S U"
       and ih: "∃σ ζ R. s = (σ, NodeS i ζ R)"
       and tr: "(s, a, s') ∈ trans (⟨i : T : R_i⟩_o)"
       and "S (fst s) (fst s') a"
     from ih obtain σ ζ R where "s = (σ, NodeS i ζ R)" by auto
     with tr have "((σ, NodeS i ζ R), a, s') ∈ onode_sos (trans T)"
       by (simp add: onode_comps)
     then obtain σ' ζ' R' where "s' = (σ', NodeS i ζ' R')"
       using onode_sos_dest_is_net_state' by metis
     with tr ‹s = (σ, NodeS i ζ R)› show "∃σ ζ R. s' = (σ, NodeS i ζ R)"
       by simp
  qed

lemma node_net_state:
  assumes "(σ, s) ∈ oreachable (⟨i : T : R_i⟩_o) S U"
    shows "∃ζ R. s = NodeS i ζ R"
  using assms
  by (metis Pair_inject node_net_state')

lemma node_net_state_trans [elim]:
  assumes sor: "(σ, s) ∈ oreachable (⟨i : ζ_i : R_i⟩_o) S U"
      and str: "((σ, s), a, (σ', s')) ∈ trans (⟨i : ζ_i : R_i⟩_o)"
  obtains ζ R ζ' R'
    where "s = NodeS i ζ R"
      and "s' = NodeS i ζ' R'"
  proof -
    assume *: "∧ζ R ζ' R'. s = NodeS i ζ R ==> s' = NodeS i ζ' R' ==> thesis"
    from sor obtain ζ R where "s = NodeS i ζ R"
      by (metis node_net_state)
    moreover with str obtain ζ' R' where "s' = NodeS i ζ' R'"
      by (simp only: onode_comps)
         (metis onode_sos_dest_is_net_state'')
    ultimately show thesis by (rule *)
  qed

lemma nodemap_induct' [consumes, case_names init other local]:
  assumes "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
      and init: "∧σ ζ. (σ, NodeS ii ζ R_i) ∈ init (⟨ii : T : R_i⟩_o) ==> P (σ, NodeS ii ζ R_i)"
      and other: "∧σ ζ R σ' a.
                  [ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U;
                    U σ σ'; P (σ, NodeS ii ζ R) ] ==> P (σ', NodeS ii ζ R)"
      and local: "∧σ ζ R σ' ζ' R' a.
                  [ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U;
                    ((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R_i⟩_o);
                    S σ σ' a; P (σ, NodeS ii ζ R) ] ==> P (σ', NodeS ii ζ' R')"
    shows "P (σ, NodeS ii ζ R)"
  using assms(1) proof induction
    fix s
    assume "s ∈ init (⟨ii : T : R_i⟩_o)"
    hence "s ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
      by (rule oreachable_init)
    with ‹s ∈ init (⟨ii : T : R_i⟩_o)› obtain σ ζ where "s = (σ, NodeS ii ζ R_i)"
      by (simp add: onode_comps) metis
    with ‹s ∈ init (⟨ii : T : R_i⟩_o)› and init show "P s" by simp
  next
    fix s a σ'
    assume sr: "s ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
       and "U (fst s) σ'"
       and "P s"
    from sr obtain σ ζ R where "s = (σ, NodeS ii ζ R)"
      using node_net_state' by metis
    with sr ‹U (fst s) σ'› ‹P s› show "P (σ', snd s)"
    by simp (metis other)
  next
    fix s a s'
    assume sr: "s ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
       and tr: "(s, a, s') ∈ trans (⟨ii : T : R_i⟩_o)"
       and "S (fst s) (fst s') a"
       and "P s"
    from this(1-3) have "s' ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
      by - (erule(2) oreachable_local)
    then obtain σ' ζ' R' where [simp]: "s' = (σ', NodeS ii ζ' R')"
      using node_net_state' by metis
    from sr and ‹P s› obtain σ ζ R
      where [simp]: "s = (σ, NodeS ii ζ R)"
        and A1: "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
        and A4: "P (σ, NodeS ii ζ R)"
      using node_net_state' by metis
    with tr and ‹S (fst s) (fst s') a›
      have A2: "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R_i⟩_o)"
       and A3: "S σ σ' a" by simp_all
    from A1 A2 A3 A4 have "P (σ', NodeS ii ζ' R')" by (rule local)
    thus "P s'" by simp
  qed

lemma nodemap_induct [consumes, case_names init step]:
  assumes "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
      and init: "∧σ ζ. (σ, NodeS ii ζ R_i) ∈ init (⟨ii : T : R_i⟩_o) ==> P σ ζ R_i"
      and other: "∧σ ζ R σ' a.
                  [ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U;
                    U σ σ'; P σ ζ R ] ==> P σ' ζ R"
      and local: "∧σ ζ R σ' ζ' R' a.
                  [ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U;
                    ((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R_i⟩_o);
                    S σ σ' a; P σ ζ R ] ==> P σ' ζ' R'"
    shows "P σ ζ R"
  using assms(1) proof (induction "(σ, NodeS ii ζ R)" arbitrary: σ ζ R)
    fix σ ζ R
    assume a1: "(σ, NodeS ii ζ R) ∈ init (⟨ii : T : R_i⟩_o)"
    hence "R = R_i" by (simp add: init_onode_comp)
    with a1 have "(σ, NodeS ii ζ R_i) ∈ init (⟨ii : T : R_i⟩_o)" by simp
    with init and ‹R = R_i› show "P σ ζ R" by simp
  next
    fix st a σ' ζ' R'
    assume "st ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
       and tr: "(st, a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R_i⟩_o)"
       and "S (fst st) (fst (σ', NodeS ii ζ' R')) a"
       and IH: "∧σ ζ R. st = (σ, NodeS ii ζ R) ==> P σ ζ R"
    from this(1) obtain σ ζ R where "st = (σ, NodeS ii ζ R)"
                                and "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
      by (metis node_net_state')
    note this(2)
    moreover from tr and ‹st = (σ, NodeS ii ζ R)›
      have "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R_i⟩_o)" by simp
    moreover from ‹S (fst st) (fst (σ', NodeS ii ζ' R')) a› and ‹st = (σ, NodeS ii ζ R)›
      have "S σ σ' a" by simp
    moreover from IH and ‹st = (σ, NodeS ii ζ R)› have "P σ ζ R" .
    ultimately show "P σ' ζ' R'" by (rule local)
  next
    fix st σ' ζ R
    assume "st ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
       and "U (fst st) σ'"
       and "snd st = NodeS ii ζ R"
       and IH: "∧σ ζ R. st = (σ, NodeS ii ζ R) ==> P σ ζ R"
    from this(1,3) obtain σ where "st = (σ, NodeS ii ζ R)"
                              and "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
      by (metis surjective_pairing)
    note this(2)
    moreover from ‹U (fst st) σ'› and ‹st = (σ, NodeS ii ζ R)› have "U σ σ'" by simp
    moreover from IH and ‹st = (σ, NodeS ii ζ R)› have "P σ ζ R" .
    ultimately show "P σ' ζ R" by (rule other)
  qed

lemma node_addressD [dest, simp]:
  assumes "(σ, NodeS i ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o) S U"
    shows "i = ii"
  using assms by (clarsimp dest!: node_net_state')

lemma node_proc_reachable [dest]:
  assumes "(σ, NodeS i ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o)
                                         (otherwith S {ii} (oarrivemsg I)) (other U {ii})"
      and sgivesu: "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
    shows "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
  proof -
    from assms(1) have "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o)
                                             (otherwith S {ii} (oarrivemsg I)) (other U {ii})"
      by - (frule node_addressD, simp)
    thus ?thesis
    proof (induction rule: nodemap_induct)
      fix σ ζ
      assume "(σ, NodeS ii ζ R_i) ∈ init (⟨ii : T : R_i⟩_o)"
      hence "(σ, ζ) ∈ init T" by (auto simp: onode_comps)
      thus "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
        by (rule oreachable_init)
    next
      fix σ ζ R σ' ζ' R' a
      assume "other U {ii} σ σ'"
         and "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
      thus "(σ', ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
        by - (rule oreachable_other')
    next
      fix σ ζ R σ' ζ' R' a
      assume rs: "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o)
                                         (otherwith S {ii} (oarrivemsg I)) (other U {ii})"
         and tr: "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R_i⟩_o)"
         and ow: "otherwith S {ii} (oarrivemsg I) σ σ' a"
         and ih: "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"

      from ow have *: "σ' ii = σ ii ==> other U {ii} σ σ'"
        by (clarsimp elim!: otherwithE) (rule otherI, simp_all, metis sgivesu)
      from tr have "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ onode_sos (trans T)"
        by (simp add: onode_comps)
      thus "(σ', ζ') ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
      proof cases
        case onode_bcast
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case onode_gcast
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case onode_ucast
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case onode_notucast
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case onode_deliver
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case onode_tau
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case onode_receive
        with ih and ow show ?thesis
          by (auto elim!: oreachable_local' otherwithE)
      next
        case (onode_arrive m)
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      next
        case onode_connect1
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      next
        case onode_connect2
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      next
        case onode_connect_other
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      next
        case onode_disconnect1
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      next
        case onode_disconnect2
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      next
        case onode_disconnect_other
        hence "ζ' = ζ" and "σ' ii = σ ii" by auto
        from this(2) have "other U {ii} σ σ'" by (rule *)
        with ih and ‹ζ' = ζ› show ?thesis by auto
      qed
    qed
  qed

lemma node_proc_reachable_statelessassm [dest]:
  assumes "(σ, NodeS i ζ R) ∈ oreachable (⟨ii : T : R_i⟩_o)
                                         (otherwith (λ_ _. True) {ii} (oarrivemsg I))
                                         (other (λ_ _. True) {ii})"
    shows "(σ, ζ) ∈ oreachable T
                               (otherwith (λ_ _. True) {ii} (orecvmsg I)) (other (λ_ _. True) {ii})"
  using assms
  by (rule node_proc_reachable) simp_all

lemma node_lift:
  assumes "T ⊨ (otherwith S {ii} (orecvmsg I), other U {ii} →) global P"
      and "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
    shows "⟨ii : T : R_i⟩_o ⊨ (otherwith S {ii} (oarrivemsg I), other U {ii} →) global P"
  proof (rule oinvariant_oreachableI)
    fix σ ζ
    assume "(σ, ζ) ∈ oreachable (⟨ii : T : R_i⟩_o) (otherwith S {ii} (oarrivemsg I)) (other U {ii})"
    moreover then obtain i s R where "ζ = NodeS i s R"
      by (metis node_net_state)
    ultimately have "(σ, NodeS i s R) ∈ oreachable (⟨ii : T : R_i⟩_o)
                                                   (otherwith S {ii} (oarrivemsg I)) (other U {ii})"
      by simp
    hence "(σ, s) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
      by - (erule node_proc_reachable, erule assms(2))
    with assms(1) show "global P (σ, ζ)"
      by (metis fst_conv globalsimp oinvariantD)
  qed

lemma node_lift_step [intro]:
  assumes pinv: "T ⊨_A (otherwith S {i} (orecvmsg I), other U {i} →) globala (λ(σ, _, σ'). Q σ σ')"
      and other: "∧σ σ'. other U {i} σ σ' ==> Q σ σ'"
      and sgivesu: "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
    shows "⟨i : T : R_i⟩_o ⊨_A (otherwith S {i} (oarrivemsg I), other U {i} →)
                            globala (λ(σ, _, σ'). Q σ σ')"
    (is "_ ⊨_A (?S, ?U →) _")
  proof (rule ostep_invariantI, simp)
    fix σ s a σ' s'
    assume rs: "(σ, s) ∈ oreachable (⟨i : T : R_i⟩_o) ?S ?U"
       and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : T : R_i⟩_o)"
       and ow: "?S σ σ' a"
    from ow have *: "σ' i = σ i ==> other U {i} σ σ'"
      by (clarsimp elim!: otherwithE) (rule otherI, simp_all, metis sgivesu)
    from rs tr obtain ζ R
      where [simp]: "s = NodeS i ζ R"
        and "(σ, NodeS i ζ R) ∈ oreachable (⟨i : T : R_i⟩_o) ?S ?U"
      by (metis node_net_state)
    from this(2) have or: "(σ, ζ) ∈ oreachable T (otherwith S {i} (orecvmsg I)) ?U"
      by (rule node_proc_reachable [OF _ assms(3)])
    from tr have "((σ, NodeS i ζ R), a, (σ', s')) ∈ onode_sos (trans T)"
      by (simp add: onode_comps)
    thus "Q σ σ'"
    proof cases
      fix m ζ'
      assume "a = R:*cast(m)"
         and tr': "((σ, ζ), broadcast m, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (broadcast m)"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix D m ζ'
      assume "a = (R ∩ D):*cast(m)"
         and tr': "((σ, ζ), groupcast D m, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (groupcast D m)"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix d m ζ'
      assume "a = {d}:*cast(m)"
         and tr': "((σ, ζ), unicast d m, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (unicast d m)"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix d ζ'
      assume "a = τ"
         and tr': "((σ, ζ), ¬unicast d, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (¬unicast d)"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix d ζ'
      assume "a = i:deliver(d)"
         and tr': "((σ, ζ), deliver d, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (deliver d)"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix ζ'
      assume "a = τ"
         and tr': "((σ, ζ), τ, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' τ"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix m ζ'
      assume "a = {i}¬{}:arrive(m)"
         and tr': "((σ, ζ), receive m, (σ', ζ')) ∈ trans T"
      from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (receive m)"
        by (auto elim!: otherwithE)
      with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
    next
      fix m
      assume "a = {}¬{i}:arrive(m)"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    next
      fix i'
      assume "a = connect(i, i')"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    next
      fix i'
      assume "a = connect(i', i)"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    next
      fix i' i''
      assume "a = connect(i', i'')"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    next
      fix i'
      assume "a = disconnect(i, i')"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    next
      fix i'
      assume "a = disconnect(i', i)"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    next
      fix i' i''
      assume "a = disconnect(i', i'')"
         and "σ' i = σ i"
      from this(2) have "other U {i} σ σ'" by (rule *)
      thus ?thesis by (rule other)
    qed
  qed

lemma node_lift_step_statelessassm [intro]:
  assumes "T ⊨_A (λσ _. orecvmsg I σ, other (λ_ _. True) {i} →)
                       globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
      and "∧ξ. Q ξ ξ"
    shows "⟨i : T : R_i⟩_o ⊨_A (λσ _. oarrivemsg I σ, other (λ_ _. True) {i} →)
                            globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
  proof -
    from assms(1)
      have "T ⊨_A (otherwith (λ_ _. True) {i} (orecvmsg I), other (λ_ _. True) {i} →)
                  globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
        by rule auto
    with assms(2) have "⟨i : T : R_i⟩_o ⊨_A (otherwith (λ_ _. True) {i} (oarrivemsg I),
                                          other (λ_ _. True) {i} →)
                                         globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
      by - (rule node_lift_step, auto)
    thus ?thesis by rule auto
  qed

lemma node_lift_anycast [intro]:
  assumes pinv: "T ⊨_A (otherwith S {i} (orecvmsg I), other U {i} →)
                       globala (λ(σ, a, σ'). anycast (Q σ σ') a)"
      and "∧ξ ξ'. S ξ ξ' ==> U ξ ξ'"
    shows "⟨i : T : R_i⟩_o ⊨_A (otherwith S {i} (oarrivemsg I), other U {i} →)
                            globala (λ(σ, a, σ'). castmsg (Q σ σ') a)"
    (is "_ ⊨_A (?S, ?U →) _")
  proof (rule ostep_invariantI, simp)
    fix σ s a σ' s'
    assume rs: "(σ, s) ∈ oreachable (⟨i : T : R_i⟩_o) ?S ?U"
       and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : T : R_i⟩_o)"
       and "?S σ σ' a"
    from this(1-2) obtain ζ R
      where [simp]: "s = NodeS i ζ R"
        and "(σ, NodeS i ζ R) ∈ oreachable (⟨i : T : R_i⟩_o) ?S ?U"
      by (metis node_net_state)
    from this(2) have "(σ, ζ) ∈ oreachable T (otherwith S {i} (orecvmsg I)) ?U"
      by (rule node_proc_reachable [OF _ assms(2)])
    moreover from tr have "((σ, NodeS i ζ R), a, (σ', s')) ∈ onode_sos (trans T)"
      by (simp add: onode_comps)
    ultimately show "castmsg (Q σ σ') a" using ‹?S σ σ' a›
      by - (erule onode_sos.cases, auto elim!: otherwithE dest!: ostep_invariantD [OF pinv])
  qed

lemma node_lift_anycast_statelessassm [intro]:
  assumes pinv: "T ⊨_A (λσ _. orecvmsg I σ, other (λ_ _. True) {i} →)
                       globala (λ(σ, a, σ'). anycast (Q σ σ') a)"
    shows "⟨i : T : R_i⟩_o ⊨_A (λσ _. oarrivemsg I σ, other (λ_ _. True) {i} →)
                            globala (λ(σ, a, σ'). castmsg (Q σ σ') a)"
    (is "_ ⊨_A (?S, _ →) _")
  proof -
    from assms(1)
      have "T ⊨_A (otherwith (λ_ _. True) {i} (orecvmsg I), other (λ_ _. True) {i} →)
                  globala (λ(σ, a, σ'). anycast (Q σ σ') a)"
        by rule auto
    hence "⟨i : T : R_i⟩_o ⊨_A (otherwith (λ_ _. True) {i} (oarrivemsg I), other (λ_ _. True) {i} →)
                            globala (λ(σ, a, σ'). castmsg (Q σ σ') a)"
      by (rule node_lift_anycast) simp_all
    thus ?thesis
      by rule auto
  qed

lemma node_local_deliver:
  "⟨i : ζ_i : R_i⟩_o ⊨_A (S, U →) globala (λ(_, a, _). ∀j. j≠i ⟶ (∀d. a ≠ j:deliver(d)))"
  proof (rule ostep_invariantI, simp)
    fix σ s a σ' s'
    assume 1: "(σ, s) ∈ oreachable (⟨i : ζ_i : R_i⟩_o) S U"
       and 2: "((σ, s), a, (σ', s')) ∈ trans (⟨i : ζ_i : R_i⟩_o)"
       and "S σ σ' a"
    moreover from 1 2 obtain ζ R ζ' R' where "s = NodeS i ζ R" and "s' = NodeS i ζ' R'" ..
    ultimately show "∀j. j≠i ⟶ (∀d. a ≠ j:deliver(d))"
      by (cases a) (auto simp add: onode_comps)
  qed

lemma node_tau_deliver_unchanged:
  "⟨i : ζ_i : R_i⟩_o ⊨_A (S, U →) globala (λ(σ, a, σ'). a = τ ∨ (∃i d. a = i:deliver(d))
                                                     ⟶ (∀j. j≠i ⟶ σ' j = σ j))"
  proof (rule ostep_invariantI, clarsimp simp only: globalasimp snd_conv fst_conv)
    fix σ s a σ' s' j
    assume 1: "(σ, s) ∈ oreachable (⟨i : ζ_i : R_i⟩_o) S U"
       and 2: "((σ, s), a, (σ', s')) ∈ trans (⟨i : ζ_i : R_i⟩_o)"
       and "S σ σ' a"
       and "a = τ ∨ (∃i d. a = i:deliver(d))"
       and "j ≠ i"
    moreover from 1 2 obtain ζ R ζ' R' where "s = NodeS i ζ R" and "s' = NodeS i ζ' R'" ..
    ultimately show "σ' j = σ j"
      by (cases a) (auto simp del: step_node_tau simp add: onode_comps)
  qed

end