Theory Singleton

(*
  Title:      Singleton.thy
  Author:     Diego Marmsoler
*)
section "A Theory of Singletons"
text‹
  In the following, we formalize the specification of the singleton pattern as described in~\<^cite>‹"Marmsoler2018c"›.
›
  
theory Singleton
imports DynamicArchitectures.Dynamic_Architecture_Calculus
begin
subsection Singletons
text ‹
  In the following we formalize a variant of the Singleton pattern.
›
locale singleton = dynamic_component cmp active
    for active :: "'id ⇒ cnf ⇒ bool" ("∥_∥⇘_⇙" [0,110]60)
    and cmp :: "'id ⇒ cnf ⇒ 'cmp" ("σ⇘_⇙(_)" [0,110]60) +
assumes alwaysActive: "⋀k. ∃id. ∥id∥⇘k⇙"
    and unique: "∃id. ∀k. ∀id'. (∥id'∥⇘k⇙ ⟶ id = id')"
begin
subsubsection "Calculus Interpretation"
text ‹
\noindent
@{thm[source] baIA}: @{thm baIA [no_vars]}
›
text ‹
\noindent
@{thm[source] baIN1}: @{thm baIN1 [no_vars]}
›
text ‹
\noindent
@{thm[source] baIN2}: @{thm baIN2 [no_vars]}
›

subsubsection "Architectural Guarantees"

definition "the_singleton ≡ THE id. ∀k. ∀id'. ∥id'∥⇘k⇙ ⟶ id' = id"

theorem ts_prop:
  fixes k::cnf
  shows "⋀id. ∥id∥⇘k⇙ ⟹ id = the_singleton"
    and "∥the_singleton∥⇘k⇙"
proof -
  { fix id
    assume a1: "∥id∥⇘k⇙"
  have "(THE id. ∀k. ∀id'. ∥id'∥⇘k⇙ ⟶ id' = id) = id"
  proof (rule the_equality)
    show "∀k id'. ∥id'∥⇘k⇙ ⟶ id' = id"
    proof
      fix k show "∀id'. ∥id'∥⇘k⇙ ⟶ id' = id"
      proof
        fix id' show "∥id'∥⇘k⇙ ⟶ id' = id"
        proof
          assume "∥id'∥⇘k⇙"
          from unique have "∃id. ∀k. ∀id'. (∥id'∥⇘k⇙ ⟶ id = id')" .
          then obtain i'' where "∀k. ∀id'. (∥id'∥⇘k⇙ ⟶ i'' = id')" by auto
            with ‹∥id'∥⇘k⇙› have "id=i''" and "id'=i''" using a1 by auto
          thus "id' = id" by simp
        qed
      qed
    qed
  next
      fix i'' show "∀k id'. ∥id'∥⇘k⇙ ⟶ id' = i'' ⟹ i'' = id" using a1 by auto
  qed
    hence "∥id∥⇘k⇙ ⟹ id = the_singleton" by (simp add: the_singleton_def)
  } note g1 = this
  thus "⋀id. ∥id∥⇘k⇙ ⟹ id = the_singleton" by simp

  from alwaysActive obtain id where "∥id∥⇘k⇙" by blast
  with g1 have "id = the_singleton" by simp
  with ‹∥id∥⇘k⇙› show "∥the_singleton∥⇘k⇙" by simp
qed
declare ts_prop(2)[simp]
  
lemma lNact_active[simp]:
  fixes cid t n
  shows "⟨the_singleton ⇐ t⟩⇘n⇙ = n"
  using lNact_active ts_prop(2) by auto

lemma lNxt_active[simp]:
  fixes cid t n
  shows "⟨the_singleton → t⟩⇘n⇙ = n"
by (simp add: nxtAct_active)
    
lemma baI[intro]:
  fixes t n a
  assumes "φ (σ⇘the_singleton⇙(t n))"
  shows "eval the_singleton t t' n [φ]⇩b" using assms by (simp add: baIANow)
  
lemma baE[elim]:
  fixes t n a
  assumes "eval the_singleton t t' n [φ]⇩b"                      
  shows "φ (σ⇘the_singleton⇙(t n))" using assms by (simp add: baEANow)

lemma evtE[elim]:
  fixes t id n a
  assumes "eval the_singleton t t' n (◇⇩b γ)"
  shows "∃n'≥n. eval the_singleton t t' n' γ"
proof -
  have "∥the_singleton∥⇘t n⇙" by simp
  with assms obtain n' where "n'≥⟨the_singleton → t⟩⇘n⇙" and "(∃i≥n'. ∥the_singleton∥⇘t i⇙ ∧
    (∀n''≥⟨the_singleton ⇐ t⟩⇘n'⇙. n'' ≤ ⟨the_singleton → t⟩⇘n'⇙ ⟶ eval the_singleton t t' n'' γ)) ∨
    ¬ (∃i≥n'. ∥the_singleton∥⇘t i⇙) ∧ eval the_singleton t t' n' γ" using evtEA[of n "the_singleton" t] by blast
  moreover have "∥the_singleton∥⇘t n'⇙" by simp
  ultimately have
    "∀n''≥⟨the_singleton ⇐ t⟩⇘n'⇙. n'' ≤ ⟨the_singleton → t⟩⇘n'⇙ ⟶ eval the_singleton t t' n'' γ" by auto
  hence "eval the_singleton t t' n' γ" by simp
  moreover from ‹n'≥⟨the_singleton → t⟩⇘n⇙› have "n'≥n" by (simp add: nxtAct_active)
  ultimately show ?thesis by auto
qed
  
lemma globE[elim]:
  fixes t id n a
  assumes "eval the_singleton t t' n (□⇩b γ)"
  shows "∀n'≥n. eval the_singleton t t' n' γ"
proof
  fix n' show "n ≤ n' ⟶ eval the_singleton t t' n' γ"
  proof
    assume "n≤n'"
    hence "⟨the_singleton ⇐ t⟩⇘n⇙ ≤ n'" by simp
    moreover have "∥the_singleton∥⇘t n⇙" by simp
    ultimately show "eval the_singleton t t' n' γ"
      using ‹eval the_singleton t t' n (□⇩b γ)› globEA by blast
  qed
qed

lemma untilI[intro]:
  fixes t::"nat ⇒ cnf"
    and t'::"nat ⇒ 'cmp"
    and n::nat
    and n'::nat
  assumes "n'≥n"
    and "eval the_singleton t t' n' γ"
    and "⋀n''. ⟦n≤n''; n''<n'⟧ ⟹ eval the_singleton t t' n'' γ'"
  shows "eval the_singleton t t' n (γ' 𝔘⇩b γ)"
proof -
  have "∥the_singleton∥⇘t n⇙" by simp 
  moreover from ‹n'≥n› have "⟨the_singleton ⇐ t⟩⇘n⇙ ≤ n'" by simp
  moreover have "∥the_singleton∥⇘t n'⇙" by simp
  moreover have
    "∃n''≥⟨the_singleton ⇐ t⟩⇘n'⇙. n'' ≤ ⟨the_singleton → t⟩⇘n'⇙ ∧ eval the_singleton t t' n'' γ ∧
    (∀n'''≥⟨the_singleton → t⟩⇘n⇙. n''' < ⟨the_singleton ⇐ t⟩⇘n''⇙ ⟶
      (∃n''''≥⟨the_singleton ⇐ t⟩⇘n'''⇙. n'''' ≤ ⟨the_singleton → t⟩⇘n'''⇙ ∧ eval the_singleton t t' n'''' γ'))"
  proof -
    have "n'≥⟨the_singleton ⇐ t⟩⇘n'⇙" by simp
    moreover have "n' ≤ ⟨the_singleton → t⟩⇘n'⇙" by simp
    moreover from assms(3) have "(∀n''≥⟨the_singleton → t⟩⇘n⇙. n'' < ⟨the_singleton ⇐ t⟩⇘n'⇙ ⟶
      (∃n'''≥⟨the_singleton ⇐ t⟩⇘n''⇙. n''' ≤ ⟨the_singleton → t⟩⇘n''⇙ ∧ eval the_singleton t t' n''' γ'))"
      by auto
    ultimately show ?thesis using ‹eval the_singleton t t' n' γ› by auto
  qed
  ultimately show ?thesis using untilIA[of n "the_singleton" t n' t' γ γ'] by blast
qed

lemma untilE[elim]:
  fixes t id n γ' γ
  assumes "eval the_singleton t t' n (γ' 𝔘⇩b γ)"
  shows "∃n'≥n. eval the_singleton t t' n' γ ∧ (∀n''≥n. n'' < n' ⟶ eval the_singleton t t' n'' γ')"
proof -
  have "∥the_singleton∥⇘t n⇙" by simp
  with ‹eval the_singleton t t' n (γ' 𝔘⇩b γ)› obtain n' where "n'≥⟨the_singleton → t⟩⇘n⇙" and
   "(∃i≥n'. ∥the_singleton∥⇘t i⇙) ∧
   (∀n''≥⟨the_singleton ⇐ t⟩⇘n'⇙. n'' ≤ ⟨the_singleton → t⟩⇘n'⇙ ⟶ eval the_singleton t t' n'' γ) ∧
   (∀n''≥⟨the_singleton ⇐ t⟩⇘n⇙. n'' < ⟨the_singleton ⇐ t⟩⇘n'⇙ ⟶ eval the_singleton t t' n'' γ') ∨
   ¬ (∃i≥n'. ∥the_singleton∥⇘t i⇙) ∧
   eval the_singleton t t' n' γ ∧ (∀n''≥⟨the_singleton ⇐ t⟩⇘n⇙. n'' < n' ⟶ eval the_singleton t t' n'' γ')"
  using untilEA[of n "the_singleton" t t' γ' γ] by auto
  moreover have "∥the_singleton∥⇘t n'⇙" by simp
  ultimately have
    "(∀n''≥⟨the_singleton ⇐ t⟩⇘n'⇙. n'' ≤ ⟨the_singleton → t⟩⇘n'⇙ ⟶ eval the_singleton t t' n'' γ) ∧
    (∀n''≥⟨the_singleton ⇐ t⟩⇘n⇙. n'' < ⟨the_singleton ⇐ t⟩⇘n'⇙ ⟶ eval the_singleton t t' n'' γ')" by auto
  hence "eval the_singleton t t' n' γ" and "(∀n''≥n. n'' < n' ⟶ eval the_singleton t t' n'' γ')" by auto
  with ‹eval the_singleton t t' n' γ› ‹n'≥⟨the_singleton → t⟩⇘n⇙› show ?thesis by auto
qed
end

end