Theory Closed

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

section "Lemmas for closed networks"

theory Closed
imports Pnet
begin

lemma complete_net_preserves_subnets:
  assumes "(SubnetS s t, a, st')  cnet_sos (pnet_sos (trans (pnet np p1)) (trans (pnet np p2)))"
    shows "s' t'. st' = SubnetS s' t'"
  using assms by cases (auto dest: partial_net_preserves_subnets)

lemma complete_net_reachable_is_subnet:
  assumes "st  reachable (closed (pnet np (p1  p2))) I"
    shows "s t. st = SubnetS s t"
  using assms by induction (auto dest!: complete_net_preserves_subnets)

lemma closed_reachable_par_subnet_induct [consumes, case_names init step]:
  assumes "SubnetS s t  reachable (closed (pnet np (p1  p2))) I"
      and init: "s t. SubnetS s t  init (closed (pnet np (p1  p2)))  P s t"
      and step: "s t s' t' a. 
                    SubnetS s t  reachable (closed (pnet np (p1  p2))) I;
                    P s t; (SubnetS s t, a, SubnetS s' t')  trans (closed (pnet np (p1  p2))); I a 
                     P s' t'"
    shows "P s t"
  using assms(1) proof (induction "SubnetS s t" arbitrary: s t)
    fix s t
    assume "SubnetS s t  init (closed (pnet np (p1  p2)))"
    with init show "P s t" .
  next
    fix st a s' t'
    assume "st  reachable (closed (pnet np (p1  p2))) I"
       and tr: "(st, a, SubnetS s' t')  trans (closed (pnet np (p1  p2)))"
       and "I a"
       and IH: "s t. st = SubnetS s t  P s t"
    from this(1) obtain s t where "st = SubnetS s t"
                              and "SubnetS s t  reachable (closed (pnet np (p1  p2))) I"
      by (metis complete_net_reachable_is_subnet)
    note this(2)
    moreover from IH and st = SubnetS s t have "P s t" .
    moreover from tr and st = SubnetS s t
      have "(SubnetS s t, a, SubnetS s' t')  trans (closed (pnet np (p1  p2)))" by simp
    ultimately show "P s' t'"
      using I a by (rule assms(3))
  qed

lemma reachable_closed_reachable_pnet [elim]:
  assumes "s  reachable (closed (pnet np n)) TT"
    shows "s  reachable (pnet np n) TT"
  using assms proof (induction rule: reachable.induct)
    fix s s' a
    assume sr: "s  reachable (pnet np n) TT"
       and "(s, a, s')  trans (closed (pnet np n))"
    from this(2) have "(s, a, s')  cnet_sos (trans (pnet np n))" by simp
    thus "s'  reachable (pnet np n) TT"
      by cases (insert sr, auto elim!: reachable_step)
  qed (auto elim: reachable_init)

lemma closed_node_net_state [elim]:
  assumes "st  reachable (closed (pnet np ii; Ri)) TT"
  obtains ξ p q R where "st = NodeS ii ((ξ, p), q) R"
  using assms by (metis net_node_reachable_is_node reachable_closed_reachable_pnet surj_pair)

lemma closed_subnet_net_state [elim]:
  assumes "st  reachable (closed (pnet np (p1  p2))) TT"
  obtains s t where "st = SubnetS s t"
  using assms by (metis reachable_closed_reachable_pnet net_par_reachable_is_subnet)

lemma closed_imp_pnet_trans [elim, dest]:
  assumes "(s, a, s')  trans (closed (pnet np n))"
    shows "a'. (s, a', s')  trans (pnet np n)"
  using assms by (auto elim!: cnet_sos.cases)

lemma reachable_not_in_net_tree_ips [elim]:
  assumes "s  reachable (closed (pnet np n)) TT"
      and "inet_tree_ips n"
    shows "netmap s i = None"
  using assms proof induction
    fix s
    assume "s  init (closed (pnet np n))"
       and "i  net_tree_ips n"
    thus "netmap s i = None"                                     
    proof (induction n arbitrary: s)
      fix ii R s
      assume "s  init (closed (pnet np ii; R))"
         and "i  net_tree_ips ii; R"
      from this(2) have "i  ii" by simp
      moreover from s  init (closed (pnet np ii; R)) obtain p where "s = NodeS ii p R"
        by simp (metis pnet.simps(1) pnet_node_init')
      ultimately show "netmap s i = None" by simp
    next
      fix p1 p2 s
      assume IH1: "s. s  init (closed (pnet np p1))  i  net_tree_ips p1
                         netmap s i = None"
         and IH2: "s. s  init (closed (pnet np p2))  i  net_tree_ips p2
                         netmap s i = None"
         and "s  init (closed (pnet np (p1  p2)))"
         and "i  net_tree_ips (p1  p2)"
      from this(3) obtain s1 s2 where "s = SubnetS s1 s2"
                                  and "s1  init (closed (pnet np p1))"
                                  and "s2  init (closed (pnet np p2))" by simp metis
      moreover from i  net_tree_ips (p1  p2) have "i  net_tree_ips p1"
                                                  and "i  net_tree_ips p2" by auto
      ultimately have "netmap s1 i = None"
                  and "netmap s2 i = None"
        using IH1 IH2 by auto
      with s = SubnetS s1 s2 show "netmap s i = None" by simp
    qed
  next
    fix s a s'
    assume sr: "s  reachable (closed (pnet np n)) TT"
       and tr: "(s, a, s')  trans (closed (pnet np n))"
       and IH: "i  net_tree_ips n  netmap s i = None"
       and "i  net_tree_ips n"
    from this(3-4) have "inet_ips s" by auto
    with tr have "inet_ips s'"
      by simp (erule cnet_sos.cases, (metis net_ips_is_dom_netmap pnet_maintains_dom)+)
    thus "netmap s' i = None" by simp
  qed

lemma closed_pnet_aodv_init [elim]:
  assumes "s  init (closed (pnet np n))"
      and "inet_tree_ips n"
    shows "the (netmap s i)  init (np i)"
  using assms proof (induction n arbitrary: s)
    fix ii R s
    assume "s  init (closed (pnet np ii; R))"
       and "inet_tree_ips ii; R"
    hence "s  init (pnet np i; R)" by simp
    then obtain p where "s = NodeS i p R"
                    and "p  init (np i)" ..
    with s = NodeS i p R have "netmap s = [i  p]" by simp
    with p  init (np i) show "the (netmap s i)  init (np i)" by simp
  next
    fix p1 p2 s
    assume IH1: "s. s  init (closed (pnet np p1)) 
                      inet_tree_ips p1  the (netmap s i)  init (np i)"
       and IH2: "s. s  init (closed (pnet np p2)) 
                     inet_tree_ips p2  the (netmap s i)  init (np i)"
       and "s  init (closed (pnet np (p1  p2)))"
       and "inet_tree_ips (p1  p2)"
    from this(3) obtain s1 s2 where "s = SubnetS s1 s2"
                                and "s1  init (closed (pnet np p1))"
                                and "s2  init (closed (pnet np p2))"
      by auto
    from this(2) have "net_tree_ips p1 = net_ips s1"
      by (clarsimp dest!: pnet_init_net_ips_net_tree_ips)
    from s2  init (closed (pnet np p2)) have "net_tree_ips p2 = net_ips s2"
      by (clarsimp dest!: pnet_init_net_ips_net_tree_ips)
    show "the (netmap s i)  init (np i)"
    proof (cases "inet_tree_ips p2")
      assume "inet_tree_ips p2"
      with s2  init (closed (pnet np p2)) have "the (netmap s2 i)  init (np i)"
        by (rule IH2)
      moreover from inet_tree_ips p2 and net_tree_ips p2 = net_ips s2
        have "inet_ips s2" by simp
      ultimately show ?thesis
        using s = SubnetS s1 s2 by (auto simp add: net_ips_is_dom_netmap)
    next
      assume "inet_tree_ips p2"
      with inet_tree_ips (p1  p2) have "inet_tree_ips p1" by simp
      with s1  init (closed (pnet np p1)) have "the (netmap s1 i)  init (np i)"
        by (rule IH1)
      moreover from inet_tree_ips p1 and net_tree_ips p1 = net_ips s1
        have "inet_ips s1" by simp
      moreover from inet_tree_ips p2 and net_tree_ips p2 = net_ips s2
        have "inet_ips s2" by simp
      ultimately show ?thesis
        using s = SubnetS s1 s2
        by (simp add: map_add_dom_app_simps net_ips_is_dom_netmap)
    qed
  qed

end