(*<*)
―‹ ********************************************************************
 * Project : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version : 2.0
 *
 * Author : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 * (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file : Example of Copy Buffer
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 * * Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above
 * copyright notice, this list of conditions and the following
 * disclaimer in the documentation and/or other materials provided
 * with the distribution.
 *
 * * Neither the name of the copyright holders nor the names of its
 * contributors may be used to endorse or promote products derived
 * from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

chapter‹ Annex: Running Example with Buffer over infinite Alphabet›

(*<*)
theory      CopyBuffer 
  imports   "HOL-CSP"
begin 
(*>*)

section‹ Defining the Copy-Buffer Example ›


datatype 'a channel = left 'a | right 'a | mid 'a | ack

definition SYN  :: "'a channel set"
  where     "SYN ≡ range mid ∪ {ack}"

definition COPY :: "'a channel process"
  where     "COPY ≡ μ COPY. left?x → right!x → COPY"

definition SEND :: "'a channel process"
  where     "SEND ≡ μ SEND. left?x → mid!x → ack → SEND"

definition REC  :: "'a channel process"
  where     "REC ≡ μ REC. mid?x → right!x → ack → REC"


definition SYSTEM :: "'a channel process"
  where     ‹SYSTEM ≡ SEND [ SYN ] REC \ SYN›

thm SYSTEM_def

section‹ The Standard Proof ›

subsection‹ Channels and Synchronization Sets›

text‹ First part: abstract properties for these events to SYN.
 This kind of stuff could be automated easily by some
 extra-syntax for channels and SYN-sets. ›

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)

lemma "finite (SYN:: 'a channel set) ==> finite {(t::'a). True}"
  by (metis (no_types) SYN_def UNIV_def channel.inject(3) finite_Un finite_imageD inj_on_def)

subsection‹ Definitions by Recursors ›

text‹ Second part: Derive recursive process equations, which
 are easier to handle in proofs. This part IS actually
 automated if we could reuse the fixrec-syntax below. ›

lemma COPY_rec:
  "COPY = left?x → right!x → COPY"
  by(simp add: COPY_def,rule trans, rule fix_eq, simp)

lemma SEND_rec: 
  "SEND = left?x → mid!x → ack → SEND"
  by(simp add: SEND_def,rule trans, rule fix_eq, simp)

lemma REC_rec:
  "REC = mid?x → right!x → ack → REC"
  by(simp add: REC_def,rule trans, rule fix_eq, simp)


subsection‹ Various Samples of Refinement Proofs ›


(* ************************************************************************* *)
(*                                                            *)
(* Setup for rewriting                                          *)
(*                                                          *)
(* ************************************************************************* *)

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

lemmas mono_rules = mono_read_FD mono_write_FD mono_write0_FD



text‹An example for a very explicit structured proof.
 Slow-motion for presentations. Note that the proof makes
 no assumption over the structure of the content of the channel;
 it is truly polymorphic wrt. the channel type typ‹'α›.›

lemma impl_refines_spec' : "(COPY :: 'a channel process) ⊑_FD SYSTEM"
  unfolding  SYSTEM_def COPY_def
proof (rule fix_ind)
  show "adm (λa. a ⊑_FD (SEND [SYN] REC \\ SYN))" 
    by (simp add: cont2mono)
next 
  show "⊥ ⊑_FD (SEND [SYN] REC \\ SYN)"
    by simp
next
  fix x :: "'a channel process"
  assume hyp : "x ⊑_FD (SEND [SYN] REC \\ SYN)"
  show "(Λ x. left?xa → right!xa → x)⋅x ⊑_FD (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 ⊑_FD ?lhs"
      by (simp only : "*" mono_read_FD mono_write_FD hyp)
  qed
qed



text‹An example for a highly automated proof.›
text‹Not too bad in automation considering what is inferred, but wouldn't scale for large examples. ›


lemma impl_refines_spec : "COPY ⊑_FD SYSTEM"
  unfolding SYSTEM_def COPY_def
  apply(rule fix_ind, auto intro: le_FD_adm simp:  cont_fun monofunI)
  apply(subst SEND_rec, subst REC_rec)
  apply (simp add: Sync_rules Hiding_rules mono_read_FD mono_write_FD) (*  write0_Sync_write0 write_is_write0 *)
  oops


lemma spec_refines_impl : 
  assumes fin: "finite (SYN:: 'a channel set)"
  shows        "SYSTEM ⊑_FD (COPY :: 'a channel process)"
  apply(simp add: SYSTEM_def SEND_def)
  apply(rule fix_ind, simp_all)
   apply (intro le_FD_adm)
    apply (simp add: fin)
   apply (simp add: cont2mono)
  apply (simp add: Sync_commute)
  apply (subst COPY_rec, subst REC_rec)
  apply (simp add: read_def write_def comp_def)
  apply (subst Mprefix_Sync_Mprefix_right) apply auto[2]
  apply (simp add: Sync_rules Hiding_rules comp_def)
  apply (subst Hiding_Mprefix_disjoint) apply auto[1]
  apply (intro mono_Mprefix_FD ballI)
  apply (subst Mprefix_Sync_Mprefix_subset) apply auto[2]
  apply (subst Hiding_Mprefix_non_disjoint) apply auto[1]
  apply simp
  apply (fold write0_def)
  by (simp add: Hiding_write0_disjoint Hiding_write0_non_disjoint Sync_commute mono_write0_FD write0_Sync_write0)



text‹ Note that this was actually proven for the
 Process ordering, not the refinement ordering.
 But the former implies the latter.
 And due to anti-symmetry, equality follows
 for the case of finite alphabets \ldots ›

lemma spec_equal_impl : 
  assumes fin:  "finite (SYN::('a channel)set)"
  shows         "SYSTEM = (COPY::'a channel process)"
  by (simp add: FD_antisym fin impl_refines_spec' spec_refines_impl)

subsection‹Deadlock Freeness Proof ›

text‹HOL-CSP can be used to prove deadlock-freeness of processes with infinite alphabet. In the
  of the @{term COPY} - process, this can be formulated as the following refinement problem:›

lemma DF_COPY : "(DF (range left ∪ range right)) ⊑_FD COPY"
  apply(simp add:DF_def,rule fix_ind2)
proof -
  show "adm (λa. a ⊑_FD COPY)"   by(rule le_FD_adm, simp_all add: monofunI)
next
  show "⊥ ⊑_FD COPY" by fastforce
next
  have 1: "(⊓xa∈ (range left ∪ range right) → ⊥) ⊑_FD (⊓xa∈ range left → ⊥)"
    by (simp add: Mndetprefix_FD_subset)
  have 2: "(⊓xa∈ range left → ⊥) ⊑_FD (left?x → ⊥)" 
    unfolding read_def
    by (meson Mndetprefix_FD_Mprefix BOT_leFD mono_Mndetprefix_FD trans_FD)
  show "(Λ x. ⊓xa∈(range left ∪ range right) → x)⋅⊥ ⊑_FD COPY" 
    by simp (metis (mono_tags, lifting) 1 2 COPY_rec mono_read_FD BOT_leFD trans_FD)
next
  fix P::"'a channel process"
  assume  *: "P ⊑_FD COPY" and ** : "(Λ x. ⊓xa∈(range left ∪ range right) → x)⋅P ⊑_FD COPY"
  have 1:"⊓xa∈ (range left ∪ range right) → P ⊑_FD ⊓xa∈ range right → P"
    by (simp add: Mndetprefix_FD_subset)
  have 2:"⊓xa∈ range right → P ⊑_FD right!x → P" for x
    apply (unfold write_def, rule trans_FD[OF Mndetprefix_FD_subset[of ‹{right x}› ‹range right›]])
    by (simp_all add: Mndetprefix_FD_Mprefix Mprefix_singl)
  from 1 2 have ab:"⊓xa∈ (range left ∪ range right) → P ⊑_FD right!x → P" for x
    using trans_FD by blast
  hence 3:"left?x → ⊓xa∈ (range left ∪ range right) → P ⊑_FD left?x → right!x → P"
    by (simp add: mono_read_FD)
  have 4:"∧X. ⊓xa∈ (range left ∪ range right) → X ⊑_FD ⊓xa∈ range left → X"
    by (rule Mndetprefix_FD_subset, simp, blast) 
  have 5:"∧X. ⊓xa∈ range left → X ⊑_FD left?x → X"
    by (unfold read_def, subst K_record_comp, fact Mndetprefix_FD_Mprefix)
  from 3 4[of "⊓xa∈ (range left ∪ range right) → P"] 
    5  [of "⊓xa∈ (range left ∪ range right) → P"] 
  have 6:"⊓xa∈ (range left ∪ range right) →
                  ⊓xa∈ (range left ∪ range right) → P ⊑_FD left?x → right!x → P"
    using trans_FD by blast
  from * ** have 7:"left?x → right!x → P ⊑_FD left?x → right!x → COPY"
    by (simp add: mono_read_FD mono_write_FD)

  show "(Λ x. ⊓xa∈(range left ∪ range right) → x)⋅
             ((Λ x. ⊓xa∈(range left ∪ range right) → x)⋅P) ⊑_FD COPY"
    by simp (metis (mono_tags, lifting) "6" "7" COPY_rec trans_FD)
qed

section‹ An Alternative Approach: Using the fixrec-Package ›

subsection‹ Channels and Synchronisation Sets ›

text‹ As before. ›

subsection‹ Process Definitions via fixrec-Package ›

fixrec
  COPY' :: "'a channel process"
  and
  SEND' :: "'a channel process"
  and
  REC' :: "'a channel process"
  where
    COPY'_rec[simp del]:  "COPY' = left?x → right!x → COPY'"
  |  SEND'_rec[simp del]:  "SEND' = left?x → mid!x → ack → SEND'"
  |  REC'_rec[simp del] :  "REC' = mid?x → right!x → ack → REC'"

thm COPY'_rec
definition SYSTEM' :: "'a channel process"
  where     ‹SYSTEM' ≡ ((SEND' [ SYN ] REC') \ SYN)›

subsection‹ Another Refinement Proof on fixrec-infrastructure ›

text‹ Third part: No comes the proof by fixpoint induction.
 Not too bad in automation considering what is inferred,
 but wouldn't scale for large examples. ›
thm COPY'_SEND'_REC'.induct
lemma impl_refines_spec'' : "(COPY'::'a channel process) ⊑_FD SYSTEM'"
  apply (unfold SYSTEM'_def)
  apply (rule_tac P=‹λ a b c. a ⊑_FD ((SEND' [SYN] REC') \ SYN)› in COPY'_SEND'_REC'.induct)
    apply (subst case_prod_beta')+
    apply (intro le_FD_adm, simp_all add: monofunI)
  apply (subst SEND'_rec, subst REC'_rec)
  by (simp add: Sync_rules Hiding_rules mono_read_FD mono_write_FD)

lemma spec_refines_impl' : 
  assumes fin:  "finite (SYN::'a channel set)"
  shows         "SYSTEM' ⊑_FD (COPY'::'a channel process)"
proof(unfold SYSTEM'_def, rule_tac P=‹λ a b c. ((b [SYN] REC') \ SYN) ⊑_FD COPY'›
    in  COPY'_SEND'_REC'.induct, goal_cases)
  case 1
  have aa:‹adm (λ(a::'a channel process). ((a [SYN] REC') \ SYN) ⊑_FD COPY')›
    apply (intro le_FD_adm)
    by (simp_all add: fin cont2mono)
  thus ?case using adm_subst[of "λ(a,b,c). b", simplified, OF aa] by (simp add: split_def)
next
  case 2
  then show ?case by (simp add: Sync_commute)
next
  case (3 a aa b)
  then show ?case 
    by (subst COPY'_rec, subst REC'_rec)
      (simp add: Sync_rules Hiding_rules mono_read_FD mono_write_FD)
qed

lemma spec_equal_impl' : 
  assumes fin:  "finite (SYN::('a channel)set)"
  shows         "SYSTEM' = (COPY'::'a channel process)"
  apply (rule FD_antisym)
   apply (rule spec_refines_impl'[OF fin])
  apply (rule impl_refines_spec'')
  done



subsection‹Proof-techniques over alphabets of processes:›

text‹An elementary proof technique to determine the alphabet ‹α(P)› of a process ‹P› (which is
  general a true subset of the set of possible events ‹Σ›) is based on a noetherian induction
  over the length of lists:›

lemma alphabet_of_COPY : ‹α(COPY::('α channel) process) = range left ∪ range right›
proof(intro equalityI)
  show "α(COPY::('α channel) process) ⊆ range left ∪ range right" 
  proof -
    have * : "size t ≤ n ==> t ∈ T COPY ==> x ∉ range right ==> ev x ∈ set t ==> x ∈ range left"  
      for n::nat and x::‹'α channel› and t:: ‹'α channel trace›
      proof(induct n  arbitrary : x t)
        case 0
        then show ?case by simp 
      next
        case (Suc n)
        then show ?case
        proof -
          assume 1 : ‹t ∈ T COPY›
          have  ** : ‹t ∈ T (left?x → right!x → COPY)› by (metis COPY_rec Suc.prems(2))
          assume 2 : ‹x ∉ range right›
          assume 3 : ‹ev x ∈ set t›
          show       ‹x ∈ range left›
            apply(insert **) 
            apply(subst (asm) T_read_inj_on, meson channel.inject(1) injI)
            apply(auto) using 3 apply force
            apply(subst (asm) T_write, auto) 
            using 3 apply auto[1] 
            by (metis Suc.hyps Suc.prems(1) 2 3 Suc_leD Suc_le_mono event_ptick.inject(1) 
                      insertE length_Cons list.simps(15) range_eqI)
        qed
      qed
    show ?thesis
      unfolding events_of_def 
      using * by blast
  qed
next
  show "range left ∪ range right ⊆ α(COPY::('α channel) process)"
  proof - 
    have * : " ∃x∈T (COPY::('α channel) process). ev (left xa) ∈ set x" for xa
               apply(subst COPY_rec) 
               by (metis (mono_tags, lifting) Mprefix_projs(3) Nil_elem_T insert_iff 
                         list.simps(15) mem_Collect_eq rangeI  read_def)
    have **: " ∃x∈T (COPY::('α channel) process). ev (right xa) ∈ set x" for xa
               apply(subst COPY_rec) 
               apply(subst T_read_inj_on,meson channel.inject(1) injI)
               by (metis (mono_tags, lifting) T_write UNIV_I insert_iff 
                          is_processT1_TR list.simps(15) mem_Collect_eq)
   show ?thesis
     unfolding events_of_def using * ** by auto
  qed   
qed

text‹ A more advanced technique promising a higher degree of automation is requiring a
  space argument, which is not yet at our disposition here. ›

section‹More on CopyBuffer›

text‹The CopyBuffer is a running example in the HOL-CSP theory and will be reused as a demonstrator
  various contexts, be it in proofs or model-checking. With respect to the former, the reader is
  to the session ▩‹CSP_RefTK› where specific support for deadlock and lifelock refinement
  is developed, such that goals of the form:

 {theory_text [indent=10,margin=70]
 ‹corollary df_COPY: "deadlock_free COPY"
 and lf_COPY: "lifelock_free COPY"›}

  be solved with a reasonable degree of automation.

  respect to model-checking, the reader is referred to the session ▩‹FDR› where techniques for
  model-checking of HOL-CSP processes is introduced.
 ›



(*<*)
end
(*>*)