Session Consensus_Refined

Theory Infra

theory Infra imports Main  
begin

(******************************************************************************)
subsection ‹Prover configuration›
(******************************************************************************)

declare if_split_asm [split]


(******************************************************************************)
subsection ‹Forward reasoning ("attributes")›
(******************************************************************************)

text ‹The following lemmas are used to produce intro/elim rules from
set definitions and relation definitions.›

lemmas set_def_to_intro = eqset_imp_iff [THEN iffD2]
lemmas set_def_to_dest = eqset_imp_iff [THEN iffD1]
lemmas set_def_to_elim = set_def_to_dest [elim_format]

lemmas setc_def_to_intro = 
  set_def_to_intro [where B="{x. P x}", simplified] for P

lemmas setc_def_to_dest = 
  set_def_to_dest [where B="{x. P x}", simplified] for P

lemmas setc_def_to_elim = setc_def_to_dest [elim_format]

lemmas rel_def_to_intro = setc_def_to_intro [where x="(s, t)"] for s t
lemmas rel_def_to_dest = setc_def_to_dest [where x="(s, t)"] for s t
lemmas rel_def_to_elim = rel_def_to_dest [elim_format]


(******************************************************************************)
subsection ‹General results›
(******************************************************************************)

subsubsection ‹Maps›
(******************************************************************************)

text ‹We usually remove @{term"domIff"} from the simpset and clasets due
to annoying behavior. Sometimes the lemmas below are more well-behaved than 
@{term "domIff"}. Usually to be used as "dest: dom\_lemmas". However, adding 
them as permanent dest rules slows down proofs too much, so we refrain from 
doing this.›

lemma map_definedness: 
  "f x = Some y  x  dom f"
by (simp add: domIff)

lemma map_definedness_contra:
  " f x = Some y; z  dom f   x  z"
by (auto simp add: domIff)

lemmas dom_lemmas = map_definedness map_definedness_contra


subsubsection ‹Set›
(******************************************************************************)

declare image_comp[symmetric, simp]
(*
lemma image_comp [simp]: "(g o f)`A = g`f`A"
by (auto)
*)

lemma vimage_image_subset: "A  f-`(f`A)"
by (auto simp add: image_def vimage_def)


subsubsection ‹Relations›
(******************************************************************************)

lemma Image_compose [simp]:
  "(R1 O R2)``A  = R2``(R1``A)"
by (auto)


subsubsection ‹Lists›
(******************************************************************************)

lemma map_id: "map id = id"      (* already in simpset *)
by (simp)

― ‹Do NOT add the following equation to the simpset! (looping)›
lemma map_comp: "map (g o f) = map g o map f"  
by (simp)

declare map_comp_map [simp del]

lemma take_prefix: " take n l = xs   xs'. l = xs @ xs'"
by (induct l arbitrary: n xs, auto)
   (case_tac n, auto)


subsubsection ‹Finite sets›
(******************************************************************************)

text ‹Cardinality.›

declare arg_cong [where f=card, intro] 

lemma finite_positive_cardI [intro!]: 
  " A  {}; finite A   0 < card A"
by (auto)

lemma finite_positive_cardD [dest!]: 
  " 0 < card A; finite A   A  {}"
by (auto)

lemma finite_zero_cardI [intro!]: 
  " A = {}; finite A   card A = 0"
by (auto)

lemma finite_zero_cardD [dest!]: 
  " card A = 0; finite A   A = {}"
by (auto)


end





Theory Consensus_Types

(*<*)
theory Consensus_Types
imports Main
begin
(*>*)

subsection ‹Consensus: types›
typedecl process

text ‹Once we start taking maximums (e.g. in Last\_Voting), we will need the process set to be finite›
axiomatization where process_finite: 
  (* "class.finite TYPE(process)" *)
  "OFCLASS(process, finite_class)"

instance process :: finite by (rule process_finite)

abbreviation
  "N  card (UNIV::process set)"   ― ‹number of processes›

typedecl val     ― ‹Type of values to choose from›

type_synonym round = nat

end

Theory Quorums

(*<*)
theory Quorums
imports Consensus_Types
begin
(*>*)

subsection ‹Quorums›
(******************************************************************************)


locale quorum = 
  fixes Quorum :: "'a set set"
  assumes 
    qintersect: " Q  Quorum; Q'  Quorum   Q  Q'  {}"
    ― ‹Non-emptiness needed for some invariants of Coordinated Voting›
    and Quorum_not_empty: "Q. Q  Quorum"

lemma (in quorum) quorum_non_empty: "Q  Quorum  Q  {}"
by (auto dest: qintersect)

lemma (in quorum) empty_not_quorum: "{}  Quorum  False"
  using quorum_non_empty
  by blast

locale quorum_process = quorum Quorum
  for Quorum :: "process set set"

locale mono_quorum = quorum_process +
  assumes mono_quorum: " Q  Quorum; Q  Q'   Q'  Quorum"

lemma (in mono_quorum) UNIV_quorum:
  "UNIV  Quorum"
  using Quorum_not_empty mono_quorum
  by(blast)

definition majs :: "(process set) set" where
  "majs  {S. card S > N div 2}"

lemma majsI:
  "N div 2 < card S  S  majs"
  by(simp add: majs_def)

lemma card_Compl:
  fixes S :: "('a :: finite) set"
  shows "card (-S) = card (UNIV :: 'a set) - card S"
proof-
  have "card S + card (-S) = card (UNIV :: 'a set)"
    by(rule card_Un_disjoint[of S "-S", simplified Compl_partition, symmetric])
      (auto)
  thus ?thesis
    by simp
qed

lemma majorities_intersect:
  "card (Q :: process set) + card Q' > N  Q  Q'  {}"
  by (metis card_Un_disjoint card_mono finite not_le top_greatest)

interpretation majorities: mono_quorum majs
proof
  fix Q Q' assume "Q  majs" "Q'  majs"
  thus "Q  Q'  {}"
    by (intro majorities_intersect) (auto simp add: majs_def)
next
  show "Q. Q  majs" 
    apply(rule_tac x=UNIV in exI)
    apply(auto simp add: majs_def intro!: div_less_dividend finite_UNIV_card_ge_0)
    done
next
  fix Q Q'
  assume "Q  majs" "Q  Q'"
  thus "Q'  majs" using card_mono[OF _ Q  Q']
    by(auto simp add: majs_def)
qed

end

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"

lemma div_Suc:
  "Suc m div n = (if Suc m mod n = 0 then Suc (m div n) else m div n)" (is "_ = ?rhs")
proof (cases "Suc m mod n = 0")
  case True
  then show ?thesis
    by simp (metis Zero_not_Suc diff_Suc_Suc div_geq minus_mod_eq_mult_div mod_Suc mod_less neq0_conv nonzero_mult_div_cancel_left)
next
  case False
  then show ?thesis
    by simp (metis diff_Suc_Suc div_eq_0_iff minus_mod_eq_mult_div mod_Suc neq0_conv nonzero_mult_div_cancel_left)
qed

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 = (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)"
proof-
  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))
    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

Theory Two_Steps

(*<*)
theory Two_Steps
imports Consensus_Misc
begin
(*>*)
subsection ‹Step definitions for 2-step algorithms›

definition two_phase where "two_phase (r::nat)  r div 2"

definition two_step where "two_step (r::nat)  r mod 2"

lemma two_phase_zero [simp]: "two_phase 0 = 0"
by (simp add: two_phase_def)

lemma two_step_zero [simp]: "two_step 0 = 0"
by (simp add: two_step_def)

lemma two_phase_step: "(two_phase r * 2) + two_step r = r"
  by (auto simp add: two_phase_def two_step_def)

lemma two_step_phase_Suc:
  "two_step r = 0  two_phase (Suc r) = two_phase r"
  "two_step r = 0  two_step (Suc r) = 1"
  "two_step r = 0  two_phase (Suc (Suc r)) = Suc (two_phase r)"
  "two_step r = (Suc 0)  two_phase (Suc r) = Suc (two_phase r)"
  "two_step r = (Suc 0)  two_step (Suc r) = 0"
  by(simp_all add: two_step_def two_phase_def mod_Suc div_Suc)

end

Theory Three_Steps

(*<*)
theory Three_Steps
imports "../Consensus_Misc"
begin
(*>*)
subsection ‹Step definitions for 3-step algorithms›

abbreviation (input) "nr_steps  3"

definition three_phase where "three_phase (r::nat)  r div nr_steps"

definition three_step where "three_step (r::nat)  r mod nr_steps"

lemma three_phase_zero [simp]: "three_phase 0 = 0"
by (simp add: three_phase_def)

lemma three_step_zero [simp]: "three_step 0 = 0"
by (simp add: three_step_def)

lemma three_phase_step: "(three_phase r * nr_steps) + three_step r = r"
  by (auto simp add: three_phase_def three_step_def)

lemma three_step_Suc:
  "three_step r = 0  three_step (Suc (Suc r)) = 2"
  "three_step r = 0  three_step (Suc r) = 1"
  "three_step r = (Suc 0)  three_step (Suc r) = 2"
  "three_step r = (Suc 0)  three_step (Suc (Suc r)) = 0"
  "three_step r = (Suc (Suc 0))  three_step ((Suc r)) = 0"
  by(unfold three_step_def, simp_all add: mod_Suc)

lemma three_step_phase_Suc:
  "three_step r = 0  three_phase (Suc r) = three_phase r"
  "three_step r = 0  three_phase (Suc (Suc r)) = three_phase r"
  "three_step r = 0  three_phase (Suc (Suc (Suc r))) = Suc (three_phase r)"
  "three_step r = (Suc 0)  three_phase (Suc r) = three_phase r"
  "three_step r = (Suc 0)  three_phase (Suc (Suc r)) = Suc (three_phase r)"
  "three_step r = (Suc (Suc 0))  three_phase (Suc r) = Suc (three_phase r)"
  by(simp_all add: three_step_def three_phase_def mod_Suc div_Suc)

lemma three_step2_phase_Suc:
  "three_step r = 2  (3 * (Suc (three_phase r)) - 1) = r"
  apply(simp add: three_step_def three_phase_def)
  by (metis add_2_eq_Suc' mult_div_mod_eq)

lemma three_stepE:
  " three_step r = 0  P; three_step r = 1  P; three_step r = 2  P   P"
  by(unfold three_step_def, arith)

end

Theory Refinement

section ‹Models, Invariants and Refinements›

theory Refinement imports Infra 
begin

(******************************************************************************)
subsection ‹Specifications, reachability, and behaviours.›
(******************************************************************************)

text ‹Transition systems are multi-pointed graphs.›

record 's TS = 
  init :: "'s set"
  trans :: "('s × 's) set"


text ‹The inductive set of reachable states.›

inductive_set 
  reach ::  "('s, 'a) TS_scheme  's set" 
  for T :: "('s, 'a) TS_scheme"
where
  r_init [intro]:  "s  init T  s  reach T"
| r_trans [intro]: " (s, t)  trans T; s  reach T   t  reach T"

(* inductive_cases reach_invert: "t ∈ reach T" *)


subsubsection ‹Finite behaviours›
(******************************************************************************)

text ‹Note that behaviours grow at the head of the list, i.e., the initial 
state is at the end.›

inductive_set 
  beh :: "('s, 'a) TS_scheme  ('s list) set"
  for T :: "('s, 'a) TS_scheme" 
where
  b_empty [iff]: "[]  beh T"
| b_init [intro]: "s  init T  [s]  beh T"
| b_trans [intro]: " s # b  beh T; (s, t)  trans T   t # s # b  beh T"

inductive_cases beh_non_empty: "s # b  beh T"


text ‹Behaviours are prefix closed.›

lemma beh_immediate_prefix_closed:
  "s # b  beh T  b  beh T"
by (erule beh_non_empty, auto) 

lemma beh_prefix_closed:
  "c @ b  beh T  b  beh T"
by (induct c, auto dest!: beh_immediate_prefix_closed)


text ‹States in behaviours are exactly reachable.›

lemma beh_in_reach [rule_format]:
  "b  beh T  (s  set b. s  reach T)"
by (erule beh.induct) (auto)
  
lemma reach_in_beh:
  "s  reach T  b  beh T. s  set b" 
proof (induction rule: reach.induct)
  case (r_init s) thus ?case by (auto intro: bexI [where x="[s]"])
next
  case (r_trans s t) thus ?case
  proof -
    from r_trans(3) obtain b b0 b1 where "b  beh T" "b = b1 @ s # b0" by (auto dest: split_list)
    hence "s # b0  beh T" by (auto intro: beh_prefix_closed)
    hence "t # s # b0  beh T" using (s, t)  trans T  by auto 
    thus ?thesis by - (rule bexI, auto)
  qed
qed

lemma reach_equiv_beh_states: "reach T = (bbeh T. set b)"
by (auto intro!: reach_in_beh beh_in_reach)

text ‹Consecutive states in a behavior are connected by the transition relation›

lemma beh_consecutive_in_trans:
  assumes "b  beh TS"
  and "Suc i < length b"
  and "s = b ! Suc i"
  and "t = b ! i"
  shows "(s, t)  trans TS"
proof-
  from assms have
    "b = take i b @ t # s # drop (Suc (Suc i)) b"    
    by(auto simp add: id_take_nth_drop Cons_nth_drop_Suc)
  thus ?thesis
    by (metis assms(1) beh_non_empty beh_prefix_closed list.distinct(1) list.inject)
qed

subsubsection ‹Specifications, observability, and implementation› 
(******************************************************************************)

text ‹Specifications add an observer function to transition systems.›

record ('s, 'o) spec = "'s TS" +
  obs :: "'s  'o" 

lemma beh_obs_upd [simp]: "beh (S(| obs := x |)) = beh S"
by (safe) (erule beh.induct, auto)+

lemma reach_obs_upd [simp]: "reach (S(| obs := x |)) = reach S"
by (safe) (erule reach.induct, auto)+

text ‹Observable behaviour and reachability.›

definition 
  obeh :: "('s, 'o) spec  ('o list) set" where
  "obeh S  (map (obs S))`(beh S)"

definition 
  oreach :: "('s, 'o) spec  'o set" where 
  "oreach S  (obs S)`(reach S)"

lemma oreach_equiv_obeh_states: "oreach S = (bobeh S. set b)"
by (auto simp add: reach_equiv_beh_states oreach_def obeh_def)


lemma obeh_pi_translation:
  "(map pi)`(obeh S) = obeh (S(| obs := pi o (obs S) |))"
  by (simp add: obeh_def image_comp)

lemma oreach_pi_translation:
  "pi`(oreach S) = oreach (S(| obs := pi o (obs S) |))"
by (auto simp add: oreach_def)


text ‹A predicate $P$ on the states of a specification is \emph{observable} 
if it cannot distinguish between states yielding the same observation. 
Equivalently, $P$ is observable if it is the inverse image under the 
observation function of a predicate on observations.›

definition 
  observable :: "['s  'o, 's set]  bool"
where
  "observable ob P  s s'. ob s = ob s'  s'  P  s  P"

definition 
  observable2 :: "['s  'o, 's set]  bool"
where
  "observable2 ob P  Q. P = ob-`Q"

definition 
  observable3 :: "['s  'o, 's set]  bool"
where
  "observable3 ob P  ob-`ob`P  P"    ― ‹other direction holds trivially›

lemma observableE [elim]:
  "observable ob P; ob s = ob s'; s'  P  s  P"
by (unfold observable_def) (fast)

lemma observable2_equiv_observable: "observable2 ob P = observable ob P"
by (unfold observable_def observable2_def) (auto)

lemma observable3_equiv_observable2: "observable3 ob P = observable2 ob P"
by (unfold observable3_def observable2_def) (auto)

lemma observable_id [simp]: "observable id P" 
by (simp add: observable_def)

text ‹The set extension of a function @{term "ob"} is the left adjoint of 
a Galois connection on the powerset lattices over domain and range of @{term "ob"} 
where the right adjoint is the inverse image function.›

lemma image_vimage_adjoints: "(ob`P  Q) = (P  ob-`Q)"
by auto

declare image_vimage_subset [simp, intro]
declare vimage_image_subset [simp, intro]

text ‹Similar but "reversed" (wrt to adjointness) relationships only hold under
additional conditions.›

lemma image_r_vimage_l: " Q  ob`P; observable ob P   ob-`Q  P"
by (auto)

lemma vimage_l_image_r: " ob-`Q  P; Q  range ob   Q  ob`P"
by (drule image_mono [where f=ob], auto)


text ‹Internal and external invariants›

lemma external_from_internal_invariant: 
  " reach S  P; (obs S)`P  Q   
   oreach S  Q"
by (auto simp add: oreach_def)

lemma external_from_internal_invariant_vimage: 
  " reach S  P; P  (obs S)-`Q 
   oreach S  Q"
by (erule external_from_internal_invariant) (auto)


lemma external_to_internal_invariant_vimage: 
  " oreach S  Q; (obs S)-`Q  P 
   reach S  P"
by (auto simp add: oreach_def)

lemma external_to_internal_invariant:
  " oreach S  Q; Q  (obs S)`P; observable (obs S) P  
   reach S  P"
by (erule external_to_internal_invariant_vimage) (auto)


lemma external_equiv_internal_invariant_vimage: 
  " P = (obs S)-`Q  
   (oreach S  Q) = (reach S  P)"
by (fast intro: external_from_internal_invariant_vimage
                external_to_internal_invariant_vimage 
         del: subsetI)

lemma external_equiv_internal_invariant: 
  " (obs S)`P = Q; observable (obs S) P  
   (oreach S  Q) = (reach S  P)"
by (rule external_equiv_internal_invariant_vimage) (auto)


text ‹Our notion of implementation is inclusion of observable behaviours.›

definition 
  implements :: "['p  'o, ('s, 'o) spec, ('t, 'p) spec]  bool" where
  "implements pi Sa Sc  (map pi)`(obeh Sc)  obeh Sa"


text ‹Reflexivity and transitivity›

lemma implements_refl: "implements id S S"
by (auto simp add: implements_def)

lemma implements_trans:
  " implements pi1 S1 S2; implements pi2 S2 S3  
   implements (pi1 o pi2) S1 S3"
by (auto simp add: implements_def image_comp del: subsetI
         dest: image_mono [where f="map pi1"])


text ‹Preservation of external invariants›

lemma implements_oreach:
  "implements pi Sa Sc  pi`(oreach Sc)  oreach Sa"
by (auto simp add: implements_def oreach_equiv_obeh_states dest!: subsetD)

lemma external_invariant_preservation:
  " oreach Sa  Q; implements pi Sa Sc 
   pi`(oreach Sc)  Q"
by (rule subset_trans [OF implements_oreach]) (auto)

lemma external_invariant_translation:
  " oreach Sa  Q; pi-`Q  P; implements pi Sa Sc 
   oreach Sc  P"
apply (rule subset_trans [OF vimage_image_subset, of pi])
apply (rule subset_trans [where B="pi-`Q"])
apply (intro vimage_mono external_invariant_preservation, auto)
done


text ‹Preservation of internal invariants›

lemma internal_invariant_translation:
  " reach Sa  Pa; Pa  obs Sa -` Qa; pi -` Qa  Q; obs S -` Q  P;
     implements pi Sa S 
   reach S  P"
by (rule external_from_internal_invariant_vimage [
      THEN external_invariant_translation, 
      THEN external_to_internal_invariant_vimage]) 
   (assumption+)



(******************************************************************************)
subsection ‹Invariants›
(******************************************************************************)

text ‹First we define Hoare triples over transition relations and then
we derive proof rules to establish invariants.›


subsubsection ‹Hoare triples›
(******************************************************************************)

definition 
  PO_hoare :: "['s set, ('s × 's) set, 's set]  bool"
     ("(3{_} _ {> _})" [0, 0, 0] 90)
where
  "{pre} R {> post}  R``pre  post"

lemmas PO_hoare_defs = PO_hoare_def Image_def

lemma "{P} R {> Q} = (s t. s  P  (s, t)  R  t  Q)"
by (auto simp add: PO_hoare_defs)

lemma hoareD:
  " {I} R {>J}; s  I; (s, s')  R   s'  J"
  by(auto simp add: PO_hoare_def)

text ‹Some essential facts about Hoare triples.›

lemma hoare_conseq_left [intro]:
  " {P'} R {> Q}; P  P' 
   {P} R {> Q}"
by (auto simp add: PO_hoare_defs)

lemma hoare_conseq_right:
  " {P} R {> Q'}; Q'  Q 
   {P} R {> Q}"
by (auto simp add: PO_hoare_defs)

lemma hoare_false_left [simp]:
  "{{}} R {> Q}"
by (auto simp add: PO_hoare_defs)

lemma hoare_true_right [simp]:
  "{P} R {> UNIV}"
by (auto simp add: PO_hoare_defs)

lemma hoare_conj_right [intro!]:
  " {P} R {> Q1}; {P} R {> Q2} 
   {P} R {> Q1  Q2}"
by (auto simp add: PO_hoare_defs)


text ‹Special transition relations.›

lemma hoare_stop [simp, intro!]:
  "{P} {} {> Q}"
by (auto simp add: PO_hoare_defs)

lemma hoare_skip [simp, intro!]: 
  "P  Q  {P} Id {> Q}"
by (auto simp add: PO_hoare_defs)

lemma hoare_trans_Un [iff]:
  "{P} R1  R2 {> Q} = ({P} R1 {> Q}  {P} R2 {> Q})"
by (auto simp add: PO_hoare_defs)

lemma hoare_trans_UN [iff]:
  "{P}  x. R x {> Q} = (x. {P} R x {> Q})"
by (auto simp add: PO_hoare_defs)



subsubsection ‹Characterization of reachability›
(******************************************************************************)

lemma reach_init: "reach T  I  init T  I"
by (auto dest: subsetD)

lemma reach_trans: "reach T  I  {reach T} trans T {> I}"
by (auto simp add: PO_hoare_defs)


text ‹Useful consequences.›

corollary init_reach [iff]: "init T  reach T" 
by (rule reach_init, simp)

corollary trans_reach [iff]: "{reach T} trans T {> reach T}" 
by (rule reach_trans, simp)



subsubsection ‹Invariant proof rules›
(******************************************************************************)

text ‹Basic proof rule for invariants.›

lemma inv_rule_basic:
  " init T  P; {P} (trans T) {> P} 
   reach T  P"
by (safe, erule reach.induct, auto simp add: PO_hoare_def)


text ‹General invariant proof rule. This rule is complete (set 
@{term "I = reach T"}).›

lemma inv_rule:
  " init T  I; I  P; {I} (trans T) {> I} 
   reach T  P"
apply (rule subset_trans, auto)              ― ‹strengthen goal›
apply (erule reach.induct, auto simp add: PO_hoare_def)
done

text ‹The following rule is equivalent to the previous one.›

lemma INV_rule:
  " init T  I; {I  reach T} (trans T) {> I} 
   reach T  I"
by (safe, erule reach.induct, auto simp add: PO_hoare_defs)


text ‹Proof of equivalence.›

lemma inv_rule_from_INV_rule:
  " init T  I; I  P; {I} (trans T) {> I} 
   reach T  P"
apply (rule subset_trans, auto del: subsetI)
apply (rule INV_rule, auto)
done

lemma INV_rule_from_inv_rule:
  " init T  I; {I  reach T} (trans T) {> I} 
   reach T  I"
by (rule_tac I="I  reach T" in inv_rule, auto)


text ‹Incremental proof rule for invariants using auxiliary invariant(s). 
This rule might have become obsolete by addition of $INV\_rule$.›

lemma inv_rule_incr:
  " init T  I; {I  J} (trans T) {> I}; reach T  J     
   reach T  I"
by (rule INV_rule, auto)


(******************************************************************************)
subsection ‹Refinement›
(******************************************************************************)

text ‹Our notion of refinement is simulation. We first define a general
notion of relational Hoare tuple, which we then use to define the refinement
proof obligation.  Finally, we show that observation-consistent refinement 
of specifications implies the implementation relation between them.›


subsubsection ‹Relational Hoare tuples›
(******************************************************************************)

text ‹Relational Hoare tuples formalize the following generalized simulation 
diagram:

\begin{verbatim}
                           o -- Ra --> o
                           |           |
                          pre         post
                           |           |
                           v           V
                           o -- Rc --> o
\end{verbatim}

Here, $Ra$ and $Rc$ are the abstract and concrete transition relations, 
and $pre$ and $post$ are the pre- and post-relations.
(In the definiton below, the operator @{term "(O)"} stands for relational 
composition, which is defined as follows: @{thm relcomp_def [no_vars]}.)›

definition
  PO_rhoare :: 
    "[('s × 't) set, ('s × 's) set, ('t × 't) set, ('s × 't) set]  bool"
     ("(4{_} _, _ {> _})" [0, 0, 0] 90)
where
  "{pre} Ra, Rc {> post}  pre O Rc  Ra O post"

lemmas PO_rhoare_defs = PO_rhoare_def relcomp_unfold


text ‹Facts about relational Hoare tuples.›

lemma relhoare_conseq_left [intro]:
  " {pre'} Ra, Rc {> post}; pre  pre'  
   {pre} Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs dest!: subsetD)

lemma relhoare_conseq_right:                    ― ‹do NOT declare [intro]›
  " {pre} Ra, Rc {> post'}; post'  post  
   {pre} Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs)

lemma relhoare_false_left [simp]:               ― ‹do NOT declare [intro]›
  "{ {} } Ra, Rc {> post}"
by (auto simp add: PO_rhoare_defs)

lemma relhoare_true_right [simp]:                ― ‹not true in general›
  "{pre} Ra, Rc {> UNIV} = (Domain (pre O Rc)  Domain Ra)"
by (auto simp add: PO_rhoare_defs)

lemma Domain_rel_comp [intro]:
  "Domain pre  R  Domain (pre O Rc)  R"
by (auto simp add: Domain_def)

lemma rel_hoare_skip [iff]: "{R} Id, Id {> R}"
by (auto simp add: PO_rhoare_def)


text ‹Reflexivity and transitivity.›

lemma relhoare_refl [simp]: "{Id} R, R {> Id}"
by (auto simp add: PO_rhoare_defs)

lemma rhoare_trans:
  " {R1} T1, T2 {> R1}; {R2} T2, T3 {> R2} 
   {R1 O R2} T1, T3 {> R1 O R2}"
apply (auto simp add: PO_rhoare_def del: subsetI)
apply (drule subset_refl [THEN relcomp_mono, where r=R1])
apply (drule subset_refl [THEN [2] relcomp_mono, where s=R2])
apply (auto simp add: O_assoc del: subsetI)
done


text ‹Conjunction in the post-relation cannot be split in general.  However, 
here are two useful special cases.  In the first case the abstract transtition 
relation is deterministic and in the second case one conjunct is a cartesian 
product of two state predicates.›

lemma relhoare_conj_right_det:                 
  " {pre} Ra, Rc {> post1}; {pre} Ra, Rc {> post2};
     single_valued Ra                            ― ‹only for deterministic Ra›!›
   {pre} Ra, Rc {> post1  post2}"
by (auto simp add: PO_rhoare_defs dest: single_valuedD dest!: subsetD)

lemma relhoare_conj_right_cartesian [intro]:
  " {Domain pre} Ra {> I}; {Range pre} Rc {> J};
     {pre} Ra, Rc {> post}  
   {pre} Ra, Rc {> post  I × J}"
by (force simp add: PO_rhoare_defs PO_hoare_defs Domain_def Range_def)


text ‹Separate rule for cartesian products.›

corollary relhoare_cartesian:
  " {Domain pre} Ra {> I}; {Range pre} Rc {> J};
     {pre} Ra, Rc {> post}                       ― ‹any post›, including UNIV›!›
   {pre} Ra, Rc {> I × J}"
by (auto intro: relhoare_conseq_right)


text ‹Unions of transition relations.›

lemma relhoare_concrete_Un [simp]:
  "{pre} Ra, Rc1  Rc2 {> post} 
   = ({pre} Ra, Rc1 {> post}  {pre} Ra, Rc2 {> post})"
apply (auto simp add: PO_rhoare_defs)
apply (auto dest!: subsetD)
done

lemma relhoare_concrete_UN [simp]:
  "{pre} Ra, x. Rc x {> post} = (x. {pre} Ra, Rc x {> post})"
apply (auto simp add: PO_rhoare_defs)
 apply (auto dest!: subsetD)
done

lemma relhoare_abstract_Un_left [intro]:
  " {pre} Ra1, Rc {> post} 
   {pre} Ra1  Ra2, Rc {> post}"
by (auto simp add: PO_rhoare_defs)

lemma relhoare_abstract_Un_right [intro]:
  " {pre} Ra2, Rc {> post} 
   {pre} Ra1  Ra2, Rc {> post}"
by (auto simp add: PO_rhoare_defs)

lemma relhoare_abstract_UN [intro!]:   ― ‹might be too aggressive?›
  " {pre} Ra x, Rc {> post} 
   {pre} x. Ra x, Rc {> post}"
apply (auto simp add: PO_rhoare_defs)
apply (auto dest!: subsetD)
done



subsubsection ‹Refinement proof obligations›
(******************************************************************************)

text ‹A transition system refines another one if the initial states and the
transitions are refined. 
Initial state refinement means that for each concrete initial state there is 
a related abstract one. Transition refinement means that the simulation 
relation is preserved (as expressed by a relational Hoare tuple). 
›

definition 
  PO_refines :: 
    "[('s × 't) set, ('s, 'a) TS_scheme, ('t, 'b) TS_scheme]  bool" 
where
  "PO_refines R Ta Tc  (
       init Tc  R``(init Ta)
      {R} (trans Ta), (trans Tc) {> R} 
  )"


text ‹Basic refinement rule. This is just an introduction rule for the
definition.›

lemma refine_basic:
  " init Tc  R``(init Ta); {R} (trans Ta), (trans Tc) {> R} 
   PO_refines R Ta Tc"
by (simp add: PO_refines_def)


text ‹The following proof rule uses individual invariants @{term "I"} 
and @{term "J"} of the concrete and abstract systems to strengthen the 
simulation relation $R$. 

The hypotheses state that these state predicates are indeed invariants.
Note that the pre-condition of the invariant preservation hypotheses for 
@{term "I"} and @{term "J"} are strengthened by adding the predicates 
@{term "Domain (R  UNIV × J)"} and @{term "Range (R  I × UNIV)"}, 
respectively.  In particular, the latter predicate may be essential, if a 
concrete invariant depends on the simulation relation and an abstract invariant, 
i.e. to "transport" abstract invariants to the concrete system.›

lemma refine_init_using_invariants:
  " init Tc  R``(init Ta); init Ta  I; init Tc  J 
   init Tc  (R  I × J)``(init Ta)"
by (auto simp add: Image_def dest!: bspec subsetD)

lemma refine_trans_using_invariants:
  " {R  I × J} (trans Ta), (trans Tc) {> R};
     {I  Domain (R  UNIV × J)} (trans Ta) {> I}; 
     {J  Range (R  I × UNIV)} (trans Tc) {> J} 
   {R  I × J} (trans Ta), (trans Tc) {> R   I × J}"
by (rule relhoare_conj_right_cartesian) (auto)


text ‹This is our main rule for refinements.›

lemma refine_using_invariants:
  " {R  I × J} (trans Ta), (trans Tc) {> R};
     {I  Domain (R  UNIV × J)} (trans Ta) {> I}; 
     {J  Range (R  I × UNIV)} (trans Tc) {> J}; 
     init Tc  R``(init Ta); 
     init Ta  I; init Tc  J 
   PO_refines (R  I × J) Ta Tc"
by (unfold PO_refines_def)
   (intro refine_init_using_invariants refine_trans_using_invariants conjI)


subsubsection ‹Deriving invariants from refinements›
(******************************************************************************)

text ‹Some invariants can only be proved after the simulation has been 
established, because they depend on the simulation relation and some abstract
invariants.  Here is a rule to derive invariant theorems from the refinement.›

lemma PO_refines_implies_Range_init:
  "PO_refines R Ta Tc  init Tc  Range R"
by (auto simp add: PO_refines_def)

lemma PO_refines_implies_Range_trans:
  "PO_refines R Ta Tc  {Range R} trans Tc {> Range R}"
by (auto simp add: PO_refines_def PO_rhoare_def PO_hoare_def)

lemma PO_refines_implies_Range_invariant:
  "PO_refines R Ta Tc  reach Tc  Range R"
by (rule INV_rule)
   (auto intro!: PO_refines_implies_Range_init 
                 PO_refines_implies_Range_trans)

text ‹The following rules are more useful in proofs.›

corollary INV_init_from_refinement: 
  " PO_refines R Ta Tc; Range R  I 
   init Tc  I"
by (drule PO_refines_implies_Range_init, auto)

corollary INV_trans_from_refinement: 
  " PO_refines R Ta Tc; K  Range R; Range R  I 
   {K} trans Tc {> I}"
apply (drule PO_refines_implies_Range_trans)
apply (auto intro: hoare_conseq_right)
done

corollary INV_from_refinement: 
  " PO_refines R Ta Tc; Range R  I 
   reach Tc  I"
by (drule PO_refines_implies_Range_invariant, fast)

subsubsection ‹Transfering abstract invariants to concrete systems›
(******************************************************************************)

lemmas hoare_conseq = hoare_conseq_right[OF hoare_conseq_left] for P' R Q'

lemma PO_refines_implies_R_image_init:
  "PO_refines R Ta Tc  init Tc  R `` (init Ta)"
  apply(rule subset_trans[where B="R `` init Ta"])
   apply (auto simp add: PO_refines_def)
  done

lemma commute_dest:
  " R O Tc  Ta O R; (sa, sc)  R; (sc, sc')  Tc   sa'. (sa, sa')  Ta  (sa', sc')  R"
  by(auto)

lemma PO_refines_implies_R_image_trans:
  assumes "PO_refines R Ta Tc"
  shows "{R `` reach Ta} trans Tc {> R `` reach Ta}" using assms
proof(unfold PO_hoare_def Image_def PO_refines_def PO_rhoare_def, safe)
  fix sc sc' sa
  assume R: "(sa, sc)  R"
    and step: "(sc, sc')  TS.trans Tc"
    and sa_reach: "sa  reach Ta"
    and trans_ref: "R O trans Tc  trans Ta O R"
  from commute_dest[OF trans_ref R step] sa_reach
  show " sa'reach Ta. (sa', sc')  R"
    by(auto)
qed

lemma PO_refines_implies_R_image_invariant:
  assumes "PO_refines R Ta Tc"
  shows "reach Tc  R `` reach Ta" 
proof(rule INV_rule)
  show "init Tc  R `` reach Ta"
    by (rule subset_trans[OF PO_refines_implies_R_image_init, OF assms]) (auto)
next
  show "{R `` reach Ta  reach Tc} TS.trans Tc {> R `` reach Ta}" using assms
    by (auto intro!: PO_refines_implies_R_image_trans)
qed

lemma abs_INV_init_transfer:
  assumes
    "PO_refines R Ta Tc"
    "init Ta  I"
  shows "init Tc  R `` I" using PO_refines_implies_R_image_init[OF assms(1)] assms(2)
    by(blast elim!: subset_trans intro: Image_mono)

lemma abs_INV_trans_transfer:
  assumes
    ref: "PO_refines R Ta Tc"
    and abs_hoare: "{I} trans Ta {> J}"
  shows "{R `` I} trans Tc {> R `` J}"
proof(unfold PO_hoare_def Image_def, safe)
  fix sc sc' sa
  assume step: "(sc, sc')  trans Tc" and abs_inv: "sa  I" and R: "(sa, sc)  R"
  from ref step and R obtain sa' where 
    abs_step: "(sa, sa')  trans Ta" and R': "(sa', sc')  R"
    by(auto simp add: PO_refines_def PO_rhoare_def)
  with hoareD[OF abs_hoare abs_inv abs_step]
  show "sa'J. (sa', sc')  R"
    by(blast)
qed
    
lemma abs_INV_transfer:
  assumes
    "PO_refines R Ta Tc"
    "reach Ta  I"
  shows "reach Tc  R `` I" using PO_refines_implies_R_image_invariant[OF assms(1)] assms(2)
  by(auto)

subsubsection ‹Refinement of specifications›
(******************************************************************************)

text ‹Lift relation membership to finite sequences›

inductive_set 
  seq_lift :: "('s × 't) set  ('s list × 't list) set" 
  for R :: "('s × 't) set"
where
  sl_nil [iff]: "([], [])  seq_lift R"
| sl_cons [intro]: 
    " (xs, ys)  seq_lift R; (x, y)  R   (x#xs, y#ys)  seq_lift R"

inductive_cases sl_cons_right_invert: "(ba', t # bc)  seq_lift R" 


text ‹For each concrete behaviour there is a related abstract one.›

lemma behaviour_refinement:
assumes "PO_refines R Ta Tc" "bc  beh Tc" 
shows "ba  beh Ta. (ba, bc)  seq_lift R" 
using assms(2)
proof (induct rule: beh.induct)
  case b_empty thus ?case by auto 
next 
  case (b_init s) thus ?case using assms(1) by (auto simp add: PO_refines_def)
next
  case (b_trans s b s') show ?case
  proof -
    from b_trans(2) obtain t c where "t # c  beh Ta" "(t, s)  R" "(t # c, s # b)  seq_lift R"
      by (auto elim!: sl_cons_right_invert)
    moreover
    from (t, s)  R (s, s')  TS.trans Tc assms(1) 
    obtain t' where "(t, t')  trans Ta" "(t', s')  R" 
      by (auto simp add: PO_refines_def PO_rhoare_def)
    ultimately 
    have "t' # t # c  beh Ta" "(t' # t # c, s' # s # b)  seq_lift R" by auto
    thus ?thesis by (auto)
  qed
qed


text ‹Observation consistency of a relation is defined using a mediator 
function @{term "pi"} to abstract the concrete observation.  This allows us 
to also refine the observables as we move down a refinement branch.
›

definition 
  obs_consistent :: 
    "[('s × 't) set, 'p  'o, ('s, 'o) spec, ('t, 'p) spec]  bool"
where
  "obs_consistent R pi Sa Sc  (s t. (s, t)  R  pi (obs Sc t) = obs Sa s)"

lemma obs_consistent_refl [iff]: "obs_consistent Id id S S"
by (simp add: obs_consistent_def)

lemma obs_consistent_trans [intro]: 
  " obs_consistent R1 pi1 S1 S2; obs_consistent R2 pi2 S2 S3 
   obs_consistent (R1 O R2) (pi1 o pi2) S1 S3"
by (auto simp add: obs_consistent_def)

lemma obs_consistent_empty: "obs_consistent {} pi Sa Sc"
by (auto simp add: obs_consistent_def)

lemma obs_consistent_conj1 [intro]: 
  "obs_consistent R pi Sa Sc  obs_consistent (R  R') pi Sa Sc"
by (auto simp add: obs_consistent_def)

lemma obs_consistent_conj2 [intro]: 
  "obs_consistent R pi Sa Sc  obs_consistent (R'  R) pi Sa Sc"
by (auto simp add: obs_consistent_def)

lemma obs_consistent_behaviours:
  " obs_consistent R pi Sa Sc; bc  beh Sc; ba  beh Sa; (ba, bc)  seq_lift R
   map pi (map (obs Sc) bc) = map (obs Sa) ba"
by (erule seq_lift.induct) (auto simp add: obs_consistent_def) 


text ‹Definition of refinement proof obligations.›

definition 
  refines :: 
    "[('s × 't) set, 'p  'o, ('s, 'o) spec, ('t, 'p) spec]  bool" 
where
  "refines R pi Sa Sc  obs_consistent R pi Sa Sc  PO_refines R Sa Sc"

lemmas refines_defs = 
  refines_def PO_refines_def

lemma refinesI: 
  " PO_refines R Sa Sc; obs_consistent R pi Sa Sc 
   refines R pi Sa Sc"
by (simp add: refines_def)

lemma PO_refines_from_refines: 
  "refines R pi Sa Sc  PO_refines R Sa Sc"
by (simp add: refines_def)


text ‹Reflexivity and transitivity of refinement.›

lemma refinement_reflexive: "refines Id id S S"
by (auto simp add: refines_defs)

lemma refinement_transitive: 
  " refines R1 pi1 S1 S2; refines R2 pi2 S2 S3  
   refines (R1 O R2) (pi1 o pi2) S1 S3"
apply (auto simp add: refines_defs del: subsetI intro: rhoare_trans)
apply (fastforce dest: Image_mono)
done


text ‹Soundness of refinement for proving implementation›

lemma observable_behaviour_refinement:
  " refines R pi Sa Sc; bc  obeh Sc   map pi bc  obeh Sa"
by (auto simp add: refines_def obeh_def image_def
         dest!: behaviour_refinement obs_consistent_behaviours)

theorem refinement_soundness: 
  "refines R pi Sa Sc  implements pi Sa Sc"
by (auto simp add: implements_def 
         elim!: observable_behaviour_refinement)


text ‹Extended versions of proof rules including observations›

lemmas Refinement_basic = refine_basic [THEN refinesI]
lemmas Refinement_using_invariants = refine_using_invariants [THEN refinesI]

lemmas INV_init_from_Refinement = 
  INV_init_from_refinement [OF PO_refines_from_refines]

lemmas INV_trans_from_Refinement = 
  INV_trans_from_refinement [OF PO_refines_from_refines]

lemmas INV_from_Refinement = 
  INV_from_refinement [OF PO_refines_from_refines]


end

Theory HO_Transition_System

(*<*)
theory HO_Transition_System
imports Heard_Of.HOModel Refinement
begin
(*>*)

subsection ‹Transition system semantics for HO models›

text ‹The HO development already defines two trace semantics for algorithms in this model, the
coarse- and fine-grained ones. However, both of these are defined on infinite traces. Since the
semantics of our transition systems are defined on finite traces, we also provide such a semantics
for the HO model. Since we only use refinement for safety properties, the result also extend to
infinite traces (although we do not prove this in Isabelle).›

definition CHO_trans where
"CHO_trans A HOs SHOs coord = 
  {((r, st), (r', st'))|r r' st st'.
      r' = Suc r
       CSHOnextConfig A r st (HOs r) (SHOs r) (coord r) st'
  }"

definition CHO_to_TS :: 
  "('proc, 'pst, 'msg) CHOAlgorithm 
   (nat  'proc HO)
   (nat  'proc HO)
   (nat  'proc coord) 
   (nat × ('proc  'pst)) TS" 
where
  "CHO_to_TS A HOs SHOs coord  
    init = {(0, st)|st. CHOinitConfig A st (coord 0)},
    trans = CHO_trans A HOs SHOs coord
  "


definition get_msgs ::
  "('proc  'proc  'pst  'msg)
   ('proc  'pst)
   'proc HO
   'proc HO
   'proc  ('proc  'msg)set"
where
  "get_msgs snd_f cfg HO SHO  λp.
   {μ. (q. q  HO p  μ q  None)
      (q. q  SHO p  HO p  μ q = Some (snd_f q p (cfg q)))}"

definition CSHO_trans_alt
  :: 
  "(nat  'proc  'proc  'pst  'msg)
   (nat  'proc  'pst  ('proc  'msg)  'proc  'pst  bool)
   (nat  'proc HO)
   (nat  'proc HO)
   (nat  'proc  'proc)
   ((nat × ('proc  'pst)) × (nat × ('proc  'pst)))set"
where
  "CSHO_trans_alt snd_f nxt_st HOs SHOs coords 
    r μ. {((r, cfg), (Suc r, cfg'))|cfg cfg'. p.
      μ p  (get_msgs (snd_f r) cfg (HOs r) (SHOs r) p)
       (p. nxt_st r p (cfg p) (μ p) (coords r p) (cfg' p))
    }"

lemma CHO_trans_alt:
  "CHO_trans A HOs SHOs coords = CSHO_trans_alt (sendMsg A) (CnextState A) HOs SHOs coords"
  apply(rule equalityI)
   apply(force simp add: CHO_trans_def CSHO_trans_alt_def CSHOnextConfig_def SHOmsgVectors_def 
    get_msgs_def restrict_map_def map_add_def choice_iff)
  apply(force simp add: CHO_trans_def CSHO_trans_alt_def CSHOnextConfig_def SHOmsgVectors_def 
    get_msgs_def restrict_map_def map_add_def)
  done

definition K where
  "K y  λx. y"

lemma SHOmsgVectors_get_msgs:
  "SHOmsgVectors A r p cfg HOp SHOp = get_msgs (sendMsg A r) cfg (K HOp) (K SHOp) p"
  by(auto simp add: SHOmsgVectors_def get_msgs_def K_def)

lemma get_msgs_K:
  "get_msgs snd_f cfg (K (HOs r p)) (K (SHOs r p)) p
  = get_msgs snd_f cfg (HOs r) (SHOs r) p"
  by(auto simp add: get_msgs_def K_def)

lemma CSHORun_get_msgs:
  "CSHORun (A ::  ('proc, 'pst, 'msg) CHOAlgorithm) rho HOs SHOs coords = (
     CHOinitConfig A (rho 0) (coords 0)
    (r. μ. 
    (p.
      μ p  get_msgs (sendMsg A r) (rho r) (HOs r) (SHOs r) p
       CnextState A r p (rho r p) (μ p) (coords (Suc r) p) (rho (Suc r) p))))"
   by(auto simp add: CSHORun_def CSHOnextConfig_def SHOmsgVectors_get_msgs nextState_def get_msgs_K
     Bex_def choice_iff)

lemmas CSHORun_step = CSHORun_get_msgs[THEN iffD1, THEN conjunct2]

lemma get_msgs_dom:
  "msgs  get_msgs send s HOs SHOs p  dom msgs = HOs p"
  by(auto simp add: get_msgs_def)

lemma get_msgs_benign:
  "get_msgs snd_f cfg HOs HOs p = { (Some o (λq. (snd_f q p (cfg q)))) |` (HOs p)}"
  by(auto simp add: get_msgs_def restrict_map_def)

end

Theory Voting

section ‹The Voting Model›

theory Voting imports Refinement Consensus_Misc Quorums
begin

subsection ‹Model definition›
(******************************************************************************)

record v_state = 
  (* We want 0 to be the first round, and we also have to use something in the initial state
     - hence next_round *)
  next_round :: round 
  votes :: "round  (process, val) map"
  decisions :: "(process, val)map"

text ‹Initially, no rounds have been executed (the next round is 0), no votes have been
  cast, and no decisions have been made.›

definition v_init :: "v_state set" where
  "v_init = {  next_round = 0, votes = λr a. None, decisions = Map.empty  }"  

context quorum_process begin

definition quorum_for :: "process set  val  (process, val)map  bool" where
  quorum_for_def':
  "quorum_for Q v v_f  Q  Quorum  v_f ` Q = {Some v}"

text ‹The following definition of @{term quorum_for} is easier to reason about in Isabelle.›

lemma quorum_for_def:
  "quorum_for Q v v_f = (Q  Quorum  (p  Q. v_f p = Some v))"
  by(auto simp add: quorum_for_def' image_def dest: quorum_non_empty)

definition locked_in_vf :: "(process, val)map  val  bool" where
  "locked_in_vf v_f v  Q. quorum_for Q v v_f"

definition locked_in :: "v_state  round  val  bool" where
  "locked_in s r v = locked_in_vf (votes s r) v"

definition d_guard :: "(process  val option)  (process  val option)  bool" where
  "d_guard r_decisions r_votes  p v.
    r_decisions p = Some v  locked_in_vf r_votes v"

definition no_defection :: "v_state  (process, val)map  round  bool" where
  no_defection_def':
  "no_defection s r_votes r  
    r' < r. Q  Quorum. v. (votes s r') ` Q = {Some v}  r_votes ` Q  {None, Some v}"

text ‹The following definition of @{term no_defection} is easier to reason about in Isabelle.›

lemma no_defection_def:
  "no_defection s round_votes r =
    (r' < r. a Q v. quorum_for Q v (votes s r')  a  Q  round_votes a  {None, Some v})"
  apply(auto simp add: no_defection_def' Ball_def quorum_for_def')
   apply(blast)
  by (metis option.discI option.inject)
  
definition locked :: "v_state  val set" where
  "locked s = {v. r. locked_in s r v}"

text ‹The sole system event.›

definition v_round :: "round  (process, val)map  (process, val)map  (v_state × v_state) set" where
  "v_round r r_votes r_decisions = {(s, s').
     ― ‹guards›
     r = next_round s
      no_defection s r_votes r
      d_guard r_decisions r_votes
      ― ‹actions›
     s' = s 
       next_round := Suc r,
       votes := (votes s)(r := r_votes),
       decisions := (decisions s) ++ r_decisions
     
  }"

lemmas v_evt_defs = v_round_def

definition v_trans :: "(v_state × v_state) set" where
  "v_trans = (r v_f d_f. v_round r v_f d_f)  Id"

definition v_TS :: "v_state TS" where
  "v_TS =  init = v_init, trans = v_trans "

lemmas v_TS_defs = v_TS_def v_init_def v_trans_def


subsection ‹Invariants›
(******************************************************************************)

text ‹The only rounds where votes could have been cast are the ones 
  preceding the next round.›
definition Vinv1 where
  "Vinv1 = {s. r. next_round s  r  votes s r = Map.empty }"

lemmas Vinv1I = Vinv1_def [THEN setc_def_to_intro, rule_format]
lemmas Vinv1E [elim] = Vinv1_def [THEN setc_def_to_elim, rule_format]
lemmas Vinv1D = Vinv1_def [THEN setc_def_to_dest, rule_format]

text ‹The votes cast must respect the @{term no_defection} property.› 
definition Vinv2 where
  "Vinv2 = {s. r. no_defection s (votes s r) r }"

lemmas Vinv2I = Vinv2_def [THEN setc_def_to_intro, rule_format]
lemmas Vinv2E [elim] = Vinv2_def [THEN setc_def_to_elim, rule_format]
lemmas Vinv2D = Vinv2_def [THEN setc_def_to_dest, rule_format]

definition Vinv3 where
  "Vinv3 = {s. ran (decisions s)  locked s}"

lemmas Vinv3I = Vinv3_def [THEN setc_def_to_intro, rule_format]
lemmas Vinv3E [elim] = Vinv3_def [THEN setc_def_to_elim, rule_format]
lemmas Vinv3D = Vinv3_def [THEN setc_def_to_dest, rule_format]

subsubsection ‹Proofs of invariants›
(******************************************************************************)

(*************************) 
lemma Vinv1_v_round: 
  "{Vinv1} v_round r v_f d_f {> Vinv1}" 
  by(auto simp add: PO_hoare_defs v_round_def intro!: Vinv1I)

lemmas Vinv1_event_pres = Vinv1_v_round

lemma Vinv1_inductive:
  "init v_TS  Vinv1"
  "{Vinv1} trans v_TS {> Vinv1}"
  apply (simp add: v_TS_defs Vinv1_def)
  by (auto simp add: v_TS_defs Vinv1_event_pres)

lemma Vinv1_invariant: "reach v_TS  Vinv1"
  by (rule inv_rule_basic, auto intro!: Vinv1_inductive)

text ‹The following two lemmas will be useful later, when we
  start taking votes with the maximum timestamp.›

lemma Vinv1_finite_map_graph:
   "s  Vinv1  finite (map_graph (case_prod (votes s)))"
  apply(rule finite_dom_finite_map_graph)
  apply(rule finite_subset[where B="{0..< v_state.next_round s} × UNIV"])
   apply(auto simp add: Vinv1_def dom_def not_le[symmetric])
  done

lemma Vinv1_finite_vote_set:
   "s  Vinv1  finite (vote_set (votes s) Q)"
   apply(drule Vinv1_finite_map_graph)
   apply(clarsimp simp add: map_graph_def fun_graph_def vote_set_def)
   apply(erule finite_surj[where f="λ((r, a), v). (r, v)"])
   by(force simp add: image_def)   

lemma process_mru_map_add:
  assumes
    "s  Vinv1"
  shows 
    "process_mru ((votes s)(next_round s := v_f)) = 
    (process_mru (votes s) ++ (λp. map_option (Pair (next_round s)) (v_f p)))"
proof-
  from assms[THEN Vinv1D] have empty: "r'  next_round s. votes s r' = Map.empty"
    by simp
  show ?thesis
    by(auto  simp add: process_mru_new_votes[OF empty] map_add_def split: option.split)
qed

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

lemma no_defection_empty:
  "no_defection s Map.empty r'"
  by(auto simp add: no_defection_def)

lemma no_defection_preserved:
assumes
  "s  Vinv1"
  "r = next_round s"
  "no_defection s v_f r"
  "no_defection s (votes s r') r'"
  "votes s' = (votes s)(r := v_f)"
shows 
  "no_defection s' (votes s' r') r'" using assms
  by(force simp add: no_defection_def)
  
(********)

lemma Vinv2_v_round: 
  "{Vinv2  Vinv1} v_round r v_f d_f {> Vinv2}" 
  apply(auto simp add: PO_hoare_defs intro!: Vinv2I)
  apply(rename_tac s' r' s)
  apply(erule no_defection_preserved)
      apply(auto simp add: v_round_def intro!: v_state.equality)
  done

lemmas Vinv2_event_pres = Vinv2_v_round

lemma Vinv2_inductive:
  "init v_TS  Vinv2"
  "{Vinv2  Vinv1} trans v_TS {> Vinv2}" 
  apply(simp add: v_TS_defs Vinv2_def no_defection_def)
  by (auto simp add: v_TS_defs Vinv2_event_pres)

lemma Vinv2_invariant: "reach v_TS  Vinv2"
  by (rule inv_rule_incr, auto intro: Vinv2_inductive Vinv1_invariant del: subsetI)

(*************************)
lemma locked_preserved:
assumes
  "s  Vinv1"
  "r = next_round s"
  "votes s' = (votes s)(r := v_f)"
shows 
  "locked s  locked s'" using assms
  apply(auto simp add: locked_def locked_in_def locked_in_vf_def quorum_for_def dest!: Vinv1D)
  by (metis option.distinct(1))
  

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

lemma Vinv3_v_round: 
  "{Vinv3  Vinv1} v_round r v_f d_f {> Vinv3}"
proof(clarsimp simp add: PO_hoare_defs, intro Vinv3I, safe)
  fix s s' v
  assume step: "(s, s')  v_round r v_f d_f" and inv3: "s  Vinv3" and inv1: "s  Vinv1"
  and dec: "v  ran (decisions s')"
  have "locked s  locked s'" using step
    by(intro locked_preserved[OF inv1, where s'=s']) (auto simp add: v_round_def)
  with Vinv3D[OF inv3] step dec
  show "v  locked s'"
    apply(auto simp add: v_round_def dest!: ran_map_addD)
    apply(auto simp add: locked_def locked_in_def d_guard_def ran_def)
    done
qed

lemmas Vinv3_event_pres = Vinv3_v_round

lemma Vinv3_inductive:
  "init v_TS  Vinv3"
  "{Vinv3  Vinv1} trans v_TS {> Vinv3}" 
  apply(simp add: v_TS_defs Vinv3_def no_defection_def)
  by (auto simp add: v_TS_defs Vinv3_event_pres)

lemma Vinv3_invariant: "reach v_TS  Vinv3"
  by (rule inv_rule_incr, auto intro: Vinv3_inductive Vinv1_invariant del: subsetI)


subsection ‹Agreement and stability›
(******************************************************************************)

text ‹Only a singe value can be locked within the votes for one round.›
lemma locked_in_vf_same:
  " locked_in_vf v_f v; locked_in_vf v_f w   v = w" using qintersect
  apply(auto simp add: locked_in_vf_def quorum_for_def image_iff)
  by (metis Int_iff all_not_in_conv option.inject)

text ‹In any reachable state, no two different values can be locked in
  different rounds.›
theorem locked_in_different:
assumes
  "s  Vinv2"
  "locked_in s r1 v"
  "locked_in s r2 w"
  "r1 < r2"
shows
  "v = w"
proof- 
  ― ‹To be locked, @{term v} and @{term w} must each have received votes from a quorum.›
  from assms(2-3) obtain Q1 Q2 
  where Q12: "Q1  Quorum" "Q2  Quorum" "quorum_for Q1 v (votes s r1)" "quorum_for Q2 w (votes s r2)"
    by(auto simp add: locked_in_def locked_in_vf_def quorum_for_def)
  ― ‹By the quorum intersection property, some process from @{term Q1} voted for @{term w}:›
  then obtain a where "a  Q1" "votes s r2 a = Some w" 
    using qintersect[OF Q1  Quorum Q2  Quorum]
    by(auto simp add: quorum_for_def)
  ― ‹But from @{term Vinv2} we conclude that @{term a} could not have defected by voting
        @{term w}, so @{term ?thesis}:›
  thus ?thesis using s  Vinv2› ‹quorum_for Q1 v (votes s r1) r1 < r2
    by(fastforce simp add: Vinv2_def no_defection_def quorum_for_def')
qed

text ‹It is simple to extend the previous theorem to any two (not necessarily different) rounds.›
theorem locked_unique: 
assumes 
  "s  Vinv2"
  "v  locked s" "w  locked s"
shows 
  "v = w"
proof -
  from assms(2-3) obtain r1 r2 where quoIn: "locked_in s r1 v" "locked_in s r2 w"
    by (auto simp add: locked_def)
  have "r1 < r2  r1 = r2  r2 < r1" by (rule linorder_less_linear) 
  thus ?thesis
  proof (elim disjE)
    assume "r1 = r2"
    with quoIn show ?thesis
      by(simp add: locked_in_def locked_in_vf_same)
  qed(auto intro: locked_in_different[OF s  Vinv2›] quoIn sym)
qed

text ‹We now prove that decisions are stable; once a process makes a decision, it never
  changes it, and it does not go back to an undecided state. Note that behaviors grow at 
  the front; hence @{term "tr ! (i-j)"} is later in the trace than @{term "tr ! i"}.›
lemma stable_decision:
  assumes beh: "tr  beh v_TS"
  and len: "i < length tr"
  and s: "s = nth tr i"
  and t: "t = nth tr (i - j)"
  and dec: 
    "decisions s p = Some v"
  shows
    "decisions t p = Some v"
proof-
  ― ‹First, we show that the both @{term s} and @{term t} respect the invariants.›
  have reach: "s  reach v_TS" "t  reach v_TS" using beh s t len
     apply(simp_all add: reach_equiv_beh_states)
     apply (metis len nth_mem) 
    apply (metis less_imp_diff_less nth_mem)
    done
  hence invs2: "s  Vinv2" and invs3: "s  Vinv3"
    by(blast dest: Vinv2_invariant[THEN subsetD] Vinv3_invariant[THEN subsetD])+
    
  show ?thesis using t
  proof(induction j arbitrary: t)
    case (Suc j)
    hence dec_j: "decisions (tr ! (i - j)) p = Some v" 
      by simp
    thus "decisions t p = Some v" using Suc
    ― ‹As @{term "(-)"} is a total function on naturals, we perform a case distinction;
          if @{term "i < j"}, the induction step is trivial.›
    proof(cases "i  j") 
      ― ‹The non-trivial case.›
      case False
      define t' where "t' = tr ! (i - j)"
      ― ‹Both @{term t} and @{term t'} are reachable, thus respect the invariants, and
        they are related by the transition relation.›
      hence "t'  reach v_TS" "t  reach v_TS" using beh len Suc
        by (metis beh_in_reach less_imp_diff_less nth_mem)+
      hence invs: "t'  Vinv1" "t'  Vinv3" "t  Vinv2" "t  Vinv3"
        by(blast dest: Vinv1_invariant[THEN subsetD] Vinv2_invariant[THEN subsetD] 
          Vinv3_invariant[THEN subsetD])+
      hence locked_v: "v  locked t'" using Suc
        by(auto simp add: t'_def intro: ranI)
      have "i - j = Suc (i - (Suc j))" using False
        by simp
      hence trans: "(t', t)  trans v_TS" using beh len Suc 
        by(auto simp add: t'_def intro!: beh_consecutive_in_trans)
      ― ‹Thus @{term v} also remains locked in @{term t}, and @{term p} does not 
        revoke, nor change its decision.›
      hence locked_v_t: "v  locked t" using locked_v
        by(auto simp add: v_TS_defs v_round_def
          intro: locked_preserved[OF invs(1), THEN subsetD, OF _ _ locked_v])
      from trans obtain w where "decisions t p = Some w" using dec_j
        by(fastforce simp add: t'_def v_TS_defs v_round_def 
          split: option.split option.split_asm)
      thus ?thesis using invs(4)[THEN Vinv3D] locked_v_t locked_unique[OF invs(3)]
        by (metis contra_subsetD ranI)
    qed(auto)
  next
    case 0
    thus "decisions t p = Some v" using assms
      by auto
  qed
qed

text ‹Finally, we prove that the Voting model ensures agreement. Without a loss 
  of generality, we assume that t› preceeds s› in the trace.›
lemma Voting_agreement:
  assumes beh: "tr  beh v_TS"
  and len: "i < length tr"
  and s: "s = nth tr i"
  and t: "t = nth tr (i - j)"
  and dec: 
    "decisions s p = Some v"
    "decisions t q = Some w"
  shows "w = v"
proof-
  ― ‹Again, we first prove that the invariants hold for @{term s}.›
  have reach: "s  reach v_TS" using beh s t len
    apply(simp_all add: reach_equiv_beh_states)
    by (metis nth_mem)
  hence invs2: "s  Vinv2" and invs3: "s  Vinv3"
    by(blast dest: Vinv2_invariant[THEN subsetD] Vinv3_invariant[THEN subsetD])+

  ― ‹We now proceed to prove the thesis by induction.›
  thus ?thesis using assms
  proof(induction j arbitrary: t)
    case 0
    hence
      "v  locked (tr ! i)"
      "w  locked (tr ! i)"
      by(auto intro: ranI)
    thus ?thesis using invs2 using assms 0
      by(auto dest: locked_unique)
  next
    case (Suc j)
    thus ?thesis
    ― ‹Again, the totality of @{term "(-)"} makes the claim trivial if @{term "i < j"}.›
    proof(cases "i  j")
      case False
      ― ‹In the non-trivial case, the proof follows from the decision stability theorem 
        and the uniqueness of locked values.›
      have dec_t: "decisions t p = Some v" using Suc
        by(auto intro: stable_decision[OF beh len s ])
      have "t  reach v_TS" using beh len Suc
        by (metis beh_in_reach less_imp_diff_less nth_mem)
      hence invs: "t  Vinv2" "t  Vinv3"
        by(blast dest: Vinv2_invariant[THEN subsetD] Vinv3_invariant[THEN subsetD])+
      from dec_t have "v  locked t" using invs(2)
        by(auto intro: ranI) 
      moreover have locked_w_t: "w  locked t" using Suc t  Vinv3›[THEN Vinv3D]
        by(auto intro: ranI)
      ultimately show ?thesis using locked_unique[OF t  Vinv2›]
        by blast
    qed(auto)
  qed
qed

end (* context quorum *)

end

Theory Voting_Opt

section ‹The Optimized Voting Model›

theory Voting_Opt
imports Voting
begin

subsection ‹Model definition›
(*****************************************************************************)

record opt_v_state = 
  next_round :: round 
  last_vote :: "(process, val) map"
  decisions :: "(process, val)map"

definition flv_init where
  "flv_init = {  next_round = 0, last_vote = Map.empty, decisions = Map.empty  }"

context quorum_process begin

definition fmru_lv :: "(process, round × val)map  (process set, round × val)map" where
  "fmru_lv lvs Q = option_Max_by fst (ran (lvs |` Q))"

definition flv_guard :: "(process, round × val)map  process set  val  bool" where
  "flv_guard lvs Q v  Q  Quorum  
    (let alv = fmru_lv lvs Q in alv = None  (r. alv = Some (r, v)))"

definition opt_no_defection :: "opt_v_state  (process, val)map  bool" where
  opt_no_defection_def':
    "opt_no_defection s round_votes  
    v. Q. quorum_for Q v (last_vote s)  round_votes ` Q  {None, Some v}"

lemma opt_no_defection_def:
  "opt_no_defection s round_votes =
    (a Q v. quorum_for Q v (last_vote s)  a  Q  round_votes a  {None, Some v})"
  apply(auto simp add: opt_no_defection_def')
  by (metis option.distinct(1) option.sel)
                    
definition flv_round :: "round  (process, val)map   (process, val)map  (opt_v_state × opt_v_state) set" where
  "flv_round r r_votes r_decisions = {(s, s').
     ― ‹guards›
     r = next_round s
      opt_no_defection s r_votes
      d_guard r_decisions r_votes
      ― ‹actions›
     s' = s 
       next_round := Suc r
       , last_vote := last_vote s ++ r_votes
       , decisions := (decisions s) ++ r_decisions
     
  }"

lemmas flv_evt_defs = flv_round_def flv_guard_def

definition flv_trans :: "(opt_v_state × opt_v_state) set" where
  "flv_trans = (r v_f d_f. flv_round r v_f d_f)"

definition flv_TS :: "opt_v_state TS" where
  "flv_TS =  init = flv_init, trans = flv_trans "

lemmas flv_TS_defs = flv_TS_def flv_init_def flv_trans_def

subsection ‹Refinement›
(******************************************************************************)

definition flv_ref_rel :: "(v_state × opt_v_state)set" where
  "flv_ref_rel = {(sa, sc).
    sc = 
      next_round = v_state.next_round sa
      , last_vote = map_option snd o (process_mru (votes sa))
      , decisions = v_state.decisions sa
    
  }"

subsubsection ‹Guard strengthening›
(******************************************************************************)

lemma process_mru_Max:
  assumes 
    inv: "sa  Vinv1"
    and process_mru: "process_mru (votes sa) p = Some (r, v)"
  shows 
    "votes sa r p = Some v  (r' > r. votes sa r' p = None)"
proof-
  from process_mru have not_empty: "vote_set (votes sa) {p}  {}"
    by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def)
  note Max_by_conds = Vinv1_finite_vote_set[OF inv] this
  from Max_by_dest[OF Max_by_conds, where f=fst]
  have
    r: 
      "(r, v) = Max_by fst (vote_set (votes sa) {p})" 
      "votes sa r p = Some v" 
      using process_mru
      by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def vote_set_def)
  have "r' >r . votes sa r' p = None"
  proof(safe)
    fix r'
    assume less: "r < r'"
    hence "v. (r', v)  vote_set (votes sa) {p}" using process_mru
      by(auto dest!: Max_by_ge[where f=fst, OF Vinv1_finite_vote_set[OF inv]] 
        simp add: process_mru_def mru_of_set_def option_Max_by_def)
    thus "votes sa r' p = None"
      by(auto simp add: vote_set_def)
  qed
  thus ?thesis using r(2)
    by(auto)
qed

lemma opt_no_defection_imp_no_defection:
  assumes
    conc_guard: "opt_no_defection sc round_votes"
    and R: "(sa, sc)  flv_ref_rel"
    and ainv: "sa  Vinv1" "sa  Vinv2"
  shows
    "no_defection sa round_votes r"
proof(unfold no_defection_def, safe)
  fix r' v a Q w
  assume
    r'_less: "r' < r"
    and a_votes_w: "round_votes a = Some w"
    and Q: "quorum_for Q v (votes sa r')"
    and a_in_Q: "a  Q"
  have "Q  Quorum" using Q
    by(auto simp add: quorum_for_def)
  hence "quorum_for Q v (last_vote sc)"
  proof(clarsimp simp add: quorum_for_def)
    fix q
    assume "q  Q"
    with Q have q_r': "votes sa r' q = Some v"
      by(auto simp add: quorum_for_def)
    hence votes: "vote_set (votes sa) {q}  {}"
      by(auto simp add: vote_set_def)
    then obtain w where w: "last_vote sc q = Some w" using R
      by(clarsimp simp add: flv_ref_rel_def process_mru_def mru_of_set_def
        option_Max_by_def)
    with R obtain r_max where "process_mru (votes sa) q = Some (r_max, w)"
      by(clarsimp simp add: flv_ref_rel_def)
    from process_mru_Max[OF ainv(1) this] q_r' have
      "votes sa r_max q = Some w" 
      "r'  r_max"
      using q_r'
      by(auto simp add: not_less[symmetric])
    thus "last_vote sc q = Some v" using ainv(2) Q q  Q
      apply(case_tac "r_max = r'")
       apply(clarsimp simp add: w Vinv2_def no_defection_def q_r' dest: le_neq_implies_less)
      apply(fastforce simp add: w Vinv2_def no_defection_def q_r' dest!: le_neq_implies_less)
      done
  qed
  thus "round_votes a = Some v" using conc_guard a_in_Q a_votes_w r'_less
    by(fastforce simp add: opt_no_defection_def)
qed

subsubsection ‹Action refinement›
(******************************************************************************)

lemma act_ref:
  assumes
    inv: "s  Vinv1"
  shows 
    "map_option snd o (process_mru ((votes s)(v_state.next_round s := v_f)))
    = ((map_option snd o (process_mru (votes s))) ++ v_f)"
    by(auto simp add: process_mru_map_add[OF inv] map_add_def split: option.split)

subsubsection ‹The complete refinement proof›
(******************************************************************************)

lemma flv_round_refines:
  "{flv_ref_rel  (Vinv1  Vinv2) × UNIV}
    v_round r v_f  d_f, flv_round r v_f d_f
  {> flv_ref_rel}"
  by(auto simp add: PO_rhoare_defs flv_round_def v_round_def 
    flv_ref_rel_def act_ref
    intro: opt_no_defection_imp_no_defection)
  
lemma Last_Voting_Refines:
  "PO_refines (flv_ref_rel  (Vinv1  Vinv2) × UNIV) v_TS flv_TS"
proof(rule refine_using_invariants)
  show "init flv_TS  flv_ref_rel `` init v_TS"
    by(auto simp add: flv_TS_defs v_TS_defs flv_ref_rel_def
      process_mru_def mru_of_set_def vote_set_def option_Max_by_def)
next
  show 
    "{flv_ref_rel  (Vinv1  Vinv2) × UNIV} trans v_TS, trans flv_TS {> flv_ref_rel}"
    by(auto simp add: v_TS_defs flv_TS_defs intro!: flv_round_refines)
next
  show
    "{Vinv1  Vinv2  Domain (flv_ref_rel  UNIV × UNIV)} 
      trans v_TS 
    {> Vinv1  Vinv2}" 
    using Vinv1_inductive(2) Vinv2_inductive(2)
    by blast
qed(auto intro!: Vinv1_inductive(1) Vinv2_inductive(1))

end

end

Theory OneThirdRule_Defs

section ‹The OneThirdRule Algorithm›

theory OneThirdRule_Defs
imports Heard_Of.HOModel "../Consensus_Types"
begin

text ‹The contents of this file have been taken almost verbatim from the
  Heard Of Model AFP entry. The only difference is that the types have been
  changed.›


subsection ‹Model of the algorithm›

text ‹
  The state of each process consists of two fields: last_vote› holds
  the current value proposed by the process and decision› the
  value (if any, hence the option type) it has decided.
›

record 'val pstate =
  last_vote :: "'val"
  decision :: "'val option"

text ‹
  The initial value of field last_vote› is unconstrained, but no decision
  has been taken initially.
›

definition OTR_initState where
  "OTR_initState p st  decision st = None"

text ‹
  Given a vector msgs› of values (possibly null) received from 
  each process, @{term "HOV msgs v"} denotes the set of processes from
  which value v› was received.
›

definition HOV :: "(process  'val option)  'val  process set" where
  "HOV msgs v  { q . msgs q = Some v }"

text @{term "MFR msgs v"} (``most frequently received'') holds for
  vector msgs› if no value has been received more frequently
  than v›.

  Some such value always exists, since there is only a finite set of
  processes and thus a finite set of possible cardinalities of the
  sets @{term "HOV msgs v"}.
›

definition MFR :: "(process  'val option)  'val  bool" where
  "MFR msgs v  w. card (HOV msgs w)  card (HOV msgs v)"

lemma MFR_exists: "v. MFR msgs v"
proof -
  let ?cards = "{ card (HOV msgs v) | v . True }"
  let ?mfr = "Max ?cards"
  have "v. card (HOV msgs v)  N" by (auto intro: card_mono)
  hence "?cards  { 0 .. N }" by auto
  hence fin: "finite ?cards" by (metis atLeast0AtMost finite_atMost finite_subset)
  hence "?mfr  ?cards" by (rule Max_in) auto
  then obtain v where v: "?mfr = card (HOV msgs v)" by auto
  have "MFR msgs v"
  proof (auto simp: MFR_def)
    fix w
    from fin have "card (HOV msgs w)  ?mfr" by (rule Max_ge) auto
    thus "card (HOV msgs w)  card (HOV msgs v)" by (unfold v)
  qed
  thus ?thesis ..
qed

text ‹
  Also, if a process has heard from at least one other process,
  the most frequently received values are among the received messages.
›

lemma MFR_in_msgs:
  assumes HO:"HOs m p  {}"
      and v: "MFR (HOrcvdMsgs OTR_M m p (HOs m p) (rho m)) v"
             (is "MFR ?msgs v")
  shows "q  HOs m p. v = the (?msgs q)"
proof -
  from HO obtain q where q: "q  HOs m p"
    by auto
  with v have "HOV ?msgs (the (?msgs q))  {}"
    by (auto simp: HOV_def HOrcvdMsgs_def)
  hence HOp: "0 < card (HOV ?msgs (the (?msgs q)))"
    by auto
  also from v have "  card (HOV ?msgs v)"
    by (simp add: MFR_def)
  finally have "HOV ?msgs v  {}"
    by auto
  thus ?thesis
    by (auto simp: HOV_def HOrcvdMsgs_def)
qed

text @{term "TwoThirds msgs v"} holds if value v› has been
  received from more than $2/3$ of all processes.
›

definition TwoThirds where
  "TwoThirds msgs v  (2*N) div 3 < card (HOV msgs v)"

text ‹
  The next-state relation of algorithm \emph{One-Third Rule} for every process
  is defined as follows:
  if the process has received values from more than $2/3$ of all processes,
  the last_vote› field is set to the smallest among the most frequently received
  values, and the process decides value $v$ if it received $v$ from more than
  $2/3$ of all processes. If p› hasn't heard from more than $2/3$ of
  all processes, the state remains unchanged.
  (Note that Some› is the constructor of the option datatype, whereas
  ϵ› is Hilbert's choice operator.)
  We require the type of values to be linearly ordered so that the minimum
  is guaranteed to be well-defined.
›

definition OTR_nextState where
  "OTR_nextState r p (st::('val::linorder) pstate) msgs st'  
   if (2*N) div 3 < card {q. msgs q  None}
   then st' =  last_vote = Min {v . MFR msgs v},
          decision = (if (v. TwoThirds msgs v)
                    then Some (ϵv. TwoThirds msgs v)
                    else decision st) 
   else st' = st"

text ‹
  The message sending function is very simple: at every round, every process
  sends its current proposal (field last_vote› of its local state) to all 
  processes.
›

definition OTR_sendMsg where
  "OTR_sendMsg r p q st  last_vote st"

subsection ‹Communication predicate for \emph{One-Third Rule}›

text ‹
  We now define the communication predicate for the \emph{One-Third Rule}
  algorithm to be correct.
  It requires that, infinitely often, there is a round where all processes
  receive messages from the same set Π› of processes where Π›
  contains more than two thirds of all processes.
  The ``per-round'' part of the communication predicate is trivial.
›

definition OTR_commPerRd where
  "OTR_commPerRd HOrs  True"

definition OTR_commGlobal where
  "OTR_commGlobal HOs 
    r. r0 Π. r0  r  (p. HOs r0 p = Π)  card Π > (2*N) div 3"

subsection ‹The \emph{One-Third Rule} Heard-Of machine›

text ‹
  We now define the HO machine for the \emph{One-Third Rule} algorithm
  by assembling the algorithm definition and its communication-predicate.
  Because this is an uncoordinated algorithm, the crd› arguments
  of the initial- and next-state predicates are unused.
›

definition OTR_HOMachine where
  "OTR_HOMachine =
     CinitState =  (λ p st crd. OTR_initState p st),
     sendMsg =  OTR_sendMsg,
     CnextState = (λ r p st msgs crd st'. OTR_nextState r p st msgs st'),
     HOcommPerRd = OTR_commPerRd,
     HOcommGlobal = OTR_commGlobal "

abbreviation "OTR_M  OTR_HOMachine::(process, 'val::linorder pstate, 'val) HOMachine"

end

Theory OneThirdRule_Proofs

(*<*)
theory OneThirdRule_Proofs
imports Heard_Of.Majorities 
  "../HO_Transition_System" "../Voting_Opt" OneThirdRule_Defs
begin
(*>*)

subsection ‹Proofs›

definition majs :: "(process set) set" where
  "majs  {S. card S > (2 * N) div 3}"

lemma card_Compl:
  fixes S :: "('a :: finite) set"
  shows "card (-S) = card (UNIV :: 'a set) - card S"
proof-
  have "card S + card (-S) = card (UNIV :: 'a set)"
    by(rule card_Un_disjoint[of S "-S", simplified Compl_partition, symmetric])
      (auto)
  thus ?thesis
    by simp
qed

lemma m_mult_div_Suc_m:
  "n > 0  m * n div Suc m < n"
  by (simp add: less_mult_imp_div_less)
  
interpretation majorities: quorum_process majs
proof
  fix Q Q' assume "Q  majs" "Q'  majs"
  hence "(4 * N) div 3 < card Q + card Q'"
    by(auto simp add: majs_def)
  thus "Q  Q'  {}"
    apply (intro majorities_intersect)
    apply(auto)
    done
next
  have "N > 0"
    by auto
  have "2 * N div 3 < N"
    by(simp only: eval_nat_numeral m_mult_div_Suc_m[OF ‹N > 0])
  thus "Q. Q  majs" 
    apply(rule_tac x=UNIV in exI)
    apply(auto simp add: majs_def intro!: div_less_dividend)
    done
qed

lemma card_Un_le:
  " finite A; finite B   card (A  B)  card A + card B"
  by(simp only: card_Un_Int)


lemma qintersect_card:
  assumes "Q  majs" "Q'  majs"
  shows "card (Q  Q') > card (Q  -Q')"
proof-
  have "card (Q  -Q')  card (-Q')"
    by(auto intro!: card_mono)
  also have "... < N - (card (-Q) + card (-Q'))"
  proof-
    have sum: "N < card Q + card Q'" using assms
      by(auto simp add: majs_def)
    have le_N: "card Q  N" "card Q'  N" by (auto intro!: card_mono)
    show ?thesis using assms sum
      apply(simp add: card_Compl)
      apply(intro diff_less_mono2)
      apply(auto simp add: majs_def card_Compl)
       apply(simp add: diff_add_assoc2[symmetric, OF le_N(1)] add_diff_assoc[OF le_N(2)])
      by (metis add_mono le_N(1) le_N(2) less_diff_conv2 nat_add_left_cancel_less) 
  qed              
  also have "...  card (Q  Q')"
  proof-
    have "N - (card (-Q) + card (-Q'))  card (-(-Q  -Q'))"
      apply(simp only: card_Compl[where S="-Q  -Q'"])
      apply(auto intro!: diff_le_mono2 card_Un_le)
      done
    thus ?thesis
      by(auto)
  qed
  finally show ?thesis . 
qed

axiomatization where val_linorder: 
  (* "class.finite TYPE(process)" *)
  "OFCLASS(val, linorder_class)"

instance val :: linorder by (rule val_linorder)

type_synonym p_TS_state = "(nat × (process  (val pstate)))"

definition K where
  "K y  λx. y"

definition OTR_Alg where
  "OTR_Alg =
     CinitState =  (λ p st crd. OTR_initState p st),
     sendMsg =  OTR_sendMsg,
     CnextState = (λ r p st msgs crd st'. OTR_nextState r p st msgs st')
   "

definition OTR_TS ::
  "(round  process HO)
   (round  process HO)
   (round  process)
   p_TS_state TS"
where
  "OTR_TS HOs SHOs crds = CHO_to_TS OTR_Alg HOs SHOs (K o crds)"

lemmas OTR_TS_defs = OTR_TS_def CHO_to_TS_def OTR_Alg_def CHOinitConfig_def
  OTR_initState_def

definition
  "OTR_trans_step HOs  r μ.
   {((r, cfg), Suc r, cfg')|cfg cfg'.
    (p. μ p  get_msgs (OTR_sendMsg r) cfg (HOs r) (HOs r) p) 
    (p. OTR_nextState r p (cfg p) (μ p) (cfg' p))}"

definition CSHOnextConfig where
  "CSHOnextConfig A r cfg HO SHO coord cfg' 
   p. μ  SHOmsgVectors A r p cfg (HO p) (SHO p).
          CnextState A r p (cfg p) μ (coord p) (cfg' p)"

type_synonym rHO = "nat  process HO"

subsubsection ‹Refinement›
(******************************************************************************)

definition otr_ref_rel :: "(opt_v_state × p_TS_state)set" where
  "otr_ref_rel =  {(sa, (r, sc)).
    r = next_round sa
     (p. decisions sa p = decision (sc p))
     majorities.opt_no_defection sa (Some o last_vote o sc)
  }"

lemma decide_origin:
  assumes 
    send: "μ p  get_msgs (OTR_sendMsg r) sc (HOs r) (HOs r) p"
    and nxt: "OTR_nextState r p (sc p) (μ p) (sc' p)"
    and new_dec: "decision (sc' p)  decision (sc p)"
  shows
    "v. decision (sc' p) = Some v  {q. last_vote (sc q) = v}  majs"
proof-
  from new_dec and nxt obtain v where 
    p_dec_v: "decision (sc' p) = Some v" 
    and two_thirds_v: "TwoThirds (μ p) v"
    apply(auto simp add: OTR_nextState_def split: if_split_asm)
    by (metis exE_some)
  then have "2 * N div 3 < card {q. last_vote (sc q) = v}" using send
    by(auto simp add: get_msgs_benign OTR_sendMsg_def TwoThirds_def HOV_def 
      restrict_map_def elim!: less_le_trans intro!: card_mono)
  with p_dec_v show ?thesis by (auto simp add: majs_def)
qed

lemma MFR_in_msgs:
  assumes HO:"dom msgs  {}"
      and v: "MFR msgs v"
  shows "q  dom msgs. v = the (msgs q)"
proof -
  from HO obtain q where q: "q  dom msgs"
    by auto
  with v have "HOV msgs (the (msgs q))  {}"
    by (auto simp: HOV_def )
  hence HOp: "0 < card (HOV msgs (the (msgs q)))"
    by auto
  also from v have "  card (HOV msgs v)"
    by (simp add: MFR_def)
  finally have "HOV msgs v  {}"
    by auto
  thus ?thesis
    by (force simp: HOV_def)
qed

lemma step_ref:
  "{otr_ref_rel} 
      (r v_f d_f. majorities.flv_round r v_f d_f), 
      OTR_trans_step HOs 
    {> otr_ref_rel}"
proof(simp add: PO_rhoare_defs OTR_trans_step_def, safe)
  fix sa r sc sc' μ
  assume
    R: "(sa, r, sc)  otr_ref_rel"
    and send: "p. μ p  get_msgs (OTR_sendMsg r) sc (HOs r) (HOs r) p"
    and nxt: "p. OTR_nextState r p (sc p) (μ p) (sc' p)"
  note step=send nxt
  define d_f
    where "d_f p = (if decision (sc' p)  decision (sc p) then decision (sc' p) else None)" for p

  define sa' where "sa' =  
    opt_v_state.next_round = Suc r
    , opt_v_state.last_vote = opt_v_state.last_vote sa ++ (Some o last_vote o sc) 
    , opt_v_state.decisions = opt_v_state.decisions sa ++ d_f
    "
  
  have "majorities.d_guard d_f (Some o last_vote o sc)"
  proof(clarsimp simp add: majorities.d_guard_def d_f_def)
    fix p v
    assume
      "Some v  decision (sc p)" 
      "decision (sc' p) = Some v"
    from this and 
      decide_origin[where μ=μ and HOs=HOs and sc'=sc', OF send[THEN spec, of p] nxt[THEN spec, of p]]
    show "quorum_process.locked_in_vf majs (Some  last_vote  sc) v"
      by(auto simp add: majorities.locked_in_vf_def majorities.quorum_for_def)
  qed
  hence
    "(sa, sa')  majorities.flv_round r (Some o last_vote o sc) d_f" using R
    by(auto simp add: majorities.flv_round_def otr_ref_rel_def sa'_def)
  moreover have "(sa', Suc r, sc')  otr_ref_rel"
  proof(unfold otr_ref_rel_def, safe)
    fix p
    show "opt_v_state.decisions sa' p = decision (sc' p)" using R nxt[THEN spec, of p]
      by(auto simp add: otr_ref_rel_def sa'_def map_add_def d_f_def OTR_nextState_def
        split: option.split)
  next
    show "quorum_process.opt_no_defection majs sa' (Some  last_vote  sc')"
    proof(clarsimp simp add: sa'_def majorities.opt_no_defection_def map_add_def majorities.quorum_for_def)
      fix Q p v
      assume Q: "Q  majs" and Q_v: "q  Q. last_vote (sc q) = v" and p_Q: "p  Q"
      hence old: "last_vote (sc p) = v" by simp
      have v_maj: "{q. last_vote (sc q) = v}  majs" using Q Q_v
        apply(simp add: majs_def)
        apply(erule less_le_trans, rule card_mono, auto)
        done
      show "last_vote (sc' p) = v"
      proof(rule ccontr)
        assume new: "last_vote (sc' p)  v"
        let ?w = "last_vote (sc' p)"
        have 
          w_MFR: "?w = Min {z. MFR (μ p) z}" (is "?w = Min ?MFRs") and dom_maj: "dom (μ p)  majs" 
          using old new nxt[THEN spec, where x=p]
          by(auto simp add: OTR_nextState_def majs_def dom_def split: if_split_asm)
        from dom_maj have not_empty: "dom (μ p)  {}" by(elim majorities.quorum_non_empty)
        from MFR_exists obtain mfr_v where mfr_v: "mfr_v  ?MFRs"
          by fastforce
        from not_empty obtain q z where "μ p q = Some z" by(fastforce)
        hence "0 < card (HOV (μ p) (the (μ p q)))"
          by(auto simp add: HOV_def)
        have "?w  {z. MFR (μ p) z}"
        proof(unfold w_MFR, rule Min_in)
          have "?MFRs  (the o (μ p)) ` (dom (μ p))" using not_empty
            by(auto simp: image_def intro: MFR_in_msgs)
          thus "finite ?MFRs" by (auto elim: finite_subset)
        qed(auto simp add: MFR_exists)
        hence card_HOV: "card (HOV (μ p) v)  card (HOV (μ p) ?w)"
          by(auto simp add: MFR_def)
        have "dom (μ p) = HOs r p" using send[THEN spec, where x=p]
          by(auto simp add: get_msgs_def)
        from this[symmetric] have "v'. HOV (μ p) v' = {q. last_vote (sc q) = v'}  dom (μ p)" 
          using send[THEN spec, where x=p]
          by(fastforce simp add: HOV_def get_msgs_benign OTR_sendMsg_def restrict_map_def)
        hence card_le1: "card ({q. last_vote (sc q) = v}  dom (μ p))  card ({q. last_vote (sc q) = ?w}  dom (μ p))"
          using card_HOV
          by(simp)
        have 
          "card ({q. last_vote (sc q) = v}  dom (μ p))  card ({q. last_vote (sc q)  v}  dom (μ p))"
          apply(rule le_trans[OF card_le1], rule card_mono)
           apply(auto simp add: new[symmetric])
          done
        thus False using qintersect_card[OF dom_maj v_maj]
          by(simp add: Int_commute Collect_neg_eq)
      qed
    qed
  qed(auto simp add: sa'_def)

  ultimately show 
    "sa'. (ra v_f d_f. (sa, sa')  quorum_process.flv_round majs ra v_f d_f) 
     (sa', Suc r, sc')  otr_ref_rel"
    by blast
qed

lemma OTR_Refines_LV_VOting:
  "PO_refines (otr_ref_rel) 
    majorities.flv_TS (OTR_TS HOs HOs crds)"
proof(rule refine_basic)
  show "init (OTR_TS HOs HOs crds)  otr_ref_rel `` init (quorum_process.flv_TS majs)"
    by(auto simp add: OTR_TS_def CHO_to_TS_def OTR_Alg_def CHOinitConfig_def OTR_initState_def
      majorities.flv_TS_def flv_init_def majorities.opt_no_defection_def majorities.quorum_for_def'
      otr_ref_rel_def)
next
  show 
    "{otr_ref_rel} TS.trans (quorum_process.flv_TS majs), TS.trans (OTR_TS HOs HOs crds) {> otr_ref_rel}"
    using step_ref
    by(simp add: majorities.flv_TS_defs OTR_TS_def CHO_to_TS_def OTR_Alg_def 
      CSHO_trans_alt_def CHO_trans_alt OTR_trans_step_def)
qed

subsubsection ‹Termination›
(******************************************************************************)

text ‹The termination proof for the algorithm is already given in the Heard-Of Model AFP
  entry, and we do not repeat it here.›


end

Theory Ate_Defs

section ‹The $A_{T,E}$ Algorithm›

theory Ate_Defs
imports Heard_Of.HOModel "../Consensus_Types"
begin

text ‹The contents of this file have been taken almost verbatim from the
  Heard Of Model AFP entry. The only difference is that the types have been
  changed.›

subsection ‹Model of the algorithm›

text ‹The following record models the local state of a process.›

record 'val pstate =
  x :: "'val"              ― ‹current value held by process›
  decide :: "'val option"  ― ‹value the process has decided on, if any›

text ‹
  The x› field of the initial state is unconstrained, but no
  decision has yet been taken.
›

definition Ate_initState where
  "Ate_initState p st  (decide st = None)"

locale ate_parameters =
  fixes α::nat and T::nat and E::nat
  assumes TNaE:"T  2*(N + 2*α - E)"
      and TltN:"T < N"
      and EltN:"E < N"

begin

text ‹The following are consequences of the assumptions on the parameters.›

lemma majE: "2 * (E - α)  N"
using TNaE TltN by auto

lemma Egta: "E > α"
using majE EltN by auto

lemma Tge2a: "T  2 * α"
using TNaE EltN by auto

text ‹
  At every round, each process sends its current x›.
  If it received more than T› messages, it selects the smallest value
  and store it in x›. As in algorithm \emph{OneThirdRule}, we
  therefore require values to be linearly ordered.

  If more than E› messages holding the same value are received,
  the process decides that value.
›

definition mostOftenRcvd where
  "mostOftenRcvd (msgs::process  'val option) 
   {v. w. card {qq. msgs qq = Some w}  card {qq. msgs qq = Some v}}"

definition 
  Ate_sendMsg :: "nat  process  process  'val pstate  'val"
where
  "Ate_sendMsg r p q st  x st"

definition
  Ate_nextState :: "nat  process  ('val::linorder) pstate  (process  'val option)
                         'val pstate  bool"
where
  "Ate_nextState r p st msgs st' 
     (if card {q. msgs q  None} > T
      then x st' = Min (mostOftenRcvd msgs)
      else x st' = x st)
    (   (v. card {q. msgs q = Some v} > E   decide st' = Some v)
        ¬ (v. card {q. msgs q = Some v} > E) 
          decide st' = decide st)"


subsection ‹Communication predicate for $A_{T,E}$›

definition Ate_commPerRd where
  "Ate_commPerRd HOrs SHOrs 
   p. card (HOrs p - SHOrs p)  α"

text ‹
  The global communication predicate stipulates the three following
  conditions:
  \begin{itemize}
  \item for every process p› there are infinitely many rounds 
    where p› receives more than T› messages,
  \item for every process p› there are infinitely many rounds 
    where p› receives more than E› uncorrupted messages,
  \item and there are infinitely many rounds in which more than
    E - α› processes receive uncorrupted messages from the
    same set of processes, which contains more than T› processes.
  \end{itemize}
›
definition
  Ate_commGlobal where
  "Ate_commGlobal HOs SHOs 
     (r p. r' > r. card (HOs r' p) > T)
    (r p.  r' > r. card (SHOs r' p  HOs r' p) > E)
    (r. r' > r. π1 π2.
        card π1 > E - α
       card π2 > T
       (p  π1. HOs r' p = π2  SHOs r' p  HOs r' p = π2))"

subsection ‹The $A_{T,E}$ Heard-Of machine›

text ‹
  We now define the non-coordinated SHO machine for the Ate algorithm
  by assembling the algorithm definition and its communication-predicate.
›

definition Ate_SHOMachine where
  "Ate_SHOMachine =  
    CinitState =  (λ p st crd. Ate_initState p (st::('val::linorder) pstate)),
    sendMsg =  Ate_sendMsg,
    CnextState = (λ r p st msgs crd st'. Ate_nextState r p st msgs st'),
    SHOcommPerRd = (Ate_commPerRd:: process HO  process HO  bool),
    SHOcommGlobal = Ate_commGlobal
   "

abbreviation
  "Ate_M  (Ate_SHOMachine::(process, 'val::linorder pstate, 'val) SHOMachine)"

end   ― ‹locale @{text "ate_parameters"}

end   (* theory AteDefs *)

Theory Ate_Proofs

(*<*)
theory Ate_Proofs
imports "../Voting_Opt" Ate_Defs Heard_Of.Majorities 
  "../HO_Transition_System"
begin
(*>*)

subsection ‹Proofs›
axiomatization where val_linorder: 
  "OFCLASS(val, linorder_class)"

instance val :: linorder by (rule val_linorder)

context ate_parameters
begin

definition majs :: "(process set) set" where
  "majs  {S. card S > E}"

interpretation majorities: quorum_process majs
proof
  fix Q Q' assume "Q  majs" "Q'  majs"
  hence "N < card Q + card Q'" using majE
    by(auto simp add: majs_def)
  thus "Q  Q'  {}"
    apply (intro majorities_intersect)
    apply(auto)
    done
next
  from EltN
  show "Q. Q  majs" 
    apply(rule_tac x=UNIV in exI)
    apply(auto simp add: majs_def intro!: div_less_dividend)
    done
qed

type_synonym p_TS_state = "(nat × (process  (val pstate)))"

definition K where
  "K y  λx. y"

definition Ate_Alg where
  "Ate_Alg =
     CinitState =  (λ p st crd. Ate_initState p st),
     sendMsg =  Ate_sendMsg,
     CnextState = (λ r p st msgs crd st'. Ate_nextState r p st msgs st')
   "

definition Ate_TS ::
  "(round  process HO)
   (round  process HO)
   (round  process)
   p_TS_state TS"
where
  "Ate_TS HOs SHOs crds = CHO_to_TS Ate_Alg HOs SHOs (K o crds)"

lemmas Ate_TS_defs = Ate_TS_def CHO_to_TS_def Ate_Alg_def CHOinitConfig_def
  Ate_initState_def

definition
  "Ate_trans_step HOs  r μ.
   {((r, cfg), Suc r, cfg')|cfg cfg'.
    (p. μ p  get_msgs (Ate_sendMsg r) cfg (HOs r) (HOs r) p) 
    (p. Ate_nextState r p (cfg p) (μ p) (cfg' p))}"

definition CSHOnextConfig where
  "CSHOnextConfig A r cfg HO SHO coord cfg' 
   p. μ  SHOmsgVectors A r p cfg (HO p) (SHO p).
          CnextState A r p (cfg p) μ (coord p) (cfg' p)"

type_synonym rHO = "nat  process HO"

subsubsection ‹Refinement›
(******************************************************************************)

definition ate_ref_rel :: "(opt_v_state × p_TS_state)set" where
  "ate_ref_rel =  {(sa, (r, sc)).
    r = next_round sa
     (p. decisions sa p = Ate_Defs.decide (sc p))
     majorities.opt_no_defection sa (Some o x o sc)
  }"

lemma decide_origin:
  assumes 
    send: "μ p  get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) p"
    and nxt: "Ate_nextState r p (sc p) (μ p) (sc' p)"
    and new_dec: "decide (sc' p)  decide (sc p)"
  shows
    "v. decide (sc' p) = Some v  {q. x (sc q) = v}  majs" using assms
  by(auto simp add: get_msgs_benign Ate_sendMsg_def Ate_nextState_def
    majs_def restrict_map_def elim!: order.strict_trans2 intro!: card_mono)

lemma other_values_received:
  assumes nxt: "Ate_nextState  r q (sc q) μq ((sc') q)"
  and muq: "μq  get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) q"
  and vsent: "card {qq. sendMsg Ate_M r qq q (sc qq) = v} > E - α"
             (is "card ?vsent > _")
  shows "card ({qq. μq qq  Some v}  HOs r q)  N + 2*α - E"
proof -
  from nxt muq
  have "({qq. μq qq  Some v}  HOs r q) - (HOs r q - HOs r q)
          {qq. sendMsg Ate_M r qq q (sc qq)  v}"
    (is "?notvrcvd - ?aho  ?notvsent") 
    unfolding get_msgs_def SHOmsgVectors_def Ate_SHOMachine_def by auto
  hence "card ?notvsent  card (?notvrcvd - ?aho)"
    and "card (?notvrcvd - ?aho)  card ?notvrcvd - card ?aho"
    by (auto simp: card_mono diff_card_le_card_Diff)
  moreover
  have 1: "card ?notvsent + card ?vsent = card (?notvsent  ?vsent)"
    by (subst card_Un_Int) auto
  have "?notvsent  ?vsent = (UNIV::process set)" by auto
  hence "card (?notvsent  ?vsent) = N" by simp
  with 1 vsent have "card ?notvsent   N - (E + 1 - α)" by auto
  ultimately
  show ?thesis using EltN Egta by auto
qed

text ‹
  If more than E - α› processes send a value v› to some
  process q› at some round r›, and if q› receives more than
  T› messages in r›, then v› is the most frequently
  received value by q› in r›.
›

lemma mostOftenRcvd_v:
  assumes nxt: "Ate_nextState  r q (sc q) μq ((sc') q)"
  and muq: "μq  get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) q"
  and threshold_T: "card {qq. μq qq  None} > T"
  and threshold_E: "card {qq. sendMsg Ate_M r qq q (sc qq) = v} > E - α"
  shows "mostOftenRcvd μq = {v}"
proof -
  from muq have hodef:"HOs r q = {qq. μq qq  None}"
    unfolding get_msgs_def SHOmsgVectors_def by auto

  from nxt muq threshold_E
  have "card ({qq. μq qq  Some v}  HOs r q)  N + 2*α - E"
    (is "card ?heardnotv  _")
    by (rule other_values_received)
  moreover
  have "card ?heardnotv  T + 1 - card {qq. μq qq = Some v}"
  proof -
    from muq
    have "?heardnotv = (HOs r q) - {qq. μq qq = Some v}"
      and "{qq. μq qq = Some v}  HOs r q"
      unfolding SHOmsgVectors_def get_msgs_def by auto
    hence "card ?heardnotv = card (HOs r q) - card {qq. μq qq = Some v}"
      by (auto simp: card_Diff_subset)
    with hodef threshold_T show ?thesis by auto
  qed
  ultimately
  have "card {qq. μq qq = Some v} > card ?heardnotv"
    using TNaE by auto
  moreover
  {
    fix w
    assume w: "w  v"
    with hodef have "{qq. μq qq = Some w}  ?heardnotv" by auto
    hence "card {qq. μq qq = Some w}  card ?heardnotv" by (auto simp: card_mono)
  }
  ultimately
  have "{w. card {qq. μq qq = Some w}  card {qq. μq qq = Some v}} = {v}"
    by force
  thus ?thesis unfolding mostOftenRcvd_def by auto
qed

lemma step_ref:
  "{ate_ref_rel} 
      (r v_f d_f. majorities.flv_round r v_f d_f), 
      Ate_trans_step HOs 
    {> ate_ref_rel}"
proof(simp add: PO_rhoare_defs Ate_trans_step_def, safe)
  fix sa r sc sc' μ
  assume
    R: "(sa, r, sc)  ate_ref_rel"
    and send: "p. μ p  get_msgs (Ate_sendMsg r) sc (HOs r) (HOs r) p"
    and nxt: "p. Ate_nextState r p (sc p) (μ p) (sc' p)"
  note step=send nxt
  define d_f
    where "d_f p = (if decide (sc' p)  decide (sc p) then decide (sc' p) else None)" for p

  define sa' where "sa' =  
    opt_v_state.next_round = Suc r
    , opt_v_state.last_vote = opt_v_state.last_vote sa ++ (Some o x o sc) 
    , opt_v_state.decisions = opt_v_state.decisions sa ++ d_f
    "
  
  have "majorities.d_guard d_f (Some o x o sc)"
  proof(clarsimp simp add: majorities.d_guard_def d_f_def)
    fix p v
    assume
      "Some v  decide (sc p)" 
      "decide (sc' p) = Some v"
    from this and 
      decide_origin[where μ=μ and HOs=HOs and sc'=sc', OF send[THEN spec, of p] nxt[THEN spec, of p]]
    show "quorum_process.locked_in_vf majs (Some  x  sc) v"
      by(auto simp add: majorities.locked_in_vf_def majorities.quorum_for_def)
  qed
  hence
    "(sa, sa')  majorities.flv_round r (Some o x o sc) d_f" using R
    by(auto simp add: majorities.flv_round_def ate_ref_rel_def sa'_def)
  moreover have "(sa', Suc r, sc')  ate_ref_rel"
  proof(unfold ate_ref_rel_def, safe)
    fix p
    show "opt_v_state.decisions sa' p = decide (sc' p)" using R nxt[THEN spec, of p]
      by(auto simp add: ate_ref_rel_def sa'_def map_add_def d_f_def Ate_nextState_def
        split: option.split)
  next
    show "quorum_process.opt_no_defection majs sa' (Some  x  sc')"
    proof(clarsimp simp add: sa'_def majorities.opt_no_defection_def map_add_def majorities.quorum_for_def)
      fix Q p v
      assume Q: "Q  majs" and Q_v: "q  Q. x (sc q) = v" and p_Q: "p  Q"
      hence old: "x (sc p) = v" by simp

      have v_maj: "{q. x (sc q) = v}  majs" using Q Q_v
        apply(simp add: majs_def)
        apply(erule less_le_trans, rule card_mono, auto)
        done
      show "x (sc' p) = v"
      proof(cases "T < card {qq. μ p qq  None}")
        case True
        have
          "E - α < card {qq. sendMsg Ate_M r qq p (sc qq) = v}" using v_maj
          by(auto simp add: Ate_SHOMachine_def Ate_sendMsg_def majs_def)
        from mostOftenRcvd_v[where HOs=HOs and sc=sc and sc'=sc', 
          OF nxt[THEN spec, of p] send[THEN spec, of p] True this]
        show ?thesis using nxt[THEN spec, of p] old
          by(clarsimp simp add: Ate_nextState_def)
      next
        case False
        thus ?thesis using nxt[THEN spec, of p] old
          by(clarsimp simp add: Ate_nextState_def)
      qed
    qed
  qed(auto simp add: sa'_def)

  ultimately show 
    "sa'. (ra v_f d_f. (sa, sa')  quorum_process.flv_round majs ra v_f d_f) 
     (sa', Suc r, sc')  ate_ref_rel"
    by blast
qed

lemma Ate_Refines_LV_VOting:
  "PO_refines (ate_ref_rel) 
    majorities.flv_TS (Ate_TS HOs HOs crds)"
proof(rule refine_basic)
  show "init (Ate_TS HOs HOs crds)  ate_ref_rel `` init (quorum_process.flv_TS majs)"
    by(auto simp add: Ate_TS_def CHO_to_TS_def Ate_Alg_def CHOinitConfig_def Ate_initState_def
      majorities.flv_TS_def flv_init_def majorities.opt_no_defection_def majorities.quorum_for_def'
      ate_ref_rel_def)
next
  show 
    "{ate_ref_rel} TS.trans (quorum_process.flv_TS majs), TS.trans (Ate_TS HOs HOs crds) {> ate_ref_rel}"
    using step_ref
    by(simp add: majorities.flv_TS_defs Ate_TS_def CHO_to_TS_def Ate_Alg_def 
      CSHO_trans_alt_def CHO_trans_alt Ate_trans_step_def)
qed

end   ― ‹context @{text "ate_parameters"}

subsubsection ‹Termination›
(******************************************************************************)

text ‹The termination proof for the algorithm is already given in the Heard-Of Model AFP
  entry, and we do not repeat it here.›

end   (* theory AteProof *)

Theory Same_Vote

section ‹The Same Vote Model›
                                                                                            
theory Same_Vote
imports Voting
begin

context quorum_process begin

subsection ‹Model definition›
(******************************************************************************)

text ‹The system state remains the same as in the Voting model, but the
  voting event is changed.›

definition safe :: "v_state  round  val  bool" where
  safe_def': "safe s r v  
    r' < r. Q  Quorum. w. (votes s r') ` Q = {Some w}  v = w"

text ‹This definition of @{term safe} is easier to reason about in Isabelle.›
lemma safe_def:
  "safe s r v =
    (r' < r. Q w. quorum_for Q w (votes s r')   v = w)"
  by(auto simp add: safe_def' quorum_for_def' Ball_def)

definition sv_round :: "round  process set  val  (process, val)map  (v_state × v_state) set" where
  "sv_round r S v r_decisions = {(s, s').
     ― ‹guards›
     r = next_round s
      (S  {}  safe s r v)
      d_guard r_decisions (const_map v S)
      ― ‹actions›
     s' = s 
       next_round := Suc r
       , votes := (votes s)(r := const_map v S)
       , decisions := (decisions s ++ r_decisions)
     
  }"

definition sv_trans :: "(v_state × v_state) set" where
  "sv_trans = (r S v D. sv_round r S v D)  Id"

definition sv_TS :: "v_state TS" where
  "sv_TS =  init = v_init, trans = sv_trans "

lemmas sv_TS_defs = sv_TS_def v_init_def sv_trans_def

subsection ‹Refinement›
(******************************************************************************)

lemma safe_imp_no_defection:
  "safe s (next_round s) v  no_defection s (const_map v S) (next_round s)" 
  by(auto simp add: safe_def no_defection_def restrict_map_def const_map_def)
 
lemma const_map_quorum_locked:
  "S  Quorum  locked_in_vf (const_map v S) v"
  by(auto simp add: locked_in_vf_def const_map_def quorum_for_def)

lemma sv_round_refines:
  "{Id} v_round r (const_map v S) r_decisions, sv_round r S v r_decisions {> Id}"
  by(auto simp add: PO_rhoare_defs sv_round_def v_round_def  no_defection_empty
    dest!: safe_imp_no_defection const_map_quorum_locked)

lemma Same_Vote_Refines:
  "PO_refines Id v_TS sv_TS"
  by(auto simp add: PO_refines_def sv_TS_def sv_trans_def v_TS_defs intro!: 
    sv_round_refines relhoare_refl)


subsection ‹Invariants›
(******************************************************************************)

definition SV_inv3 where
  "SV_inv3 = {s. r a b v w. 
    votes s r a = Some v  votes s r b = Some w  v = w
  }"

lemmas SV_inv3I = SV_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas SV_inv3E [elim] = SV_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas SV_inv3D = SV_inv3_def [THEN setc_def_to_dest, rule_format]
 
subsubsection ‹Proof of invariants›
(******************************************************************************)

lemma SV_inv3_v_round: 
  "{SV_inv3} sv_round r S v D {> SV_inv3}" 
  apply(clarsimp simp add: PO_hoare_defs intro!: SV_inv3I)
  apply(force simp add: sv_round_def const_map_def restrict_map_def SV_inv3_def)
  done

lemmas SV_inv3_event_pres = SV_inv3_v_round 

lemma SV_inv3_inductive:
  "init sv_TS  SV_inv3" 
  "{SV_inv3} trans sv_TS {> SV_inv3}" 
  apply (simp add: sv_TS_defs SV_inv3_def)
  by (auto simp add: sv_TS_defs SV_inv3_event_pres)

lemma SV_inv3_invariant: "reach sv_TS  SV_inv3"
  by (auto intro!: inv_rule_basic SV_inv3_inductive del: subsetI)

text ‹

This is a different characterization of @{term safe}, due to Lampson~\cite{lampson_abcds_2001}:
  @{term "safe' s r v = (r'< r. (Q  Quorum. a  Q. w. votes s r' a = Some w  w = v))"}

It is, however, strictly stronger than our characterization, since we do not at this point assume
the "completeness" of our quorum system (for any set S, either S or the complement of S is a
quorum), and the following is thus not provable: @{term "s  SV_inv3  safe' s = safe s"}.

›

subsubsection ‹Transfer of abstract invariants›
(******************************************************************************)

lemma SV_inv1_inductive:
  "init sv_TS  Vinv1"
  "{Vinv1} trans sv_TS {> Vinv1}" 
  apply(rule abs_INV_init_transfer[OF Same_Vote_Refines Vinv1_inductive(1), simplified])
  apply(rule abs_INV_trans_transfer[OF Same_Vote_Refines Vinv1_inductive(2), simplified])
  done

lemma SV_inv1_invariant:
  "reach sv_TS  Vinv1"
  by(rule abs_INV_transfer[OF Same_Vote_Refines Vinv1_invariant, simplified])

lemma SV_inv2_inductive:
  "init sv_TS  Vinv2"
  "{Vinv2  Vinv1} trans sv_TS {> Vinv2}" 
  apply(rule abs_INV_init_transfer[OF Same_Vote_Refines Vinv2_inductive(1), simplified])
  apply(rule abs_INV_trans_transfer[OF Same_Vote_Refines Vinv2_inductive(2), simplified])
  done

lemma SV_inv2_invariant:
  "reach sv_TS  Vinv2"
  by(rule abs_INV_transfer[OF Same_Vote_Refines Vinv2_invariant, simplified])

subsubsection ‹Additional invariants›
(******************************************************************************)

text ‹With Same Voting, the voted values are safe in the next round.›

definition SV_inv4 :: "v_state set" where
  "SV_inv4 = {s. v a r. votes s r a = Some v  safe s (Suc r) v }"

lemmas SV_inv4I = SV_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas SV_inv4E [elim] = SV_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas SV_inv4D = SV_inv4_def [THEN setc_def_to_dest, rule_format]

lemma SV_inv4_sv_round: 
  "{SV_inv4  (Vinv1  Vinv2)} sv_round r S v D {> SV_inv4}" 
proof(clarsimp simp add: PO_hoare_defs intro!: SV_inv4I)
  fix s v' a r' s'
  assume 
    step: "(s, s')  sv_round r S v D"
    and invs: "s  SV_inv4" "s  Vinv1" "s  Vinv2"
    and vote: "votes s' r' a = Some v'"
  thus "safe s' (Suc r') v'"
  proof(cases "r=r'")
    case True
    moreover hence safe: "safe s' r' v'" using step vote
      by(force simp add: sv_round_def const_map_is_Some safe_def quorum_for_def)
    ultimately show ?thesis using step vote
      by(force simp add: safe_def less_Suc_eq sv_round_def quorum_for_def const_map_is_Some 
        dest: quorum_non_empty)
  qed(clarsimp simp add: sv_round_def safe_def Vinv2_def Vinv1_def  SV_inv4_def
      intro: Quorum_not_empty)
qed

lemmas SV_inv4_event_pres = SV_inv4_sv_round 

lemma SV_inv4_inductive:
  "init sv_TS  SV_inv4" 
  "{SV_inv4  (Vinv1  Vinv2)} trans sv_TS {> SV_inv4}"
  apply(simp add: sv_TS_defs SV_inv4_def)
  by (auto simp add: sv_TS_defs SV_inv4_event_pres)

lemma SV_inv4_invariant: "reach sv_TS  SV_inv4"
  by (rule inv_rule_incr)
  (auto intro: SV_inv4_inductive SV_inv2_invariant SV_inv1_invariant del: subsetI)

end (* context quorum_process *)

end

Theory Observing_Quorums

section ‹The Observing Quorums Model›

theory Observing_Quorums
imports Same_Vote
begin

subsection ‹Model definition›
(******************************************************************************)

text ‹The state adds one field to the Voting model state:›
record obsv_state = v_state +
  obs :: "round  (process, val) map"

text ‹For the observation mechanism to work, we need monotonicity of quorums.›
context mono_quorum begin

definition obs_safe 
  where
  "obs_safe r s v  (r' < r. p. obs s r' p  {None, Some v})"

definition obsv_round 
  :: "round  process set  val  (process, val)map  process set  (obsv_state × obsv_state) set" 
  where
  "obsv_round r S v r_decisions Os = {(s, s').
     ― ‹guards›
     r = next_round s
      (S  {}  obs_safe r s v)
      d_guard r_decisions (const_map v S)
      (S  Quorum  Os = UNIV)
      (Os  {}  S  {})
      ― ‹actions›
     s' = s 
       next_round := Suc r
       , votes := (votes s)(r := const_map v S)
       , decisions := decisions s ++ r_decisions
       , obs := (obs s)(r := const_map v Os)
     
  }"

definition obsv_trans :: "(obsv_state × obsv_state) set" where
  "obsv_trans = (r S v d_f Os. obsv_round r S v d_f Os)  Id"

definition obsv_init :: "obsv_state set" where
  "obsv_init = {  next_round = 0, votes = λr a. None, decisions = Map.empty, obs = λr a. None  }"  

definition obsv_TS :: "obsv_state TS" where
  "obsv_TS =  init = obsv_init, trans = obsv_trans "

lemmas obsv_TS_defs = obsv_TS_def obsv_init_def obsv_trans_def


subsection ‹Invariants›
(******************************************************************************)

definition OV_inv1 where
  "OV_inv1 = {s. r Q v. quorum_for Q v (votes s r) 
    (Q'  Quorum. quorum_for Q' v (obs s r))}"

lemmas OV_inv1I = OV_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas OV_inv1E [elim] = OV_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas OV_inv1D = OV_inv1_def [THEN setc_def_to_dest, rule_format]
 
subsubsection ‹Proofs of invariants›
(******************************************************************************)
  
lemma OV_inv1_obsv_round: 
  "{OV_inv1} obsv_round r S v d_f Ob {> OV_inv1}"
proof(clarsimp simp add: PO_hoare_defs intro!: OV_inv1I)
  fix v' s s' Q Q' r'
  assume 
    Q: "quorum_for Q v' (votes s' r')"  
    and inv: "s  OV_inv1"
    and step: "(s, s')  obsv_round r S v d_f Ob"
    and quorum: "Q'  Quorum"
  from Q inv[THEN OV_inv1D] step quorum
  show "quorum_for Q' v' (obs s' r')"
  proof(cases "r'=r")
    case True
    with step and Q have "S  Quorum"
      by(fastforce simp add: obsv_round_def obs_safe_def quorum_for_def const_map_is_Some
        ball_conj_distrib subset_eq[symmetric] intro: mono_quorum[where Q'=S])      
    thus ?thesis using step inv[THEN OV_inv1D] Q quorum
      by(clarsimp simp add: obsv_round_def obs_safe_def quorum_for_def const_map_is_Some
        ball_conj_distrib subset_eq[symmetric] dest!: quorum_non_empty)
  qed(clarsimp simp add: obsv_round_def obs_safe_def quorum_for_def)
qed

lemma OV_inv1_inductive:
  "init obsv_TS  OV_inv1" 
  "{OV_inv1} trans obsv_TS {> OV_inv1}" 
  apply (simp add: obsv_TS_defs OV_inv1_def) 
   apply (auto simp add: obsv_TS_defs OV_inv1_obsv_round quorum_for_def dest: empty_not_quorum)
  done

lemma quorum_for_const_map:
  "(quorum_for Q w (const_map v S)) = (Q  Quorum  Q  S  w = v)"
  by(auto simp add: quorum_for_def const_map_is_Some dest: quorum_non_empty)

subsection ‹Refinement›
(******************************************************************************)

definition obsv_ref_rel where 
  "obsv_ref_rel  {(sa, sc).
    sa = v_state.truncate sc
  }"

lemma obsv_round_refines:
  "{obsv_ref_rel  UNIV × OV_inv1} sv_round r S v dec_f, obsv_round r S v dec_f Ob {> obsv_ref_rel}"
  apply(clarsimp simp add: PO_rhoare_defs sv_round_def obsv_round_def safe_def obsv_ref_rel_def 
    v_state.truncate_def obs_safe_def quorum_for_def OV_inv1_def)
  by (metis UNIV_I UNIV_quorum  option.distinct(1) option.inject)

lemma Observable_Refines:
  "PO_refines (obsv_ref_rel  UNIV × OV_inv1) sv_TS obsv_TS"
proof(rule refine_using_invariants)
  show "init obsv_TS  obsv_ref_rel `` init sv_TS"
  by(auto simp add: PO_refines_def sv_TS_defs  obsv_TS_defs  obsv_ref_rel_def 
    v_state.truncate_def)
next
  show "{obsv_ref_rel  UNIV × OV_inv1} trans sv_TS, trans obsv_TS {> obsv_ref_rel}"
    by(auto simp add: PO_refines_def sv_TS_defs  obsv_TS_defs intro!: 
      obsv_round_refines relhoare_refl)
qed(auto intro: OV_inv1_inductive del: subsetI)

subsection ‹Additional invariants›
(******************************************************************************)

definition OV_inv2 where
  "OV_inv2 = {s. r  next_round s. obs s r = Map.empty }"

lemmas OV_inv2I = OV_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas OV_inv2E [elim] = OV_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas OV_inv2D = OV_inv2_def [THEN setc_def_to_dest, rule_format]

definition OV_inv3 where
  "OV_inv3 = {s. r p v. obs s r p = Some v 
    obs_safe r s v}"

lemmas OV_inv3I = OV_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas OV_inv3E [elim] = OV_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas OV_inv3D = OV_inv3_def [THEN setc_def_to_dest, rule_format]

definition OV_inv4 where
  "OV_inv4 = {s. r p q v w. obs s r p = Some v  obs s r q = Some w 
    w = v}"

lemmas OV_inv4I = OV_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas OV_inv4E [elim] = OV_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas OV_inv4D = OV_inv4_def [THEN setc_def_to_dest, rule_format]


subsubsection ‹Proofs of additional invariants›
(******************************************************************************)

lemma OV_inv2_inductive:
  "init obsv_TS  OV_inv2"
  "{OV_inv2} trans obsv_TS {> OV_inv2}" 
  by(auto simp add: PO_hoare_defs OV_inv2_def obsv_TS_defs obsv_round_def const_map_is_Some)

lemma SVinv3_inductive:
  "init obsv_TS  SV_inv3"
  "{SV_inv3} trans obsv_TS {> SV_inv3}" 
  by(auto simp add: PO_hoare_defs SV_inv3_def obsv_TS_defs obsv_round_def const_map_is_Some)

lemma OV_inv3_obsv_round: 
  "{OV_inv3  OV_inv2} obsv_round r S v D Ob {> OV_inv3}"
proof(clarsimp simp add: PO_hoare_defs intro!: OV_inv3I)
  fix s s' r_w p w
  assume Assms:
    "obs s' r_w p = Some w" 
    "s  OV_inv3"
    "(s, s')  obsv_round r S v D Ob"
    "s  OV_inv2"
  hence "s'  OV_inv2"
    by(force simp add: obsv_TS_defs intro: OV_inv2_inductive(2)[THEN hoareD, OF s  OV_inv2›])
  hence "r_w  next_round s'" using Assms
    by(auto simp add: OV_inv2_def intro!: leI)
  hence r_w_le: "r_w  next_round s" using Assms
    by(auto simp add: obsv_round_def le_Suc_eq)
  show "obs_safe r_w s' w"
  proof(cases "r_w = next_round s")
    case True
    thus ?thesis using Assms
      by(auto simp add: obsv_round_def const_map_is_Some obs_safe_def)
  next
    case False
    hence "r_w < next_round s" using r_w_le
      by(metis less_le)
    moreover have "r'. r'  next_round s  obs s' r' = obs s r'" using Assms(3)
      by(auto simp add: obsv_round_def)
    ultimately have 
      "r'  r_w. obs s' r' = obs s r'"
      by(auto)
    thus ?thesis using Assms
      by(auto simp add: OV_inv3_def obs_safe_def)
  qed
qed

lemma OV_inv3_inductive:
  "init obsv_TS  OV_inv3"
  "{OV_inv3  OV_inv2} trans obsv_TS {> OV_inv3}" 
  apply(auto simp add: obsv_TS_def obsv_trans_def intro: OV_inv3_obsv_round)
  apply(auto simp add: obsv_init_def OV_inv3_def)
  done

lemma OV_inv4_inductive:
  "init obsv_TS  OV_inv4"
  "{OV_inv4} trans obsv_TS {> OV_inv4}" 
  by(auto simp add: PO_hoare_defs OV_inv4_def obsv_TS_defs obsv_round_def const_map_is_Some)

end

end

Theory Observing_Quorums_Opt

section ‹The Optimized Observing Quorums Model›

theory Observing_Quorums_Opt
imports Observing_Quorums
begin

subsection ‹Model definition›
(******************************************************************************)

record opt_obsv_state = 
  next_round :: round 
  decisions :: "(process, val)map"
  last_obs :: "(process, val)map"

context mono_quorum
begin

definition opt_obs_safe where
  "opt_obs_safe obs_f v  p. obs_f p  {None, Some v}"

definition olv_round where
  "olv_round r S v r_decisions Ob  {(s, s').
    ― ‹guards›
    r = next_round s
     (S  {}  opt_obs_safe (last_obs s) v)
     (S  Quorum  Ob = UNIV)
     d_guard r_decisions (const_map v S)
     (Ob  {}  S  {})
     ― ‹actions›
    s' = s 
     next_round := Suc r
     , decisions := decisions s ++ r_decisions
     , last_obs := last_obs s ++ const_map v Ob
   
  }"

definition olv_init where
  "olv_init = {  next_round = 0, decisions = Map.empty, last_obs = Map.empty  }"

definition olv_trans :: "(opt_obsv_state × opt_obsv_state) set" where
  "olv_trans = (r S v D Ob. olv_round r S v D Ob)  Id"

definition olv_TS :: "opt_obsv_state TS" where
  "olv_TS =  init = olv_init, trans = olv_trans "

lemmas olv_TS_defs = olv_TS_def olv_init_def olv_trans_def

subsection ‹Refinement›
(******************************************************************************)

definition olv_ref_rel where
  "olv_ref_rel  {(sa, sc).
    next_round sc = v_state.next_round sa
     decisions sc = v_state.decisions sa
     last_obs sc = map_option snd o process_mru (obsv_state.obs sa)
  }"


lemma OV_inv2_finite_map_graph:
   "s  OV_inv2  finite (map_graph (case_prod (obsv_state.obs s)))"
  apply(rule finite_dom_finite_map_graph)
  apply(rule finite_subset[where B="{0..< v_state.next_round s} × UNIV"])
   apply(auto simp add: OV_inv2_def dom_def not_le[symmetric])
  done

lemma OV_inv2_finite_obs_set:
   "s  OV_inv2  finite (vote_set (obsv_state.obs s) Q)"
   apply(drule OV_inv2_finite_map_graph)
   apply(clarsimp simp add: map_graph_def fun_graph_def vote_set_def)
   apply(erule finite_surj[where f="λ((r, a), v). (r, v)"])
   by(force simp add: image_def)   

lemma olv_round_refines:
  "{olv_ref_rel  (OV_inv2  OV_inv3  OV_inv4) × UNIV} obsv_round r S v D Ob, olv_round r S v D Ob {>olv_ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs)
  fix sa :: obsv_state and sc sc'
  assume
    ainv: "sa  OV_inv2" "sa  OV_inv3" "sa  OV_inv4"
    and step: "(sc, sc')  olv_round r S v D Ob"
    and R: "(sa, sc)  olv_ref_rel"

  ― ‹Abstract guard.›
  have "S  {}  obs_safe (v_state.next_round sa) sa v"
  proof(rule impI, rule ccontr)
    assume S_nonempty: "S  {}" and no_Q: "¬ obs_safe (v_state.next_round sa) sa v"
    from no_Q obtain r_w w where 
      r_w: "r_w < v_state.next_round sa"
      and all_obs: "p. obsv_state.obs sa r_w p = Some w"
      and diff: "w  v" using ainv(3)[THEN OV_inv4D]
      by(simp add: obs_safe_def)  (metis)
    from diff step R obtain p where 
      p_w: "S  {}  (map_option snd  process_mru (obsv_state.obs sa)) p  Some w"
      by (simp add: opt_obs_safe_def quorum_for_def olv_round_def  olv_ref_rel_def)  
       (metis option.distinct(1) option.sel snd_conv)
    from all_obs have nempty: "vote_set (obsv_state.obs sa) {p}  {}" 
      by(auto simp add:  vote_set_def)
    then obtain r_w' w' where w': "process_mru (obsv_state.obs sa) p = Some (r_w', w')"
      by (simp add: process_mru_def mru_of_set_def) 
        (metis option_Max_by_def surj_pair)
    hence max: "(r_w', w') = Max_by fst (vote_set (obsv_state.obs sa) {p})"
      by(auto simp add: process_mru_def mru_of_set_def option_Max_by_def)
    hence w'_obs: "(r_w', w')  vote_set (obsv_state.obs sa) {p}" 
      using Max_by_in[OF OV_inv2_finite_obs_set[OF ainv(1), of "{p}"] nempty]
      by fastforce
    have "r_w  r_w'" using all_obs
      apply -
      apply(rule Max_by_ge[OF OV_inv2_finite_obs_set[OF ainv(1), of "{p}"], of "(r_w, w)" fst, 
                            simplified max[symmetric], simplified])
      apply(auto simp add: quorum_for_def vote_set_def)
      done
    moreover have "w'  w" using p_w w' S_nonempty
      by(auto)
    ultimately have "r_w < r_w'" using all_obs w'_obs
      apply(elim le_neq_implies_less)
      apply(auto simp add: quorum_for_def vote_set_def)
      done
    thus False using ainv(2)[THEN OV_inv3D] w'_obs all_obs w'  w
      by(fastforce simp add: vote_set_def obs_safe_def)
  qed

  ― ‹Action refinement.›
  moreover have 
    "(map_option snd  process_mru (obsv_state.obs sa)) ++ const_map v Ob =
      map_option snd  process_mru ((obsv_state.obs sa)(v_state.next_round sa := const_map v Ob))"
  proof-
    from sa  OV_inv2›[THEN OV_inv2D] 
    have empty: "r'v_state.next_round sa. obsv_state.obs sa r' = Map.empty"
      by simp
    show ?thesis
      by(auto simp add: map_add_def const_map_def restrict_map_def process_mru_new_votes[OF empty])
  qed

  ultimately show "sa'. (sa, sa')  obsv_round r S v D Ob  (sa', sc')  olv_ref_rel" 
    using R step
    by(clarsimp simp add: obsv_round_def olv_round_def olv_ref_rel_def)

qed

lemma OLV_Refines:
  "PO_refines (olv_ref_rel  (OV_inv2  OV_inv3  OV_inv4) × UNIV) obsv_TS olv_TS"
proof(rule refine_using_invariants)
  show "init olv_TS  olv_ref_rel `` init obsv_TS"
    by(auto simp add: obsv_TS_defs olv_TS_defs olv_ref_rel_def process_mru_def mru_of_set_def
      vote_set_def option_Max_by_def intro!: ext)
next
  show
    "{olv_ref_rel  (OV_inv2  OV_inv3  OV_inv4) × UNIV} TS.trans obsv_TS, TS.trans olv_TS {> olv_ref_rel}"
    by(auto simp add: PO_refines_def obsv_TS_defs olv_TS_defs 
      intro!: olv_round_refines)
qed (auto intro: OV_inv2_inductive OV_inv3_inductive OV_inv4_inductive
  OV_inv2_inductive(1)[THEN subsetD] OV_inv3_inductive(1)[THEN subsetD] 
  OV_inv4_inductive(1)[THEN subsetD])

end

end

Theory Two_Step_Observing

section ‹Two-Step Observing Quorums Model›

theory Two_Step_Observing
imports "../Observing_Quorums_Opt" "../Two_Steps"
begin

text ‹To make the coming proofs of concrete algorithms easier, in this model we split 
  the @{term olv_round} into two steps.›

subsection ‹Model definition›
(******************************************************************************)
record tso_state = opt_obsv_state +
  r_votes :: "process  val option"

context mono_quorum
begin

definition tso_round0 
  :: "round  process set  val  (tso_state × tso_state)set"
  where
  "tso_round0 r S v  {(s, s').
    ― ‹guards›
    r = next_round s
     two_step r = 0
     (S  {}  opt_obs_safe (last_obs s) v)
    ― ‹actions›
     s' = s
      next_round := Suc r
      , r_votes := const_map v S
    
  }"

definition obs_guard :: "(process, val)map  (process, val)map  bool" where
  "obs_guard r_obs r_v  p.
    (v. r_obs p = Some v  (q. r_v q = Some v))
     (dom r_v  Quorum  (q  dom r_v. r_obs p = r_v q))"

definition tso_round1 
  :: "round  (process, val)map  (process, val)map  (tso_state × tso_state)set" 
  where
  "tso_round1 r r_decisions r_obs  {(s, s').
    ― ‹guards›
    r = next_round s
     two_step r = 1
     d_guard r_decisions (r_votes s)
     obs_guard r_obs (r_votes s)
    ― ‹actions›
     s' = s
      next_round := Suc r
      , decisions := decisions s ++ r_decisions
      , last_obs := last_obs s ++ r_obs
    
  }"

definition tso_init where
  "tso_init = {  next_round = 0, decisions = Map.empty, last_obs = Map.empty, r_votes = Map.empty  }"

definition tso_trans :: "(tso_state × tso_state) set" where
  "tso_trans = (r S v. tso_round0 r S v)  (r d_f o_f. tso_round1 r d_f o_f)  Id"

definition tso_TS :: "tso_state TS" where
  "tso_TS =  init = tso_init, trans = tso_trans "

lemmas tso_TS_defs = tso_TS_def tso_init_def tso_trans_def

subsection ‹Refinement›
(******************************************************************************)

definition basic_rel :: "(opt_obsv_state × tso_state)set" where
  "basic_rel = {(sa, sc).
    next_round sa = two_phase (next_round sc)
     last_obs sc = last_obs sa
     decisions sc = decisions sa
  }"

definition step0_rel :: "(opt_obsv_state × tso_state)set" where
  "step0_rel = basic_rel"

definition step1_add_rel :: "(opt_obsv_state × tso_state)set" where
  "step1_add_rel = {(sa, sc). S v.
    r_votes sc = const_map v S
     (S  {}  opt_obs_safe (last_obs sc) v)
  }"

definition step1_rel :: "(opt_obsv_state × tso_state)set" where
  "step1_rel = basic_rel  step1_add_rel"

definition tso_ref_rel :: "(opt_obsv_state × tso_state)set" where
  "tso_ref_rel  {(sa, sc).
    (two_step (next_round sc) = 0  (sa, sc)  step0_rel)
     (two_step (next_round sc) = 1  
        (sa, sc)  step1_rel
         (sc' r S v. (sc', sc)  tso_round0 r S v  (sa, sc')  step0_rel))
  }"

lemma const_map_equality:
  "(const_map v S = const_map v' S') = (S = S'  (S = {}  v = v'))"
  apply(simp add: const_map_def restrict_map_def)
  by (metis equals0D option.distinct(2) option.inject subsetI subset_antisym)

lemma rhoare_skipI:
  " sa sc sc'.  (sa, sc)  Pre; (sc, sc')  Tc   (sa, sc')  Post   {Pre} Id, Tc {>Post}"
  by(auto simp add: PO_rhoare_defs)

lemma tso_round0_refines:
  "{tso_ref_rel} Id, tso_round0 r S v {>tso_ref_rel}"
  apply(rule rhoare_skipI)
  apply(auto simp add: tso_ref_rel_def basic_rel_def step1_rel_def 
     step1_add_rel_def  step0_rel_def tso_round0_def const_map_equality conj_disj_distribR
     ex_disj_distrib two_step_phase_Suc)
  done

lemma tso_round1_refines:
  "{tso_ref_rel} r S v dec_f Ob. olv_round r S v dec_f Ob, tso_round1 r dec_f o_f {>tso_ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs)
  fix sa sc and sc'
  assume
    R: "(sa, sc)  tso_ref_rel" 
    and step1: "(sc, sc')  tso_round1 r dec_f o_f"

  hence step_r: "two_step r = 1" and r_next: "next_round sc = r" by (auto simp add: tso_round1_def)
  then obtain r0 sc0 S0 v0 where 
    R0: "(sa, sc0)  step0_rel" and step0: "(sc0, sc)  tso_round0 r0 S0 v0"
    using R
    by(auto simp add: tso_ref_rel_def) 

  from step_r r_next R obtain S v where
    v: "r_votes sc = const_map v S"
    and safe: "S  {}  opt_obs_safe (last_obs sc) v"
    by(auto simp add: tso_ref_rel_def step1_rel_def step1_add_rel_def)

  define sa' where "sa' = sa 
      next_round := Suc (next_round sa)
      , decisions := decisions sa ++ dec_f
      , last_obs := last_obs sa ++ const_map v (dom o_f)
    "

  have "S  Quorum  dom o_f = UNIV" using step1 v
    by(auto simp add: tso_round1_def obs_guard_def const_map_def)
  moreover have "o_f  Map.empty  S  {}" using step1 v
    by(auto simp add: tso_round1_def obs_guard_def dom_const_map)
  ultimately have 
    abs_step: 
    "(sa, sa')  olv_round (next_round sa) S v dec_f (dom o_f)" using R safe v step_r r_next step1
    by(clarsimp simp add: tso_ref_rel_def step1_rel_def basic_rel_def sa'_def 
      olv_round_def tso_round1_def)

  from v have post_rel: "(sa', sc')  tso_ref_rel" using R step1
    apply(clarsimp simp add: tso_round0_def tso_round1_def 
      step0_rel_def basic_rel_def  sa'_def tso_ref_rel_def two_step_phase_Suc o_def
      const_map_is_Some const_map_is_None const_map_equality obs_guard_def 
      intro!: arg_cong2[where f=map_add, OF refl])
    apply(auto simp add: const_map_def restrict_map_def intro!: ext)
    done

  from abs_step post_rel show 
    "sa'. (r' S' w dec_f' Ob'. (sa, sa')  olv_round r' S' w dec_f' Ob')  (sa', sc')  tso_ref_rel"
    by blast
qed
  
lemma TS_Observing_Refines:
  "PO_refines tso_ref_rel olv_TS tso_TS"
  apply(auto simp add: PO_refines_def olv_TS_defs tso_TS_defs 
    intro!: tso_round0_refines tso_round1_refines)
  apply(auto simp add: tso_ref_rel_def step0_rel_def basic_rel_def tso_init_def quorum_for_def 
    dest: empty_not_quorum)
  done

subsection ‹Invariants›
(******************************************************************************)

definition TSO_inv1 where
  "TSO_inv1 = {s. two_step (next_round s) = Suc 0 
    (v. p w. r_votes s p = Some w  w = v)}"

lemmas TSO_inv1I = TSO_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas TSO_inv1E [elim] = TSO_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas TSO_inv1D = TSO_inv1_def [THEN setc_def_to_dest, rule_format]

definition TSO_inv2 where
  "TSO_inv2 = {s. two_step (next_round s) = Suc 0 
    (p v. (r_votes s p = Some v  (q. last_obs s q  {None, Some v})))}"

lemmas TSO_inv2I = TSO_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas TSO_inv2E [elim] = TSO_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas TSO_inv2D = TSO_inv2_def [THEN setc_def_to_dest, rule_format]

subsubsection ‹Proofs of invariants›
(******************************************************************************)

lemma TSO_inv1_inductive:
  "init tso_TS  TSO_inv1"
  "{TSO_inv1} TS.trans tso_TS {> TSO_inv1}"
  by(auto simp add: TSO_inv1_def tso_TS_defs PO_hoare_def 
    tso_round0_def tso_round1_def const_map_is_Some two_step_phase_Suc)
  
lemma TSO_inv1_invariant:
  "reach tso_TS  TSO_inv1"
  by(intro inv_rule_basic TSO_inv1_inductive)

lemma TSO_inv2_inductive:
  "init tso_TS  TSO_inv2"
  "{TSO_inv2} TS.trans tso_TS {> TSO_inv2}"
  by(auto simp add: TSO_inv2_def tso_TS_defs PO_hoare_def 
    opt_obs_safe_def tso_round0_def tso_round1_def const_map_is_Some two_step_phase_Suc)
  
lemma TSO_inv2_invariant:
  "reach tso_TS  TSO_inv2"
  by(intro inv_rule_basic TSO_inv2_inductive)

end

end

Theory Uv_Defs

section ‹The UniformVoting Algorithm›
theory Uv_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Quorums"
begin

text ‹The contents of this file have been taken almost verbatim from the
  Heard Of Model AFP entry. The only difference is that the types have been
  changed.›

subsection ‹Model of the algorithm›

abbreviation "nSteps  2"

definition phase where "phase (r::nat)  r div nSteps"

definition step where "step (r::nat)  r mod nSteps"

text ‹
  The following record models the local state of a process.
›

record 'val pstate =
  last_obs :: 'val                ― ‹current value held by process›
  agreed_vote :: "'val option"    ― ‹value the process voted for, if any›
  decide :: "'val option"  ― ‹value the process has decided on, if any›

text ‹
  Possible messages sent during the execution of the algorithm, and characteristic
  predicates to distinguish types of messages.
›

datatype 'val msg =
  Val 'val
| ValVote 'val "'val option"
| Null  ― ‹dummy message in case nothing needs to be sent›

definition isValVote where "isValVote m  z v. m = ValVote z v"

definition isVal where "isVal m  v. m = Val v"

text ‹
  Selector functions to retrieve components of messages. These functions
  have a meaningful result only when the message is of appropriate kind.
›

fun getvote where
  "getvote (ValVote z v) = v"

fun getval where
  "getval (ValVote z v) = z"
| "getval (Val z) = z"


definition UV_initState where
  "UV_initState p st  (agreed_vote st = None)  (decide st = None)"

text ‹
  We separately define the transition predicates and the send functions
  for each step and later combine them to define the overall next-state relation.
›

definition msgRcvd where  ― ‹processes from which some message was received›
  "msgRcvd (msgs:: process  'val msg) = {q . msgs q  None}"

definition smallestValRcvd where
  "smallestValRcvd (msgs::process  ('val::linorder) msg) 
   Min {v. q. msgs q = Some (Val v)}"

text ‹
  In step 0, each process sends its current last_obs› value.

  It updates its last_obs› field to the smallest value it has received.
  If the process has received the same value v› from all processes
  from which it has heard, it updates its agreed_vote› field to v›.
›

definition send0 where
  "send0 r p q st  Val (last_obs st)"

definition next0 where
  "next0 r p st (msgs::process  ('val::linorder) msg) st' 
       (v. (q  msgRcvd msgs. msgs q = Some (Val v))
            st' = st  agreed_vote := Some v, last_obs := smallestValRcvd msgs )
     ¬(v. q  msgRcvd msgs. msgs q = Some (Val v))
        st' = st  last_obs := smallestValRcvd msgs "

text ‹
  In step 1, each process sends its current last_obs› and agreed_vote› values.
›

definition send1 where
  "send1 r p q st  ValVote (last_obs st) (agreed_vote st)"

definition valVoteRcvd where
  ― ‹processes from which values and votes were received›
  "valVoteRcvd (msgs :: process  'val msg)  
   {q . z v. msgs q = Some (ValVote z v)}"

definition smallestValNoVoteRcvd where
  "smallestValNoVoteRcvd (msgs::process  ('val::linorder) msg) 
   Min {v. q. msgs q = Some (ValVote v None)}"

definition someVoteRcvd where
  ― ‹set of processes from which some vote was received›
  "someVoteRcvd (msgs :: process  'val msg) 
   { q . q  msgRcvd msgs  isValVote (the (msgs q))  getvote (the (msgs q))  None }"

definition identicalVoteRcvd where
  "identicalVoteRcvd (msgs :: process  'val msg) v 
   q  msgRcvd msgs. isValVote (the (msgs q))  getvote (the (msgs q)) = Some v"

definition x_update where
 "x_update st msgs st' 
   (q  someVoteRcvd msgs . last_obs st' = the (getvote (the (msgs q))))
  someVoteRcvd msgs = {}  last_obs st' = smallestValNoVoteRcvd msgs"

definition dec_update where
  "dec_update st msgs st' 
    (v. identicalVoteRcvd msgs v  decide st' = Some v)
   ¬(v. identicalVoteRcvd msgs v)  decide st' = decide st"

definition next1 where
  "next1 r p st msgs st' 
     x_update st msgs st'
    dec_update st msgs st'
    agreed_vote st' = None"

text ‹
  The overall send function and next-state relation are simply obtained as 
  the composition of the individual relations defined above.
›

definition UV_sendMsg where
  "UV_sendMsg (r::nat)  if step r = 0 then send0 r else send1 r"

definition UV_nextState where
  "UV_nextState r  if step r = 0 then next0 r else next1 r"


definition (in quorum_process) UV_commPerRd where
  "UV_commPerRd HOrs  p. HOrs p  Quorum"

definition UV_commGlobal where
  "UV_commGlobal HOs  r. p q. HOs r p = HOs r q"


subsection ‹The \emph{UniformVoting} Heard-Of machine›

text ‹
  We now define the HO machine for \emph{Uniform Voting} by assembling the
  algorithm definition and its communication predicate. Notice that the
  coordinator arguments for the initialization and transition functions are
  unused since \emph{UniformVoting} is not a coordinated algorithm.
›

definition (in quorum_process) UV_HOMachine where
  "UV_HOMachine =  
    CinitState =  (λp st crd. UV_initState p st),
    sendMsg =  UV_sendMsg,
    CnextState = (λr p st msgs crd st'. UV_nextState r p st msgs st'),
    HOcommPerRd = UV_commPerRd,
    HOcommGlobal = UV_commGlobal
  "

abbreviation (in quorum_process)
  "UV_M  (UV_HOMachine::(process, 'val::linorder pstate, 'val msg) HOMachine)"

end

Theory Uv_Proofs

(*<*)
theory Uv_Proofs
imports Heard_Of.Reduction
  Two_Step_Observing "../HO_Transition_System" Uv_Defs
begin
(*>*)

subsection ‹Proofs›
type_synonym uv_TS_state = "(nat × (process  (val pstate)))"

axiomatization where val_linorder: 
  "OFCLASS(val, linorder_class)"

instance val :: linorder by (rule val_linorder)

lemma two_step_step:
   "step = two_step"
   "phase = two_phase"
   by(auto simp add: step_def two_step_def phase_def two_phase_def)

context mono_quorum
begin

definition UV_Alg :: "(process, val pstate, val msg)CHOAlgorithm" where
  "UV_Alg = CHOAlgorithm.truncate UV_M"

definition UV_TS ::
  "(round  process HO)  (round  process HO)  (round  process)  uv_TS_state TS"
where
  "UV_TS HOs SHOs crds = CHO_to_TS UV_Alg HOs SHOs (K o crds)"

lemmas UV_TS_defs = UV_TS_def CHO_to_TS_def UV_Alg_def CHOinitConfig_def
  UV_initState_def

type_synonym rHO = "nat  process HO"

definition UV_trans_step 
  where
  "UV_trans_step HOs SHOs nxt_f snd_f stp  r μ.
    {((r, cfg), (Suc r, cfg'))|cfg cfg'. step r = stp   (p.
      μ p  get_msgs (snd_f r) cfg (HOs r) (SHOs r) p
       nxt_f r p (cfg p) (μ p) (cfg' p)
    )}"

lemma step_less_D:
  "0 < step r  step r = Suc 0"
  by(auto simp add: step_def)

lemma UV_trans:
  "CSHO_trans_alt UV_sendMsg (λr p st msgs crd st'. UV_nextState r p st msgs st') HOs SHOs crds = 
  UV_trans_step HOs SHOs next0 send0 0
   UV_trans_step HOs SHOs  next1 send1 1
  "
proof
  show "CSHO_trans_alt UV_sendMsg (λr p st msgs crd. UV_nextState r p st msgs) HOs SHOs crds
     UV_trans_step HOs SHOs next0 send0 0  UV_trans_step HOs SHOs next1 send1 1"
  by(force simp add: CSHO_trans_alt_def UV_sendMsg_def UV_nextState_def UV_trans_step_def 
    K_def dest!: step_less_D)
next
  show " UV_trans_step HOs SHOs next0 send0 0 
    UV_trans_step HOs SHOs next1 send1 1
     CSHO_trans_alt UV_sendMsg
        (λr p st msgs crd. UV_nextState r p st msgs) HOs SHOs crds"
  by(force simp add: CSHO_trans_alt_def UV_sendMsg_def UV_nextState_def UV_trans_step_def)
qed

subsubsection ‹Invariants›
(******************************************************************************)

definition UV_inv1
  :: "uv_TS_state set" 
where  
  "UV_inv1  = {(r, s). 
    two_step r = 0  (p. agreed_vote (s p) = None)
  }"

lemmas UV_inv1I = UV_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas UV_inv1E [elim] = UV_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas UV_inv1D = UV_inv1_def [THEN setc_def_to_dest, rule_format]

lemma UV_inv1_inductive:
  "init (UV_TS HOs SHOs crds)  UV_inv1"
  "{UV_inv1} TS.trans (UV_TS HOs SHOs crds) {> UV_inv1}"
  by(auto simp add: UV_inv1_def UV_TS_defs CHO_trans_alt UV_trans PO_hoare_def 
    UV_HOMachine_def CHOAlgorithm.truncate_def UV_trans_step_def 
    all_conj_distrib two_step_phase_Suc two_step_step next1_def)
  
lemma UV_inv1_invariant:
  "reach (UV_TS HOs SHOs crds)  UV_inv1"
  by(intro inv_rule_basic UV_inv1_inductive)

subsubsection ‹Refinement›
(******************************************************************************)

definition ref_rel :: "(tso_state × uv_TS_state)set" where
  "ref_rel  {(sa, (r, sc)).
    r = next_round sa
     (step r = 1  r_votes sa = agreed_vote o sc)
     (p v. last_obs (sc p) = v  (q. opt_obsv_state.last_obs sa q  {None, Some v}))
     decisions sa = decide o sc
  }"

(******************************************************************************)
text ‹Agreement for UV only holds if the communication predicates hold›
context
  fixes
    HOs :: "nat  process  process set"
    and rho :: "nat  process  'val pstate"
  assumes global: "UV_commGlobal HOs"
  and per_rd: "r. UV_commPerRd (HOs r)"
  and run: "HORun fA rho HOs"
begin
(******************************************************************************)

lemma HOs_intersect:
  "HOs r p  HOs r' q  {}" using per_rd
  apply(simp add: UV_commPerRd_def)
  apply(blast dest: qintersect)
  done

lemma HOs_nonempty:
  "HOs r p  {}" 
  using HOs_intersect
  by blast

lemma vote_origin:
  assumes
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and inv: "(r, cfg)  UV_inv1"
  and step_r: "two_step r = 0"
  shows 
    "agreed_vote (cfg' p) = Some v  (q  HOs r p. last_obs (cfg q) = v)" 
  using send[THEN spec, where x=p] step[THEN spec, where x=p] inv step_r HOs_nonempty
  by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)
  
lemma same_new_vote:
  assumes 
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and inv: "(r, cfg)  UV_inv1"
  and step_r: "two_step r = 0"
  obtains v where "p w. agreed_vote (cfg' p) = Some w  w = v" 
proof(cases "p v. agreed_vote (cfg' p) = Some v")
  case True
  assume asm: "v. p w. agreed_vote (cfg' p) = Some w  w = v  thesis"
  from True obtain p v where "agreed_vote (cfg' p) = Some v" by auto

  hence "p w. agreed_vote (cfg' p) = Some w  w = v" (is "?LV(v)")
    using vote_origin[OF send step inv step_r] HOs_intersect
    by(force)

  from asm[OF this] show ?thesis .
qed(auto)

lemma x_origin1:
  assumes
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  and last_obs: "last_obs (cfg' p) = v"
  shows 
    "q. last_obs (cfg q) = v" 
proof-
  have "smallestValRcvd (μ p)  {v. q. μ p q = Some (Val v)}" (is "smallestValRcvd ?msgs  ?vals")
  unfolding smallestValRcvd_def
  proof(rule Min_in)
    have "?vals  getval ` ((the  ?msgs) ` (HOs r p))"
      using send[THEN spec, where x=p]
      by (auto simp: image_def get_msgs_benign restrict_map_def send0_def)
    thus "finite ?vals" by (auto simp: finite_subset)
  next
    from send[THEN spec, where x=p]
    show "?vals  {}" using HOs_nonempty[of r p]
      by (auto simp: image_def get_msgs_benign restrict_map_def send0_def)
  qed
  hence "v  ?vals" using last_obs step[THEN spec, of p] 
    by(auto simp add: next0_def all_conj_distrib)
  thus ?thesis using send[THEN spec, of p]
    by(auto simp add: get_msgs_benign send0_def restrict_map_def)
qed
    
lemma step0_ref:
  "{ref_rel  UNIV × UV_inv1} r S v. tso_round0 r S v, 
    UV_trans_step HOs HOs next0 send0 0 {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs UV_trans_step_def two_step_step all_conj_distrib)
  fix sa r cfg μ cfg'
  assume
    R: "(sa, (r, cfg))  ref_rel"
    and step_r: "two_step r = 0" 
    and send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
    and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
    and inv: "(r, cfg)  UV_inv1"

  from R have next_r: "next_round sa = r"
    by(simp add: ref_rel_def)

  from HOs_nonempty send have "p. q. q  msgRcvd (μ p)"
    by(fastforce simp add: get_msgs_benign send0_def msgRcvd_def restrict_map_def)
  with step have same_dec: "decide o cfg' = decide o cfg"
    apply(simp add: next0_def o_def)
    by (metis pstate.select_convs(3) pstate.surjective pstate.update_convs(1) pstate.update_convs(2))

  define S where "S = {p. v. agreed_vote (cfg' p) = Some v}"
  from same_new_vote[OF send step inv step_r] 
  obtain v where v: "p  S. agreed_vote (cfg' p) = Some v"
    by(simp add: S_def) (metis)
  hence vote_const_map: "agreed_vote o cfg' = const_map v S"
    by(auto simp add: S_def const_map_def restrict_map_def intro!: ext)

  note x_origin = x_origin1[OF send step step_r]

  define sa' where "sa' = sa next_round := Suc r, r_votes := const_map v S "

  have "p. p  S  opt_obs_safe (opt_obsv_state.last_obs sa) v"
    using vote_origin[OF send step inv step_r] R per_rd[THEN spec, of r] v
    apply(clarsimp simp add: UV_commPerRd_def opt_obs_safe_def ref_rel_def)
    by metis
    
  hence "(sa, sa')  tso_round0 r S v" using next_r step_r v R 
    vote_origin[OF send step inv step_r]
    by(auto simp add: tso_round0_def sa'_def all_conj_distrib)

  moreover have "(sa', Suc r, cfg')  ref_rel" using step send v R same_dec step_r next_r
    apply(clarsimp simp add: ref_rel_def sa'_def two_step_step two_step_phase_Suc vote_const_map)
    by (metis x_origin)
  ultimately show
    "sa'. (r S v. (sa, sa')  tso_round0 r S v)  (sa', Suc r, cfg')  ref_rel"
    by blast
qed


lemma x_origin2:
  assumes
  send: "p. μ p  get_msgs (send1 r) cfg (HOs r) (HOs r) p"
  and step: "p. next1 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = Suc 0"
  and last_obs: "last_obs (cfg' p) = v"
  shows 
    "(q. last_obs (cfg q) = v)  (q. agreed_vote (cfg q) = Some v)" 
proof(cases "q  HOs r p. w. μ p q = Some (ValVote w None)")
  case True
  hence empty: "someVoteRcvd (μ p) = {}" using send[THEN spec, of p] HOs_nonempty[of r p]
    by(auto simp add: someVoteRcvd_def msgRcvd_def isValVote_def 
      get_msgs_benign send1_def restrict_map_def)
  have "smallestValNoVoteRcvd (μ p)  {v. q. μ p q = Some (ValVote v None)}" 
    (is "smallestValNoVoteRcvd ?msgs  ?vals")
  unfolding smallestValNoVoteRcvd_def
  proof(rule Min_in)
    have "?vals  getval ` ((the  ?msgs) ` (HOs r p))"
      using send[THEN spec, where x=p]
      by (auto simp: image_def get_msgs_benign restrict_map_def send0_def)
    thus "finite ?vals" by (auto simp: finite_subset)
  next
    from send[THEN spec, where x=p] True HOs_nonempty[of r p]
    show "?vals  {}" 
      by (auto simp: image_def get_msgs_benign restrict_map_def send1_def)
  qed
  hence "v  ?vals" using empty step[THEN spec, of p] last_obs
    by(auto simp add: next1_def x_update_def)
  thus ?thesis using send[THEN spec, of p]
    by(auto simp add: get_msgs_benign restrict_map_def send1_def)
next
  case False
  hence "someVoteRcvd (μ p)  {}" using send[THEN spec, of p] HOs_nonempty[of r p]
    by(auto simp add: someVoteRcvd_def msgRcvd_def isValVote_def 
      get_msgs_benign send1_def restrict_map_def)
  hence "q  someVoteRcvd (μ p). v = the (getvote (the (μ p q)))" using step[THEN spec, of p] last_obs
    by(auto simp add: next1_def x_update_def)
  thus ?thesis using send[THEN spec, of p]
    by(auto simp add: next1_def x_update_def someVoteRcvd_def isValVote_def 
      send1_def get_msgs_benign msgRcvd_def restrict_map_def)
qed

definition D where
  "D cfg cfg'  {p. decide (cfg' p)  decide (cfg p) }"

lemma decide_origin:
  assumes
  send: "p. μ p  get_msgs (send1 r) cfg (HOs r) (HOs r) p"
  and step: "p. next1 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = Suc 0"
  shows 
    "D cfg cfg'  {p. v. decide (cfg' p) = Some v  (q  HOs r p. agreed_vote (cfg q) = Some v)}" 
  using assms
  by(fastforce simp add: D_def next1_def get_msgs_benign send1_def msgRcvd_def o_def restrict_map_def
    x_update_def dec_update_def identicalVoteRcvd_def all_conj_distrib someVoteRcvd_def isValVote_def
    smallestValNoVoteRcvd_def)
  
lemma step1_ref:
  "{ref_rel  (TSO_inv1  TSO_inv2) × UNIV} r d_f o_f. tso_round1 r d_f o_f, 
    UV_trans_step HOs HOs next1 send1 (Suc 0) {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs UV_trans_step_def two_step_step all_conj_distrib)
  fix sa r cfg μ and cfg' :: "process  val pstate"
  assume
    R: "(sa, (r, cfg))  ref_rel"
    and step_r: "two_step r = Suc 0" 
    and send: "p. μ p  get_msgs (send1 r) cfg (HOs r) (HOs r) p"
    and step: "p. next1 r p (cfg p) (μ p) (cfg' p)"
    and ainv: "sa  TSO_inv1"
    and ainv2: "sa  TSO_inv2"

  from R have next_r: "next_round sa = r"
    by(simp add: ref_rel_def)

  define S where "S = {p. v. agreed_vote (cfg p) = Some v}"
  from R obtain v where v: "p  S. agreed_vote (cfg p) = Some v" using ainv step_r
    by(auto simp add: ref_rel_def TSO_inv1_def S_def two_step_step)

  define Ob where "Ob = {p. last_obs (cfg' p) = v}"
  define o_f where "o_f p = (if S  Quorum then Some v else None)" for p :: process

  define dec_f where "dec_f p = (if p  D cfg cfg' then decide (cfg' p) else None)" for p

  {
    fix p w
    assume "agreed_vote (cfg p) = Some w"
    hence "w = v" using v
      by(unfold S_def, auto)
  } note v'=this
    
  have d_guard: "d_guard dec_f (agreed_vote  cfg)" using per_rd[THEN spec, of r]
    by(fastforce simp add: d_guard_def locked_in_vf_def quorum_for_def dec_f_def
      UV_commPerRd_def dest!: decide_origin[OF send step step_r, THEN subsetD])

  have "dom (agreed_vote  cfg)  Quorum  Ob = UNIV"
  proof(auto simp add: Ob_def)
    fix p
    assume Q: "dom (agreed_vote  cfg)  Quorum" (is "?Q  Quorum")
    hence "?Q  HOs r p  {}"  using per_rd[THEN spec, of r]
      by(auto simp add: UV_commPerRd_def dest: qintersect)
    hence "someVoteRcvd (μ p)  {}" using send[THEN spec, of p]
      by(force simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def 
        isValVote_def send1_def)
    moreover have "q  someVoteRcvd (μ p). x'. μ p q = Some (ValVote x' (Some v))"
      using send[THEN spec, of p]
      by(auto simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def
        isValVote_def send1_def dest: v')
    ultimately show "last_obs (cfg' p) = v" using step[THEN spec, of p]
      by(auto simp add: next1_def x_update_def)
  qed
  note Ob_UNIV=this[rule_format]

  have obs_guard: "obs_guard o_f (agreed_vote  cfg)"
    apply(auto simp add: obs_guard_def o_f_def S_def dom_def
      dest: v' Ob_UNIV quorum_non_empty) 
    apply (metis S_def all_not_in_conv  empty_not_quorum v)
    done

  define sa' where "sa' = sa 
    next_round := Suc (next_round sa)
    , decisions := decisions sa ++ dec_f
    , opt_obsv_state.last_obs := opt_obsv_state.last_obs sa ++ o_f
    "


  ― ‹Abstract step›
  have abs_step: "(sa, sa')  tso_round1 r dec_f o_f"  using next_r step_r R d_guard obs_guard
    by(auto simp add: tso_round1_def sa'_def ref_rel_def two_step_step)

  ― ‹Relation preserved›
  have "p. ((decide  cfg) ++ dec_f) p = decide (cfg' p)"
  proof
    fix p
    show "((decide  cfg) ++ dec_f) p = decide (cfg' p)" using step[THEN spec, of p]
      by(auto simp add: dec_f_def D_def next1_def dec_update_def map_add_def)
  qed
  note dec_rel=this[rule_format]

  have "p. (q. o_f q = None  opt_obsv_state.last_obs sa q = None 
         (opt_obsv_state.last_obs sa ++ o_f) q = Some (last_obs (cfg' p)))"
  proof(intro allI impI, cases "S  Quorum")
    fix p 
    case True 
    hence "last_obs (cfg' p) = v" using Ob_UNIV
      by(auto simp add: S_def Ob_def dom_def)
    thus "(q. o_f q = None  opt_obsv_state.last_obs sa q = None 
         (opt_obsv_state.last_obs sa ++ o_f) q = Some (last_obs (cfg' p)))"
      using True
      by(auto simp add: o_f_def)
  next
    fix p
    case False
    hence empty: "o_f = Map.empty"
      by(auto simp add: o_f_def)
    note last_obs = x_origin2[OF send step step_r refl, of p]
    thus "(q. o_f q = None  opt_obsv_state.last_obs sa q = None 
         (opt_obsv_state.last_obs sa ++ o_f) q = Some (last_obs (cfg' p)))"
    proof(elim disjE exE)
      fix q
      assume "last_obs (cfg q) = last_obs (cfg' p)"
      from this[symmetric] show ?thesis using R step_r empty
        by(simp add: ref_rel_def two_step_step)
    next
      fix q
      assume "agreed_vote (cfg q) = Some (last_obs (cfg' p))" 
      from this[symmetric] show ?thesis using R ainv2 step_r empty
        apply(auto simp add: ref_rel_def two_step_step TSO_inv2_def)
        by metis
    qed
  qed
  note obs_rel=this[rule_format]

  have post_rel: 
    "(sa', Suc r, cfg')  ref_rel" using step send next_r R step_r
    by(auto simp add: sa'_def ref_rel_def two_step_step
      two_step_phase_Suc dec_rel obs_rel)
    
  from abs_step post_rel show
    "sa'. (r d_f o_f. (sa, sa')  tso_round1 r d_f o_f)  (sa', Suc r, cfg')  ref_rel"
    by blast
qed

lemma UV_Refines_votes:
  "PO_refines (ref_rel  (TSO_inv1  TSO_inv2) × UV_inv1)
    tso_TS (UV_TS HOs HOs crds)"
proof(rule refine_using_invariants)
  show "init (UV_TS HOs HOs crds)  ref_rel `` init tso_TS"
    by(auto simp add: UV_TS_defs UV_HOMachine_def CHOAlgorithm.truncate_def 
      tso_TS_defs ref_rel_def tso_init_def Let_def o_def)
next
  show 
    "{ref_rel  (TSO_inv1  TSO_inv2) × UV_inv1} TS.trans tso_TS, 
      TS.trans (UV_TS HOs HOs crds) {> ref_rel}"
    apply(simp add: tso_TS_defs UV_TS_defs UV_HOMachine_def CHOAlgorithm.truncate_def)
    apply(auto simp add: CHO_trans_alt UV_trans intro!: step0_ref step1_ref)
    done
qed(auto intro!: TSO_inv1_inductive TSO_inv2_inductive UV_inv1_inductive)

end (* HO predicate context *)

end (* mono_quorum context *)

subsubsection ‹Termination›
(******************************************************************************)

text ‹As the model of the algorithm is taken verbatim from the HO Model AFP, we
  do not repeat the termination proof here and refer to that AFP entry.›

end (* theory *)

Theory BenOr_Defs

section ‹The Ben-Or Algorithm›

theory BenOr_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Quorums" "../Two_Steps"
begin

consts coin :: "round  process  val"

record 'val pstate =
  x :: 'val                ― ‹current value held by process›
  vote :: "'val option"    ― ‹value the process voted for, if any›
  decide :: "'val option"  ― ‹value the process has decided on, if any›

datatype 'val msg =
  Val 'val
| Vote "'val option"
| Null  ― ‹dummy message in case nothing needs to be sent›

definition isVote where "isVote m  v. m = Vote v"

definition isVal where "isVal m  v. m = Val v"

fun getvote where
  "getvote (Vote v) = v"

fun getval where
  "getval (Val z) = z"

definition BenOr_initState where
  "BenOr_initState p st  (vote st = None)  (decide st = None)"

definition msgRcvd where  ― ‹processes from which some message was received›
  "msgRcvd (msgs:: process  'val msg) = {q . msgs q  None}"

definition send0 where
  "send0 r p q st  Val (x st)"

definition next0 where
  "next0 r p st (msgs::process  'val msg) st' 
       (v. (q  msgRcvd msgs. msgs q = Some (Val v))
            st' = st  vote := Some v )
     ¬(v. q  msgRcvd msgs. msgs q = Some (Val v))
        st' = st  vote := None "

definition send1 where
  "send1 r p q st  Vote (vote st)"

definition someVoteRcvd where
  ― ‹set of processes from which some vote was received›
  "someVoteRcvd (msgs :: process  'val msg) 
   { q . q  msgRcvd msgs  isVote (the (msgs q))  getvote (the (msgs q))  None }"

definition identicalVoteRcvd where
  "identicalVoteRcvd (msgs :: process  'val msg) v 
   q  msgRcvd msgs. isVote (the (msgs q))  getvote (the (msgs q)) = Some v"

definition x_update where
 "x_update r p msgs st' 
   (q  someVoteRcvd msgs . x st' = the (getvote (the (msgs q))))
  someVoteRcvd msgs = {}  x st' = coin r p"

definition dec_update where
  "dec_update st msgs st' 
    (v. identicalVoteRcvd msgs v  decide st' = Some v)
   ¬(v. identicalVoteRcvd msgs v)  decide st' = decide st"

definition next1 where
  "next1 r p st msgs st' 
     x_update r p msgs st'
    dec_update st msgs st'
    vote st' = None"

definition BenOr_sendMsg where
  "BenOr_sendMsg (r::nat)  if two_step r = 0 then send0 r else send1 r"

definition BenOr_nextState where
  "BenOr_nextState r  if two_step r = 0 then next0 r else next1 r"

subsection ‹The \emph{Ben-Or} Heard-Of machine›
(******************************************************************************)

definition (in quorum_process) BenOr_commPerRd where
  "BenOr_commPerRd HOrs  p. HOrs p  Quorum"

definition BenOr_commGlobal where
  "BenOr_commGlobal HOs  r. two_step r = 1
     (p q. HOs r p = HOs r q  (coin r p :: val) = coin r q)"



definition (in quorum_process) BenOr_HOMachine where
  "BenOr_HOMachine =  
    CinitState =  (λp st crd. BenOr_initState p st),
    sendMsg =  BenOr_sendMsg,
    CnextState = (λr p st msgs crd st'. BenOr_nextState r p st msgs st'),
    HOcommPerRd = BenOr_commPerRd,
    HOcommGlobal = BenOr_commGlobal
  "

abbreviation (in quorum_process)
  "BenOr_M  (BenOr_HOMachine::(process, val pstate, val msg) HOMachine)"

end

Theory BenOr_Proofs

(*<*)
theory BenOr_Proofs
imports Heard_Of.Reduction
  Two_Step_Observing "../HO_Transition_System" BenOr_Defs
begin
(*>*)

subsection ‹Proofs›

type_synonym ben_or_TS_state = "(nat × (process  (val pstate)))"

consts 
  val0 :: val 
  val1 :: val

text ‹Ben-Or works only on binary values.›
axiomatization where 
  val_exhaust: "v = val0  v = val1"
  and val_diff: "val0  val1"

context mono_quorum
begin

definition BenOr_Alg :: "(process, val pstate, val msg)CHOAlgorithm" where
  "BenOr_Alg = CHOAlgorithm.truncate BenOr_M"

definition BenOr_TS ::
  "(round  process HO)  (round  process HO)  (round  process)  ben_or_TS_state TS"
where
  "BenOr_TS HOs SHOs crds = CHO_to_TS BenOr_Alg HOs SHOs (K o crds)"

lemmas BenOr_TS_defs = BenOr_TS_def CHO_to_TS_def BenOr_Alg_def CHOinitConfig_def
  BenOr_initState_def

type_synonym rHO = "nat  process HO"

definition BenOr_trans_step 
  where
  "BenOr_trans_step HOs SHOs nxt_f snd_f stp  r μ.
    {((r, cfg), (Suc r, cfg'))|cfg cfg'. two_step r = stp   (p.
      μ p  get_msgs (snd_f r) cfg (HOs r) (SHOs r) p
       nxt_f r p (cfg p) (μ p) (cfg' p)
    )}"

lemma two_step_less_D:
  "0 < two_step r  two_step r = Suc 0"
  by(auto simp add: two_step_def)

lemma BenOr_trans:
  "CSHO_trans_alt BenOr_sendMsg (λr p st msgs crd st'. BenOr_nextState r p st msgs st') HOs SHOs crds = 
  BenOr_trans_step HOs SHOs next0 send0 0
   BenOr_trans_step HOs SHOs  next1 send1 1
  "
proof
  show "CSHO_trans_alt BenOr_sendMsg (λr p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
     BenOr_trans_step HOs SHOs next0 send0 0  BenOr_trans_step HOs SHOs next1 send1 1"
  by(force simp add: CSHO_trans_alt_def BenOr_sendMsg_def BenOr_nextState_def BenOr_trans_step_def 
    K_def dest!: two_step_less_D)
next
  show " BenOr_trans_step HOs SHOs next0 send0 0 
    BenOr_trans_step HOs SHOs next1 send1 1
     CSHO_trans_alt BenOr_sendMsg
        (λr p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds"
  by(force simp add: CSHO_trans_alt_def BenOr_sendMsg_def BenOr_nextState_def BenOr_trans_step_def)
qed

definition "BenOr_A = CHOAlgorithm.truncate BenOr_M"

subsubsection ‹Refinement›
(******************************************************************************)

text ‹Agreement for BenOr only holds if the communication predicates hold›
context
  fixes
    HOs :: "nat  process  process set"
    and rho :: "nat  process  val pstate"
  assumes comm_global: "BenOr_commGlobal HOs"
  and per_rd: "r. BenOr_commPerRd (HOs r)"
  and run: "HORun BenOr_A rho HOs"
begin
(******************************************************************************)

definition no_vote_diff where
  "no_vote_diff sc p  vote (sc p) = None 
            (q q'. x (sc q)  x (sc q'))"

definition ref_rel :: "(tso_state × ben_or_TS_state)set" where
  "ref_rel  {(sa, (r, sc)).
    r = next_round sa
     (two_step r = 1  r_votes sa = vote o sc)
     (two_step r = 1  (p. no_vote_diff sc p))
     (p v. x (sc p) = v  (q. last_obs sa q  {None, Some v}))
     decisions sa = decide o sc
  }"

lemma HOs_intersect:
  "HOs r p  HOs r' q  {}" using per_rd
  apply(simp add: BenOr_commPerRd_def)
  apply(blast dest: qintersect)
  done

lemma HOs_nonempty:
  "HOs r p  {}" 
  using HOs_intersect
  by blast

lemma vote_origin:
  assumes
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows 
    "vote (cfg' p) = Some v  (q  HOs r p. x (cfg q) = v)" 
  using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
  by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)
  
lemma same_new_vote:
  assumes 
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  obtains v where "p w. vote (cfg' p) = Some w  w = v" 
proof(cases "p v. vote (cfg' p) = Some v")
  case True
  assume asm: "v. p w. vote (cfg' p) = Some w  w = v  thesis"
  from True obtain p v where "vote (cfg' p) = Some v" by auto

  hence "p w. vote (cfg' p) = Some w  w = v" (is "?LV(v)")
    using vote_origin[OF send step step_r] HOs_intersect
    by(force)

  from asm[OF this] show ?thesis .
qed(auto)

lemma no_x_change:
  assumes
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows 
    "x (cfg' p) = x (cfg p)" 
  using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
  by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)

lemma no_vote:
  assumes 
  send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows
    "no_vote_diff cfg' p" 
    unfolding no_vote_diff_def
proof
  assume
    "vote (cfg' p) = None"
  hence "(q q'. x (cfg q)  x (cfg q'))"
   using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty 
   apply(clarsimp simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)
   by metis
  thus "(q q'. x (cfg' q)  x (cfg' q'))" 
    using no_x_change[OF send step step_r]
    by(simp)
qed
  

lemma step0_ref:
  "{ref_rel} r S v. tso_round0 r S v, 
    BenOr_trans_step HOs HOs next0 send0 0 {> ref_rel}"
proof(clarsimp simp add: PO_rhoare_defs BenOr_trans_step_def all_conj_distrib)
  fix sa r cfg μ cfg'
  assume
    R: "(sa, (r, cfg))  ref_rel"
    and step_r: "two_step r = 0" 
    and send: "p. μ p  get_msgs (send0 r) cfg (HOs r) (HOs r) p"
    and step: "p. next0 r p (cfg p) (μ p) (cfg' p)"

  from R have next_r: "next_round sa = r"
    by(simp add: ref_rel_def)

  from HOs_nonempty send have "p. q. q  msgRcvd (μ p)"
    by(fastforce simp add: get_msgs_benign send0_def msgRcvd_def restrict_map_def)
  with step have same_dec: "decide o cfg' = decide o cfg"
    apply(simp add: next0_def o_def)
    by (metis pstate.select_convs(3) pstate.surjective pstate.update_convs(2))
 
  define S where "S = {p. v. vote (cfg' p) = Some v}"
  from same_new_vote[OF send step step_r] 
  obtain v where v: