Theory OPnet_Lifting

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

section "Lifting rules for (open) partial networks"

theory OPnet_Lifting
imports ONode_Lifting OAWN_SOS OPnet
begin

lemma oreachable_par_subnet_induct [consumes, case_names init other local]:
  assumes "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U"
      and init: "⋀σ s t. (σ, SubnetS s t) ∈ init (opnet onp (p⇩1 ∥ p⇩2)) ⟹ P σ s t"
      and other: "⋀σ s t σ'. ⟦ (σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U;
                                U σ σ'; P σ s t ⟧ ⟹ P σ' s t"
      and local: "⋀σ s t σ' s' t' a. ⟦ (σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U;
                    ((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2));
                    S σ σ' a; P σ s t ⟧ ⟹ P σ' s' t'"
    shows "P σ s t"
  using assms(1) proof (induction "(σ, SubnetS s t)" arbitrary: s t σ)
    fix s t σ
    assume "(σ, SubnetS s t) ∈ init (opnet onp (p⇩1 ∥ p⇩2))"
    with init show "P σ s t" .
  next
    fix st a s' t' σ'
    assume "st ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U"
       and tr: "(st, a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))"
       and "S (fst st) (fst (σ', SubnetS s' t')) a"
       and IH: "⋀s t σ. st = (σ, SubnetS s t) ⟹ P σ s t"
    from this(1) obtain s t σ where "st = (σ, SubnetS s t)"
                                and "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U"
      by (metis net_par_oreachable_is_subnet prod.collapse)
    note this(2)
    moreover from tr and ‹st = (σ, SubnetS s t)›
      have "((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))" by simp
    moreover from ‹S (fst st) (fst (σ', SubnetS s' t')) a› and ‹st = (σ, SubnetS s t)›
      have "S σ σ' a" by simp
    moreover from IH and ‹st = (σ, SubnetS s t)› have "P σ s t" .
    ultimately show "P σ' s' t'" by (rule local)
  next
    fix st σ' s t
    assume "st ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U"
       and "U (fst st) σ'"
       and "snd st = SubnetS s t"
       and IH: "⋀s t σ. st = (σ, SubnetS s t) ⟹ P σ s t"
    from this(1,3) obtain σ where "st = (σ, SubnetS s t)"
                              and "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) S U"
      by (metis prod.collapse)
    note this(2)
    moreover from ‹U (fst st) σ'› and ‹st = (σ, SubnetS s t)› have "U σ σ'" by simp
    moreover from IH and ‹st = (σ, SubnetS s t)› have "P σ s t" .
    ultimately show "P σ' s t" by (rule other)
  qed

lemma other_net_tree_ips_par_left:
  assumes "other U (net_tree_ips (p⇩1 ∥ p⇩2)) σ σ'"
      and "⋀ξ. U ξ ξ"
    shows "other U (net_tree_ips p⇩1) σ σ'"
  proof -
    from assms(1) obtain ineq: "∀i∈net_tree_ips (p⇩1 ∥ p⇩2). σ' i = σ i"
                     and outU: "∀j. j∉net_tree_ips (p⇩1 ∥ p⇩2) ⟶ U (σ j) (σ' j)" ..
    show ?thesis
    proof (rule otherI)
      fix i
      assume "i∈net_tree_ips p⇩1"
      hence "i∈net_tree_ips (p⇩1 ∥ p⇩2)" by simp
      with ineq show "σ' i = σ i" ..
    next
      fix j
      assume "j∉net_tree_ips p⇩1"
      show "U (σ j) (σ' j)"
      proof (cases "j∈net_tree_ips p⇩2")
        assume "j∈net_tree_ips p⇩2"
        hence "j∈net_tree_ips (p⇩1 ∥ p⇩2)" by simp
        with ineq have "σ' j = σ j" ..
        thus "U (σ j) (σ' j)"
          by simp (rule ‹⋀ξ. U ξ ξ›)
      next
        assume "j∉net_tree_ips p⇩2"
        with ‹j∉net_tree_ips p⇩1› have "j∉net_tree_ips (p⇩1 ∥ p⇩2)" by simp
        with outU show "U (σ j) (σ' j)" by simp
      qed
    qed
  qed

lemma other_net_tree_ips_par_right:
  assumes "other U (net_tree_ips (p⇩1 ∥ p⇩2)) σ σ'"
      and "⋀ξ. U ξ ξ"
    shows "other U (net_tree_ips p⇩2) σ σ'"
  proof -
    from assms(1) have "other U (net_tree_ips (p⇩2 ∥ p⇩1)) σ σ'"
      by (subst net_tree_ips_commute)
    thus ?thesis using ‹⋀ξ. U ξ ξ›
      by (rule other_net_tree_ips_par_left)
  qed

lemma ostep_arrive_invariantD [elim]:
  assumes "p ⊨⇩A (λσ _. oarrivemsg I σ, U →) P"
      and "(σ, s) ∈ oreachable p (otherwith S IPS (oarrivemsg I)) U"
      and "((σ, s), a, (σ', s')) ∈ trans p"
      and "oarrivemsg I σ a"
    shows "P ((σ, s), a, (σ', s'))"
  proof -
    from assms(2) have "(σ, s) ∈ oreachable p (λσ _ a. oarrivemsg I σ a) U"
      by (rule oreachable_weakenE) auto
    thus "P ((σ, s), a, (σ', s'))"
      using assms(3-4) by (rule ostep_invariantD [OF assms(1)])
  qed

lemma opnet_sync_action_subnet_oreachable:
  assumes "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2))
                                         (λσ _. oarrivemsg I σ) (other U (net_tree_ips (p⇩1 ∥ p⇩2)))"
          (is "_ ∈ oreachable _ (?S (p⇩1 ∥ p⇩2)) (?U (p⇩1 ∥ p⇩2))")

      and "⋀ξ. U ξ ξ"

      and act1: "opnet onp p⇩1 ⊨⇩A (λσ _. oarrivemsg I σ, other U (net_tree_ips p⇩1) →)
                   globala (λ(σ, a, σ'). castmsg (I σ) a
                                          ∧ (a = τ ∨ (∃i d. a = i:deliver(d)) ⟶
                                                 ((∀i∈net_tree_ips p⇩1. U (σ i) (σ' i))
                                               ∧ (∀i. i∉net_tree_ips p⇩1 ⟶ σ' i = σ i))))"

      and act2: "opnet onp p⇩2 ⊨⇩A (λσ _. oarrivemsg I σ, other U (net_tree_ips p⇩2) →)
                   globala (λ(σ, a, σ'). castmsg (I σ) a
                                          ∧ (a = τ ∨ (∃i d. a = i:deliver(d)) ⟶
                                                 ((∀i∈net_tree_ips p⇩2. U (σ i) (σ' i))
                                               ∧ (∀i. i∉net_tree_ips p⇩2 ⟶ σ' i = σ i))))"

    shows "(σ, s) ∈ oreachable (opnet onp p⇩1) (λσ _. oarrivemsg I σ) (other U (net_tree_ips p⇩1))
           ∧ (σ, t) ∈ oreachable (opnet onp p⇩2) (λσ _. oarrivemsg I σ) (other U (net_tree_ips p⇩2))
           ∧ net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}"
  using assms(1)
  proof (induction rule: oreachable_par_subnet_induct)
    case (init σ s t)
    hence sinit: "(σ, s) ∈ init (opnet onp p⇩1)"
      and tinit: "(σ, t) ∈ init (opnet onp p⇩2)"
      and "net_ips s ∩ net_ips t = {}" by auto
    moreover from sinit have "net_ips s = net_tree_ips p⇩1"
      by (rule opnet_net_ips_net_tree_ips_init)
    moreover from tinit have "net_ips t = net_tree_ips p⇩2"
      by (rule opnet_net_ips_net_tree_ips_init)
    ultimately show ?case by (auto elim: oreachable_init)
  next
    case (other σ s t σ')
    hence "other U (net_tree_ips (p⇩1 ∥ p⇩2)) σ σ'"
      and IHs: "(σ, s) ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
      and IHt: "(σ, t) ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
      and "net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}" by auto

    have "(σ', s) ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
    proof -
      from ‹?U (p⇩1 ∥ p⇩2) σ σ'› and ‹⋀ξ. U ξ ξ› have "?U p⇩1 σ σ'"
        by (rule other_net_tree_ips_par_left)
      with IHs show ?thesis by - (erule(1) oreachable_other')
    qed

    moreover have "(σ', t) ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
    proof -
      from ‹?U (p⇩1 ∥ p⇩2) σ σ'› and ‹⋀ξ. U ξ ξ› have "?U p⇩2 σ σ'"
        by (rule other_net_tree_ips_par_right)
      with IHt show ?thesis by - (erule(1) oreachable_other')
    qed

    ultimately show ?case using ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}› by simp
  next
    case (local σ s t σ' s' t' a)
    hence stor: "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) (?S (p⇩1 ∥ p⇩2)) (?U (p⇩1 ∥ p⇩2))"
      and tr: "((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))"
      and "oarrivemsg I σ a"
      and sor: "(σ, s) ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
      and tor: "(σ, t) ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
      and "net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}" by auto
    from tr have "((σ, SubnetS s t), a, (σ', SubnetS s' t'))
                    ∈ opnet_sos (trans (opnet onp p⇩1)) (trans (opnet onp p⇩2))" by simp
    hence "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)
         ∧ (σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
    proof (cases)
      fix H K m H' K'
      assume "a = (H ∪ H')¬(K ∪ K'):arrive(m)"
         and str: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), H'¬K':arrive(m), (σ', t')) ∈ trans (opnet onp p⇩2)"
      from this(1) and ‹oarrivemsg I σ a› have "I σ m" by simp

      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹I σ m› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix R m H K
      assume str: "((σ, s), R:*cast(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), H¬K:arrive(m), (σ', t')) ∈ trans (opnet onp p⇩2)"                                    
      from sor str have "I σ m"
        by - (drule(1) ostep_invariantD [OF act1], simp_all)
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹I σ m› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix R m H K
      assume str: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), R:*cast(m), (σ', t')) ∈ trans (opnet onp p⇩2)"                                    
      from tor ttr have "I σ m"
        by - (drule(1) ostep_invariantD [OF act2], simp_all)
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹I σ m› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix i i'
      assume str: "((σ, s), connect(i, i'), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), connect(i, i'), (σ', t')) ∈ trans (opnet onp p⇩2)"
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix i i'
      assume str: "((σ, s), disconnect(i, i'), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), disconnect(i, i'), (σ', t')) ∈ trans (opnet onp p⇩2)"
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix i d
      assume "t' = t"
         and str: "((σ, s), i:deliver(d), (σ', s')) ∈ trans (opnet onp p⇩1)"

      from sor str have "∀j. j∉net_tree_ips p⇩1 ⟶ σ' j = σ j"
        by - (drule(1) ostep_invariantD [OF act1], simp_all)
      moreover with ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
        have "∀j. j∈net_tree_ips p⇩2 ⟶ σ' j = σ j" by auto
      moreover from sor str have "∀j∈net_tree_ips p⇩1. U (σ j) (σ' j)"
        by - (drule(1) ostep_invariantD [OF act1], simp_all)
      ultimately have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
        using tor ‹t' = t› by (clarsimp elim!: oreachable_other')
                              (metis otherI ‹⋀ξ. U ξ ξ›)+

      moreover from sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis by (rule conjI [rotated])
    next
      fix i d
      assume "s' = s"
         and ttr: "((σ, t), i:deliver(d), (σ', t')) ∈ trans (opnet onp p⇩2)"

      from tor ttr have "∀j. j∉net_tree_ips p⇩2 ⟶ σ' j = σ j"
        by - (drule(1) ostep_invariantD [OF act2], simp_all)
      moreover with ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
        have "∀j. j∈net_tree_ips p⇩1 ⟶ σ' j = σ j" by auto
      moreover from tor ttr have "∀j∈net_tree_ips p⇩2. U (σ j) (σ' j)"
        by - (drule(1) ostep_invariantD [OF act2], simp_all)
      ultimately have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
        using sor ‹s' = s› by (clarsimp elim!: oreachable_other')
                              (metis otherI ‹⋀ξ. U ξ ξ›)+

      moreover from tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      assume "t' = t"
         and str: "((σ, s), τ, (σ', s')) ∈ trans (opnet onp p⇩1)"

      from sor str have "∀j. j∉net_tree_ips p⇩1 ⟶ σ' j = σ j"
        by - (drule(1) ostep_invariantD [OF act1], simp_all)
      moreover with ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
        have "∀j. j∈net_tree_ips p⇩2 ⟶ σ' j = σ j" by auto
      moreover from sor str have "∀j∈net_tree_ips p⇩1. U (σ j) (σ' j)"
        by - (drule(1) ostep_invariantD [OF act1], simp_all)
      ultimately have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
        using tor ‹t' = t› by (clarsimp elim!: oreachable_other')
                              (metis otherI ‹⋀ξ. U ξ ξ›)+

      moreover from sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis by (rule conjI [rotated])
    next
      assume "s' = s"
         and ttr: "((σ, t), τ, (σ', t')) ∈ trans (opnet onp p⇩2)"

      from tor ttr have "∀j. j∉net_tree_ips p⇩2 ⟶ σ' j = σ j"
        by - (drule(1) ostep_invariantD [OF act2], simp_all)
      moreover with ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
        have "∀j. j∈net_tree_ips p⇩1 ⟶ σ' j = σ j" by auto
      moreover from tor ttr have "∀j∈net_tree_ips p⇩2. U (σ j) (σ' j)"
        by - (drule(1) ostep_invariantD [OF act2], simp_all)
      ultimately have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
        using sor ‹s' = s› by (clarsimp elim!: oreachable_other')
                              (metis otherI ‹⋀ξ. U ξ ξ›)+

      moreover from tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    qed
    with ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}› show ?case by simp
  qed

text ‹
  `Splitting' reachability is trivial when there are no assumptions on interleavings, but
  this is useless for showing non-trivial properties, since the interleaving steps can do
  anything at all. This lemma is too weak.
›

lemma subnet_oreachable_true_true:
  assumes "(σ, SubnetS s⇩1 s⇩2) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) (λ_ _ _. True) (λ_ _. True)"
    shows "(σ, s⇩1) ∈ oreachable (opnet onp p⇩1) (λ_ _ _. True) (λ_ _. True)"
          "(σ, s⇩2) ∈ oreachable (opnet onp p⇩2) (λ_ _ _. True) (λ_ _. True)"
          (is "_ ∈ ?oreachable p⇩2")
  using assms proof -
    from assms have "(σ, s⇩1) ∈ ?oreachable p⇩1 ∧ (σ, s⇩2) ∈ ?oreachable p⇩2"
    proof (induction rule: oreachable_par_subnet_induct)
      fix σ s⇩1 s⇩2
      assume "(σ, SubnetS s⇩1 s⇩2) ∈ init (opnet onp (p⇩1 ∥ p⇩2))"
      thus "(σ, s⇩1) ∈ ?oreachable p⇩1 ∧ (σ, s⇩2) ∈ ?oreachable p⇩2"
        by (auto dest: oreachable_init)
    next
      case (local σ s⇩1 s⇩2 σ' s⇩1' s⇩2' a)
      hence "(σ, SubnetS s⇩1 s⇩2) ∈ ?oreachable (p⇩1 ∥ p⇩2)"
        and sr1: "(σ, s⇩1) ∈ ?oreachable p⇩1"
        and sr2: "(σ, s⇩2) ∈ ?oreachable p⇩2"
        and "((σ, SubnetS s⇩1 s⇩2), a, (σ', SubnetS s⇩1' s⇩2')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))" by auto
      from this(4)
        have "((σ, SubnetS s⇩1 s⇩2), a, (σ', SubnetS s⇩1' s⇩2'))
                ∈ opnet_sos (trans (opnet onp p⇩1)) (trans (opnet onp p⇩2))" by simp
      thus "(σ', s⇩1') ∈ ?oreachable p⇩1 ∧ (σ', s⇩2') ∈ ?oreachable p⇩2"
      proof cases
        fix R m H K
        assume "a = R:*cast(m)"
           and tr1: "((σ, s⇩1), R:*cast(m), (σ', s⇩1')) ∈ trans (opnet onp p⇩1)"
           and tr2: "((σ, s⇩2), H¬K:arrive(m), (σ', s⇩2')) ∈ trans (opnet onp p⇩2)"
        from sr1 and tr1 and TrueI have "(σ', s⇩1') ∈ ?oreachable p⇩1"
          by (rule oreachable_local')
        moreover from sr2 and tr2 and TrueI have "(σ', s⇩2') ∈ ?oreachable p⇩2"
          by (rule oreachable_local')
        ultimately show ?thesis ..
      next
        assume "a = τ"
           and "s⇩2' = s⇩2"
           and tr1: "((σ, s⇩1), τ, (σ', s⇩1')) ∈ trans (opnet onp p⇩1)"
        from sr2 and this(2) have "(σ', s⇩2') ∈ ?oreachable p⇩2" by auto
        moreover have "(λ_ _. True) σ σ'" by (rule TrueI)
        ultimately have "(σ', s⇩2') ∈ ?oreachable p⇩2"
          by (rule oreachable_other')
        moreover from sr1 and tr1 and TrueI have "(σ', s⇩1') ∈ ?oreachable p⇩1"
          by (rule oreachable_local')
      qed (insert sr1 sr2, simp_all, (metis (no_types) oreachable_local'
                                                       oreachable_other')+)
    qed auto
    thus "(σ, s⇩1) ∈ ?oreachable p⇩1"
         "(σ, s⇩2) ∈ ?oreachable p⇩2" by auto
  qed

text ‹
  It may also be tempting to try splitting from the assumption
  @{term "(σ, SubnetS s⇩1 s⇩2) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) (λ_ _ _. True) (λ_ _. False)"},
  where the environment step would be trivially true (since the assumption is false), but the
  lemma cannot be shown when only one side acts, since it must guarantee the assumption for
  the other side.
›

lemma lift_opnet_sync_action:
  assumes "⋀ξ. U ξ ξ"
      and act1: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, _). castmsg (I σ) a)"
      and act2: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, σ'). (a ≠ τ ∧ (∀d. a ≠ i:deliver(d)) ⟶ S (σ i) (σ' i)))"
      and act3: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, σ'). (a = τ ∨ (∃d. a = i:deliver(d)) ⟶ U (σ i) (σ' i)))"
  shows "opnet onp p ⊨⇩A (λσ _. oarrivemsg I σ, other U (net_tree_ips p) →)
                       globala (λ(σ, a, σ'). castmsg (I σ) a
                                              ∧ (a ≠ τ ∧ (∀i d. a ≠ i:deliver(d)) ⟶
                                                     (∀i∈net_tree_ips p. S (σ i) (σ' i)))
                                              ∧ (a = τ ∨ (∃i d. a = i:deliver(d)) ⟶
                                                     ((∀i∈net_tree_ips p. U (σ i) (σ' i))
                                                   ∧ (∀i. i∉net_tree_ips p ⟶ σ' i = σ i))))"
    (is "opnet onp p ⊨⇩A (?I, ?U p →) ?inv (net_tree_ips p)")
  proof (induction p)
    fix i R
    show "opnet onp ⟨i; R⟩ ⊨⇩A (?I, ?U ⟨i; R⟩ →) ?inv (net_tree_ips ⟨i; R⟩)"
    proof (rule ostep_invariantI, simp only: opnet.simps net_tree_ips.simps)
      fix σ s a σ' s'
      assume sor: "(σ, s) ∈ oreachable (⟨i : onp i : R⟩⇩o) (λσ _. oarrivemsg I σ) (other U {i})"
         and str: "((σ, s), a, (σ', s')) ∈ trans (⟨i : onp i : R⟩⇩o)"
         and oam: "oarrivemsg I σ a"             
      hence "castmsg (I σ) a"
        by - (drule(2) ostep_invariantD [OF act1], simp)
      moreover from sor str oam have "a ≠ τ ∧ (∀i d. a ≠ i:deliver(d)) ⟶ S (σ i) (σ' i)"
        by - (drule(2) ostep_invariantD [OF act2], simp)
      moreover have "a = τ ∨ (∃i d. a = i:deliver(d)) ⟶ U (σ i) (σ' i)"
      proof -
        from sor str oam have "a = τ ∨ (∃d. a = i:deliver(d)) ⟶ U (σ i) (σ' i)"
          by - (drule(2) ostep_invariantD [OF act3], simp)
        moreover from sor str oam have "∀j. j≠i ⟶ (∀d. a ≠ j:deliver(d))"
          by - (drule(2) ostep_invariantD [OF node_local_deliver], simp)
        ultimately show ?thesis
          by clarsimp metis
      qed
      moreover from sor str oam have "∀j. j≠i ⟶ (∀d. a ≠ j:deliver(d))"
        by - (drule(2) ostep_invariantD [OF node_local_deliver], simp)
      moreover from sor str oam have "a = τ ∨ (∃i d. a = i:deliver(d)) ⟶ (∀j. j≠i ⟶ σ' j = σ j)"
        by - (drule(2) ostep_invariantD [OF node_tau_deliver_unchanged], simp)
      ultimately show "?inv {i} ((σ, s), a, (σ', s'))" by simp
    qed
  next
    fix p⇩1 p⇩2
    assume inv1: "opnet onp p⇩1 ⊨⇩A (?I, ?U p⇩1 →) ?inv (net_tree_ips p⇩1)"
       and inv2: "opnet onp p⇩2 ⊨⇩A (?I, ?U p⇩2 →) ?inv (net_tree_ips p⇩2)"
    show "opnet onp (p⇩1 ∥ p⇩2) ⊨⇩A (?I, ?U (p⇩1 ∥ p⇩2) →) ?inv (net_tree_ips (p⇩1 ∥ p⇩2))"
    proof (rule ostep_invariantI)
      fix σ st a σ' st'
      assume "(σ, st) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) ?I (?U (p⇩1 ∥ p⇩2))"
         and "((σ, st), a, (σ', st')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))"
         and "oarrivemsg I σ a"
      from this(1) obtain s t
        where "st = SubnetS s t"
          and *: "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) ?I (?U (p⇩1 ∥ p⇩2))"
        by - (frule net_par_oreachable_is_subnet, metis)

      from this(2) and inv1 and inv2
        obtain sor: "(σ, s) ∈ oreachable (opnet onp p⇩1) ?I (?U p⇩1)"
           and tor: "(σ, t) ∈ oreachable (opnet onp p⇩2) ?I (?U p⇩2)"
           and "net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}"
          by - (drule opnet_sync_action_subnet_oreachable [OF _ ‹⋀ξ. U ξ ξ›], auto)

      from * and ‹((σ, st), a, (σ', st')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))› and ‹st = SubnetS s t›
        obtain s' t' where "st' = SubnetS s' t'"
                       and "((σ, SubnetS s t), a, (σ', SubnetS s' t'))
                              ∈ opnet_sos (trans (opnet onp p⇩1)) (trans (opnet onp p⇩2))"
          by clarsimp (frule opartial_net_preserves_subnets, metis)

      from this(2)
        have"castmsg (I σ) a
             ∧ (a ≠ τ ∧ (∀i d. a ≠ i:deliver(d)) ⟶ (∀i∈net_tree_ips (p⇩1 ∥ p⇩2). S (σ i) (σ' i)))
             ∧ (a = τ ∨ (∃i d. a = i:deliver(d)) ⟶ (∀i∈net_tree_ips (p⇩1 ∥ p⇩2). U (σ i) (σ' i))
                                                  ∧ (∀i. i ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ σ' i = σ i))"
      proof cases
        fix R m H K
        assume "a = R:*cast(m)" 
           and str: "((σ, s), R:*cast(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
           and ttr: "((σ, t), H¬K:arrive(m), (σ', t')) ∈ trans (opnet onp p⇩2)"
        from sor and str have "I σ m ∧ (∀i∈net_tree_ips p⇩1. S (σ i) (σ' i))"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover with tor and ttr have "∀i∈net_tree_ips p⇩2. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv2])
        ultimately show ?thesis
          using ‹a = R:*cast(m)› by auto
      next
        fix R m H K
        assume "a = R:*cast(m)" 
           and str: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
           and ttr: "((σ, t), R:*cast(m), (σ', t')) ∈ trans (opnet onp p⇩2)"
        from tor and ttr have "I σ m ∧ (∀i∈net_tree_ips p⇩2. S (σ i) (σ' i))"
          by (auto dest: ostep_invariantD [OF inv2])
        moreover with sor and str have "∀i∈net_tree_ips p⇩1. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        ultimately show ?thesis
          using ‹a = R:*cast(m)› by auto
      next
        fix H K m H' K'
        assume "a = (H ∪ H')¬(K ∪ K'):arrive(m)"
           and str: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
           and ttr: "((σ, t), H'¬K':arrive(m), (σ', t')) ∈ trans (opnet onp p⇩2)"
        from this(1) and ‹oarrivemsg I σ a› have "I σ m" by simp
        with sor and str have "∀i∈net_tree_ips p⇩1. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover from tor and ttr and ‹I σ m› have "∀i∈net_tree_ips p⇩2. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv2])
        ultimately show ?thesis
          using ‹a = (H ∪ H')¬(K ∪ K'):arrive(m)› by auto
      next
        fix i d
        assume "a = i:deliver(d)"
           and str: "((σ, s), i:deliver(d), (σ', s')) ∈ trans (opnet onp p⇩1)"
        with sor have "((∀i∈net_tree_ips p⇩1. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p⇩1 ⟶ σ' i = σ i))"
          by (auto dest!: ostep_invariantD [OF inv1])
        with ‹a = i:deliver(d)› and ‹⋀ξ. U ξ ξ› show ?thesis
          by auto
      next
        fix i d
        assume "a = i:deliver(d)"
           and ttr: "((σ, t), i:deliver(d), (σ', t')) ∈ trans (opnet onp p⇩2)"
        with tor have "((∀i∈net_tree_ips p⇩2. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p⇩2 ⟶ σ' i = σ i))"
          by (auto dest!: ostep_invariantD [OF inv2])
        with ‹a = i:deliver(d)› and ‹⋀ξ. U ξ ξ› show ?thesis
          by auto
      next
        assume "a = τ"
           and str: "((σ, s), τ, (σ', s')) ∈ trans (opnet onp p⇩1)"
        with sor have "((∀i∈net_tree_ips p⇩1. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p⇩1 ⟶ σ' i = σ i))"
          by (auto dest!: ostep_invariantD [OF inv1])
        with ‹a = τ› and ‹⋀ξ. U ξ ξ› show ?thesis
          by auto
      next
        assume "a = τ"
           and ttr: "((σ, t), τ, (σ', t')) ∈ trans (opnet onp p⇩2)"
        with tor have "((∀i∈net_tree_ips p⇩2. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p⇩2 ⟶ σ' i = σ i))"
          by (auto dest!: ostep_invariantD [OF inv2])
        with ‹a = τ› and ‹⋀ξ. U ξ ξ› show ?thesis
          by auto
      next
        fix i i'
        assume "a = connect(i, i')"
           and str: "((σ, s), connect(i, i'), (σ', s')) ∈ trans (opnet onp p⇩1)"
           and ttr: "((σ, t), connect(i, i'), (σ', t')) ∈ trans (opnet onp p⇩2)"
        from sor and str have "∀i∈net_tree_ips p⇩1. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover from tor and ttr have "∀i∈net_tree_ips p⇩2. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv2])
        ultimately show ?thesis
          using ‹a = connect(i, i')› by auto
      next
        fix i i'
        assume "a = disconnect(i, i')"
           and str: "((σ, s), disconnect(i, i'), (σ', s')) ∈ trans (opnet onp p⇩1)"
           and ttr: "((σ, t), disconnect(i, i'), (σ', t')) ∈ trans (opnet onp p⇩2)"
        from sor and str have "∀i∈net_tree_ips p⇩1. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover from tor and ttr have "∀i∈net_tree_ips p⇩2. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv2])
        ultimately show ?thesis
          using ‹a = disconnect(i, i')› by auto
      qed
      thus "?inv (net_tree_ips (p⇩1 ∥ p⇩2)) ((σ, st), a, (σ', st'))" by simp
    qed
  qed

theorem subnet_oreachable:
  assumes "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2))
                                (otherwith S (net_tree_ips (p⇩1 ∥ p⇩2)) (oarrivemsg I))
                                (other U (net_tree_ips (p⇩1 ∥ p⇩2)))"
          (is "_ ∈ oreachable _ (?S (p⇩1 ∥ p⇩2)) (?U (p⇩1 ∥ p⇩2))")

      and "⋀ξ. S ξ ξ"
      and "⋀ξ. U ξ ξ"

      and node1: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, _). castmsg (I σ) a)"
      and node2: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, σ'). (a ≠ τ ∧ (∀d. a ≠ i:deliver(d)) ⟶ S (σ i) (σ' i)))"
      and node3: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, σ'). (a = τ ∨ (∃d. a = i:deliver(d)) ⟶ U (σ i) (σ' i)))"

    shows "(σ, s) ∈ oreachable (opnet onp p⇩1)
                               (otherwith S (net_tree_ips p⇩1) (oarrivemsg I))
                               (other U (net_tree_ips p⇩1))
           ∧ (σ, t) ∈ oreachable (opnet onp p⇩2)
                                  (otherwith S (net_tree_ips p⇩2) (oarrivemsg I))
                                  (other U (net_tree_ips p⇩2))
           ∧ net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}"
  using assms(1) proof (induction rule: oreachable_par_subnet_induct)
    case (init σ s t)
    hence sinit: "(σ, s) ∈ init (opnet onp p⇩1)"
      and tinit: "(σ, t) ∈ init (opnet onp p⇩2)"
      and "net_ips s ∩ net_ips t = {}" by auto
    moreover from sinit have "net_ips s = net_tree_ips p⇩1"
      by (rule opnet_net_ips_net_tree_ips_init)
    moreover from tinit have "net_ips t = net_tree_ips p⇩2"
      by (rule opnet_net_ips_net_tree_ips_init)
    ultimately show ?case by (auto elim: oreachable_init)
  next
    case (other σ s t σ')
    hence "other U (net_tree_ips (p⇩1 ∥ p⇩2)) σ σ'"
      and IHs: "(σ, s) ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
      and IHt: "(σ, t) ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
      and "net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}" by auto

    have "(σ', s) ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
    proof -
      from ‹?U (p⇩1 ∥ p⇩2) σ σ'› and ‹⋀ξ. U ξ ξ› have "?U p⇩1 σ σ'"
        by (rule other_net_tree_ips_par_left)
      with IHs show ?thesis by - (erule(1) oreachable_other')
    qed

    moreover have "(σ', t) ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
    proof -
      from ‹?U (p⇩1 ∥ p⇩2) σ σ'› and ‹⋀ξ. U ξ ξ› have "?U p⇩2 σ σ'"
        by (rule other_net_tree_ips_par_right)
      with IHt show ?thesis by - (erule(1) oreachable_other')
    qed

    ultimately show ?case using ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}› by simp
  next
    case (local σ s t σ' s' t' a)
    hence stor: "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) (?S (p⇩1 ∥ p⇩2)) (?U (p⇩1 ∥ p⇩2))"
      and tr: "((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p⇩1 ∥ p⇩2))"
      and "?S (p⇩1 ∥ p⇩2) σ σ' a"
      and sor: "(σ, s) ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
      and tor: "(σ, t) ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
      and "net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}" by auto

    have act: "⋀p. opnet onp p ⊨⇩A (λσ _. oarrivemsg I σ, other U (net_tree_ips p) →)
                 globala (λ(σ, a, σ'). castmsg (I σ) a
                                        ∧ (a ≠ τ ∧ (∀i d. a ≠ i:deliver(d)) ⟶
                                               (∀i∈net_tree_ips p. S (σ i) (σ' i)))
                                        ∧ (a = τ ∨ (∃i d. a = i:deliver(d)) ⟶
                                               ((∀i∈net_tree_ips p. U (σ i) (σ' i))
                                             ∧ (∀i. i∉net_tree_ips p ⟶ σ' i = σ i))))"
      by (rule lift_opnet_sync_action [OF assms(3-6)])

    from ‹?S (p⇩1 ∥ p⇩2) σ σ' a› have "∀j. j ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ S (σ j) (σ' j)"
                                and "oarrivemsg I σ a"
      by (auto elim!: otherwithE)
    from tr have "((σ, SubnetS s t), a, (σ', SubnetS s' t'))
                    ∈ opnet_sos (trans (opnet onp p⇩1)) (trans (opnet onp p⇩2))" by simp
    hence "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)
         ∧ (σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
    proof (cases)
      fix H K m H' K'
      assume "a = (H ∪ H')¬(K ∪ K'):arrive(m)"
         and str: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), H'¬K':arrive(m), (σ', t')) ∈ trans (opnet onp p⇩2)"
      from this(1) and ‹?S (p⇩1 ∥ p⇩2) σ σ' a› have "I σ m" by auto

      with sor str have "∀i∈net_tree_ips p⇩1. S (σ i) (σ' i)"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      moreover from ‹I σ m› tor ttr have "∀i∈net_tree_ips p⇩2. S (σ i) (σ' i)"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      ultimately have "∀i. S (σ i) (σ' i)"
        using ‹∀j. j ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ S (σ j) (σ' j)› by auto

      with ‹I σ m› sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹∀i. S (σ i) (σ' i)› ‹I σ m› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix R m H K
      assume str: "((σ, s), R:*cast(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), H¬K:arrive(m), (σ', t')) ∈ trans (opnet onp p⇩2)"                                    
      from sor str have "I σ m"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      with sor str tor ttr have "∀i. S (σ i) (σ' i)"
        using ‹∀j. j ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ S (σ j) (σ' j)›
        by (fastforce dest!: ostep_arrive_invariantD [OF act] ostep_arrive_invariantD [OF act])
      with ‹I σ m› sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹∀i. S (σ i) (σ' i)› ‹I σ m› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix R m H K
      assume str: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), R:*cast(m), (σ', t')) ∈ trans (opnet onp p⇩2)"                                    
      from tor ttr have "I σ m"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      with sor str tor ttr have "∀i. S (σ i) (σ' i)"
        using ‹∀j. j ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ S (σ j) (σ' j)›
        by (fastforce dest!: ostep_arrive_invariantD [OF act] ostep_arrive_invariantD [OF act])
      with ‹I σ m› sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹∀i. S (σ i) (σ' i)› ‹I σ m› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix i i'
      assume str: "((σ, s), connect(i, i'), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), connect(i, i'), (σ', t')) ∈ trans (opnet onp p⇩2)"
      with sor tor have "∀i. S (σ i) (σ' i)"
        using ‹∀j. j ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ S (σ j) (σ' j)›
        by (fastforce dest!: ostep_arrive_invariantD [OF act] ostep_arrive_invariantD [OF act])
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹∀i. S (σ i) (σ' i)› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix i i'
      assume str: "((σ, s), disconnect(i, i'), (σ', s')) ∈ trans (opnet onp p⇩1)"
         and ttr: "((σ, t), disconnect(i, i'), (σ', t')) ∈ trans (opnet onp p⇩2)"
      with sor tor have "∀i. S (σ i) (σ' i)"
        using ‹∀j. j ∉ net_tree_ips (p⇩1 ∥ p⇩2) ⟶ S (σ j) (σ' j)›
        by (fastforce dest!: ostep_arrive_invariantD [OF act] ostep_arrive_invariantD [OF act])
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)
      moreover from ‹∀i. S (σ i) (σ' i)› tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    next
      fix i d
      assume "t' = t"
         and str: "((σ, s), i:deliver(d), (σ', s')) ∈ trans (opnet onp p⇩1)"
      from sor str have "∀j. j∉net_tree_ips p⇩1 ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p⇩1 ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹⋀ξ. S ξ ξ›)
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
      proof -
        from ‹∀j. j∉net_tree_ips p⇩1 ⟶ σ' j = σ j› and ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
          have "∀j. j∈net_tree_ips p⇩2 ⟶ σ' j = σ j" by auto
        moreover from sor str have "∀j∈net_tree_ips p⇩1. U (σ j) (σ' j)"
          by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
        ultimately show ?thesis
          using tor ‹t' = t› ‹∀j. j ∉ net_tree_ips p⇩1 ⟶ σ' j = σ j›
          by (clarsimp elim!: oreachable_other')
             (metis otherI ‹⋀ξ. U ξ ξ›)+
      qed
      ultimately show ?thesis ..
    next
      fix i d
      assume "s' = s"
         and ttr: "((σ, t), i:deliver(d), (σ', t')) ∈ trans (opnet onp p⇩2)"
      from tor ttr have "∀j. j∉net_tree_ips p⇩2 ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p⇩2 ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹⋀ξ. S ξ ξ›)
      with tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
      proof -
        from ‹∀j. j∉net_tree_ips p⇩2 ⟶ σ' j = σ j› and ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
          have "∀j. j∈net_tree_ips p⇩1 ⟶ σ' j = σ j" by auto
        moreover from tor ttr have "∀j∈net_tree_ips p⇩2. U (σ j) (σ' j)"
          by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
        ultimately show ?thesis
          using sor ‹s' = s› ‹∀j. j ∉ net_tree_ips p⇩2 ⟶ σ' j = σ j›
          by (clarsimp elim!: oreachable_other')
             (metis otherI ‹⋀ξ. U ξ ξ›)+
      qed
      ultimately show ?thesis by - (rule conjI)
    next
      assume "s' = s"
         and ttr: "((σ, t), τ, (σ', t')) ∈ trans (opnet onp p⇩2)"
      from tor ttr have "∀j. j∉net_tree_ips p⇩2 ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p⇩2 ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹⋀ξ. S ξ ξ›)
      with tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
      proof -
        from ‹∀j. j∉net_tree_ips p⇩2 ⟶ σ' j = σ j› and ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
          have "∀j. j∈net_tree_ips p⇩1 ⟶ σ' j = σ j" by auto
        moreover from tor ttr have "∀j∈net_tree_ips p⇩2. U (σ j) (σ' j)"
          by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
        ultimately show ?thesis
          using sor ‹s' = s› ‹∀j. j ∉ net_tree_ips p⇩2 ⟶ σ' j = σ j›
          by (clarsimp elim!: oreachable_other')
             (metis otherI ‹⋀ξ. U ξ ξ›)+
      qed
      ultimately show ?thesis by - (rule conjI)
    next
      assume "t' = t"
         and str: "((σ, s), τ, (σ', s')) ∈ trans (opnet onp p⇩1)"
      from sor str have "∀j. j∉net_tree_ips p⇩1 ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p⇩1 ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹⋀ξ. S ξ ξ›)
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p⇩1) (?S p⇩1) (?U p⇩1)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', t') ∈ oreachable (opnet onp p⇩2) (?S p⇩2) (?U p⇩2)"
      proof -
        from ‹∀j. j∉net_tree_ips p⇩1 ⟶ σ' j = σ j› and ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}›
          have "∀j. j∈net_tree_ips p⇩2 ⟶ σ' j = σ j" by auto
        moreover from sor str have "∀j∈net_tree_ips p⇩1. U (σ j) (σ' j)"
          by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
        ultimately show ?thesis
          using tor ‹t' = t› ‹∀j. j ∉ net_tree_ips p⇩1 ⟶ σ' j = σ j›
          by (clarsimp elim!: oreachable_other')
             (metis otherI ‹⋀ξ. U ξ ξ›)+
      qed
      ultimately show ?thesis ..
    qed
    with ‹net_tree_ips p⇩1 ∩ net_tree_ips p⇩2 = {}› show ?case by simp
  qed

lemmas subnet_oreachable1 [dest] = subnet_oreachable [THEN conjunct1, rotated 1]
lemmas subnet_oreachable2 [dest] = subnet_oreachable [THEN conjunct2, THEN conjunct1, rotated 1]
lemmas subnet_oreachable_disjoint [dest] = subnet_oreachable
                                                    [THEN conjunct2, THEN conjunct2, rotated 1]

corollary pnet_lift:
  assumes "⋀ii R⇩i. ⟨ii : onp ii : R⇩i⟩⇩o
              ⊨ (otherwith S {ii} (oarrivemsg I), other U {ii} →) global (P ii)"

      and "⋀ξ. S ξ ξ"
      and "⋀ξ. U ξ ξ"

      and node1: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, _). castmsg (I σ) a)"
      and node2: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, σ'). (a ≠ τ ∧ (∀d. a ≠ i:deliver(d)) ⟶ S (σ i) (σ' i)))"
      and node3: "⋀i R. ⟨i : onp i : R⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other U {i} →)
                      globala (λ(σ, a, σ'). (a = τ ∨ (∃d. a = i:deliver(d)) ⟶ U (σ i) (σ' i)))"

    shows "opnet onp p ⊨ (otherwith S (net_tree_ips p) (oarrivemsg I),
                       other U (net_tree_ips p) →) global (λσ. ∀i∈net_tree_ips p. P i σ)"
      (is "_ ⊨ (?owS p, ?U p →) _")
  proof (induction p)
    fix ii R⇩i
    from assms(1) show "opnet onp ⟨ii; R⇩i⟩ ⊨ (?owS ⟨ii; R⇩i⟩, ?U ⟨ii; R⇩i⟩ →)
                                         global (λσ. ∀i∈net_tree_ips ⟨ii; R⇩i⟩. P i σ)" by auto
  next
    fix p⇩1 p⇩2
    assume ih1: "opnet onp p⇩1 ⊨ (?owS p⇩1, ?U p⇩1 →) global (λσ. ∀i∈net_tree_ips p⇩1. P i σ)"
       and ih2: "opnet onp p⇩2 ⊨ (?owS p⇩2, ?U p⇩2 →) global (λσ. ∀i∈net_tree_ips p⇩2. P i σ)"
    show "opnet onp (p⇩1 ∥ p⇩2) ⊨ (?owS (p⇩1 ∥ p⇩2), ?U (p⇩1 ∥ p⇩2) →)
                             global (λσ. ∀i∈net_tree_ips (p⇩1 ∥ p⇩2). P i σ)"
    unfolding oinvariant_def
    proof
      fix pq
      assume "pq ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2)) (?owS (p⇩1 ∥ p⇩2)) (?U (p⇩1 ∥ p⇩2))"
      moreover then obtain σ s t where "pq = (σ, SubnetS s t)"
        by (metis net_par_oreachable_is_subnet surjective_pairing)
      ultimately have "(σ, SubnetS s t) ∈ oreachable (opnet onp (p⇩1 ∥ p⇩2))
                                               (?owS (p⇩1 ∥ p⇩2)) (?U (p⇩1 ∥ p⇩2))" by simp
      then obtain sor: "(σ, s) ∈ oreachable (opnet onp p⇩1) (?owS p⇩1) (?U p⇩1)"
              and tor: "(σ, t) ∈ oreachable (opnet onp p⇩2) (?owS p⇩2) (?U p⇩2)"
        by - (drule subnet_oreachable [OF _ _ _ node1 node2 node3], auto intro: assms(2-3))
      from sor have "∀i∈net_tree_ips p⇩1. P i σ"
        by (auto dest: oinvariantD [OF ih1])
      moreover from tor have "∀i∈net_tree_ips p⇩2. P i σ"
        by (auto dest: oinvariantD [OF ih2])
      ultimately have "∀i∈net_tree_ips (p⇩1 ∥ p⇩2). P i σ" by auto
      with ‹pq = (σ, SubnetS s t)› show "global (λσ. ∀i∈net_tree_ips (p⇩1 ∥ p⇩2). P i σ) pq" by simp
    qed
  qed

end