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