Theory Hiding_Destructive

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Destructiveness of Hiding›

(*<*)
theory Hiding_Destructive
  imports "HOL-CSPM" Prefixes_Constructive
begin
(*>*)


subsection ‹Refinement›

lemma Hiding_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_FD : ‹(P ↓ n) \ S ⊑⇩_F⇩_D P \ S ↓ n›
proof (unfold refine_defs, safe)
  show * : ‹t ∈ 𝒟 (P \ S ↓ n) ⟹ t ∈ 𝒟 ((P ↓ n) \ S)› for t
  proof (elim D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kE)
    show ‹t ∈ 𝒟 (P \ S) ⟹ t ∈ 𝒟 ((P ↓ n) \ S)›
      by (simp add: D_Hiding restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_projs) blast
  next
    fix u v
    assume ‹t = u @ v› ‹u ∈ 𝒯 (P \ S)› ‹length u = n› ‹tF u› ‹ftF v›
    from ‹u ∈ 𝒯 (P \ S)›[simplified T_Hiding, simplified]
    consider ‹u ∈ 𝒟 (P \ S)› | u' where ‹u = trace_hide u' (ev ` S)› ‹(u', ev ` S) ∈ ℱ P›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹t ∈ 𝒟 ((P ↓ n) \ S)›
    proof cases
      assume ‹u ∈ 𝒟 (P \ S)›
      hence ‹t ∈ 𝒟 (P \ S)› by (simp add: ‹ftF v› ‹t = u @ v› ‹tF u› is_processT7)
      with restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_approx_self le_approx1 mono_Hiding
      show ‹t ∈ 𝒟 ((P ↓ n) \ S)› by blast
    next
      fix u' assume ‹u = trace_hide u' (ev ` S)› ‹(u', ev ` S) ∈ ℱ P›
      with ‹length u = n› ‹tF u› Hiding_tickFree length_filter_le F_T
      have ‹n ≤ length u'› ‹tickFree u'› ‹u' ∈ 𝒯 P› by blast+
      with ‹u = trace_hide u' (ev ` S)›
      have ‹u' = (take n u') @ (drop n u') ∧ take n u' ∈ 𝒯 P ∧
            length (take n u') = n ∧ tF (take n u') ∧ ftF (drop n u')›
        by (simp add: min_def) (metis append_take_drop_id is_processT3_TR_append
            tickFree_append_iff tickFree_imp_front_tickFree)
      with D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k have ‹u' ∈ 𝒟 (P ↓ n)› by blast
      with Hiding_tickFree ‹ftF v› ‹t = u @ v› ‹u = trace_hide u' (ev ` S)› ‹tF u›
      show ‹t ∈ 𝒟 ((P ↓ n) \ S)› by (simp add: D_Hiding) blast
    qed
  qed

  fix s X
  assume ‹(s, X) ∈ ℱ ((P \ S) ↓ n)›
  then consider ‹s ∈ 𝒟 ((P \ S) ↓ n)› | ‹(s, X) ∈ ℱ (P \ S)›
    unfolding restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
  thus ‹(s, X) ∈ ℱ ((P ↓ n) \ S)›
  proof cases
    from "*" D_F show ‹s ∈ 𝒟 ((P \ S) ↓ n) ⟹ (s, X) ∈ ℱ ((P ↓ n) \ S)› by blast
  next
    show ‹(s, X) ∈ ℱ (P \ S) ⟹ (s, X) ∈ ℱ ((P ↓ n) \ S)›
      using restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_approx_self D_F mono_Hiding proc_ord2a by blast
  qed
qed


subsection ‹Destructiveness›

lemma Hiding_destructive :
  ‹∃P Q :: ('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k. P ↓ n = Q ↓ n ∧ (P \ S) ↓ Suc 0 ≠ (Q \ S) ↓ Suc 0› if ‹S ≠ {}›
proof -
  from ‹S ≠ {}› obtain e where ‹e ∈ S› by blast
  define P :: ‹('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹P ≡ iterate (Suc n)⋅(Λ X. write0 e X)⋅(SKIP undefined)›
  define Q :: ‹('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k› where ‹Q ≡ iterate (Suc n)⋅(Λ X. write0 e X)⋅STOP›
  have ‹P ↓ n = Q ↓ n›
    unfolding P_def Q_def by (induct n) (simp_all add: restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_write0) 
  have ‹P \ S = SKIP undefined›
    unfolding P_def by (induct n) (simp_all add: Hiding_write0_non_disjoint ‹e ∈ S›)
  hence ‹(P \ S) ↓ Suc 0 = SKIP undefined› by simp
  have ‹Q \ S = STOP›
    unfolding Q_def by (induct n) (simp_all add: Hiding_write0_non_disjoint ‹e ∈ S›)
  hence ‹(Q \ S) ↓ Suc 0 = STOP› by simp

  have ‹P ↓ n = Q ↓ n ∧ (P \ S) ↓ Suc 0 ≠ (Q \ S) ↓ Suc 0›
    by (simp add: ‹P ↓ n = Q ↓ n› ‹(P \ S) ↓ Suc 0 = SKIP undefined›
        ‹(Q \ S) ↓ Suc 0 = STOP›)
  thus ?thesis by blast
qed



(*<*)
end
  (*>*)