Theory Consensus

section ‹The Consensus Data Type›

theory Consensus
imports RDR
begin

text ‹This theory provides a model for the RDR locale, thus showing 
  that the assumption of the RDR locale are consistent.›

typedecl proc
typedecl val

locale Consensus
― ‹To avoid name clashes›
begin

fun δ::"val option ⇒ (proc × val) ⇒ val option" (infix "∙" 65) where
  "δ None r = Some (snd r)"
| "δ (Some v) r = Some v"

fun γ::"val option ⇒ (proc × val) ⇒ val" where
  "γ None r = snd r"
| "γ (Some v) r = v"

interpretation pre_RDR δ γ None .
notation exec (infix "⋆" 65)
notation less_eq (infix "≼" 50 )
notation None ("⊥")

lemma single_use:
  fixes r rs
  shows  "⊥ ⋆ ([r]@rs) = Some (snd r)" 
proof (induct rs)
  case Nil
  thus ?case by simp
next
  case (Cons r rs)
  thus ?case by auto
qed

lemma bot: "∃ rs . s = ⊥ ⋆ rs"
proof (cases s)
  case None
  hence "s = ⊥ ⋆ []" by auto
  thus ?thesis by blast
next
  case (Some v)
  obtain r where "⊥ ⋆ [r] = Some v" by force
  thus ?thesis using Some by metis
qed

lemma prec_eq_None_or_equal:
fixes s1 s2
assumes "s1 ≼ s2"
shows "s1 = None ∨ s1 = s2" using assms single_use  
proof -
  { assume 1:"s1 ≠ None" and 2:"s1 ≠ s2"
    obtain r rs where 3:"s1 = ⊥ ⋆ ([r]@rs)" using bot using 1
      by (metis append_butlast_last_id pre_RDR.exec.simps(1)) 
    obtain rs' where 4:"s2 = s1 ⋆ rs'" using assms 
      by (auto simp add:less_eq_def)
    have "s2 = ⊥ ⋆ ([r]@(rs@rs'))" using 3 4
      by (metis exec_append) 
    hence "s1 = s2" using 3
      by (metis single_use)
    with 2 have False by auto }
  thus ?thesis by blast
qed

interpretation RDR δ γ ⊥
proof (unfold_locales)
  fix s r 
  assume "contains s r"
  show "s ∙ r = s"
  proof -
    obtain rs where "s = ⊥ ⋆ rs" and "rs ≠ []" 
      using ‹contains s r›
      by (auto simp add:contains_def, force)
    thus ?thesis
    by (metis δ.simps(2) rev_exhaust single_use)
  qed
next
  fix s and r r' :: "proc × val"
  assume 1:"fst r ≠ fst r'"
  thus "γ s r = γ ((s ∙ r) ∙ r') r"
    by (metis δ.simps γ.simps not_Some_eq)
next
  fix s1 s2
  assume "s1 ≼ s2 ∧ s2 ≼ s1"
  thus "s1 = s2" by (metis prec_eq_None_or_equal) 
next
  fix s1 s2
  show "∃ s . is_glb s s1 s2" 
  by (simp add:is_glb_def is_lb_def)
    (metis bot pre_RDR.less_eq_def prec_eq_None_or_equal) 
next
  fix s
  show "⊥ ≼ s"
  by (metis bot pre_RDR.less_eq_def)
next
  fix s1 s2 s3 rs
  assume "s1 ≼ s2" and "s2 ≼ s3" and "s3 = s1 ⋆ rs"
  thus "∃ rs' rs'' . s2 = s1 ⋆ rs' ∧ s3 = s2 ⋆ rs'' 
    ∧ set rs' ⊆ set rs ∧ set rs'' ⊆ set rs"
  by (metis Consensus.prec_eq_None_or_equal 
      in_set_insert insert_Nil list.distinct(1)
        pre_RDR.exec.simps(1) subsetI)
qed

end

end