(*  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₁ ∥ p₂)) S U"
      and init: "∧σ s t. (σ, SubnetS s t) ∈ init (opnet onp (p₁ ∥ p₂)) ==> P σ s t"
      and other: "∧σ s t σ'. [ (σ, SubnetS s t) ∈ oreachable (opnet onp (p₁ ∥ p₂)) S U;
                                U σ σ'; P σ s t ] ==> P σ' s t"
      and local: "∧σ s t σ' s' t' a. [ (σ, SubnetS s t) ∈ oreachable (opnet onp (p₁ ∥ p₂)) S U;
                    ((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p₁ ∥ p₂));
                    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₁ ∥ p₂))"
    with init show "P σ s t" .
  next
    fix st a s' t' σ'
    assume "st ∈ oreachable (opnet onp (p₁ ∥ p₂)) S U"
       and tr: "(st, a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p₁ ∥ p₂))"
       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₁ ∥ p₂)) 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₁ ∥ p₂))" 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₁ ∥ p₂)) 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₁ ∥ p₂)) 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₁ ∥ p₂)) σ σ'"
      and "∧ξ. U ξ ξ"
    shows "other U (net_tree_ips p₁) σ σ'"
  proof -
    from assms(1) obtain ineq: "∀i∈net_tree_ips (p₁ ∥ p₂). σ' i = σ i"
                     and outU: "∀j. j∉net_tree_ips (p₁ ∥ p₂) ⟶ U (σ j) (σ' j)" ..
    show ?thesis
    proof (rule otherI)
      fix i
      assume "i∈net_tree_ips p₁"
      hence "i∈net_tree_ips (p₁ ∥ p₂)" by simp
      with ineq show "σ' i = σ i" ..
    next
      fix j
      assume "j∉net_tree_ips p₁"
      show "U (σ j) (σ' j)"
      proof (cases "j∈net_tree_ips p₂")
        assume "j∈net_tree_ips p₂"
        hence "j∈net_tree_ips (p₁ ∥ p₂)" by simp
        with ineq have "σ' j = σ j" ..
        thus "U (σ j) (σ' j)"
          by simp (rule ‹∧ξ. U ξ ξ›)
      next
        assume "j∉net_tree_ips p₂"
        with ‹j∉net_tree_ips p₁› have "j∉net_tree_ips (p₁ ∥ p₂)" 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₁ ∥ p₂)) σ σ'"
      and "∧ξ. U ξ ξ"
    shows "other U (net_tree_ips p₂) σ σ'"
  proof -
    from assms(1) have "other U (net_tree_ips (p₂ ∥ p₁)) σ σ'"
      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₁ ∥ p₂))
                                         (λσ _. oarrivemsg I σ) (other U (net_tree_ips (p₁ ∥ p₂)))"
          (is "_ ∈ oreachable _ (?S (p₁ ∥ p₂)) (?U (p₁ ∥ p₂))")

      and "∧ξ. U ξ ξ"

      and act1: "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₁. U (σ i) (σ' i))
                                               ∧ (∀i. i∉net_tree_ips p₁ ⟶ σ' i = σ i))))"

      and act2: "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₂. U (σ i) (σ' i))
                                               ∧ (∀i. i∉net_tree_ips p₂ ⟶ σ' i = σ i))))"

    shows "(σ, s) ∈ oreachable (opnet onp p₁) (λσ _. oarrivemsg I σ) (other U (net_tree_ips p₁))
           ∧ (σ, t) ∈ oreachable (opnet onp p₂) (λσ _. oarrivemsg I σ) (other U (net_tree_ips p₂))
           ∧ net_tree_ips p₁ ∩ net_tree_ips p₂ = {}"
  using assms(1)
  proof (induction rule: oreachable_par_subnet_induct)
    case (init σ s t)
    hence sinit: "(σ, s) ∈ init (opnet onp p₁)"
      and tinit: "(σ, t) ∈ init (opnet onp p₂)"
      and "net_ips s ∩ net_ips t = {}" by auto
    moreover from sinit have "net_ips s = net_tree_ips p₁"
      by (rule opnet_net_ips_net_tree_ips_init)
    moreover from tinit have "net_ips t = net_tree_ips p₂"
      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₁ ∥ p₂)) σ σ'"
      and IHs: "(σ, s) ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
      and IHt: "(σ, t) ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
      and "net_tree_ips p₁ ∩ net_tree_ips p₂ = {}" by auto

    have "(σ', s) ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
    proof -
      from ‹?U (p₁ ∥ p₂) σ σ'› and ‹∧ξ. U ξ ξ› have "?U p₁ σ σ'"
        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₂) (?S p₂) (?U p₂)"
    proof -
      from ‹?U (p₁ ∥ p₂) σ σ'› and ‹∧ξ. U ξ ξ› have "?U p₂ σ σ'"
        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₁ ∩ net_tree_ips p₂ = {}› by simp
  next
    case (local σ s t σ' s' t' a)
    hence stor: "(σ, SubnetS s t) ∈ oreachable (opnet onp (p₁ ∥ p₂)) (?S (p₁ ∥ p₂)) (?U (p₁ ∥ p₂))"
      and tr: "((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p₁ ∥ p₂))"
      and "oarrivemsg I σ a"
      and sor: "(σ, s) ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
      and tor: "(σ, t) ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
      and "net_tree_ips p₁ ∩ net_tree_ips p₂ = {}" by auto
    from tr have "((σ, SubnetS s t), a, (σ', SubnetS s' t'))
                    ∈ opnet_sos (trans (opnet onp p₁)) (trans (opnet onp p₂))" by simp
    hence "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)
         ∧ (σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
    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₁)"
         and ttr: "((σ, t), H'¬K':arrive(m), (σ', t')) ∈ trans (opnet onp p₂)"
      from this(1) and ‹oarrivemsg I σ a› have "I σ m" by simp

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

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

      moreover from sor str
        have "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
          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₂)"

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

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

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

      moreover from sor str
        have "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
          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₂)"

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

      moreover from tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
          by - (erule(1) oreachable_local, auto)
      ultimately show ?thesis ..
    qed
    with ‹net_tree_ips p₁ ∩ net_tree_ips p₂ = {}› 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₁ s₂) ∈ oreachable (opnet onp (p₁ ∥ p₂)) (λ_ _ _. True) (λ_ _. True)"
    shows "(σ, s₁) ∈ oreachable (opnet onp p₁) (λ_ _ _. True) (λ_ _. True)"
          "(σ, s₂) ∈ oreachable (opnet onp p₂) (λ_ _ _. True) (λ_ _. True)"
          (is "_ ∈ ?oreachable p₂")
  using assms proof -
    from assms have "(σ, s₁) ∈ ?oreachable p₁ ∧ (σ, s₂) ∈ ?oreachable p₂"
    proof (induction rule: oreachable_par_subnet_induct)
      fix σ s₁ s₂
      assume "(σ, SubnetS s₁ s₂) ∈ init (opnet onp (p₁ ∥ p₂))"
      thus "(σ, s₁) ∈ ?oreachable p₁ ∧ (σ, s₂) ∈ ?oreachable p₂"
        by (auto dest: oreachable_init)
    next
      case (local σ s₁ s₂ σ' s₁' s₂' a)
      hence "(σ, SubnetS s₁ s₂) ∈ ?oreachable (p₁ ∥ p₂)"
        and sr1: "(σ, s₁) ∈ ?oreachable p₁"
        and sr2: "(σ, s₂) ∈ ?oreachable p₂"
        and "((σ, SubnetS s₁ s₂), a, (σ', SubnetS s₁' s₂')) ∈ trans (opnet onp (p₁ ∥ p₂))" by auto
      from this(4)
        have "((σ, SubnetS s₁ s₂), a, (σ', SubnetS s₁' s₂'))
                ∈ opnet_sos (trans (opnet onp p₁)) (trans (opnet onp p₂))" by simp
      thus "(σ', s₁') ∈ ?oreachable p₁ ∧ (σ', s₂') ∈ ?oreachable p₂"
      proof cases
        fix R m H K
        assume "a = R:*cast(m)"
           and tr1: "((σ, s₁), R:*cast(m), (σ', s₁')) ∈ trans (opnet onp p₁)"
           and tr2: "((σ, s₂), H¬K:arrive(m), (σ', s₂')) ∈ trans (opnet onp p₂)"
        from sr1 and tr1 and TrueI have "(σ', s₁') ∈ ?oreachable p₁"
          by (rule oreachable_local')
        moreover from sr2 and tr2 and TrueI have "(σ', s₂') ∈ ?oreachable p₂"
          by (rule oreachable_local')
        ultimately show ?thesis ..
      next
        assume "a = τ"
           and "s₂' = s₂"
           and tr1: "((σ, s₁), τ, (σ', s₁')) ∈ trans (opnet onp p₁)"
        from sr2 and this(2) have "(σ', s₂') ∈ ?oreachable p₂" by auto
        moreover have "(λ_ _. True) σ σ'" by (rule TrueI)
        ultimately have "(σ', s₂') ∈ ?oreachable p₂"
          by (rule oreachable_other')
        moreover from sr1 and tr1 and TrueI have "(σ', s₁') ∈ ?oreachable p₁"
          by (rule oreachable_local')
      qed (insert sr1 sr2, simp_all, (metis (no_types) oreachable_local'
                                                       oreachable_other')+)
    qed auto
    thus "(σ, s₁) ∈ ?oreachable p₁"
         "(σ, s₂) ∈ ?oreachable p₂" by auto
  qed

text ‹
 It may also be tempting to try splitting from the assumption
 @{term "(σ, SubnetS s₁ s₂) ∈ oreachable (opnet onp (p₁ ∥ p₂)) (λ_ _ _. 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₁ p₂
    assume inv1: "opnet onp p₁ ⊨_A (?I, ?U p₁ →) ?inv (net_tree_ips p₁)"
       and inv2: "opnet onp p₂ ⊨_A (?I, ?U p₂ →) ?inv (net_tree_ips p₂)"
    show "opnet onp (p₁ ∥ p₂) ⊨_A (?I, ?U (p₁ ∥ p₂) →) ?inv (net_tree_ips (p₁ ∥ p₂))"
    proof (rule ostep_invariantI)
      fix σ st a σ' st'
      assume "(σ, st) ∈ oreachable (opnet onp (p₁ ∥ p₂)) ?I (?U (p₁ ∥ p₂))"
         and "((σ, st), a, (σ', st')) ∈ trans (opnet onp (p₁ ∥ p₂))"
         and "oarrivemsg I σ a"
      from this(1) obtain s t
        where "st = SubnetS s t"
          and *: "(σ, SubnetS s t) ∈ oreachable (opnet onp (p₁ ∥ p₂)) ?I (?U (p₁ ∥ p₂))"
        by - (frule net_par_oreachable_is_subnet, metis)

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

      from * and ‹((σ, st), a, (σ', st')) ∈ trans (opnet onp (p₁ ∥ p₂))› 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₁)) (trans (opnet onp p₂))"
          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₁ ∥ p₂). S (σ i) (σ' i)))
             ∧ (a = τ ∨ (∃i d. a = i:deliver(d)) ⟶ (∀i∈net_tree_ips (p₁ ∥ p₂). U (σ i) (σ' i))
                                                  ∧ (∀i. i ∉ net_tree_ips (p₁ ∥ p₂) ⟶ σ' 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₁)"
           and ttr: "((σ, t), H¬K:arrive(m), (σ', t')) ∈ trans (opnet onp p₂)"
        from sor and str have "I σ m ∧ (∀i∈net_tree_ips p₁. S (σ i) (σ' i))"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover with tor and ttr have "∀i∈net_tree_ips p₂. 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₁)"
           and ttr: "((σ, t), R:*cast(m), (σ', t')) ∈ trans (opnet onp p₂)"
        from tor and ttr have "I σ m ∧ (∀i∈net_tree_ips p₂. S (σ i) (σ' i))"
          by (auto dest: ostep_invariantD [OF inv2])
        moreover with sor and str have "∀i∈net_tree_ips p₁. 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₁)"
           and ttr: "((σ, t), H'¬K':arrive(m), (σ', t')) ∈ trans (opnet onp p₂)"
        from this(1) and ‹oarrivemsg I σ a› have "I σ m" by simp
        with sor and str have "∀i∈net_tree_ips p₁. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover from tor and ttr and ‹I σ m› have "∀i∈net_tree_ips p₂. 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₁)"
        with sor have "((∀i∈net_tree_ips p₁. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p₁ ⟶ σ' 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₂)"
        with tor have "((∀i∈net_tree_ips p₂. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p₂ ⟶ σ' 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₁)"
        with sor have "((∀i∈net_tree_ips p₁. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p₁ ⟶ σ' 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₂)"
        with tor have "((∀i∈net_tree_ips p₂. U (σ i) (σ' i))
                       ∧ (∀i. i∉net_tree_ips p₂ ⟶ σ' 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₁)"
           and ttr: "((σ, t), connect(i, i'), (σ', t')) ∈ trans (opnet onp p₂)"
        from sor and str have "∀i∈net_tree_ips p₁. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover from tor and ttr have "∀i∈net_tree_ips p₂. 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₁)"
           and ttr: "((σ, t), disconnect(i, i'), (σ', t')) ∈ trans (opnet onp p₂)"
        from sor and str have "∀i∈net_tree_ips p₁. S (σ i) (σ' i)"
          by (auto dest: ostep_invariantD [OF inv1])
        moreover from tor and ttr have "∀i∈net_tree_ips p₂. 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₁ ∥ p₂)) ((σ, st), a, (σ', st'))" by simp
    qed
  qed

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

      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₁)
                               (otherwith S (net_tree_ips p₁) (oarrivemsg I))
                               (other U (net_tree_ips p₁))
           ∧ (σ, t) ∈ oreachable (opnet onp p₂)
                                  (otherwith S (net_tree_ips p₂) (oarrivemsg I))
                                  (other U (net_tree_ips p₂))
           ∧ net_tree_ips p₁ ∩ net_tree_ips p₂ = {}"
  using assms(1) proof (induction rule: oreachable_par_subnet_induct)
    case (init σ s t)
    hence sinit: "(σ, s) ∈ init (opnet onp p₁)"
      and tinit: "(σ, t) ∈ init (opnet onp p₂)"
      and "net_ips s ∩ net_ips t = {}" by auto
    moreover from sinit have "net_ips s = net_tree_ips p₁"
      by (rule opnet_net_ips_net_tree_ips_init)
    moreover from tinit have "net_ips t = net_tree_ips p₂"
      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₁ ∥ p₂)) σ σ'"
      and IHs: "(σ, s) ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
      and IHt: "(σ, t) ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
      and "net_tree_ips p₁ ∩ net_tree_ips p₂ = {}" by auto

    have "(σ', s) ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
    proof -
      from ‹?U (p₁ ∥ p₂) σ σ'› and ‹∧ξ. U ξ ξ› have "?U p₁ σ σ'"
        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₂) (?S p₂) (?U p₂)"
    proof -
      from ‹?U (p₁ ∥ p₂) σ σ'› and ‹∧ξ. U ξ ξ› have "?U p₂ σ σ'"
        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₁ ∩ net_tree_ips p₂ = {}› by simp
  next
    case (local σ s t σ' s' t' a)
    hence stor: "(σ, SubnetS s t) ∈ oreachable (opnet onp (p₁ ∥ p₂)) (?S (p₁ ∥ p₂)) (?U (p₁ ∥ p₂))"
      and tr: "((σ, SubnetS s t), a, (σ', SubnetS s' t')) ∈ trans (opnet onp (p₁ ∥ p₂))"
      and "?S (p₁ ∥ p₂) σ σ' a"
      and sor: "(σ, s) ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
      and tor: "(σ, t) ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
      and "net_tree_ips p₁ ∩ net_tree_ips p₂ = {}" 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₁ ∥ p₂) σ σ' a› have "∀j. j ∉ net_tree_ips (p₁ ∥ p₂) ⟶ 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₁)) (trans (opnet onp p₂))" by simp
    hence "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)
         ∧ (σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
    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₁)"
         and ttr: "((σ, t), H'¬K':arrive(m), (σ', t')) ∈ trans (opnet onp p₂)"
      from this(1) and ‹?S (p₁ ∥ p₂) σ σ' a› have "I σ m" by auto

      with sor str have "∀i∈net_tree_ips p₁. 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₂. 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₁ ∥ p₂) ⟶ S (σ j) (σ' j)› by auto

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

      moreover have "(σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
      proof -
        from ‹∀j. j∉net_tree_ips p₁ ⟶ σ' j = σ j› and ‹net_tree_ips p₁ ∩ net_tree_ips p₂ = {}›
          have "∀j. j∈net_tree_ips p₂ ⟶ σ' j = σ j" by auto
        moreover from sor str have "∀j∈net_tree_ips p₁. 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₁ ⟶ σ' 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₂)"
      from tor ttr have "∀j. j∉net_tree_ips p₂ ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p₂ ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹∧ξ. S ξ ξ›)
      with tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
      proof -
        from ‹∀j. j∉net_tree_ips p₂ ⟶ σ' j = σ j› and ‹net_tree_ips p₁ ∩ net_tree_ips p₂ = {}›
          have "∀j. j∈net_tree_ips p₁ ⟶ σ' j = σ j" by auto
        moreover from tor ttr have "∀j∈net_tree_ips p₂. 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₂ ⟶ σ' 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₂)"
      from tor ttr have "∀j. j∉net_tree_ips p₂ ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p₂ ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹∧ξ. S ξ ξ›)
      with tor ttr
        have "(σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
      proof -
        from ‹∀j. j∉net_tree_ips p₂ ⟶ σ' j = σ j› and ‹net_tree_ips p₁ ∩ net_tree_ips p₂ = {}›
          have "∀j. j∈net_tree_ips p₁ ⟶ σ' j = σ j" by auto
        moreover from tor ttr have "∀j∈net_tree_ips p₂. 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₂ ⟶ σ' 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₁)"
      from sor str have "∀j. j∉net_tree_ips p₁ ⟶ σ' j = σ j"
        by - (drule(1) ostep_arrive_invariantD [OF act], simp_all)
      hence "∀j. j∉net_tree_ips p₁ ⟶ S (σ j) (σ' j)"
         by (auto intro: ‹∧ξ. S ξ ξ›)
      with sor str
        have "(σ', s') ∈ oreachable (opnet onp p₁) (?S p₁) (?U p₁)"
          by - (erule(1) oreachable_local, auto)

      moreover have "(σ', t') ∈ oreachable (opnet onp p₂) (?S p₂) (?U p₂)"
      proof -
        from ‹∀j. j∉net_tree_ips p₁ ⟶ σ' j = σ j› and ‹net_tree_ips p₁ ∩ net_tree_ips p₂ = {}›
          have "∀j. j∈net_tree_ips p₂ ⟶ σ' j = σ j" by auto
        moreover from sor str have "∀j∈net_tree_ips p₁. 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₁ ⟶ σ' j = σ j›
          by (clarsimp elim!: oreachable_other')
             (metis otherI ‹∧ξ. U ξ ξ›)+
      qed
      ultimately show ?thesis ..
    qed
    with ‹net_tree_ips p₁ ∩ net_tree_ips p₂ = {}› 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₁ p₂
    assume ih1: "opnet onp p₁ ⊨ (?owS p₁, ?U p₁ →) global (λσ. ∀i∈net_tree_ips p₁. P i σ)"
       and ih2: "opnet onp p₂ ⊨ (?owS p₂, ?U p₂ →) global (λσ. ∀i∈net_tree_ips p₂. P i σ)"
    show "opnet onp (p₁ ∥ p₂) ⊨ (?owS (p₁ ∥ p₂), ?U (p₁ ∥ p₂) →)
                             global (λσ. ∀i∈net_tree_ips (p₁ ∥ p₂). P i σ)"
    unfolding oinvariant_def
    proof
      fix pq
      assume "pq ∈ oreachable (opnet onp (p₁ ∥ p₂)) (?owS (p₁ ∥ p₂)) (?U (p₁ ∥ p₂))"
      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₁ ∥ p₂))
                                               (?owS (p₁ ∥ p₂)) (?U (p₁ ∥ p₂))" by simp
      then obtain sor: "(σ, s) ∈ oreachable (opnet onp p₁) (?owS p₁) (?U p₁)"
              and tor: "(σ, t) ∈ oreachable (opnet onp p₂) (?owS p₂) (?U p₂)"
        by - (drule subnet_oreachable [OF _ _ _ node1 node2 node3], auto intro: assms(2-3))
      from sor have "∀i∈net_tree_ips p₁. P i σ"
        by (auto dest: oinvariantD [OF ih1])
      moreover from tor have "∀i∈net_tree_ips p₂. P i σ"
        by (auto dest: oinvariantD [OF ih2])
      ultimately have "∀i∈net_tree_ips (p₁ ∥ p₂). P i σ" by auto
      with ‹pq = (σ, SubnetS s t)› show "global (λσ. ∀i∈net_tree_ips (p₁ ∥ p₂). P i σ) pq" by simp
    qed
  qed

end