Quelle  Seq_Invariants.thy

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

section "Invariant proofs on individual processes"

theory Seq_Invariants
imports AWN.Invariants Aodv Aodv_Data Aodv_Predicates Fresher

begin

text ‹
 The proposition numbers are taken from the December 2013 version of
 the Fehnker et al technical report.
 ›

text ‹Proposition 7.2›

lemma sequence_number_increases:
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), _, (ξ', _)). sn ξ ≤ sn ξ')"
  by inv_cterms

lemma sequence_number_one_or_bigger:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, _). 1 ≤ sn ξ)"
  by (rule onll_step_to_invariantI [OF sequence_number_increases])
     (auto simp: σ_{AODV_def})

text ‹We can get rid of the onl/onll if desired...›

lemma sequence_number_increases':
  "paodv i ⊨!!!_A (λ((ξ, _), _, (ξ', _)). sn ξ ≤ sn ξ')"
  by (rule step_invariant_weakenE [OF sequence_number_increases]) (auto dest!: onllD)

lemma sequence_number_one_or_bigger':
  "paodv i ⊨!!! (λ(ξ, _). 1 ≤ sn ξ)"
  by (rule invariant_weakenE [OF sequence_number_one_or_bigger]) auto

lemma sip_in_kD:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l). l ∈ ({PAodv-:7} ∪ {PAodv-:5} ∪ {PRrep-:0..PRrep-:1}
                                     ∪ {PRreq-:0..PRreq-:3}) ⟶ sip ξ ∈ kD (rt ξ))"
  by inv_cterms

lemma rrep_1_update_changes:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l). (l = PRrep-:1 ⟶
                        rt ξ ≠ update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {})))"
  by inv_cterms

lemma addpreRT_partly_welldefined:
  "paodv i ⊨!!!
     onl Γ_AODV (λ(ξ, l). (l ∈ {PRreq-:16..PRreq-:18} ∪ {PRrep-:2..PRrep-:6} ⟶ dip ξ ∈ kD (rt ξ))
                      ∧ (l ∈ {PRreq-:3..PRreq-:17} ⟶ oip ξ ∈ kD (rt ξ)))"
  by inv_cterms

text ‹Proposition 7.38›

lemma includes_nhip:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l). ∀dip∈kD(rt ξ). the (nhop (rt ξ) dip)∈kD(rt ξ))"
  proof -
    { fix ip and ξ ξ' :: state
      assume "∀dip∈kD (rt ξ). the (nhop (rt ξ) dip) ∈ kD (rt ξ)"
         and "ξ' = ξ(rt := update (rt ξ) ip (0, unk, val, Suc 0, ip, {}))"
      hence "∀dip∈kD (rt ξ).
               the (nhop (update (rt ξ) ip (0, unk, val, Suc 0, ip, {})) dip) = ip
             ∨ the (nhop (update (rt ξ) ip (0, unk, val, Suc 0, ip, {})) dip) ∈ kD (rt ξ)"
        by clarsimp (metis nhop_update_unk_val update_another)
    } note one_hop = this
    {  fix ip sip sn hops and ξ ξ' :: state
       assume "∀dip∈kD (rt ξ). the (nhop (rt ξ) dip) ∈ kD (rt ξ)"
          and "ξ' = ξ(rt := update (rt ξ) ip (sn, kno, val, Suc hops, sip, {}))"
          and "sip ∈ kD (rt ξ)"
       hence "(the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) ip) = ip
                 ∨ the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) ip) ∈ kD (rt ξ))
               ∧ (∀dip∈kD (rt ξ).
                    the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) dip) = ip
                    ∨ the (nhop (update (rt ξ) ip (sn, kno, val, Suc hops, sip, {})) dip) ∈ kD (rt ξ))"
         by (metis kD_update_unchanged nhop_update_changed update_another)
    } note nhip_is_sip = this
    show ?thesis
      by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf sip_in_kD]
                              onl_invariant_sterms [OF aodv_wf addpreRT_partly_welldefined]
                       solve: one_hop nhip_is_sip)
  qed

text ‹Proposition 7.22: needed in Proposition 7.4›

lemma addpreRT_welldefined:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l). (l ∈ {PRreq-:16..PRreq-:18} ⟶ dip ξ ∈ kD (rt ξ)) ∧
                               (l = PRreq-:17 ⟶ oip ξ ∈ kD (rt ξ)) ∧
                               (l = PRrep-:5 ⟶ dip ξ ∈ kD (rt ξ)) ∧
                               (l = PRrep-:6 ⟶ (the (nhop (rt ξ) (dip ξ))) ∈ kD (rt ξ)))"
  (is "_ ⊨!!! onl Γ_AODV ?P")
  unfolding invariant_def
  proof
    fix s
    assume "s ∈ reachable (paodv i) TT"
    then obtain ξ p where "s = (ξ, p)"
                      and "(ξ, p) ∈ reachable (paodv i) TT"
      by (metis prod.exhaust)
    have "onl Γ_AODV ?P (ξ, p)"
    proof (rule onlI)
      fix l
      assume "l ∈ labels Γ_AODV p"
      with ‹(ξ, p) ∈ reachable (paodv i) TT›
        have I1: "l ∈ {PRreq-:16..PRreq-:18} ⟶ dip ξ ∈ kD(rt ξ)"
         and I2: "l = PRreq-:17 ⟶ oip ξ ∈ kD(rt ξ)"
         and I3: "l ∈ {PRrep-:2..PRrep-:6} ⟶ dip ξ ∈ kD(rt ξ)"
         by (auto dest!: invariantD [OF addpreRT_partly_welldefined])
      moreover from ‹(ξ, p) ∈ reachable (paodv i) TT› ‹l ∈ labels Γ_AODV p› and I3
        have "l = PRrep-:6 ⟶ (the (nhop (rt ξ) (dip ξ))) ∈ kD(rt ξ)"
          by (auto dest!: invariantD [OF includes_nhip])
      ultimately show "?P (ξ, l)"
        by simp
    qed
    with ‹s = (ξ, p)› show "onl Γ_AODV ?P s"
      by simp
  qed

text ‹Proposition 7.4›

lemma known_destinations_increase:
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), _, (ξ', _)). kD (rt ξ) ⊆ kD (rt ξ'))"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined]
                 simp add: subset_insertI)

text ‹Proposition 7.5›

lemma rreqs_increase:
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), _, (ξ', _)). rreqs ξ ⊆ rreqs ξ')"
  by (inv_cterms simp add: subset_insertI)

lemma dests_bigger_than_sqn:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l). l ∈ {PAodv-:15..PAodv-:19}
                                 ∪ {PPkt-:7..PPkt-:11}
                                 ∪ {PRreq-:9..PRreq-:13}
                                 ∪ {PRreq-:21..PRreq-:25}
                                 ∪ {PRrep-:10..PRrep-:14}
                                 ∪ {PRerr-:1..PRerr-:5}
                         ⟶ (∀ip∈dom(dests ξ). ip∈kD(rt ξ) ∧ sqn (rt ξ) ip ≤ the (dests ξ ip)))"
  proof -
    have sqninv:
      "∧dests rt rsn ip.
       [ ∀ip∈dom(dests). ip∈kD(rt) ∧ sqn rt ip ≤ the (dests ip); dests ip = Some rsn ]
        ==> sqn (invalidate rt dests) ip ≤ rsn"
        by (rule sqn_invalidate_in_dests [THEN eq_imp_le], assumption) auto
    have indests:
      "∧dests rt rsn ip.
       [ ∀ip∈dom(dests). ip∈kD(rt) ∧ sqn rt ip ≤ the (dests ip); dests ip = Some rsn ]
        ==> ip∈kD(rt) ∧ sqn rt ip ≤ rsn"
        by (metis domI option.sel)
    show ?thesis
      by inv_cterms
         (clarsimp split: if_split_asm option.split_asm
                   elim!: sqninv indests)+
  qed

text ‹Proposition 7.6›

lemma sqns_increase:
   "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), _, (ξ', _)). ∀ip. sqn (rt ξ) ip ≤ sqn (rt ξ') ip)"
  proof -
    { fix ξ :: state
      assume *: "∀ip∈dom(dests ξ). ip ∈ kD (rt ξ) ∧ sqn (rt ξ) ip ≤ the (dests ξ ip)"
      have "∀ip. sqn (rt ξ) ip ≤ sqn (invalidate (rt ξ) (dests ξ)) ip"
      proof
        fix ip
        from * have "ip∉dom(dests ξ) ∨ sqn (rt ξ) ip ≤ the (dests ξ ip)" by simp
        thus "sqn (rt ξ) ip ≤ sqn (invalidate (rt ξ) (dests ξ)) ip"
          by (metis domI invalidate_sqn option.sel)
      qed
    } note solve_invalidate = this
    show ?thesis
      by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined]
                              onl_invariant_sterms [OF aodv_wf dests_bigger_than_sqn]
                    simp add: solve_invalidate)
  qed

text ‹Proposition 7.7›

lemma ip_constant:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, _). ip ξ = i)"
  by (inv_cterms simp add: σ_{AODV_def})

text ‹Proposition 7.8›

lemma sender_ip_valid':
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), a, _). anycast (λm. not_Pkt m ⟶ msg_sender m = ip ξ) a)"
  by inv_cterms

lemma sender_ip_valid:
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), a, _). anycast (λm. not_Pkt m ⟶ msg_sender m = i) a)"
  by (rule step_invariant_weaken_with_invariantE [OF ip_constant sender_ip_valid'])
     (auto dest!: onlD onllD)

lemma received_msg_inv:
  "paodv i ⊨!!! (recvmsg P →) onl Γ_AODV (λ(ξ, l). l ∈ {PAodv-:1} ⟶ P (msg ξ))"
  by inv_cterms

text ‹Proposition 7.9›

lemma sip_not_ip':
  "paodv i ⊨!!! (recvmsg (λm. not_Pkt m ⟶ msg_sender m ≠ i) →) onl Γ_AODV (λ(ξ, _). sip ξ ≠ ip ξ)"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]
                          onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
                simp add: clear_locals_sip_not_ip') clarsimp+

lemma sip_not_ip:
  "paodv i ⊨!!! (recvmsg (λm. not_Pkt m ⟶ msg_sender m ≠ i) →) onl Γ_AODV (λ(ξ, _). sip ξ ≠ i)"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]
                          onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
                simp add: clear_locals_sip_not_ip') clarsimp+

text ‹Neither ‹sip_not_ip'› nor ‹sip_not_ip› is needed to show loop freedom.›

text ‹Proposition 7.10›

lemma hop_count_positive:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, _). ∀ip∈kD (rt ξ). the (dhops (rt ξ) ip) ≥ 1)"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined]) auto

lemma rreq_dip_in_vD_dip_eq_ip:
  "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l). (l ∈ {PRreq-:16..PRreq-:18} ⟶ dip ξ ∈ vD(rt ξ))
                            ∧ (l ∈ {PRreq-:5, PRreq-:6} ⟶ dip ξ = ip ξ)
                            ∧ (l ∈ {PRreq-:15..PRreq-:18} ⟶ dip ξ ≠ ip ξ))"
  proof (inv_cterms, elim conjE)
    fix l ξ pp p'
    assume "(ξ, pp) ∈ reachable (paodv i) TT"
       and "{PRreq-:17}[λξ. ξ(rt := the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}))] p'
              ∈ sterms Γ_AODV pp"
       and "l = PRreq-:17"
       and "dip ξ ∈ vD (rt ξ)"
    from this(1-3) have "oip ξ ∈ kD (rt ξ)"
      by (auto dest: onl_invariant_sterms [OF aodv_wf addpreRT_welldefined, where l="PRreq-:17"])
    with ‹dip ξ ∈ vD (rt ξ)›
      show "dip ξ ∈ vD (the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}))" by simp
  qed

text ‹Proposition 7.11›

lemma anycast_msg_zhops:
  "∧rreqid dip dsn dsk oip osn sip.
      paodv i ⊨!!!_A onll Γ_AODV (λ(_, a, _). anycast msg_zhops a)"
  proof (inv_cterms inv add:
           onl_invariant_sterms [OF aodv_wf rreq_dip_in_vD_dip_eq_ip [THEN invariant_restrict_inD]]
           onl_invariant_sterms [OF aodv_wf hop_count_positive [THEN invariant_restrict_inD]],
         elim conjE)
    fix l ξ a pp p' pp'
    assume "(ξ, pp) ∈ reachable (paodv i) TT"
       and "{PRreq-:18}unicast(λξ. the (nhop (rt ξ) (oip ξ)),
               λξ. Rrep (the (dhops (rt ξ) (dip ξ))) (dip ξ) (sqn (rt ξ) (dip ξ)) (oip ξ) (ip ξ)).
                     p' ▹ pp' ∈ sterms Γ_AODV pp"
       and "l = PRreq-:18"
       and "a = unicast (the (nhop (rt ξ) (oip ξ)))
                 (Rrep (the (dhops (rt ξ) (dip ξ))) (dip ξ) (sqn (rt ξ) (dip ξ)) (oip ξ) (ip ξ))"
       and *: "∀ip∈kD (rt ξ). Suc 0 ≤ the (dhops (rt ξ) ip)"
       and "dip ξ ∈ vD (rt ξ)"
    from ‹dip ξ ∈ vD (rt ξ)› have "dip ξ ∈ kD (rt ξ)"
      by (rule vD_iD_gives_kD(1))
    with * have "Suc 0 ≤ the (dhops (rt ξ) (dip ξ))" ..
    thus "0 < the (dhops (rt ξ) (dip ξ))" by simp
  qed

lemma hop_count_zero_oip_dip_sip:
  "paodv i ⊨!!! (recvmsg msg_zhops →) onl Γ_AODV (λ(ξ, l).
                 (l∈{PAodv-:4..PAodv-:5} ∪ {PRreq-:n|n. True} ⟶
                          (hops ξ = 0 ⟶ oip ξ = sip ξ))
                 ∧
                 ((l∈{PAodv-:6..PAodv-:7} ∪ {PRrep-:n|n. True} ⟶
                          (hops ξ = 0 ⟶ dip ξ = sip ξ))))"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) auto

lemma osn_rreq:
  "paodv i ⊨!!! (recvmsg rreq_rrep_sn →) onl Γ_AODV (λ(ξ, l).
                                    l ∈ {PAodv-:4, PAodv-:5} ∪ {PRreq-:n|n. True} ⟶ 1 ≤ osn ξ)"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) clarsimp

lemma osn_rreq':
  "paodv i ⊨!!! (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ_AODV (λ(ξ, l).
                                    l ∈ {PAodv-:4, PAodv-:5} ∪ {PRreq-:n|n. True} ⟶ 1 ≤ osn ξ)"
  proof (rule invariant_weakenE [OF osn_rreq])
    fix a
    assume "recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) a"
    thus "recvmsg rreq_rrep_sn a"
      by (cases a) simp_all
  qed

lemma dsn_rrep:
  "paodv i ⊨!!! (recvmsg rreq_rrep_sn →) onl Γ_AODV (λ(ξ, l).
                                    l ∈ {PAodv-:6, PAodv-:7} ∪ {PRrep-:n|n. True} ⟶ 1 ≤ dsn ξ)"
  by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]) clarsimp

lemma dsn_rrep':
  "paodv i ⊨!!! (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ_AODV (λ(ξ, l).
                                    l ∈ {PAodv-:6, PAodv-:7} ∪ {PRrep-:n|n. True} ⟶ 1 ≤ dsn ξ)"
  proof (rule invariant_weakenE [OF dsn_rrep])
    fix a
    assume "recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) a"
    thus "recvmsg rreq_rrep_sn a"
      by (cases a) simp_all
  qed

lemma hop_count_zero_oip_dip_sip':
  "paodv i ⊨!!! (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ_AODV (λ(ξ, l).
                 (l∈{PAodv-:4..PAodv-:5} ∪ {PRreq-:n|n. True} ⟶
                          (hops ξ = 0 ⟶ oip ξ = sip ξ))
                 ∧
                 ((l∈{PAodv-:6..PAodv-:7} ∪ {PRrep-:n|n. True} ⟶
                          (hops ξ = 0 ⟶ dip ξ = sip ξ))))"
  proof (rule invariant_weakenE [OF hop_count_zero_oip_dip_sip])
    fix a
    assume "recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) a"
    thus "recvmsg msg_zhops a"
      by (cases a) simp_all
  qed

text ‹Proposition 7.12›

lemma zero_seq_unk_hops_one':
  "paodv i ⊨!!! (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ_AODV (λ(ξ, _).
                 ∀dip∈kD(rt ξ). (sqn (rt ξ) dip = 0 ⟶ sqnf (rt ξ) dip = unk)
                              ∧ (sqnf (rt ξ) dip = unk ⟶ the (dhops (rt ξ) dip) = 1)
                              ∧ (the (dhops (rt ξ) dip) = 1 ⟶ the (nhop (rt ξ) dip) = dip))"
  proof -
  { fix dip and ξ :: state and P
    assume "sqn (invalidate (rt ξ) (dests ξ)) dip = 0"
       and all: "∀ip. sqn (rt ξ) ip ≤ sqn (invalidate (rt ξ) (dests ξ)) ip"
       and *: "sqn (rt ξ) dip = 0 ==> P ξ dip"
    have "P ξ dip"
    proof -
      from all have "sqn (rt ξ) dip ≤ sqn (invalidate (rt ξ) (dests ξ)) dip" ..
      with ‹sqn (invalidate (rt ξ) (dests ξ)) dip = 0› have "sqn (rt ξ) dip = 0" by simp
      thus "P ξ dip" by (rule *)
    qed
  } note sqn_invalidate_zero [elim!] = this

  { fix dsn hops :: nat and sip oip rt and ip dip :: ip
    assume "∀dip∈kD(rt).
                (sqn rt dip = 0 ⟶ π₃(the (rt dip)) = unk) ∧
                (π₃(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
                (the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
       and "hops = 0 ⟶ sip = dip"
       and "Suc 0 ≤ dsn"
       and "ip ≠ dip ⟶ ip∈kD(rt)"
    hence "the (dhops (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip) = Suc 0 ⟶
           the (nhop (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip) = ip"
      by - (rule update_cases, auto simp add: sqn_def dest!: bspec)
  } note prreq_ok1 [simp] = this

  { fix ip dsn hops sip oip rt dip
    assume "∀dip∈kD(rt).
                (sqn rt dip = 0 ⟶ π₃(the (rt dip)) = unk) ∧
                (π₃(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
                (the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
       and "Suc 0 ≤ dsn"
       and "ip ≠ dip ⟶ ip∈kD(rt)"
    hence "π₃(the (update rt dip (dsn, kno, val, Suc hops, sip, {}) ip)) = unk ⟶
           the (dhops (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip) = Suc 0"
      by - (rule update_cases, auto simp add: sqn_def sqnf_def dest!: bspec)
  } note prreq_ok2 [simp] = this

  { fix ip dsn hops sip oip rt dip
    assume "∀dip∈kD(rt).
                (sqn rt dip = 0 ⟶ π₃(the (rt dip)) = unk) ∧
                (π₃(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
                (the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
       and "Suc 0 ≤ dsn"
       and "ip ≠ dip ⟶ ip∈kD(rt)"
    hence "sqn (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip = 0 ⟶
           π₃ (the (update rt dip (dsn, kno, val, Suc hops, sip, {}) ip)) = unk"
      by - (rule update_cases, auto simp add: sqn_def dest!: bspec)
  } note prreq_ok3 [simp] = this

  { fix rt sip
    assume "∀dip∈kD rt.
              (sqn rt dip = 0 ⟶ π₃(the (rt dip)) = unk) ∧
              (π₃(the (rt dip)) = unk ⟶ the (dhops rt dip) = Suc 0) ∧
              (the (dhops rt dip) = Suc 0 ⟶ the (nhop rt dip) = dip)"
    hence "∀dip∈kD rt.
          (sqn (update rt sip (0, unk, val, Suc 0, sip, {})) dip = 0 ⟶
           π₃(the (update rt sip (0, unk, val, Suc 0, sip, {}) dip)) = unk)
        ∧ (π₃(the (update rt sip (0, unk, val, Suc 0, sip, {}) dip)) = unk ⟶
           the (dhops (update rt sip (0, unk, val, Suc 0, sip, {})) dip) = Suc 0)
        ∧ (the (dhops (update rt sip (0, unk, val, Suc 0, sip, {})) dip) = Suc 0 ⟶
           the (nhop (update rt sip (0, unk, val, Suc 0, sip, {})) dip) = dip)"
    by - (rule update_cases, simp_all add: sqnf_def sqn_def)
  } note prreq_ok4 [simp] = this

  have prreq_ok5 [simp]: "∧sip rt.
    π₃(the (update rt sip (0, unk, val, Suc 0, sip, {}) sip)) = unk ⟶
    the (dhops (update rt sip (0, unk, val, Suc 0, sip, {})) sip) = Suc 0"
    by (rule update_cases) simp_all

  have prreq_ok6 [simp]: "∧sip rt.
    sqn (update rt sip (0, unk, val, Suc 0, sip, {})) sip = 0 ⟶
    π₃ (the (update rt sip (0, unk, val, Suc 0, sip, {}) sip)) = unk"
    by (rule update_cases) simp_all

  show ?thesis
    by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]
                            onl_invariant_sterms [OF aodv_wf hop_count_zero_oip_dip_sip']
                            seq_step_invariant_sterms_TT [OF sqns_increase aodv_wf aodv_trans]
                            onl_invariant_sterms [OF aodv_wf osn_rreq']
                            onl_invariant_sterms [OF aodv_wf dsn_rrep']) clarsimp+
  qed

lemma zero_seq_unk_hops_one:
  "paodv i ⊨!!! (recvmsg (λm. rreq_rrep_sn m ∧ msg_zhops m) →) onl Γ_AODV (λ(ξ, _).
                 ∀dip∈kD(rt ξ). (sqn (rt ξ) dip = 0 ⟶ (sqnf (rt ξ) dip = unk
                                                         ∧ the (dhops (rt ξ) dip) = 1
                                                         ∧ the (nhop (rt ξ) dip) = dip)))"
  by (rule invariant_weakenE [OF zero_seq_unk_hops_one']) auto

lemma kD_unk_or_atleast_one:
  "paodv i ⊨!!! (recvmsg rreq_rrep_sn →) onl Γ_AODV (λ(ξ, l).
                               ∀dip∈kD(rt ξ). π₃(the (rt ξ dip)) = unk ∨ 1 ≤ π₂(the (rt ξ dip)))"
  proof -
    { fix sip rt dsn1 dsn2 dsk1 dsk2 flag1 flag2 hops1 hops2 nhip1 nhip2 pre1 pre2
      assume "dsk1 = unk ∨ Suc 0 ≤ dsn2"
      hence "π₃(the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1, pre1) sip)) = unk
            ∨ Suc 0 ≤ sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2, pre2)) sip"
        unfolding update_def by (cases "dsk1 =unk") (clarsimp split: option.split)+
    } note fromsip [simp] = this

    { fix dip sip rt dsn1 dsn2 dsk1 dsk2 flag1 flag2 hops1 hops2 nhip1 nhip2 pre1 pre2
      assume allkd: "∀dip∈kD(rt). π₃(the (rt dip)) = unk ∨ Suc 0 ≤ sqn rt dip"
         and    **: "dsk1 = unk ∨ Suc 0 ≤ dsn2"
      have "∀dip∈kD(rt). π₃(the (update rt sip (dsn1, dsk1, flag1, hops1, nhip1, pre1) dip)) = unk
            ∨ Suc 0 ≤ sqn (update rt sip (dsn2, dsk2, flag2, hops2, nhip2, pre2)) dip"
        (is "∀dip∈kD(rt). ?prop dip")
      proof
        fix dip
        assume "dip∈kD(rt)"
        thus "?prop dip"
        proof (cases "dip = sip")
          assume "dip = sip"
          with ** show ?thesis
            by simp
        next
          assume "dip ≠ sip"
          with ‹dip∈kD(rt)› allkd show ?thesis
            by simp
        qed
      qed
    } note solve_update [simp] = this

    { fix dip rt dests
      assume  *: "∀ip∈dom(dests). ip∈kD(rt) ∧ sqn rt ip ≤ the (dests ip)"
         and **: "∀ip∈kD(rt). π₃(the (rt ip)) = unk ∨ Suc 0 ≤ sqn rt ip"
      have "∀dip∈kD(rt). π₃(the (rt dip)) = unk ∨ Suc 0 ≤ sqn (invalidate rt dests) dip"
      proof
        fix dip
        assume "dip∈kD(rt)"
        with ** have "π₃(the (rt dip)) = unk ∨ Suc 0 ≤ sqn rt dip" ..
        thus "π₃ (the (rt dip)) = unk ∨ Suc 0 ≤ sqn (invalidate rt dests) dip"
        proof
          assume "π₃(the (rt dip)) = unk" thus ?thesis ..
        next
          assume "Suc 0 ≤ sqn rt dip"
          have "Suc 0 ≤ sqn (invalidate rt dests) dip"
          proof (cases "dip∈dom(dests)")
            assume "dip∈dom(dests)"
            with * have "sqn rt dip ≤ the (dests dip)" by simp
            with ‹Suc 0 ≤ sqn rt dip› have "Suc 0 ≤ the (dests dip)" by simp
            with ‹dip∈dom(dests)› ‹dip∈kD(rt)› [THEN kD_Some] show ?thesis
              unfolding invalidate_def sqn_def by auto
          next
            assume "dip∉dom(dests)"
            with ‹Suc 0 ≤ sqn rt dip› ‹dip∈kD(rt)› [THEN kD_Some] show ?thesis
              unfolding invalidate_def sqn_def by auto
          qed
        thus ?thesis by (rule disjI2)
        qed
      qed
    } note solve_invalidate [simp] = this

    show ?thesis
      by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]
                              onl_invariant_sterms [OF aodv_wf dests_bigger_than_sqn
                                                               [THEN invariant_restrict_inD]]
                              onl_invariant_sterms [OF aodv_wf osn_rreq]
                              onl_invariant_sterms [OF aodv_wf dsn_rrep]
                    simp add: proj3_inv proj2_eq_sqn)
  qed

text ‹Proposition 7.13›

lemma rreq_rrep_sn_any_step_invariant:
  "paodv i ⊨!!!_A (recvmsg rreq_rrep_sn →) onll Γ_AODV (λ(_, a, _). anycast rreq_rrep_sn a)"
  proof -
    have sqnf_kno: "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l).
                                      (l ∈ {PRreq-:16..PRreq-:18} ⟶ sqnf (rt ξ) (dip ξ) = kno))"
      by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined])
    show ?thesis
      by (inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]
                              onl_invariant_sterms [OF aodv_wf sequence_number_one_or_bigger
                                                               [THEN invariant_restrict_inD]]
                              onl_invariant_sterms [OF aodv_wf kD_unk_or_atleast_one]
                              onl_invariant_sterms_TT [OF aodv_wf sqnf_kno]
                              onl_invariant_sterms [OF aodv_wf osn_rreq]
                              onl_invariant_sterms [OF aodv_wf dsn_rrep])
         (auto simp: proj2_eq_sqn)
  qed

text ‹Proposition 7.14›

lemma rreq_rrep_fresh_any_step_invariant:
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a)"
  proof -                                                      
    have rreq_oip: "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l).
                       (l ∈ {PRreq-:3, PRreq-:4, PRreq-:15, PRreq-:27}
                               ⟶ oip ξ ∈ kD(rt ξ)
                                 ∧ (sqn (rt ξ) (oip ξ) > (osn ξ)
                                     ∨ (sqn (rt ξ) (oip ξ) = (osn ξ)
                                        ∧ the (dhops (rt ξ) (oip ξ)) ≤ Suc (hops ξ)
                                        ∧ the (flag (rt ξ) (oip ξ)) = val))))"
      proof inv_cterms
        fix l ξ l' pp p'
        assume "(ξ, pp) ∈ reachable (paodv i) TT"
           and "{PRreq-:2}[λξ. ξ(rt :=
                update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {}))] p' ∈ sterms Γ_AODV pp"
           and "l' = PRreq-:3"
        show "osn ξ < sqn (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ)
           ∨ (sqn (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ) = osn ξ
             ∧ the (dhops (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ))
                                                                            ≤ Suc (hops ξ)
             ∧ the (flag (update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})) (oip ξ))
                                                                            = val)"
          unfolding update_def by (clarsimp split: option.split)
                                  (metis linorder_neqE_nat not_less)
      qed

    have rrep_prrep: "paodv i ⊨!!! onl Γ_AODV (λ(ξ, l).
          (l ∈ {PRrep-:2..PRrep-:7} ⟶ (dip ξ ∈ kD(rt ξ)
                                        ∧ sqn (rt ξ) (dip ξ) = dsn ξ
                                        ∧ the (dhops (rt ξ) (dip ξ)) = Suc (hops ξ)
                                        ∧ the (flag (rt ξ) (dip ξ)) = val
                                        ∧ the (nhop (rt ξ) (dip ξ)) ∈ kD (rt ξ))))"
      by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rrep_1_update_changes]
                              onl_invariant_sterms [OF aodv_wf sip_in_kD])

    show ?thesis
      by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rreq_oip]
                              onl_invariant_sterms [OF aodv_wf rreq_dip_in_vD_dip_eq_ip]
                              onl_invariant_sterms [OF aodv_wf rrep_prrep])
  qed

text ‹Proposition 7.15›

lemma rerr_invalid_any_step_invariant:
  "paodv i ⊨!!!_A onll Γ_AODV (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a)"
  proof -
    have dests_inv: "paodv i ⊨!!!
                      onl Γ_AODV (λ(ξ, l). (l ∈ {PAodv-:15, PPkt-:7, PRreq-:9,
                                            PRreq-:21, PRrep-:10, PRerr-:1}
                          ⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ)))
                         ∧ (l ∈ {PAodv-:16..PAodv-:19}
                              ∪ {PPkt-:8..PPkt-:11}
                              ∪ {PRreq-:10..PRreq-:13}
                              ∪ {PRreq-:22..PRreq-:25}
                              ∪ {PRrep-:11..PRrep-:14}
                              ∪ {PRerr-:2..PRerr-:5} ⟶ (∀ip∈dom(dests ξ). ip∈iD(rt ξ)
                                                          ∧ the (dests ξ ip) = sqn (rt ξ) ip))
                         ∧ (l = PPkt-:14 ⟶ dip ξ∈iD(rt ξ)))"
      by inv_cterms (clarsimp split: if_split_asm option.split_asm simp: domIff)+
    show ?thesis
      by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf dests_inv])
  qed

text ‹Proposition 7.16›

text ‹
 Some well-definedness obligations are irrelevant for the Isabelle development:

 \begin{enumerate}
 \item In each routing table there is at most one entry for each destination: guaranteed by type.

 \item In each store of queued data packets there is at most one data queue for
 each destination: guaranteed by structure.

 \item Whenever a set of pairs @{term "(rip, rsn)"} is assigned to the variable
 @{term "dests"} of type @{typ "ip ⇀ sqn"}, or to the first argument of
 the function @{term "rerr"}, this set is a partial function, i.e., there
 is at most one entry @{term "(rip, rsn)"} for each destination
 @{term "rip"}: guaranteed by type.
 \end{enumerate}
 ›

lemma dests_vD_inc_sqn:
  "paodv i ⊨!!!
        onl Γ_AODV (λ(ξ, l). (l ∈ {PAodv-:15, PPkt-:7, PRreq-:9, PRreq-:21, PRrep-:10}
             ⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ) ∧ the (dests ξ ip) = inc (sqn (rt ξ) ip)))
           ∧ (l = PRerr-:1
             ⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ) ∧ the (dests ξ ip) > sqn (rt ξ) ip)))"
  by inv_cterms (clarsimp split: if_split_asm option.split_asm)+

text ‹Proposition 7.27›

lemma route_tables_fresher:
  "paodv i ⊨!!!_A (recvmsg rreq_rrep_sn →) onll Γ_AODV (λ((ξ, _), _, (ξ', _)).
                                                                ∀dip∈kD(rt ξ). rt ξ ⊑ rt ξ')"
  proof (inv_cterms inv add:
           onl_invariant_sterms [OF aodv_wf dests_vD_inc_sqn [THEN invariant_restrict_inD]]
           onl_invariant_sterms [OF aodv_wf hop_count_positive [THEN invariant_restrict_inD]]
           onl_invariant_sterms [OF aodv_wf osn_rreq]
           onl_invariant_sterms [OF aodv_wf dsn_rrep]
           onl_invariant_sterms [OF aodv_wf addpreRT_welldefined [THEN invariant_restrict_inD]])
    fix ξ pp p'
    assume "(ξ, pp) ∈ reachable (paodv i) (recvmsg rreq_rrep_sn)"
       and "{PRreq-:2}[λξ. ξ(rt := update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {}))]
               p' ∈ sterms Γ_AODV pp"
       and "Suc 0 ≤ osn ξ"
       and *: "∀ip∈kD (rt ξ). Suc 0 ≤ the (dhops (rt ξ) ip)"
    show "∀ip∈kD (rt ξ). rt ξ ⊑ update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
    proof
      fix ip
      assume "ip∈kD (rt ξ)"
      moreover with * have "1 ≤ the (dhops (rt ξ) ip)" by simp
      moreover from ‹Suc 0 ≤ osn ξ›
        have "update_arg_wf (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})" ..
      ultimately show "rt ξ ⊑ update (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
        by (rule rt_fresher_update)
    qed
  next
    fix ξ pp p'
    assume "(ξ, pp) ∈ reachable (paodv i) (recvmsg rreq_rrep_sn)"
       and "{PRrep-:1}[λξ. ξ(rt := update (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {}))]
            p' ∈ sterms Γ_AODV pp"
       and "Suc 0 ≤ dsn ξ"
       and *: "∀ip∈kD (rt ξ). Suc 0 ≤ the (dhops (rt ξ) ip)"
    show "∀ip∈kD (rt ξ). rt ξ ⊑ update (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
    proof
      fix ip
      assume "ip∈kD (rt ξ)"
      moreover with * have "1 ≤ the (dhops (rt ξ) ip)" by simp
      moreover from ‹Suc 0 ≤ dsn ξ›
        have "update_arg_wf (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})" ..
      ultimately show "rt ξ ⊑ update (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
        by (rule rt_fresher_update)
    qed
  qed

end