# Theory Consensus_Misc

```(*<*)
theory Consensus_Misc
imports Main
begin
(*>*)

subsection ‹Miscellaneous lemmas›

method_setup clarsimp_all =
‹Method.sections clasimp_modifiers >>
K (SIMPLE_METHOD o CHANGED_PROP o PARALLEL_ALLGOALS o clarsimp_tac)›
"clarify simplified, all goals"

definition flip where
flip_def: "flip f ≡ λx y. f y x"

lemma option_expand':
"⟦(option = None) = (option' = None); ⋀x y. ⟦option = Some x; option' = Some y⟧ ⟹ x = y⟧ ⟹
option = option'"
by(rule option.expand, auto)

(*********************************)
subsection ‹Argmax›
definition Max_by :: "('a ⇒ 'b :: linorder) ⇒ 'a set ⇒ 'a" where
"Max_by f S = (SOME x. x ∈ S ∧ f x = Max (f ` S))"

lemma Max_by_dest:
assumes "finite A" and "A ≠ {}"
shows "Max_by f A ∈ A ∧ f (Max_by f A) = Max (f ` A)" (is "?P (Max_by f A)")
proof(simp only: Max_by_def some_eq_ex[where P="?P"])
from assms have "finite (f ` A)" "f ` A ≠ {}" by auto
from Max_in[OF this] show "∃x. x ∈ A ∧ f x = Max (f ` A)"
by (metis image_iff)
qed

lemma Max_by_in:
assumes "finite A" and "A ≠ {}"
shows "Max_by f A ∈ A" using assms
by(rule Max_by_dest[THEN conjunct1])

lemma Max_by_ge:
assumes "finite A" "x ∈ A"
shows "f x ≤ f (Max_by f A)"
proof-
from assms(1) have fin_image: "finite (f ` A)" by simp
from assms(2) have non_empty: "A ≠ {}" by auto
have "f x ∈ f ` A" using assms(2) by simp
from Max_ge[OF fin_image this] and Max_by_dest[OF assms(1) non_empty, of f] show ?thesis
by(simp)
qed

lemma finite_UN_D:
"finite (⋃S) ⟹ ∀A ∈ S. finite A"
by (metis Union_upper finite_subset)

lemma Max_by_eqI:
assumes
fin: "finite A"
and "⋀y. y ∈ A ⟹ cmp_f y ≤ cmp_f x"
and in_X: "x ∈ A"
and inj: "inj_on cmp_f A"
shows "Max_by cmp_f A = x"
proof-
have in_M: "Max_by cmp_f A ∈ A" using assms
by(auto intro!: Max_by_in)
hence "cmp_f (Max_by cmp_f A) ≤ cmp_f x" using assms
by auto
also have "cmp_f x ≤ cmp_f (Max_by cmp_f A)"
by (intro Max_by_ge assms)
finally show ?thesis  using inj in_M in_X
qed

lemma Max_by_Union_distrib:
"⟦ finite A; A = ⋃S; S ≠ {}; {} ∉ S; inj_on cmp_f A ⟧ ⟹
Max_by cmp_f A = Max_by cmp_f (Max_by cmp_f ` S)"
proof(rule Max_by_eqI, assumption)
fix y
assume assms: "finite A" "A = ⋃S" "{} ∉ S" "y ∈ A"
then obtain B where B_def: "B ∈ S" "y ∈ B" by auto
hence "cmp_f y ≤ cmp_f (Max_by cmp_f B)" using assms
by (metis Max_by_ge finite_UN_D)
also have "... ≤ cmp_f (Max_by cmp_f (Max_by cmp_f ` S))" using B_def(1) assms
by (metis Max_by_ge finite_UnionD finite_imageI imageI)
finally show "cmp_f y ≤ cmp_f (Max_by cmp_f (Max_by cmp_f ` S))" .
next
assume assms: "finite A" "A = ⋃S" "{} ∉ S" "S ≠ {}"
hence "Max_by cmp_f ` S ≠ {}" "finite (Max_by cmp_f ` S)"
apply (metis image_is_empty)
by (metis assms(1) assms(2) finite_UnionD finite_imageI)
hence "Max_by cmp_f (Max_by cmp_f ` S) ∈ (Max_by cmp_f ` S)"
by(blast intro!: Max_by_in)
also have "(Max_by cmp_f ` S) ⊆ A"
proof -
have f1: "∀v0 v1. (¬ finite v0 ∨ v0 = {}) ∨ Max_by (v1::'a ⇒ 'b) v0 ∈ v0" using Max_by_in by blast
have "∀v1. v1 ∉ S ∨ finite v1" using assms(1) assms(2) finite_UN_D by blast
then obtain v2_13 :: "'a set set ⇒ 'a ⇒ 'a set" where "Max_by cmp_f ` S ⊆ ⋃S" using f1 assms(3) by blast
thus "Max_by cmp_f ` S ⊆ A" using assms(2) by presburger
qed
finally show "Max_by cmp_f (Max_by cmp_f ` S) ∈ A" .
qed

lemma Max_by_UNION_distrib:
"⟦finite A; A = (⋃x∈S. f x); S ≠ {}; {} ∉ f ` S; inj_on cmp_f A⟧ ⟹
Max_by cmp_f A = Max_by cmp_f (Max_by cmp_f ` (f ` S))"
by(force intro!: Max_by_Union_distrib)

lemma Max_by_eta:
"Max_by f = (λS. (SOME x. x ∈ S ∧ f x = Max (f ` S)))"

lemma Max_is_Max_by_id:
"⟦ finite S; S ≠ {} ⟧ ⟹ Max S = Max_by id S "
by (metis (mono_tags, lifting) Max_in someI_ex)

definition option_Max_by :: "('a ⇒ 'b :: linorder) ⇒ 'a set ⇒ 'a option" where
"option_Max_by cmp_f A ≡ if A = {} then None else Some (Max_by cmp_f A)"

(*********************************)

subsection ‹Function and map graphs›

definition fun_graph where
"fun_graph f = {(x, f x)|x. True}"

definition map_graph :: "('a, 'b)map ⇒ ('a × 'b) set" where
"map_graph f = {(x, y)|x y. (x, Some y) ∈ fun_graph f}"

lemma map_graph_mem[simp]:
"((x, y) ∈ map_graph f) = (f x = Some y)"
by(auto simp add: dom_def map_graph_def fun_graph_def)

lemma finite_fun_graph:
"finite A ⟹ finite (fun_graph f ∩ (A × UNIV))"
apply(rule bij_betw_finite[where A=A and f="λx. (x, f x)", THEN iffD1])
by(auto simp add: fun_graph_def bij_betw_def inj_on_def)

lemma finite_map_graph:
"finite A ⟹ finite (map_graph f ∩ (A × UNIV))"
dest!: finite_fun_graph[where f=f]
intro!: finite_surj[where A="fun_graph f ∩ (A × UNIV)" and f="apsnd the"]
)

lemma finite_dom_finite_map_graph:
"finite (dom f) ⟹ finite (map_graph f)"
apply(erule finite_surj[where f="λx. (x, the (f x))"])
by (metis option.sel)

(*******************************************************************)
"x ∈ ran (m ++ f) ⟹ x ∈ ran m ∨ x ∈ ran f"

subsection ‹Constant maps›

definition const_map :: "'v ⇒ 'k set ⇒ ('k, 'v)map" where
"const_map v S ≡ (λ_. Some v) |` S"

lemma const_map_empty[simp]:
"const_map v {} = Map.empty"

lemma const_map_ran[simp]: "x ∈ ran (const_map v S) = (S ≠ {} ∧ x = v)"
by(auto simp add: const_map_def ran_def restrict_map_def)

lemma const_map_is_None:
"(const_map y A  x = None) = (x ∉ A)"

lemma const_map_is_Some:
"(const_map y A x = Some z) = (z = y ∧ x ∈ A)"

lemma const_map_in_set:
"x ∈ A ⟹ const_map v A x = Some v"

lemma const_map_notin_set:
"x ∉ A ⟹ const_map v A x = None"

lemma dom_const_map:
"dom (const_map v S) = S"

(*******************************************************************)
(*******************************************************************)

definition vote_set :: "('round ⇒ ('process, 'val)map) ⇒ 'process set ⇒ ('round × 'val)set" where
"vote_set vs Q ≡ {(r, v)|a r v. ((r, a), v) ∈ map_graph (case_prod vs) ∧ a ∈ Q}"

lemma inj_on_fst_vote_set:
"inj_on fst (vote_set v_hist {p})"

lemma finite_vote_set:
assumes "∀r'≥(r :: nat). v_hist r' = Map.empty"
"finite S"
shows "finite (vote_set v_hist S)"
proof-
define vs where "vs = {((r, a), v)|r a v. ((r, a), v) ∈ map_graph (case_prod v_hist) ∧ a ∈ S}"
have "vs
= (⋃p∈S. ((λ(r, v). ((r, p), v)) ` (map_graph (λr. v_hist r p))))"
by(auto simp add: map_graph_def fun_graph_def vs_def)
also have "... ≤ (⋃p∈S. (λr. ((r, p), the (v_hist r p))) ` {0..<r})"
using assms(1)
apply auto
apply (auto simp add: map_graph_def fun_graph_def image_def)
apply (metis le_less_linear option.distinct(1))
done
also note I=finite_subset[OF calculation]
have "finite vs"
by(auto intro: I assms(2) nat_seg_image_imp_finite[where n=r])

thus ?thesis
apply(clarsimp simp add: map_graph_def fun_graph_def vote_set_def vs_def)
apply(erule finite_surj[where f="λ((r, a), v). (r, v)"])
qed

definition mru_of_set
:: "('round :: linorder ⇒ ('process, 'val)map) ⇒ ('process set, 'round × 'val)map" where
"mru_of_set vs ≡ λQ. option_Max_by fst (vote_set vs Q)"

definition process_mru
:: "('round :: linorder ⇒ ('process, 'val)map) ⇒ ('process, 'round × 'val)map" where
"process_mru vs ≡ λa. mru_of_set vs {a}"

lemma process_mru_is_None:
"(process_mru v_f a = None) = (vote_set v_f {a} = {})"
by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def)

lemma process_mru_is_Some:
"(process_mru v_f a = Some rv) = (vote_set v_f {a} ≠ {} ∧ rv = Max_by fst (vote_set v_f {a}))"
by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def)

lemma vote_set_upd:
"vote_set (v_hist(r := v_f)) {p} =
(if p ∈ dom v_f
then insert (r, the (v_f p))
else id
)
(if v_hist r p = None
then vote_set v_hist {p}
else vote_set v_hist {p} - {(r, the (v_hist r p))}
)
"
by(auto simp add: vote_set_def const_map_is_Some split: if_split_asm)

lemma finite_vote_set_upd:
" finite (vote_set v_hist {a}) ⟹
finite (vote_set (v_hist(r := v_f)) {a})"

lemma vote_setD:
"rv ∈ vote_set v_f {a} ⟹ v_f (fst rv) a = Some (snd rv)"

assumes
"∀r' ≥ (r :: nat). v_hist r' = Map.empty"
shows
"process_mru (v_hist(r := v_f)) =
(process_mru v_hist ++ (λp. map_option (Pair r) (v_f p)))"
proof(rule ext, rule option_expand')
fix p
show
"(process_mru (v_hist(r := v_f)) p = None) =
((process_mru v_hist ++ (λp. map_option (Pair r) (v_f p))) p = None)" using assms
by(force simp add: vote_set_def restrict_map_def  const_map_is_None process_mru_is_None)
next
fix p rv rv'
assume eqs:
"process_mru (v_hist(r := v_f)) p = Some rv"
"(process_mru v_hist ++ (λp. map_option (Pair r) (v_f p))) p = Some rv'"
moreover have "v_hist (r) p = None" using assms(1)
by(auto)

ultimately show "rv = rv'"  using eqs assms
process_mru_is_Some vote_set_upd dest!: vote_setD intro!: Max_by_eqI
finite_vote_set[OF assms]
intro: ccontr inj_on_fst_vote_set)
qed

end
```