# Theory MRU_Vote

```section ‹The MRU Vote Model›

theory MRU_Vote
imports Same_Vote
begin

context quorum_process
begin

text ‹This model is identical to Same Vote, except that it replaces
the @{term safe} guard with the following one, which says that ‹v› is the
most recently used (MRU) vote of a quorum:
›

definition mru_guard :: "v_state ⇒ process set ⇒ val ⇒ bool" where
"mru_guard s Q v ≡ Q ∈ Quorum ∧ (let mru = mru_of_set (votes s) Q in
mru = None ∨ (∃r. mru = Some (r, v)))"

text ‹The concrete algorithms will not refine the MRU Voting model directly, but its optimized
version instead. For simplicity, we thus do not create the model explicitly, but just prove guard
strengthening. We will show later that the optimized model refines the Same Vote model.›

lemma mru_vote_implies_safe:
assumes
inv4: "s ∈ SV_inv4"
and inv1: "s ∈ Vinv1"
and mru_vote: "mru_guard s Q v"
and is_Quorum: "Q ∈ Quorum"
shows "safe s (v_state.next_round s) v" using mru_vote
proof(clarsimp simp add: mru_guard_def mru_of_set_def option_Max_by_def)
― ‹The first case: some votes have been cast. We prove that the most recently used one is
safe.›
fix r
assume
nempty: "vote_set (votes s) Q ≠ {}"
and max: "Max_by fst (vote_set (votes s) Q) = (r, v)"

from Max_by_in[OF Vinv1_finite_vote_set[OF inv1] nempty] max

have no_larger: "∀a'∈Q. ∀r'>r. votes s r' a' = None"
proof(safe, rule ccontr, clarsimp)
fix a' r' w
assume "a' ∈ Q"  "votes s r' a' = Some w" and gt: "r' > r"
hence "(r', w) ∈ vote_set (votes s) Q"
thus False
using Max_by_ge[where f=fst, OF Vinv1_finite_vote_set[where Q=Q, OF inv1]] max gt
qed

have "safe s (Suc r) v" using inv4 in_votes and SV_inv4_def

thus "safe s (v_state.next_round s) v" using no_larger is_Quorum[THEN qintersect]