Theory GlobalNdet

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff
 *
 * This file       : Global non-deterministic choice
 *
 * 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 Global Non-Deterministic Choice ›
theory GlobalNdet                                               
  imports MultiNdet
begin 


section‹ General Non-Deterministic Choice Definition›

text‹ This is an experimental definition of a generalized non-deterministic choice  \<^term>‹a ⊓ b›
for an arbitrary set. The present version is "totalised" for the case of \<^term>‹A = {}› by
\<^const>‹STOP›, which is not the neutral element of the \<^const>‹Ndet› operator (because
there is no neutral element for \<^const>‹Ndet›).›

lemma ‹∄P. ∀Q. (P :: 'α process) ⊓ Q = Q›
proof -
  { fix P :: ‹'α process›
    assume * : ‹∀Q. P ⊓ Q = Q›
    hence ‹P = STOP›
      by (erule_tac x = STOP in allE) (simp add: Ndet_is_STOP_iff)
    with * have False
      by (erule_tac x = SKIP in allE) 
         (metis mono_Ndet_FD_right Ndet_commute 
                SKIP_FD_iff SKIP_Neq_STOP idem_FD)
  }
  thus ?thesis by blast
qed



lift_definition GlobalNdet :: ‹['α set, 'α ⇒ 'β process] ⇒ 'β process›
  is   ‹λA P.   if A = {} 
              then ({(s, X). s = []}, {})
              else (⋃a∈A. ℱ (P a), ⋃a∈A. 𝒟 (P a))›
proof -
  show ‹?thesis A P›
   (is ‹is_process (  if A = {} then ({(s, X). s = []}, {}) else (?f, ?d))›) for A P
  proof (split if_split, intro conjI impI)
    show ‹is_process ({(s, X). s = []}, {})›
      by (metis STOP.rsp eq_onp_def)
  next
    show ‹is_process (⋃a∈A. ℱ (P a), ⋃a∈A. 𝒟 (P a))› if nonempty: ‹A ≠ {}›
      unfolding is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv
    proof (intro conjI allI impI)
      show ‹([], {}) ∈ ?f› using is_processT1 nonempty by blast
    next
      show ‹(s, X) ∈ ?f ⟹ front_tickFree s› for s X
        using is_processT2 by blast
    next
      show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
        using is_processT3 by blast
    next
      show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
        using is_processT4 by blast
    next
      show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟹ (s, X ∪ Y) ∈ ?f› for s X Y
        using is_processT5 by simp blast
    next
      show ‹(s @ [tick], {}) ∈ ?f ⟹ (s, X - {tick}) ∈ ?f› for s X
        using is_processT6 by blast
    next
      show ‹s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ ?d› for s t
        using is_processT7 by blast
    next
      show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X 
        using is_processT8 by blast
    next
      show ‹s @ [tick] ∈ ?d ⟹ s ∈ ?d› for s
        using is_processT9 by blast
    qed
  qed
qed
  
  


syntax  "_GlobalNdet" :: ‹[pttrn,'a set,'b process] ⇒ 'b process› (‹(3⊓ _∈_. / _)› 76)
syntax_consts "_GlobalNdet" ⇌ GlobalNdet
translations  "⊓ p ∈ A. P " ⇌ "CONST GlobalNdet A (λp. P)"

text‹Note that the global non-deterministic choice @{term [eta_contract = false] ‹⊓ p ∈ A. P p›}
     is different from the multi-non-deterministic prefix
     @{term [eta_contract = false] ‹⊓ p ∈ A → P p›} which guarantees continuity 
     even when \<^term>‹A› is \<^const>‹infinite› due to the fact that it communicates
     its choice via an internal prefix operator.

     It is also subtly different from the multi-non-deterministic choice
     @{term [eta_contract = false] ‹⨅ p ∈ A. P p›} 
     which is only defined when \<^term>‹A› is \<^const>‹finite›.›

lemma empty_GlobalNdet[simp] : ‹GlobalNdet {} P = STOP›
  by (simp add: GlobalNdet.abs_eq STOP_def)



section ‹The Projections›

lemma F_GlobalNdet:
  ‹ℱ (⊓ x ∈ A. P x) = (if A = {} then {(s, X). s = []} else (⋃ x∈A. ℱ (P x)))›
  by (simp add: Failures_def FAILURES_def GlobalNdet.rep_eq)

lemma D_GlobalNdet:
  ‹𝒟 (⊓ x ∈ A. P x) = (if A = {} then {} else (⋃ x∈A. 𝒟 (P x)))›
  by (simp add: Divergences_def DIVERGENCES_def GlobalNdet.rep_eq)

lemma T_GlobalNdet:
  ‹𝒯 (⊓ x ∈ A. P x) = (if A = {} then {[]} else (⋃ x∈A. 𝒯 (P x)))›
  by (auto simp: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric]
    F_GlobalNdet intro: F_T T_F)
 
lemma mono_GlobalNdet_eq:
  ‹∀x ∈ A. P x = Q x ⟹ GlobalNdet A P = GlobalNdet A Q›
  by (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)

lemma mono_GlobalNdet_eq2:
  ‹∀x ∈ A. P (f x) = Q x ⟹ GlobalNdet (f ` A) P = GlobalNdet A Q›
  by (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)




section ‹Factorization of \<^const>‹Ndet› in front of \<^const>‹GlobalNdet››

lemma GlobalNdet_factorization_union:
  ‹⟦A ≠ {}; B ≠ {}⟧ ⟹
   (⊓ p ∈ A. P p) ⊓ (⊓ p ∈ B. P p) = (⊓ p ∈ A ∪ B . P p)›
  by (subst Process_eq_spec) (simp add: F_GlobalNdet D_GlobalNdet F_Ndet D_Ndet)
 



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

lemma GlobalNdet_BOT_absorb: ‹P a = ⊥ ⟹ a ∈ A ⟹ (⊓ x ∈ A. P x) = ⊥›
  using is_processT2
  by (subst Process_eq_spec)
     (auto simp add: F_GlobalNdet D_GlobalNdet F_UU D_UU D_imp_front_tickFree)


lemma GlobalNdet_is_BOT_iff: ‹(⊓ x ∈ A. P x) = ⊥ ⟷ (∃a ∈ A. P a = ⊥)›
  by (simp add: BOT_iff_D D_GlobalNdet)
  


section ‹First Properties›

lemma GlobalNdet_id: ‹A ≠ {} ⟹ (⊓ p ∈ A. P) = P›
  by (subst Process_eq_spec) (simp add: F_GlobalNdet D_GlobalNdet)


lemma GlobalNdet_STOP_id: ‹(⊓ p ∈ A. STOP) = STOP›
  by (cases ‹A = {}›) (simp_all add: GlobalNdet_id)


lemma GlobalNdet_unit[simp] : ‹(⊓ x ∈ {a}. P x) = P a› 
  by(auto simp : Process_eq_spec F_GlobalNdet D_GlobalNdet)


lemma GlobalNdet_distrib_unit:
  ‹A - {a} ≠ {} ⟹ (⊓ x ∈ insert a A. P x) = P a ⊓ (⊓ x ∈ A - {a}. P x)›
  by (metis GlobalNdet_factorization_union GlobalNdet_unit 
            empty_not_insert insert_Diff_single insert_is_Un)



section ‹Behaviour of \<^const>‹GlobalNdet› with \<^const>‹Ndet››

lemma GlobalNdet_Ndet:
  ‹(⊓ a ∈ A. P a) ⊓ (⊓ a ∈ A. Q a) = ⊓ a ∈ A. P a ⊓ Q a›
  by (auto simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Ndet D_Ndet)



section ‹Commutativity›

lemma GlobalNdet_sets_commute:
  ‹(⊓ a ∈ A. ⊓ b ∈ B. P a b) = ⊓ b ∈ B. ⊓ a ∈ A. P a b›
  by (auto simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet 
                     F_Ndet D_Ndet F_STOP D_STOP)



section ‹Behaviour with Injectivity›

lemma inj_on_mapping_over_GlobalNdet: 
  ‹inj_on f A ⟹ (⊓ x ∈ A. P x) = ⊓ x ∈ f ` A. P (inv_into A f x)›
  by (simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet
                F_Ndet D_Ndet F_STOP D_STOP)






section ‹Cartesian Product Results›

lemma GlobalNdet_cartprod_σs_set_σs_set:
  ‹(⊓ (s, t) ∈ A × B. P (s @ t)) = ⊓ u ∈ {s @ t |s t. (s, t) ∈ A × B}. P u›
  apply (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)
  by safe auto


lemma GlobalNdet_cartprod_s_set_σs_set:
  ‹(⊓ (s, t) ∈ A × B. P (s # t)) = ⊓ u ∈ {s # t |s t. (s, t) ∈ A × B}. P u›
  apply (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)
  by safe auto


lemma GlobalNdet_cartprod_s_set_s_set:
  ‹(⊓ (s, t) ∈ A × B. P [s, t]) = ⊓ u ∈ {[s, t] |s t. (s, t) ∈ A × B}. P u›
  apply (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)
  by safe auto


lemma GlobalNdet_cartprod: ‹(⊓(s, t) ∈ A × B. P s t) = ⊓s ∈ A. ⊓t ∈ B. P s t›
  apply (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)
  by safe auto
  

  
section ‹Link with \<^const>‹MultiNdet››

text ‹This operator is in fact an extension of \<^const>‹MultiNdet› to arbitrary sets:
      when \<^term>‹A› is \<^const>‹finite›, we have
      @{term [eta_contract = false] ‹(⊓a ∈ A. P a) = ⨅a ∈ A. P a›}.›

lemma finite_GlobalNdet_is_MultiNdet:
  ‹finite A ⟹ (⊓ p ∈ A. P p) = ⨅ p ∈ A. P p›
  by (simp add: Process_eq_spec F_GlobalNdet F_MultiNdet D_GlobalNdet D_MultiNdet)


text ‹We obtain immediately the continuity when \<^term>‹A› is \<^const>‹finite›
      (and this is a necessary hypothesis for continuity).›

lemma GlobalNdet_cont[simp]:
  ‹⟦finite A; ∀x. cont (f x)⟧ ⟹ cont (λy. (⊓ z ∈ A. (f z y)))›
  by (simp add: finite_GlobalNdet_is_MultiNdet) 
                                    


section ‹Link with \<^const>‹Mndetprefix››

text ‹This is a trick to make proof of \<^const>‹Mndetprefix› using
      \<^const>‹GlobalNdet› as it has an easier denotational definition.›

lemma Mndetprefix_GlobalNdet: ‹⊓ x ∈ A → P x = ⊓ x ∈ A. (x → P x)›
  apply (cases ‹A = {}›, simp)
  by (subst Process_eq_spec_optimized) 
     (simp_all add: F_Mndetprefix D_Mndetprefix F_GlobalNdet D_GlobalNdet)
  
lemma write0_GlobalNdet:
  ‹A ≠ {} ⟹ (⊓ x∈A. (a → P x)) = (a → (⊓ x∈A. P x))›
  by (auto simp add: Process_eq_spec write0_def 
                     F_GlobalNdet D_GlobalNdet F_Mprefix D_Mprefix)


section ‹Properties›

lemma GlobalNdet_Det:
  ‹A ≠ {} ⟹ (⊓ a ∈ A. P a) □ Q = ⊓ a ∈ A. P a □ Q›
  by (auto simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet
                     F_Det D_Det Un_def T_GlobalNdet) 

lemma Mndetprefix_STOP: ‹A ⊆ C ⟹ (⊓ a ∈ A → P a) ⟦C⟧ STOP = STOP›
proof (subst STOP_iff_T, intro subset_antisym subsetI)
  show ‹s ∈ {[]} ⟹ s ∈ 𝒯 (Mndetprefix A P ⟦C⟧ STOP)› for s
    by (simp add: Nil_elem_T)
next
  show ‹A ⊆ C ⟹ s ∈ 𝒯 (Mndetprefix A P ⟦C⟧ STOP) ⟹ s ∈ {[]}› for s
    by (auto simp add: STOP_iff_T T_Sync T_Mndetprefix D_Mndetprefix
                       T_STOP D_STOP write0_def T_Mprefix D_Mprefix subset_iff
                split: if_split_asm) 
       (metis Sync.sym emptyLeftNonSync hd_in_set imageI insert_iff)+
qed


lemma GlobalNdet_Sync_distr:
  ‹A ≠ {} ⟹ (⊓ x ∈ A. P x) ⟦ C ⟧ Q = ⊓ x ∈ A. (P x ⟦ C ⟧ Q)›
  apply (auto simp: Process_eq_spec T_GlobalNdet
                    F_GlobalNdet D_GlobalNdet D_Sync F_Sync) ― ‹takes some seconds›
  using front_tickFree_Nil by blast+ 

lemma Mndetprefix_Mprefix_Sync_distr:
  ‹⟦A ⊆ B; B ⊆ C⟧ ⟹ (⊓ a ∈ A → P a) ⟦ C ⟧ (□ b ∈ B → Q b) =
                      ⊓ a ∈ A → (P a ⟦ C ⟧ Q a)›
  ― ‹does not hold in general when \<^term>‹A ⊆ C››
  apply (cases ‹A = {}›, simp,
         metis (no_types, lifting) Mprefix_STOP Mprefix_Sync_distr_subset
                                   empty_subsetI inf_bot_left)
  apply (cases ‹B = {}›, simp add: Mprefix_STOP Mndetprefix_STOP)
  apply (subst Mndetprefix_GlobalNdet, subst GlobalNdet_Sync_distr, assumption)
  apply (subst Mndetprefix_GlobalNdet, subst Mprefix_singl[symmetric]) 
  apply (unfold write0_def, rule mono_GlobalNdet_eq[rule_format])
  apply (subst Mprefix_Sync_distr_subset[of _ C B P Q], blast, blast)
  by (metis (no_types, lifting) in_mono inf_le1 insert_disjoint(1)
                                Mprefix_singl subset_singletonD)


corollary Mndetprefix_Mprefix_Par_distr:
  ‹A ⊆ B ⟹ ((⊓ a ∈ A → P a) || (□ b ∈ B → Q b)) = ⊓ a ∈ A → P a || Q a›
  by (simp add: Mndetprefix_Mprefix_Sync_distr)


lemma Mndetprefix_Sync_Det_distr:
  ‹(⊓ a ∈ A → (P a ⟦ C ⟧ (⊓ b ∈ B → Q b))) □
   (⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧ Q b))
   ⊑⇩F⇩D (⊓ a ∈ A → P a) ⟦ C ⟧ (⊓ b ∈ B → Q b)›
  if set_hyps : ‹A ≠ {}› ‹B ≠ {}› ‹A ∩ C = {}› ‹B ∩ C = {}›
   ― ‹both surprising: equality does not hold + deterministic choice›
proof -
  have mono_GlobalNdet_FD:
    ‹⋀P Q A. ∀x ∈ A. P x ⊑⇩F⇩D Q x ⟹ GlobalNdet A P ⊑⇩F⇩D GlobalNdet A Q›
    by (auto simp: failure_divergence_refine_def le_ref_def F_GlobalNdet D_GlobalNdet)

  have * : ‹a ∈ A ⟹ b ∈ B ⟹
           (⊓b ∈ B.  (a → (P a ⟦C⟧ (b → Q b)))) □
           (⊓a ∈ A.  (b → ((a → P a) ⟦C⟧ Q b))) ⊑⇩F⇩D
           (a → P a) ⟦C⟧ (b → Q b)› for a b
    apply (subst Mprefix_Sync_distr_indep[of ‹{a}› C ‹{b}›, unfolded Mprefix_singl])
    using that(3) 
      apply (simp add: disjoint_iff; fail)
    using that(4) 
     apply (simp add: disjoint_iff; fail)
    apply (rule mono_Det_FD)
    unfolding failure_divergence_refine_def le_ref_def
    by (auto simp add: D_GlobalNdet F_GlobalNdet)

  have ‹(⊓a ∈ A. ⊓b ∈ B. (a → (P a ⟦C⟧ (b → Q b)))) □
        (⊓b ∈ B. ⊓a ∈ A. (b → ((a → P a) ⟦C⟧ Q b))) ⊑⇩F⇩D
        ⊓b ∈ B. ⊓a ∈ A.  ((a → P a) ⟦C⟧ (b → Q b))›
    apply (subst Det_commute, subst GlobalNdet_Det, simp add: set_hyps(2))
    apply (subst Det_commute, subst GlobalNdet_Det, simp add: set_hyps(1))
    apply (intro ballI impI mono_GlobalNdet_FD) 
    using "*" by blast

  thus ?thesis
    apply (simp add: Mndetprefix_GlobalNdet GlobalNdet_Sync_distr)
    apply (subst (1 2 3) Sync_commute, simp add: GlobalNdet_Sync_distr set_hyps(2))
    apply (subst (1 2 3) Sync_commute, simp add: GlobalNdet_Sync_distr set_hyps(1))
    by (simp add: set_hyps(1, 2) write0_GlobalNdet)
qed





lemma GlobalNdet_Mprefix_distr:
  ‹A ≠ {} ⟹ (⊓ a ∈ A. □ b ∈ B → P a b) = □ b ∈ B → (⊓ a ∈ A. P a b)›
  by (auto simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Mprefix D_Mprefix)



lemma GlobalNdet_Det_distrib:
  ‹(⊓ a ∈ A. P a □ Q a) = (⊓ a ∈ A. P a) □ (⊓ a ∈ A. Q a)›
  if ‹∃Q' b. ∀a. Q a = (b → Q' a)›
proof -
  from that obtain b Q' where ‹∀a. (Q a = (b → Q' a))› by blast
  thus ?thesis
    apply (cases ‹A = {}›, simp add: Det_STOP)
    apply (simp add: Process_eq_spec F_Det D_Det write0_def
                     F_GlobalNdet D_GlobalNdet T_GlobalNdet, safe)
    by (auto simp add: F_Mprefix D_Mprefix T_Mprefix)
qed



end