Theory D_Seq_Invariants

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

section "Invariant proofs on individual processes"

theory D_Seq_Invariants
imports AWN.Invariants D_Aodv D_Aodv_Data D_Aodv_Predicates D_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-:18..PRreq-:20}  {PRrep-:2..PRrep-:6}  dip ξ  kD (rt ξ))
                       (l  {PRreq-:3..PRreq-:19}  oip ξ  kD (rt ξ)))"
  by inv_cterms

text ‹Proposition 7.38›

lemma includes_nhip:
  "paodv i  onl ΓAODV (λ(ξ, l). dipkD(rt ξ). the (nhop (rt ξ) dip)kD(rt ξ))"
  proof -
    { fix ip and ξ ξ' :: state
      assume "dipkD (rt ξ). the (nhop (rt ξ) dip)  kD (rt ξ)"
         and "ξ' = ξrt := update (rt ξ) ip (0, unk, val, Suc 0, ip, {})"
      hence "dipkD (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 "dipkD (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 ξ))
                (dipkD (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-:18..PRreq-:20}  dip ξ  kD (rt ξ)) 
                               (l = PRreq-:19  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-:18..PRreq-:20}  dip ξ  kD(rt ξ)"
         and I2: "l = PRreq-:19  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-:11..PRreq-:15}
                                  {PRreq-:24..PRreq-:28}
                                  {PRrep-:10..PRrep-:14}
                                  {PRerr-:1..PRerr-:5}
                          (ipdom(dests ξ). ipkD(rt ξ)  sqn (rt ξ) ip  the (dests ξ ip)))"
  proof -
    have sqninv:
      "dests rt rsn ip.
        ipdom(dests). ipkD(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.
        ipdom(dests). ipkD(rt)  sqn rt ip  the (dests ip); dests ip = Some rsn 
         ipkD(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 *: "ipdom(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 "ipdom(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 (λ(ξ, _). ipkD (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-:18..PRreq-:21}  dip ξ  vD(rt ξ))
                             (l  {PRreq-:6, PRreq-:7}  dip ξ = ip ξ)
                             (l  {PRreq-:17..PRreq-:21}  dip ξ  ip ξ))"
  proof (inv_cterms, elim conjE)
    fix l ξ pp p'
    assume "(ξ, pp)  reachable (paodv i) TT"
       and "{PRreq-:19}λξ. ξrt := the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}) p'
               sterms ΓAODV pp"
       and "l = PRreq-:19"
       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-:19"])
    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-:20}unicast(λξ. the (nhop (rt ξ) (oip ξ)),
               λξ. Rrep (the (dhops (rt ξ) (dip ξ))) (dip ξ) (sqn (rt ξ) (dip ξ)) (oip ξ) (ip ξ)).
                     p'  pp'  sterms ΓAODV pp"
       and "l = PRreq-:20"
       and "a = unicast (the (nhop (rt ξ) (oip ξ)))
                 (Rrep (the (dhops (rt ξ) (dip ξ))) (dip ξ) (sqn (rt ξ) (dip ξ)) (oip ξ) (ip ξ))"
       and *: "ipkD (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 (λ(ξ, _).
                 dipkD(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 "dipkD(rt).
                (sqn rt dip = 0  π3(the (rt dip)) = unk) 
                (π3(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  ipkD(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 "dipkD(rt).
                (sqn rt dip = 0  π3(the (rt dip)) = unk) 
                (π3(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  ipkD(rt)"
    hence "π3(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 "dipkD(rt).
                (sqn rt dip = 0  π3(the (rt dip)) = unk) 
                (π3(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  ipkD(rt)"
    hence "sqn (update rt dip (dsn, kno, val, Suc hops, sip, {})) ip = 0 
           π3 (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 "dipkD rt.
              (sqn rt dip = 0  π3(the (rt dip)) = unk) 
              (π3(the (rt dip)) = unk  the (dhops rt dip) = Suc 0) 
              (the (dhops rt dip) = Suc 0  the (nhop rt dip) = dip)"
    hence "dipkD rt.
          (sqn (update rt sip (0, unk, val, Suc 0, sip, {})) dip = 0 
           π3(the (update rt sip (0, unk, val, Suc 0, sip, {}) dip)) = unk)
         (π3(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.
    π3(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 
    π3 (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 (λ(ξ, _).
                 dipkD(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).
                               dipkD(rt ξ). π3(the (rt ξ dip)) = unk  1  π2(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 "π3(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: "dipkD(rt). π3(the (rt dip)) = unk  Suc 0  sqn rt dip"
         and    **: "dsk1 = unk  Suc 0  dsn2"
      have "dipkD(rt). π3(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 "dipkD(rt). ?prop dip")
      proof
        fix dip
        assume "dipkD(rt)"
        thus "?prop dip"
        proof (cases "dip = sip")
          assume "dip = sip"
          with ** show ?thesis
            by simp
        next
          assume "dip  sip"
          with dipkD(rt) allkd show ?thesis
            by simp
        qed
      qed
    } note solve_update [simp] = this

    { fix dip rt dests
      assume  *: "ipdom(dests). ipkD(rt)  sqn rt ip  the (dests ip)"
         and **: "ipkD(rt). π3(the (rt ip)) = unk  Suc 0  sqn rt ip"
      have "dipkD(rt). π3(the (rt dip)) = unk  Suc 0  sqn (invalidate rt dests) dip"
      proof
        fix dip
        assume "dipkD(rt)"
        with ** have "π3(the (rt dip)) = unk  Suc 0  sqn rt dip" ..
        thus "π3 (the (rt dip)) = unk  Suc 0  sqn (invalidate rt dests) dip"
        proof
          assume "π3(the (rt dip)) = unk" thus ?thesis ..
        next
          assume "Suc 0  sqn rt dip"
          have "Suc 0  sqn (invalidate rt dests) dip"
          proof (cases "dipdom(dests)")
            assume "dipdom(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 dipdom(dests) dipkD(rt) [THEN kD_Some] show ?thesis
              unfolding invalidate_def sqn_def by auto
          next
            assume "dipdom(dests)"
            with Suc 0  sqn rt dip dipkD(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-:18..PRreq-:20}  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-:9}  {PRreq-:17, PRreq-:30, PRreq-:32}
                                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])
 
    have rreq_oip_kD: "paodv i  onl ΓAODV (λ(ξ, l). (l  {PRreq-:3..PRreq-:28}  oip ξ  kD(rt ξ)))"
      by(inv_cterms inv add: onl_invariant_sterms_TT [OF aodv_wf addpreRT_welldefined]) 

    have rreq_dip_kD_oip_sqn: "paodv i  onl ΓAODV (λ(ξ, l).
                       (l  {PRreq-:18..PRreq-:21}
                               (dip ξ  kD(rt ξ)
                                  (sqn (rt ξ) (oip ξ) > (osn ξ)
                                      (sqn (rt ξ) (oip ξ) = (osn ξ)
                                         the (dhops (rt ξ) (oip ξ))  Suc (hops ξ)
                                         the (flag (rt ξ) (oip ξ)) = val)))))"
      by(inv_cterms inv add: onl_invariant_sterms [OF aodv_wf rreq_oip]
                             onl_invariant_sterms [OF aodv_wf addpreRT_welldefined])

    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]
                              onl_invariant_sterms [OF aodv_wf rreq_oip_kD]
                              onl_invariant_sterms [OF aodv_wf rreq_dip_kD_oip_sqn])
  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-:11,
                                            PRreq-:24, PRrep-:10, PRerr-:1}
                           (ipdom(dests ξ). ipvD(rt ξ)))
                          (l  {PAodv-:16..PAodv-:19}
                               {PPkt-:8..PPkt-:11}
                               {PRreq-:12..PRreq-:15}
                               {PRreq-:25..PRreq-:28}
                               {PRrep-:11..PRrep-:14}
                               {PRerr-:2..PRerr-:5}  (ipdom(dests ξ). ipiD(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-:11, PRreq-:24, PRrep-:10}
              (ipdom(dests ξ). ipvD(rt ξ)  the (dests ξ ip) = inc (sqn (rt ξ) ip)))
            (l = PRerr-:1
              (ipdom(dests ξ). ipvD(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 (λ((ξ, _), _, (ξ', _)).
                                                                dipkD(rt ξ). rt ξ ⊑⇘diprt ξ')"
  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 *: "ipkD (rt ξ). Suc 0  the (dhops (rt ξ) ip)"
    show "ipkD (rt ξ). rt ξ ⊑⇘ipupdate (rt ξ) (oip ξ) (osn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
    proof
      fix ip
      assume "ipkD (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 ξ ⊑⇘ipupdate (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 *: "ipkD (rt ξ). Suc 0  the (dhops (rt ξ) ip)"
    show "ipkD (rt ξ). rt ξ ⊑⇘ipupdate (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
    proof
      fix ip
      assume "ipkD (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 ξ ⊑⇘ipupdate (rt ξ) (dip ξ) (dsn ξ, kno, val, Suc (hops ξ), sip ξ, {})"
        by (rule rt_fresher_update)
    qed
  qed

end