Theory CopyBufferRevisited

theory CopyBufferRevisited
imports  "HOL-CSPM" "HOL-CSP.CopyBuffer"

begin

section‹Objective›

text‹This theory contains a number of standard proof techniques for classical assertions
of the paradigmatic ▩‹CopyBuffer› example (arbitrary alphabet). The core of this example
has already been presented in the \<^theory>‹HOL-CSP› session, here we add the missing proofs 
for the assertions \<^term>‹deadlock_free› and  \<^term>‹lifelock_free› known from FDR4 for CSPM.
The proof-style is deliberately optimized for readability and clear algebraic presentation 
rather than for brievity and automation.›

section‹Deadlock-Freeness of COPY, SEND and REC›

lemma deadlock_free_COPY : ‹deadlock_free (COPY :: 'a channel process)›
proof (rule deadlock_free_gen_n_coinduct[where A = ‹range left ∪ range right› and n = 1])
  show ‹range left ∪ range right ≠ ({} :: 'a channel set)› by blast
next
  fix x :: ‹'a channel process›
  assume hyp : ‹x ⊑⇩F⇩D COPY›
  have 1 : ‹⊓a∈(range left ∪ range right) → x ⊑⇩F⇩D ⊓a∈range right → x›
    by (rule Mndetprefix_FD_subset) simp_all
  have 2 : ‹⊓a∈range right → x ⊑⇩F⇩D right❙!v → x› for v
    apply (unfold write_def, rule trans_FD[OF Mndetprefix_FD_subset[of ‹{right v}› ‹range right›]])
    by (simp_all add: Mndetprefix_FD_Mprefix Mprefix_singl)
  have ab : ‹⊓a∈(range left ∪ range right) → x ⊑⇩F⇩D right❙!v → x› for v
    using 1 2 trans_FD by blast
  have 3 : ‹left❙?v → ⊓a∈(range left ∪ range right) → x ⊑⇩F⇩D left❙?v → right❙!v → x›
    by (simp add: ab mono_read_FD)
  have 4 : ‹⊓a∈(range left ∪ range right) → X ⊑⇩F⇩D ⊓a∈range left → X› for X
    by (rule Mndetprefix_FD_subset) simp_all
  have 5 : ‹⊓a∈range left → X ⊑⇩F⇩D left❙?v → X› for X
    unfolding read_def by (subst K_record_comp) (fact Mndetprefix_FD_Mprefix)
  have 6 : ‹⊓a∈(range left ∪ range right) → ⊓a∈(range left ∪ range right) → x
              ⊑⇩F⇩D left❙?v → right❙!v → x› for v
    using 3 4[of ‹⊓a∈(range left ∪ range right) → x›]
      5[of ‹⊓a∈(range left ∪ range right) → x›] trans_FD by blast
  have 7 : ‹left❙?v → right❙!v → x ⊑⇩F⇩D left❙?v → right❙!v → COPY› for v
    by (simp add: hyp mono_read_FD mono_write_FD)
  show ‹⊓a∈(range left ∪ range right) →
        ((λX. ⊓a∈(range left ∪ range right) → X) ^^ 1) x ⊑⇩F⇩D COPY›
    using 6 7 by simp (metis (mono_tags, lifting) COPY_rec trans_FD)
qed

text‹\<^const>‹SEND› and \<^const>‹REC› cycle over three steps instead of two, so we instantiate
‹deadlock_free_gen_n_coinduct› at \<^term>‹n = (2::nat)› this time, with the alphabet being
the whole set of events \<^const>‹SEND› (resp.\ \<^const>‹REC›) ever touches along its cycle.›

lemma deadlock_free_SEND : ‹deadlock_free (SEND :: 'a channel process)›
proof (rule deadlock_free_gen_n_coinduct
         [where A = ‹range left ∪ range mid ∪ {ack}› and n = 2])
  show ‹range left ∪ range mid ∪ {ack} ≠ ({} :: 'a channel set)› by blast
next
  define A :: ‹'a channel set› where ‹A ≡ range left ∪ range mid ∪ {ack}›
  fix x :: ‹'a channel process›
  assume hyp : ‹x ⊑⇩F⇩D SEND›
  have step_ack : ‹⊓a∈A → Z ⊑⇩F⇩D ack → Z› for Z
    apply (rule trans_FD[OF Mndetprefix_FD_subset[of ‹{ack}› A]])
    by (simp_all add: A_def Mndetprefix_FD_Mprefix Mprefix_singl)
  have M1 : ‹⊓a∈A → Z ⊑⇩F⇩D ⊓a∈range mid → Z› for Z
    by (rule Mndetprefix_FD_subset) (auto simp: A_def)
  have M2 : ‹⊓a∈range mid → Z ⊑⇩F⇩D mid❙!v → Z› for Z v
    apply (unfold write_def, rule trans_FD[OF Mndetprefix_FD_subset[of ‹{mid v}› ‹range mid›]])
    by (simp_all add: Mndetprefix_FD_Mprefix Mprefix_singl)
  have step_mid : ‹⊓a∈A → Z ⊑⇩F⇩D mid❙!v → Z› for Z v 
    by (metis M1 M2 trans_FD)
  have L1 : ‹⊓a∈A → Z ⊑⇩F⇩D ⊓a∈range left → Z› for Z
    by (rule Mndetprefix_FD_subset) (auto simp: A_def)
  have L2 : ‹⊓a∈range left → Z ⊑⇩F⇩D left❙?v → Z› for Z
    unfolding read_def by (subst K_record_comp) (fact Mndetprefix_FD_Mprefix)
  have step_left : ‹⊓a∈A → Z ⊑⇩F⇩D left❙?v → Z› for Z
    using L1 L2 trans_FD by blast
  have level2 : ‹⊓a∈A → ⊓a∈A → x ⊑⇩F⇩D mid❙!v → ack → x› for v
    using step_mid[of ‹⊓a∈A → x› v] step_ack[of x] mono_write_FD trans_FD 
    by fast
  have level1 : ‹⊓a∈A → ⊓a∈A → ⊓a∈A → x ⊑⇩F⇩D left❙?v → mid❙!v → ack → x› for v
    using step_left[of ‹⊓a∈A → ⊓a∈A → x›] level2 mono_read_FD trans_FD
    by (metis (no_types, lifting))
  have final : ‹left❙?v → mid❙!v → ack → x ⊑⇩F⇩D left❙?v → mid❙!v → ack → SEND› for v
    by (simp add: hyp mono_read_FD mono_write_FD mono_write0_FD)
  have conv : "2 = Suc(Suc 0)" by simp 
  show ‹⊓a∈A → ((λX. ⊓a∈A → X) ^^ 2) x ⊑⇩F⇩D SEND›
    apply(subst conv) (* why is this necessary ? *)
    using level1 final conv apply simp
    by (metis (mono_tags, lifting) SEND_rec dual_order.trans)
qed

text‹\<^const>‹REC› mirrors \<^const>‹SEND› exactly (read on \<^const>‹mid›, write on \<^const>‹right›,
then the fixed event \<^const>‹ack›), so the same three-layer peeling argument applies. This time
each intermediate ‹⊑⇩F⇩D›-fact is built by an explicit ‹rule trans_FD[OF …]› application
rather than handing several facts to ‹blast›/‹metis› at once: the underlying monotonicity
lemmas (‹mono_read_FD›, ‹mono_write_FD›) are themselves ‹⋀›-quantified rules, and leaving
their instantiation to an unguided search over several such rules simultaneously is what made
the analogous \<^const>‹SEND› proof slow above; fully applying each step explicitly keeps every
call a single, cheap, fully-determined unification.›

lemma deadlock_free_REC : ‹deadlock_free (REC :: 'a channel process)›
proof (rule deadlock_free_gen_n_coinduct
         [where A = ‹range mid ∪ range right ∪ {ack}› and n = 2])
  show ‹range mid ∪ range right ∪ {ack} ≠ ({} :: 'a channel set)› by blast
next
  define A :: ‹'a channel set› where ‹A ≡ range mid ∪ range right ∪ {ack}›
  fix x :: ‹'a channel process›
  assume hyp : ‹x ⊑⇩F⇩D REC›
  have step_ack : ‹⊓a∈A → Z ⊑⇩F⇩D ack → Z› for Z
    apply (rule trans_FD[OF Mndetprefix_FD_subset[of ‹{ack}› A]])
    by (simp_all add: A_def Mndetprefix_FD_Mprefix Mprefix_singl)
  have R1 : ‹⊓a∈A → Z ⊑⇩F⇩D ⊓a∈range right → Z› for Z
    by (rule Mndetprefix_FD_subset) (auto simp: A_def)
  have R2 : ‹⊓a∈range right → Z ⊑⇩F⇩D right❙!v → Z› for Z v
    apply (unfold write_def, rule trans_FD[OF Mndetprefix_FD_subset[of ‹{right v}› ‹range right›]])
    by (simp_all add: Mndetprefix_FD_Mprefix Mprefix_singl)
  have step_right : ‹⊓a∈A → Z ⊑⇩F⇩D right❙!v → Z› for Z v
    by (rule trans_FD[OF R1 R2])
  have M1 : ‹⊓a∈A → Z ⊑⇩F⇩D ⊓a∈range mid → Z› for Z
    by (rule Mndetprefix_FD_subset) (auto simp: A_def)
  have M2 : ‹⊓a∈range mid → Z ⊑⇩F⇩D mid❙?v → Z› for Z
    unfolding read_def by (subst K_record_comp) (fact Mndetprefix_FD_Mprefix)
  have step_mid : ‹⊓a∈A → Z ⊑⇩F⇩D mid❙?v → Z› for Z
    by (rule trans_FD[OF M1 M2])
  have level2 : ‹⊓a∈A → ⊓a∈A → x ⊑⇩F⇩D right❙!v → ack → x› for v
    by (rule trans_FD[OF step_right[of ‹⊓a∈A → x› v]]) (simp add: step_ack mono_write_FD)
  have level1 : ‹⊓a∈A → ⊓a∈A → ⊓a∈A → x ⊑⇩F⇩D mid❙?v → right❙!v → ack → x› for v
    by (rule trans_FD[OF step_mid]) (simp add: level2 mono_read_FD)
  have final : ‹mid❙?v → right❙!v → ack → x ⊑⇩F⇩D mid❙?v → right❙!v → ack → REC› for v
    by (simp add: hyp mono_read_FD mono_write_FD mono_write0_FD)
  show ‹⊓a∈A → ((λX. ⊓a∈A → X) ^^ 2) x ⊑⇩F⇩D REC›
    using level1 final by (simp add: eval_nat_numeral) (metis (mono_tags, lifting) REC_rec trans_FD)
qed

subsection‹Deadlock-Freeness of SYSTEM›

text‹\<^const>‹SYSTEM› is built from \<^const>‹SEND› and \<^const>‹REC› by synchronisation and hiding,
so its own alphabet does not fit the simple ‹deadlock_free_gen_n_coinduct› pattern at all
(it is not a bounded lasso over a fixed set). Instead we transport deadlock-freeness from
\<^const>‹COPY› along the classical refinement \<^term>‹COPY ⊑⇩F⇩D SYSTEM›: since
\<^term>‹deadlock_free P ≡ DF UNIV ⊑⇩F⇩D P›, deadlock-freeness is monotone under ‹⊑⇩F⇩D›
by plain transitivity, so \<^const>‹deadlock_free› \<^const>‹COPY› together with \<^term>‹COPY ⊑⇩F⇩D SYSTEM›
gives \<^const>‹deadlock_free› \<^const>‹SYSTEM› directly, without needing the stronger fact
(\<^term>‹SYSTEM = COPY›, which only holds when \<^term>‹SYN› is finite).›

lemma simplification_lemmas [simp] :
  ‹range left ∩ SYN = {}›  ‹range right ∩ SYN = {}›  ‹ack ∈ SYN›    ‹range mid ⊆ SYN›
  ‹mid x ∈ SYN›            ‹right x ∉ SYN›           ‹left x ∉ SYN› ‹inj mid›
  by (auto simp: SYN_def inj_on_def)

lemmas Sync_rules   = read_Sync_read_subset_forced_read_same_chan
                      read_Sync_read_left read_Sync_read_right
                      write_Sync_read_left write_Sync_read_right
                      read_Sync_write_left read_Sync_write_right
                      write_Sync_write_subset
                      write_Sync_read_subset read_Sync_write_subset
                      write0_Sync_write_right write0_Sync_write0

lemmas Hiding_rules = Hiding_read_disjoint Hiding_write_subset Hiding_write_disjoint
                      Hiding_write0_non_disjoint Hiding_write0_disjoint

text‹Again the refineness proof known from the ▩‹CopyBuffer›-theory:›
lemma COPY_FD_SYSTEM : ‹(COPY :: 'a channel process) ⊑⇩F⇩D SYSTEM›
  unfolding SYSTEM_def COPY_def
proof (rule fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \ SYN))›
    by (simp add: cont2mono)
next
  show ‹⊥ ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \ SYN)›
    by simp
next
  fix x :: ‹'a channel process›
  assume hyp : ‹x ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \ SYN)›
  show ‹(Λ x. left❙?xa → right❙!xa → x)⋅x ⊑⇩F⇩D (SEND ⟦SYN⟧ REC \ SYN)›
    apply (subst SEND_rec, subst REC_rec)
    apply (simp add: cont_fun)
  proof -
    have ‹left❙?x → mid❙!x → ack → SEND ⟦SYN⟧ mid❙?x → right❙!x → ack → REC \ SYN
             =  left❙?x → (mid❙!x → ack → SEND ⟦SYN⟧ mid❙?x → right❙!x → ack → REC \ SYN)›
      (is ‹?lhs = _›)
      by (simp add: Sync_rules Hiding_rules)
    also have ‹… =  left❙?x → (mid❙!x → (ack → SEND ⟦SYN⟧ right❙!x → ack → REC) \ SYN)›
      by (simp add: Sync_rules Hiding_rules)
    also have ‹… = left❙?x → (ack → SEND ⟦SYN⟧ right❙!x → ack → REC) \ SYN›
      by (simp add: Sync_rules Hiding_rules)
    also have ‹… = left❙?x → right❙!x → (ack → SEND ⟦SYN⟧ ack → REC) \ SYN›
      by (simp add: Sync_rules Hiding_rules)
    also have ‹… = left❙?x → right❙!x → (SEND ⟦SYN⟧ REC \ SYN)› (is ‹_ = ?rhs›)
      by (simp add: Sync_rules Hiding_rules)
    finally have * : ‹?lhs = ?rhs› .
    show ‹left❙?xa → right❙!xa → x ⊑⇩F⇩D ?lhs›
      by (simp only: "*" mono_read_FD mono_write_FD hyp)
  qed
qed

lemma deadlock_free_SYSTEM : ‹deadlock_free (SYSTEM :: 'a channel process)›
  using deadlock_free_COPY COPY_FD_SYSTEM deadlock_free_mono_FD by blast

section‹Lifelock-Freeness of COPY, SEND, REC and SYSTEM›

text‹A direct CHAOS-based coinduction here (mirroring ‹deadlock_free_gen_n_coinduct›) would
not simply reuse the same combinatorics: \<^const>‹CHAOS›'s step is built on ∗‹external›
choice (\<^term>‹□a∈A → X›), for which restricting the offered alphabet is not a refinement the
way it is for \<^const>‹Mndetprefix› (‹Mndetprefix_FD_subset›) --- internal choice may always
commit to fewer branches, but external choice genuinely changes what is offered. Fortunately
none of that is needed here: the library already proves the general, unconditional fact
‹deadlock_free_implies_lifelock_free› : \<^term>‹deadlock_free P ⟹ lifelock_free P› (deadlock-freeness
is always the stronger property), so lifelock-freeness of \<^const>‹COPY›, \<^const>‹SEND›,
\<^const>‹REC› and \<^const>‹SYSTEM› follows at once from what is already proved above.›

lemma lifelock_free_COPY : ‹lifelock_free (COPY :: 'a channel process)›
  by (rule deadlock_free_implies_lifelock_free[OF deadlock_free_COPY])

lemma lifelock_free_SEND : ‹lifelock_free (SEND :: 'a channel process)›
  by (rule deadlock_free_implies_lifelock_free[OF deadlock_free_SEND])

lemma lifelock_free_REC : ‹lifelock_free (REC :: 'a channel process)›
  by (rule deadlock_free_implies_lifelock_free[OF deadlock_free_REC])

lemma lifelock_free_SYSTEM : ‹lifelock_free (SYSTEM :: 'a channel process)›
  by (rule deadlock_free_implies_lifelock_free[OF deadlock_free_SYSTEM])



end