Theory A_Quality_Increases
section "The quality increases predicate"
theory A_Quality_Increases
imports A_Aodv_Predicates A_Fresher
begin
definition quality_increases :: "state ⇒ state ⇒ bool"
where "quality_increases ξ ξ' ≡ (∀dip∈kD(rt ξ). dip ∈ kD(rt ξ') ∧ rt ξ ⊑⇘dip⇙ rt ξ')
∧ (∀dip. sqn (rt ξ) dip ≤ sqn (rt ξ') dip)"
lemma quality_increasesI [intro!]:
assumes "⋀dip. dip ∈ kD(rt ξ) ⟹ dip ∈ kD(rt ξ')"
and "⋀dip. ⟦ dip ∈ kD(rt ξ); dip ∈ kD(rt ξ') ⟧ ⟹ rt ξ ⊑⇘dip⇙ rt ξ'"
and "⋀dip. sqn (rt ξ) dip ≤ sqn (rt ξ') dip"
shows "quality_increases ξ ξ'"
unfolding quality_increases_def using assms by clarsimp
lemma quality_increasesE [elim]:
fixes dip
assumes "quality_increases ξ ξ'"
and "dip∈kD(rt ξ)"
and "⟦ dip ∈ kD(rt ξ'); rt ξ ⊑⇘dip⇙ rt ξ'; sqn (rt ξ) dip ≤ sqn (rt ξ') dip ⟧ ⟹ R dip ξ ξ'"
shows "R dip ξ ξ'"
using assms unfolding quality_increases_def by clarsimp
lemma quality_increases_rt_fresherD [dest]:
fixes ip
assumes "quality_increases ξ ξ'"
and "ip∈kD(rt ξ)"
shows "rt ξ ⊑⇘ip⇙ rt ξ'"
using assms by auto
lemma quality_increases_sqnE [elim]:
fixes dip
assumes "quality_increases ξ ξ'"
and "sqn (rt ξ) dip ≤ sqn (rt ξ') dip ⟹ R dip ξ ξ'"
shows "R dip ξ ξ'"
using assms unfolding quality_increases_def by clarsimp
lemma quality_increases_refl [intro, simp]: "quality_increases ξ ξ"
by rule simp_all
lemma strictly_fresher_quality_increases_right [elim]:
fixes σ σ' dip
assumes "rt (σ i) ⊏⇘dip⇙ rt (σ nhip)"
and qinc: "quality_increases (σ nhip) (σ' nhip)"
and "dip∈kD(rt (σ nhip))"
shows "rt (σ i) ⊏⇘dip⇙ rt (σ' nhip)"
proof -
from qinc have "rt (σ nhip) ⊑⇘dip⇙ rt (σ' nhip)" using ‹dip∈kD(rt (σ nhip))›
by auto
with ‹rt (σ i) ⊏⇘dip⇙ rt (σ nhip)› show ?thesis ..
qed
lemma kD_quality_increases [elim]:
assumes "i∈kD(rt ξ)"
and "quality_increases ξ ξ'"
shows "i∈kD(rt ξ')"
using assms by auto
lemma kD_nsqn_quality_increases [elim]:
assumes "i∈kD(rt ξ)"
and "quality_increases ξ ξ'"
shows "i∈kD(rt ξ') ∧ nsqn (rt ξ) i ≤ nsqn (rt ξ') i"
proof -
from assms have "i∈kD(rt ξ')" ..
moreover with assms have "rt ξ ⊑⇘i⇙ rt ξ'" by auto
ultimately have "nsqn (rt ξ) i ≤ nsqn (rt ξ') i"
using ‹i∈kD(rt ξ)› by - (erule(2) rt_fresher_imp_nsqn_le)
with ‹i∈kD(rt ξ')› show ?thesis ..
qed
lemma nsqn_quality_increases [elim]:
assumes "i∈kD(rt ξ)"
and "quality_increases ξ ξ'"
shows "nsqn (rt ξ) i ≤ nsqn (rt ξ') i"
using assms by (rule kD_nsqn_quality_increases [THEN conjunct2])
lemma kD_nsqn_quality_increases_trans [elim]:
assumes "i∈kD(rt ξ)"
and "s ≤ nsqn (rt ξ) i"
and "quality_increases ξ ξ'"
shows "i∈kD(rt ξ') ∧ s ≤ nsqn (rt ξ') i"
proof
from ‹i∈kD(rt ξ)› and ‹quality_increases ξ ξ'› show "i∈kD(rt ξ')" ..
next
from ‹i∈kD(rt ξ)› and ‹quality_increases ξ ξ'› have "nsqn (rt ξ) i ≤ nsqn (rt ξ') i" ..
with ‹s ≤ nsqn (rt ξ) i› show "s ≤ nsqn (rt ξ') i" by (rule le_trans)
qed
lemma nsqn_quality_increases_nsqn_lt_lt [elim]:
assumes "i∈kD(rt ξ)"
and "quality_increases ξ ξ'"
and "s < nsqn (rt ξ) i"
shows "s < nsqn (rt ξ') i"
proof -
from assms(1-2) have "nsqn (rt ξ) i ≤ nsqn (rt ξ') i" ..
with ‹s < nsqn (rt ξ) i› show "s < nsqn (rt ξ') i" by simp
qed
lemma nsqn_quality_increases_dhops [elim]:
assumes "i∈kD(rt ξ)"
and "quality_increases ξ ξ'"
and "nsqn (rt ξ) i = nsqn (rt ξ') i"
shows "the (dhops (rt ξ) i) ≥ the (dhops (rt ξ') i)"
using assms unfolding quality_increases_def
by (clarsimp) (drule(1) bspec, clarsimp simp: rt_fresher_def2)
lemma nsqn_quality_increases_nsqn_eq_le [elim]:
assumes "i∈kD(rt ξ)"
and "quality_increases ξ ξ'"
and "s = nsqn (rt ξ) i"
shows "s < nsqn (rt ξ') i ∨ (s = nsqn (rt ξ') i ∧ the (dhops (rt ξ) i) ≥ the (dhops (rt ξ') i))"
using assms by (metis nat_less_le nsqn_quality_increases nsqn_quality_increases_dhops)
lemma quality_increases_rreq_rrep_props [elim]:
fixes sn ip hops sip
assumes qinc: "quality_increases (σ sip) (σ' sip)"
and "1 ≤ sn"
and *: "ip∈kD(rt (σ sip)) ∧ sn ≤ nsqn (rt (σ sip)) ip
∧ (nsqn (rt (σ sip)) ip = sn
⟶ (the (dhops (rt (σ sip)) ip) ≤ hops
∨ the (flag (rt (σ sip)) ip) = inv))"
shows "ip∈kD(rt (σ' sip)) ∧ sn ≤ nsqn (rt (σ' sip)) ip
∧ (nsqn (rt (σ' sip)) ip = sn
⟶ (the (dhops (rt (σ' sip)) ip) ≤ hops
∨ the (flag (rt (σ' sip)) ip) = inv))"
(is "_ ∧ ?nsqnafter")
proof -
from * obtain "ip∈kD(rt (σ sip))" and "sn ≤ nsqn (rt (σ sip)) ip" by auto
from ‹quality_increases (σ sip) (σ' sip)›
have "sqn (rt (σ sip)) ip ≤ sqn (rt (σ' sip)) ip" ..
from ‹quality_increases (σ sip) (σ' sip)› and ‹ip∈kD (rt (σ sip))›
have "ip∈kD (rt (σ' sip))" ..
from ‹sn ≤ nsqn (rt (σ sip)) ip› have ?nsqnafter
proof
assume "sn < nsqn (rt (σ sip)) ip"
also from ‹ip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
have "... ≤ nsqn (rt (σ' sip)) ip" ..
finally have "sn < nsqn (rt (σ' sip)) ip" .
thus ?thesis by simp
next
assume "sn = nsqn (rt (σ sip)) ip"
with ‹ip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
have "sn < nsqn (rt (σ' sip)) ip
∨ (sn = nsqn (rt (σ' sip)) ip
∧ the (dhops (rt (σ' sip)) ip) ≤ the (dhops (rt (σ sip)) ip))" ..
hence "sn < nsqn (rt (σ' sip)) ip
∨ (nsqn (rt (σ' sip)) ip = sn ∧ (the (dhops (rt (σ' sip)) ip) ≤ hops
∨ the (flag (rt (σ' sip)) ip) = inv))"
proof
assume "sn < nsqn (rt (σ' sip)) ip" thus ?thesis ..
next
assume "sn = nsqn (rt (σ' sip)) ip
∧ the (dhops (rt (σ sip)) ip) ≥ the (dhops (rt (σ' sip)) ip)"
hence "sn = nsqn (rt (σ' sip)) ip"
and "the (dhops (rt (σ' sip)) ip) ≤ the (dhops (rt (σ sip)) ip)" by auto
from * and ‹sn = nsqn (rt (σ sip)) ip› have "the (dhops (rt (σ sip)) ip) ≤ hops
∨ the (flag (rt (σ sip)) ip) = inv"
by simp
thus ?thesis
proof
assume "the (dhops (rt (σ sip)) ip) ≤ hops"
with ‹the (dhops (rt (σ' sip)) ip) ≤ the (dhops (rt (σ sip)) ip)›
have "the (dhops (rt (σ' sip)) ip) ≤ hops" by simp
with ‹sn = nsqn (rt (σ' sip)) ip› show ?thesis by simp
next
assume "the (flag (rt (σ sip)) ip) = inv"
with ‹ip∈kD(rt (σ sip))› have "nsqn (rt (σ sip)) ip = sqn (rt (σ sip)) ip - 1" ..
with ‹sn ≥ 1› and ‹sn = nsqn (rt (σ sip)) ip›
have "sqn (rt (σ sip)) ip > 1" by simp
from ‹ip∈kD(rt (σ' sip))› show ?thesis
proof (rule vD_or_iD)
assume "ip∈iD(rt (σ' sip))"
hence "the (flag (rt (σ' sip)) ip) = inv" ..
with ‹sn = nsqn (rt (σ' sip)) ip› show ?thesis
by simp
next
assume "ip∈vD(rt (σ' sip))"
hence "nsqn (rt (σ' sip)) ip = sqn (rt (σ' sip)) ip" ..
with ‹sqn (rt (σ sip)) ip ≤ sqn (rt (σ' sip)) ip›
have "nsqn (rt (σ' sip)) ip ≥ sqn (rt (σ sip)) ip" by simp
with ‹sqn (rt (σ sip)) ip > 1›
have "nsqn (rt (σ' sip)) ip > sqn (rt (σ sip)) ip - 1" by simp
with ‹nsqn (rt (σ sip)) ip = sqn (rt (σ sip)) ip - 1›
have "nsqn (rt (σ' sip)) ip > nsqn (rt (σ sip)) ip" by simp
with ‹sn = nsqn (rt (σ sip)) ip› have "nsqn (rt (σ' sip)) ip > sn"
by simp
thus ?thesis ..
qed
qed
qed
thus ?thesis by (metis (mono_tags) le_cases not_le)
qed
with ‹ip∈kD (rt (σ' sip))› show "ip∈kD (rt (σ' sip)) ∧ ?nsqnafter" ..
qed
lemma quality_increases_rreq_rrep_props':
fixes sn ip hops sip
assumes "∀j. quality_increases (σ j) (σ' j)"
and "1 ≤ sn"
and *: "ip∈kD(rt (σ sip)) ∧ sn ≤ nsqn (rt (σ sip)) ip
∧ (nsqn (rt (σ sip)) ip = sn
⟶ (the (dhops (rt (σ sip)) ip) ≤ hops
∨ the (flag (rt (σ sip)) ip) = inv))"
shows "ip∈kD(rt (σ' sip)) ∧ sn ≤ nsqn (rt (σ' sip)) ip
∧ (nsqn (rt (σ' sip)) ip = sn
⟶ (the (dhops (rt (σ' sip)) ip) ≤ hops
∨ the (flag (rt (σ' sip)) ip) = inv))"
proof -
from assms(1) have "quality_increases (σ sip) (σ' sip)" ..
thus ?thesis using assms(2-3) by (rule quality_increases_rreq_rrep_props)
qed
lemma rteq_quality_increases:
assumes "∀j. j ≠ i ⟶ quality_increases (σ j) (σ' j)"
and "rt (σ' i) = rt (σ i)"
shows "∀j. quality_increases (σ j) (σ' j)"
using assms by clarsimp (metis order_refl quality_increasesI rt_fresher_refl)
definition msg_fresh :: "(ip ⇒ state) ⇒ msg ⇒ bool"
where "msg_fresh σ m ≡
case m of Rreq hopsc _ _ _ oipc osnc sipc ⇒ osnc ≥ 1 ∧ (sipc ≠ oipc ⟶
oipc∈kD(rt (σ sipc)) ∧ nsqn (rt (σ sipc)) oipc ≥ osnc
∧ (nsqn (rt (σ sipc)) oipc = osnc
⟶ (hopsc ≥ the (dhops (rt (σ sipc)) oipc)
∨ the (flag (rt (σ sipc)) oipc) = inv)))
| Rrep hopsc dipc dsnc _ sipc ⇒ dsnc ≥ 1 ∧ (sipc ≠ dipc ⟶
dipc∈kD(rt (σ sipc)) ∧ nsqn (rt (σ sipc)) dipc ≥ dsnc
∧ (nsqn (rt (σ sipc)) dipc = dsnc
⟶ (hopsc ≥ the (dhops (rt (σ sipc)) dipc)
∨ the (flag (rt (σ sipc)) dipc) = inv)))
| Rerr destsc sipc ⇒ (∀ripc∈dom(destsc). (ripc∈kD(rt (σ sipc))
∧ the (destsc ripc) - 1 ≤ nsqn (rt (σ sipc)) ripc))
| _ ⇒ True"
lemma msg_fresh [simp]:
"⋀hops dip dsn dsk oip osn sip.
msg_fresh σ (Rreq hops dip dsn dsk oip osn sip) =
(osn ≥ 1 ∧ (sip ≠ oip ⟶ oip∈kD(rt (σ sip))
∧ nsqn (rt (σ sip)) oip ≥ osn
∧ (nsqn (rt (σ sip)) oip = osn
⟶ (hops ≥ the (dhops (rt (σ sip)) oip)
∨ the (flag (rt (σ sip)) oip) = inv))))"
"⋀hops dip dsn oip sip. msg_fresh σ (Rrep hops dip dsn oip sip) =
(dsn ≥ 1 ∧ (sip ≠ dip ⟶ dip∈kD(rt (σ sip))
∧ nsqn (rt (σ sip)) dip ≥ dsn
∧ (nsqn (rt (σ sip)) dip = dsn
⟶ (hops ≥ the (dhops (rt (σ sip)) dip))
∨ the (flag (rt (σ sip)) dip) = inv)))"
"⋀dests sip. msg_fresh σ (Rerr dests sip) =
(∀ripc∈dom(dests). (ripc∈kD(rt (σ sip))
∧ the (dests ripc) - 1 ≤ nsqn (rt (σ sip)) ripc))"
"⋀d dip. msg_fresh σ (Newpkt d dip) = True"
"⋀d dip sip. msg_fresh σ (Pkt d dip sip) = True"
unfolding msg_fresh_def by simp_all
lemma msg_fresh_inc_sn [simp, elim]:
"msg_fresh σ m ⟹ rreq_rrep_sn m"
by (cases m) simp_all
lemma recv_msg_fresh_inc_sn [simp, elim]:
"orecvmsg (msg_fresh) σ m ⟹ recvmsg rreq_rrep_sn m"
by (cases m) simp_all
lemma rreq_nsqn_is_fresh [simp]:
fixes σ msg hops dip dsn dsk oip osn sip
assumes "rreq_rrep_fresh (rt (σ sip)) (Rreq hops dip dsn dsk oip osn sip)"
and "rreq_rrep_sn (Rreq hops dip dsn dsk oip osn sip)"
shows "msg_fresh σ (Rreq hops dip dsn dsk oip osn sip)"
(is "msg_fresh σ ?msg")
proof -
let ?rt = "rt (σ sip)"
from assms(2) have "1 ≤ osn" by simp
thus ?thesis
unfolding msg_fresh_def
proof (simp only: msg.case, intro conjI impI)
assume "sip ≠ oip"
with assms(1) show "oip ∈ kD(?rt)" by simp
next
assume "sip ≠ oip"
and "nsqn ?rt oip = osn"
show "the (dhops ?rt oip) ≤ hops ∨ the (flag ?rt oip) = inv"
proof (cases "oip∈vD(?rt)")
assume "oip∈vD(?rt)"
hence "nsqn ?rt oip = sqn ?rt oip" ..
with ‹nsqn ?rt oip = osn› have "sqn ?rt oip = osn" by simp
with assms(1) and ‹sip ≠ oip› have "the (dhops ?rt oip) ≤ hops"
by simp
thus ?thesis ..
next
assume "oip∉vD(?rt)"
moreover from assms(1) and ‹sip ≠ oip› have "oip∈kD(?rt)" by simp
ultimately have "oip∈iD(?rt)" by auto
hence "the (flag ?rt oip) = inv" ..
thus ?thesis ..
qed
next
assume "sip ≠ oip"
with assms(1) have "osn ≤ sqn ?rt oip" by auto
thus "osn ≤ nsqn (rt (σ sip)) oip"
proof (rule nat_le_eq_or_lt)
assume "osn < sqn ?rt oip"
hence "osn ≤ sqn ?rt oip - 1" by simp
also have "... ≤ nsqn ?rt oip" by (rule sqn_nsqn)
finally show "osn ≤ nsqn ?rt oip" .
next
assume "osn = sqn ?rt oip"
with assms(1) and ‹sip ≠ oip› have "oip∈kD(?rt)"
and "the (flag ?rt oip) = val"
by auto
hence "nsqn ?rt oip = sqn ?rt oip" ..
with ‹osn = sqn ?rt oip› have "nsqn ?rt oip = osn" by simp
thus "osn ≤ nsqn ?rt oip" by simp
qed
qed simp
qed
lemma rrep_nsqn_is_fresh [simp]:
fixes σ msg hops dip dsn oip sip
assumes "rreq_rrep_fresh (rt (σ sip)) (Rrep hops dip dsn oip sip)"
and "rreq_rrep_sn (Rrep hops dip dsn oip sip)"
shows "msg_fresh σ (Rrep hops dip dsn oip sip)"
(is "msg_fresh σ ?msg")
proof -
let ?rt = "rt (σ sip)"
from assms have "sip ≠ dip ⟶ dip∈kD(?rt) ∧ sqn ?rt dip = dsn ∧ the (flag ?rt dip) = val"
by simp
hence "sip ≠ dip ⟶ dip∈kD(?rt) ∧ nsqn ?rt dip ≥ dsn"
by clarsimp
with assms show "msg_fresh σ ?msg"
by clarsimp
qed
lemma rerr_nsqn_is_fresh [simp]:
fixes σ msg dests sip
assumes "rerr_invalid (rt (σ sip)) (Rerr dests sip)"
shows "msg_fresh σ (Rerr dests sip)"
(is "msg_fresh σ ?msg")
proof -
let ?rt = "rt (σ sip)"
from assms have *: "(∀rip∈dom(dests). (rip∈iD(rt (σ sip))
∧ the (dests rip) = sqn (rt (σ sip)) rip))"
by clarsimp
have "(∀rip∈dom(dests). (rip∈kD(rt (σ sip))
∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip))"
proof
fix rip
assume "rip ∈ dom dests"
with * have "rip∈iD(rt (σ sip))" and "the (dests rip) = sqn (rt (σ sip)) rip"
by auto
from this(2) have "the (dests rip) - 1 = sqn (rt (σ sip)) rip - 1" by simp
also have "... ≤ nsqn (rt (σ sip)) rip" by (rule sqn_nsqn)
finally have "the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip" .
with ‹rip∈iD(rt (σ sip))›
show "rip∈kD(rt (σ sip)) ∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
by clarsimp
qed
thus "msg_fresh σ ?msg"
by simp
qed
lemma quality_increases_msg_fresh [elim]:
assumes qinc: "∀j. quality_increases (σ j) (σ' j)"
and "msg_fresh σ m"
shows "msg_fresh σ' m"
using assms(2)
proof (cases m)
fix hops rreqid dip dsn dsk oip osn sip
assume [simp]: "m = Rreq hops dip dsn dsk oip osn sip"
and "msg_fresh σ m"
then have "osn ≥ 1" and "sip = oip ∨ (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)))"
by auto
from this(2) show ?thesis
proof
assume "sip = oip" with ‹osn ≥ 1› show ?thesis by simp
next
assume "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))"
moreover from qinc have "quality_increases (σ sip) (σ' sip)" ..
ultimately have "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))"
using ‹osn ≥ 1› by (rule quality_increases_rreq_rrep_props [rotated 2])
with ‹osn ≥ 1› show "msg_fresh σ' m"
by (clarsimp)
qed
next
fix hops dip dsn oip sip
assume [simp]: "m = Rrep hops dip dsn oip sip"
and "msg_fresh σ m"
then have "dsn ≥ 1" and "sip = dip ∨ (dip∈kD(rt (σ sip)) ∧ dsn ≤ nsqn (rt (σ sip)) dip
∧ (nsqn (rt (σ sip)) dip = dsn
⟶ (the (dhops (rt (σ sip)) dip) ≤ hops
∨ the (flag (rt (σ sip)) dip) = inv)))"
by auto
from this(2) show "?thesis"
proof
assume "sip = dip" with ‹dsn ≥ 1› show ?thesis by simp
next
assume "dip∈kD(rt (σ sip)) ∧ dsn ≤ nsqn (rt (σ sip)) dip
∧ (nsqn (rt (σ sip)) dip = dsn
⟶ (the (dhops (rt (σ sip)) dip) ≤ hops
∨ the (flag (rt (σ sip)) dip) = inv))"
moreover from qinc have "quality_increases (σ sip) (σ' sip)" ..
ultimately have "dip∈kD(rt (σ' sip)) ∧ dsn ≤ nsqn (rt (σ' sip)) dip
∧ (nsqn (rt (σ' sip)) dip = dsn
⟶ (the (dhops (rt (σ' sip)) dip) ≤ hops
∨ the (flag (rt (σ' sip)) dip) = inv))"
using ‹dsn ≥ 1› by (rule quality_increases_rreq_rrep_props [rotated 2])
with ‹dsn ≥ 1› show "msg_fresh σ' m"
by clarsimp
qed
next
fix dests sip
assume [simp]: "m = Rerr dests sip"
and "msg_fresh σ m"
then have *: "∀rip∈dom(dests). rip∈kD(rt (σ sip))
∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
by simp
have "∀rip∈dom(dests). rip∈kD(rt (σ' sip))
∧ the (dests rip) - 1 ≤ nsqn (rt (σ' sip)) rip"
proof
fix rip
assume "rip∈dom(dests)"
with * have "rip∈kD(rt (σ sip))" and "the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
by - (drule(1) bspec, clarsimp)+
moreover from qinc have "quality_increases (σ sip) (σ' sip)" by simp
ultimately show "rip∈kD(rt (σ' sip)) ∧ the (dests rip) - 1 ≤ nsqn (rt (σ' sip)) rip" ..
qed
thus ?thesis by simp
qed simp_all
end