Theory A_Quality_Increases

(*  Title:       variants/a_norreqid/Quality_Increases.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
    Author:      Peter Höfner, NICTA
*)

section "The quality increases predicate"

theory A_Quality_Increases
imports A_Aodv_Predicates A_Fresher
begin

definition quality_increases :: "state  state  bool"
where "quality_increases ξ ξ'  (dipkD(rt ξ). dip  kD(rt ξ')  rt ξ ⊑⇘diprt ξ')
                                                (dip. sqn (rt ξ) dip  sqn (rt ξ') dip)"

lemma quality_increasesI [intro!]:
  assumes "dip. dip  kD(rt ξ)  dip  kD(rt ξ')"
      and "dip.  dip  kD(rt ξ); dip  kD(rt ξ')   rt ξ ⊑⇘diprt ξ'"          
      and "dip. sqn (rt ξ) dip  sqn (rt ξ') dip"
    shows "quality_increases ξ ξ'"
  unfolding quality_increases_def using assms by clarsimp

lemma quality_increasesE [elim]:
    fixes dip
  assumes "quality_increases ξ ξ'"
      and "dipkD(rt ξ)"
      and " dip  kD(rt ξ'); rt ξ ⊑⇘diprt ξ'; sqn (rt ξ) dip  sqn (rt ξ') dip   R dip ξ ξ'"
    shows "R dip ξ ξ'"
  using assms unfolding quality_increases_def by clarsimp

lemma quality_increases_rt_fresherD [dest]:
    fixes ip
  assumes "quality_increases ξ ξ'"
      and "ipkD(rt ξ)"
    shows "rt ξ ⊑⇘iprt ξ'"
  using assms by auto

lemma quality_increases_sqnE [elim]:
    fixes dip
  assumes "quality_increases ξ ξ'"
      and "sqn (rt ξ) dip  sqn (rt ξ') dip  R dip ξ ξ'"
    shows "R dip ξ ξ'"
  using assms unfolding quality_increases_def by clarsimp

lemma quality_increases_refl [intro, simp]: "quality_increases ξ ξ"
  by rule simp_all

lemma strictly_fresher_quality_increases_right [elim]:
    fixes σ σ' dip
  assumes "rt (σ i) ⊏⇘diprt (σ nhip)"                       
      and qinc: "quality_increases (σ nhip) (σ' nhip)"
      and "dipkD(rt (σ nhip))"
    shows "rt (σ i) ⊏⇘diprt (σ' nhip)"
  proof -
    from qinc have "rt (σ nhip) ⊑⇘diprt (σ' nhip)" using dipkD(rt (σ nhip))
      by auto
    with rt (σ i) ⊏⇘diprt (σ nhip) show ?thesis ..
  qed

lemma kD_quality_increases [elim]:
  assumes "ikD(rt ξ)"
      and "quality_increases ξ ξ'"
    shows "ikD(rt ξ')"
  using assms by auto

lemma kD_nsqn_quality_increases [elim]:
  assumes "ikD(rt ξ)"
      and "quality_increases ξ ξ'"
    shows "ikD(rt ξ')  nsqn (rt ξ) i  nsqn (rt ξ') i"
  proof -
    from assms have "ikD(rt ξ')" ..
    moreover with assms have "rt ξ ⊑⇘irt ξ'" by auto
    ultimately have "nsqn (rt ξ) i  nsqn (rt ξ') i"
      using ikD(rt ξ) by - (erule(2) rt_fresher_imp_nsqn_le)
    with ikD(rt ξ') show ?thesis ..
  qed

lemma nsqn_quality_increases [elim]:
  assumes "ikD(rt ξ)"
      and "quality_increases ξ ξ'"
    shows "nsqn (rt ξ) i  nsqn (rt ξ') i"
  using assms by (rule kD_nsqn_quality_increases [THEN conjunct2])

lemma kD_nsqn_quality_increases_trans [elim]:
  assumes "ikD(rt ξ)"
      and "s  nsqn (rt ξ) i"
      and "quality_increases ξ ξ'"
    shows "ikD(rt ξ')  s  nsqn (rt ξ') i"
  proof
    from ikD(rt ξ) and quality_increases ξ ξ' show "ikD(rt ξ')" ..
  next
    from ikD(rt ξ) and quality_increases ξ ξ' have "nsqn (rt ξ) i  nsqn (rt ξ') i" ..
    with s  nsqn (rt ξ) i show "s  nsqn (rt ξ') i" by (rule le_trans)
  qed

lemma nsqn_quality_increases_nsqn_lt_lt [elim]:
  assumes "ikD(rt ξ)"
      and "quality_increases ξ ξ'"
     and "s < nsqn (rt ξ) i"
    shows "s < nsqn (rt ξ') i"
  proof -
    from assms(1-2) have "nsqn (rt ξ) i  nsqn (rt ξ') i" ..
    with s < nsqn (rt ξ) i show "s < nsqn (rt ξ') i" by simp
  qed

lemma nsqn_quality_increases_dhops [elim]:
  assumes "ikD(rt ξ)"
      and "quality_increases ξ ξ'"
      and "nsqn (rt ξ) i = nsqn (rt ξ') i"
    shows "the (dhops (rt ξ) i)  the (dhops (rt ξ') i)"
  using assms unfolding quality_increases_def
  by (clarsimp) (drule(1) bspec, clarsimp simp: rt_fresher_def2)

lemma nsqn_quality_increases_nsqn_eq_le [elim]:
  assumes "ikD(rt ξ)"
      and "quality_increases ξ ξ'"
      and "s = nsqn (rt ξ) i"
    shows "s < nsqn (rt ξ') i  (s = nsqn (rt ξ') i  the (dhops (rt ξ) i)  the (dhops (rt ξ') i))"
  using assms by (metis nat_less_le nsqn_quality_increases nsqn_quality_increases_dhops)

lemma quality_increases_rreq_rrep_props [elim]:
    fixes sn ip hops sip
  assumes qinc: "quality_increases (σ sip) (σ' sip)"
      and "1  sn"
      and *: "ipkD(rt (σ sip))  sn  nsqn (rt (σ sip)) ip
                                 (nsqn (rt (σ sip)) ip = sn
                                     (the (dhops (rt (σ sip)) ip)  hops
                                           the (flag (rt (σ sip)) ip) = inv))"
    shows "ipkD(rt (σ' sip))  sn  nsqn (rt (σ' sip)) ip
                               (nsqn (rt (σ' sip)) ip = sn
                                   (the (dhops (rt (σ' sip)) ip)  hops
                                         the (flag (rt (σ' sip)) ip) = inv))"
      (is "_  ?nsqnafter")
  proof -
    from *  obtain "ipkD(rt (σ sip))" and "sn  nsqn (rt (σ sip)) ip" by auto

    from quality_increases (σ sip) (σ' sip)
       have "sqn (rt (σ sip)) ip  sqn (rt (σ' sip)) ip" ..
    from quality_increases (σ sip) (σ' sip) and ipkD (rt (σ sip))
      have "ipkD (rt (σ' sip))" ..

    from sn  nsqn (rt (σ sip)) ip have ?nsqnafter
    proof
      assume "sn < nsqn (rt (σ sip)) ip"
      also from ipkD(rt (σ sip)) and quality_increases (σ sip) (σ' sip)
        have "...  nsqn (rt (σ' sip)) ip" ..
      finally have "sn < nsqn (rt (σ' sip)) ip" .
      thus ?thesis by simp
    next
      assume "sn = nsqn (rt (σ sip)) ip"
      with ipkD(rt (σ sip)) and quality_increases (σ sip) (σ' sip)
        have "sn < nsqn (rt (σ' sip)) ip
               (sn = nsqn (rt (σ' sip)) ip
                  the (dhops (rt (σ' sip)) ip)  the (dhops (rt (σ sip)) ip))" ..
      hence "sn < nsqn (rt (σ' sip)) ip
               (nsqn (rt (σ' sip)) ip = sn  (the (dhops (rt (σ' sip)) ip)  hops
                                                  the (flag (rt (σ' sip)) ip) = inv))"
      proof
        assume "sn < nsqn (rt (σ' sip)) ip" thus ?thesis ..
      next
        assume "sn = nsqn (rt (σ' sip)) ip
                 the (dhops (rt (σ sip)) ip)  the (dhops (rt (σ' sip)) ip)"
        hence "sn = nsqn (rt (σ' sip)) ip"
          and "the (dhops (rt (σ' sip)) ip)  the (dhops (rt (σ sip)) ip)" by auto

        from * and sn = nsqn (rt (σ sip)) ip have "the (dhops (rt (σ sip)) ip)  hops
                                                        the (flag (rt (σ sip)) ip) = inv"
          by simp
        thus ?thesis
        proof
          assume "the (dhops (rt (σ sip)) ip)  hops"
          with  the (dhops (rt (σ' sip)) ip)  the (dhops (rt (σ sip)) ip)
           have "the (dhops (rt (σ' sip)) ip)  hops" by simp
          with sn = nsqn (rt (σ' sip)) ip show ?thesis by simp
        next
          assume "the (flag (rt (σ sip)) ip) = inv"
          with ipkD(rt (σ sip)) have "nsqn (rt (σ sip)) ip = sqn (rt (σ sip)) ip - 1" ..

          with sn  1 and sn = nsqn (rt (σ sip)) ip
            have "sqn (rt (σ sip)) ip > 1" by simp

          from ipkD(rt (σ' sip)) show ?thesis
          proof (rule vD_or_iD)
            assume "ipiD(rt (σ' sip))"
            hence "the (flag (rt (σ' sip)) ip) = inv" ..
            with sn = nsqn (rt (σ' sip)) ip show ?thesis
              by simp
          next
            (* the tricky case: sn = nsqn (rt (σ' sip)) ip
                                ∧ ip∈iD(rt (σ sip))
                                ∧ ip∈vD(rt (σ' sip)) *)
            assume "ipvD(rt (σ' sip))"
            hence "nsqn (rt (σ' sip)) ip = sqn (rt (σ' sip)) ip" ..
            with sqn (rt (σ sip)) ip  sqn (rt (σ' sip)) ip
              have "nsqn (rt (σ' sip)) ip  sqn (rt (σ sip)) ip" by simp

            with sqn (rt (σ sip)) ip > 1
              have "nsqn (rt (σ' sip)) ip > sqn (rt (σ sip)) ip - 1" by simp
            with nsqn (rt (σ sip)) ip = sqn (rt (σ sip)) ip - 1
              have "nsqn (rt (σ' sip)) ip > nsqn (rt (σ sip)) ip" by simp
            with sn = nsqn (rt (σ sip)) ip have "nsqn (rt (σ' sip)) ip > sn"
              by simp
            thus ?thesis ..
          qed
        qed
      qed
      thus ?thesis by (metis (mono_tags) le_cases not_le)
    qed
    with ipkD (rt (σ' sip)) show "ipkD (rt (σ' sip))  ?nsqnafter" ..
  qed

lemma quality_increases_rreq_rrep_props':
    fixes sn ip hops sip
  assumes "j. quality_increases (σ j) (σ' j)"
      and "1  sn"
      and *: "ipkD(rt (σ sip))  sn  nsqn (rt (σ sip)) ip
                                 (nsqn (rt (σ sip)) ip = sn
                                     (the (dhops (rt (σ sip)) ip)  hops
                                           the (flag (rt (σ sip)) ip) = inv))"
    shows "ipkD(rt (σ' sip))  sn  nsqn (rt (σ' sip)) ip
                               (nsqn (rt (σ' sip)) ip = sn
                                   (the (dhops (rt (σ' sip)) ip)  hops
                                         the (flag (rt (σ' sip)) ip) = inv))"
  proof -
    from assms(1) have "quality_increases (σ sip) (σ' sip)" ..
    thus ?thesis using assms(2-3) by (rule quality_increases_rreq_rrep_props)
  qed

lemma rteq_quality_increases:
  assumes "j. j  i  quality_increases (σ j) (σ' j)"
      and "rt (σ' i) = rt (σ i)"
    shows "j. quality_increases (σ j) (σ' j)"
  using assms by clarsimp (metis order_refl quality_increasesI rt_fresher_refl)

definition msg_fresh :: "(ip  state)  msg  bool"
where "msg_fresh σ m 
         case m of Rreq hopsc  _ _ _ oipc osnc sipc  osnc  1  (sipc  oipc 
                       oipckD(rt (σ sipc))  nsqn (rt (σ sipc)) oipc  osnc
                        (nsqn (rt (σ sipc)) oipc = osnc
                              (hopsc  the (dhops (rt (σ sipc)) oipc)
                                   the (flag (rt (σ sipc)) oipc) = inv)))
                   | Rrep hopsc dipc dsnc _ sipc  dsnc  1  (sipc  dipc 
                       dipckD(rt (σ sipc))  nsqn (rt (σ sipc)) dipc  dsnc
                        (nsqn (rt (σ sipc)) dipc = dsnc
                              (hopsc  the (dhops (rt (σ sipc)) dipc)
                                    the (flag (rt (σ sipc)) dipc) = inv)))
                   | Rerr destsc sipc  (ripcdom(destsc). (ripckD(rt (σ sipc))
                                          the (destsc ripc) - 1  nsqn (rt (σ sipc)) ripc))
                   | _  True"

lemma msg_fresh [simp]:
  "hops dip dsn dsk oip osn sip.
           msg_fresh σ (Rreq hops dip dsn dsk oip osn sip) =
                            (osn  1  (sip  oip  oipkD(rt (σ sip))
                                      nsqn (rt (σ sip)) oip  osn
                                      (nsqn (rt (σ sip)) oip = osn
                                            (hops  the (dhops (rt (σ sip)) oip)
                                                 the (flag (rt (σ sip)) oip) = inv))))"
  "hops dip dsn oip sip. msg_fresh σ (Rrep hops dip dsn oip sip) =
                            (dsn  1  (sip  dip  dipkD(rt (σ sip))
                                      nsqn (rt (σ sip)) dip  dsn
                                      (nsqn (rt (σ sip)) dip = dsn
                                            (hops  the (dhops (rt (σ sip)) dip))
                                                  the (flag (rt (σ sip)) dip) = inv)))"
  "dests sip.            msg_fresh σ (Rerr dests sip) =
                            (ripcdom(dests). (ripckD(rt (σ sip))
                                      the (dests ripc) - 1  nsqn (rt (σ sip)) ripc))"
  "d dip.                msg_fresh σ (Newpkt d dip)   = True"
  "d dip sip.            msg_fresh σ (Pkt d dip sip)  = True"
  unfolding msg_fresh_def by simp_all

lemma msg_fresh_inc_sn [simp, elim]:
  "msg_fresh σ m  rreq_rrep_sn m"
  by (cases m) simp_all

lemma recv_msg_fresh_inc_sn [simp, elim]:
  "orecvmsg (msg_fresh) σ m  recvmsg rreq_rrep_sn m"
  by (cases m) simp_all

lemma rreq_nsqn_is_fresh [simp]:
  fixes σ msg hops dip dsn dsk oip osn sip
  assumes "rreq_rrep_fresh (rt (σ sip)) (Rreq hops dip dsn dsk oip osn sip)"
      and "rreq_rrep_sn (Rreq hops  dip dsn dsk oip osn sip)"
  shows "msg_fresh σ (Rreq hops  dip dsn dsk oip osn sip)"
        (is "msg_fresh σ ?msg")
  proof -
    let ?rt = "rt (σ sip)"
    from assms(2) have "1  osn" by simp
    thus ?thesis
    unfolding msg_fresh_def
    proof (simp only: msg.case, intro conjI impI)
      assume "sip  oip"
      with assms(1) show "oip  kD(?rt)" by simp
    next
      assume "sip  oip"
         and "nsqn ?rt oip = osn"
      show "the (dhops ?rt oip)  hops  the (flag ?rt oip) = inv"
      proof (cases "oipvD(?rt)")
        assume "oipvD(?rt)"
        hence "nsqn ?rt oip = sqn ?rt oip" ..
        with nsqn ?rt oip = osn have "sqn ?rt oip = osn" by simp
        with assms(1) and sip  oip have "the (dhops ?rt oip)  hops"
          by simp
        thus ?thesis ..
      next
        assume "oipvD(?rt)"
        moreover from assms(1) and sip  oip have "oipkD(?rt)" by simp
        ultimately have "oipiD(?rt)" by auto
        hence "the (flag ?rt oip) = inv" ..
        thus ?thesis ..
      qed
    next
      assume "sip  oip"
      with assms(1) have "osn  sqn ?rt oip" by auto
      thus "osn  nsqn (rt (σ sip)) oip"
      proof (rule nat_le_eq_or_lt)
        assume "osn < sqn ?rt oip"
        hence "osn  sqn ?rt oip - 1" by simp
        also have "...  nsqn ?rt oip" by (rule sqn_nsqn)
        finally show "osn  nsqn ?rt oip" .
      next
        assume "osn = sqn ?rt oip"
        with assms(1) and sip  oip have "oipkD(?rt)"
                                       and "the (flag ?rt oip) = val"
          by auto
        hence "nsqn ?rt oip = sqn ?rt oip" ..
        with osn = sqn ?rt oip have "nsqn ?rt oip = osn" by simp
        thus "osn  nsqn ?rt oip" by simp
      qed
    qed simp
  qed

lemma rrep_nsqn_is_fresh [simp]:
  fixes σ msg hops dip dsn oip sip
  assumes "rreq_rrep_fresh (rt (σ sip)) (Rrep hops dip dsn oip sip)"
      and "rreq_rrep_sn (Rrep hops dip dsn oip sip)"
  shows "msg_fresh σ (Rrep hops dip dsn oip sip)"
        (is "msg_fresh σ ?msg")
  proof -
    let ?rt = "rt (σ sip)"
    from assms have "sip  dip  dipkD(?rt)  sqn ?rt dip = dsn  the (flag ?rt dip) = val"
      by simp
    hence "sip  dip  dipkD(?rt)  nsqn ?rt dip  dsn"
    by clarsimp
    with assms show "msg_fresh σ ?msg"
      by clarsimp
  qed

lemma rerr_nsqn_is_fresh [simp]:
  fixes σ msg dests sip
  assumes "rerr_invalid (rt (σ sip)) (Rerr dests sip)"
  shows "msg_fresh σ (Rerr dests sip)"
        (is "msg_fresh σ ?msg")
  proof -
    let ?rt = "rt (σ sip)"
    from assms have *: "(ripdom(dests). (ripiD(rt (σ sip))
                                      the (dests rip) = sqn (rt (σ sip)) rip))"
      by clarsimp
    have "(ripdom(dests). (ripkD(rt (σ sip))
                                      the (dests rip) - 1  nsqn (rt (σ sip)) rip))"
    proof
      fix rip
      assume "rip  dom dests"
      with * have "ripiD(rt (σ sip))" and "the (dests rip) = sqn (rt (σ sip)) rip"
        by auto

      from this(2) have "the (dests rip) - 1 = sqn (rt (σ sip)) rip - 1" by simp
      also have "...  nsqn (rt (σ sip)) rip" by (rule sqn_nsqn)
      finally have "the (dests rip) - 1  nsqn (rt (σ sip)) rip" .

      with ripiD(rt (σ sip))
        show "ripkD(rt (σ sip))  the (dests rip) - 1  nsqn (rt (σ sip)) rip"
          by clarsimp
    qed
    thus "msg_fresh σ ?msg"
      by simp
  qed

lemma quality_increases_msg_fresh [elim]:
  assumes qinc: "j. quality_increases (σ j) (σ' j)"
      and "msg_fresh σ m"
    shows "msg_fresh σ' m"
  using assms(2)
  proof (cases m)
    fix hops rreqid dip dsn dsk oip osn sip
    assume [simp]: "m = Rreq hops  dip dsn dsk oip osn sip"
       and "msg_fresh σ m"
    then have "osn  1" and "sip = oip  (oipkD(rt (σ sip))  osn  nsqn (rt (σ sip)) oip
                                            (nsqn (rt (σ sip)) oip = osn
                                                  (the (dhops (rt (σ sip)) oip)  hops
                                                       the (flag (rt (σ sip)) oip) = inv)))"
      by auto
    from this(2) show ?thesis
    proof
      assume "sip = oip" with osn  1 show ?thesis by simp
    next
      assume "oipkD(rt (σ sip))  osn  nsqn (rt (σ sip)) oip
                                   (nsqn (rt (σ sip)) oip = osn
                                       (the (dhops (rt (σ sip)) oip)  hops
                                            the (flag (rt (σ sip)) oip) = inv))"
      moreover from qinc have "quality_increases (σ sip) (σ' sip)" ..
      ultimately have "oipkD(rt (σ' sip))  osn  nsqn (rt (σ' sip)) oip
                                            (nsqn (rt (σ' sip)) oip = osn
                                               (the (dhops (rt (σ' sip)) oip)  hops
                                                     the (flag (rt (σ' sip)) oip) = inv))"
       using osn  1 by (rule quality_increases_rreq_rrep_props [rotated 2])
      with osn  1 show "msg_fresh σ' m"
        by (clarsimp)
    qed
  next
    fix hops dip dsn oip sip
    assume [simp]: "m = Rrep hops dip dsn oip sip"
       and "msg_fresh σ m"
    then have "dsn  1" and "sip = dip  (dipkD(rt (σ sip))  dsn  nsqn (rt (σ sip)) dip
                                            (nsqn (rt (σ sip)) dip = dsn
                                                  (the (dhops (rt (σ sip)) dip)  hops
                                                       the (flag (rt (σ sip)) dip) = inv)))"
      by auto
    from this(2) show "?thesis"
    proof
      assume "sip = dip" with dsn  1 show ?thesis by simp
    next
      assume "dipkD(rt (σ sip))  dsn  nsqn (rt (σ sip)) dip
                                   (nsqn (rt (σ sip)) dip = dsn
                                       (the (dhops (rt (σ sip)) dip)  hops
                                            the (flag (rt (σ sip)) dip) = inv))"
      moreover from qinc have "quality_increases (σ sip) (σ' sip)" ..
      ultimately have "dipkD(rt (σ' sip))  dsn  nsqn (rt (σ' sip)) dip
                                            (nsqn (rt (σ' sip)) dip = dsn
                                               (the (dhops (rt (σ' sip)) dip)  hops
                                                     the (flag (rt (σ' sip)) dip) = inv))"
        using dsn  1 by (rule quality_increases_rreq_rrep_props [rotated 2])
      with dsn  1 show "msg_fresh σ' m"
        by clarsimp
    qed
  next
    fix dests sip
    assume [simp]: "m = Rerr dests sip"
       and "msg_fresh σ m"
    then have *: "ripdom(dests). ripkD(rt (σ sip))
                               the (dests rip) - 1  nsqn (rt (σ sip)) rip"
      by simp
    have "ripdom(dests). ripkD(rt (σ' sip))
                          the (dests rip) - 1  nsqn (rt (σ' sip)) rip"
      proof
        fix rip
        assume "ripdom(dests)"
        with * have "ripkD(rt (σ sip))" and "the (dests rip) - 1  nsqn (rt (σ sip)) rip"
          by - (drule(1) bspec, clarsimp)+
        moreover from qinc have "quality_increases (σ sip) (σ' sip)" by simp
        ultimately show "ripkD(rt (σ' sip))  the (dests rip) - 1  nsqn (rt (σ' sip)) rip" ..
      qed
    thus ?thesis by simp
  qed simp_all

end