Theory Global_Deterministic_Choice

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Global deterministic choice
 *
 * 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 ‹Definitions of the Architectural Operators›

section‹ The Global Deterministic Choice ›

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

subsection ‹Definition›

text ‹This is an experimental generalization of the deterministic choice.
      In previous versions, this was done by folding the binary operator \<^term>‹(□)›,
      but the set was of course necessarily finite.
      Now we give an abstract definition with the failures and the divergences.›

lift_definition GlobalDet :: ‹['b set, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  is ‹λA P. ({(s, X). s = [] ∧ (s, X) ∈ (⋂a∈A. ℱ (P a))} ∪
             {(s, X). s ≠ [] ∧ (s, X) ∈ (⋃a∈A. ℱ (P a))} ∪
             {(s, X). s = [] ∧ s ∈ (⋃a∈A. 𝒟 (P a))} ∪
             {(s, X). ∃r. s = [] ∧ ✓(r) ∉ X ∧ [✓(r)] ∈ (⋃a∈A. 𝒯 (P a))},
             ⋃a∈A. 𝒟 (P a))›
proof -
  show ‹?thesis A P› (is ‹is_process (?f, ⋃a∈A. 𝒟 (P a))›) for A P
  proof (unfold is_process_def DIVERGENCES_def FAILURES_def fst_conv snd_conv, intro conjI allI impI)
    show ‹([], {}) ∈ ?f› by (simp add: is_processT1)
  next
    show ‹(s, X) ∈ ?f ⟹ ftF s› for s X by (auto intro: is_processT2)
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
      by (auto intro!: is_processT1 dest: is_processT3)
  next
    fix s X Y
    assume assm : ‹(s, Y) ∈ ?f ∧ X ⊆ Y›
    then consider ‹s = []› ‹⋀a. a ∈ A ⟹ (s, Y) ∈ ℱ (P a)›
      | e s' a where ‹a ∈ A› ‹s = e # s'› ‹(s, Y) ∈ ℱ (P a)›
      | a where ‹a ∈ A› ‹s = []› ‹s ∈ 𝒟 (P a)›
      | a r where ‹a ∈ A› ‹s = []› ‹✓(r) ∉ Y› ‹[✓(r)] ∈ 𝒯 (P a)›
      by (cases s) auto
    thus ‹(s, X) ∈ ?f›
    proof cases
      assume ‹s = []› ‹⋀a. a ∈ A ⟹ (s, Y) ∈ ℱ (P a)›
      from this(2) assm have ‹a ∈ A ⟹ (s, X) ∈ ℱ (P a)› for a
        by (meson is_processT4)
      with ‹s = []› show ‹(s, X) ∈ ?f› by fast
    next
      fix e s' a assume ‹a ∈ A› ‹s = e # s'› ‹(s, Y) ∈ ℱ (P a)›
      from ‹(s, Y) ∈ ℱ (P a)› assm[THEN conjunct2]
      have ‹(s, X) ∈ ℱ (P a)› by (fact is_processT4)
      with ‹a ∈ A› ‹s = e # s'› show ‹(s, X) ∈ ?f› by blast
    next
      show ‹a ∈ A ⟹ s = [] ⟹ s ∈ 𝒟 (P a) ⟹ (s, X) ∈ ?f› for a by blast
    next
      fix a r assume ‹a ∈ A› ‹s = []› ‹✓(r) ∉ Y› ‹[✓(r)] ∈ 𝒯 (P a)›
      from ‹✓(r) ∉ Y› assm[THEN conjunct2] have ‹✓(r) ∉ X› by blast
      with ‹a ∈ A› ‹s = []› ‹[✓(r)] ∈ 𝒯 (P a)› show ‹(s, X) ∈ ?f› by blast
    qed
  next
    fix s X Y
    assume assm : ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)›
    then consider ‹s = []› ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (P a)›
      | e s' a where ‹a ∈ A› ‹s = e # s'› ‹(s, X) ∈ ℱ (P a)›
      | a where ‹a ∈ A› ‹s = []› ‹s ∈ 𝒟 (P a)›
      | a r where ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (P a)›
      by (cases s) auto
    thus ‹(s, X ∪ Y) ∈ ?f›
    proof cases
      assume ‹s = []› ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (P a)›
      from this(2) assm[THEN conjunct2]
      have ‹a ∈ A ⟹ (s, X ∪ Y) ∈ ℱ (P a)› for a
        by (simp add: is_processT5)
      with ‹s = []› show ‹(s, X ∪ Y) ∈ ?f› by blast
    next
      fix e s' a assume ‹a ∈ A› ‹s = e # s'› ‹(s, X) ∈ ℱ (P a)›
      from ‹(s, X) ∈ ℱ (P a)› assm[THEN conjunct2]
      have ‹(s, X ∪ Y) ∈ ℱ (P a)› by (simp add: ‹a ∈ A› is_processT5)
      with ‹a ∈ A› ‹s = e # s'› show ‹(s, X ∪ Y) ∈ ?f› by blast
    next
      show ‹a ∈ A ⟹ s = [] ⟹ s ∈ 𝒟 (P a) ⟹ (s, X ∪ Y) ∈ ?f› for a by blast
    next
      fix a r assume ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (P a)›
      with assm[THEN conjunct2] T_F show ‹(s, X ∪ Y) ∈ ?f› by simp blast
    qed
  next
    fix s r X
    assume ‹(s @ [✓(r)], {}) ∈ ?f›
    then obtain a where ‹a ∈ A› ‹(s @ [✓(r)], {}) ∈ ℱ (P a)› by blast
    from this(2) have ‹(s, X - {✓(r)}) ∈ ℱ (P a)› by (fact is_processT6)
    show ‹(s, X - {✓(r)}) ∈ ?f›
    proof (cases ‹s = []›)
      show ‹s = [] ⟹ (s, X - {✓(r)}) ∈ ?f›
        by simp (metis F_T ‹(s @ [✓(r)], {}) ∈ ℱ (P a)› ‹a ∈ A› append_Nil)
    next
      assume ‹s ≠ []›
      with ‹a ∈ A› ‹(s, X - {✓(r)}) ∈ ℱ (P a)›
      show ‹(s, X - {✓(r)}) ∈ ?f› by blast
    qed
  next
    show ‹s ∈ (⋃a∈A. 𝒟 (P a)) ∧ tF s ∧ ftF t ⟹ s @ t ∈ (⋃a∈A. 𝒟 (P a))› for s t
      by (blast intro: is_processT7)
  next
    show ‹s ∈ (⋃a∈A. 𝒟 (P a)) ⟹ (s, X) ∈ ?f› for s X
      by (blast intro: is_processT8)
  next
    show ‹s @ [✓(r)] ∈ (⋃a∈A. 𝒟 (P a)) ⟹ s ∈ (⋃a∈A. 𝒟 (P a))› for s r
      by (blast intro: is_processT9)
  qed
qed


syntax "_GlobalDet" :: ‹[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 "_GlobalDet" ⇌ GlobalDet
translations  "□ p ∈ A. P " ⇌ "CONST GlobalDet A (λp. P)"



subsection ‹The projections›

lemma F_GlobalDet:
  ‹ℱ (□ x ∈ A. P x) =
   {(s, X). s = [] ∧ (s, X) ∈ (⋂a∈A. ℱ (P a))} ∪
   {(s, X). s ≠ [] ∧ (s, X) ∈ (⋃a∈A. ℱ (P a))} ∪
   {(s, X). s = [] ∧ s ∈ (⋃a∈A. 𝒟 (P a))} ∪
   {(s, X). ∃r. s = [] ∧ ✓(r) ∉ X ∧ [✓(r)] ∈ (⋃a∈A. 𝒯 (P a))}›
  by (simp add: Failures.rep_eq FAILURES_def GlobalDet.rep_eq)

lemma F_GlobalDet':
  ‹ℱ (□ x ∈ A. P x) =
   {([], X)| X. (∃a∈A. P a = ⊥) ∨ (∀a∈A. ([], X) ∈ ℱ (P a)) ∨
                (∃a∈A. ∃r. ✓(r) ∉ X ∧ [✓(r)] ∈ 𝒯 (P a))} ∪
   {(s, X)| a s X. a ∈ A ∧ s ≠ [] ∧ (s, X) ∈ ℱ (P a)}›
  (is ‹ℱ (□ x ∈ A. P x) = ?rhs›)
proof (intro subset_antisym subsetI)
  fix sX assume ‹sX ∈ ℱ (□ x ∈ A. P x)›
  obtain s X where ‹sX = (s, X)› using prod.exhaust_sel by blast
  with ‹sX ∈ ℱ (□ x ∈ A. P x)› show ‹sX ∈ ?rhs›
    by (auto simp add: F_GlobalDet BOT_iff_Nil_D)
next
  fix sX assume ‹sX ∈ ?rhs›
  obtain s X where ‹sX = (s, X)› using prod.exhaust_sel by blast
  with ‹sX ∈ ?rhs› show ‹sX ∈ ℱ (□ x ∈ A. P x)›
    by (auto simp add: F_GlobalDet BOT_iff_Nil_D)
qed


lemma D_GlobalDet: ‹𝒟 (□ x ∈ A. P x) = (⋃a∈A. 𝒟 (P a))›
  by (simp add: Divergences.rep_eq DIVERGENCES_def GlobalDet.rep_eq)

lemma T_GlobalDet:
  ‹𝒯 (□ x ∈ A. P x) = (if A = {} then {[]} else (⋃ x∈A. 𝒯 (P x)))›
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_GlobalDet
      intro: is_processT1 is_processT8)

lemma T_GlobalDet': ‹𝒯 (□ x ∈ A. P x) = (insert [] (⋃ x∈A. 𝒯 (P x)))›
  by (simp add: T_GlobalDet)
    (metis T_GlobalDet insert_absorb is_processT1_TR)

lemmas GlobalDet_projs = F_GlobalDet D_GlobalDet T_GlobalDet


lemma mono_GlobalDet_eq:
  ‹(⋀x. x ∈ A ⟹ P x = Q x) ⟹ GlobalDet A P = GlobalDet A Q›
  by (subst Process_eq_spec, simp add: F_GlobalDet D_GlobalDet)

lemma mono_GlobalDet_eq2:
  ‹(⋀x. x ∈ A ⟹ P (f x) = Q x) ⟹ GlobalDet (f ` A) P = GlobalDet A Q›
  by (subst Process_eq_spec, simp add: F_GlobalDet D_GlobalDet)




subsection ‹Factorization of \<^const>‹Det› in front of \<^const>‹GlobalDet››

lemma Process_eq_optimized_bisI :
  assumes ‹⋀s. s ∈ 𝒟 P ⟹ s ∈ 𝒟 Q› ‹⋀s. s ∈ 𝒟 Q ⟹ s ∈ 𝒟 P›
    and ‹⋀X. 𝒟 P = 𝒟 Q ⟹ ([], X) ∈ ℱ P ⟹ ([], X) ∈ ℱ Q›
    and ‹⋀X. 𝒟 Q = 𝒟 P ⟹ ([], X) ∈ ℱ Q ⟹ ([], X) ∈ ℱ P›
    and ‹⋀a s X. 𝒟 P = 𝒟 Q ⟹ (a # s, X) ∈ ℱ P ⟹ (a # s, X) ∈ ℱ Q›
    and ‹⋀a s X. 𝒟 Q = 𝒟 P ⟹ (a # s, X) ∈ ℱ Q ⟹ (a # s, X) ∈ ℱ P›
  shows ‹P = Q›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 Q› for s by (fact assms(1))
next
  show ‹s ∈ 𝒟 Q ⟹ s ∈ 𝒟 P› for s by (fact assms(2))
next
  show ‹𝒟 P = 𝒟 Q ⟹ (s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ Q› for s X
    by (metis assms(3, 5) neq_Nil_conv)
next
  show ‹𝒟 P = 𝒟 Q ⟹ (s, X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ P› for s X
    by (metis assms(4, 6) neq_Nil_conv)
qed


lemma GlobalDet_factorization_union:
  ‹(□ p ∈ A. P p) □ (□ p ∈ B. P p) = □ p ∈ (A ∪ B) . P p›
  by (rule Process_eq_optimized_bisI)
    (auto simp add: D_Det D_GlobalDet F_Det F_GlobalDet T_GlobalDet split: if_split_asm)

lemma GlobalDet_Union :
  ‹(□a ∈ (⋃i ∈ I. A i). P a) = □i ∈ I. □a ∈ A i. P a› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s) (auto simp add: GlobalDet_projs)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; simp add: GlobalDet_projs split: if_split_asm) blast+
qed


subsection ‹First properties›

lemma GlobalDet_id [simp] : ‹A ≠ {} ⟹ (□ p ∈ A. P) = P›
  by (auto simp add: Process_eq_spec F_GlobalDet D_GlobalDet
      intro: is_processT8 is_processT6_TR_notin)

lemma GlobalDet_unit[simp] : ‹(□ x ∈ {a}. P x) = P a› 
  by (auto simp add: Process_eq_spec F_GlobalDet D_GlobalDet
      intro: is_processT8 is_processT6_TR_notin)

(* TODO: move this ? *)
lemma GlobalDet_empty[simp] : ‹(□a ∈ {}. P a) = STOP›
  by (simp add: STOP_iff_T T_GlobalDet)


lemma GlobalDet_distrib_unit:
  ‹(□ x ∈ insert a A. P x) = P a □ (□ x ∈ (A - {a}). P x)›
  by (metis GlobalDet_factorization_union GlobalDet_unit Un_Diff_cancel insert_is_Un)

(* useful ? *)
lemma GlobalDet_distrib_unit_bis : 
  ‹a ∉ A ⟹ (□ x ∈ insert a A. P x) = P a □ (□ x ∈ A. P x)›
  by (simp add: GlobalDet_distrib_unit)



subsection ‹Behaviour of \<^const>‹GlobalDet› with \<^const>‹Det››

lemma GlobalDet_Det_GlobalDet:
  ‹(□ a ∈ A. P a) □ (□ a ∈ A. Q a) = □ a ∈ A. P a □ Q a›
  (is ‹?G1 □ ?G2 = ?G›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 (?G1 □ ?G2) ⟹ s ∈ 𝒟 ?G›
    and ‹s ∈ 𝒟 ?G ⟹ s ∈ 𝒟 (?G1 □ ?G2)› for s
    by (auto simp add: D_Det D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ (?G1 □ ?G2) ⟹ (s, X) ∈ ℱ ?G› for s X
    by (cases s) (auto simp add: F_Det D_Det T_Det D_GlobalDet T_GlobalDet' F_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?G ⟹ (s, X) ∈ ℱ (?G1 □ ?G2)› for s X
    by (cases s; simp add: F_Det D_Det T_Det D_GlobalDet T_GlobalDet' F_GlobalDet) blast+
qed


subsection ‹Commutativity›

lemma GlobalDet_sets_commute:
  ‹(□ a ∈ A. □ b ∈ B. P a b) = □ b ∈ B. □ a ∈ A. P a b› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s; simp add: F_GlobalDet T_GlobalDet' D_GlobalDet split: if_split_asm, blast)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; simp add: F_GlobalDet T_GlobalDet' D_GlobalDet split: if_split_asm, blast)
qed


subsection ‹Behaviour with injectivity›

lemma inj_on_mapping_over_GlobalDet: 
  ‹inj_on f A ⟹ (□ x ∈ A. P x) = □ x ∈ f ` A. P (inv_into A f x)›
  by (simp add: Process_eq_spec F_GlobalDet D_GlobalDet)



subsection ‹Cartesian product results›

lemma GlobalDet_cartprod_σs_set_σs_set:
  ‹(□ (s, t) ∈ A × B. P (s @ t)) = □ u ∈ {s @ t |s t. (s, t) ∈ A × B}. P u›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s; simp add: F_GlobalDet, blast)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; simp add: F_GlobalDet, blast)
qed



lemma GlobalDet_cartprod_s_set_σs_set:
  ‹(□ (s, t) ∈ A × B. P (s # t)) = □ u ∈ {s # t |s t. (s, t) ∈ A × B}. P u›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s; simp add: F_GlobalDet, blast)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; simp add: F_GlobalDet, blast)
qed


lemma GlobalDet_cartprod_s_set_s_set:
  ‹(□ (s, t) ∈ A × B. P [s, t]) = □ u ∈ {[s, t] |s t. (s, t) ∈ A × B}. P u›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s; simp add: F_GlobalDet, blast)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; simp add: F_GlobalDet, blast)
qed


lemma GlobalDet_cartprod: ‹(□(s, t) ∈ A × B. P s t) = □s ∈ A. □t ∈ B. P s t›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s) (auto simp add: F_GlobalDet T_GlobalDet D_GlobalDet)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; simp add: F_GlobalDet T_GlobalDet D_GlobalDet
        split: if_split_asm) blast
qed



subsection ‹Link with \<^const>‹Mprefix››

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

lemma Mprefix_GlobalDet: ‹□ a ∈ A → P a = □ a ∈ A. a → P a›
  by (simp add: Process_eq_spec write0_projs GlobalDet_projs Mprefix_projs, safe, auto)

lemma read_is_GlobalDet_write0 :
  ‹c❙?a∈A → P a = □b∈c ` A. b → P (inv_into A c b)›
  by (simp add: read_def Mprefix_GlobalDet)

lemma read_is_GlobalDet_write :
  ‹inj_on c A ⟹ c❙?a∈A → P a = □a∈A. c❙!a → P a›
  by (auto simp add: read_is_GlobalDet_write0 write_def write0_def
      intro: mono_GlobalDet_eq2)




subsection ‹Properties›

lemma GlobalDet_Det: ‹(□ a ∈ A. P a) □ Q = (if A = {} then Q else □ a ∈ A. P a □ Q)›
  (is ‹?lhs = (if A = {} then Q else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = Q›
    by (auto simp add: Process_eq_spec F_Det F_STOP D_STOP T_STOP D_Det
        intro: is_processT8 is_processT6_TR_notin)
next
  show ‹?lhs = ?rhs› if ‹A ≠ {}›
  proof (subst Process_eq_spec, safe)
    show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
      and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
      by (auto simp add: ‹A ≠ {}› D_Det D_GlobalDet)
  next
    from ‹A ≠ {}› show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
      by (cases s) (auto simp add: F_Det F_GlobalDet D_Det T_Det D_GlobalDet T_GlobalDet)
  next
    from ‹A ≠ {}› show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
      by (cases s; simp add: F_Det F_GlobalDet D_Det T_Det D_GlobalDet T_GlobalDet, blast)
  qed
qed


(* TODO: useful ? *)
lemma Mndetprefix_Sync_Mprefix_strong_subset:
  ‹⟦A ⊆ B; B ⊆ C⟧ ⟹ ⊓ a ∈ A → P a ⟦ C ⟧ □ b ∈ B → Q b = ⊓ a ∈ A → (P a ⟦ C ⟧ Q a)›
  by (simp add: Mndetprefix_Sync_Mprefix_subset STOP_Sync_Mprefix Mprefix_is_STOP_iff)

lemma Mprefix_Sync_Mndetprefix_strong_subset:
  ‹⟦A ⊆ C; B ⊆ A⟧ ⟹ □ a ∈ A → P a ⟦ C ⟧ ⊓ b ∈ B → Q b = ⊓ b ∈ B → (P b ⟦ C ⟧ Q b)›
  by (subst (1 2) Sync_commute, simp add: Mndetprefix_Sync_Mprefix_strong_subset)


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

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



subsection ‹Continuity›

lemma mono_GlobalDet : ‹(□a ∈ A. P a) ⊑ □a ∈ A. Q a› if ‹⋀x. x ∈ A ⟹ P x ⊑ Q x›
proof (unfold le_approx_def, safe)
  show ‹s ∈ 𝒟 (□a ∈ A. Q a) ⟹ s ∈ 𝒟 (□a ∈ A. P a)› for s
    using that[THEN le_approx1] by (auto simp add: D_GlobalDet)
next
  fix s X assume ‹s ∉ 𝒟 (□a ∈ A. P a)› ‹X ∈ ℛ⇩a (□a ∈ A. P a) s›
  from ‹s ∉ 𝒟 (□a ∈ A. P a)› have * : ‹∀a∈A. s ∉ 𝒟 (P a)›
    by (simp add: D_GlobalDet)
  with that le_approx2
  have ** : ‹a ∈ A ⟹ (s, X) ∈ ℱ (Q a) ⟷ (s, X) ∈ ℱ (P a)› for a X by blast
  from ‹X ∈ ℛ⇩a (□a ∈ A. P a) s› "*"
  consider ‹s = []› ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (P a)›
    | e s' a where ‹a ∈ A› ‹s = e # s'› ‹(s, X) ∈ ℱ (P a)›
    | a r where ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (P a)›
    by (cases s) (auto simp add: Refusals_after_def F_GlobalDet)
  thus ‹X ∈ ℛ⇩a (□a ∈ A. Q a) s›
  proof cases
    assume ‹s = []› ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (P a)›
    from this(2) "**" have ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (Q a)› by simp
    with ‹s = []› show ‹X ∈ ℛ⇩a (□a ∈ A. Q a) s›
      by (simp add: Refusals_after_def F_GlobalDet)
  next
    fix e s' a assume ‹a ∈ A› ‹s = e # s'› ‹(s, X) ∈ ℱ (P a)›
    from ‹(s, X) ∈ ℱ (P a)› "**" have ‹(s, X) ∈ ℱ (Q a)› by (simp add: ‹a ∈ A›)
    with ‹a ∈ A› ‹s = e # s'› show ‹X ∈ ℛ⇩a (□a ∈ A. Q a) s›
      by (auto simp add: Refusals_after_def F_GlobalDet)
  next
    fix a r assume ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (P a)›
    from ‹a ∈ A› ‹[✓(r)] ∈ 𝒯 (P a)› have ‹[✓(r)] ∈ 𝒯 (Q a)›
      by (fold T_F_spec, simp add: "**"[OF ‹a ∈ A›])
        (metis "*" ‹s = []› is_processT9 proc_ord2a self_append_conv2 that)
    with ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› show ‹X ∈ ℛ⇩a (□a ∈ A. Q a) s›
      by (auto simp add: Refusals_after_def F_GlobalDet)
  qed
next
  fix s X assume ‹s ∉ 𝒟 (□a ∈ A. P a)› ‹X ∈ ℛ⇩a (□a ∈ A. Q a) s›
  from ‹s ∉ 𝒟 (□a ∈ A. P a)› have * : ‹∀a∈A. s ∉ 𝒟 (P a)›
    by (simp add: D_GlobalDet)
  with that le_approx2
  have ** : ‹a ∈ A ⟹ (s, X) ∈ ℱ (Q a) ⟷ (s, X) ∈ ℱ (P a)› for a X by blast
  from ‹X ∈ ℛ⇩a (□a ∈ A. Q a) s›
  consider ‹s = []› ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (Q a)›
    | e s' a where ‹a ∈ A› ‹s = e # s'› ‹(s, X) ∈ ℱ (Q a)›
    | a where ‹a ∈ A› ‹s = []› ‹s ∈ 𝒟 (Q a)›
    | a r where ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (Q a)›
    by (cases s) (auto simp add: Refusals_after_def F_GlobalDet)
  thus ‹X ∈ ℛ⇩a (□a ∈ A. P a) s›
  proof cases
    assume ‹s = []› ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (Q a)›
    from this(2) "**" have ‹⋀a. a ∈ A ⟹ (s, X) ∈ ℱ (P a)› by simp
    with ‹s = []› show ‹X ∈ ℛ⇩a (□a ∈ A. P a) s›
      by (simp add: Refusals_after_def F_GlobalDet)
  next
    fix e s' a assume ‹a ∈ A› ‹s = e # s'› ‹(s, X) ∈ ℱ (Q a)›
    from ‹(s, X) ∈ ℱ (Q a)› "**" have ‹(s, X) ∈ ℱ (P a)› by (simp add: ‹a ∈ A›)
    with ‹a ∈ A› ‹s = e # s'› show ‹X ∈ ℛ⇩a (□a ∈ A. P a) s›
      by (auto simp add: Refusals_after_def F_GlobalDet)
  next
    show ‹a ∈ A ⟹ s = [] ⟹ s ∈ 𝒟 (Q a) ⟹ X ∈ ℛ⇩a (□a ∈ A. P a) s› for a
      by (simp add: Refusals_after_def F_GlobalDet)
        (meson le_approx1 subsetD that)
  next
    fix a r assume ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› ‹[✓(r)] ∈ 𝒯 (Q a)›
    from ‹a ∈ A› ‹[✓(r)] ∈ 𝒯 (Q a)› have ‹[✓(r)] ∈ 𝒯 (P a)›
      by (fold T_F_spec, simp add: "**"[OF ‹a ∈ A›])
        (metis "*" ‹s = []› is_processT9 proc_ord2a self_append_conv2 that)
    with ‹a ∈ A› ‹s = []› ‹✓(r) ∉ X› show ‹X ∈ ℛ⇩a (□a ∈ A. P a) s›
      by (auto simp add: Refusals_after_def F_GlobalDet)
  qed
next
  from that[THEN le_approx3]
  show ‹s ∈ min_elems (𝒟 (□a ∈ A. P a)) ⟹ s ∈ 𝒯 (□a ∈ A. Q a)› for s
    by (auto simp add: min_elems_def subset_iff less_list_def less_eq_list_def
        prefix_def D_GlobalDet T_GlobalDet) blast
qed


lemma chain_GlobalDet : ‹chain Y ⟹ chain (λi. □a ∈ A. Y i a)›
  by (simp add: ch2ch_monofun fun_belowD mono_GlobalDet monofunI)


lemma GlobalDet_cont [simp] : ‹⟦finite A; ⋀a. a ∈ A ⟹ cont (P a)⟧ ⟹ cont (λy. □ z∈A. P z y)›
  by (induct A rule: finite_induct)
    (simp_all add: GlobalDet_distrib_unit)



end