Theory Consistency

subsection ‹Consistency of sets of WOOT Messages \label{sec:consistency}›

theory Consistency
  imports SortKeys Psi Sorting DistributedExecution
begin

definition insert_messages :: "('ℐ, 'Σ) message set ⇒ ('ℐ, 'Σ) insert_message set"
  where "insert_messages M = {x. Insert x ∈ M}"

lemma insert_insert_message:
  "insert_messages (M ∪ {Insert m}) = insert_messages M ∪ {m}"
  by (simp add:insert_messages_def, simp add:set_eq_iff)

definition delete_messages :: "('ℐ, 'Σ) message set ⇒ 'ℐ delete_message set"
  where "delete_messages M = {x. Delete x ∈ M}"

fun depends_on where "depends_on M x y = (x ∈ M ∧ y ∈ M ∧ I x ∈ deps (Insert y))"

definition a_conditions ::
  "('ℐ :: linorder, 'Σ) insert_message set ⇒ ('ℐ extended ⇒ 'ℐ position) ⇒ bool"
  where "a_conditions M a = (
    a ⊢ < a ⊣ ∧
    (∀m. m ∈ M ⟶ a (P m) < a (S m) ∧
                   a ⟦I m⟧ = ⟦Ψ (a (P m), a (S m)) (I m)⟧))"

definition consistent :: "('ℐ :: linorder, 'Σ) message set ⇒ bool"
  where "consistent M ≡
    inj_on I (insert_messages M) ∧
    (⋃ (deps ` M) ⊆ (I ` insert_messages M)) ∧
    wfP (depends_on (insert_messages M)) ∧
    (∃a. a_conditions (insert_messages M) a)"

lemma consistent_subset:
  assumes "consistent N"
  assumes "M ⊆ N"
  assumes "⋃ (deps ` M) ⊆ (I ` insert_messages M)"
  shows "consistent M"
proof -
  have a:"insert_messages M ⊆ insert_messages N"
    using assms(2) insert_messages_def by blast
  hence b:"inj_on I (insert_messages M)"
    using assms(1) consistent_def inj_on_subset by blast
  have "wfP (depends_on (insert_messages N))"
    using assms(1) consistent_def by blast
  moreover have 
    "depends_on (insert_messages M) ≤ depends_on (insert_messages N)" 
    using a by auto
  ultimately have c:"wfP (depends_on (insert_messages M))"
    using a wf_subset [to_pred] by blast
  obtain a where "a_conditions (insert_messages N) a"
    using assms(1) consistent_def by blast
  hence "a_conditions (insert_messages M) a"
    by (meson a a_conditions_def subset_iff)
  thus ?thesis using b c assms(3) consistent_def by blast
qed

lemma pred_is_dep: "P m = ⟦ i ⟧ ⟶ i ∈ deps (Insert m)"
  by (metis Un_iff deps.simps(1) extended.set_intros extended.simps(27)
      extended_to_set.simps(1) insert_message.exhaust_sel)

lemma succ_is_dep: "S m = ⟦ i ⟧ ⟶ i ∈ deps (Insert m)"
  by (metis Un_insert_right deps.simps(1) extended_to_set.simps(1) insertI1
      insert_message.exhaust_sel)

lemma a_subset:
  fixes M N a
  assumes "M ⊆ N"
  assumes "a_conditions (insert_messages N) a"
  shows "a_conditions (insert_messages M) a"
  using assms by (simp add:a_conditions_def insert_messages_def, blast)

definition delete_maybe :: "'ℐ  ⇒ ('ℐ, 'Σ) message set ⇒ 'Σ  ⇒ 'Σ option" where 
  "delete_maybe i D s = (if Delete (DeleteMessage i) ∈ D then None else Some s)"

definition to_woot_character ::
  "('ℐ, 'Σ) message set ⇒ ('ℐ, 'Σ) insert_message ⇒ ('ℐ, 'Σ) woot_character"
  where
    "to_woot_character D m = (
       case m of
         (InsertMessage l i u s) ⇒ InsertMessage l i u (delete_maybe i D s))"

lemma to_woot_character_keeps_i [simp]: "I (to_woot_character M m) = I m"
  by (cases m, simp add:to_woot_character_def)

lemma to_woot_character_keeps_i_lifted [simp]: 
  "I ` to_woot_character M ` X = I ` X"
  by (metis (no_types, lifting) image_cong image_image to_woot_character_keeps_i)

lemma to_woot_character_keeps_P [simp]: "P (to_woot_character M m) = P m"
  by (cases m, simp add:to_woot_character_def)

lemma to_woot_character_keeps_S [simp]: "S (to_woot_character M m) = S m"
  by (cases m, simp add:to_woot_character_def)

lemma to_woot_character_insert_no_eff:
  "to_woot_character (insert (Insert m) M) = to_woot_character M"
  by (rule HOL.ext, simp add:delete_maybe_def to_woot_character_def insert_message.case_eq_if)

definition is_associated_string ::
  "('ℐ, 'Σ) message set ⇒ ('ℐ :: linorder, 'Σ) woot_character list ⇒ bool"
  where "is_associated_string M s ≡ (
    consistent M ∧
    set s = to_woot_character M ` (insert_messages M) ∧
    (∀a. a_conditions (insert_messages M) a ⟶ 
         sorted_wrt (<) (map a (ext_ids s))))"

fun is_certified_associated_string where
  "is_certified_associated_string M (Inr v) = is_associated_string M v" |
  "is_certified_associated_string M (Inl _) = False"

lemma associated_string_unique:
  assumes "is_associated_string M s"
  assumes "is_associated_string M t"
  shows "s = t"
  using assms
  apply (simp add:ext_ids_def is_associated_string_def consistent_def
         sorted_wrt_append)
  by (metis sort_set_unique)

lemma is_certified_associated_string_unique:
  assumes "is_certified_associated_string M s"
  assumes "is_certified_associated_string M t"
  shows "s = t"
  using assms by (case_tac s, case_tac [!] t, (simp add:associated_string_unique)+)

lemma empty_consistent: "consistent {}"
proof -
  have "a_conditions {} (λx. (case x of ⊢ ⇒ ⊢ | ⊣ ⇒ ⊣))"
    by (simp add: a_conditions_def)
  hence "∃f. a_conditions {} f" by blast
  moreover have "wfP (depends_on {})" by (simp add: wfP_eq_minimal)
  ultimately show ?thesis by (simp add:consistent_def insert_messages_def)
qed

lemma empty_associated: "is_associated_string {} []"
  by (simp add:is_associated_string_def insert_messages_def empty_consistent 
      ext_ids_def a_conditions_def)

text ‹The empty set of messages is consistent and the associated string is the empty string.›

end