Quelle  Closed.thy

(*  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; R_i⟩)) 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 "i∉net_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 "i∉net_ips s" by auto
    with tr have "i∉net_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 "i∈net_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 "i∈net_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)) ==>
                      i∈net_tree_ips p1 ==> the (netmap s i) ∈ init (np i)"
       and IH2: "∧s. s ∈ init (closed (pnet np p2)) ==>
                     i∈net_tree_ips p2 ==> the (netmap s i) ∈ init (np i)"
       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 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 "i∈net_tree_ips p2")
      assume "i∈net_tree_ips p2"
      with ‹s2 ∈ init (closed (pnet np p2))› have "the (netmap s2 i) ∈ init (np i)"
        by (rule IH2)
      moreover from ‹i∈net_tree_ips p2› and ‹net_tree_ips p2 = net_ips s2›
        have "i∈net_ips s2" by simp
      ultimately show ?thesis
        using ‹s = SubnetS s1 s2› by (auto simp add: net_ips_is_dom_netmap)
    next
      assume "i∉net_tree_ips p2"
      with ‹i∈net_tree_ips (p1 ∥ p2)› have "i∈net_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 ‹i∈net_tree_ips p1› and ‹net_tree_ips p1 = net_ips s1›
        have "i∈net_ips s1" by simp
      moreover from ‹i∉net_tree_ips p2› and ‹net_tree_ips p2 = net_ips s2›
        have "i∉net_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