(*<*)
―‹ ********************************************************************
 * 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: A Note on a Classical Example: The ``Merge Anomaly''›

theory MergeAnomaly
  imports "HOL-CSP"
begin

text‹Manfred Broy proposed in his 'Habilitationsschrift' (🚫‹Published in
 `A Theory for Nondeterminism, Parallelism, Communication, and Concurrency. TCS (1986)''›)
  stream processing language ‹AMPL›, which is in many respect similar to 🚫‹HOL-CSP›.
 , the underlying Powerset-construction contained a error that made it possible
  in an interleaving between a stream ‹1^\∞› and a stream ‹1.0^\∞› a ‹0› can get ahead of the
  ‹1› which contradicts the intuition that interleaving should preserve causality in
  inputs.

  we believe in the importance of a ∗‹formally verified› semantics of a language for
 , we take this anecdotical reference to the Merge-Anomaly as an example to
  in the process algebra 🚫‹HOL-CSP›, so in a setting with trace, failure and
 /divergence semantics.

 , we define the three processes corresponding to the notation ‹1^\∞›, ‹0^\∞› and ‹1.0^\∞›:
 ›

definition ones      :: "nat process" where ‹ones = (μ X. 1 → X)›
definition zeros     :: "nat process" where ‹zeros = (μ X. 0 → X)›
definition oneszeros :: "nat process" where ‹oneszeros = (μ X. ◻x∈{0,1} → X)›

text‹... and derive the more handy recursive stream-equations:›

lemma ones_rec: "ones = 1 → ones"  by (subst cont_process_rec[OF ones_def]) simp_all

lemma zeros_rec: "zeros = 0 → zeros" by (subst cont_process_rec[OF zeros_def]) simp_all

lemma oneszeros_rec: "oneszeros = ◻x∈{0,1} → oneszeros" 
      by (subst cont_process_rec[OF oneszeros_def]) simp_all

text‹Now, we can establish that ‹ones ||| zeros› and ‹oneszeros› are indeed equal
  the failure/divergence semantics in 🚫‹HOL-CSP›. This is formally proven as follows: ›

lemma ones_Inter_zeros_eq_oneszeros : ‹ones ||| zeros = oneszeros›
proof (rule FD_antisym)
  show ‹oneszeros ⊑_FD ones ||| zeros›
  proof (unfold oneszeros_def, induct rule: cont_fix_ind)
    fix X assume ‹X ⊑_FD ones ||| zeros›
    have ‹ones ||| zeros = (1 → (ones ||| 0 → zeros)) ◻ (0 → (1 → ones ||| zeros))›
      by (subst ones_rec, subst zeros_rec) (simp add: write0_Inter_write0)
    also have ‹… = (1 → (ones ||| zeros)) ◻ (0 → (ones ||| zeros))›
      by (simp del: One_nat_def flip: ones_rec zeros_rec)
    also have ‹… = ◻a∈{0, 1} → (ones ||| zeros)›
      by (metis Mprefix_Un_distrib Mprefix_singl Un_insert_right sup_bot.right_neutral)
    also have ‹◻a∈{0, 1} → X ⊑_FD …›
      by (simp add: ‹X ⊑_FD ones ||| zeros› mono_Mprefix_FD)
    finally show ‹◻a∈{0, 1} → X ⊑_FD ones ||| zeros› .
  qed simp_all
next
  show ‹ones ||| zeros ⊑_FD oneszeros›
    ― ‹With stronger theoretical footprint, this could be skipped since const‹oneszeros›
 is a deterministic process (therefore maximal for term‹(⊑_FD)›).›
  proof (unfold ones_def zeros_def, induct rule: parallel_fix_ind_inc)
    fix X Y
    assume hyps : ‹(Λ X. 1 → X)⋅X ||| Y ⊑_FD oneszeros›
                  ‹X ||| (Λ Y. 0 → Y)⋅Y ⊑_FD oneszeros›
    have ‹(Λ X. 1 → X)⋅X ||| (Λ Y. 0 → Y)⋅Y = (1 → X) ||| (0 → Y)› by simp
    also have ‹… = (1 → (X ||| 0 → Y)) ◻ (0 → (1 → X ||| Y))›
      by (simp add: write0_Inter_write0)
    also have ‹… = ◻a ∈ {0, 1} → (if a = 0 then 1 → X ||| Y else X ||| 0 → Y)›
      by (auto simp add: write0_def Mprefix_Det_Mprefix intro: mono_Mprefix_eq)
    also have ‹… ⊑_FD oneszeros›
      by (subst oneszeros_rec)
        (use hyps in ‹auto intro: mono_Mprefix_FD›)
    finally show ‹(Λ X. 1 → X)⋅X ||| (Λ Y. 0 → Y)⋅Y ⊑_FD oneszeros› .
  qed simp_all
qed

text‹As a consequence, in the trace model, we can establish that there will be no ``Anomaly''
  🚫‹HOL-CSP›, so ‹ones ||| (1 → zeros)› will be equal to ‹1 → oneszeros› in the
  intended trace-projection. The proof proceeds indirectly over induction over the traces;
  is the recommended proof strategy if arguments over trace sets have to be established. In
 , an argument over the term‹lfp›-operator, which seems natural at first sight, is amazingly
 . We have:›

lemma ‹T (ones ||| (1 → zeros)) = T (1 → oneszeros)› (is ‹?lhs = ?rhs›)
proof (rule set_eqI)
  show ‹t ∈ ?lhs ⟷ t ∈ ?rhs› for t
  proof (induct t)
    case Nil show ?case by simp
  next
    case (Cons e t)
    show ?case
    proof (rule iffI)
      assume ‹e # t ∈ T (1 → oneszeros)›
      hence ‹e = ev 1› ‹t ∈ T oneszeros›
        by (simp_all add: T_write0)
      thus ‹e # t ∈ T (ones ||| 1 → zeros)›
        apply (subst ones_rec)
        apply (simp del: One_nat_def add: write0_Inter_write0 T_Det T_write0)
        apply (fold ones_rec ones_Inter_zeros_eq_oneszeros)
        ..
    next
      show ‹e # t ∈ T (ones ||| 1 → zeros) ==> e # t ∈ T (1 → oneszeros)›
        apply (subst (asm) ones_rec)
        apply (simp del: One_nat_def add: write0_Inter_write0 T_Det T_write0)
        apply (fold ones_rec)
        apply (unfold Cons.hyps)
        apply (unfold ones_Inter_zeros_eq_oneszeros)
        apply (subst (asm) (2) oneszeros_rec, subst oneszeros_rec)
        by (auto simp add: T_Mprefix T_write0)
    qed
  qed
qed


text‹However, ‹ones ||| (1 → zeros)› will be ∗‹not› equal to ‹1 → oneszeros› in the failure
  and therefore not in the failure/divergence model. The deeper reason is the interleave
  ∗‹can neither refuse› ‹0› or ‹1›; it is designed to be sensitive to the process
  and let pass any possible interleaving admitted by the context which is reflected
  the rule @{thm Read_Write_CSP_Laws.write0_Inter_write0}.›


lemma ‹ones ||| (1 → zeros) ≠ 1 → oneszeros› (is ‹?P1 ≠ ?P2›) 
proof -
  have ‹([ev 1], {ev 0}) ∉ F ?P2›
    by (subst oneszeros_rec)
      (simp add: Process_eq_spec F_write0 F_Mprefix)
  moreover have ‹([ev 1], {ev 0}) ∈ F ?P1›
    by (subst ones_rec, subst ones_rec)
      (simp add: write0_Inter_write0 Process_eq_spec F_Det F_write0)
  ultimately show ‹?P1 ≠ ?P2› by metis
qed

text‹One might ask what happens if we would have defined the process const‹oneszeros› via the
 -deterministic choice, so using the following definition:›

definition oneszeros' :: "nat process" where ‹oneszeros' = (μ X. ⊓x∈{0,1} → X)›

lemma oneszeros'_rec : ‹oneszeros' = ⊓x ∈ {0, 1} → oneszeros'›
  by (subst cont_process_rec[OF oneszeros'_def]) simp_all

text‹But this means that already the first step in the above argument breaks down:
  interleaving ∗‹can neither refuse› ‹0› or ‹1›, while the deterministic choice of
 const‹oneszeros'› does, we can easily show:›

lemma ‹ones ||| zeros ≠ oneszeros'›
proof (rule notI)
  assume ‹ones ||| zeros = oneszeros'›
  with ones_Inter_zeros_eq_oneszeros have ‹oneszeros' = oneszeros› by metis
  moreover have ‹([], {ev 0}) ∈ F oneszeros'›
    by (subst oneszeros'_rec)
      (simp add: F_Mndetprefix')
  moreover have ‹([], {ev 0}) ∉ F oneszeros›
    by (subst oneszeros_rec) (simp add: F_Mprefix)
  ultimately show False by simp
qed



end