Theory Consensus_Misc

theory Consensus_Misc
imports Main

subsection ‹Miscellaneous lemmas›

method_setup clarsimp_all =
  Method.sections clasimp_modifiers >>
  "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)

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)"
  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

lemma finite_UN_D:
  "finite (S)  A  S. finite A"
  by (metis Union_upper finite_subset)

lemma Max_by_eqI:
    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"
  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)
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))" .
  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
  finally show "Max_by cmp_f (Max_by cmp_f ` S)  A" .

lemma Max_by_UNION_distrib:
  "finite A; A = (xS. 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)"
  define vs where "vs = {((r, a), v)|r a v. ((r, a), v)  map_graph (case_prod v_hist)  a  S}"
  have "vs
      = (pS. ((λ(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 "...  (pS. (λ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))
  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)

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:
    "r'  (r :: nat). v_hist r' = Map.empty"
    "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
    "(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)
  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)

  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)