Theory OClosed_Transfer

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

section "Transfer open results onto closed models"

theory OClosed_Transfer
imports Closed OClosed_Lifting
begin

locale openproc =
  fixes np  :: "ip  ('s, ('m::msg) seq_action) automaton"
    and onp :: "ip  ((ip  'g) × 'l, 'm seq_action) automaton"
    and sr  :: "'s  ('g × 'l)"
  assumes  init: "{ (σ, ζ) |σ ζ s. s  init (np i)
                              (σ i, ζ) = sr s
                              (j. ji  σ j  (fst o sr) ` init (np j)) }  init (onp i)"
      and init_notempty: "j. init (np j)  {}"
      and trans: "s a s' σ σ'.  σ i = fst (sr s);
                                  σ' i = fst (sr s');
                                  (s, a, s')  trans (np i) 
                    ((σ, snd (sr s)), a, (σ', snd (sr s')))  trans (onp i)"
begin

lemma init_pnet_p_NodeS:
  assumes "NodeS i s R  init (pnet np p)"
    shows "p = i; R"
  using assms by (cases p) (auto simp add: node_comps)

lemma init_pnet_p_SubnetS:
  assumes "SubnetS s1 s2  init (pnet np p)"
  obtains p1 p2 where "p = (p1  p2)"
                  and "s1  init (pnet np p1)"
                  and "s2  init (pnet np p2)"
  using assms by (cases p) (auto simp add: node_comps)

lemma init_pnet_fst_sr_netgmap:
  assumes "s  init (pnet np p)"
      and "i  net_ips s"
      and "wf_net_tree p"
    shows "the (fst (netgmap sr s) i)  (fst  sr) ` init (np i)"
  using assms proof (induction s arbitrary: p)
    fix ii s Ri p
    assume "NodeS ii s Ri  init (pnet np p)"
       and "i  net_ips (NodeS ii s Ri)"
       and "wf_net_tree p"
    note this(1)
    moreover then have "p = ii; Ri"
      by (rule init_pnet_p_NodeS)
    ultimately have "s  init (np ii)"
      by (clarsimp simp: node_comps)
    with i  net_ips (NodeS ii s Ri)
      show "the (fst (netgmap sr (NodeS ii s Ri)) i)  (fst  sr) ` init (np i)"
        by clarsimp
  next
    fix s1 s2 p
    assume IH1: "p. s1  init (pnet np p)
                   i  net_ips s1
                   wf_net_tree p
                   the (fst (netgmap sr s1) i)  (fst  sr) ` init (np i)"
       and IH2: "p. s2  init (pnet np p)
                   i  net_ips s2
                   wf_net_tree p
                   the (fst (netgmap sr s2) i)  (fst  sr) ` init (np i)"
       and "SubnetS s1 s2  init (pnet np p)"
       and "i  net_ips (SubnetS s1 s2)"
       and "wf_net_tree p"
    from this(3) obtain p1 p2 where "p = (p1  p2)"
                                and "s1  init (pnet np p1)"
                                and "s2  init (pnet np p2)"
      by (rule init_pnet_p_SubnetS)
    from this(1) and wf_net_tree p have "wf_net_tree p1"
                                      and "wf_net_tree p2"
                                      and "net_tree_ips p1  net_tree_ips p2 = {}"
      by auto
    from i  net_ips (SubnetS s1 s2) have "i  net_ips s1  i  net_ips s2"
      by simp
    thus "the (fst (netgmap sr (SubnetS s1 s2)) i)  (fst  sr) ` init (np i)"
    proof
      assume "i  net_ips s1"
      hence "i  net_ips s2"
      proof -
        from s1  init (pnet np p1) and i  net_ips s1 have "inet_tree_ips p1" ..
        with net_tree_ips p1  net_tree_ips p2 = {} have "inet_tree_ips p2" by auto
        with s2  init (pnet np p2) show ?thesis ..
      qed
      moreover from s1  init (pnet np p1)  i  net_ips s1 and wf_net_tree p1
        have "the (fst (netgmap sr s1) i)  (fst  sr) ` init (np i)"
          by (rule IH1)
      ultimately show ?thesis by simp
    next
      assume "i  net_ips s2"
      moreover with s2  init (pnet np p2) have "the (fst (netgmap sr s2) i)  (fst  sr) ` init (np i)"
        using wf_net_tree p2 by (rule IH2)
      moreover from s2  init (pnet np p2) and i  net_ips s2 have "inet_tree_ips p2" ..
      ultimately show ?thesis by simp
    qed
  qed

lemma init_lifted:
  assumes "wf_net_tree p"                                                          
  shows "{ (σ, snd (netgmap sr s)) |σ s. s  init (pnet np p)
                                (i. if inet_tree_ips p then σ i = the (fst (netgmap sr s) i)
                                      else σ i  (fst o sr) ` init (np i)) }  init (opnet onp p)"
  using assms proof (induction p)
    fix i R
    assume "wf_net_tree i; R"
    show "{(σ, snd (netgmap sr s)) |σ s. s  init (pnet np i; R)
             (j. if j  net_tree_ips i; R then σ j = the (fst (netgmap sr s) j)
                   else σ j  (fst  sr) ` init (np j))}  init (opnet onp i; R)"
      by (clarsimp simp add: node_comps onode_comps)
         (rule subsetD [OF init], auto)
  next
    fix p1 p2
    assume IH1: "wf_net_tree p1
                 {(σ, snd (netgmap sr s)) |σ s. s  init (pnet np p1)
                       (i. if i  net_tree_ips p1 then σ i = the (fst (netgmap sr s) i)
                             else σ i  (fst  sr) ` init (np i))}  init (opnet onp p1)"
                (is "_  ?S1  _")
       and IH2: "wf_net_tree p2
                  {(σ, snd (netgmap sr s)) |σ s. s  init (pnet np p2)
                        (i. if i  net_tree_ips p2 then σ i = the (fst (netgmap sr s) i)
                              else σ i  (fst  sr) ` init (np i))}  init (opnet onp p2)"
                (is "_  ?S2  _")
        and "wf_net_tree (p1  p2)"
    from this(3) have "wf_net_tree p1"
                  and "wf_net_tree p2"
                  and "net_tree_ips p1  net_tree_ips p2 = {}" by auto
    show "{(σ, snd (netgmap sr s)) |σ s. s  init (pnet np (p1  p2))
             (i. if i  net_tree_ips (p1  p2) then σ i = the (fst (netgmap sr s) i)
                   else σ i  (fst  sr) ` init (np i))}  init (opnet onp (p1  p2))"
    proof (rule, clarsimp simp only: split_paired_all pnet.simps automaton.simps)
      fix σ s1 s2
      assume σ_desc: "i. if i  net_tree_ips (p1  p2)
                          then σ i = the (fst (netgmap sr (SubnetS s1 s2)) i)
                          else σ i  (fst  sr) ` init (np i)"
         and "s1  init (pnet np p1)"
         and "s2  init (pnet np p2)"
      from this(2-3) have "net_ips s1 = net_tree_ips p1"
                      and "net_ips s2 = net_tree_ips p2" by auto
      have "(σ, snd (netgmap sr s1))  ?S1"
      proof -
        { fix i
          assume "i  net_tree_ips p1"
          with net_tree_ips p1  net_tree_ips p2 = {} have "i  net_tree_ips p2" by auto
          with s2  init (pnet np p2) have "i  net_ips s2" ..
          hence "the ((fst (netgmap sr s1) ++ fst (netgmap sr s2)) i) = the (fst (netgmap sr s1) i)"
            by simp
        }
        moreover
        { fix i
          assume "i  net_tree_ips p1"
          have "σ i  (fst  sr) ` init (np i)"
          proof (cases "i  net_tree_ips p2")
            assume "i  net_tree_ips p2"
            with i  net_tree_ips p1 and σ_desc show ?thesis
              by (auto dest: spec [of _ i])
          next
            assume "i  net_tree_ips p2"
            with s2  init (pnet np p2) have "i  net_ips s2" ..
            with s2  init (pnet np p2) have "the (fst (netgmap sr s2) i)  (fst  sr) ` init (np i)"
              using wf_net_tree p2 by (rule init_pnet_fst_sr_netgmap)
            with inet_tree_ips p2 and inet_ips s2 show ?thesis
              using σ_desc by simp
          qed
        }
        ultimately show ?thesis
          using s1  init (pnet np p1) and σ_desc by auto
      qed
      hence "(σ, snd (netgmap sr s1))  init (opnet onp p1)"
        by (rule subsetD [OF IH1 [OF wf_net_tree p1]])

      have "(σ, snd (netgmap sr s2))  ?S2"
      proof -
        { fix i
          assume "i  net_tree_ips p2"
          with s2  init (pnet np p2) have "i  net_ips s2" ..
          hence "the ((fst (netgmap sr s1) ++ fst (netgmap sr s2)) i) = the (fst (netgmap sr s2) i)"
            by simp
        }
        moreover
        { fix i
          assume "i  net_tree_ips p2"
          have "σ i  (fst  sr) ` init (np i)"
          proof (cases "i  net_tree_ips p1")
            assume "i  net_tree_ips p1"
            with i  net_tree_ips p2 and σ_desc show ?thesis
              by (auto dest: spec [of _ i])
          next
            assume "i  net_tree_ips p1"
            with s1  init (pnet np p1) have "i  net_ips s1" ..
            with s1  init (pnet np p1) have "the (fst (netgmap sr s1) i)  (fst  sr) ` init (np i)"
              using wf_net_tree p1 by (rule init_pnet_fst_sr_netgmap)
            moreover from s2  init (pnet np p2) and i  net_tree_ips p2 have "inet_ips s2" ..
            ultimately show ?thesis
              using inet_tree_ips p1 inet_ips s1 and inet_tree_ips p2 σ_desc by simp
          qed
        }
        ultimately show ?thesis
          using s2  init (pnet np p2) and σ_desc by auto
      qed
      hence "(σ, snd (netgmap sr s2))  init (opnet onp p2)"
        by (rule subsetD [OF IH2 [OF wf_net_tree p2]])

      with (σ, snd (netgmap sr s1))  init (opnet onp p1)
        show "(σ, snd (netgmap sr (SubnetS s1 s2)))  init (opnet onp (p1  p2))"
        using net_tree_ips p1  net_tree_ips p2 = {}
              net_ips s1 = net_tree_ips p1
              net_ips s2 = net_tree_ips p2 by simp
    qed
  qed

lemma init_pnet_opnet [elim]:
  assumes "wf_net_tree p"
      and "s  init (pnet np p)"
    shows "netgmap sr s  netmask (net_tree_ips p) ` init (opnet onp p)"
  proof -
    from wf_net_tree p
      have "{ (σ, snd (netgmap sr s)) |σ s. s  init (pnet np p)
                               (i. if inet_tree_ips p then σ i = the (fst (netgmap sr s) i)
                                     else σ i  (fst o sr) ` init (np i)) }  init (opnet onp p)"
        (is "?S  _")
      by (rule init_lifted)
    hence "netmask (net_tree_ips p) ` ?S  netmask (net_tree_ips p) ` init (opnet onp p)"
      by (rule image_mono)
    moreover have "netgmap sr s  netmask (net_tree_ips p) ` ?S"
    proof -
      { fix i
        from init_notempty have "s. s  (fst  sr) ` init (np i)" by auto
        hence "(SOME x. x  (fst  sr) ` init (np i))  (fst  sr) ` init (np i)" ..
      }
      with s  init (pnet np p) and init_notempty
        have "(λi. if i  net_tree_ips p
                   then the (fst (netgmap sr s) i)
                   else SOME x. x  (fst  sr) ` init (np i), snd (netgmap sr s))  ?S"
          (is "?s  ?S") by auto
      moreover have "netgmap sr s = netmask (net_tree_ips p) ?s"
      proof (intro prod_eqI ext)
        fix i
        show "fst (netgmap sr s) i = fst (netmask (net_tree_ips p) ?s) i"
        proof (cases "i  net_tree_ips p")
          assume "i  net_tree_ips p"
          with sinit (pnet np p) have "inet_ips s" ..
          hence "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
            by (rule some_the_fst_netgmap)
          with inet_tree_ips p show ?thesis
            by simp
        next
          assume "i  net_tree_ips p"
          moreover with sinit (pnet np p) have "inet_ips s" ..
          ultimately show ?thesis
            by simp
        qed
      qed simp
      ultimately show ?thesis
        by (rule rev_image_eqI)
    qed
    ultimately show ?thesis
      by (rule rev_subsetD [rotated])
  qed

lemma transfer_connect:
  assumes "(s, connect(i, i'), s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), connect(i, i'), (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms have "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))  trans (opnet onp n)
                      netgmap sr s' = netmask (net_tree_ips n) (σ, snd (netgmap sr s'))"
      proof (induction n arbitrary: s s' ζ)
        fix ii Ri ns ns' ζ
        assume "(ns, connect(i, i'), ns')  trans (pnet np ii; Ri)"
           and "netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)"
        from this(1) have "(ns, connect(i, i'), ns')  node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover then obtain ni s s' R R' where "ns  = NodeS ni s R"
                                            and "ns' = NodeS ni s' R'" ..
        ultimately have "(NodeS ni s R, connect(i, i'), NodeS ni s' R')  node_sos (trans (np ii))"
          by simp
        moreover then have "s' = s" by auto
        ultimately have "((σ, NodeS ni (snd (sr s)) R), connect(i, i'), (σ, NodeS ni (snd (sr s)) R'))
                                                                       onode_sos (trans (onp ii))"
          by - (rule node_connectTE', auto intro!: onode_sos.intros [simplified])
        with ns = NodeS ni s R ns' = NodeS ni s' R' s' = s
             and netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)
          show "((σ, snd (netgmap sr ns)), connect(i, i'), (σ, snd (netgmap sr ns')))  trans (opnet onp ii; Ri)
                 netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ, snd (netgmap sr ns'))"
            by (simp add: onode_comps)
      next
        fix n1 n2 s s' ζ
        assume IH1: "s s' ζ. (s, connect(i, i'), s')  trans (pnet np n1)
                       s  reachable (pnet np n1) TT
                       netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                       wf_net_tree n1
                       ((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))  trans (opnet onp n1)
                           netgmap sr s' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s'))"
           and IH2: "s s' ζ. (s, connect(i, i'), s')  trans (pnet np n2)
                       s  reachable (pnet np n2) TT
                       netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                       wf_net_tree n2
                       ((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))  trans (opnet onp n2)
                           netgmap sr s' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s'))"
           and tr: "(s, connect(i, i'), s')  trans (pnet np (n1  n2))"
           and sr: "s  reachable (pnet np (n1  n2)) TT"
           and nm: "netgmap sr s = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
           and "wf_net_tree (n1  n2)"
        from this(3) have "(s, connect(i, i'), s')  pnet_sos (trans (pnet np n1))
                                                               (trans (pnet np n2))"
          by simp
        then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                    and "s' = SubnetS s1' s2'"
                                    and "(s1, connect(i, i'), s1')  trans (pnet np n1)"
                                    and "(s2, connect(i, i'), s2')  trans (pnet np n2)"
          by (rule partial_connectTE) auto
        from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
          by simp

        from wf_net_tree (n1  n2) have "wf_net_tree n1" and "wf_net_tree n2"
                                      and "net_tree_ips n1  net_tree_ips n2 = {}" by auto

        from sr s = SubnetS s1 s2 have "s1  reachable (pnet np n1) TT" by (metis subnet_reachable(1))
        hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

        from sr s = SubnetS s1 s2 have "s2  reachable (pnet np n2) TT" by (metis subnet_reachable(2))
        hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

        from nm s = SubnetS s1 s2
          have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)" by simp
        hence "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          using net_tree_ips n1  net_tree_ips n2 = {} net_ips s1 = net_tree_ips n1
                and net_ips s2 = net_tree_ips n2 by (rule netgmap_subnet_split1)
        with (s1, connect(i, i'), s1')  trans (pnet np n1)
         and s1  reachable (pnet np n1) TT
         have "((σ, snd (netgmap sr s1)), connect(i, i'), (σ, snd (netgmap sr s1')))  trans (opnet onp n1)"
          and "netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))"
           using wf_net_tree n1 unfolding atomize_conj by (rule IH1)

        from netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)
             net_ips s1 = net_tree_ips n1 and net_ips s2 = net_tree_ips n2
          have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
            by (rule netgmap_subnet_split2)
        with (s2, connect(i, i'), s2')  trans (pnet np n2)
         and s2  reachable (pnet np n2) TT
         have "((σ, snd (netgmap sr s2)), connect(i, i'), (σ, snd (netgmap sr s2')))  trans (opnet onp n2)"
          and "netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))"
           using wf_net_tree n2 unfolding atomize_conj by (rule IH2)

        have "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))
                                          trans (opnet onp (n1  n2))"
        proof -
          from ((σ, snd (netgmap sr s1)), connect(i, i'), (σ, snd (netgmap sr s1')))  trans (opnet onp n1)
           and ((σ, snd (netgmap sr s2)), connect(i, i'), (σ, snd (netgmap sr s2')))  trans (opnet onp n2)
            have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), connect(i, i'),
                   (σ, SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                                            opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
              by (rule opnet_connect)
          with s = SubnetS s1 s2 s' = SubnetS s1' s2' show ?thesis by simp
        qed

        moreover from netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))
                      netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))
                      s' = SubnetS s1' s2'
          have "netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ, snd (netgmap sr s'))" ..

        ultimately show "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))
                                                                 trans (opnet onp (n1  n2))
                          netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ, snd (netgmap sr s'))" ..
      qed
    moreover from netgmap sr s = netmask (net_tree_ips n) (σ, ζ) have "ζ = snd (netgmap sr s)" by simp
    ultimately show " σ' ζ'. ((σ, ζ), connect(i, i'), (σ', ζ'))  trans (opnet onp n)
                               (j. j  net_ips ζ  σ' j = σ j)
                               netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_disconnect:
  assumes "(s, disconnect(i, i'), s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), disconnect(i, i'), (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms have "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))  trans (opnet onp n)
                      netgmap sr s' = netmask (net_tree_ips n) (σ, snd (netgmap sr s'))"
      proof (induction n arbitrary: s s' ζ)
        fix ii Ri ns ns' ζ
        assume "(ns, disconnect(i, i'), ns')  trans (pnet np ii; Ri)"
           and "netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)"
        from this(1) have "(ns, disconnect(i, i'), ns')  node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover then obtain ni s s' R R' where "ns  = NodeS ni s R"
                                            and "ns' = NodeS ni s' R'" ..
        ultimately have "(NodeS ni s R, disconnect(i, i'), NodeS ni s' R')  node_sos (trans (np ii))"
          by simp
        moreover then have "s' = s" by auto
        ultimately have "((σ, NodeS ni (snd (sr s)) R), disconnect(i, i'), (σ, NodeS ni (snd (sr s)) R'))
                                                                       onode_sos (trans (onp ii))"
          by - (rule node_disconnectTE', auto intro!: onode_sos.intros [simplified])
        with ns = NodeS ni s R ns' = NodeS ni s' R' s' = s
             and netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)
          show "((σ, snd (netgmap sr ns)), disconnect(i, i'), (σ, snd (netgmap sr ns')))  trans (opnet onp ii; Ri)
                 netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ, snd (netgmap sr ns'))"
            by (simp add: onode_comps)
      next
        fix n1 n2 s s' ζ
        assume IH1: "s s' ζ. (s, disconnect(i, i'), s')  trans (pnet np n1)
                       s  reachable (pnet np n1) TT
                       netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                       wf_net_tree n1
                       ((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))  trans (opnet onp n1)
                           netgmap sr s' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s'))"
           and IH2: "s s' ζ. (s, disconnect(i, i'), s')  trans (pnet np n2)
                       s  reachable (pnet np n2) TT
                       netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                       wf_net_tree n2
                       ((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))  trans (opnet onp n2)
                           netgmap sr s' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s'))"
           and tr: "(s, disconnect(i, i'), s')  trans (pnet np (n1  n2))"
           and sr: "s  reachable (pnet np (n1  n2)) TT"
           and nm: "netgmap sr s = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
           and "wf_net_tree (n1  n2)"
        from this(3) have "(s, disconnect(i, i'), s')  pnet_sos (trans (pnet np n1))
                                                               (trans (pnet np n2))"
          by simp
        then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                    and "s' = SubnetS s1' s2'"
                                    and "(s1, disconnect(i, i'), s1')  trans (pnet np n1)"
                                    and "(s2, disconnect(i, i'), s2')  trans (pnet np n2)"
          by (rule partial_disconnectTE) auto
        from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
          by simp

        from wf_net_tree (n1  n2) have "wf_net_tree n1" and "wf_net_tree n2"
                                      and "net_tree_ips n1  net_tree_ips n2 = {}" by auto

        from sr s = SubnetS s1 s2 have "s1  reachable (pnet np n1) TT" by (metis subnet_reachable(1))
        hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

        from sr s = SubnetS s1 s2 have "s2  reachable (pnet np n2) TT" by (metis subnet_reachable(2))
        hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

        from nm s = SubnetS s1 s2
          have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)" by simp
        hence "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          using net_tree_ips n1  net_tree_ips n2 = {} net_ips s1 = net_tree_ips n1
                and net_ips s2 = net_tree_ips n2 by (rule netgmap_subnet_split1)
        with (s1, disconnect(i, i'), s1')  trans (pnet np n1)
         and s1  reachable (pnet np n1) TT
         have "((σ, snd (netgmap sr s1)), disconnect(i, i'), (σ, snd (netgmap sr s1')))  trans (opnet onp n1)"
          and "netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))"
           using wf_net_tree n1 unfolding atomize_conj by (rule IH1)

        from netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)
             net_ips s1 = net_tree_ips n1 and net_ips s2 = net_tree_ips n2
          have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
            by (rule netgmap_subnet_split2)
        with (s2, disconnect(i, i'), s2')  trans (pnet np n2)
         and s2  reachable (pnet np n2) TT
         have "((σ, snd (netgmap sr s2)), disconnect(i, i'), (σ, snd (netgmap sr s2')))  trans (opnet onp n2)"
          and "netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))"
           using wf_net_tree n2 unfolding atomize_conj by (rule IH2)

        have "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))
                                          trans (opnet onp (n1  n2))"
        proof -
          from ((σ, snd (netgmap sr s1)), disconnect(i, i'), (σ, snd (netgmap sr s1')))  trans (opnet onp n1)
           and ((σ, snd (netgmap sr s2)), disconnect(i, i'), (σ, snd (netgmap sr s2')))  trans (opnet onp n2)
            have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), disconnect(i, i'),
                   (σ, SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                                            opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
              by (rule opnet_disconnect)
          with s = SubnetS s1 s2 s' = SubnetS s1' s2' show ?thesis by simp
        qed

        moreover from netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))
                      netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))
                      s' = SubnetS s1' s2'
          have "netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ, snd (netgmap sr s'))" ..

        ultimately show "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))
                                                                 trans (opnet onp (n1  n2))
                          netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ, snd (netgmap sr s'))" ..
      qed
    moreover from netgmap sr s = netmask (net_tree_ips n) (σ, ζ) have "ζ = snd (netgmap sr s)" by simp
    ultimately show "σ' ζ'. ((σ, ζ), disconnect(i, i'), (σ', ζ'))  trans (opnet onp n)
                               (j. j  net_ips ζ  σ' j = σ j)
                               netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_tau:
  assumes "(s, τ, s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), τ, (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms(4,2,1) obtain i where "inet_ips s"
                                 and "j. ji  netmap s' j = netmap s j"
                                 and "net_ip_action np τ i n s s'"
      by (metis pnet_tau_single_node)
    from this(2) have "j. ji  fst (netgmap sr s') j = fst (netgmap sr s) j"
      by (clarsimp intro!: netmap_is_fst_netgmap')
    from (s, τ, s')  trans (pnet np n) have "net_ips s' = net_ips s"
      by (rule pnet_maintains_dom [THEN sym])
    define σ' where "σ' j = (if j = i then the (fst (netgmap sr s') i) else σ j)" for j
    from j. ji  fst (netgmap sr s') j = fst (netgmap sr s) j
         and netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "j. ji  σ' j = σ j"
        unfolding σ'_def by clarsimp

    from assms(2) have "net_ips s = net_tree_ips n"
      by (rule pnet_net_ips_net_tree_ips)

    from netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "ζ = snd (netgmap sr s)" by simp

    from j. ji  fst (netgmap sr s') j = fst (netgmap sr s) j i  net_ips s
         net_ips s = net_tree_ips n net_ips s' = net_ips s
         netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
        unfolding σ'_def [abs_def] by - (rule ext, clarsimp)

    hence "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      by (rule prod_eqI, simp)

    with assms(1, 3)
      have "((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s')))  trans (opnet onp n)"
        using assms(2,4) inet_ips s and net_ip_action np τ i n s s'
    proof (induction n arbitrary: s s' ζ)
      fix ii Ri ns ns' ζ
      assume "(ns, τ, ns')  trans (pnet np ii; Ri)"
         and nsr: "ns  reachable (pnet np ii; Ri) TT"
         and "netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)"
         and "netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))"
         and "inet_ips ns"
      from this(1) have "(ns, τ, ns')  node_sos (trans (np ii))"
        by (simp add: node_comps)
      moreover with nsr obtain s s' R R' where "ns  = NodeS ii s R"
                                           and "ns' = NodeS ii s' R'"
         by (metis net_node_reachable_is_node node_tauTE')
      moreover from i  net_ips ns and ns  = NodeS ii s R have "ii = i" by simp
      ultimately have ntr: "(NodeS i s R, τ, NodeS i s' R')  node_sos (trans (np i))"
        by simp
      hence "R' = R" by (metis net_state.inject(1) node_tauTE')

      from ntr obtain a where "(s, a, s')  trans (np i)"
                          and "(d. a = ¬unicast d  dR)  (a = τ)"
        by (rule node_tauTE') auto

      from netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ) ns  = NodeS ii s R and ii = i
        have "σ i = fst (sr s)" by simp (metis map_upd_Some_unfold)

      moreover from netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))
                    ns' = NodeS ii s' R' and ii = i
        have "σ' i = fst (sr s')"
          unfolding σ'_def [abs_def] by clarsimp (hypsubst_thin,
                                        metis (full_types, lifting) fun_upd_same option.sel)
      ultimately have "((σ, snd (sr s)), a, (σ', snd (sr s')))  trans (onp i)"
        using (s, a, s')  trans (np i) by (rule trans)

      from (d. a = ¬unicast d  dR)  (a = τ) j. ji  σ' j = σ j R'=R
           and ((σ, snd (sr s)), a, (σ', snd (sr s')))  trans (onp i)
        have "((σ, NodeS i (snd (sr s)) R), τ, (σ', NodeS i (snd (sr s')) R'))  onode_sos (trans (onp i))"
          by (metis onode_sos.onode_notucast onode_sos.onode_tau)

      with ns  = NodeS ii s R ns' = NodeS ii s' R' ii = i
        show "((σ, snd (netgmap sr ns)), τ, (σ', snd (netgmap sr ns')))  trans (opnet onp ii; Ri)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ
      assume IH1: "s s' ζ. (s, τ, s')  trans (pnet np n1)
                     netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                     netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                     s  reachable (pnet np n1) TT
                     wf_net_tree n1
                     inet_ips s
                     net_ip_action np τ i n1 s s'
                     ((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s')))  trans (opnet onp n1)"
         and IH2: "s s' ζ. (s, τ, s')  trans (pnet np n2)
                     netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                     netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                     s  reachable (pnet np n2) TT
                     wf_net_tree n2
                     inet_ips s
                     net_ip_action np τ i n2 s s'
                     ((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s')))  trans (opnet onp n2)"
         and tr: "(s, τ, s')  trans (pnet np (n1  n2))"
         and sr: "s  reachable (pnet np (n1  n2)) TT"
         and nm: "netgmap sr s = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
         and nm': "netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ', snd (netgmap sr s'))"
         and "wf_net_tree (n1  n2)"
         and "inet_ips s"
         and "net_ip_action np τ i (n1  n2) s s'"
      from tr have "(s, τ, s')  pnet_sos (trans (pnet np n1)) (trans (pnet np n2))" by simp
      then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                  and "s' = SubnetS s1' s2'"
        by (rule partial_tauTE) auto
      from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
        by simp
      from s' = SubnetS s1' s2' and nm'
        have "netgmap sr (SubnetS s1' s2') = netmask (net_tree_ips (n1  n2)) (σ', snd (netgmap sr s'))"
          by simp

      from wf_net_tree (n1  n2) have "wf_net_tree n1"
                                    and "wf_net_tree n2"
                                    and "net_tree_ips n1  net_tree_ips n2 = {}" by auto

      from sr [simplified s = SubnetS s1 s2] have "s1  reachable (pnet np n1) TT"
        by (rule subnet_reachable(1))
      hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

      from sr [simplified s = SubnetS s1 s2] have "s2  reachable (pnet np n2) TT"
        by (rule subnet_reachable(2))
      hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

      from nm [simplified s = SubnetS s1 s2]
           net_tree_ips n1  net_tree_ips n2 = {}
           net_ips s1 = net_tree_ips n1
           net_ips s2 = net_tree_ips n2 
        have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          by (rule netgmap_subnet_split1)

      from nm [simplified s = SubnetS s1 s2]
           net_ips s1 = net_tree_ips n1
           net_ips s2 = net_tree_ips n2 
        have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
          by (rule netgmap_subnet_split2)

      from inet_ips s and s = SubnetS s1 s2 have "inet_ips s1  inet_ips s2" by auto
        thus "((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s')))  trans (opnet onp (n1  n2))"
      proof
        assume "inet_ips s1"
        with s = SubnetS s1 s2 s' = SubnetS s1' s2' net_ip_action np τ i (n1  n2) s s'
          have "(s1, τ, s1')  trans (pnet np n1)"
           and "net_ip_action np τ i n1 s1 s1'"
           and "s2' = s2" by simp_all

        from net_ips s1 = net_tree_ips n1 and (s1, τ, s1')  trans (pnet np n1)
          have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

        from nm' [simplified s' = SubnetS s1' s2' s2' = s2]
                        net_tree_ips n1  net_tree_ips n2 = {}
                        net_ips s1' = net_tree_ips n1
                        net_ips s2 = net_tree_ips n2
          have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
            by (rule netgmap_subnet_split1)

        from (s1, τ, s1')  trans (pnet np n1)
             netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))
             netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))
             s1  reachable (pnet np n1) TT
             wf_net_tree n1
             inet_ips s1
             net_ip_action np τ i n1 s1 s1'
          have "((σ, snd (netgmap sr s1)), τ, (σ', snd (netgmap sr s1')))  trans (opnet onp n1)"
             by (rule IH1)

        with s = SubnetS s1 s2 s' = SubnetS s1' s2' s2' = s2 show ?thesis
          by (simp del: step_node_tau) (erule opnet_tau1)
      next
        assume "inet_ips s2"
        with s = SubnetS s1 s2 s' = SubnetS s1' s2' net_ip_action np τ i (n1  n2) s s'
          have "(s2, τ, s2')  trans (pnet np n2)"
           and "net_ip_action np τ i n2 s2 s2'"
           and "s1' = s1" by simp_all

        from net_ips s2 = net_tree_ips n2 and (s2, τ, s2')  trans (pnet np n2)
          have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

        from nm' [simplified s' = SubnetS s1' s2' s1' = s1]
                        net_ips s1 = net_tree_ips n1
                        net_ips s2' = net_tree_ips n2
          have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
            by (rule netgmap_subnet_split2)

        from (s2, τ, s2')  trans (pnet np n2)
             netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))
             netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))
             s2  reachable (pnet np n2) TT
             wf_net_tree n2
             inet_ips s2
             net_ip_action np τ i n2 s2 s2'
          have "((σ, snd (netgmap sr s2)), τ, (σ', snd (netgmap sr s2')))  trans (opnet onp n2)"
             by (rule IH2)

        with s = SubnetS s1 s2 s' = SubnetS s1' s2' s1' = s1 show ?thesis
          by (simp del: step_node_tau) (erule opnet_tau2)
      qed
    qed
    with ζ = snd (netgmap sr s) have "((σ, ζ), τ, (σ', snd (netgmap sr s')))  trans (opnet onp n)"
      by simp
    moreover from j. ji  σ' j = σ j i  net_ips s ζ = snd (netgmap sr s)
      have "j. jnet_ips ζ  σ' j = σ j" by (metis net_ips_netgmap)
    ultimately have "((σ, ζ), τ, (σ', snd (netgmap sr s')))  trans (opnet onp n)
                      (j. jnet_ips ζ  σ' j = σ j)
                      netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      using netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s')) by simp
    thus "σ' ζ'. ((σ, ζ), τ, (σ', ζ'))  trans (opnet onp n)
                   (j. jnet_ips ζ  σ' j = σ j)
                   netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_deliver:
  assumes "(s, i:deliver(d), s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), i:deliver(d), (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms(4,2,1) obtain "inet_ips s"
                         and "j. ji  netmap s' j = netmap s j"
                         and "net_ip_action np (i:deliver(d)) i n s s'"
      by (metis delivered_to_net_ips pnet_deliver_single_node)
    from this(2) have "j. ji  fst (netgmap sr s') j = fst (netgmap sr s) j"
      by (clarsimp intro!: netmap_is_fst_netgmap')
    from (s, i:deliver(d), s')  trans (pnet np n) have "net_ips s' = net_ips s"
      by (rule pnet_maintains_dom [THEN sym])
    define σ' where "σ' j = (if j = i then the (fst (netgmap sr s') i) else σ j)" for j
    from j. ji  fst (netgmap sr s') j = fst (netgmap sr s) j
         and netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "j. ji  σ' j = σ j"
        unfolding σ'_def by clarsimp

    from assms(2) have "net_ips s = net_tree_ips n"
      by (rule pnet_net_ips_net_tree_ips)

    from netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "ζ = snd (netgmap sr s)" by simp

    from j. ji  fst (netgmap sr s') j = fst (netgmap sr s) j i  net_ips s
         net_ips s = net_tree_ips n net_ips s' = net_ips s
         netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
        unfolding σ'_def [abs_def] by - (rule ext, clarsimp)

    hence "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      by (rule prod_eqI, simp)

    with assms(1, 3)
      have "((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s')))  trans (opnet onp n)"
        using assms(2,4) inet_ips s and net_ip_action np (i:deliver(d)) i n s s'
    proof (induction n arbitrary: s s' ζ)
      fix ii Ri ns ns' ζ
      assume "(ns, i:deliver(d), ns')  trans (pnet np ii; Ri)"
         and nsr: "ns  reachable (pnet np ii; Ri) TT"
         and "netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)"
         and "netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))"
         and "inet_ips ns"
      from this(1) have "(ns, i:deliver(d), ns')  node_sos (trans (np ii))"
        by (simp add: node_comps)
      moreover with nsr obtain s s' R R' where "ns  = NodeS ii s R"
                                           and "ns' = NodeS ii s' R'"
         by (metis net_node_reachable_is_node node_sos_dest)
      moreover from i  net_ips ns and ns  = NodeS ii s R have "ii = i" by simp
      ultimately have ntr: "(NodeS i s R, i:deliver(d), NodeS i s' R')  node_sos (trans (np i))"
        by simp
      hence "R' = R" by (metis net_state.inject(1) node_deliverTE')

      from ntr have "(s, deliver d, s')  trans (np i)"
        by (rule node_deliverTE') simp

      from netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ) ns  = NodeS ii s R and ii = i
        have "σ i = fst (sr s)" by simp (metis map_upd_Some_unfold)

      moreover from netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))
                    ns' = NodeS ii s' R' and ii = i
        have "σ' i = fst (sr s')"
          unfolding σ'_def [abs_def] by clarsimp (hypsubst_thin,
                                        metis (lifting, full_types) fun_upd_same option.sel)
      ultimately have "((σ, snd (sr s)), deliver d, (σ', snd (sr s')))  trans (onp i)"
        using (s, deliver d, s')  trans (np i) by (rule trans)

      with j. ji  σ' j = σ j R'=R
        have "((σ, NodeS i (snd (sr s)) R), i:deliver(d), (σ', NodeS i (snd (sr s')) R'))
                                                                       onode_sos (trans (onp i))"
          by (metis onode_sos.onode_deliver)

      with ns  = NodeS ii s R ns' = NodeS ii s' R' ii = i
        show "((σ, snd (netgmap sr ns)), i:deliver(d), (σ', snd (netgmap sr ns')))  trans (opnet onp ii; Ri)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ
      assume IH1: "s s' ζ. (s, i:deliver(d), s')  trans (pnet np n1)
                     netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                     netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                     s  reachable (pnet np n1) TT
                     wf_net_tree n1
                     inet_ips s
                     net_ip_action np (i:deliver(d)) i n1 s s'
                     ((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s')))  trans (opnet onp n1)"
         and IH2: "s s' ζ. (s, i:deliver(d), s')  trans (pnet np n2)
                     netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                     netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                     s  reachable (pnet np n2) TT
                     wf_net_tree n2
                     inet_ips s
                     net_ip_action np (i:deliver(d)) i n2 s s'
                     ((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s')))  trans (opnet onp n2)"
         and tr: "(s, i:deliver(d), s')  trans (pnet np (n1  n2))"
         and sr: "s  reachable (pnet np (n1  n2)) TT"
         and nm: "netgmap sr s = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
         and nm': "netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ', snd (netgmap sr s'))"
         and "wf_net_tree (n1  n2)"
         and "inet_ips s"
         and "net_ip_action np (i:deliver(d)) i (n1  n2) s s'"
      from tr have "(s, i:deliver(d), s')  pnet_sos (trans (pnet np n1)) (trans (pnet np n2))" by simp
      then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                  and "s' = SubnetS s1' s2'"
        by (rule partial_deliverTE) auto
      from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
        by simp
      from s' = SubnetS s1' s2' and nm'
        have "netgmap sr (SubnetS s1' s2') = netmask (net_tree_ips (n1  n2)) (σ', snd (netgmap sr s'))"
          by simp

      from wf_net_tree (n1  n2) have "wf_net_tree n1"
                                    and "wf_net_tree n2"
                                    and "net_tree_ips n1  net_tree_ips n2 = {}" by auto

      from sr [simplified s = SubnetS s1 s2] have "s1  reachable (pnet np n1) TT"
        by (rule subnet_reachable(1))
      hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

      from sr [simplified s = SubnetS s1 s2] have "s2  reachable (pnet np n2) TT"
        by (rule subnet_reachable(2))
      hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

      from nm [simplified s = SubnetS s1 s2]
           net_tree_ips n1  net_tree_ips n2 = {}
           net_ips s1 = net_tree_ips n1
           net_ips s2 = net_tree_ips n2 
        have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          by (rule netgmap_subnet_split1)

      from nm [simplified s = SubnetS s1 s2]
           net_ips s1 = net_tree_ips n1
           net_ips s2 = net_tree_ips n2 
        have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
          by (rule netgmap_subnet_split2)

      from inet_ips s and s = SubnetS s1 s2 have "inet_ips s1  inet_ips s2" by auto
        thus "((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s')))  trans (opnet onp (n1  n2))"
      proof
        assume "inet_ips s1"
        with s = SubnetS s1 s2 s' = SubnetS s1' s2' net_ip_action np (i:deliver(d)) i (n1  n2) s s'
          have "(s1, i:deliver(d), s1')  trans (pnet np n1)"
           and "net_ip_action np (i:deliver(d)) i n1 s1 s1'"
           and "s2' = s2" by simp_all

        from net_ips s1 = net_tree_ips n1 and (s1, i:deliver(d), s1')  trans (pnet np n1)
          have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

        from nm' [simplified s' = SubnetS s1' s2' s2' = s2]
                        net_tree_ips n1  net_tree_ips n2 = {}
                        net_ips s1' = net_tree_ips n1
                        net_ips s2 = net_tree_ips n2
          have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
            by (rule netgmap_subnet_split1)

        from (s1, i:deliver(d), s1')  trans (pnet np n1)
             netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))
             netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))
             s1  reachable (pnet np n1) TT
             wf_net_tree n1
             inet_ips s1
             net_ip_action np (i:deliver(d)) i n1 s1 s1'
          have "((σ, snd (netgmap sr s1)), i:deliver(d), (σ', snd (netgmap sr s1')))  trans (opnet onp n1)"
             by (rule IH1)

        with s = SubnetS s1 s2 s' = SubnetS s1' s2' s2' = s2 show ?thesis
          by simp (erule opnet_deliver1)
      next
        assume "inet_ips s2"
        with s = SubnetS s1 s2 s' = SubnetS s1' s2' net_ip_action np (i:deliver(d)) i (n1  n2) s s'
          have "(s2, i:deliver(d), s2')  trans (pnet np n2)"
           and "net_ip_action np (i:deliver(d)) i n2 s2 s2'"
           and "s1' = s1" by simp_all

        from net_ips s2 = net_tree_ips n2 and (s2, i:deliver(d), s2')  trans (pnet np n2)
          have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

        from nm' [simplified s' = SubnetS s1' s2' s1' = s1]
                        net_ips s1 = net_tree_ips n1
                        net_ips s2' = net_tree_ips n2
          have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
            by (rule netgmap_subnet_split2)

        from (s2, i:deliver(d), s2')  trans (pnet np n2)
             netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))
             netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))
             s2  reachable (pnet np n2) TT
             wf_net_tree n2
             inet_ips s2
             net_ip_action np (i:deliver(d)) i n2 s2 s2'
          have "((σ, snd (netgmap sr s2)), i:deliver(d), (σ', snd (netgmap sr s2')))  trans (opnet onp n2)"
             by (rule IH2)

        with s = SubnetS s1 s2 s' = SubnetS s1' s2' s1' = s1 show ?thesis
          by simp (erule opnet_deliver2)
      qed
    qed
    with ζ = snd (netgmap sr s) have "((σ, ζ), i:deliver(d), (σ', snd (netgmap sr s')))  trans (opnet onp n)"
      by simp
    moreover from j. ji  σ' j = σ j i  net_ips s ζ = snd (netgmap sr s)
      have "j. jnet_ips ζ  σ' j = σ j" by (metis net_ips_netgmap)
    ultimately have "((σ, ζ), i:deliver(d), (σ', snd (netgmap sr s')))  trans (opnet onp n)
                      (j. jnet_ips ζ  σ' j = σ j)
                      netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      using netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s')) by simp
    thus "σ' ζ'. ((σ, ζ), i:deliver(d), (σ', ζ'))  trans (opnet onp n)
                   (j. jnet_ips ζ  σ' j = σ j)
                   netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_arrive':
  assumes "(s, H¬K:arrive(m), s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s  = netmask (net_tree_ips n) (σ, ζ)"
      and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
      and "wf_net_tree n"
  shows "((σ, ζ), H¬K:arrive(m), (σ', ζ'))  trans (opnet onp n)"
  proof -

    from assms(2) have "net_ips s = net_tree_ips n" ..
    with assms(1) have "net_ips s' = net_tree_ips n"
      by (metis pnet_maintains_dom)

    from netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "ζ = snd (netgmap sr s)" by simp

    from netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')
      have "ζ' = snd (netgmap sr s')"
       and "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
         by simp_all

    from assms(1-3) netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s')) assms(5)
      have "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))  trans (opnet onp n)"
      proof (induction n arbitrary: s s' ζ H K)
        fix ii Ri ns ns' ζ H K
        assume "(ns, H¬K:arrive(m), ns')  trans (pnet np ii; Ri)"
           and nsr: "ns  reachable (pnet np ii; Ri) TT"
           and "netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)"
           and "netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))"
        from this(1) have "(ns, H¬K:arrive(m), ns')  node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover with nsr obtain s s' R where "ns  = NodeS ii s R"
                                          and "ns' = NodeS ii s' R"
          by (metis net_node_reachable_is_node node_arriveTE')
        ultimately have "(NodeS ii s R, H¬K:arrive(m), NodeS ii s' R)  node_sos (trans (np ii))"
          by simp
        from this(1) have "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
        proof (rule node_arriveTE)
          assume "(s, receive m, s')  trans (np ii)"
             and "H = {ii}"
             and "K = {}"
          from netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ) and ns  = NodeS ii s R
            have "σ ii = fst (sr s)"
              by simp (metis map_upd_Some_unfold)
          moreover from netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))
                        and ns' = NodeS ii s' R
            have "σ' ii = fst (sr s')" by simp (metis map_upd_Some_unfold)
          ultimately have "((σ, snd (sr s)), receive m, (σ', snd (sr s')))  trans (onp ii)"
            using (s, receive m, s')  trans (np ii) by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), {ii}¬{}:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
            by (rule onode_receive)
          with H={ii} and K={}
            show "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
              by simp
        next
          assume "H = {}"
             and "s' = s"
             and "K = {ii}"
          from s' = s netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))
                        netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)
                        ns = NodeS ii s R and ns' = NodeS ii s' R
            have "σ' ii = σ ii" by simp (metis option.sel)
          hence "((σ, NodeS ii (snd (sr s)) R), {}¬{ii}:arrive(m), (σ', NodeS ii (snd (sr s)) R))
                                                                       onode_sos (trans (onp ii))"
            by (rule onode_arrive)
          with H={} K={ii} and s' = s
          show "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      onode_sos (trans (onp ii))"
            by simp
        qed
      with ns = NodeS ii s R ns' = NodeS ii s' R
        show "((σ, snd (netgmap sr ns)), H¬K:arrive(m), (σ', snd (netgmap sr ns')))
                                                              trans (opnet onp ii; Ri)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ H K
      assume IH1: "s s' ζ H K. (s, H¬K:arrive(m), s')  trans (pnet np n1)
                          s  reachable (pnet np n1) TT
                          netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                          netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                          wf_net_tree n1
                          ((σ, snd (netgmap sr s)), H¬K:arrive(m), σ', snd (netgmap sr s'))
                                                                         trans (opnet onp n1)"
        and IH2: "s s' ζ H K. (s, H¬K:arrive(m), s')  trans (pnet np n2)
                          s  reachable (pnet np n2) TT
                          netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                          netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                          wf_net_tree n2
                          ((σ, snd (netgmap sr s)), H¬K:arrive(m), σ', snd (netgmap sr s'))
                                                                         trans (opnet onp n2)"
        and "(s, H¬K:arrive(m), s')  trans (pnet np (n1  n2))"
        and sr: "s  reachable (pnet np (n1  n2)) TT"
        and nm: "netgmap sr s = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
        and nm': "netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ', snd (netgmap sr s'))"
        and "wf_net_tree (n1  n2)"
      from this(3) have "(s, H¬K:arrive(m), s')  pnet_sos (trans (pnet np n1))
                                                              (trans (pnet np n2))"
        by simp
      thus "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))
                                                                    trans (opnet onp (n1  n2))"
      proof (rule partial_arriveTE)
        fix s1 s1' s2 s2' H1 H2 K1 K2
        assume "s = SubnetS s1 s2"
           and "s' = SubnetS s1' s2'"
           and tr1: "(s1, H1¬K1:arrive(m), s1')  trans (pnet np n1)"
           and tr2: "(s2, H2¬K2:arrive(m), s2')  trans (pnet np n2)"
           and "H = H1  H2"
           and "K = K1  K2"

        from wf_net_tree (n1  n2) have "wf_net_tree n1"
                                      and "wf_net_tree n2"
                                      and "net_tree_ips n1  net_tree_ips n2 = {}" by auto

        from sr [simplified s = SubnetS s1 s2] have "s1  reachable (pnet np n1) TT"
          by (rule subnet_reachable(1))
        hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
        with tr1 have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

        from sr [simplified s = SubnetS s1 s2] have "s2  reachable (pnet np n2) TT"
          by (rule subnet_reachable(2))
        hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
        with tr2 have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

        from (s1, H1¬K1:arrive(m), s1')  trans (pnet np n1)
             s1  reachable (pnet np n1) TT
          have "((σ, snd (netgmap sr s1)), H1¬K1:arrive(m), (σ', snd (netgmap sr s1')))
                                                                             trans (opnet onp n1)"
          proof (rule IH1 [OF _ _ _ _ wf_net_tree n1])
            from nm [simplified s = SubnetS s1 s2]
                 net_tree_ips n1  net_tree_ips n2 = {}
                 net_ips s1 = net_tree_ips n1
                 net_ips s2 = net_tree_ips n2 
              show "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
                by (rule netgmap_subnet_split1)
          next
            from nm' [simplified s' = SubnetS s1' s2']
                 net_tree_ips n1  net_tree_ips n2 = {}
                 net_ips s1' = net_tree_ips n1
                 net_ips s2' = net_tree_ips n2 
              show "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
                by (rule netgmap_subnet_split1)
          qed

        moreover from (s2, H2¬K2:arrive(m), s2')  trans (pnet np n2)
                      s2  reachable (pnet np n2) TT
          have "((σ, snd (netgmap sr s2)), H2¬K2:arrive(m), (σ', snd (netgmap sr s2')))
                                                                             trans (opnet onp n2)"
          proof (rule IH2 [OF _ _ _ _ wf_net_tree n2])
            from nm [simplified s = SubnetS s1 s2]
                 net_ips s1 = net_tree_ips n1
                 net_ips s2 = net_tree_ips n2 
              show "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
                by (rule netgmap_subnet_split2)
          next
            from nm' [simplified s' = SubnetS s1' s2']
                 net_ips s1' = net_tree_ips n1
                 net_ips s2' = net_tree_ips n2 
              show "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
                by (rule netgmap_subnet_split2)
          qed
        ultimately show "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))
                                                                      trans (opnet onp (n1  n2))"
          using s = SubnetS s1 s2 s' = SubnetS s1' s2' H = H1  H2 K = K1  K2
            by simp (rule opnet_sos.opnet_arrive)
      qed
    qed
    with ζ = snd (netgmap sr s) and ζ' = snd (netgmap sr s')
      show "((σ, ζ), H¬K:arrive(m), (σ', ζ'))  trans (opnet onp n)"
        by simp
  qed

lemma transfer_arrive:
  assumes "(s, H¬K:arrive(m), s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s  = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), H¬K:arrive(m), (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    define σ' where "σ' i = (if inet_tree_ips n then the (fst (netgmap sr s') i) else σ i)" for i

    from assms(2) have "net_ips s = net_tree_ips n"
      by (rule pnet_net_ips_net_tree_ips)
    with assms(1) have "net_ips s' = net_tree_ips n"
      by (metis pnet_maintains_dom)

    have "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
    proof (rule prod_eqI)
      from net_ips s' = net_tree_ips n
        show "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
          unfolding σ'_def [abs_def] by - (rule ext, clarsimp)
    qed simp

    moreover with assms(1-3)
    have "((σ, ζ), H¬K:arrive(m), (σ', snd (netgmap sr s')))  trans (opnet onp n)"
      using wf_net_tree n by (rule transfer_arrive')

    moreover have "j. jnet_ips ζ  σ' j = σ j"
    proof -
      have "j. jnet_tree_ips n  σ' j = σ j" unfolding σ'_def by simp
      with assms(3) and net_ips s = net_tree_ips n
        show ?thesis
          by clarsimp (metis (mono_tags) net_ips_netgmap snd_conv)
    qed

    ultimately show "σ' ζ'. ((σ, ζ), H¬K:arrive(m), (σ', ζ'))  trans (opnet onp n)
                           (j. jnet_ips ζ  σ' j = σ j)
                           netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_cast:
  assumes "(s, mR:*cast(m), s')  trans (pnet np n)"
      and "s  reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), mR:*cast(m), (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    define σ' where "σ' i = (if inet_tree_ips n then the (fst (netgmap sr s') i) else σ i)" for i

    from assms(2) have "net_ips s = net_tree_ips n" ..
    with assms(1) have "net_ips s' = net_tree_ips n"
      by (metis pnet_maintains_dom)
    have "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
    proof (rule prod_eqI)
      from net_ips s' = net_tree_ips n
        show "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
      unfolding σ'_def [abs_def] by - (rule ext, clarsimp simp add: some_the_fst_netgmap)
    qed simp

    from net_ips s' = net_tree_ips n and net_ips s = net_tree_ips n 
      have "j. jnet_ips (snd (netgmap sr s))  σ' j = σ j"
        unfolding σ'_def by simp

    from netgmap sr s = netmask (net_tree_ips n) (σ, ζ)
      have "ζ = snd (netgmap sr s)" by simp

    from assms(1-3) netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s')) assms(4)
      have "((σ, snd (netgmap sr s)), mR:*cast(m), (σ', snd (netgmap sr s')))  trans (opnet onp n)"
      proof (induction n arbitrary: s s' ζ mR)
        fix ii Ri ns ns' ζ mR
        assume "(ns, mR:*cast(m), ns')  trans (pnet np ii; Ri)"
           and nsr: "ns  reachable (pnet np ii; Ri) TT"
           and "netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ)"
           and "netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))"
        from this(1) have "(ns, mR:*cast(m), ns')  node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover with nsr obtain s s' R where "ns  = NodeS ii s R"
                                          and "ns' = NodeS ii s' R"
          by (metis net_node_reachable_is_node node_castTE')
        ultimately have "(NodeS ii s R, mR:*cast(m), NodeS ii s' R)  node_sos (trans (np ii))"
          by simp

        from netgmap sr ns = netmask (net_tree_ips ii; Ri) (σ, ζ) and ns  = NodeS ii s R
          have "σ ii = fst (sr s)"
            by simp (metis map_upd_Some_unfold)
        from netgmap sr ns' = netmask (net_tree_ips ii; Ri) (σ', snd (netgmap sr ns'))
             and ns' = NodeS ii s' R
          have "σ' ii = fst (sr s')" by simp (metis map_upd_Some_unfold)

        from (NodeS ii s R, mR:*cast(m), NodeS ii s' R)  node_sos (trans (np ii))
          have "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
        proof (rule node_castTE)
          assume "(s, broadcast m, s')  trans (np ii)"
             and "mR = R"
          from σ ii = fst (sr s) σ' ii = fst (sr s') and this(1)
            have "((σ, snd (sr s)), broadcast m, (σ', snd (sr s')))  trans (onp ii)"
              by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), R:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
            by (rule onode_bcast)
          with mR = R show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
              by simp
        next
          fix D
          assume "(s, groupcast D m, s')  trans (np ii)"
             and "mR = R  D"
          from σ ii = fst (sr s) σ' ii = fst (sr s') and this(1)
            have "((σ, snd (sr s)), groupcast D m, (σ', snd (sr s')))  trans (onp ii)"
              by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), (R  D):*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
            by (rule onode_gcast)
          with mR = R  D show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
              by simp
        next
          fix d
          assume "(s, unicast d m, s')  trans (np ii)"
             and "d  R"
             and "mR = {d}"
          from σ ii = fst (sr s) σ' ii = fst (sr s') and this(1)
            have "((σ, snd (sr s)), unicast d m, (σ', snd (sr s')))  trans (onp ii)"
              by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), {d}:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
            using dR by (rule onode_ucast)
          with mR={d} show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                       onode_sos (trans (onp ii))"
            by simp
        qed
      with ns = NodeS ii s R ns' = NodeS ii s' R
        show "((σ, snd (netgmap sr ns)), mR:*cast(m), (σ', snd (netgmap sr ns')))
                                                              trans (opnet onp ii; Ri)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ mR
      assume IH1: "s s' ζ mR. (s, mR:*cast(m), s')  trans (pnet np n1)
                          s  reachable (pnet np n1) TT
                          netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                          netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                          wf_net_tree n1
                          ((σ, snd (netgmap sr s)), mR:*cast(m), σ', snd (netgmap sr s'))
                                                                         trans (opnet onp n1)"
        and IH2: "s s' ζ mR. (s, mR:*cast(m), s')  trans (pnet np n2)
                          s  reachable (pnet np n2) TT
                          netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                          netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                          wf_net_tree n2
                          ((σ, snd (netgmap sr s)), mR:*cast(m), σ', snd (netgmap sr s'))
                                                                         trans (opnet onp n2)"
        and "(s, mR:*cast(m), s')  trans (pnet np (n1  n2))"
        and sr: "s  reachable (pnet np (n1  n2)) TT"
        and nm: "netgmap sr s = netmask (net_tree_ips (n1  n2)) (σ, ζ)"
        and nm': "netgmap sr s' = netmask (net_tree_ips (n1  n2)) (σ', snd (netgmap sr s'))"
        and "wf_net_tree (n1  n2)"
      from this(3) have "(s, mR:*cast(m), s')  pnet_sos (trans (pnet np n1)) (trans (pnet np n2))"
        by simp
      then obtain s1 s1' s2 s2' H K
        where "s  = SubnetS s1  s2"
          and "s' = SubnetS s1' s2'"
          and "H  mR"
          and "K  mR = {}"
          and trtr: "((s1, mR:*cast(m), s1')  trans (pnet np n1)
                                   (s2, H¬K:arrive(m), s2')  trans (pnet np n2))
                     ((s1, H¬K:arrive(m), s1')  trans (pnet np n1)
                                   (s2, mR:*cast(m), s2')  trans (pnet np n2))"
          by (rule partial_castTE) metis+

      from wf_net_tree (n1  n2) have "wf_net_tree n1"
                                    and "wf_net_tree n2"
                                    and "net_tree_ips n1  net_tree_ips n2 = {}" by auto

      from sr [simplified s = SubnetS s1 s2] have "s1  reachable (pnet np n1) TT"
        by (rule subnet_reachable(1))
      hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
      with trtr have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

      from sr [simplified s = SubnetS s1 s2] have "s2  reachable (pnet np n2) TT"
        by (rule subnet_reachable(2))
      hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
      with trtr have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

      from nm [simplified s = SubnetS s1 s2]
           net_tree_ips n1  net_tree_ips n2 = {}
           net_ips s1 = net_tree_ips n1
           net_ips s2 = net_tree_ips n2 
        have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          by (rule netgmap_subnet_split1)

      from nm' [simplified s' = SubnetS s1' s2']
           net_tree_ips n1  net_tree_ips n2 = {}
           net_ips s1' = net_tree_ips n1
           net_ips s2' = net_tree_ips n2 
        have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
          by (rule netgmap_subnet_split1)

      from nm [simplified s = SubnetS s1 s2]
           net_ips s1 = net_tree_ips n1
           net_ips s2 = net_tree_ips n2 
        have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
          by (rule netgmap_subnet_split2)

      from nm' [simplified s' = SubnetS s1' s2']
           net_ips s1' = net_tree_ips n1
           net_ips s2' = net_tree_ips n2 
        have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
          by (rule netgmap_subnet_split2)

      from trtr show "((σ, snd (netgmap sr s)), mR:*cast(m), (σ', snd (netgmap sr s')))
                                                               trans (opnet onp (n1  n2))"
      proof (elim disjE conjE)
        assume "(s1, mR:*cast(m), s1')  trans (pnet np n1)"
           and "(s2, H¬K:arrive(m), s2')  trans (pnet np n2)"
        from (s1, mR:*cast(m), s1')  trans (pnet np n1)
             s1  reachable (pnet np n1) TT
             netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))
             netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))
             wf_net_tree n1
          have "((σ, snd (netgmap sr s1)), mR:*cast(m), (σ', snd (netgmap sr s1')))  trans (opnet onp n1)"
            by (rule IH1)

        moreover from (s2, H¬K:arrive(m), s2')  trans (pnet np n2)
             s2  reachable (pnet np n2) TT
             netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))
             netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))
             wf_net_tree n2
          have "((σ, snd (netgmap sr s2)), H¬K:arrive(m), (σ', snd (netgmap sr s2')))  trans (opnet onp n2)"
            by (rule transfer_arrive')

        ultimately have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), mR:*cast(m),
                          (σ', SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                              opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
          using H  mR and K  mR = {} by (rule opnet_sos.intros(1))
        with s = SubnetS s1 s2 s' = SubnetS s1' s2' show ?thesis by simp
      next
        assume "(s1, H¬K:arrive(m), s1')  trans (pnet np n1)"
           and "(s2, mR:*cast(m), s2')  trans (pnet np n2)"
        from (s1, H¬K:arrive(m), s1')  trans (pnet np n1)
             s1  reachable (pnet np n1) TT
             netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))
             netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))
             wf_net_tree n1
          have "((σ, snd (netgmap sr s1)), H¬K:arrive(m), (σ', snd (netgmap sr s1')))  trans (opnet onp n1)"
            by (rule transfer_arrive')

        moreover from (s2, mR:*cast(m), s2')  trans (pnet np n2)
             s2  reachable (pnet np n2) TT
             netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))
             netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))
             wf_net_tree n2
          have "((σ, snd (netgmap sr s2)), mR:*cast(m), (σ', snd (netgmap sr s2')))  trans (opnet onp n2)"
            by (rule IH2)

        ultimately have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), mR:*cast(m),
                          (σ', SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                              opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
          using H  mR and K  mR = {} by (rule opnet_sos.intros(2))
        with s = SubnetS s1 s2 s' = SubnetS s1' s2' show ?thesis by simp
      qed
    qed
    with ζ = snd (netgmap sr s) have "((σ, ζ), mR:*cast(m), (σ', snd (netgmap sr s')))  trans (opnet onp n)"
      by simp
    moreover from j. jnet_ips (snd (netgmap sr s))  σ' j = σ j ζ = snd (netgmap sr s)
      have "j. jnet_ips ζ  σ' j = σ j" by simp
    moreover note netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))
    ultimately show "σ' ζ'. ((σ, ζ), mR:*cast(m), (σ', ζ'))  trans (opnet onp n)
                            (j. jnet_ips ζ  σ' j = σ j)
                            netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
      by auto
  qed

lemma transfer_pnet_action:
  assumes "s  reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
      and "(s, a, s')  trans (pnet np n)"
  obtains σ' ζ' where "((σ, ζ), a, (σ', ζ'))  trans (opnet onp n)"
                  and "j. jnet_ips ζ  σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    show "σ' ζ'. ((σ, ζ), a, (σ', ζ'))  trans (opnet onp n)
                   (j. jnet_ips ζ  σ' j = σ j)
                   netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
    proof (cases a)
      case node_cast
      with assms(4) show ?thesis
        by (auto elim!: transfer_cast [OF _ assms(1-3)])
    next
      case node_deliver
      with assms(4) show ?thesis
        by (auto elim!: transfer_deliver [OF _ assms(1-3)])
    next
      case node_arrive
      with assms(4) show ?thesis
        by (auto elim!: transfer_arrive [OF _ assms(1-3)])
    next
      case node_connect
      with assms(4) show ?thesis
        by (auto elim!: transfer_connect [OF _ assms(1-3)])
    next
      case node_disconnect
      with assms(4) show ?thesis
        by (auto elim!: transfer_disconnect [OF _ assms(1-3)])
    next
      case node_newpkt
      with assms(4) have False by (metis pnet_never_newpkt)
      thus ?thesis ..
    next
      case node_tau
      with assms(4) show ?thesis
        by (auto elim!: transfer_tau [OF _ assms(1-3), simplified])
    qed
  qed

lemma transfer_action_pnet_closed:
  assumes "(s, a, s')  trans (closed (pnet np n))"
  obtains a' where "(s, a', s')  trans (pnet np n)"
               and "σ ζ σ' ζ'.  ((σ, ζ), a', (σ', ζ'))  trans (opnet onp n);
                                  (j. jnet_ips ζ  σ' j = σ j) 
                             ((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))"
  proof (atomize_elim)
    from assms have "(s, a, s')  cnet_sos (trans (pnet np n))" by simp
    thus "a'. (s, a', s')  trans (pnet np n)
                 (σ ζ σ' ζ'. ((σ, ζ), a', (σ', ζ'))  trans (opnet onp n)
                                (j. j  net_ips ζ  σ' j = σ j)
                                ((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n)))"
    proof cases
      case (cnet_cast R m) thus ?thesis
      by (auto intro!: exI [where x="R:*cast(m)"] dest!: ocnet_cast)
    qed (auto intro!: ocnet_sos.intros [simplified])
  qed

lemma transfer_action:
  assumes "s  reachable (closed (pnet np n)) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
      and "(s, a, s')  trans (closed (pnet np n))"
  obtains σ' ζ' where "((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms(1) have "s  reachable (pnet np n) TT" ..
    from assms(4)
      show "σ' ζ'. ((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))
                     netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
        by (cases a)
           ((elim transfer_action_pnet_closed
                  transfer_pnet_action [OF s  reachable (pnet np n) TT assms(2-3)])?,
            (auto intro!: exI)[1])+
  qed

lemma pnet_reachable_transfer':
  assumes "wf_net_tree n"
      and "s  reachable (closed (pnet np n)) TT"
    shows "netgmap sr s  netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
          (is " _  ?f ` ?oreachable n")
  using assms(2) proof induction
    fix s
    assume "s  init (closed (pnet np n))"
    hence "s  init (pnet np n)" by simp
    with wf_net_tree n have "netgmap sr s  netmask (net_tree_ips n) ` init (opnet onp n)"
      by (rule init_pnet_opnet)
    hence "netgmap sr s  netmask (net_tree_ips n) ` init (oclosed (opnet onp n))"
      by simp
    moreover have "netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
                                         netmask (net_tree_ips n) ` ?oreachable n"
      by (intro image_mono subsetI) (rule oreachable_init)
    ultimately show "netgmap sr s  netmask (net_tree_ips n) ` ?oreachable n"
      by (rule rev_subsetD)
  next
    fix s a s'
    assume "s  reachable (closed (pnet np n)) TT"
       and "netgmap sr s  netmask (net_tree_ips n) ` ?oreachable n"
       and "(s, a, s')  trans (closed (pnet np n))"
    from this(2) obtain σ ζ where "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
                              and "(σ, ζ)  ?oreachable n"
      by clarsimp
    from s  reachable (closed (pnet np n)) TT this(1) wf_net_tree n
         and (s, a, s')  trans (closed (pnet np n))
      obtain σ' ζ' where "((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))"
                     and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
        by (rule transfer_action)
    from (σ, ζ)  ?oreachable n and this(1) have "(σ', ζ')  ?oreachable n"
      by (rule oreachable_local) simp
    with netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')
      show "netgmap sr s'  netmask (net_tree_ips n) ` ?oreachable n" by (rule image_eqI)
  qed

definition
  someinit :: "nat  'g"
where
  "someinit i  SOME x. x  (fst o sr) ` init (np i)"

definition
  initmissing :: "((nat  'g option) × 'a)  (nat  'g) × 'a"
where
  "initmissing σ = (λi. case (fst σ) i of None  someinit i | Some s  s, snd σ)"

lemma initmissing_def':
  "initmissing = apfst (default someinit)"
  by (auto simp add: initmissing_def default_def)

lemma netmask_initmissing_netgmap:
  "netmask (net_ips s) (initmissing (netgmap sr s)) = netgmap sr s"
  proof (intro prod_eqI ext)
    fix i
    show "fst (netmask (net_ips s) (initmissing (netgmap sr s))) i = fst (netgmap sr s) i"
      unfolding initmissing_def by (clarsimp split: option.split)
  qed (simp add: initmissing_def)

lemma snd_initmissing [simp]:
  "snd (initmissing x)= snd x"
  unfolding initmissing_def by simp

lemma initmnissing_snd_netgmap [simp]:
  assumes "initmissing (netgmap sr s) = (σ, ζ)"
    shows "snd (netgmap sr s) = ζ"
  using assms unfolding initmissing_def by simp


lemma in_net_ips_fst_init_missing [simp]:
  assumes "i  net_ips s"
    shows "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)"
  using assms unfolding initmissing_def by (clarsimp split: option.split)

lemma not_in_net_ips_fst_init_missing [simp]:
  assumes "i  net_ips s"
    shows "fst (initmissing (netgmap sr s)) i = someinit i"
  using assms unfolding initmissing_def by (clarsimp split: option.split)

lemma initmissing_oreachable_netmask [elim]:
  assumes "initmissing (netgmap sr s)  oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
          (is "_  ?oreachable n")
      and "net_ips s = net_tree_ips n"
    shows "netgmap sr s  netmask (net_tree_ips n) ` ?oreachable n"
  proof -
    obtain σ ζ where "initmissing (netgmap sr s) = (σ, ζ)" by (metis surj_pair)
    with assms(1) have "(σ, ζ)  ?oreachable n" by simp

    have "netgmap sr s = netmask (net_ips s) (σ, ζ)"
    proof (intro prod_eqI ext)
      fix i
      show "fst (netgmap sr s) i = fst (netmask (net_ips s) (σ, ζ)) i"
      proof (cases "inet_ips s")
        assume "inet_ips s"
        hence "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)"
          by (rule in_net_ips_fst_init_missing)
        moreover from inet_ips s have "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
          by (rule some_the_fst_netgmap)
        ultimately show ?thesis
          using initmissing (netgmap sr s) = (σ, ζ) by simp
      qed simp
    next
      from initmissing (netgmap sr s) = (σ, ζ)
        show "snd (netgmap sr s) = snd (netmask (net_ips s) (σ, ζ))"
          by simp
    qed
    with assms(2) have "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)" by simp
    moreover from (σ, ζ)  ?oreachable n
      have "netmask (net_ips s) (σ, ζ)  netmask (net_ips s) ` ?oreachable n"
        by (rule imageI)
    ultimately show ?thesis
      by (simp only: assms(2))
  qed

lemma pnet_reachable_transfer:
  assumes "wf_net_tree n"
      and "s  reachable (closed (pnet np n)) TT"
    shows "initmissing (netgmap sr s)  oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
          (is " _  ?oreachable n")
  using assms(2) proof induction
    fix s
    assume "s  init (closed (pnet np n))"
    hence "s  init (pnet np n)" by simp

    from wf_net_tree n have "initmissing (netgmap sr s)  init (opnet onp n)"
    proof (rule init_lifted [THEN subsetD], intro CollectI exI conjI allI)
      show "initmissing (netgmap sr s) = (fst (initmissing (netgmap sr s)), snd (netgmap sr s))"
        by (metis snd_initmissing surjective_pairing)
    next
      from s  init (pnet np n) show "s  init (pnet np n)" ..
    next
      fix i
      show "if i  net_tree_ips n
            then (fst (initmissing (netgmap sr s))) i = the (fst (netgmap sr s) i)
            else (fst (initmissing (netgmap sr s))) i  (fst  sr) ` init (np i)"
      proof (cases "i  net_tree_ips n", simp_all only: if_True if_False)
        assume "i  net_tree_ips n"
        with s  init (pnet np n) have "i  net_ips s" ..
        thus "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)" by simp
      next
        assume "i  net_tree_ips n"
        with s  init (pnet np n) have "i  net_ips s" ..
        hence "fst (initmissing (netgmap sr s)) i = someinit i" by simp
        moreover have "someinit i  (fst  sr) ` init (np i)"
        unfolding someinit_def proof (rule someI_ex)
          from init_notempty show "x. x  (fst o sr) ` init (np i)" by auto
        qed
        ultimately show "fst (initmissing (netgmap sr s)) i  (fst  sr) ` init (np i)"
          by simp
      qed
    qed
    hence "initmissing (netgmap sr s)  init (oclosed (opnet onp n))" by simp
    thus "initmissing (netgmap sr s)  ?oreachable n" ..
  next
    fix s a s'
    assume "s  reachable (closed (pnet np n)) TT"
       and "(s, a, s')  trans (closed (pnet np n))"
       and "initmissing (netgmap sr s)  ?oreachable n"
    from this(1) have "s  reachable (pnet np n) TT" ..
    hence "net_ips s = net_tree_ips n" by (rule pnet_net_ips_net_tree_ips)
    with initmissing (netgmap sr s)  ?oreachable n
      have "netgmap sr s  netmask (net_tree_ips n) ` ?oreachable n"
        by (rule initmissing_oreachable_netmask)

    obtain σ ζ where "(σ, ζ) = initmissing (netgmap sr s)" by (metis surj_pair)
    with initmissing (netgmap sr s)  ?oreachable n
      have "(σ, ζ)  ?oreachable n" by simp
    from (σ, ζ) = initmissing (netgmap sr s) and net_ips s = net_tree_ips n [symmetric]
      have "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
        by (clarsimp simp add: netmask_initmissing_netgmap)

    with s  reachable (closed (pnet np n)) TT
      obtain σ' ζ' where "((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))"
                     and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
        using wf_net_tree n and (s, a, s')  trans (closed (pnet np n))
        by (rule transfer_action)

    from (σ, ζ)  ?oreachable n have "net_ips ζ = net_tree_ips n"
      by (rule opnet_net_ips_net_tree_ips [OF oclosed_oreachable_oreachable])
    with ((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))
      have "j. jnet_tree_ips n  σ' j = σ j"
        by (clarsimp elim!: ocomplete_no_change)
    have "initmissing (netgmap sr s') = (σ', ζ')"
    proof (intro prod_eqI ext)
      fix i
      from netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')
           j. jnet_tree_ips n  σ' j = σ j
           (σ, ζ) = initmissing (netgmap sr s)
           net_ips s = net_tree_ips n
      show "fst (initmissing (netgmap sr s')) i = fst (σ', ζ') i"
        unfolding initmissing_def by simp
    next
      from netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')
        show "snd (initmissing (netgmap sr s')) = snd (σ', ζ')" by simp
    qed
    moreover from (σ, ζ)  ?oreachable n ((σ, ζ), a, (σ', ζ'))  trans (oclosed (opnet onp n))
      have "(σ', ζ')  ?oreachable n"
        by (rule oreachable_local) (rule TrueI)

    ultimately show "initmissing (netgmap sr s')  ?oreachable n"
      by simp
  qed

definition
  netglobal :: "((nat  'g)  bool)  's net_state  bool"
where
  "netglobal P  (λs. P (fst (initmissing (netgmap sr s))))"

lemma netglobalsimp [simp]:
  "netglobal P s = P (fst (initmissing (netgmap sr s)))"
  unfolding netglobal_def by simp

lemma netglobalE [elim]:
  assumes "netglobal P s"
      and "σ.  P σ; fst (initmissing (netgmap sr s)) = σ   Q σ"
    shows "netglobal Q s"
  using assms by simp

lemma netglobal_weakenE [elim]:
  assumes "p  netglobal P"
      and "σ. P σ  Q σ"
    shows "p  netglobal Q"
  using assms(1) proof (rule invariant_weakenE)
    fix s
    assume "netglobal P s"
    thus "netglobal Q s"
      by (rule netglobalE) (erule assms(2))
  qed

lemma close_opnet:
  assumes "wf_net_tree n"
      and "oclosed (opnet onp n)  (λ_ _ _. True, U →) global P"
    shows "closed (pnet np n)  netglobal P"
  unfolding invariant_def proof
    fix s
    assume "s  reachable (closed (pnet np n)) TT"
    with assms(1)
      have "initmissing (netgmap sr s)  oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
        by (rule pnet_reachable_transfer)
    with assms(2) have "global P (initmissing (netgmap sr s))" ..
    thus "netglobal P s" by simp
  qed

end

locale openproc_parq =
  op?: openproc np onp sr for np :: "ip  ('s, ('m::msg) seq_action) automaton" and onp sr
  + fixes qp :: "('t, 'm seq_action) automaton"
    assumes init_qp_notempty: "init qp  {}"

sublocale openproc_parq  openproc "λi. np i ⟨⟨ qp"
                                   "λi. onp i ⟨⟨⇘iqp"
                                   "λ(p, q). (fst (sr p), (snd (sr p), q))"
  proof unfold_locales
    fix i
    show "{ (σ, ζ) |σ ζ s. s  init (np i ⟨⟨ qp)
                          (σ i, ζ) = ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)
                          (j. ji  σ j  (fst o (λ(p, q). (fst (sr p), (snd (sr p), q))))
                                                  ` init (np j ⟨⟨ qp)) }  init (onp i ⟨⟨⇘iqp)"
       (is "?S  _")
    proof
      fix s
      assume "s  ?S"
      then obtain σ p lq
        where "s = (σ, (snd (sr p), lq))"
          and "lq  init qp"
          and "p  init (np i)"
          and "σ i = fst (sr p)"
          and "j. j  i  σ j  (fst  (λ(p, q). (fst (sr p), snd (sr p), q)))
                                                                        ` (init (np j) × init qp)"
        by auto
      from this(5) have "j. j  i  σ j  (fst  sr) ` init (np j)"
        by auto
      with p  init (np i) and σ i = fst (sr p) have "(σ, snd (sr p))  init (onp i)"
        by - (rule init [THEN subsetD], auto)
      with lq init qp have "((σ, snd (sr p)), lq)  init (onp i) × init qp"
        by simp
      hence "(σ, (snd (sr p), lq))  extg ` (init (onp i) × init qp)"
        by (rule rev_image_eqI) simp
      with s = (σ, (snd (sr p), lq)) show "s  init (onp i ⟨⟨⇘iqp)"
        by simp
    qed
  next
    fix i s a s' σ σ'
    assume "σ i = fst ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)"
       and "σ' i = fst ((λ(p, q). (fst (sr p), (snd (sr p), q))) s')"
       and "(s, a, s')  trans (np i ⟨⟨ qp)"
    then obtain p q p' q' where "s  = (p, q)"
                            and "s' = (p', q')"
                            and "σ i  = fst (sr p)"
                            and "σ' i = fst (sr p')"
      by (clarsimp split: prod.split_asm)
    from this(1-2) and (s, a, s')  trans (np i ⟨⟨ qp)
      have "((p, q), a, (p', q'))  parp_sos (trans (np i)) (trans qp)" by simp
    hence "((σ, (snd (sr p), q)), a, (σ', (snd (sr p'), q')))  trans (onp i ⟨⟨⇘iqp)"
    proof cases
      assume "q' = q"
         and "(p, a, p')  trans (np i)"
         and "m. a  receive m"
      from σ i = fst (sr p) and σ' i = fst (sr p') this(2)
        have "((σ, snd (sr p)), a, (σ', snd (sr p')))  trans (onp i)" by (rule trans)
      with q' = q and m. a  receive m
        show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q')))  trans (onp i ⟨⟨⇘iqp)"
          by (auto elim!: oparleft)
    next
      assume "p' = p"
         and "(q, a, q')  trans qp"
         and "m. a  send m"
      with σ i = fst (sr p) and σ' i = fst (sr p')
        show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q')))  trans (onp i ⟨⟨⇘iqp)"
          by (auto elim!: oparright)
    next
      fix m
      assume "a = τ"
         and "(p, receive m, p')  trans (np i)"
         and "(q, send m, q')  trans qp"
      from σ i = fst (sr p) and σ' i = fst (sr p') this(2)
        have "((σ, snd (sr p)), receive m, (σ', snd (sr p')))  trans (onp i)"
          by (rule trans)
      with (q, send m, q')  trans qp and a = τ
        show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q')))  trans (onp i ⟨⟨⇘iqp)"
          by (simp del: step_seq_tau) (rule oparboth)
    qed
    with s = (p, q) s' = (p', q')
      show "((σ, snd ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)), a,
                 (σ', snd ((λ(p, q). (fst (sr p), (snd (sr p), q))) s')))  trans (onp i ⟨⟨⇘iqp)"
        by simp
  next
    show "j. init (np j ⟨⟨ qp)  {}"
      by (clarsimp simp add: init_notempty init_qp_notempty)
  qed

end