Theory Multi_Non_Deterministic_Prefix_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       : Multi non deterministic prefix 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.
 ******************************************************************************›
(*>*)

section‹ Multiple non Deterministic Prefix Choice ›

(*<*)
theory Multi_Non_Deterministic_Prefix_Choice
  imports Constant_Processes Multi_Deterministic_Prefix_Choice Non_Deterministic_Choice
begin
  (*>*)

section‹Multiple non deterministic prefix operator›

lift_definition Mndetprefix :: ‹['a set, 'a ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  is ‹λA P.   if A = {} then process⇩₀_of_process STOP
            else (⋃a∈A. ℱ (a → P a), ⋃a∈A. 𝒟 (a → P a))›
proof (split if_split, intro conjI impI)
  show ‹is_process (process⇩₀_of_process STOP)›
    by (metis STOP.rep_eq STOP.rsp eq_onp_def)
next
  show ‹is_process (⋃a∈A. ℱ (a → P a), ⋃a∈A. 𝒟 (a → P a))› (is ‹is_process (?f, ?d)›)
    if ‹A ≠ {}› for A and P :: ‹'a ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  proof (unfold is_process_def DIVERGENCES_def FAILURES_def fst_conv snd_conv, intro conjI allI impI)
    show ‹([], {}) ∈ ?f› by (simp add: ex_in_conv is_processT1 ‹A ≠ {}›)
  next
    show ‹(s, X) ∈ ?f ⟹ front_tickFree s› for s X
      by (blast intro: is_processT2)
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
      by (blast intro: is_processT3)
  next
    show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
      by (blast intro: is_processT4)
  next
    show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟹
          (s, X ∪ Y) ∈ ?f› for s X Y by (blast intro!: is_processT5)
  next
    show ‹(s @ [✓(r)], {}) ∈ ?f ⟹ (s, X - {✓(r)}) ∈ ?f› for s r X
      by (blast intro: is_processT6)
  next
    show ‹s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ ?d› for s t
      by (blast intro: is_processT7)
  next
    show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X
      by (blast intro!: is_processT8)
  next
    show ‹s @ [✓(r)] ∈ ?d ⟹ s ∈ ?d› for s r
      by (blast intro!: is_processT9)
  qed
qed


syntax "_Mndetprefix" :: "pttrn ⇒ 'a set ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k" 
  (‹(3⊓((_)/∈(_))/ → (_))› [78,78,77] 77)
syntax_consts "_Mndetprefix" ⇌ Mndetprefix
  (* "_writeS"  :: "['b ⇒ 'a, pttrn, 'b set, ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] => ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k" 
                          ("(4(_❙!_❙|_) /→ _)" [0,0,50,78] 50) *)

translations "⊓a ∈ A → P" ⇌ "CONST Mndetprefix A (λa. P)"
  (* "_writeS c p b P"  => "CONST Mndetprefix (c ` {p. b}) (λ_. P)" *)



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

lemma D_Mndetprefix : ‹𝒟 (⊓a ∈ A → P a) = (if A = {} then {} else ⋃x∈A. 𝒟 (x → P x))›
  by (simp add: Divergences.rep_eq DIVERGENCES_def STOP.rep_eq Mndetprefix.rep_eq)

lemma T_Mndetprefix: ‹𝒯 (⊓a ∈ A → P a) = (if A = {} then {[]} else ⋃x∈A. 𝒯 (x → P x))›
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Mndetprefix)

lemma mono_Mndetprefix_eq: ‹(⋀a. a ∈ A ⟹ P a = Q a) ⟹ ⊓a ∈ A → P a = ⊓a ∈ A → Q a›
  by (cases ‹A = {}›, simp; subst Process_eq_spec, auto simp add: F_Mndetprefix D_Mndetprefix)


lemma F_Mndetprefix' :
  ‹ℱ (⊓a ∈ A → P a) =
   (  if A = {} then {(s, X). s = []}
    else {([], X)| X. ∃a ∈ A. ev a ∉ X} ∪ {(ev a # s, X) |a s X. a ∈ A ∧ (s, X) ∈ ℱ (P a)})›
  by (simp add: F_Mndetprefix write0_def F_Mprefix) blast

lemma D_Mndetprefix' : ‹𝒟 (⊓a ∈ A → P a) = {ev a # s |a s. a ∈ A ∧ s ∈ 𝒟 (P a)}›
  by (auto simp add: D_Mndetprefix write0_def D_Mprefix)

lemma T_Mndetprefix' : ‹𝒯 (⊓a ∈ A → P a) = insert [] {ev a # s |a s. a ∈ A ∧ s ∈ 𝒯 (P a)}›
  by (auto simp add: T_Mndetprefix write0_def T_Mprefix)

lemmas Mndetprefix_projs = F_Mndetprefix' D_Mndetprefix' T_Mndetprefix'


text‹ Thus we know now, that Mndetprefix yields processes. Direct consequences are the following
  distributivities: ›

lemma Mndetprefix_singl [simp] : ‹⊓ a ∈ {a} → P a = a → P a› 
  by (auto simp add: Process_eq_spec F_Mndetprefix D_Mndetprefix)

lemma Mndetprefix_Un_distrib :
  ‹A ≠ {} ⟹ B ≠ {} ⟹ ⊓x ∈ (A ∪ B) → P x = (⊓a ∈ A → P a) ⊓ (⊓b ∈ B → P b)›
  by(auto simp : Process.Process_eq_spec F_Ndet D_Ndet F_Mndetprefix D_Mndetprefix)

text‹ The two lemmas @{thm Mndetprefix_singl} and @{thm Mndetprefix_Un_distrib} together give us that @{const Mndetprefix} 
      can be represented by a fold in the finite case. ›                                         

lemma Mndetprefix_distrib_unit :
  ‹A - {a} ≠ {} ⟹ ⊓ x ∈ insert a A → P x = (a → P a) ⊓ (⊓x ∈ (A - {a}) → P x)›
  by (metis Un_Diff_cancel insert_is_Un insert_not_empty Mndetprefix_Un_distrib Mndetprefix_singl)

text‹ This also implies that \<^const>‹Mndetprefix› is continuous when \<^term>‹finite A›,
      but this is not really useful since we have the general case. ›


subsection‹General case Continuity›

lemma mono_Mndetprefix : ‹⊓a ∈ A → P a ⊑ ⊓a ∈ A → Q a›
  (is ‹?P ⊑ ?Q›) if ‹⋀a. a ∈ A ⟹ P a ⊑ Q a›
proof (unfold le_approx_def, intro conjI impI allI subsetI)
  from that[THEN le_approx1] show ‹s ∈ 𝒟 ?Q ⟹ s ∈ 𝒟 ?P› for s
    by (auto simp add: D_Mndetprefix')
next
  from that[THEN le_approx2] show ‹s ∉ 𝒟 ?P ⟹ ℛ⇩_a ?P s = ℛ⇩_a ?Q s› for s
    by (auto simp add: Refusals_after_def D_Mndetprefix' F_Mndetprefix')
next
  from that[THEN le_approx3] show ‹s ∈ min_elems (𝒟 ?P) ⟹ s ∈ 𝒯 ?Q› for s
    by (simp add: min_elems_def D_Mndetprefix' T_Mndetprefix' subset_iff) (metis less_cons)
qed


lemma chain_Mndetprefix : ‹chain Y ⟹ chain (λi. ⊓a∈A → Y i a)›
  by (simp add: fun_belowD mono_Mndetprefix chain_def)


lemma cont_Mndetprefix_prem : ‹⊓a ∈ A → (⨆i. Y i a) = (⨆i. ⊓a ∈ A → Y i a)›
  (is ‹?lhs = ?rhs›) if ‹chain Y›
proof (subst Process_eq_spec, safe)
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (auto simp add: F_Mndetprefix' limproc_is_thelub ‹chain Y› F_LUB
        ch2ch_fun chain_Mndetprefix split: if_split_asm)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (simp add: F_Mndetprefix' limproc_is_thelub ‹chain Y› F_LUB ch2ch_fun
        chain_Mndetprefix split: if_split_asm) blast
next
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Mndetprefix' limproc_is_thelub ‹chain Y› D_LUB ch2ch_fun chain_Mndetprefix)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (simp add: D_Mndetprefix' limproc_is_thelub ‹chain Y› D_LUB ch2ch_fun chain_Mndetprefix) blast
qed


lemma Mndetprefix_cont [simp] : ‹cont (λb. ⊓a ∈ A → f a b)› if * : ‹⋀a. a ∈ A ⟹ cont (f a)›
proof -
  define g where ‹g a b ≡ if a ∈ A then f a b else undefined› for a b
  have ‹(λb. ⊓a ∈ A → f a b) = (λb. ⊓a ∈ A → g a b)›
    by (intro ext mono_Mndetprefix_eq) (simp add: g_def)
  moreover have ‹cont (λb. ⊓a ∈ A → g a b)›
  proof (rule cont_compose[where c = ‹Mndetprefix A›])
    show ‹cont (Mndetprefix A)›
    proof (rule contI2)
      show ‹monofun (Mndetprefix A)› by (simp add: fun_belowD mono_Mndetprefix monofunI)
    next
      show ‹chain Y ⟹ Mndetprefix A (⨆i. Y i) ⊑ (⨆i. Mndetprefix A (Y i))›
        for Y :: ‹nat ⇒ 'a ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
        by (simp add: cont_Mndetprefix_prem lub_fun)
    qed
  next
    show ‹cont (λb a. g a b)› 
      by (rule cont2cont_lambda, rule contI2)
        (simp_all add: cont2monofunE cont2contlubE g_def monofunI "*")
  qed
  ultimately show ‹cont (λb. ⊓a∈A → f a b)› by simp
qed


(* TODO: redo the formatting with subsections, sections, etc. *)

subsection‹ High-level Syntax for Write ›

text ‹A version with a non deterministic choice is also introduced.›

definition ndet_write :: ‹['a ⇒ 'b, 'a set, 'a ⇒ ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  where ‹ndet_write c A P ≡ Mndetprefix (c ` A) (P o (inv_into A c))›

definition "write" :: ‹['a ⇒ 'b, 'a, ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  where ‹write c a P ≡ Mprefix {c a} (λx. P)›

syntax
  "_ndet_write"   :: ‹['a ⇒ 'b, pttrn, ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  (‹(3((_)❙!❙!(_)) /→ _)› [78,78,77] 77)
  "_ndet_writeX"  :: ‹['a ⇒ 'b, pttrn, bool,('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  (‹(3((_)❙!❙!(_))❙|_ /→ _)› [78,78,78,77] 77)
  "_ndet_writeS"  :: ‹['a ⇒ 'b, pttrn, 'b set,('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('b, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k›
  (‹(3((_)❙!❙!(_))∈_ /→ _)› [78,78,78,77] 77)
  "_write" ::  ‹['a ⇒ 'b, 'a, ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k] ⇒ ('a, 'r)process⇩_p⇩_t⇩_i⇩_c⇩_k› (‹(3(_)❙!(_) /→ _)› [78,78,77] 77)


syntax_consts "_ndet_write"  ⇌ ndet_write
  and         "_ndet_writeX" ⇌ ndet_write
  and         "_ndet_writeS" ⇌ ndet_write
  and         "_write"       ⇌ "write"


translations
  "_ndet_write c p P"      ⇌ "CONST ndet_write c CONST UNIV (λp. P)"
  "_ndet_writeX c p b P"   => "CONST ndet_write c {p. b} (λp. P)"
  "_ndet_writeS c p A P"   => "CONST ndet_write c A (λp. P)"
  "_write c a P"           ⇌ "CONST write c a P"

text ‹Syntax checks.›

term ‹c❙!❙!x → P x›
term ‹c❙!❙!x∈A → P x›
term ‹c❙!❙!x❙|(0<x) → P x›

term ‹(c ∘ c')❙!❙!a∈A → d❙?b∈B → event → e❙!a' → P a b›

term ‹c❙!x → P›


lemma read_id [simp] : ‹id❙?a ∈ A → P a = □a ∈ A → P a›
  by (auto simp add: read_def intro!: mono_Mprefix_eq)
    (metis f_inv_into_f id_apply image_id)

lemma ndet_write_id [simp] : ‹id❙!❙!a ∈ A → P a = ⊓a ∈ A → P a›
  by (auto simp add: ndet_write_def intro!: mono_Mndetprefix_eq)
    (metis f_inv_into_f id_apply image_id)


lemma mono_ndet_write: ‹(⋀a. a ∈ A ⟹ P a ⊑ Q a) ⟹ (c❙!❙!a∈A → P a) ⊑ (c❙!❙!a∈A → Q a)›
  unfolding ndet_write_def by (simp add: inv_into_into mono_Mndetprefix)

lemma ndet_write_cont[simp]:
  ‹(⋀a. a ∈ A ⟹ cont (λb. P b a)) ⟹ cont (λy. c❙!❙!a∈A → P y a)›
  unfolding ndet_write_def o_def by (rule Mndetprefix_cont) (simp add: inv_into_into)


lemma mono_write: ‹P ⊑ Q ⟹ c❙!a → P ⊑ c❙!a → Q›
  unfolding write_def by (simp add: mono_Mprefix)

lemma write_cont[simp]: ‹cont P ⟹ cont (λx. c❙!a → P x)›
  unfolding write_def by simp


lemma read_singl[simp] : ‹c❙?a∈{x} → P a = c❙!x → P x›
  by (simp add: read_def Mprefix_singl write_def)

lemma ndet_write_singl[simp] : ‹c❙!❙!a∈{x} → P a = c❙!x → P x›
  by (simp add: ndet_write_def Mprefix_singl write_def)

lemma write_is_write0 : ‹c❙!x → P = c x → P›
  by (simp add: write0_def write_def)


lemma read_id_is_Mprefix : ‹read id A P = Mprefix A P›
  by (auto simp add: read_def intro!: mono_Mprefix_eq)
    (metis f_inv_into_f id_apply image_id)

lemma ndet_write_id_is_Mndetprefix : ‹ndet_write id A P = Mndetprefix A P›
  by (auto simp add: ndet_write_def intro!: mono_Mndetprefix_eq)
    (metis f_inv_into_f id_apply image_id)



(*<*)
end
  (*>*)