Theory Multi_Sequential_Composition

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Multi sequential composition
 *
 * 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.
 ******************************************************************************›
(*>*)


section ‹Multiple Sequential Composition›

(*<*)
theory Multi_Sequential_Composition
  imports "HOL-CSP"
begin
  (*>*)

text ‹Because of the fact that \<^term>‹SKIP r› is not exactly a neutral element for
      @{const [source] Seq} (cf @{thm SKIP_Seq Seq_SKIP}), we do the folding
      on the reversed list.›


subsection ‹Definition›

fun MultiSeq_rev :: ‹['b list, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where MultiSeq_rev_Nil  : ‹MultiSeq_rev   []    P = SKIP undefined›
  |     MultiSeq_rev_Cons : ‹MultiSeq_rev (l # L) P = MultiSeq_rev L P ❙; P l›


definition MultiSeq :: ‹['b list, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹MultiSeq L P ≡ MultiSeq_rev (rev L) P›


lemma MultiSeq_Nil  [simp] : ‹MultiSeq []        P = SKIP undefined›
  and MultiSeq_snoc [simp] : ‹MultiSeq (L @ [l]) P = MultiSeq L P ❙; P l›
  by (simp_all add: MultiSeq_def)


lemma MultiSeq_elims :
  ‹MultiSeq L P = Q ⟹
   (⋀P'. L = [] ⟹ P = P' ⟹ Q = SKIP undefined ⟹ thesis) ⟹
   (⋀l L' P'. L = L' @ [l] ⟹ P = P' ⟹ Q = MultiSeq L' P' ❙; P' l ⟹ thesis) ⟹ thesis›
  by (simp add: MultiSeq_def, erule MultiSeq_rev.elims, simp_all)



syntax  "_MultiSeq" :: ‹[pttrn, 'b list, 'b ⇒ 'r ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'r] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3SEQ _∈@_./ _)› [78,78,77] 77)
syntax_consts "_MultiSeq" ⇌ MultiSeq
translations  "SEQ p ∈@ L. P" ⇌ "CONST MultiSeq L (λp. P)"



subsection ‹First Properties›

lemma ‹SEQ p ∈@ []. P p = SKIP undefined› by (fact MultiSeq_Nil)

lemma ‹SEQ i ∈@ (L @ [l]). P i = SEQ i ∈@ L. P i ❙; P l› by (fact MultiSeq_snoc)

lemma MultiSeq_singl [simp] : ‹SEQ l ∈@ [l]. P l = P l› by (simp add: MultiSeq_def)



subsection ‹Some Tests›

lemma ‹SEQ p ∈@ []. P p = SKIP undefined› 
  and ‹SEQ p ∈@ [a]. P p = P a› 
  and ‹SEQ p ∈@ [a, b]. P p = P a ❙; P b› 
  and ‹SEQ p ∈@ [a, b, c]. P p = P a ❙; P b ❙; P c›
  by (simp_all add: MultiSeq_def)


lemma test_MultiSeq: ‹(SEQ p ∈@ [1::int .. 3]. P p) = P 1 ❙; P 2 ❙; P 3›
  by (simp add: upto.simps MultiSeq_def)


subsection ‹Continuity›

lemma mono_MultiSeq :
  ‹(⋀x. x ∈ set L ⟹ P x ⊑ Q x) ⟹ SEQ l ∈@ L. P l ⊑ SEQ l ∈@ L. Q l›
  by (induct L rule: rev_induct, simp_all add: fun_belowI mono_Seq)

lemma MultiSeq_cont[simp]:
  ‹(⋀x. x ∈ set L ⟹ cont (P x)) ⟹ cont (λy. SEQ z ∈@ L. P z y)›
  by (induct L rule: rev_induct) simp_all



subsection ‹Factorization of \<^const>‹Seq› in front of \<^const>‹MultiSeq››

lemma MultiSeq_factorization_append:
  ‹L2 ≠ [] ⟹ SEQ p ∈@ L1. P p ❙; SEQ p ∈@ L2. P p = SEQ p ∈@ (L1 @ L2). P p›
  by (induct L2 rule: rev_induct, simp_all)
    (metis (no_types, lifting) MultiSeq_singl MultiSeq_snoc
      Seq_assoc append_assoc append_self_conv2)



subsection ‹\<^term>‹⊥› Absorbtion›


lemma MultiSeq_BOT_absorb:
  ‹SEQ z ∈@ (L1 @ a # L2). P z = SEQ z ∈@ L1. P z ❙; ⊥› if ‹P a = ⊥›
proof (cases ‹L2 = []›)
  from ‹P a = ⊥› show ‹L2 = [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; ⊥› by simp
next
  show ‹L2 ≠ [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; ⊥›
    by (simp add: ‹P a = ⊥› flip: Seq_assoc MultiSeq_factorization_append
        [of L2 ‹L1 @ [a]›, simplified])
qed



subsection ‹First Properties›

lemma MultiSeq_SKIP_neutral:
  ‹SEQ z ∈@ (L1 @ a # L2). P z =
   (  if L2 = [] then SEQ z ∈@ L1. P z ❙; SKIP r
    else SEQ z ∈@ (L1 @ L2). P z)› if ‹P a = SKIP r›
proof (split if_split, intro conjI impI)
  show ‹L2 = [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; SKIP r›
    by (simp add: ‹P a = SKIP r›)
next
  assume ‹L2 ≠ []›
  have ‹MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; P a ❙; MultiSeq L2 P›
    by (metis (mono_tags, opaque_lifting) Cons_eq_appendI MultiSeq_factorization_append
        MultiSeq_snoc ‹L2 ≠ []› append_eq_appendI self_append_conv2)
  also have ‹… = MultiSeq L1 P ❙; MultiSeq L2 P›
    by (simp add: ‹P a = SKIP r› flip: Seq_assoc)
  also have ‹… = MultiSeq (L1 @ L2) P›
    by (simp add: MultiSeq_factorization_append ‹L2 ≠ []›)
  finally show ‹MultiSeq (L1 @ a # L2) P = MultiSeq (L1 @ L2) P› .
qed


lemma MultiSeq_STOP_absorb:
  ‹SEQ z ∈@ (L1 @ a # L2). P z = SEQ z ∈@ L1. P z ❙; STOP› if ‹P a = STOP›
proof (cases ‹L2 = []›)
  show ‹L2 = [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; STOP›
    by (simp add: ‹P a = STOP›)
next
  show ‹L2 ≠ [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; STOP›
    by (simp add: ‹P a = STOP› flip: Seq_assoc MultiSeq_factorization_append
        [of L2 ‹L1 @ [a]›, simplified])
qed


lemma mono_MultiSeq_eq:
  ‹(⋀x. x ∈ set L ⟹ P x = Q x) ⟹ MultiSeq L P = MultiSeq L Q›
  by (induct L rule: rev_induct) simp_all


(* TODO: try this when we will have Seq_is_SKIP_iff *)
(* lemma MultiSeq_is_SKIP_iff:
  ‹MultiSeq L P = SKIP ⟷ (∀a ∈ set L. P a = SKIP)›
  by (induct L, simp_all add: Seq_is_SKIP_iff) *)



subsection ‹Commutativity›

text ‹Of course, since the sequential composition \<^term>‹P ❙; Q› is not commutative,
      the result here is negative: the order of the elements of list \<^term>‹L›
      does matter in @{term [eta_contract = false] ‹SEQ z ∈@ L. P z›}.›



subsection ‹Behaviour with Injectivity›

lemma inj_on_mapping_over_MultiSeq:
  ‹inj_on f (set C) ⟹
   SEQ x ∈@ C. P x = SEQ x ∈@ map f C. P (inv_into (set C) f x)›
proof (induct C rule: rev_induct)
  show ‹inj_on f (set []) ⟹ MultiSeq [] P =
        SEQ x∈@map f []. P (inv_into (set []) f x)› by simp
next
  case (snoc a C)
  hence f1: ‹inv_into (insert a (set C)) f (f a) = a› by force
  show ?case
    apply (simp add: f1, intro ext arg_cong[where f = ‹λx. x ❙; P a›])
    apply (subst "snoc.hyps"(1), rule inj_on_subset[OF "snoc.prems"],
        simp add: subset_insertI)
    using snoc.prems by (auto intro!: mono_MultiSeq_eq)
qed



subsection ‹Definition of ‹first_elem››

primrec first_elem :: ‹['a ⇒ bool, 'a list] ⇒ nat›
  where ‹first_elem P [] = 0›
  |     ‹first_elem P (x # L) = (if P x then 0 else Suc (first_elem P L))›

text ‹\<^const>‹first_elem› returns the first index \<^term>‹i› such that
      \<^term>‹P (L ! i) = True› if it exists, \<^term>‹length L› otherwise.

      This will be very useful later.›

value ‹first_elem (λx. 4 < x) [0::nat, 2, 5]›
lemma ‹first_elem (λx. 5 < x) [0::nat, 2, 5] = 3› by simp 
lemma ‹P ` set L ⊆ {False} ⟹ first_elem P L = length L› by (induct L; simp)


(*<*)
end
  (*>*)