Theory OAWN_Convert

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

section "Transfer standard invariants into open invariants"

theory OAWN_Convert
imports AWN_SOS_Labels AWN_Invariants
        OAWN_SOS OAWN_Invariants
begin

definition initiali :: "'i ⇒ (('i ⇒ 'g) × 'l) set ⇒ ('g × 'l) set ⇒ bool"
where "initiali i OI CI ≡ ({(σ i, p)|σ p. (σ, p) ∈ OI} = CI)"

lemma initialiI [intro]:
  assumes OICI: "⋀σ p. (σ, p) ∈ OI ⟹ (σ i, p) ∈ CI"
      and CIOI: "⋀ξ p. (ξ, p) ∈ CI ⟹ ∃σ. ξ = σ i ∧ (σ, p) ∈ OI"
    shows "initiali i OI CI"
  unfolding initiali_def
  by (intro set_eqI iffI) (auto elim!: OICI CIOI)

lemma open_from_initialiD [dest]:
  assumes "initiali i OI CI"
      and "(σ, p) ∈ OI"
    shows "∃ξ. σ i = ξ ∧ (ξ, p) ∈ CI"
  using assms unfolding initiali_def by auto

lemma closed_from_initialiD [dest]:
  assumes "initiali i OI CI"
      and "(ξ, p) ∈ CI"
    shows "∃σ. σ i = ξ ∧ (σ, p) ∈ OI"
  using assms unfolding initiali_def by auto

definition
  seql :: "'i ⇒ (('s × 'l) ⇒ bool) ⇒ (('i ⇒ 's) × 'l) ⇒ bool"
where
  "seql i P ≡ (λ(σ, p). P (σ i, p))"

lemma seqlI [intro]:
  "P (fst s i, snd s) ⟹ seql i P s"
  by (clarsimp simp: seql_def)

lemma same_seql [elim]:
  assumes "∀j∈{i}. σ' j = σ j"
      and "seql i P (σ', s)"
    shows "seql i P (σ, s)"
  using assms unfolding seql_def by (clarsimp)

lemma seqlsimp:
  "seql i P (σ, p) = P (σ i, p)"
  unfolding seql_def by simp

lemma other_steps_resp_local [intro!, simp]: "other_steps (other A I) I"
  by (clarsimp elim!: otherE)

lemma seql_onl_swap:
  "seql i (onl Γ P) = onl Γ (seql i P)"
  unfolding seql_def onl_def by simp

lemma oseqp_sos_resp_local_steps [intro!, simp]:
  fixes Γ :: "'p ⇒ ('s, 'm, 'p, 'l) seqp"
  shows "local_steps (oseqp_sos Γ i) {i}"
  proof
    fix σ σ' ζ ζ' :: "nat ⇒ 's" and s a s'
    assume tr: "((σ, s), a, σ', s') ∈ oseqp_sos Γ i"
       and "∀j∈{i}. ζ j = σ j"
    thus "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, s), a, (ζ', s')) ∈ oseqp_sos Γ i"
    proof induction
      fix σ σ' l ms p
      assume "σ' i = σ i"
         and "∀j∈{i}. ζ j = σ j"
      hence "((ζ, {l}broadcast(ms).p), broadcast (ms (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
        by (metis obroadcastT singleton_iff)
      with ‹∀j∈{i}. ζ j = σ j› show "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧
            ((ζ, {l}broadcast(ms).p), broadcast (ms (σ i)), (ζ', p)) ∈ oseqp_sos Γ i"
        by blast
    next
      fix σ σ' :: "nat ⇒ 's" and fmsg :: "'m ⇒ 's ⇒ 's" and msg l p
      assume *:  "σ' i = fmsg msg (σ i)"
         and **: "∀j∈{i}. ζ j = σ j"
      hence "∀j∈{i}. (ζ(i := fmsg msg (ζ i))) j = σ' j" by clarsimp
      moreover from * **
        have "((ζ, {l}receive(fmsg).p), receive msg, (ζ(i := fmsg msg (ζ i)), p)) ∈ oseqp_sos Γ i"
        by (metis fun_upd_same oreceiveT)
      ultimately show "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧
                            ((ζ, {l}receive(fmsg).p), receive msg, (ζ', p)) ∈ oseqp_sos Γ i"
        by blast
    next
      fix σ' σ l p and fas :: "'s ⇒ 's"
      assume *:  "σ' i = fas (σ i)"
         and **: "∀j∈{i}. ζ j = σ j"
      hence "∀j∈{i}. (ζ(i := fas (ζ i))) j = σ' j" by clarsimp
      moreover from * ** have "((ζ, {l}⟦fas⟧ p), τ, (ζ(i := fas (ζ i)), p)) ∈ oseqp_sos Γ i"
        by (metis fun_upd_same oassignT)
      ultimately show "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, {l}⟦fas⟧ p), τ, (ζ', p)) ∈ oseqp_sos Γ i"
        by blast
    next
      fix g :: "'s ⇒ 's set" and σ σ' l p
      assume *:  "σ' i ∈ g (σ i)"
         and **: "∀j∈{i}. ζ j = σ j"
      hence "∀j∈{i}. (SOME ζ'. ζ' i = σ' i) j = σ' j" by simp (metis (lifting, full_types) some_eq_ex)
      moreover with * ** have "((ζ, {l}⟨g⟩ p), τ, (SOME ζ'. ζ' i = σ' i, p)) ∈ oseqp_sos Γ i"
        by simp (metis oguardT step_seq_tau)
      ultimately show "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, {l}⟨g⟩ p), τ, (ζ', p)) ∈ oseqp_sos Γ i"
        by blast
    next
      fix σ pn a σ' p'
      assume "((σ, Γ pn), a, (σ', p')) ∈ oseqp_sos Γ i"
         and IH: "∀j∈{i}. ζ j = σ j ⟹ ∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, Γ pn), a, (ζ', p')) ∈ oseqp_sos Γ i"
         and "∀j∈{i}. ζ j = σ j"
      then obtain ζ' where "∀j∈{i}. ζ' j = σ' j"
                       and "((ζ, Γ pn), a, (ζ', p')) ∈ oseqp_sos Γ i"
        by blast
      thus "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, call(pn)), a, (ζ', p')) ∈ oseqp_sos Γ i"
        by blast
    next
      fix σ p a σ' p' q
      assume "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
         and "∀j∈{i}. ζ j = σ j ⟹ ∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, p), a, (ζ', p')) ∈ oseqp_sos Γ i"
         and "∀j∈{i}. ζ j = σ j"
      then obtain ζ' where "∀j∈{i}. ζ' j = σ' j"
                       and "((ζ, p), a, (ζ', p')) ∈ oseqp_sos Γ i"
        by blast
      thus "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, p ⊕ q), a, (ζ', p')) ∈ oseqp_sos Γ i"
        by blast
    next
      fix σ p a σ' q q'
      assume "((σ, q), a, (σ', q')) ∈ oseqp_sos Γ i"
         and "∀j∈{i}. ζ j = σ j ⟹ ∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, q), a, (ζ', q')) ∈ oseqp_sos Γ i"
         and "∀j∈{i}. ζ j = σ j"
      then obtain ζ' where "∀j∈{i}. ζ' j = σ' j"
                       and "((ζ, q), a, (ζ', q')) ∈ oseqp_sos Γ i"
        by blast
      thus "∃ζ'. (∀j∈{i}. ζ' j = σ' j) ∧ ((ζ, p ⊕ q), a, (ζ', q')) ∈ oseqp_sos Γ i"
        by blast
    qed (simp_all, (metis ogroupcastT ounicastT onotunicastT osendT odeliverT)+)
  qed

lemma oseqp_sos_subreachable [intro!, simp]:
  assumes "trans OA = oseqp_sos Γ i"
    shows "subreachable OA (other ANY {i}) {i}"
  by rule (clarsimp simp add: assms(1))+

lemma oseq_step_is_seq_step:
    fixes σ :: "ip ⇒ 's"
  assumes "((σ, p), a :: 'm seq_action, (σ', p')) ∈ oseqp_sos Γ i"
      and "σ i = ξ"
    shows "∃ξ'. σ' i = ξ' ∧ ((ξ, p), a, (ξ', p')) ∈ seqp_sos Γ"
  using assms proof induction
    fix σ σ' l ms p
    assume "σ' i = σ i"
       and "σ i = ξ"
    hence "σ' i = ξ" by simp
    have "((ξ, {l}broadcast(ms).p), broadcast (ms ξ), (ξ, p)) ∈ seqp_sos Γ"
      by auto
    with ‹σ i = ξ› and ‹σ' i = ξ› show "∃ξ'. σ' i = ξ'
             ∧ ((ξ, {l}broadcast(ms).p), broadcast (ms (σ i)), (ξ', p)) ∈ seqp_sos Γ"
       by clarsimp
  next
    fix fmsg :: "'m ⇒ 's ⇒ 's" and msg :: 'm and σ' σ l p
    assume "σ' i = fmsg msg (σ i)"
       and "σ i = ξ"
    have "((ξ, {l}receive(fmsg).p), receive msg, (fmsg msg ξ, p)) ∈ seqp_sos Γ"
      by auto
    with ‹σ' i = fmsg msg (σ i)› and ‹σ i = ξ›
      show "∃ξ'. σ' i = ξ' ∧ ((ξ, {l}receive(fmsg).p), receive msg, (ξ', p)) ∈ seqp_sos Γ"
         by clarsimp
  qed (simp_all, (metis assignT choiceT1 choiceT2 groupcastT guardT
                        callT unicastT notunicastT sendT deliverT step_seq_tau)+)

lemma reachable_oseq_seqp_sos:
  assumes "(σ, p) ∈ reachable OA I"
      and "initiali i (init OA) (init A)"
      and spo: "trans OA = oseqp_sos Γ i"
      and sp: "trans A = seqp_sos Γ"
      shows "∃ξ. σ i = ξ ∧ (ξ, p) ∈ reachable A I"
  using assms(1) proof (induction rule: reachable_pair_induct)
    fix σ p
    assume "(σ, p) ∈ init OA"
    with ‹initiali i (init OA) (init A)› obtain ξ where "σ i = ξ"
                                                    and "(ξ, p) ∈ init A"
      by auto
    from ‹(ξ, p) ∈ init A› have "(ξ, p) ∈ reachable A I" ..
    with ‹σ i = ξ› show "∃ξ. σ i = ξ ∧ (ξ, p) ∈ reachable A I"
      by auto
  next
    fix σ p σ' p' a
    assume "(σ, p) ∈ reachable OA I"
       and IH: "∃ξ. σ i = ξ ∧ (ξ, p) ∈ reachable A I"
       and otr: "((σ, p), a, (σ', p')) ∈ trans OA"
       and "I a"
    from IH obtain ξ where "σ i = ξ"
                       and cr: "(ξ, p) ∈ reachable A I"
      by clarsimp
    from otr and spo have "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i" by simp
    with ‹σ i = ξ› obtain ξ' where "σ' i = ξ'"
                               and "((ξ, p), a, (ξ', p')) ∈ seqp_sos Γ"
        by (auto dest!: oseq_step_is_seq_step)
    from this(2) and sp have ctr: "((ξ, p), a, (ξ', p')) ∈ trans A" by simp
    from ‹(ξ, p) ∈ reachable A I› and ctr and ‹I a›
      have "(ξ', p') ∈ reachable A I" ..
    with ‹σ' i = ξ'› show "∃ξ. σ' i = ξ ∧ (ξ, p') ∈ reachable A I"
      by blast
  qed

lemma reachable_oseq_seqp_sos':
  assumes "s ∈ reachable OA I"
      and "initiali i (init OA) (init A)"
      and "trans OA = oseqp_sos Γ i"
      and "trans A = seqp_sos Γ"
    shows "∃ξ. (fst s) i = ξ ∧ (ξ, snd s) ∈ reachable A I"
  using assms
  by - (cases s, auto dest: reachable_oseq_seqp_sos)

text ‹
  Any invariant shown in the (simpler) closed semantics can be transferred to an invariant in
  the open semantics.
›

theorem open_seq_invariant [intro]:
  assumes "A ⊫ (I →) P"
      and "initiali i (init OA) (init A)"
      and spo: "trans OA = oseqp_sos Γ i"
      and sp: "trans A = seqp_sos Γ"
    shows "OA ⊨ (act I, other ANY {i} →) (seql i P)"
  proof -
    have "OA ⊫ (I →) (seql i P)"
      proof (rule invariant_arbitraryI)
        fix s                                      
        assume "s ∈ reachable OA I"
        with ‹initiali i (init OA) (init A)› obtain ξ where "(fst s) i = ξ"
                                                        and "(ξ, snd s) ∈ reachable A I"
          by (auto dest: reachable_oseq_seqp_sos' [OF _ _ spo sp])
        with ‹A ⊫ (I →) P› have "P (ξ, snd s)" by auto
        with ‹(fst s) i = ξ› show "seql i P s" by auto
      qed
    moreover from spo have "subreachable OA (other ANY {i}) {i}" ..
    ultimately show ?thesis
    proof (rule open_closed_invariant)
      fix σ σ' s
      assume "∀j∈{i}. σ' j = σ j"
         and "seql i P (σ', s)"
      thus "seql i P (σ, s)" ..
    qed
  qed

definition
  seqll :: "'i ⇒ ((('s × 'l) × 'a × ('s × 'l)) ⇒ bool)
               ⇒ ((('i ⇒ 's) × 'l) × 'a × (('i ⇒ 's) × 'l)) ⇒ bool"
where
  "seqll i P ≡ (λ((σ, p), a, (σ', p')). P ((σ i, p), a, (σ' i, p')))"

lemma same_seqll [elim]:
  assumes "∀j∈{i}. σ⇩1' j = σ⇩1 j"
      and "∀j∈{i}. σ⇩2' j = σ⇩2 j"
      and "seqll i P ((σ⇩1', s), a, (σ⇩2', s'))"
    shows "seqll i P ((σ⇩1,  s), a, (σ⇩2,  s'))"
  using assms unfolding seqll_def by (clarsimp)

lemma seqllI [intro!]:
  assumes "P ((σ i, p), a, (σ' i, p'))"
    shows "seqll i P ((σ, p), a, (σ', p'))"
  using assms unfolding seqll_def by simp

lemma seqllD [dest]:
  assumes "seqll i P ((σ, p), a, (σ', p'))"
    shows "P ((σ i, p), a, (σ' i, p'))"
  using assms unfolding seqll_def by simp

lemma seqllsimp:
  "seqll i P ((σ, p), a, (σ', p')) = P ((σ i, p), a, (σ' i, p'))"
  unfolding seqll_def by simp

lemma seqll_onll_swap:
  "seqll i (onll Γ P) = onll Γ (seqll i P)"
  unfolding seqll_def onll_def by simp

theorem open_seq_step_invariant [intro]:
  assumes "A ⊫⇩A (I →) P"
      and "initiali i (init OA) (init A)"
      and spo: "trans OA = oseqp_sos Γ i"
      and sp: "trans A = seqp_sos Γ"
    shows "OA ⊨⇩A (act I, other ANY {i} →) (seqll i P)"
  proof -
    have "OA ⊫⇩A (I →) (seqll i P)"
    proof (rule step_invariant_arbitraryI)
      fix σ p a σ' p'
      assume or: "(σ, p) ∈ reachable OA I"
         and otr: "((σ, p), a, (σ', p')) ∈ trans OA"
         and "I a"
      from or ‹initiali i (init OA) (init A)› spo sp obtain ξ where "σ i = ξ"
                                                             and cr: "(ξ, p) ∈ reachable A I"
        by - (drule(3) reachable_oseq_seqp_sos', auto)
      from otr and spo have "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i" by simp
      with ‹σ i = ξ› obtain ξ' where "σ' i = ξ'"
                                 and ctr: "((ξ, p), a, (ξ', p')) ∈ seqp_sos Γ"
        by (auto dest!: oseq_step_is_seq_step)
      with sp have "((ξ, p), a, (ξ', p')) ∈ trans A" by simp
      with ‹A ⊫⇩A (I →) P› cr have "P ((ξ, p), a, (ξ', p'))" using ‹I a› ..
      with ‹σ i = ξ› and ‹σ' i = ξ'› have "P ((σ i, p), a, (σ' i, p'))" by simp
      thus "seqll i P ((σ, p), a, (σ', p'))" ..
    qed
    moreover from spo have "local_steps (trans OA) {i}" by simp
    moreover have "other_steps (other ANY {i}) {i}" ..
    ultimately show ?thesis
    proof (rule open_closed_step_invariant)
      fix σ ζ a σ' ζ' s s'
      assume "∀j∈{i}. σ j = ζ j"
         and "∀j∈{i}. σ' j = ζ' j"
         and "seqll i P ((σ, s), a, (σ', s'))"
        thus "seqll i P ((ζ, s), a, (ζ', s'))" ..
    qed
  qed

end