Theory Qmsg_Lifting

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

section "Lifting rules for parallel compositions with QMSG"

theory Qmsg_Lifting
imports Qmsg OAWN_SOS Inv_Cterms OAWN_Invariants
begin

lemma oseq_no_change_on_send:
  fixes σ s a σ' s'
  assumes "((σ, s), a, (σ', s'))  oseqp_sos Γ i"
  shows "case a of
           broadcast m      σ' i = σ i
         | groupcast ips m  σ' i = σ i
         | unicast ips m    σ' i = σ i
         | ¬unicast ips     σ' i = σ i
         | send m           σ' i = σ i
         | deliver m        σ' i = σ i
         | _  True"
  using assms by induction simp_all

lemma qmsg_no_change_on_send_or_receive:
    fixes σ s a σ' s'
  assumes "((σ, s), a, (σ', s'))  oparp_sos i (oseqp_sos Γ i) (seqp_sos ΓQMSG)"
      and "a  τ"
    shows "σ' i = σ i"
  proof -
    from assms(1) obtain p q p' q'
      where "((σ, (p, q)), a, (σ', (p', q')))  oparp_sos i (oseqp_sos Γ i) (seqp_sos ΓQMSG)"
      by (cases s, cases s', simp)
    thus ?thesis
    proof
      assume "((σ, p), a, (σ', p'))  oseqp_sos Γ i"
         and "m. a  receive m"
      with a  τ show "σ' i = σ i"
        by - (drule oseq_no_change_on_send, cases a, auto)
    next
      assume "(q, a, q')  seqp_sos ΓQMSG"
         and "σ' i = σ i"
        thus "σ' i = σ i" by simp
    next
      assume "a = τ" with a  τ show ?thesis by auto
    qed
  qed

lemma qmsg_msgs_not_empty:
  "qmsg  onl ΓQMSG (λ(msgs, l). l = ()-:1  msgs  [])"
  by inv_cterms

lemma qmsg_send_from_queue:
  "qmsg A (λ((msgs, q), a, _). sendmsg (λm. mset msgs) a)"
  proof -
    have "qmsg A onll ΓQMSG (λ((msgs, _), a, _). sendmsg (λm. mset msgs) a)"
      by (inv_cterms inv add: onl_invariant_sterms [OF qmsg_wf qmsg_msgs_not_empty])
    thus ?thesis
      by (rule step_invariant_weakenE) (auto dest!: onllD)
  qed

lemma qmsg_queue_contents:
  "qmsg A (λ((msgs, q), a, (msgs', q')). case a of
                                             receive m  set msgs'  set (msgs @ [m])
                                           | _  set msgs'  set msgs)"
  proof -
    have "qmsg A onll ΓQMSG (λ((msgs, q), a, (msgs', q')).
                                     case a of
                                       receive m  set msgs'  set (msgs @ [m])
                                     | _  set msgs'  set msgs)"
      by (inv_cterms) (clarsimp simp add: in_set_tl)+
    thus ?thesis
      by (rule step_invariant_weakenE) (auto dest!: onllD)
  qed

lemma qmsg_send_receive_or_tau:
  "qmsg A (λ(_, a, _). m. a = send m  a = receive m  a = τ)"
  proof -
   have "qmsg A onll ΓQMSG (λ(_, a, _). m. a = send m  a = receive m  a = τ)"
     by inv_cterms
   thus ?thesis
    by rule (auto dest!: onllD)
  qed

lemma par_qmsg_oreachable:
  assumes "(σ, ζ)  oreachable (A ⟨⟨⇘iqmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
           (is "_  oreachable _ ?owS _")
      and pinv: "A A (otherwith S {i} (orecvmsg R), other U {i} →)
                       globala (λ(σ, _, σ'). U (σ i) (σ' i))"
      and ustutter: "ξ. U ξ ξ"
      and sgivesu: "ξ ξ'. S ξ ξ'  U ξ ξ'"
      and upreservesq: "σ σ' m.  j. U (σ j) (σ' j); R σ m   R σ' m"
  shows "(σ, fst ζ)  oreachable A ?owS (other U {i})
          snd ζ  reachable qmsg (recvmsg (R σ))
          (mset (fst (snd ζ)). R σ m)"
  using assms(1) proof (induction rule: oreachable_pair_induct)
    fix σ pq
    assume "(σ, pq)  init (A ⟨⟨⇘iqmsg)"
    then obtain p ms q where "pq = (p, (ms, q))"
                         and "(σ, p)  init A"
                         and "(ms, q)  init qmsg"
      by (clarsimp simp del: ΓQMSG_simps)
    from this(2) have "(σ, p)  oreachable A ?owS (other U {i})" ..
    moreover from (ms, q)  init qmsg have "(ms, q)  reachable qmsg (recvmsg (R σ))" ..
    moreover from (ms, q)  init qmsg have "ms = []"
        unfolding σQMSG_def by simp
    ultimately show "(σ, fst pq)  oreachable A ?owS (other U {i})
                      snd pq  reachable qmsg (recvmsg (R σ))
                      (mset (fst (snd pq)). R σ m)"
      using pq = (p, (ms, q)) by simp
  next
    note ΓQMSG_simps [simp del]
    case (other σ pq σ')
    hence "(σ, fst pq)  oreachable A ?owS (other U {i})"
      and "other U {i} σ σ'"
      and qr: "snd pq  reachable qmsg (recvmsg (R σ))"
      and "mset (fst (snd pq)). R σ m"
      by simp_all
    from other U {i} σ σ' and ustutter have "j. U (σ j) (σ' j)"
        by (clarsimp elim!: otherE) metis
    from other U {i} σ σ'
     and (σ, fst pq)  oreachable A ?owS (other U {i})
      have "(σ', fst pq)  oreachable A ?owS (other U {i})"
        by - (rule oreachable_other')
    moreover have "mset (fst (snd pq)). R σ' m"
    proof
      fix m assume "m  set (fst (snd pq))"
      with mset (fst (snd pq)). R σ m have "R σ m" ..
      with j. U (σ j) (σ' j) show "R σ' m" by (rule upreservesq)
    qed
    moreover from qr have "snd pq  reachable qmsg (recvmsg (R σ'))"
    proof
      fix a
      assume "recvmsg (R σ) a"
      thus "recvmsg (R σ') a"
      proof (rule recvmsgE [where R=R])
        fix m assume "R σ m"
        with j. U (σ j) (σ' j) show "R σ' m" by (rule upreservesq)
      qed
    qed
    ultimately show ?case using qr by simp
  next
    case (local σ pq σ' pq' a)
    obtain p ms q p' ms' q' where "pq = (p, (ms, q))"
                              and "pq' = (p', (ms', q'))"
      by (cases pq, cases pq') metis
    with local.hyps local.IH
      have pqtr: "((σ, (p, (ms, q))), a, (σ', (p', (ms', q'))))
                     oparp_sos i (trans A) (seqp_sos ΓQMSG)"
        and por: "(σ, p)  oreachable A ?owS (other U {i})"
        and qr: "(ms, q)  reachable qmsg (recvmsg (R σ))"
        and "mset ms. R σ m"
        and "?owS σ σ' a"
      by (simp_all del: ΓQMSG_simps)

    from ?owS σ σ' a have "j. ji  S (σ j) (σ' j)"
      by (clarsimp dest!: otherwith_syncD)
    with sgivesu have "j. ji  U (σ j) (σ' j)" by simp

    from ?owS σ σ' a have "orecvmsg R σ a" by (rule otherwithE)
    hence "recvmsg (R σ) a" ..

    from pqtr have "(σ', p')  oreachable A ?owS (other U {i})
                   (ms', q')  reachable qmsg (recvmsg (R σ'))
                   (mset ms'. R σ' m)"
    proof
      assume "((σ, p), a, (σ', p'))  trans A"
         and "m. a  receive m"
         and "(ms', q') = (ms, q)"
      from this(1) have ptr: "((σ, p), a, (σ', p'))  trans A" by simp
      with pinv por and ?owS σ σ' a have "U (σ i) (σ' i)"
        by (auto dest!: ostep_invariantD)
      with j. ji  U (σ j) (σ' j) have "j. U (σ j) (σ' j)" by auto

      hence recvmsg': "a. recvmsg (R σ) a  recvmsg (R σ') a"
        by (auto elim!: recvmsgE [where R=R] upreservesq)

      from por ptr ?owS σ σ' a have "(σ', p')  oreachable A ?owS (other U {i})"
        by - (rule oreachable_local')

      moreover have "(ms', q')  reachable qmsg (recvmsg (R σ'))"
      proof -
        from qr and (ms', q') = (ms, q)
          have "(ms', q')  reachable qmsg (recvmsg (R σ))" by simp
        thus ?thesis by (rule reachable_weakenE) (erule recvmsg')
      qed

      moreover have "mset ms'. R σ' m"
      proof
        fix m
        assume "mset ms'"
        with (ms', q') = (ms, q) have "mset ms" by simp
        with mset ms. R σ m have "R σ m" ..
        with j. U (σ j) (σ' j) show "R σ' m"
          by (rule upreservesq)
      qed

      ultimately show
        "(σ', p')  oreachable A ?owS (other U {i})
           (ms', q')  reachable qmsg (recvmsg (R σ'))
           (mset ms'. R σ' m)" by simp_all
    next
      assume qtr: "((ms, q), a, (ms', q'))  seqp_sos ΓQMSG"
         and "m. a  send m"
         and "p' = p"
         and "σ' i = σ i"

      from this(4) and ξ. U ξ ξ have "U (σ i) (σ' i)" by simp
      with j. ji  U (σ j) (σ' j) have "j. U (σ j) (σ' j)" by auto

      hence recvmsg': "a. recvmsg (R σ) a  recvmsg (R σ') a"
        by (auto elim!: recvmsgE [where R=R] upreservesq)

      from qtr have tqtr: "((ms, q), a, (ms', q'))  trans qmsg" by simp

      from j. U (σ j) (σ' j) and  σ' i = σ i have "other U {i} σ σ'" by auto
      with por and p' = p
        have "(σ', p')  oreachable A ?owS (other U {i})"
          by (auto dest: oreachable_other)

      moreover have "(ms', q')  reachable qmsg (recvmsg (R σ'))"
      proof (rule reachable_weakenE [where P="recvmsg (R σ)"])
        from qr tqtr recvmsg (R σ) a show "(ms', q')  reachable qmsg (recvmsg (R σ))" ..
      qed (rule recvmsg')

      moreover have "mset ms'. R σ' m"
      proof
        fix m
        assume "m  set ms'"
        moreover have "case a of receive m  set ms'  set (ms @ [m]) | _  set ms'  set ms"
          proof -
            from qr have "(ms, q)  reachable qmsg TT" ..
            thus ?thesis using tqtr
              by (auto dest!: step_invariantD [OF qmsg_queue_contents])
          qed
        ultimately have "R σ m" using mset ms. R σ m and orecvmsg R σ a 
          by (cases a) auto
        with j. U (σ j) (σ' j) show "R σ' m"
          by (rule upreservesq)
      qed

      ultimately show "(σ', p')  oreachable A ?owS (other U {i})
                      (ms', q')  reachable qmsg (recvmsg (R σ'))
                      (mset ms'. R σ' m)" by simp
    next
      fix m
      assume "a = τ"
         and "((σ, p), receive m, (σ', p'))  trans A"
         and "((ms, q), send m, (ms', q'))  seqp_sos ΓQMSG"
      from this(2-3)
        have ptr: "((σ, p), receive m, (σ', p'))  trans A"
         and qtr: "((ms, q), send m, (ms', q'))  trans qmsg" by simp_all

      from qr have "(ms, q)  reachable qmsg TT" ..
      with qtr have "m  set ms"
        by (auto dest!: step_invariantD [OF qmsg_send_from_queue])
      with mset ms. R σ m have "R σ m" ..
      hence "orecvmsg R σ (receive m)" by simp

      with j. ji  S (σ j) (σ' j) have "?owS σ σ' (receive m)"
        by (auto intro!: otherwithI)
      with pinv por ptr have "U (σ i) (σ' i)"
        by (auto dest!: ostep_invariantD)
      with j. ji  U (σ j) (σ' j) have "j. U (σ j) (σ' j)" by auto
      hence recvmsg': "a. recvmsg (R σ) a  recvmsg (R σ') a"
        by (auto elim!: recvmsgE [where R=R] upreservesq)

      from por ptr have "(σ', p')  oreachable A ?owS (other U {i})"
        using ?owS σ σ' (receive m) by - (erule(1) oreachable_local, simp)

      moreover have "(ms', q')  reachable qmsg (recvmsg (R σ'))"
      proof (rule reachable_weakenE [where P="recvmsg (R σ)"])
        have "recvmsg (R σ) (send m)" by simp
        with qr qtr show "(ms', q')  reachable qmsg (recvmsg (R σ))" ..
      qed (rule recvmsg')

      moreover have "mset ms'. R σ' m"
      proof
        fix m
        assume "m  set ms'"
        moreover have "set ms'  set ms"
          proof -
            from qr have "(ms, q)  reachable qmsg TT" ..
            thus ?thesis using qtr
              by (auto dest!: step_invariantD [OF qmsg_queue_contents])
          qed
        ultimately have "R σ m" using mset ms. R σ m by auto
        with j. U (σ j) (σ' j) show "R σ' m"
          by (rule upreservesq)
      qed

      ultimately show "(σ', p')  oreachable A ?owS (other U {i})
                      (ms', q')  reachable qmsg (recvmsg (R σ'))
                      (mset ms'. R σ' m)" by simp
    qed
    with pq = (p, (ms, q)) and pq' = (p', (ms', q')) show ?case
      by (simp_all del: ΓQMSG_simps)
  qed

lemma par_qmsg_oreachable_statelessassm:
  assumes "(σ, ζ)  oreachable (A ⟨⟨⇘iqmsg)
                               (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})"
      and ustutter: "ξ. U ξ ξ"
  shows "(σ, fst ζ)  oreachable A (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})
          snd ζ  reachable qmsg (recvmsg R)
          (mset (fst (snd ζ)). R m)"
  proof -
    from assms(1)
      have "(σ, ζ)  oreachable (A ⟨⟨⇘iqmsg)
                                (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)))
                                (other (λ_ _. True) {i})" by auto
    moreover
      have "A A (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)),
                  other (λ_ _. True) {i} →) globala (λ(σ, _, σ'). True)"
        by auto
    ultimately
      obtain "(σ, fst ζ)  oreachable A
                           (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R))) (other (λ_ _. True) {i})"
         and  *: "snd ζ  reachable qmsg (recvmsg R)"
         and **: "(mset (fst (snd ζ)). R m)"
        by (auto dest!: par_qmsg_oreachable)
    from this(1)
      have "(σ, fst ζ)  oreachable A (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})"
        by rule auto
    thus ?thesis using * ** by simp
  qed

lemma lift_into_qmsg:
  assumes "A  (otherwith S {i} (orecvmsg R), other U {i} →) global P"
      and "ξ. U ξ ξ"
      and "ξ ξ'. S ξ ξ'  U ξ ξ'"
      and "σ σ' m.  j. U (σ j) (σ' j); R σ m   R σ' m"
      and "A A (otherwith S {i} (orecvmsg R), other U {i} →)
                 globala (λ(σ, _, σ'). U (σ i) (σ' i))"
    shows "A ⟨⟨⇘iqmsg  (otherwith S {i} (orecvmsg R), other U {i} →) global P"
  proof (rule oinvariant_oreachableI)
    fix σ ζ
    assume "(σ, ζ)  oreachable (A ⟨⟨⇘iqmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
    then obtain s where "(σ, s)  oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})"
      by (auto dest!: par_qmsg_oreachable [OF _ assms(5,2-4)])
    with assms(1) show "global P (σ, ζ)"
      by (auto dest: oinvariant_weakenD [OF assms(1)])
  qed

lemma lift_step_into_qmsg:
  assumes inv: "A A (otherwith S {i} (orecvmsg R), other U {i} →) globala P"
      and ustutter: "ξ. U ξ ξ"
      and sgivesu: "ξ ξ'. S ξ ξ'  U ξ ξ'"
      and upreservesq: "σ σ' m.  j. U (σ j) (σ' j); R σ m   R σ' m"
      and self_sync: "A A (otherwith S {i} (orecvmsg R), other U {i} →)
                            globala (λ(σ, _, σ'). U (σ i) (σ' i))"

      and recv_stutter:  "σ σ' m.  j. U (σ j) (σ' j); σ' i = σ i   P (σ, receive m, σ')"
      and receive_right: "σ σ' m.  P (σ, receive m, σ')  P (σ, τ, σ')"
    shows "A ⟨⟨⇘iqmsg A (otherwith S {i} (orecvmsg R), other U {i} →) globala P"
      (is "_ A (?owS, ?U →) _")
  proof (rule ostep_invariantI)
    fix σ ζ a σ' ζ'
    assume or: "(σ, ζ)  oreachable (A ⟨⟨⇘iqmsg) ?owS ?U"
       and otr: "((σ, ζ), a, (σ', ζ'))  trans (A ⟨⟨⇘iqmsg)"
       and "?owS σ σ' a"
    from this(2) have "((σ, ζ), a, (σ', ζ'))  oparp_sos i (trans A) (seqp_sos ΓQMSG)"
        by simp
    then obtain s msgs q s' msgs' q'
      where "ζ = (s, (msgs, q))" "ζ' = (s', (msgs', q'))"
        and "((σ, (s, (msgs, q))), a, (σ', (s', (msgs', q'))))
                oparp_sos i (trans A) (seqp_sos ΓQMSG)"
        by (metis prod_cases3)
    from this(1-2) and or
      obtain "(σ, s)  oreachable A ?owS ?U"
             "(msgs, q)  reachable qmsg (recvmsg (R σ))"
             "(mset msgs. R σ m)"
       by (auto dest: par_qmsg_oreachable [OF _ self_sync ustutter sgivesu]
                elim!: upreservesq)
    from otr ζ = (s, (msgs, q)) ζ' = (s', (msgs', q'))
      have "((σ, (s, (msgs, q))), a, (σ', (s', (msgs', q'))))
               oparp_sos i (trans A) (seqp_sos ΓQMSG)"
        by simp
    hence "globala P ((σ, s), a, (σ', s'))"
    proof
      assume "((σ, s), a, (σ', s'))  trans A"
      with (σ, s)  oreachable A ?owS ?U
        show "globala P ((σ, s), a, (σ', s'))"
          using ?owS σ σ' a by (rule ostep_invariantD [OF inv])
    next
      assume "((msgs, q), a, (msgs', q'))  seqp_sos ΓQMSG"
         and "m. a  send m"
         and "σ' i = σ i"
      from this(3) and ustutter have "U (σ i) (σ' i)" by simp
      with ?owS σ σ' a and sgivesu have "j. U (σ j) (σ' j)"
        by (clarsimp dest!: otherwith_syncD) metis
      moreover have "(m. a = receive m)  (a = τ)"
      proof -
        from (msgs, q)  reachable qmsg (recvmsg (R σ))
          have "(msgs, q)  reachable qmsg TT" ..
        moreover from ((msgs, q), a, (msgs', q'))  seqp_sos ΓQMSG
          have "((msgs, q), a, (msgs', q'))  trans qmsg" by simp
        ultimately show ?thesis
          using m. a  send m
          by (auto dest!: step_invariantD [OF qmsg_send_receive_or_tau])
      qed
      ultimately show "globala P ((σ, s), a, (σ', s'))"
        using σ' i = σ i
        by simp (metis receive_right recv_stutter step_seq_tau)
    next
      fix m
      assume "a = τ"
         and "((σ, s), receive m, (σ', s'))  trans A"
         and "((msgs, q), send m, (msgs', q'))  seqp_sos ΓQMSG"

      from (msgs, q)  reachable qmsg (recvmsg (R σ))
        have "(msgs, q)  reachable qmsg TT" ..
      moreover from ((msgs, q), send m, (msgs', q'))  seqp_sos ΓQMSG
        have "((msgs, q), send m, (msgs', q'))  trans qmsg" by simp
      ultimately have "mset msgs"
        by (auto dest!: step_invariantD [OF qmsg_send_from_queue])

      with mset msgs. R σ m have "R σ m" ..
      with ?owS σ σ' a have "?owS σ σ' (receive m)"
          by (auto dest!: otherwith_syncD)

      with ((σ, s), receive m, (σ', s'))  trans A
        have "globala P ((σ, s), receive m, (σ', s'))"
          using (σ, s)  oreachable A ?owS ?U
          by - (rule ostep_invariantD [OF inv])
      hence "P (σ, receive m, σ')" by simp
      hence "P (σ, τ, σ')" by (rule receive_right)
      with a = τ show "globala P ((σ, s), a, (σ', s'))" by simp
    qed
    with ζ = (s, (msgs, q)) and ζ' = (s', (msgs', q')) show "globala P ((σ, ζ), a, (σ', ζ'))"
      by simp
  qed

lemma lift_step_into_qmsg_statelessassm:
  assumes "A A (λσ _. orecvmsg (λ_. R) σ, other (λ_ _. True) {i} →) globala P"
      and "σ σ' m. σ' i = σ i  P (σ, receive m, σ')"
      and "σ σ' m. P (σ, receive m, σ')  P (σ, τ, σ')"
    shows "A ⟨⟨⇘iqmsg A (λσ _. orecvmsg (λ_. R) σ, other (λ_ _. True) {i} →) globala P"
  proof -
    from assms(1) have *: "A A (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)),
                                 other (λ_ _. True) {i} →) globala P"
      by rule auto
    hence "A ⟨⟨⇘iqmsg A
              (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)), other (λ_ _. True) {i} →) globala P"
      by (rule lift_step_into_qmsg)
         (auto elim!: assms(2-3) simp del: step_seq_tau)
    thus ?thesis by rule auto
  qed

end