Theory E_Global_Invariants

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

section "Global invariant proofs over sequential processes"

theory E_Global_Invariants
imports E_Seq_Invariants
        E_Aodv_Predicates
        E_Fresher
        E_Quality_Increases
        AWN.OAWN_Convert
        E_OAodv
begin

lemma other_quality_increases [elim]:
  assumes "other quality_increases I σ σ'"
    shows "j. quality_increases (σ j) (σ' j)"
  using assms by (rule, clarsimp) (metis quality_increases_refl)

lemma weaken_otherwith [elim]:
    fixes m
  assumes *: "otherwith P I (orecvmsg Q) σ σ' a"
      and weakenP: "σ m. P σ m  P' σ m"
      and weakenQ: "σ m. Q σ m  Q' σ m"
    shows "otherwith P' I (orecvmsg Q') σ σ' a"
  proof
    fix j
    assume "jI"
    with * have "P (σ j) (σ' j)" by auto
    thus "P' (σ j) (σ' j)" by (rule weakenP)
  next
    from * have "orecvmsg Q σ a" by auto
    thus "orecvmsg Q' σ a"
      by rule (erule weakenQ)
  qed

lemma oreceived_msg_inv:
  assumes other: "σ σ' m.  P σ m; other Q {i} σ σ'   P σ' m"
      and local: "σ m. P σ m  P (σ(i := σ imsg := m)) m"
    shows "opaodv i  (otherwith Q {i} (orecvmsg P), other Q {i} →)
                       onl ΓAODV (λ(σ, l). l  {PAodv-:1}  P σ (msg (σ i)))"
  proof (inv_cterms, intro impI)
    fix σ σ' l
    assume "l = PAodv-:1  P σ (msg (σ i))"
       and "l = PAodv-:1"
       and "other Q {i} σ σ'"
    from this(1-2) have "P σ (msg (σ i))" ..
    hence "P σ' (msg (σ i))" using other Q {i} σ σ'
      by (rule other)
    moreover from other Q {i} σ σ' have "σ' i = σ i" ..
    ultimately show "P σ' (msg (σ' i))" by simp
  next
    fix σ σ' msg
    assume "otherwith Q {i} (orecvmsg P) σ σ' (receive msg)"
       and "σ' i = σ imsg := msg"
    from this(1) have "P σ msg"
                 and "j. ji  Q (σ j) (σ' j)" by auto
    from this(1) have "P (σ(i := σ imsg := msg)) msg" by (rule local)
    thus "P σ' msg"
    proof (rule other)
      from σ' i = σ imsg := msg and j. ji  Q (σ j) (σ' j)
        show "other Q {i} (σ(i := σ imsg := msg)) σ'"
          by - (rule otherI, auto)
    qed
  qed

text ‹(Equivalent to) Proposition 7.27›

lemma local_quality_increases:
  "paodv i A (recvmsg rreq_rrep_sn →) onll ΓAODV (λ((ξ, _), _, (ξ', _)). quality_increases ξ ξ')"
  proof (rule step_invariantI)
    fix s a s'
    assume sr: "s  reachable (paodv i) (recvmsg rreq_rrep_sn)"
       and tr: "(s, a, s')  trans (paodv i)"
       and rm: "recvmsg rreq_rrep_sn a"
    from sr have srTT: "s  reachable (paodv i) TT" ..

    from route_tables_fresher sr tr rm
      have "onll ΓAODV (λ((ξ, _), _, (ξ', _)). dipkD (rt ξ). rt ξ ⊑⇘diprt ξ') (s, a, s')"
        by (rule step_invariantD)

    moreover from known_destinations_increase srTT tr TT_True
      have "onll ΓAODV (λ((ξ, _), _, (ξ', _)). kD (rt ξ)  kD (rt ξ')) (s, a, s')"
        by (rule step_invariantD)

    moreover from sqns_increase srTT tr TT_True
      have "onll ΓAODV (λ((ξ, _), _, (ξ', _)). ip. sqn (rt ξ) ip  sqn (rt ξ') ip) (s, a, s')"
        by (rule step_invariantD)

     ultimately show "onll ΓAODV (λ((ξ, _), _, (ξ', _)). quality_increases ξ ξ') (s, a, s')"
       unfolding onll_def by auto
  qed

lemmas olocal_quality_increases =
   open_seq_step_invariant [OF local_quality_increases initiali_aodv oaodv_trans aodv_trans,
                            simplified seqll_onll_swap]

lemma oquality_increases:
  "opaodv i A (otherwith quality_increases {i} (orecvmsg (λ_. rreq_rrep_sn)),
                other quality_increases {i} →)
                onll ΓAODV (λ((σ, _), _, (σ', _)). j. quality_increases (σ j) (σ' j))"
  (is "_ A (?S, _ →) _")
  proof (rule onll_ostep_invariantI, simp)
    fix σ p l a σ' p' l'
    assume or: "(σ, p)  oreachable (opaodv i) ?S (other quality_increases {i})"
       and ll: "l  labels ΓAODV p"
       and "?S σ σ' a"
       and tr: "((σ, p), a, (σ', p'))  oseqp_sos ΓAODV i"
       and ll': "l'  labels ΓAODV p'"
    from this(1-3) have "orecvmsg (λ_. rreq_rrep_sn) σ a"
      by (auto dest!: oreachable_weakenE [where QS="act (recvmsg rreq_rrep_sn)"
                                            and QU="other quality_increases {i}"]
                      otherwith_actionD)
    with or have orw: "(σ, p)  oreachable (opaodv i) (act (recvmsg rreq_rrep_sn))
                                                      (other quality_increases {i})"
      by - (erule oreachable_weakenE, auto)
    with tr ll ll' and orecvmsg (λ_. rreq_rrep_sn) σ a have "quality_increases (σ i) (σ' i)"
      by - (drule onll_ostep_invariantD [OF olocal_quality_increases], auto simp: seqll_def)
    with ?S σ σ' a show "j. quality_increases (σ j) (σ' j)"
      by (auto dest!: otherwith_syncD)
  qed

lemma rreq_rrep_nsqn_fresh_any_step_invariant:
  "opaodv i A (act (recvmsg rreq_rrep_sn), other A {i} →)
                onll ΓAODV (λ((σ, _), a, _). anycast (msg_fresh σ) a)"
  proof (rule ostep_invariantI, simp del: act_simp)
    fix σ p a σ' p'
    assume or: "(σ, p)  oreachable (opaodv i) (act (recvmsg rreq_rrep_sn)) (other A {i})"
       and "((σ, p), a, (σ', p'))  oseqp_sos ΓAODV i"
       and recv: "act (recvmsg rreq_rrep_sn) σ σ' a"
    obtain l l' where "llabels ΓAODV p" and "l'labels ΓAODV p'"
      by (metis aodv_ex_label)
    from ((σ, p), a, (σ', p'))  oseqp_sos ΓAODV i
      have tr: "((σ, p), a, (σ', p'))  trans (opaodv i)" by simp

    have "anycast (rreq_rrep_fresh (rt (σ i))) a"
    proof -
      have "opaodv i A (act (recvmsg rreq_rrep_sn), other A {i} →)
                           onll ΓAODV (seqll i (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a))"
        by (rule ostep_invariant_weakenE [OF
              open_seq_step_invariant [OF rreq_rrep_fresh_any_step_invariant initiali_aodv,
                                       simplified seqll_onll_swap]]) auto
      hence "onll ΓAODV (seqll i (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a))
                                                                     ((σ, p), a, (σ', p'))"
        using or tr recv by - (erule(4) ostep_invariantE)
      thus ?thesis
        using llabels ΓAODV p and l'labels ΓAODV p' by auto
    qed

    moreover have "anycast (rerr_invalid (rt (σ i))) a"
    proof -
      have "opaodv i A (act (recvmsg rreq_rrep_sn), other A {i} →)
                           onll ΓAODV (seqll i (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a))"
        by (rule ostep_invariant_weakenE [OF
              open_seq_step_invariant [OF rerr_invalid_any_step_invariant initiali_aodv,
                                       simplified seqll_onll_swap]]) auto
      hence "onll ΓAODV (seqll i (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a))
                                                                     ((σ, p), a, (σ', p'))"
        using or tr recv by - (erule(4) ostep_invariantE)
      thus ?thesis
        using llabels ΓAODV p and l'labels ΓAODV p' by auto
    qed

    moreover have "anycast rreq_rrep_sn a"
    proof -
      from or tr recv
        have "onll ΓAODV (seqll i (λ(_, a, _). anycast rreq_rrep_sn a)) ((σ, p), a, (σ', p'))"
          by (rule ostep_invariantE [OF
                open_seq_step_invariant [OF rreq_rrep_sn_any_step_invariant initiali_aodv
                                            oaodv_trans aodv_trans,
                                         simplified seqll_onll_swap]])
      thus ?thesis
        using llabels ΓAODV p and l'labels ΓAODV p' by auto
    qed

    moreover have "anycast (λm. not_Pkt m  msg_sender m = i) a"
      proof -
        have "opaodv i A (act (recvmsg rreq_rrep_sn), other A {i} →)
               onll ΓAODV (seqll i (λ((ξ, _), a, _). anycast (λm. not_Pkt m  msg_sender m = i) a))"
          by (rule ostep_invariant_weakenE [OF
                open_seq_step_invariant [OF sender_ip_valid initiali_aodv,
                                         simplified seqll_onll_swap]]) auto
        thus ?thesis using or tr recv llabels ΓAODV p and l'labels ΓAODV p'
          by - (drule(3) onll_ostep_invariantD, auto)
      qed

    ultimately have "anycast (msg_fresh σ) a"
      by (simp_all add: anycast_def
                   del: msg_fresh
                   split: seq_action.split_asm msg.split_asm) simp_all
    thus "onll ΓAODV (λ((σ, _), a, _). anycast (msg_fresh σ) a) ((σ, p), a, (σ', p'))"
      by auto
  qed

lemma oreceived_rreq_rrep_nsqn_fresh_inv:
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
               onl ΓAODV (λ(σ, l). l  {PAodv-:1}  msg_fresh σ (msg (σ i)))"
  proof (rule oreceived_msg_inv)
    fix σ σ' m
    assume *: "msg_fresh σ m"
       and "other quality_increases {i} σ σ'"
    from this(2) have "j. quality_increases (σ j) (σ' j)" ..
    thus "msg_fresh σ' m" using * ..
  next
    fix σ m
    assume "msg_fresh σ m"
    thus "msg_fresh (σ(i := σ imsg := m)) m"
    proof (cases m)
      fix dests sip
      assume "m = Rerr dests sip"
      with msg_fresh σ m show ?thesis by auto
    qed auto
  qed

lemma oquality_increases_nsqn_fresh:
  "opaodv i A (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
                onll ΓAODV (λ((σ, _), _, (σ', _)). j. quality_increases (σ j) (σ' j))"
  by (rule ostep_invariant_weakenE [OF oquality_increases]) auto

lemma oosn_rreq:
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
       onl ΓAODV (seql i (λ(ξ, l). l  {PAodv-:4, PAodv-:5}  {PRreq-:n |n. True}  1  osn ξ))"
  by (rule oinvariant_weakenE [OF open_seq_invariant [OF osn_rreq initiali_aodv]])
     (auto simp: seql_onl_swap)

lemma rreq_sip:
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
               onl ΓAODV (λ(σ, l).
                   (l  {PAodv-:4, PAodv-:5, PRreq-:0, PRreq-:2}  sip (σ i)  oip (σ i))
                     oip (σ i)  kD(rt (σ (sip (σ i))))
                         nsqn (rt (σ (sip (σ i)))) (oip (σ i))  osn (σ i)
                         (nsqn (rt (σ (sip (σ i)))) (oip (σ i)) = osn (σ i)
                             (hops (σ i)  the (dhops (rt (σ (sip (σ i)))) (oip (σ i)))
                                   the (flag (rt (σ (sip (σ i)))) (oip (σ i))) = inv)))"
    (is "_  (?S, ?U →) _")
    proof (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh
                                                              aodv_wf oaodv_trans]
                             onl_oinvariant_sterms [OF aodv_wf oreceived_rreq_rrep_nsqn_fresh_inv]
                             onl_oinvariant_sterms [OF aodv_wf oosn_rreq]
                   simp add: seqlsimp
                   simp del: One_nat_def, rule impI)
    fix σ σ' p l
    assume "(σ, p)  oreachable (opaodv i) ?S ?U"
       and "l  labels ΓAODV p"
       and pre:
           "(l = PAodv-:4  l = PAodv-:5  l = PRreq-:0  l = PRreq-:2)  sip (σ i)  oip (σ i)
              oip (σ i)  kD (rt (σ (sip (σ i))))
                  osn (σ i)  nsqn (rt (σ (sip (σ i)))) (oip (σ i))
                  (nsqn (rt (σ (sip (σ i)))) (oip (σ i)) = osn (σ i)
                     the (dhops (rt (σ (sip (σ i)))) (oip (σ i)))  hops (σ i)
                         the (flag (rt (σ (sip (σ i)))) (oip (σ i))) = inv)"
       and "other quality_increases {i} σ σ'"
       and hyp: "(l=PAodv-:4  l=PAodv-:5  l=PRreq-:0  l=PRreq-:2)  sip (σ' i)  oip (σ' i)"
           (is "?labels  sip (σ' i)  oip (σ' i)")
    from this(4) have "σ' i = σ i" ..
    with hyp have hyp': "?labels  sip (σ i)  oip (σ i)" by simp
    show "oip (σ' i)  kD (rt (σ' (sip (σ' i))))
           osn (σ' i)  nsqn (rt (σ' (sip (σ' i)))) (oip (σ' i))
           (nsqn (rt (σ' (sip (σ' i)))) (oip (σ' i)) = osn (σ' i)
              the (dhops (rt (σ' (sip (σ' i)))) (oip (σ' i)))  hops (σ' i)
                   the (flag (rt (σ' (sip (σ' i)))) (oip (σ' i))) = inv)"
    proof (cases "sip (σ i) = i")
      assume "sip (σ i)  i"
      from other quality_increases {i} σ σ'
        have "quality_increases (σ (sip (σ i))) (σ' (sip (σ' i)))"
          by (rule otherE)  (clarsimp simp: sip (σ i)  i)
      moreover from (σ, p)  oreachable (opaodv i) ?S ?U l  labels ΓAODV p and hyp
        have "1  osn (σ' i)"
          by (auto dest!: onl_oinvariant_weakenD [OF oosn_rreq]
                   simp add: seqlsimp σ' i = σ i)
      moreover from sip (σ i)  i hyp' and pre
        have "oip (σ' i)  kD (rt (σ (sip (σ i))))
               osn (σ' i)  nsqn (rt (σ (sip (σ i)))) (oip (σ' i))
               (nsqn (rt (σ (sip (σ i)))) (oip (σ' i)) = osn (σ' i)
                   the (dhops (rt (σ (sip (σ i)))) (oip (σ' i)))  hops (σ' i)
                        the (flag (rt (σ (sip (σ i)))) (oip (σ' i))) = inv)"
        by (auto simp: σ' i = σ i)
      ultimately show ?thesis
        by (rule quality_increases_rreq_rrep_props)
    next
      assume "sip (σ i) = i" thus ?thesis
        using σ' i = σ i hyp and pre by auto
    qed
  qed (auto elim!: quality_increases_rreq_rrep_props')

lemma odsn_rrep:
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
      onl ΓAODV (seql i (λ(ξ, l). l  {PAodv-:6, PAodv-:7}  {PRrep-:n|n. True}  1  dsn ξ))"
  by (rule oinvariant_weakenE [OF open_seq_invariant [OF dsn_rrep initiali_aodv]])
     (auto simp: seql_onl_swap)

lemma rrep_sip:
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
               onl ΓAODV (λ(σ, l).
                   (l  {PAodv-:6, PAodv-:7, PRrep-:0, PRrep-:1}  sip (σ i)  dip (σ i))
                     dip (σ i)  kD(rt (σ (sip (σ i))))
                         nsqn (rt (σ (sip (σ i)))) (dip (σ i))  dsn (σ i)
                         (nsqn (rt (σ (sip (σ i)))) (dip (σ i)) = dsn (σ i)
                             (hops (σ i)  the (dhops (rt (σ (sip (σ i)))) (dip (σ i)))
                                   the (flag (rt (σ (sip (σ i)))) (dip (σ i))) = inv)))"
    (is "_  (?S, ?U →) _")
  proof (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh aodv_wf
                                                            oaodv_trans]
                             onl_oinvariant_sterms [OF aodv_wf oreceived_rreq_rrep_nsqn_fresh_inv]
                             onl_oinvariant_sterms [OF aodv_wf odsn_rrep]
                   simp del: One_nat_def, rule impI)
    fix σ σ' p l
    assume "(σ, p)  oreachable (opaodv i) ?S ?U"
       and "l  labels ΓAODV p"
       and pre:
           "(l = PAodv-:6  l = PAodv-:7  l = PRrep-:0  l = PRrep-:1)  sip (σ i)  dip (σ i)
            dip (σ i)  kD (rt (σ (sip (σ i))))
                dsn (σ i)  nsqn (rt (σ (sip (σ i)))) (dip (σ i))
                (nsqn (rt (σ (sip (σ i)))) (dip (σ i)) = dsn (σ i)
                   the (dhops (rt (σ (sip (σ i)))) (dip (σ i)))  hops (σ i)
                       the (flag (rt (σ (sip (σ i)))) (dip (σ i))) = inv)"
       and "other quality_increases {i} σ σ'"
       and hyp: "(l=PAodv-:6  l=PAodv-:7  l=PRrep-:0  l=PRrep-:1)  sip (σ' i)  dip (σ' i)"
           (is "?labels  sip (σ' i)  dip (σ' i)")
    from this(4) have "σ' i = σ i" ..
    with hyp have hyp': "?labels  sip (σ i)  dip (σ i)" by simp
    show "dip (σ' i)  kD (rt (σ' (sip (σ' i))))
           dsn (σ' i)  nsqn (rt (σ' (sip (σ' i)))) (dip (σ' i))
           (nsqn (rt (σ' (sip (σ' i)))) (dip (σ' i)) = dsn (σ' i)
              the (dhops (rt (σ' (sip (σ' i)))) (dip (σ' i)))  hops (σ' i)
                  the (flag (rt (σ' (sip (σ' i)))) (dip (σ' i))) = inv)"
    proof (cases "sip (σ i) = i")
      assume "sip (σ i)  i"
      from other quality_increases {i} σ σ'
        have "quality_increases (σ (sip (σ i))) (σ' (sip (σ' i)))"
          by (rule otherE)  (clarsimp simp: sip (σ i)  i)
      moreover from (σ, p)  oreachable (opaodv i) ?S ?U l  labels ΓAODV p and hyp
        have "1  dsn (σ' i)"
          by (auto dest!: onl_oinvariant_weakenD [OF odsn_rrep]
                   simp add: seqlsimp σ' i = σ i)
      moreover from sip (σ i)  i hyp' and pre
        have "dip (σ' i)  kD (rt (σ (sip (σ i))))
               dsn (σ' i)  nsqn (rt (σ (sip (σ i)))) (dip (σ' i))
               (nsqn (rt (σ (sip (σ i)))) (dip (σ' i)) = dsn (σ' i)
                  the (dhops (rt (σ (sip (σ i)))) (dip (σ' i)))  hops (σ' i)
                      the (flag (rt (σ (sip (σ i)))) (dip (σ' i))) = inv)"
        by (auto simp: σ' i = σ i)
      ultimately show ?thesis
        by (rule quality_increases_rreq_rrep_props)
    next
      assume "sip (σ i) = i" thus ?thesis
        using σ' i = σ i hyp and pre by auto
    qed
  qed (auto simp add: seqlsimp elim!: quality_increases_rreq_rrep_props')

lemma rerr_sip:
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →)
               onl ΓAODV (λ(σ, l).
                 l  {PAodv-:8, PAodv-:9, PRerr-:0, PRerr-:1}
                  (ripcdom(dests (σ i)). ripckD(rt (σ (sip (σ i)))) 
                        the (dests (σ i) ripc) - 1  nsqn (rt (σ (sip (σ i)))) ripc))"
  (is "_  (?S, ?U →) _")
  proof -
    { fix dests rip sip rsn and σ σ' :: "ip  state"
      assume qinc: "j. quality_increases (σ j) (σ' j)"
         and *: "ripdom dests. rip  kD (rt (σ sip))
                                   the (dests rip) - 1  nsqn (rt (σ sip)) rip"
         and "dests rip = Some rsn"
      from this(3) have "ripdom dests" by auto
      with * and dests rip = Some rsn have "ripkD(rt (σ sip))"
                                         and "rsn - 1  nsqn (rt (σ sip)) rip"
        by (auto dest!: bspec)
      from qinc have "quality_increases (σ sip) (σ' sip)" ..
      have "rip  kD(rt (σ' sip))  rsn - 1  nsqn (rt (σ' sip)) rip"
      proof
        from ripkD(rt (σ sip)) and quality_increases (σ sip) (σ' sip)
          show "rip  kD(rt (σ' sip))" ..
      next
        from ripkD(rt (σ sip)) and quality_increases (σ sip) (σ' sip)
          have "nsqn (rt (σ sip)) rip  nsqn (rt (σ' sip)) rip" ..
        with rsn - 1  nsqn (rt (σ sip)) rip show "rsn - 1  nsqn (rt (σ' sip)) rip"
          by (rule le_trans)
      qed
    } note partial = this

    show ?thesis
      by (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh aodv_wf
                                                             oaodv_trans]
                              onl_oinvariant_sterms [OF aodv_wf oreceived_rreq_rrep_nsqn_fresh_inv]
                              other_quality_increases other_localD
                    simp del: One_nat_def, intro conjI)
         (clarsimp simp del: One_nat_def split: if_split_asm option.split_asm, erule(2) partial)+
  qed

lemma prerr_guard: "paodv i 
                  onl ΓAODV (λ(ξ, l). (l = PRerr-:1
                       (ipdom(dests ξ). ipvD(rt ξ)
                                              the (nhop (rt ξ) ip) = sip ξ
                                              sqn (rt ξ) ip < the (dests ξ ip))))"
  by (inv_cterms) (clarsimp split: option.split_asm if_split_asm)

lemmas odests_vD_inc_sqn =
         open_seq_invariant [OF dests_vD_inc_sqn initiali_aodv oaodv_trans aodv_trans,
                             simplified seql_onl_swap,
                             THEN oinvariant_anyact]

lemmas oprerr_guard =
         open_seq_invariant [OF prerr_guard initiali_aodv oaodv_trans aodv_trans,
                             simplified seql_onl_swap,
                             THEN oinvariant_anyact]

text ‹Proposition 7.28›

lemma seq_compare_next_hop':
  "opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
                other quality_increases {i} →) onl ΓAODV (λ(σ, _).
                   dip. let nhip = the (nhop (rt (σ i)) dip)
                         in dip  kD(rt (σ i))  nhip  dip 
                            dip  kD(rt (σ nhip))  nsqn (rt (σ i)) dip  nsqn (rt (σ nhip)) dip)"
  (is "_  (?S, ?U →) _")
  proof -

  { fix nhop and σ σ' :: "ip  state"
    assume  pre: "dipkD(rt (σ i)). nhop dip  dip 
                    dipkD(rt (σ (nhop dip)))  nsqn (rt (σ i)) dip  nsqn (rt (σ (nhop dip))) dip"
       and qinc: "j. quality_increases (σ j) (σ' j)"
    have "dipkD(rt (σ i)). nhop dip  dip 
                  dipkD(rt (σ' (nhop dip)))  nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip"
    proof (intro ballI impI)
      fix dip
      assume "dipkD(rt (σ i))"
         and "nhop dip  dip"
      with pre have "dipkD(rt (σ (nhop dip)))"
                and "nsqn (rt (σ i)) dip  nsqn (rt (σ (nhop dip))) dip"
        by auto
      from qinc have qinc_nhop: "quality_increases (σ (nhop dip)) (σ' (nhop dip))" ..
      with dipkD(rt (σ (nhop dip))) have "dipkD (rt (σ' (nhop dip)))" ..

      moreover have "nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip"
      proof -
        from dipkD(rt (σ (nhop dip))) qinc_nhop
          have "nsqn (rt (σ (nhop dip))) dip  nsqn (rt (σ' (nhop dip))) dip" ..
        with nsqn (rt (σ i)) dip  nsqn (rt (σ (nhop dip))) dip show ?thesis
          by simp
      qed

      ultimately show "dipkD(rt (σ' (nhop dip)))
                        nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip" ..
    qed
  } note basic = this

  { fix nhop and σ σ' :: "ip  state"
    assume pre: "dipkD(rt (σ i)). nhop dip  dip  dipkD(rt (σ (nhop dip)))
                                              nsqn (rt (σ i)) dip  nsqn (rt (σ (nhop dip))) dip"
       and ndest: "ripcdom (dests (σ i)). ripc  kD (rt (σ (sip (σ i))))
                                    the (dests (σ i) ripc) - 1  nsqn (rt (σ (sip (σ i)))) ripc"
       and issip: "ipdom (dests (σ i)). nhop ip = sip (σ i)"
       and qinc: "j. quality_increases (σ j) (σ' j)"
    have "dipkD(rt (σ i)). nhop dip  dip  dip  kD (rt (σ' (nhop dip)))
                  nsqn (invalidate (rt (σ i)) (dests (σ i))) dip  nsqn (rt (σ' (nhop dip))) dip"
    proof (intro ballI impI)
      fix dip
      assume "dipkD(rt (σ i))"
         and "nhop dip  dip"
      with pre and qinc have "dipkD(rt (σ' (nhop dip)))"
                         and "nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip"
        by (auto dest!: basic)

      have "nsqn (invalidate (rt (σ i)) (dests (σ i))) dip  nsqn (rt (σ' (nhop dip))) dip"
      proof (cases "dipdom (dests (σ i))")
        assume "dipdom (dests (σ i))"
        with dipkD(rt (σ i)) obtain dsn where "dests (σ i) dip = Some dsn"
          by auto
        with dipkD(rt (σ i)) have "nsqn (invalidate (rt (σ i)) (dests (σ i))) dip = dsn - 1"
           by (rule nsqn_invalidate_eq)
        moreover have "dsn - 1  nsqn (rt (σ' (nhop dip))) dip"
        proof -
          from dests (σ i) dip = Some dsn have "the (dests (σ i) dip) = dsn" by simp
          with ndest and dipdom (dests (σ i)) have "dip  kD (rt (σ (sip (σ i))))"
                                                      "dsn - 1  nsqn (rt (σ (sip (σ i)))) dip"
            by auto
          moreover from issip and dipdom (dests (σ i)) have "nhop dip = sip (σ i)" ..
          ultimately have "dip  kD (rt (σ (nhop dip)))"
                      and "dsn - 1  nsqn (rt (σ (nhop dip))) dip" by auto
          with qinc show "dsn - 1  nsqn (rt (σ' (nhop dip))) dip"
            by simp (metis kD_nsqn_quality_increases_trans)
        qed
        ultimately show ?thesis by simp
      next
        assume "dip  dom (dests (σ i))"
        with dipkD(rt (σ i))
          have "nsqn (invalidate (rt (σ i)) (dests (σ i))) dip = nsqn (rt (σ i)) dip"
            by (rule nsqn_invalidate_other)
        with nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip show ?thesis by simp
      qed
      with dipkD(rt (σ' (nhop dip)))
        show "dip  kD (rt (σ' (nhop dip)))
               nsqn (invalidate (rt (σ i)) (dests (σ i))) dip  nsqn (rt (σ' (nhop dip))) dip" ..
    qed
  } note basic_prerr = this

  { fix σ σ' :: "ip  state"
    assume a1: "dipkD(rt (σ i)). the (nhop (rt (σ i)) dip)  dip
                 dipkD(rt (σ (the (nhop (rt (σ i)) dip))))
                     nsqn (rt (σ i)) dip  nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip"
       and a2: "j. quality_increases (σ j) (σ' j)"
    have "dipkD(rt (σ i)).
          the (nhop (update (rt (σ i)) (sip (σ i)) (0, unk, val, Suc 0, sip (σ i))) dip)  dip 
          dipkD(rt (σ' (the (nhop (update (rt (σ i)) (sip (σ i))
                                        (0, unk, val, Suc 0, sip (σ i)))
                                  dip)))) 
          nsqn (update (rt (σ i)) (sip (σ i)) (0, unk, val, Suc 0, sip (σ i))) dip
           nsqn (rt (σ' (the (nhop (update (rt (σ i)) (sip (σ i))
                                      (0, unk, val, Suc 0, sip (σ i)))
                                dip))))
             dip" (is "dipkD(rt (σ i)). ?P dip")
    proof
      fix dip
      assume "dipkD(rt (σ i))"
      with a1 and a2  
        have "the (nhop (rt (σ i)) dip)  dip  dipkD(rt (σ' (the (nhop (rt (σ i)) dip))))
                         nsqn (rt (σ i)) dip  nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
           by - (drule(1) basic, auto)
      thus "?P dip" by (cases "dip = sip (σ i)") auto
    qed
  } note nhop_update_sip = this

  { fix σ σ' oip sip osn hops
    assume pre: "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
                  dipkD(rt (σ (the (nhop (rt (σ i)) dip))))
                      nsqn (rt (σ i)) dip  nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip"
       and qinc: "j. quality_increases (σ j) (σ' j)"
       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)"
    from pre and qinc
      have pre': "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
                    dipkD(rt (σ' (the (nhop (rt (σ i)) dip))))
                        nsqn (rt (σ i)) dip  nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
        by (rule basic)
    have "(the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) oip)  oip
            oipkD(rt (σ' (the (nhop (update (rt (σ i)) oip
                                                   (osn, kno, val, Suc hops, sip)) oip))))
                 nsqn (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) oip
                    nsqn (rt (σ' (the (nhop (update (rt (σ i)) oip
                                                   (osn, kno, val, Suc hops, sip)) oip)))) oip)"
       (is "?nhop_not_oip  ?oip_in_kD  ?nsqn_le_nsqn")
     proof (rule, split update_rt_split_asm)
       assume "rt (σ i) = update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)"
          and "the (nhop (rt (σ i)) oip)  oip"
       with pre' show "?oip_in_kD  ?nsqn_le_nsqn" by auto
     next
       assume rtnot: "rt (σ i)  update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)"
          and notoip: ?nhop_not_oip
       with * qinc have ?oip_in_kD
         by (clarsimp elim!: kD_quality_increases)
       moreover with * pre qinc rtnot notoip have ?nsqn_le_nsqn
        by simp (metis kD_nsqn_quality_increases_trans)
       ultimately show "?oip_in_kD  ?nsqn_le_nsqn" ..
     qed
  } note update1 = this

  { fix σ σ' oip sip osn hops
    assume pre: "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
                   dipkD(rt (σ (the (nhop (rt (σ i)) dip))))
                       nsqn (rt (σ i)) dip  nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip"
       and qinc: "j. quality_increases (σ j) (σ' j)"
       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)"
    from pre and qinc
      have pre': "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
                    dipkD(rt (σ' (the (nhop (rt (σ i)) dip))))
                        nsqn (rt (σ i)) dip  nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
        by (rule basic)
    have "dipkD(rt (σ i)).
           the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)  dip
            dipkD(rt (σ' (the (nhop (update (rt (σ i)) oip
                                                  (osn, kno, val, Suc hops, sip)) dip))))
                nsqn (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip
                   nsqn (rt (σ' (the (nhop (update (rt (σ i)) oip
                                                  (osn, kno, val, Suc hops, sip)) dip)))) dip"
       (is "dipkD(rt (σ i)). _  ?dip_in_kD dip  ?nsqn_le_nsqn dip")
     proof (intro ballI impI, split update_rt_split_asm)
       fix dip
       assume "dipkD(rt (σ i))"
          and "the (nhop (rt (σ i)) dip)  dip"
          and "rt (σ i) = update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)"
        with pre' show "?dip_in_kD dip  ?nsqn_le_nsqn dip" by simp
     next
       fix dip
       assume "dipkD(rt (σ i))"
          and notdip: "the (nhop (update (rt (σ i)) oip
                             (osn, kno, val, Suc hops, sip)) dip)  dip"
          and rtnot: "rt (σ i)  update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)"
       show "?dip_in_kD dip  ?nsqn_le_nsqn dip"
       proof (cases "dip = oip")
         assume "dip  oip"
         with pre' dipkD(rt (σ i)) notdip
           show ?thesis by clarsimp
       next
         assume "dip = oip"
         with rtnot qinc dipkD(rt (σ i)) notdip *
           have "?dip_in_kD dip"
            by simp (metis kD_quality_increases)
         moreover from dip = oip rtnot qinc dipkD(rt (σ i)) notdip *
           have "?nsqn_le_nsqn dip" by simp (metis kD_nsqn_quality_increases_trans)
         ultimately show ?thesis ..
       qed
     qed
  } note update2 = this

  have "opaodv i  (?S, ?U →) onl ΓAODV (λ(σ, _).
                   dip  kD(rt (σ i)). the (nhop (rt (σ i)) dip)  dip
                       dip  kD(rt (σ (the (nhop (rt (σ i)) dip))))
                           nsqn (rt (σ i)) dip  nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip)"
    by (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh aodv_wf
                                                           oaodv_trans]
                            onl_oinvariant_sterms [OF aodv_wf odests_vD_inc_sqn]
                            onl_oinvariant_sterms [OF aodv_wf oprerr_guard]
                            onl_oinvariant_sterms [OF aodv_wf rreq_sip]
                            onl_oinvariant_sterms [OF aodv_wf rrep_sip]
                            onl_oinvariant_sterms [OF aodv_wf rerr_sip]
                            other_quality_increases
                            other_localD
                      solve: basic basic_prerr
                      simp add: seqlsimp nsqn_invalidate nhop_update_sip
                      simp del: One_nat_def)
       (rule conjI, erule(2) update1, erule(2) update2)+

    thus ?thesis unfolding Let_def by auto
  qed

text ‹Proposition 7.30›

lemmas okD_unk_or_atleast_one =
         open_seq_invariant [OF kD_unk_or_atleast_one initiali_aodv,
                             simplified seql_onl_swap]

lemmas ozero_seq_unk_hops_one =
         open_seq_invariant [OF zero_seq_unk_hops_one initiali_aodv,
                             simplified seql_onl_swap]

lemma oreachable_fresh_okD_unk_or_atleast_one:
    fixes dip
  assumes "(σ, p)  oreachable (opaodv i)
                       (otherwith ((=)) {i} (orecvmsg (λσ m. msg_fresh σ m
                                                              msg_zhops m)))
                       (other quality_increases {i})"
      and "dipkD(rt (σ i))"
    shows "π3(the (rt (σ i) dip)) = unk  1  π2(the (rt (σ i) dip))"
    (is "?P dip")
  proof -
    have "l. llabels ΓAODV p" by (metis aodv_ex_label)
    with assms(1) have "dipkD (rt (σ i)). ?P dip"
      by - (drule oinvariant_weakenD [OF okD_unk_or_atleast_one [OF oaodv_trans aodv_trans]],
            auto dest!: otherwith_actionD onlD simp: seqlsimp)
    with dipkD(rt (σ i)) show ?thesis by simp
  qed

lemma oreachable_fresh_ozero_seq_unk_hops_one:
    fixes dip
  assumes "(σ, p)  oreachable (opaodv i)
                     (otherwith ((=)) {i} (orecvmsg (λσ m. msg_fresh σ m
                                                          msg_zhops m)))
                     (other quality_increases {i})"
      and "dipkD(rt (σ i))"
    shows "sqn (rt (σ i)) dip = 0 
             sqnf (rt (σ i)) dip = unk
              the (dhops (rt (σ i)) dip) = 1
              the (nhop (rt (σ i)) dip) = dip"
    (is "?P dip")
  proof -
    have "l. llabels ΓAODV p" by (metis aodv_ex_label)
    with assms(1) have "dipkD (rt (σ i)). ?P dip"
      by - (drule oinvariant_weakenD [OF ozero_seq_unk_hops_one [OF oaodv_trans aodv_trans]],
            auto dest!: onlD otherwith_actionD simp: seqlsimp)
    with dipkD(rt (σ i)) show ?thesis by simp
  qed

lemma seq_nhop_quality_increases':
  shows "opaodv i  (otherwith ((=)) {i}
                        (orecvmsg (λσ m. msg_fresh σ m  msg_zhops m)),
                         other quality_increases {i} →)
                        onl ΓAODV (λ(σ, _). dip. let nhip = the (nhop (rt (σ i)) dip)
                                               in dip  vD (rt (σ i))  vD (rt (σ nhip))
                                                   nhip  dip
                                                   (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
  (is "_  (?S i, _ →) _")
  proof -
    have weaken:
      "p I Q R P. p  (otherwith quality_increases I (orecvmsg Q), other quality_increases I →) P
        p  (otherwith ((=)) I (orecvmsg (λσ m. Q σ m  R σ m)), other quality_increases I →) P"
        by auto
    {
      fix i a and σ σ' :: "ip  state"
      assume a1: "dip. dipvD(rt (σ i))
                         dipvD(rt (σ (the (nhop (rt (σ i)) dip))))
                         (the (nhop (rt (σ i)) dip))  dip
                          rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
         and ow: "?S i σ σ' a"
      have "dip. dipvD(rt (σ i))
                   dipvD (rt (σ' (the (nhop (rt (σ i)) dip))))
                   (the (nhop (rt (σ i)) dip))  dip
                rt (σ i) ⊏⇘diprt (σ' (the (nhop (rt (σ i)) dip)))"
      proof clarify
        fix dip
        assume a2: "dipvD(rt (σ i))"
           and a3: "dipvD (rt (σ' (the (nhop (rt (σ i)) dip))))"
           and a4: "(the (nhop (rt (σ i)) dip))  dip"
        from ow have "j. j  i  σ j = σ' j" by auto
        show "rt (σ i) ⊏⇘diprt (σ' (the (nhop (rt (σ i)) dip)))"
        proof (cases "(the (nhop (rt (σ i)) dip)) = i")
          assume "(the (nhop (rt (σ i)) dip)) = i"
          with dip  vD(rt (σ i)) have "dip  vD(rt (σ (the (nhop (rt (σ i)) dip))))" by simp
          with a1 a2 a4 have "rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))" by simp
          with (the (nhop (rt (σ i)) dip)) = i have "rt (σ i) ⊏⇘diprt (σ i)" by simp
          hence False by simp
          thus ?thesis ..
        next
          assume "(the (nhop (rt (σ i)) dip))  i"
          with j. j  i  σ j = σ' j
            have *: "σ (the (nhop (rt (σ i)) dip)) = σ' (the (nhop (rt (σ i)) dip))" by simp
          with dipvD (rt (σ' (the (nhop (rt (σ i)) dip))))
            have "dipvD (rt (σ (the (nhop (rt (σ i)) dip))))" by simp
          with a1 a2 a4 have "rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))" by simp
          with * show ?thesis by simp
        qed
      qed
    } note basic = this

    { fix σ σ' a dip sip i
      assume a1: "dip. dipvD(rt (σ i))
                       dipvD(rt (σ (the (nhop (rt (σ i)) dip))))
                       the (nhop (rt (σ i)) dip)  dip
                       rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
         and ow: "?S i σ σ' a"
      have "dip. dipvD(update (rt (σ i)) sip (0, unk, val, Suc 0, sip))
            dipvD(rt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip))))
            the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip)  dip
            update (rt (σ i)) sip (0, unk, val, Suc 0, sip)
               ⊏⇘diprt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip)))"
      proof clarify
        fix dip
        assume a2: "dipvD (update (rt (σ i)) sip (0, unk, val, Suc 0, sip))"
           and a3: "dipvD(rt (σ' (the (nhop
                         (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip))))"
           and a4: "the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip)  dip"
        show "update (rt (σ i)) sip (0, unk, val, Suc 0, sip)
              ⊏⇘diprt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip)))"
        proof (cases "dip = sip")
          assume "dip = sip"
          with the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip)  dip
          have False by simp
          thus ?thesis ..
        next
          assume [simp]: "dip  sip"
          from a2 have "dipvD(rt (σ i))  dip = sip"
            by (rule vD_update_val)
          with dip  sip have "dipvD(rt (σ i))" by simp
          moreover from a3 have "dipvD(rt (σ' (the (nhop (rt (σ i)) dip))))" by simp
          moreover from a4 have "the (nhop (rt (σ i)) dip)  dip" by simp
          ultimately have "rt (σ i) ⊏⇘diprt (σ' (the (nhop (rt (σ i)) dip)))"
            using a1 ow by - (drule(1) basic, simp)
          with dip  sip show ?thesis
            by - (erule rt_strictly_fresher_update_other, simp)
        qed
      qed
    } note update_0_unk = this

    { fix σ a σ' nhop
      assume pre: "dip. dipvD(rt (σ i))  dipvD(rt (σ (nhop dip)))  nhop dip  dip
                          rt (σ i) ⊏⇘diprt (σ (nhop dip))"
         and ow: "?S i σ σ' a"
      have "dip. dip  vD (invalidate (rt (σ i)) (dests (σ i)))
                   dip  vD (rt (σ' (nhop dip)))  nhop dip  dip
                   rt (σ i) ⊏⇘diprt (σ' (nhop dip))"
      proof clarify
        fix dip
        assume "dipvD(invalidate (rt (σ i)) (dests (σ i)))"
           and "dipvD(rt (σ' (nhop dip)))"
           and "nhop dip  dip"
        from this(1) have "dipvD (rt (σ i))"
          by (clarsimp dest!: vD_invalidate_vD_not_dests)
        moreover from ow have "j. j  i  σ j = σ' j" by auto
        ultimately have "rt (σ i) ⊏⇘diprt (σ (nhop dip))"
          using pre dip  vD (rt (σ' (nhop dip))) nhop dip  dip
          by metis
        with j. j  i  σ j = σ' j show  "rt (σ i) ⊏⇘diprt (σ' (nhop dip))"
          by (metis rt_strictly_fresher_irefl)
      qed
    } note invalidate = this

    { fix σ a σ' dip oip osn sip hops i
      assume pre: "dip. dip  vD (rt (σ i))
                        dip  vD (rt (σ (the (nhop (rt (σ i)) dip))))
                        the (nhop (rt (σ i)) dip)  dip
                    rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
         and ow: "?S i σ σ' a"
         and "Suc 0  osn"
         and a6: "sip  oip  oip  kD (rt (σ sip))
                                  osn  nsqn (rt (σ sip)) oip
                                  (nsqn (rt (σ sip)) oip = osn
                                     the (dhops (rt (σ sip)) oip)  hops
                                          the (flag (rt (σ sip)) oip) = inv)"
         and after: "σ' i = σ irt := update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)"
      have "dip. dip  vD (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip))
                 dip  vD (rt (σ' (the (nhop (update (rt (σ i)) oip
                                      (osn, kno, val, Suc hops, sip)) dip))))
                 the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)  dip
              update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)
                 ⊏⇘diprt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)))"
      proof clarify
        fix dip
        assume a2: "dipvD(update (rt (σ i)) oip (osn, kno, val, Suc (hops), sip))"
           and a3: "dipvD(rt (σ' (the (nhop (update (rt (σ i)) oip
                                                        (osn, kno, val, Suc hops, sip)) dip))))"
           and a4: "the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)  dip"
        from ow have a5: "j. j  i  σ j = σ' j" by auto
        show "update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)
              ⊏⇘diprt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)))"
          (is "?rt1 ⊏⇘dip?rt2 dip")
        proof (cases "?rt1 = rt (σ i)")
          assume nochange [simp]:
            "update (rt (σ i)) oip (osn, kno, val, Suc hops, sip) = rt (σ i)"

          from after have "σ' i = σ i" by simp
          with a5 have "j. σ j = σ' j" by metis

          from a2 have "dipvD (rt (σ i))" by simp
          moreover from a3 have "dipvD(rt (σ (the (nhop (rt (σ i)) dip))))"
            using nochange and j. σ j = σ' j by clarsimp
          moreover from a4 have "the (nhop (rt (σ i)) dip)  dip" by simp
          ultimately have "rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
            using pre by simp

          hence "rt (σ i) ⊏⇘diprt (σ' (the (nhop (rt (σ i)) dip)))"
            using j. σ j = σ' j by simp
          thus "?thesis" by simp
        next
          assume change: "?rt1  rt (σ i)"
          from after a2 have "dipkD(rt (σ' i))" by auto
          show ?thesis
          proof (cases "dip = oip")
            assume "dip  oip"

            with a2 have "dipvD (rt (σ i))" by auto
            moreover with a3 a5 after and dip  oip
              have "dipvD(rt (σ (the (nhop (rt (σ i)) dip))))"
                by simp metis
            moreover from a4 and dip  oip have "the (nhop (rt (σ i)) dip)  dip" by simp
            ultimately have "rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
              using pre by simp

            with after and a5 and dip  oip show ?thesis
              by simp (metis rt_strictly_fresher_update_other
                             rt_strictly_fresher_irefl)
          next
            assume "dip = oip"

            with a4 and change have "sip  oip" by simp
            with a6 have "oipkD(rt (σ sip))"
                     and "osn  nsqn (rt (σ sip)) oip" by auto

            from a3 change dip = oip have "oipvD(rt (σ' sip))" by simp
            hence "the (flag (rt (σ' sip)) oip) = val" by simp

            from oipkD(rt (σ sip))
            have "osn < nsqn (rt (σ' sip)) oip  (osn = nsqn (rt (σ' sip)) oip
                                                    the (dhops (rt (σ' sip)) oip)  hops)"
            proof
              assume "oipvD(rt (σ sip))"
              hence "the (flag (rt (σ sip)) oip) = val" by simp
              with a6 sip  oip have "nsqn (rt (σ sip)) oip = osn 
                                          the (dhops (rt (σ sip)) oip)  hops"
                by simp
              show ?thesis
              proof (cases "sip = i")
                assume "sip  i"
                with a5 have "σ sip = σ' sip" by simp
                with osn  nsqn (rt (σ sip)) oip
                 and nsqn (rt (σ sip)) oip = osn  the (dhops (rt (σ sip)) oip)  hops
                show ?thesis by auto
              next
                ― ‹alternative to using @{text sip_not_ip}
                assume [simp]: "sip = i"
                have "?rt1 = rt (σ i)"
                proof (rule update_cases_kD, simp_all)
                  from Suc 0  osn show "0 < osn" by simp
                next
                  from oipkD(rt (σ sip)) and sip = i show "oipkD(rt (σ i))"
                    by simp
                next
                  assume "sqn (rt (σ i)) oip < osn"
                  also from osn  nsqn (rt (σ sip)) oip
                    have "...  nsqn (rt (σ i)) oip" by simp
                  also have "...  sqn (rt (σ i)) oip"
                    by (rule nsqn_sqn)
                  finally have "sqn (rt (σ i)) oip < sqn (rt (σ i)) oip" .
                  hence False by simp
                  thus "(λa. if a = oip
                             then Some (osn, kno, val, Suc hops, i)
                             else rt (σ i) a) = rt (σ i)" ..
                next
                  assume "sqn (rt (σ i)) oip = osn"
                     and "Suc hops < the (dhops (rt (σ i)) oip)"
                  from this(1) and oip  vD (rt (σ sip)) have "nsqn (rt (σ i)) oip = osn"
                    by simp
                  with nsqn (rt (σ sip)) oip = osn  the (dhops (rt (σ sip)) oip)  hops
                    have "the (dhops (rt (σ i)) oip)  hops" by simp
                  with Suc hops < the (dhops (rt (σ i)) oip) have False by simp
                  thus "(λa. if a = oip
                             then Some (osn, kno, val, Suc hops, i)
                             else rt (σ i) a) = rt (σ i)" ..
                next
                  assume "the (flag (rt (σ i)) oip) = inv"
                  with the (flag (rt (σ sip)) oip) = val have False by simp
                  thus "(λa. if a = oip
                             then Some (osn, kno, val, Suc hops, i)
                             else rt (σ i) a) = rt (σ i)" ..
                next
                  from oipkD(rt (σ sip))
                    show "(λa. if a = oip then Some (the (rt (σ i) oip)) else rt (σ i) a) = rt (σ i)"
                      by (auto dest!: kD_Some)
                qed
                with change have False ..
                thus ?thesis ..
              qed
            next
              assume "oipiD(rt (σ sip))"
              with the (flag (rt (σ' sip)) oip) = val and a5 have "sip = i"
                by (metis f.distinct(1) iD_flag_is_inv)
              from oipiD(rt (σ sip)) have "the (flag (rt (σ sip)) oip) = inv" by auto
              with sip = i Suc 0  osn change after oipkD(rt (σ sip))
                have "nsqn (rt (σ sip)) oip < nsqn (rt (σ' sip)) oip"
                  unfolding update_def
                  by (clarsimp split: option.split_asm if_split_asm)
                     (auto simp: sqn_def)
              with osn  nsqn (rt (σ sip)) oip have "osn < nsqn (rt (σ' sip)) oip"
                by simp
              thus ?thesis ..
            qed
            thus ?thesis
            proof
              assume osnlt: "osn < nsqn (rt (σ' sip)) oip"
              from dipkD(rt (σ' i)) and dip = oip have "dip  kD (?rt1)" by simp
              moreover from a3 have "dip  kD(?rt2 dip)" by simp
              moreover have "nsqn ?rt1 dip < nsqn (?rt2 dip) dip"
                proof -
                  have "nsqn ?rt1 oip = osn"
                    by (simp add: dip = oip nsqn_update_changed_kno_val [OF change [THEN not_sym]])
                  also have "... < nsqn (rt (σ' sip)) oip" using osnlt .
                  also have  "... = nsqn (?rt2 oip) oip" by (simp add: change)
                  finally show ?thesis
                    using dip = oip by simp
                qed
              ultimately show ?thesis
                by (rule rt_strictly_fresher_ltI)
            next
              assume osneq: "osn = nsqn (rt (σ' sip)) oip  the (dhops (rt (σ' sip)) oip)  hops"

              have "oipkD(?rt1)" by simp
              moreover from a3 dip = oip have "oipkD(?rt2 oip)" by simp

              moreover have "nsqn ?rt1 oip = nsqn (?rt2 oip) oip"
              proof -
                from osneq have "osn = nsqn (rt (σ' sip)) oip" ..
                also have "osn = nsqn ?rt1 oip"
                  by (simp add: dip = oip nsqn_update_changed_kno_val [OF change [THEN not_sym]])
                also have  "nsqn (rt (σ' sip)) oip = nsqn (?rt2 oip) oip"
                  by (simp add: change)
                finally show ?thesis .
              qed

              moreover have "π5(the (?rt2 oip oip)) < π5(the (?rt1 oip))"
              proof -
                from osneq have "the (dhops (rt (σ' sip)) oip)  hops" ..
                moreover from oip  vD (rt (σ' sip)) have "oipkD(rt (σ' sip))" by auto
                ultimately have "π5(the (rt (σ' sip) oip))  hops"
                  by (auto simp add: proj5_eq_dhops)
                also from change after have "hops < π5(the (rt (σ' i) oip))"
                  by (simp add: proj5_eq_dhops) (metis dhops_update_changed lessI)
                finally have "π5(the (rt (σ' sip) oip)) < π5(the (rt (σ' i) oip))" .
                with change after show ?thesis by simp
              qed

              ultimately have "?rt1 ⊏⇘oip?rt2 oip"
                by (rule rt_strictly_fresher_eqI)
              with dip = oip show ?thesis by simp
                qed
          qed
       qed
     qed
    } note rreq_rrep_update = this

    have "opaodv i  (otherwith ((=)) {i} (orecvmsg (λσ m. msg_fresh σ m
                                                             msg_zhops m)),
                       other quality_increases {i} →)
            onl ΓAODV
           (λ(σ, _). dip. dip  vD (rt (σ i))  vD (rt (σ (the (nhop (rt (σ i)) dip))))
                            the (nhop (rt (σ i)) dip)  dip
                            rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip))))"
      proof (inv_cterms inv add: onl_oinvariant_sterms [OF aodv_wf rreq_sip [THEN weaken]]
                                 onl_oinvariant_sterms [OF aodv_wf rrep_sip [THEN weaken]]
                                 onl_oinvariant_sterms [OF aodv_wf rerr_sip [THEN weaken]]
                                 onl_oinvariant_sterms [OF aodv_wf oosn_rreq [THEN weaken]]
                                 onl_oinvariant_sterms [OF aodv_wf odsn_rrep [THEN weaken]]
                        solve: basic update_0_unk invalidate rreq_rrep_update
                        simp add: seqlsimp)
        fix σ σ' p l
        assume or: "(σ, p)  oreachable (opaodv i) (?S i)  (other quality_increases {i})"
           and "other quality_increases {i} σ σ'"
           and ll: "l  labels ΓAODV p"
           and pre: "dip. dipvD (rt (σ i))
                            dipvD(rt (σ (the (nhop (rt (σ i)) dip))))
                            the (nhop (rt (σ i)) dip)  dip
                         rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
        from this(1-2)
          have or': "(σ', p)  oreachable (opaodv i) (?S i)  (other quality_increases {i})"
            by - (rule oreachable_other')

        from or and ll have next_hop: "dip. let nhip = the (nhop (rt (σ i)) dip)
                                             in dip  kD(rt (σ i))  nhip  dip
                                              dip  kD(rt (σ nhip))
                                                  nsqn (rt (σ i)) dip  nsqn (rt (σ nhip)) dip"
          by (auto dest!: onl_oinvariant_weakenD [OF seq_compare_next_hop'])

        from or and ll have unk_hops_one: "dipkD (rt (σ i)). sqn (rt (σ i)) dip = 0
                                                 sqnf (rt (σ i)) dip = unk
                                                     the (dhops (rt (σ i)) dip) = 1
                                                     the (nhop (rt (σ i)) dip) = dip"
          by (auto dest!: onl_oinvariant_weakenD [OF ozero_seq_unk_hops_one
                                                     [OF oaodv_trans aodv_trans]]
                          otherwith_actionD
                          simp: seqlsimp)

        from other quality_increases {i} σ σ' have "σ' i = σ i" by auto
        hence "quality_increases (σ i) (σ' i)" by auto
        with other quality_increases {i} σ σ' have "j. quality_increases (σ j) (σ' j)"
          by - (erule otherE, metis singleton_iff)

        show "dip. dip  vD (rt (σ' i))
                   dip  vD (rt (σ' (the (nhop (rt (σ' i)) dip))))
                   the (nhop (rt (σ' i)) dip)  dip
               rt (σ' i) ⊏⇘diprt (σ' (the (nhop (rt (σ' i)) dip)))"
        proof clarify
          fix dip
          assume "dipvD(rt (σ' i))"
             and "dipvD(rt (σ' (the (nhop (rt (σ' i)) dip))))"
             and "the (nhop (rt (σ' i)) dip)  dip"
          from this(1) and σ' i = σ i have "dipvD(rt (σ i))"
                                         and "dipkD(rt (σ i))"
            by auto

          from the (nhop (rt (σ' i)) dip)  dip and σ' i = σ i
            have "the (nhop (rt (σ i)) dip)  dip" (is "?nhip  _") by simp
          with dipkD(rt (σ i)) and next_hop
            have "dipkD(rt (σ (?nhip)))"
             and nsqns: "nsqn (rt (σ i)) dip  nsqn (rt (σ ?nhip)) dip"
               by (auto simp: Let_def)

          have "0 < sqn (rt (σ i)) dip"
            proof (rule neq0_conv [THEN iffD1, OF notI])
              assume "sqn (rt (σ i)) dip = 0"
              with dipkD(rt (σ i)) and unk_hops_one
                have "?nhip = dip" by simp
              with ?nhip  dip show False ..
            qed
          also have "... = nsqn (rt (σ i)) dip"
            by (rule vD_nsqn_sqn [OF dipvD(rt (σ i)), THEN sym])
          also have "...  nsqn (rt (σ ?nhip)) dip"
            by (rule nsqns)
          also have "...  sqn (rt (σ ?nhip)) dip"
            by (rule nsqn_sqn)
          finally have "0 < sqn (rt (σ ?nhip)) dip" .

          have "rt (σ i) ⊏⇘diprt (σ' ?nhip)"
          proof (cases "dipvD(rt (σ ?nhip))")
            assume "dipvD(rt (σ ?nhip))"
            with pre dipvD(rt (σ i)) and ?nhip  dip
              have "rt (σ i) ⊏⇘diprt (σ ?nhip)" by auto
            moreover from j. quality_increases (σ j) (σ' j)
              have "quality_increases (σ ?nhip) (σ' ?nhip)" ..
            ultimately show ?thesis
              using dipkD(rt (σ ?nhip))
              by (rule strictly_fresher_quality_increases_right)
          next
            assume "dipvD(rt (σ ?nhip))"
            with dipkD(rt (σ ?nhip)) have "dipiD(rt (σ ?nhip))" ..
            hence "the (flag (rt (σ ?nhip)) dip) = inv"
              by auto
            have "nsqn (rt (σ i)) dip  nsqn (rt (σ ?nhip)) dip"
              by (rule nsqns)
            also from dipiD(rt (σ ?nhip))
              have "... = sqn (rt (σ ?nhip)) dip - 1" ..
            also have "... < sqn (rt (σ' ?nhip)) dip"
              proof -
                from j. quality_increases (σ j) (σ' j)
                  have "quality_increases (σ ?nhip) (σ' ?nhip)" ..
                hence "ip. sqn (rt (σ ?nhip)) ip  sqn (rt (σ' ?nhip)) ip" by auto
                hence "sqn (rt (σ ?nhip)) dip  sqn (rt (σ' ?nhip)) dip" ..
                with 0 < sqn (rt (σ ?nhip)) dip show ?thesis by auto
              qed
            also have "... = nsqn (rt (σ' ?nhip)) dip"
              proof (rule vD_nsqn_sqn [THEN sym])
                from dipvD(rt (σ' (the (nhop (rt (σ' i)) dip)))) and σ' i = σ i
                  show "dipvD(rt (σ' ?nhip))" by simp
              qed
            finally have "nsqn (rt (σ i)) dip < nsqn (rt (σ' ?nhip)) dip" .

            moreover from dipvD(rt (σ' (the (nhop (rt (σ' i)) dip)))) and σ' i = σ i
              have "dipkD(rt (σ' ?nhip))" by auto
            ultimately show "rt (σ i) ⊏⇘diprt (σ' ?nhip)"
              using dipkD(rt (σ i)) by - (rule rt_strictly_fresher_ltI)
          qed
          with σ' i = σ i show "rt (σ' i) ⊏⇘diprt (σ' (the (nhop (rt (σ' i)) dip)))"
            by simp
        qed
      qed
    thus ?thesis unfolding Let_def .
  qed

lemma seq_compare_next_hop:
  fixes w
  shows "opaodv i  (otherwith ((=)) {i} (orecvmsg msg_fresh),
                      other quality_increases {i} →)
                       global (λσ. dip. let nhip =