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
    by(auto simp add: inj_on_def)
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)))"
  by(auto simp add: Max_by_def)

lemma Max_is_Max_by_id:
  "⟦ finite S; S ≠ {} ⟧ ⟹ Max S = Max_by id S "
  apply(clarsimp simp add: Max_by_def)
  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))"
  by(force simp add: map_graph_def
    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(simp add: dom_def map_graph_def fun_graph_def)
  apply(erule finite_surj[where f="λx. (x, the (f x))"])
  apply(clarsimp simp add: image_def)
  by (metis option.sel)

(*******************************************************************)
lemma ran_map_addD:
  "x ∈ ran (m ++ f) ⟹ x ∈ ran m ∨ x ∈ ran f"
  by(auto simp add: ran_def)

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"
  by(auto simp add: const_map_def)

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)"
  by(auto simp add: const_map_def restrict_map_def)

lemma const_map_is_Some:
  "(const_map y A x = Some z) = (z = y ∧ x ∈ A)"
  by(auto simp add: const_map_def restrict_map_def)

lemma const_map_in_set:
  "x ∈ A ⟹ const_map v A x = Some v"
  by(auto simp add: const_map_def)

lemma const_map_notin_set:
  "x ∉ A ⟹ const_map v A x = None"
  by(auto simp add: const_map_def)

lemma dom_const_map:
  "dom (const_map v S) = S"
  by(auto simp add: const_map_def)

(*******************************************************************)
subsection ‹Votes with maximum timestamps.›
(*******************************************************************)

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})"
  by(clarsimp simp add: inj_on_def vote_set_def)

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)"])
    by(force simp add: image_def)
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})"
  by(simp add: vote_set_upd)

lemma vote_setD:
  "rv ∈ vote_set v_f {a} ⟹ v_f (fst rv) a = Some (snd rv)"
  by(auto simp add: vote_set_def)

lemma process_mru_new_votes:
  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 
    by(auto simp add: map_add_Some_iff const_map_is_Some const_map_is_None 
      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