Theory Renaming_Non_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 ‹Non Destructiveness of Renaming›

(*<*)
theory Renaming_Non_Destructive
  imports Process_Restriction_Space "HOL-CSPM"
begin
  (*>*)


subsection ‹Equality›

lemma restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_Renaming:
  ‹Renaming P f g ↓ n = Renaming (P ↓ n) f g› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: Renaming_projs D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k)
      (metis append.right_neutral front_tickFree_Nil map_event⇩_p⇩_t⇩_i⇩_c⇩_k_tickFree,
        use front_tickFree_append in blast)
next
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (auto simp add: Renaming_projs D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k
        front_tickFree_append map_event⇩_p⇩_t⇩_i⇩_c⇩_k_tickFree)
next
  fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
  then obtain u where ‹(u, map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g -` X) ∈ ℱ P› ‹t = map (map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g) u›
    by (simp add: Renaming_projs restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_projs) blast
  thus ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: F_Renaming F_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k)
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  then obtain u where ‹(u, map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g -` X) ∈ ℱ (P ↓ n)› ‹t = map (map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g) u›
    unfolding Renaming_projs by blast
  from ‹(u, map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g -` X) ∈ ℱ (P ↓ n)›
  consider ‹u ∈ 𝒟 (P ↓ n)› | ‹(u, map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g -` X) ∈ ℱ P›
    unfolding restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    assume ‹u ∈ 𝒟 (P ↓ n)›
    hence ‹t ∈ 𝒟 ?rhs›
    proof (elim D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kE)
      from ‹t = map (map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g) u› show ‹u ∈ 𝒟 P ⟹ t ∈ 𝒟 ?rhs›
        by (cases ‹tF u›, simp_all add: D_Renaming D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k)
          (use front_tickFree_Nil in blast,
            metis D_imp_front_tickFree butlast_snoc div_butlast_when_non_tickFree_iff
            front_tickFree_iff_tickFree_butlast front_tickFree_single map_append
            map_event⇩_p⇩_t⇩_i⇩_c⇩_k_front_tickFree nonTickFree_n_frontTickFree)
    next
      show ‹⟦u = v @ w; v ∈ 𝒯 P; length v = n; tF v; ftF w⟧ ⟹ t ∈ 𝒟 ?rhs› for v w
        by (simp add: D_Renaming D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k ‹t = map (map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g) u›)
          (use front_tickFree_Nil map_event⇩_p⇩_t⇩_i⇩_c⇩_k_front_tickFree in blast)
    qed
    with ‹t ∉ 𝒟 ?rhs› have False ..
    thus ‹(t, X) ∈ ℱ ?lhs› ..
  next
    show ‹(u, map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g -` X) ∈ ℱ P ⟹ (t, X) ∈ ℱ (Renaming P f g ↓ n)›
      by (auto simp add: F_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k F_Renaming ‹t = map (map_event⇩_p⇩_t⇩_i⇩_c⇩_k f g) u›)
  qed
qed



subsection ‹Non Destructiveness›

lemma Renaming_non_destructive [simp] :
  ‹non_destructive (λP. Renaming P f g)›
  by (auto intro: non_destructiveI simp add: restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_Renaming)


(*<*)
end
  (*>*)