Theory OClosed_Lifting

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

section "Lifting rules for (open) closed networks"

theory OClosed_Lifting
imports OPnet_Lifting
begin

lemma trans_fst_oclosed_fst1 [dest]:
  "(s, connect(i, i'), s') ∈ ocnet_sos (trans p) ⟹ (s, connect(i, i'), s') ∈ trans p"
  by (metis prod.exhaust oconnect_completeTE)

lemma trans_fst_oclosed_fst2 [dest]:
  "(s, disconnect(i, i'), s') ∈ ocnet_sos (trans p) ⟹ (s, disconnect(i, i'), s') ∈ trans p"
  by (metis prod.exhaust odisconnect_completeTE)

lemma trans_fst_oclosed_fst3 [dest]:
  "(s, i:deliver(d), s') ∈ ocnet_sos (trans p) ⟹      (s, i:deliver(d), s') ∈ trans p"
  by (metis prod.exhaust odeliver_completeTE)

lemma oclosed_oreachable_inclosed:
  assumes "(σ, ζ) ∈ oreachable (oclosed (opnet np p)) (λ_ _ _. True) U"
    shows "(σ, ζ) ∈ oreachable (opnet np p) (otherwith ((=)) (net_tree_ips p) inoclosed) U"
    (is "_ ∈ oreachable _ ?owS _")
  using assms proof (induction rule: oreachable_pair_induct)
    fix σ ζ
    assume "(σ, ζ) ∈ init (oclosed (opnet np p))"
    hence "(σ, ζ) ∈ init (opnet np p)" by simp
    thus "(σ, ζ) ∈ oreachable (opnet np p) ?owS U" ..
  next
    fix σ ζ σ'
    assume "(σ, ζ) ∈ oreachable (opnet np p) ?owS U"
       and "U σ σ'"
    thus "(σ', ζ) ∈ oreachable (opnet np p) ?owS U"
      by - (rule oreachable_other')
  next
    fix σ ζ σ' ζ' a
    assume zor: "(σ, ζ) ∈ oreachable (opnet np p) ?owS U"
       and ztr: "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet np p))"
    from this(1) have [simp]: "net_ips ζ = net_tree_ips p"
      by (rule opnet_net_ips_net_tree_ips)
    from ztr have "((σ, ζ), a, (σ', ζ')) ∈ ocnet_sos (trans (opnet np p))" by simp
    thus "(σ', ζ') ∈ oreachable (opnet np p) ?owS U"
    proof cases
      fix i K d di
      assume "a = i:newpkt(d, di)"
         and tr: "((σ, ζ), {i}¬K:arrive(msg_class.newpkt (d, di)), (σ', ζ')) ∈ trans (opnet np p)"
         and "∀j. j ∉ net_ips ζ ⟶ σ' j = σ j"
      from this(3) have "∀j. j ∉ net_tree_ips p ⟶ σ' j = σ j"
        using ‹net_ips ζ = net_tree_ips p› by auto
      hence "otherwith ((=)) (net_tree_ips p) inoclosed σ σ' ({i}¬K:arrive(msg_class.newpkt (d, di)))"
        by auto
      with zor tr show ?thesis
        by - (rule oreachable_local')
    next
      assume "a = τ"
         and tr: "((σ, ζ), τ, (σ', ζ')) ∈ trans (opnet np p)"
         and "∀j. j ∉ net_ips ζ ⟶ σ' j = σ j"
      from this(3) have "∀j. j ∉ net_tree_ips p ⟶ σ' j = σ j"
        using ‹net_ips ζ = net_tree_ips p› by auto
      hence "otherwith ((=)) (net_tree_ips p) inoclosed σ σ' τ"
        by auto
      with zor tr show ?thesis by - (rule oreachable_local')
    qed (insert ‹net_ips ζ = net_tree_ips p›,
         auto elim!: oreachable_local' [OF zor])
  qed

lemma oclosed_oreachable_oreachable [elim]:
  assumes "(σ, ζ) ∈ oreachable (oclosed (opnet onp p)) (λ_ _ _. True) U"
    shows "(σ, ζ) ∈ oreachable (opnet onp p) (λ_ _ _. True) U"
  using assms by (rule oclosed_oreachable_inclosed [THEN oreachable_weakenE]) simp

lemma inclosed_closed [intro]:
  assumes cinv: "opnet np p ⊨ (otherwith ((=)) (net_tree_ips p) inoclosed, U →) P"
    shows "oclosed (opnet np p) ⊨ (λ_ _ _. True, U →) P"
  using assms unfolding oinvariant_def
  by (clarsimp dest!: oclosed_oreachable_inclosed)

end