Theory MultiSeq

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


chapter ‹The MultiSeq Operator›

theory MultiSeq
  imports Patch
begin



section ‹Definition›

definition MultiSeq :: ‹['a list, 'a ⇒ 'b process] ⇒ 'b process›
  where    ‹MultiSeq S P = foldr (λa r.  (P a) ❙;  r  ) S SKIP›


syntax  "_MultiSeq" :: ‹[pttrn,'a list, 'b process] ⇒ 'b process›
                       (‹(3SEQ _∈@_./ _)› 73)
translations  "SEQ i ∈@ A. P " ⇌ "CONST MultiSeq A (λi. P)"



section ‹First Properties›

lemma MultiSeq_rec0[simp]: ‹(SEQ p ∈@ []. P p) = SKIP›
  by (simp add: MultiSeq_def)


lemma MultiSeq_rec1[simp]: ‹(SEQ p ∈@ [a]. P p) = P a›
  by (simp add: MultiSeq_def Seq_SKIP)


lemma MultiSeq_Cons[simp]: ‹(SEQ i ∈@ a # L. P i) = P a ❙; (SEQ i ∈@ L. P i)›
  by (simp add: MultiSeq_def)



section ‹Some Tests›

lemma ‹(SEQ p ∈@ []. P p) = SKIP› 
  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: Seq_SKIP Seq_assoc)


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



section ‹Continuity›

lemma MultiSeq_cont[simp]:
  ‹∀x ∈ set L. cont (P x) ⟹ cont (λy. SEQ z ∈@ L. P z y)› 
  by (induct L) force+



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

lemma MultiSeq_factorization_append:
  ‹(SEQ p ∈@ A. P p) ❙; (SEQ p ∈@ B. P p) = (SEQ p ∈@ A @ B . P p)›
  by (induct A rule: list.induct, simp_all add: SKIP_Seq, metis Seq_assoc)



section ‹\<^term>‹⊥› Absorbance›


lemma MultiSeq_BOT_absorb:
  ‹P a = ⊥ ⟹ (SEQ z ∈@ l1 @ [a] @ l2. P z) = (SEQ z ∈@ l1. P z) ❙; ⊥›
  by (metis BOT_Seq MultiSeq_Cons MultiSeq_factorization_append)



section ‹First Properties›

lemma MultiSeq_SKIP_neutral:
  ‹P a = SKIP ⟹ (SEQ z ∈@ l1 @ [a] @ l2. P z) = SEQ z ∈@ l1 @ l2. P z›
  by (simp add: MultiSeq_def SKIP_Seq)


lemma MultiSeq_STOP_absorb:
  ‹P a = STOP ⟹
   (SEQ z ∈@ l1 @ [a] @ l2. P z) = (SEQ z ∈@ l1. P z) ❙; STOP›
  by (metis STOP_Seq MultiSeq_Cons MultiSeq_factorization_append)


lemma mono_MultiSeq_eq:
  ‹∀x ∈ set L. P x = Q x ⟹ MultiSeq L P = MultiSeq L Q›
  by (induct L) fastforce+


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)



section ‹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›}.›



section ‹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)
  case Nil
  show ?case by simp
next
  case (Cons a C)
  hence f1: ‹inv_into (insert a (set C)) f (f a) = a› by force
  show ?case
    apply (simp add: f1, rule arg_cong[where f = ‹λx. P a ❙; x›])
    apply (subst "Cons.hyps"(1), rule inj_on_subset[OF "Cons.prems"],
           simp add: subset_insertI)
    apply (rule mono_MultiSeq_eq)
    using "Cons.prems" by fastforce
qed



section ‹Definition of ‹first_elem››

primrec first_elem :: ‹['α ⇒ bool, 'α 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