Theory OPnet

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

section "Lemmas for open partial networks"

theory OPnet
imports OAWN_SOS OInvariants
begin

text ‹
  These lemmas mostly concern the preservation of node structure by @{term opnet_sos} transitions.
›

lemma opnet_maintains_dom:
  assumes "((σ, ns), a, (σ', ns')) ∈ trans (opnet np p)"
    shows "net_ips ns = net_ips ns'"
  using assms proof (induction p arbitrary: σ ns a σ' ns')
    fix i R σ ns a σ' ns'
    assume "((σ, ns), a, (σ', ns')) ∈ trans (opnet np ⟨i; R⟩)"
    hence "((σ, ns), a, (σ', ns')) ∈ onode_sos (trans (np i))" ..
    thus "net_ips ns = net_ips ns'"
      by (simp add: net_ips_is_dom_netmap)
         (erule onode_sos.cases, simp_all)
  next
    fix p1 p2 σ ns a σ' ns'
    assume "⋀σ ns a σ' ns'. ((σ, ns), a, (σ', ns')) ∈ trans (opnet np p1) ⟹ net_ips ns = net_ips ns'"
       and "⋀σ ns a σ' ns'. ((σ, ns), a, (σ', ns')) ∈ trans (opnet np p2) ⟹ net_ips ns = net_ips ns'"
       and "((σ, ns), a, (σ', ns')) ∈ trans (opnet np (p1 ∥ p2))"
    thus "net_ips ns = net_ips ns'"
      by simp (erule opnet_sos.cases, simp_all)
  qed

lemma opnet_net_ips_net_tree_ips:
  assumes "(σ, ns) ∈ oreachable (opnet np p) S U"
    shows "net_ips ns = net_tree_ips p"
  using assms proof (induction rule: oreachable_pair_induct)
    fix σ s
    assume "(σ, s) ∈ init (opnet np p)"
    thus "net_ips s = net_tree_ips p"
    proof (induction p arbitrary: σ s)
      fix p1 p2 σ s
      assume IH1: "(⋀σ s. (σ, s) ∈ init (opnet np p1) ⟹ net_ips s = net_tree_ips p1)"
         and IH2: "(⋀σ s. (σ, s) ∈ init (opnet np p2) ⟹ net_ips s = net_tree_ips p2)"
         and "(σ, s) ∈ init (opnet np (p1 ∥ p2))"
      thus "net_ips s = net_tree_ips (p1 ∥ p2)"
        by (clarsimp simp add: net_ips_is_dom_netmap)
           (metis Un_commute)
    qed (clarsimp simp add: onode_comps)
  next
    fix σ s σ' s' a
    assume "(σ, s) ∈ oreachable (opnet np p) S U"
       and "net_ips s = net_tree_ips p"
       and "((σ, s), a, (σ', s')) ∈ trans (opnet np p)"
       and "S σ σ' a"
    thus "net_ips s' = net_tree_ips p"
      by (simp add: net_ips_is_dom_netmap)
         (metis net_ips_is_dom_netmap opnet_maintains_dom)
  qed simp

lemma opnet_net_ips_net_tree_ips_init:
  assumes "(σ, ns) ∈ init (opnet np p)"
    shows "net_ips ns = net_tree_ips p"
  using assms(1) by (rule oreachable_init [THEN opnet_net_ips_net_tree_ips])

lemma opartial_net_preserves_subnets:
  assumes "((σ, SubnetS s t), a, (σ', st')) ∈ opnet_sos (trans (opnet np p1)) (trans (opnet np p2))"
    shows "∃s' t'. st' = SubnetS s' t'"
  using assms by cases simp_all

lemma net_par_oreachable_is_subnet:
  assumes "(σ, st) ∈ oreachable (opnet np (p1 ∥ p2)) S U"
    shows "∃s t. st = SubnetS s t"
  proof -
    define p where "p = (σ, st)"
    with assms have "p ∈ oreachable (opnet np (p1 ∥ p2)) S U" by simp
    hence "∃σ s t. p = (σ, SubnetS s t)"
      by induct (auto dest!: opartial_net_preserves_subnets)
    with p_def show ?thesis by simp
  qed

end