Theory Choices_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 Choices›

(*<*)
theory Choices_Non_Destructive
  imports Process_Restriction_Space "HOL-CSPM.CSPM_Laws"
begin
  (*>*)


subsection ‹Equality›

lemma restriction_processptick_Ndet : ‹P ⊓ Q ↓ n = (P ↓ n) ⊓ (Q ↓ n)›
  by (auto simp add: Process_eq_spec Ndet_projs restriction_processptick_projs)

lemma restriction_processptick_GlobalNdet :
  ‹(⊓a ∈ A. P a) ↓ n = (if n = 0 then ⊥ else ⊓a ∈ A. (P a ↓ n))›
  by simp (auto simp add: Process_eq_spec GlobalNdet_projs restriction_processptick_projs)


lemma restriction_processptick_GlobalDet :
  ‹(□a ∈ A. P a) ↓ n = (if n = 0 then ⊥ else □a ∈ A. (P a ↓ n))›
  (is ‹?lhs = (if n = 0 then ⊥ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹n = 0 ⟹ ?lhs = ⊥› by simp
next
  show ‹?lhs = ?rhs› if ‹n ≠ 0›
  proof (rule Process_eq_optimized_bisI)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (auto simp add: GlobalDet_projs D_restriction_processptick ‹n ≠ 0› split: if_split_asm)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (auto simp add: GlobalDet_projs D_restriction_processptick)
  next
    show ‹([], X) ∈ ℱ ?lhs ⟹ ([], X) ∈ ℱ ?rhs› for X
      by (auto simp add: restriction_processptick_projs F_GlobalDet)
  next
    show ‹([], X) ∈ ℱ ?rhs ⟹ ([], X) ∈ ℱ ?lhs› for X
      by (auto simp add: restriction_processptick_projs F_GlobalDet)
        (metis append_eq_Cons_conv eventptick.disc(2) tickFree_Cons_iff)
  next
    show ‹(e # t, X) ∈ ℱ ?lhs ⟹ (e # t, X) ∈ ℱ ?rhs› for e t X
      by (auto simp add: ‹n ≠ 0› F_restriction_processptick GlobalDet_projs split: if_split_asm)
  next
    show ‹(e # t, X) ∈ ℱ ?rhs ⟹ (e # t, X) ∈ ℱ ?lhs› for e t X
      by (auto simp add: F_restriction_processptick GlobalDet_projs)
  qed
qed


lemma restriction_processptick_Det: ‹P □ Q ↓ n = (P ↓ n) □ (Q ↓ n)› (is ‹?lhs = ?rhs›)
proof -
  have ‹P □ Q ↓ n = □i ∈ {0, 1 :: nat}. (if i = 0 then P else Q) ↓ n›
    by (simp add: GlobalDet_distrib_unit_bis)
  also have ‹… = (if n = 0 then ⊥ else □i ∈ {0, 1 :: nat}. (if i = 0 then P ↓ n else Q ↓ n))›
    by (simp add: restriction_processptick_GlobalDet if_distrib if_distribR)
  also have ‹… = (P ↓ n) □ (Q ↓ n)› by (simp add: GlobalDet_distrib_unit_bis)
  finally show ‹P □ Q ↓ n = (P ↓ n) □ (Q ↓ n)› .
qed


corollary restriction_processptick_Sliding: ‹P ⊳ Q ↓ n = (P ↓ n) ⊳ (Q ↓ n)›
  by (simp add: restriction_processptick_Det restriction_processptick_Ndet Sliding_def)




subsection ‹Non Destructiveness›

lemma GlobalNdet_non_destructive : ‹non_destructive (λP. ⊓a ∈ A. P a)›
  by (auto intro: non_destructiveI
      simp add: restriction_processptick_GlobalNdet restriction_fun_def)

lemma Ndet_non_destructive : ‹non_destructive (λ(P, Q). P ⊓ Q)›
  by (auto intro: non_destructiveI
      simp add: restriction_processptick_Ndet restriction_prod_def)

lemma GlobalDet_non_destructive : ‹non_destructive (λP. □a ∈ A. P a)›
  by (auto intro: non_destructiveI
      simp add: restriction_processptick_GlobalDet restriction_fun_def)

lemma Det_non_destructive : ‹non_destructive (λ(P, Q). P □ Q)›
  by (auto intro: non_destructiveI
      simp add: restriction_processptick_Det restriction_prod_def)

corollary Sliding_non_destructive : ‹non_destructive (λ(P, Q). P ⊳ Q)›
  by (auto intro: non_destructiveI
      simp add: restriction_processptick_Sliding restriction_prod_def)


(*<*)
end
  (*>*)