Theory CopyBuffer

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : A Combined CSP Theory
 *
 * Copyright (c) 2009 Université Paris-Sud, 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: Refinement Example with Buffer over infinite Alphabet›

theory     CopyBuffer 
 imports   CSP "Assertions"
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 [simp]: "left x    SYN"
    by(auto simp: SYN_def)
  
lemma [simp]: "right x    SYN"
    by(auto simp: SYN_def)

lemma [simp]: "ack  SYN"
    by(auto simp: SYN_def)

lemma [simp]: "mid x  SYN"
    by(auto simp: SYN_def)

lemma [simp]: "inj mid"  
  by(auto simp: 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‹ A Refinement Proof ›

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. ›

lemma impl_refines_spec : "COPY FD SYSTEM"
  apply(simp add: SYSTEM_def COPY_def)
  apply(rule fix_ind, simp_all)
  apply (intro le_FD_adm, simp_all add: cont_fun monofunI)
  apply (subst SEND_rec, subst REC_rec)
  by (simp add: Sync_rules Hiding_rules)
  

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: Hiding_set_BOT Sync_BOT Sync_commute)
  apply (subst COPY_rec, subst REC_rec)
  by (simp add: Sync_rules Hiding_rules)

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
case 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 (rule mono_Mndetprefix_FD_set, simp, blast) 
  have 2: "(xa range left   )  FD (left?x   )" 
    unfolding read_def
    by (meson Mprefix_refines_Mndetprefix_FD BOT_leFD mono_Mndetprefix_FD trans_FD)
  show "(Λ x. xarange 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. xarange left  range right   x)P FD COPY"
  have 1:"(xa range left  range right   P) FD (xa range right   P)"
    by (rule mono_Mndetprefix_FD_set, simp, blast)
  have 2:"(xa range right   P) FD (right!x   P)" for x
    apply (unfold write_def, rule trans_FD[OF mono_Mndetprefix_FD_set[of {right x} range right]])
    by simp_all
  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
  have 4:"X. (xa range left  range right  X) FD (xa range left  X)"
    by (rule mono_Mndetprefix_FD_set, simp, blast) 
  have 5:"X. (xa range left  X) FD (left?x  X)"
    by (unfold read_def, subst K_record_comp, fact Mprefix_refines_Mndetprefix_FD)
  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
                        
  show "(Λ x. xarange left  range right   x)
             ((Λ x. xarange 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)

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: Hiding_set_BOT Sync_BOT Sync_commute)
next
  case (3 a aa b)
  then show ?case 
    apply (subst COPY'_rec, subst REC'_rec)
    by (simp add: Sync_rules Hiding_rules)
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