Theory CopyBuffer-fixrec

(*<*)
―‹ ********************************************************************
 * 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       : An experimental Version of the Copy Buffer Example
 *
 * 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-fixrec" 
  imports   "HOL-CSP"
begin 
(*>*)

text‹ This file contains a version of the classical CopyBuffer Example
      with a (discouraged) use of the HOLCF - fixrec package. ›

section‹ Defining Channels and Rewrite-sets of Events›

text‹Note: This Approach is DISCOURAGED.›

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

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


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)

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


section‹ Process Definitions via HOLCF - 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)›

section‹ 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) ⊑⇩F⇩D SYSTEM"
  apply (unfold SYSTEM_def)
  apply (rule_tac P=‹λ a b c. a ⊑⇩F⇩D ((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 ⊑⇩F⇩D (COPY::'a channel process)"
proof(unfold SYSTEM_def, rule_tac P=‹λ a b c. ((b ⟦SYN⟧ REC) \ SYN) ⊑⇩F⇩D COPY› 
    in  COPY_SEND_REC.induct, goal_cases)
  case 1
  have aa:‹adm (λ(a::'a channel process). ((a ⟦SYN⟧ REC) \ SYN) ⊑⇩F⇩D 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


(*<*)
end
(*>*)