Theory HOL-CSP_RS

(***********************************************************************************
 * 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 ‹Higher-Order Rules›

(*<*)
theory "HOL-CSP_RS"
  imports
    Prefixes_Constructive
    Choices_Non_Destructive
    Renaming_Non_Destructive
    Sequential_Composition_Non_Destructive
    Synchronization_Product_Non_Destructive
    Throw_Non_Destructive
    Interrupt_Non_Destructive
    Hiding_Destructive
    CSP_Restriction_Adm
begin
  (*>*)

text ‹This is the main entry point. We configure the simplifier below.›


named_theorems restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset

subsection ‹Prefixes›

lemma Mprefix_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹constructive (λx. □a ∈ A → f a x)› if ‹(⋀a. a ∈ A ⟹ non_destructive (f a))›
proof -
  have * : ‹□a ∈ A → f a x = □a ∈ A → (if a ∈ A then f a x else STOP)› for x
    by (auto intro: mono_Mprefix_eq)
  show ‹constructive (λx. □a ∈ A → f a x)›
    by (subst "*", rule constructive_comp_non_destructive
        [OF Mprefix_constructive, of ‹λx a. if a ∈ A then f a x else STOP›])
      (auto intro: that)
qed

lemma Mndetprefix_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹constructive (λx. ⊓a ∈ A → f a x)› if ‹(⋀a. a ∈ A ⟹ non_destructive (f a))›
proof -
  have * : ‹⊓a ∈ A → f a x = ⊓a ∈ A → (if a ∈ A then f a x else STOP)› for x
    by (auto intro: mono_Mndetprefix_eq)
  show ‹constructive (λx. ⊓a ∈ A → f a x)›
    by (subst "*", rule constructive_comp_non_destructive
        [OF Mndetprefix_constructive, of ‹λx a. if a ∈ A then f a x else STOP›])
      (auto intro: that)
qed

corollary write0_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ constructive (λx. a → f x)›
  by (simp add: write0_def Mprefix_restriction_shift_process⇩p⇩t⇩i⇩c⇩k)

corollary write_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ constructive (λx. c❙!a → f x)›
  by (simp add: write_def Mprefix_restriction_shift_process⇩p⇩t⇩i⇩c⇩k)

corollary read_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹(⋀a. a ∈ A ⟹ non_destructive (f a)) ⟹ constructive (λx. c❙?a ∈ A → f a x)›
  by (simp add: read_def Mprefix_restriction_shift_process⇩p⇩t⇩i⇩c⇩k inv_into_into)

corollary ndet_write_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹(⋀a. a ∈ A ⟹ non_destructive (f a)) ⟹ constructive (λx. c❙!❙!a ∈ A → f a x)›
  by (simp add: ndet_write_def Mndetprefix_restriction_shift_process⇩p⇩t⇩i⇩c⇩k inv_into_into)


subsection ‹Choices›

lemma GlobalNdet_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹(⋀a. a ∈ A ⟹ non_destructive (f a)) ⟹ non_destructive (λx. ⊓a ∈ A. f a x)›
  ‹(⋀a. a ∈ A ⟹ constructive (f a)) ⟹ constructive (λx. ⊓a ∈ A. f a x)›
proof -
  have * : ‹⊓a ∈ A. f a x = ⊓a ∈ A. (if a ∈ A then f a x else STOP)› for x
    by (auto intro: mono_GlobalNdet_eq)

  show ‹(⋀a. a ∈ A ⟹ non_destructive (f a)) ⟹ non_destructive (λx. ⊓a ∈ A. f a x)›
    by (subst "*", rule non_destructive_comp_non_destructive
        [OF GlobalNdet_non_destructive, of ‹λx a. if a ∈ A then f a x else STOP›]) auto

  show ‹(⋀a. a ∈ A ⟹ constructive (f a)) ⟹ constructive (λx. ⊓a ∈ A. f a x)›
    by (subst "*", rule non_destructive_comp_constructive
        [OF GlobalNdet_non_destructive, of ‹λx a. if a ∈ A then f a x else STOP›]) auto
qed

lemma GlobalDet_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹(⋀a. a ∈ A ⟹ non_destructive (f a)) ⟹ non_destructive (λx. □a ∈ A. f a x)›
  ‹(⋀a. a ∈ A ⟹ constructive (f a)) ⟹ constructive (λx. □a ∈ A. f a x)›
proof -
  have * : ‹□a ∈ A. f a x = □a ∈ A. (if a ∈ A then f a x else STOP)› for x
    by (auto intro: mono_GlobalDet_eq)

  show ‹(⋀a. a ∈ A ⟹ non_destructive (f a)) ⟹ non_destructive (λx. □a ∈ A. f a x)›
    by (subst "*", rule non_destructive_comp_non_destructive
        [OF GlobalDet_non_destructive, of ‹λx a. if a ∈ A then f a x else STOP›]) auto

  show ‹(⋀a. a ∈ A ⟹ constructive (f a)) ⟹ constructive (λx. □a ∈ A. f a x)›
    by (subst "*", rule non_destructive_comp_constructive
        [OF GlobalDet_non_destructive, of ‹λx a. if a ∈ A then f a x else STOP›]) auto
qed


lemma Ndet_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ⊓ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ⊓ g x)›
  by (auto intro!: non_destructiveI constructiveI
      simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Ndet dest!: non_destructiveD constructiveD)

lemma Det_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x □ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x □ g x)›
  by (auto intro!: non_destructiveI constructiveI
      simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Det dest!: non_destructiveD constructiveD)

lemma Sliding_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ⊳ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ⊳ g x)›
  by (auto intro!: non_destructiveI constructiveI
      simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Sliding dest!: non_destructiveD constructiveD)


subsection ‹Renaming›

lemma Renaming_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive P ⟹ non_destructive (λx. Renaming (P x) f g)›
  ‹constructive P ⟹ constructive (λx. Renaming (P x) f g)›
  by (auto intro!: non_destructiveI constructiveI
      simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Renaming dest!: non_destructiveD constructiveD)


subsection ‹Sequential Composition›

lemma Seq_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ❙; g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ❙; g x)›
  by (fact non_destructive_comp_non_destructive[OF Seq_non_destructive non_destructive_prod_codomain, simplified])
    (fact non_destructive_comp_constructive[OF Seq_non_destructive constructive_prod_codomain, simplified])


lemma MultiSeq_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹(⋀l. l ∈ set L ⟹ non_destructive (f l)) ⟹ non_destructive (λx. SEQ l ∈@ L. f l x)›
  ‹(⋀l. l ∈ set L ⟹ constructive (f l)) ⟹ constructive (λx. SEQ l ∈@ L. f l x)›
  by (induct L rule: rev_induct; simp add: Seq_restriction_shift_process⇩p⇩t⇩i⇩c⇩k)+


corollary MultiSeq_non_destructive : ‹non_destructive (λP. SEQ l ∈@ L. P l)›
  by (simp add: MultiSeq_restriction_shift_process⇩p⇩t⇩i⇩c⇩k(1)[of L ‹λl x. x l›])



subsection ‹Synchronization Product›

lemma Sync_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ⟦S⟧ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ⟦S⟧ g x)›
  by (fact non_destructive_comp_non_destructive[OF Sync_non_destructive non_destructive_prod_codomain, simplified])
    (fact non_destructive_comp_constructive[OF Sync_non_destructive constructive_prod_codomain, simplified])


lemma MultiSync_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹(⋀m. m ∈# M ⟹ non_destructive (f m)) ⟹ non_destructive (λx. ❙⟦S❙⟧ m ∈# M. f m x)›
  ‹(⋀m. m ∈# M ⟹ constructive (f m)) ⟹ constructive (λx. ❙⟦S❙⟧ m ∈# M. f m x)›
  by (induct M rule: induct_subset_mset_empty_single;
      simp add: Sync_restriction_shift_process⇩p⇩t⇩i⇩c⇩k)+


corollary MultiSync_non_destructive : ‹non_destructive (λP. ❙⟦S❙⟧ m ∈# M. P m)›
  by (rule MultiSync_restriction_shift_process⇩p⇩t⇩i⇩c⇩k(1)[of M ‹λm x. x m›]) simp



subsection ‹Throw›

lemma Throw_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ (⋀a. a ∈ A ⟹ non_destructive (g a)) ⟹ non_destructive (λx. f x Θ a ∈ A. g a x)›
  ‹constructive f ⟹ (⋀a. a ∈ A ⟹ constructive (g a)) ⟹ constructive (λx. f x Θ a ∈ A. g a x)›
proof -
  have * : ‹f x Θ a ∈ A. g a x = f x Θ a ∈ A. (if a ∈ A then g a x else STOP)› for x
    by (auto intro: mono_Throw_eq)

  show ‹non_destructive f ⟹ (⋀a. a ∈ A ⟹ non_destructive (g a)) ⟹ non_destructive (λx. f x Θ a ∈ A. g a x)›
    by (subst "*", erule non_destructive_comp_non_destructive
        [OF Throw_non_destructive non_destructive_prod_codomain, simplified]) auto

  show ‹constructive f ⟹ (⋀a. a ∈ A ⟹ constructive (g a)) ⟹ constructive (λx. f x Θ a ∈ A. g a x)›
    by (subst "*", erule non_destructive_comp_constructive
        [OF Throw_non_destructive constructive_prod_codomain, simplified]) auto
qed



subsection ‹Interrupt›

lemma Interrupt_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x △ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x △ g x)›
  by (fact non_destructive_comp_non_destructive[OF Interrupt_non_destructive non_destructive_prod_codomain, simplified])
    (fact non_destructive_comp_constructive[OF Interrupt_non_destructive constructive_prod_codomain, simplified])



subsection ‹After›

lemma (in After) After_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹non_too_destructive Ψ ⟹ constructive f ⟹ non_destructive (λx. f x  after a)›
  ‹non_too_destructive Ψ ⟹ non_destructive f ⟹ non_too_destructive (λx. f x  after a)›
  by (auto intro!: non_too_destructive_comp_constructive[OF non_too_destructive_After]
      non_too_destructive_comp_non_destructive[OF non_too_destructive_After])

lemma (in AfterExt) After⇩t⇩i⇩c⇩k_restriction_shift_process⇩p⇩t⇩i⇩c⇩k [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset] :
  ‹⟦non_too_destructive Ψ; non_too_destructive Ω; constructive f⟧
   ⟹ non_destructive (λx. f x  after⇩✓ e)›
  ‹⟦non_too_destructive Ψ; non_too_destructive Ω; non_destructive f⟧
   ⟹ non_too_destructive (λx. f x  after⇩✓ e)›
  by (auto intro!: non_too_destructive_comp_constructive[OF non_too_destructive_After⇩t⇩i⇩c⇩k]
      non_too_destructive_comp_non_destructive[OF non_too_destructive_After⇩t⇩i⇩c⇩k]
      simp add: non_too_destructive_fun_iff)




subsection ‹Illustration›

declare restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset [simp]


notepad begin
  fix e f g :: 'a fix r s :: 'r
  fix A B C :: ‹'a set›
  fix S :: ‹'a ⇒ 'a ⇒ 'a ⇒ 'a set›
  define P where ‹P ≡ υ X. ((□a ∈ A → X ⊓ SKIP r) △ (f → STOP))
                            □ (g → X)
                            □ ((f → e → (⊥ ⊓ (e → X))) Θ b ∈ insert e B. (e → SKIP s))›  
    (is ‹P ≡ υ X. ?f X›)
  have ‹constructive ?f› by simp
  have ‹cont ?f› by simp
  have ‹P = ?f P›
    unfolding P_def by (subst restriction_fix_eq) simp_all


  define Q where ‹Q ≡ υ X. (λσ σ' σ'' . e → ⊓ b ∈ S σ σ' σ''. X b b b ⊓ SKIP r)› (is ‹Q ≡ υ X. ?g X›)
  have ‹constructive ?g› by simp


  define R where ‹R ≡ υ (x, y). (e → y ⊓ SKIP r, □a ∈ A → x)›
    (is ‹R ≡ υ (x, y). (?h y, ?i x)›)
  have ‹snd R = □a ∈ A → fst R›
    by (unfold R_def, subst restriction_fix_eq)
      (simp_all add: case_prod_beta')

end


text ‹Finally, we add the following new law.
      A similar result involving the least fixed-point operator inherited
      from \<^session>‹HOLCF› was already available: @{thm [source] Renaming_fix}.›

lemma Renaming_restriction_fix :
  ‹Renaming (υ X. φ X) f g = (υ X. ((λP. Renaming P f g) ∘ φ ∘ (λP. Renaming P (inv f) (inv g))) X)›
  (is ‹Renaming (υ X. φ X) f g = (υ X. ?φ' X)›) if ‹constructive φ›
  and ‹inj f› and ‹inj g› for φ :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (rule restriction_fix_unique[symmetric])
  show ‹constructive ?φ'›
    by (simp add: comp_def constructiveD constructiveI
                  restriction_process⇩p⇩t⇩i⇩c⇩k_Renaming ‹constructive φ›)
next
  from ‹inj f› ‹inj g›
  have ‹inv f ∘ f = id› ‹inv g ∘ g = id› unfolding inj_iff .
  thus ‹?φ' (Renaming (υ X. φ X) f g) = Renaming (υ X. φ X) f g›
    by (simp add: Renaming_id flip: Renaming_comp restriction_fix_eq[OF ‹constructive φ›])
qed



end