Theory Multi_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 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.
 ******************************************************************************›
(*>*)

chapter ‹ The Prefix Choice Operators ›

section‹ Multiple Deterministic Prefix Choice ›

(*<*)
theory  Multi_Deterministic_Prefix_Choice 
  imports Process 
begin 
  (*>*)

subsection‹ The Definition and some Consequences ›

lift_definition Mprefix :: ‹['a set, 'a ⇒ ('a, 'r)process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r)process⇩p⇩t⇩i⇩c⇩k›
  is ‹λA P. ({(tr, ref). tr = [] ∧ ref ∩ ev ` A = {}} ∪
             {(tr, ref). tr ≠ [] ∧ hd tr ∈ ev ` A ∧ (∃a. ev a = hd tr ∧ (tl tr, ref) ∈ ℱ (P a))},
             {d. d ≠ [] ∧ hd d ∈ ev ` A ∧ (∃a. ev a = hd d ∧ tl d ∈ 𝒟 (P a))})›
proof -
  show ‹?thesis A P› (is ‹is_process(?f, ?d)›) for P and A
  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 ⟹ front_tickFree s› for s X
      apply (cases s; simp add: image_iff)
      by (meson F_imp_front_tickFree event⇩p⇩t⇩i⇩c⇩k.disc(1) front_tickFree_Cons_iff)
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
      by (auto intro: is_processT3)
  next
    show ‹(s, Y) ∈ ?f ∧ X ⊆ Y  ⟹  (s, X) ∈ ?f› for s X Y
      by (auto intro: is_processT4)
  next
    show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟹ (s, X ∪ Y) ∈ ?f› for s X Y
      apply (cases s; simp add: disjoint_iff image_iff)
      using is_processT1 apply blast
      by (metis is_processT5)
  next
    show ‹(s @ [✓(r)], {}) ∈ ?f ⟹ (s, X - {✓(r)}) ∈ ?f› for s r X
      by (cases s) (auto intro: is_processT6)
  next
    show ‹s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ ?d› for s t
      by (cases s) (auto intro: is_processT7)
  next
    show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X
      by (auto intro: is_processT8) 
  next
    show ‹s @ [✓(r)] ∈ ?d ⟹ s ∈ ?d› for s r
      by (cases s) (auto intro: is_processT9)
  qed
qed


syntax "_Mprefix" :: ‹[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 "_Mprefix" ⇌ Mprefix
translations "□a∈A → P" ⇌ "CONST Mprefix A (λa. P)"

text‹Syntax Check:›
term ‹□x∈A → □y∈A → □z∈A → P z x y = Q›


subsection ‹ Projections in Prefix ›

lemma F_Mprefix : 
  "ℱ (□a ∈ A → P a) = {([], X)| X. X ∩ ev ` A = {}} ∪
                         {(ev a # s, X)| a s X. a ∈ A ∧ (s, X) ∈ ℱ (P a)}"
  by (subst Failures.rep_eq, auto simp add: Mprefix.rep_eq FAILURES_def)
    (metis list.collapse)

lemma D_Mprefix: ‹𝒟 (□a ∈ A → P a) = {ev a # s| a s. a ∈ A ∧ s ∈ 𝒟 (P a)}›
  by (subst Divergences.rep_eq, auto simp add: Mprefix.rep_eq DIVERGENCES_def)
    (metis list.collapse)

lemma T_Mprefix: ‹𝒯 (□a ∈ A → P a) = insert [] {ev a # s| a s. a ∈ A ∧ s ∈ 𝒯 (P a)}›
  by (subst Traces.rep_eq, auto simp add: TRACES_def Failures.rep_eq[symmetric] F_Mprefix)
    (use F_T T_F in blast)+

lemmas Mprefix_projs = F_Mprefix D_Mprefix T_Mprefix


lemma mono_Mprefix_eq: ‹(⋀a. a ∈ A ⟹ P a = Q a) ⟹ Mprefix A P = Mprefix A Q›
  by (subst Process_eq_spec) (auto simp add: F_Mprefix D_Mprefix)


subsection ‹ Basic Properties ›

lemma tick_notin_T_Mprefix [simp]: ‹[✓(r)] ∉ 𝒯 (□x ∈ A → P x)›
  by (simp add: T_Mprefix)


lemma Nil_notin_D_Mprefix [simp]: ‹[] ∉ 𝒟 (□x ∈ A → P x)›
  by (simp add: D_Mprefix)

subsection‹ Proof of Continuity Rule ›

subsubsection‹ Backpatch Isabelle 2009-1›

―‹re-introduced from Isabelle/HOLCF 2009-1; clearly
   a derived concept, but still a useful shortcut›

(* TODO really useful ? *)

definition
  contlub :: "('a::cpo ⇒ 'b::cpo) ⇒ bool" 
  where
    "contlub f = (∀Y. chain Y ⟶ f (⨆ i. Y i) = (⨆ i. f (Y i)))"

lemma contlubE:
  "⟦contlub f; chain Y⟧ ⟹ f (⨆ i. Y i) = (⨆ i. f (Y i))"
  by (simp add: contlub_def)


lemma monocontlub2cont: "⟦monofun f; contlub f⟧ ⟹ cont f"
  apply (rule contI)
  apply (rule thelubE)
   apply (erule (1) ch2ch_monofun)
  apply (erule (1) contlubE [symmetric])
  done

lemma contlubI:
  "(⋀Y. chain Y ⟹ f (⨆ i. Y i) = (⨆ i. f (Y i))) ⟹ contlub f"
  by (simp add: contlub_def)


lemma cont2contlub: "cont f ⟹ contlub f"
  apply (rule contlubI)
  apply (rule po_class.lub_eqI [symmetric])
  apply (erule (1) contE)
  done


subsubsection‹ Core of Proof  ›

lemma mono_Mprefix : ‹□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_Mprefix)
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_Mprefix F_Mprefix)
next
  from that[THEN le_approx3] show ‹s ∈ min_elems (𝒟 ?P) ⟹ s ∈ 𝒯 ?Q› for s
    by (simp add: min_elems_def D_Mprefix T_Mprefix subset_iff) (metis less_cons)
qed


lemma chain_Mprefix : ‹chain Y ⟹ chain (λi. □a∈A → Y i a)›
  by (simp add: fun_belowD mono_Mprefix chain_def)


lemma cont_Mprefix_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_Mprefix limproc_is_thelub ‹chain Y› F_LUB ch2ch_fun chain_Mprefix)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (simp add: F_Mprefix limproc_is_thelub ‹chain Y› F_LUB ch2ch_fun chain_Mprefix) blast
next
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Mprefix limproc_is_thelub ‹chain Y› D_LUB ch2ch_fun chain_Mprefix)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (simp add: D_Mprefix limproc_is_thelub ‹chain Y› D_LUB ch2ch_fun chain_Mprefix) blast
qed


lemma Mprefix_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_Mprefix_eq) (simp add: g_def)
  moreover have ‹cont (λb. □a ∈ A → g a b)›
  proof (rule cont_compose[where c = ‹Mprefix A›])
    show ‹cont (Mprefix A)›
    proof (rule contI2)
      show ‹monofun (Mprefix A)› by (simp add: fun_belowD mono_Mprefix monofunI)
    next
      show ‹chain Y ⟹ Mprefix A (⨆i. Y i) ⊑ (⨆i. Mprefix A (Y i))›
        for Y :: ‹nat ⇒ 'a ⇒ ('a, 'r)process⇩p⇩t⇩i⇩c⇩k›
        by (simp add: cont_Mprefix_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



subsection‹ High-level Syntax for Read and Write0›

text‹ The following syntax introduces the usual channel notation for CSP.
Slightly deviating from conventional wisdom, we view a channel not as a tag in
a pair, rather than as a function of type @{typ "'a⇒'b"}. This paves the way
for \emph{typed} channels over a common universe of events. ›

definition read :: ‹['a ⇒ 'b, 'a set, 'a ⇒ ('b, 'r)process⇩p⇩t⇩i⇩c⇩k] ⇒ ('b, 'r)process⇩p⇩t⇩i⇩c⇩k›
  where ‹read c A P  ≡ Mprefix (c ` A) (P ∘ (inv_into A c))›

definition write0 :: ‹['a, ('a, 'r)process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r)process⇩p⇩t⇩i⇩c⇩k› (infixr ‹→› 77)
  where ‹write0 a P ≡ Mprefix {a} (λx. P)›


subsection‹CSP$_M$-Style Syntax for Communication Primitives›

syntax
  "_read" :: ‹['a ⇒ 'b, pttrn, ('b, 'r)process⇩p⇩t⇩i⇩c⇩k] ⇒ ('b, 'r)process⇩p⇩t⇩i⇩c⇩k›
  (‹(3((_)❙?(_)) /→ _)› [78,78,77] 77)
  "_readX"  :: ‹['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)
  "_readS"  :: ‹['a ⇒ 'b, pttrn, 'a set, ('b, 'r)process⇩p⇩t⇩i⇩c⇩k] ⇒ ('b, 'r)process⇩p⇩t⇩i⇩c⇩k›
  (‹(3((_)❙?(_))∈_ /→ _)› [78,78,78,77] 77)
  (* "_write0" :: ‹['a, ('a, 'r)process⇩p⇩t⇩i⇩c⇩k] => ('a, 'r)process⇩p⇩t⇩i⇩c⇩k›  *)

translations
  "_read c p P"      ⇌ "CONST read c CONST UNIV (λp. P)"
  "_readX c p b P"   => "CONST read c {p. b} (λp. P)"
  (* "_write0 a P"      ⇌ "CONST write0 a P" *)
  "_readS c p A P"   => "CONST read c A (λp. P)"

syntax_consts "_read"  ⇌ read
  and         "_readX" ⇌ read
  and         "_readS" ⇌ read




text‹Syntax Check:›

term ‹a → P›

term ‹c❙?x → d❙?y → P a y›
term ‹c❙?x∈X → P x›
term ‹c❙?x❙|(x<0) → P x›

term ‹c❙?x → d❙?y∈B → e → u❙?t❙|(t ≥ 1) → P a y›

term ‹(c ∘ d)❙?a → P a›



lemma mono_write0 : ‹P ⊑ Q ⟹ a → P ⊑ a → Q›
  unfolding write0_def by (simp add: mono_Mprefix)

lemma mono_read : ‹(⋀a. a ∈ A ⟹ P a ⊑ Q a) ⟹ c❙?a∈A → P a ⊑ c❙?a∈A → Q a›
  unfolding read_def by (simp add: inv_into_into mono_Mprefix)


lemma read_cont[simp]:
  ‹(⋀a. a ∈ A ⟹ cont (λb. P b a)) ⟹ cont (λy. read c A (P y))›
  unfolding read_def o_def by (rule Mprefix_cont) (simp add: inv_into_into)

lemma read_cont'[simp]: ‹cont P ⟹ cont (λy. read c A (P y))›
  unfolding read_def o_def by (rule Mprefix_cont, rule cont2cont_fun)



lemma read_cont''[simp]: ‹(⋀a. cont (f a)) ⟹ cont (λy. c❙?x → f x y)› by simp


lemma write0_cont[simp]: ‹cont (P::('b::cpo ⇒ ('a, 'r)process⇩p⇩t⇩i⇩c⇩k)) ⟹ cont(λx. a → P x)›
  by (simp add: write0_def)


lemma Mprefix_singl : ‹□x ∈ {a} → P x = a → P a› 
  by (auto simp add: Process_eq_spec write0_def Mprefix_projs)

(*<*)
end
  (*>*)