Theory Global_Non_Deterministic_Choice

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Global non deterministic choice
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * 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.
 ******************************************************************************›
(*>*)


chapter‹ The Global non Deterministic Choice ›

(*<*)
theory Global_Non_Deterministic_Choice
  imports Constant_Processes Deterministic_Choice
    Non_Deterministic_Choice Multi_Non_Deterministic_Prefix_Choice
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 :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊓ Q = Q›
proof (rule ccontr, simp, elim exE)
  fix P
  assume * : ‹∀Q. (P :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊓ Q = Q›
  hence ‹P = STOP›
    by (erule_tac x = STOP in allE) (auto simp add: STOP_iff_T T_Ndet T_STOP)
  with * show False
    apply (erule_tac x = ‹SKIP undefined› in allE) 
    apply (simp add: Process_eq_spec F_STOP F_Ndet F_SKIP set_eq_iff)
    by (metis UNIV_I not_Cons_self)
qed



lift_definition GlobalNdet :: ‹['b set, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  is ‹λA P.   if A = {} 
            then ({(s, X). s = []}, {})
            else (⋃a∈A. ℱ (P a), ⋃a∈A. 𝒟 (P a))›
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))› (is ‹is_process (?f, ?d)›)
    if ‹A ≠ {}› for P :: ‹'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and A
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv,
      intro conjI impI allI)
    from ‹A ≠ {}› is_processT1 show ‹([], {}) ∈ ?f› by blast
  next
    from is_processT2 show ‹(s, X) ∈ ?f ⟹ ftF s› for s X by blast
  next
    from is_processT3 show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t by blast
  next
    from is_processT4 show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y by blast
  next
    from is_processT5
    show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)
          ⟹ (s, X ∪ Y) ∈ ?f› for s X Y by simp blast
  next
    from is_processT6
    show ‹(s @ [✓(r)], {}) ∈ ?f ⟹ (s, X - {✓(r)}) ∈ ?f› for s r X by fast
  next
    from is_processT7 show ‹s ∈ ?d ∧ tF s ∧ ftF t ⟹ s @ t ∈ ?d› for s t by blast
  next
    from is_processT8 show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X by blast
  next
    from is_processT9 show ‹s @ [✓(r)] ∈ ?d ⟹ s ∈ ?d› for s r by fast
  qed
qed


syntax "_GlobalNdet" :: ‹[pttrn,'b set,('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3⊓((_)/∈(_))./ (_))› [78,78,77] 77)
syntax_consts "_GlobalNdet" == GlobalNdet
translations  "⊓ a ∈ A. P " ⇌ "CONST GlobalNdet A (λa. P)"

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


section ‹The projections›

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

lemma D_GlobalNdet: ‹𝒟 (⊓ a ∈ A. P a) = (⋃ a∈A. 𝒟 (P a))›
  by (simp add: Divergences.rep_eq DIVERGENCES_def GlobalNdet.rep_eq)

lemma T_GlobalNdet:
  ‹𝒯 (⊓ a ∈ A. P a) = (if A = {} then {[]} else (⋃ a∈A. 𝒯 (P a)))›
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] 
      F_GlobalNdet intro: F_T T_F)

lemma T_GlobalNdet': ‹𝒯 (⊓ a ∈ A. P a) = insert [] (⋃ a∈A. 𝒯 (P a))›
  by (simp add: T_GlobalNdet)
    (metis T_GlobalNdet insert_absorb is_processT1_TR)

lemmas GlobalNdet_projs = F_GlobalNdet D_GlobalNdet T_GlobalNdet'


lemma mono_GlobalNdet_eq:
  ‹(⋀a. a ∈ A ⟹ P a = Q a) ⟹ GlobalNdet A P = GlobalNdet A Q›
  by (subst Process_eq_spec, simp add: F_GlobalNdet D_GlobalNdet)

lemma mono_GlobalNdet_eq2:
  ‹(⋀a. a ∈ A ⟹ P (f a) = Q a) ⟹ 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)

lemma GlobalNdet_Union :
  ‹(⊓a ∈ (⋃i ∈ I. A i). P a) = ⊓i ∈ {i ∈ I. A i ≠ {}}. ⊓a ∈ A i. P a›
  by (auto simp add: Process_eq_spec GlobalNdet_projs)


section ‹First properties›

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


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)

lemma GlobalNdet_distrib_unit_bis : 
  ‹(⊓ x ∈ insert a A. P x) = (if A - {a} = {} then P a else P a ⊓ (⊓ x ∈ (A - {a}). P x))›
  by (metis GlobalNdet_distrib_unit GlobalNdet_unit insert_Diff_single)



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)



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)






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: ‹⊓ a ∈ A → P a = ⊓ a ∈ A. a → P a›
  by (cases ‹A = {}›; subst Process_eq_spec_optimized) 
    (simp_all add: F_Mndetprefix D_Mndetprefix F_GlobalNdet D_GlobalNdet)

lemma write0_GlobalNdet:
  ‹x → ⊓ a ∈ A. P a = (if A = {} then x → STOP else ⊓ a ∈ A. x → P a)›
  by (auto simp add: Process_eq_spec write0_def STOP_projs
      F_GlobalNdet D_GlobalNdet F_Mprefix D_Mprefix)

lemma ndet_write_is_GlobalNdet_write0 :
  ‹c❙!❙!a∈A → P a = ⊓b∈c ` A. b → P (inv_into A c b)›
  by (simp add: ndet_write_def Mndetprefix_GlobalNdet)

lemma ndet_write_is_GlobalNdet_write :
  ‹inj_on c A ⟹ c❙!❙!a∈A → P a = ⊓a∈A. c❙!a → P a›
  by (auto simp add: ndet_write_is_GlobalNdet_write0 write_def write0_def
      intro: mono_GlobalNdet_eq2)


(* 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 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
    by (auto simp add: Process_eq_spec F_Det D_Det write0_def
        F_GlobalNdet D_GlobalNdet T_GlobalNdet F_STOP D_STOP
        F_Mprefix D_Mprefix T_Mprefix)
qed



section ‹Continuity›

lemma mono_GlobalNdet : ‹(⋀a. a ∈ A ⟹ P a ⊑ Q a) ⟹ (⊓a ∈ A. P a) ⊑ ⊓a ∈ A. Q a›
  by (simp add: le_approx_def D_GlobalNdet Refusals_after_def F_GlobalNdet
      min_elems_def T_GlobalNdet subset_iff) blast

lemma chain_GlobalNdet : ‹chain Y ⟹ chain (λi. ⊓a ∈ A. Y i a)›
  by (simp add: ch2ch_monofun fun_belowD mono_GlobalNdet monofunI)


lemma GlobalNdet_cont [simp] : ‹⟦finite A; ⋀a. a ∈ A ⟹ cont (P a)⟧ ⟹ cont (λy. ⊓ z∈A. P z y)›
proof (induct A rule: finite_induct)
  case empty
  thus ?case by (simp add: GlobalNdet.abs_eq)
next
  case (insert a A)
  thus ?case
    by (cases ‹A = {}›, simp)
      (subst GlobalNdet_distrib_unit[of A a], auto)
qed


(*<*)
end
  (*>*)