Quelle  Global_Invariants.thy

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

section "Global invariant proofs over sequential processes"

theory Global_Invariants
imports Seq_Invariants
        Aodv_Predicates
        Fresher
        Quality_Increases
        AWN.OAWN_Convert
        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 "j∉I"
    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 := σ i(msg := 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 = σ i(msg := msg)"
    from this(1) have "P σ msg"
                 and "∀j. j≠i ⟶ Q (σ j) (σ' j)" by auto
    from this(1) have "P (σ(i := σ i(msg := msg))) msg" by (rule local)
    thus "P σ' msg"
    proof (rule other)
      from ‹σ' i = σ i(msg := msg)› and ‹∀j. j≠i ⟶ Q (σ j) (σ' j)›
        show "other Q {i} (σ(i := σ i(msg := 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 (λ((ξ, _), _, (ξ', _)). ∀dip∈kD (rt ξ). rt ξ ⊑ rt ξ') (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 "l∈labels Γ_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 ‹l∈labels Γ_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 ‹l∈labels Γ_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 ‹l∈labels Γ_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 ‹l∈labels Γ_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 := σ i(msg := 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}
                 ⟶ (∀ripc∈dom(dests (σ i)). ripc∈kD(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 *: "∀rip∈dom dests. rip ∈ kD (rt (σ sip))
                                  ∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
         and "dests rip = Some rsn"
      from this(3) have "rip∈dom dests" by auto
      with * and ‹dests rip = Some rsn› have "rip∈kD(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 ‹rip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
          show "rip ∈ kD(rt (σ' sip))" ..
      next
        from ‹rip∈kD(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
                      ⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ)
                                             ∧ the (nhop (rt ξ) ip) = sip ξ
                                             ∧ sqn (rt ξ) ip < the (dests ξ ip))))"
  by (inv_cterms) (clarsimp split: option.split_asm if_split_asm)

lemmas oaddpreRT_welldefined =
         open_seq_invariant [OF addpreRT_welldefined initiali_aodv oaodv_trans aodv_trans,
                             simplified seql_onl_swap,
                             THEN oinvariant_anyact]

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: "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶
                    dip∈kD(rt (σ (nhop dip))) ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (nhop dip))) dip"
       and qinc: "∀j. quality_increases (σ j) (σ' j)"
    have "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶
                  dip∈kD(rt (σ' (nhop dip))) ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
    proof (intro ballI impI)
      fix dip
      assume "dip∈kD(rt (σ i))"
         and "nhop dip ≠ dip"
      with pre have "dip∈kD(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 ‹dip∈kD(rt (σ (nhop dip)))› have "dip∈kD (rt (σ' (nhop dip)))" ..

      moreover have "nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
      proof -
        from ‹dip∈kD(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 "dip∈kD(rt (σ' (nhop dip)))
                       ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip" ..
    qed
  } note basic = this

  { fix nhop and σ σ' :: "ip ==> state"
    assume pre: "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶ dip∈kD(rt (σ (nhop dip)))
                                             ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (nhop dip))) dip"
       and ndest: "∀ripc∈dom (dests (σ i)). ripc ∈ kD (rt (σ (sip (σ i))))
                                   ∧ the (dests (σ i) ripc) - 1 ≤ nsqn (rt (σ (sip (σ i)))) ripc"
       and issip: "∀ip∈dom (dests (σ i)). nhop ip = sip (σ i)"
       and qinc: "∀j. quality_increases (σ j) (σ' j)"
    have "∀dip∈kD(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 "dip∈kD(rt (σ i))"
         and "nhop dip ≠ dip"
      with pre and qinc have "dip∈kD(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 "dip∈dom (dests (σ i))")
        assume "dip∈dom (dests (σ i))"
        with ‹dip∈kD(rt (σ i))› obtain dsn where "dests (σ i) dip = Some dsn"
          by auto
        with ‹dip∈kD(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 ‹dip∈dom (dests (σ i))› have "dip ∈ kD (rt (σ (sip (σ i))))"
                                                      "dsn - 1 ≤ nsqn (rt (σ (sip (σ i)))) dip"
            by auto
          moreover from issip and ‹dip∈dom (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 ‹dip∈kD(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 ‹dip∈kD(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: "∀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"
       and a2: "∀j. quality_increases (σ j) (σ' j)"
    have "∀dip∈kD(rt (σ i)).
          the (nhop (update (rt (σ i)) (sip (σ i)) (0, unk, val, Suc 0, sip (σ i), {})) dip) ≠ dip ⟶
          dip∈kD(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 "∀dip∈kD(rt (σ i)). ?P dip")
    proof
      fix dip
      assume "dip∈kD(rt (σ i))"
      with a1 and a2  
        have "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 - (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: "∀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"
       and qinc: "∀j. quality_increases (σ j) (σ' j)"
       and *: "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)"
    from pre and qinc
      have pre': "∀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 (rule basic)
    have "(the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) oip) ≠ oip
           ⟶ oip∈kD(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 auto
       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: "∀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"
       and qinc: "∀j. quality_increases (σ j) (σ' j)"
       and *: "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)"
    from pre and qinc
      have pre': "∀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 (rule basic)
    have "∀dip∈kD(rt (σ i)).
           the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip) ≠ dip
           ⟶ dip∈kD(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 "∀dip∈kD(rt (σ i)). _ ⟶ ?dip_in_kD dip ∧ ?nsqn_le_nsqn dip")
     proof (intro ballI impI, split update_rt_split_asm)
       fix dip
       assume "dip∈kD(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 "dip∈kD(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' ‹dip∈kD(rt (σ i))› notdip
           show ?thesis by clarsimp
       next
         assume "dip = oip"
         with rtnot qinc ‹dip∈kD(rt (σ i))› notdip *
           have "?dip_in_kD dip"
            by simp (metis kD_quality_increases)
         moreover from ‹dip = oip› rtnot qinc ‹dip∈kD(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 oaddpreRT_welldefined]
                            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 "dip∈kD(rt (σ i))"
    shows "π₃(the (rt (σ i) dip)) = unk ∨ 1 ≤ π₂(the (rt (σ i) dip))"
    (is "?P dip")
  proof -
    have "∃l. l∈labels Γ_AODV p" by (metis aodv_ex_label)
    with assms(1) have "∀dip∈kD (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 ‹dip∈kD(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 "dip∈kD(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. l∈labels Γ_AODV p" by (metis aodv_ex_label)
    with assms(1) have "∀dip∈kD (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 ‹dip∈kD(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)) ⊏ (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. dip∈vD(rt (σ i))
                        ∧ dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))
                        ∧ (the (nhop (rt (σ i)) dip)) ≠ dip
                         ⟶ rt (σ i) ⊏ rt (σ (the (nhop (rt (σ i)) dip)))"
         and ow: "?S i σ σ' a"
      have "∀dip. dip∈vD(rt (σ i))
                  ∧ dip∈vD (rt (σ' (the (nhop (rt (σ i)) dip))))
                  ∧ (the (nhop (rt (σ i)) dip)) ≠ dip
               ⟶ rt (σ i) ⊏ rt (σ' (the (nhop (rt (σ i)) dip)))"
      proof clarify
        fix dip
        assume a2: "dip∈vD(rt (σ i))"
           and a3: "dip∈vD (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) ⊏ rt (σ' (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) ⊏ rt (σ (the (nhop (rt (σ i)) dip)))" by simp
          with ‹(the (nhop (rt (σ i)) dip)) = i› have "rt (σ i) ⊏ rt (σ 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 ‹dip∈vD (rt (σ' (the (nhop (rt (σ i)) dip))))›
            have "dip∈vD (rt (σ (the (nhop (rt (σ i)) dip))))" by simp
          with a1 a2 a4 have "rt (σ i) ⊏ rt (σ (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. dip∈vD(rt (σ i))
                      ∧ dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))
                      ∧ the (nhop (rt (σ i)) dip) ≠ dip
                      ⟶ rt (σ i) ⊏ rt (σ (the (nhop (rt (σ i)) dip)))"
         and ow: "?S i σ σ' a"
      have "∀dip. dip∈vD(update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {}))
           ∧ dip∈vD(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, {})
               ⊏ rt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip)))"
      proof clarify
        fix dip
        assume a2: "dip∈vD (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {}))"
           and a3: "dip∈vD(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, {})
              ⊏ rt (σ' (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 "dip∈vD(rt (σ i)) ∨ dip = sip"
            by (rule vD_update_val)
          with ‹dip ≠ sip› have "dip∈vD(rt (σ i))" by simp
          moreover from a3 have "dip∈vD(rt (σ' (the (nhop (rt (σ i)) dip))))" by simp
          moreover from a4 have "the (nhop (rt (σ i)) dip) ≠ dip" by simp
          ultimately have "rt (σ i) ⊏ rt (σ' (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. dip∈vD(rt (σ i)) ∧ dip∈vD(rt (σ (nhop dip))) ∧ nhop dip ≠ dip
                         ⟶ rt (σ i) ⊏ rt (σ (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) ⊏ rt (σ' (nhop dip))"
      proof clarify
        fix dip
        assume "dip∈vD(invalidate (rt (σ i)) (dests (σ i)))"
           and "dip∈vD(rt (σ' (nhop dip)))"
           and "nhop dip ≠ dip"
        from this(1) have "dip∈vD (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) ⊏ rt (σ (nhop dip))"
          using pre ‹dip ∈ vD (rt (σ' (nhop dip)))› ‹nhop dip ≠ dip›
          by metis
        with ‹∀j. j ≠ i ⟶ σ j = σ' j› show  "rt (σ i) ⊏ rt (σ' (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) ⊏ rt (σ (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 = σ i(rt := 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, {})
                 ⊏
                 rt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip)))"
      proof clarify
        fix dip
        assume a2: "dip∈vD(update (rt (σ i)) oip (osn, kno, val, Suc (hops), sip, {}))"
           and a3: "dip∈vD(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, {})
              ⊏
              rt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip)))"
          (is "?rt1 ⊏ ?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 "dip∈vD (rt (σ i))" by simp
          moreover from a3 have "dip∈vD(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) ⊏ rt (σ (the (nhop (rt (σ i)) dip)))"
            using pre by simp

          hence "rt (σ i) ⊏ rt (σ' (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 "dip∈kD(rt (σ' i))" by auto
          show ?thesis
          proof (cases "dip = oip")
            assume "dip ≠ oip"

            with a2 have "dip∈vD (rt (σ i))" by auto
            moreover with a3 a5 after and ‹dip ≠ oip›
              have "dip∈vD(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) ⊏ rt (σ (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 "oip∈kD(rt (σ sip))"
                     and "osn ≤ nsqn (rt (σ sip)) oip" by auto

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

            from ‹oip∈kD(rt (σ sip))›
            have "osn < nsqn (rt (σ' sip)) oip ∨ (osn = nsqn (rt (σ' sip)) oip
                                                   ∧ the (dhops (rt (σ' sip)) oip) ≤ hops)"
            proof
              assume "oip∈vD(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 ‹oip∈kD(rt (σ sip))› and ‹sip = i› show "oip∈kD(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, π₇ (the (rt (σ i) oip)))
                             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, π₇ (the (rt (σ i) oip)))
                             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, π₇ (the (rt (σ i) oip)))
                             else rt (σ i) a) = rt (σ i)" ..
                next
                  from ‹oip∈kD(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 "oip∈iD(rt (σ sip))"
              with ‹the (flag (rt (σ' sip)) oip) = val› and a5 have "sip = i"
                by (metis f.distinct(1) iD_flag_is_inv)
              from ‹oip∈iD(rt (σ sip))› have "the (flag (rt (σ sip)) oip) = inv" by auto
              with ‹sip = i› ‹Suc 0 ≤ osn› change after ‹oip∈kD(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 ‹dip∈kD(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 "oip∈kD(?rt1)" by simp
              moreover from a3 ‹dip = oip› have "oip∈kD(?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 "π₅(the (?rt2 oip oip)) < π₅(the (?rt1 oip))"
              proof -
                from osneq have "the (dhops (rt (σ' sip)) oip) ≤ hops" ..
                moreover from ‹oip ∈ vD (rt (σ' sip))› have "oip∈kD(rt (σ' sip))" by auto
                ultimately have "π₅(the (rt (σ' sip) oip)) ≤ hops"
                  by (auto simp add: proj5_eq_dhops)
                also from change after have "hops < π₅(the (rt (σ' i) oip))"
                  by (simp add: proj5_eq_dhops) (metis dhops_update_changed lessI)
                finally have "π₅(the (rt (σ' sip) oip)) < π₅(the (rt (σ' i) oip))" .
                with change after show ?thesis by simp
              qed

              ultimately have "?rt1 ⊏ ?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) ⊏ rt (σ (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]]
                                 onl_oinvariant_sterms [OF aodv_wf oaddpreRT_welldefined]
                        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. dip∈vD (rt (σ i))
                           ∧ dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))
                           ∧ the (nhop (rt (σ i)) dip) ≠ dip
                        ⟶ rt (σ i) ⊏ rt (σ (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: "∀dip∈kD (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) ⊏ rt (σ' (the (nhop (rt (σ' i)) dip)))"
        proof clarify
          fix dip
          assume "dip∈vD(rt (σ' i))"
             and "dip∈vD(rt (σ' (the (nhop (rt (σ' i)) dip))))"
             and "the (nhop (rt (σ' i)) dip) ≠ dip"
          from this(1) and ‹σ' i = σ i› have "dip∈vD(rt (σ i))"
                                         and "dip∈kD(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 ‹dip∈kD(rt (σ i))› and next_hop
            have "dip∈kD(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 ‹dip∈kD(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 ‹dip∈vD(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) ⊏ rt (σ' ?nhip)"
          proof (cases "dip∈vD(rt (σ ?nhip))")
            assume "dip∈vD(rt (σ ?nhip))"
            with pre ‹dip∈vD(rt (σ i))› and ‹?nhip ≠ dip›
              have "rt (σ i) ⊏ rt (σ ?nhip)" by auto
            moreover from ‹∀j. quality_increases (σ j) (σ' j)›
              have "quality_increases (σ ?nhip) (σ' ?nhip)" ..
            ultimately show ?thesis
              using ‹dip∈kD(rt (σ ?nhip))›
              by (rule strictly_fresher_quality_increases_right)
          next
            assume "dip∉vD(rt (σ ?nhip))"
            with ‹dip∈kD(rt (σ ?nhip))› have "dip∈iD(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 ‹dip∈iD(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 ‹dip∈vD(rt (σ' (the (nhop (rt (σ' i)) dip))))› and ‹σ' i = σ i›
                  show "dip∈vD(rt (σ' ?nhip))" by simp
              qed
            finally have "nsqn (rt (σ i)) dip < nsqn (rt (σ' ?nhip)) dip" .

            moreover from ‹dip∈vD(rt (σ' (the (nhop (rt (σ' i)) dip))))› and ‹σ' i = σ i›
              have "dip∈kD(rt (σ' ?nhip))" by auto
            ultimately show "rt (σ i) ⊏ rt (σ' ?nhip)"
              using ‹dip∈kD(rt (σ i))› by - (rule rt_strictly_fresher_ltI)
          qed
          with ‹σ' i = σ i› show "rt (σ' i) ⊏ rt (σ' (the (nhop (rt (σ' i)) dip)))"
            by simp
        qed
      qed
    thus ?thesis unfolding Let_def .
  qed

lemma seq_nhop_quality_increases:
  shows "opaodv i ⊨ (otherwith ((=)) {i}
                        (orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
                         other quality_increases {i} →)
                        global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
                                          in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
                                             ⟶ (rt (σ i)) ⊏ (rt (σ nhip)))"
  by (rule oinvariant_weakenE [OF seq_nhop_quality_increases']) (auto dest!: onlD)

end