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 "(in'. the_singleton∥⇘t i
    (n''the_singleton  t⟩⇘n'. n''  the_singleton  t⟩⇘n' eval the_singleton t t' n'' γ)) 
    ¬ (in'. 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 "nn'"
    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''. nn''; 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
   "(in'. 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'' γ') 
   ¬ (in'. 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