Theory 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       : 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 Binary Choice Operators›

section‹ Deterministic Choice ›

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

subsection‹The Det Operator Definition›

lift_definition Det :: ‹[('a, 'r)process⇩p⇩t⇩i⇩c⇩k, ('a, 'r)process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r)process⇩p⇩t⇩i⇩c⇩k› (infixl ‹[+]› 82)
  is ‹λP Q. ({(s, X). s = [] ∧ (s, X) ∈ ℱ P ∩ ℱ Q} ∪
             {(s, X). s ≠ [] ∧ (s, X) ∈ ℱ P ∪ ℱ Q} ∪
             {(s, X). s = [] ∧ s ∈ 𝒟 P ∪ 𝒟 Q} ∪
             {(s, X). ∃r. s = [] ∧ ✓(r) ∉ X ∧ [✓(r)] ∈ 𝒯 P ∪ 𝒯 Q},
             𝒟 P ∪ 𝒟 Q)›
proof -
  show ‹?thesis P Q› (is ‹is_process (?f, 𝒟 P ∪ 𝒟 Q)›) for P Q :: ‹('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: is_processT1)
  next
    show ‹(s, X) ∈ ?f ⟹ front_tickFree s› for s X
      by (auto simp: is_processT2)
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
      by (auto simp: is_processT1 dest!: is_processT3[rule_format])
  next
    show ‹(s, Y) ∈ ?f ∧ X ⊆ Y  ⟹  (s, X) ∈ ?f› for s X Y
      by (cases s; use is_processT4 in blast)
  next
    show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟹ (s, X ∪ Y) ∈ ?f› for s X Y
      by (cases s) (auto simp: is_processT5 T_F)
  next
    show ‹(s @ [✓(r)], {}) ∈ ?f ⟹ (s, X - {✓(r)}) ∈ ?f› for s r X
      apply (cases s; simp add: T_F_spec)
      by blast (metis T_F_spec append_Cons is_processT6)
  next
    show ‹s ∈ 𝒟 P ∪ 𝒟 Q ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ 𝒟 P ∪ 𝒟 Q› for s t
      by (auto simp: is_processT7)
  next
    show ‹s ∈ 𝒟 P ∪ 𝒟 Q ⟹ (s, X) ∈ ?f› for s X
      by (auto simp: is_processT8) 
  next
    show ‹s @ [✓(r)] ∈ 𝒟 P ∪ 𝒟 Q ⟹ s ∈ 𝒟 P ∪ 𝒟 Q› for s r
      by (meson UnCI UnE is_processT9)
  qed
qed

notation Det (infixl ‹□› 82)


subsection‹The Projections›

lemma F_Det :
  ‹ℱ (P □ Q) = {(s, X). s = [] ∧ (s, X) ∈ ℱ P ∩ ℱ Q} ∪
                {(s, X). s ≠ [] ∧ (s, X) ∈ ℱ P ∪ ℱ Q} ∪
                {(s, X). s = [] ∧ s ∈ 𝒟 P ∪ 𝒟 Q} ∪
                {(s, X). ∃r. s = [] ∧ ✓(r) ∉ X ∧ [✓(r)] ∈ 𝒯 P ∪ 𝒯 Q}›
  by (subst Failures.rep_eq, simp add: Det.rep_eq FAILURES_def)

lemma D_Det : ‹𝒟 (P □ Q) = 𝒟 P ∪ 𝒟 Q›
  by (subst Divergences.rep_eq, simp add: Det.rep_eq DIVERGENCES_def)

lemma T_Det : ‹𝒯 (P □ Q) = 𝒯 P ∪ 𝒯 Q›
  by (unfold Traces.rep_eq TRACES_def F_Det Failures.rep_eq[symmetric])
    (simp add: T_F F_T set_eq_iff, metis F_T T_F is_processT1)

lemmas Det_projs = F_Det D_Det T_Det



subsection‹Basic Laws›

text‹The following theorem of Commutativity helps to simplify the subsequent
continuity proof by symmetry breaking. It is therefore already developed here:›

lemma Det_commute : ‹P □ Q = Q □ P›
  by(auto simp: Process_eq_spec F_Det D_Det)

lemma Det_id [simp] : ‹P □ P = P›
  by (auto simp add: Process_eq_spec F_Det D_Det
      intro: is_processT8 is_processT6_TR_notin)



subsection‹The Continuity-Rule›

lemma mono_Det : ‹(P :: ('a, 'r)process⇩p⇩t⇩i⇩c⇩k) ⊑ P' ⟹ Q ⊑ Q' ⟹ P □ Q ⊑ P' □ Q'›
proof -
  have ‹(P :: ('a, 'r)process⇩p⇩t⇩i⇩c⇩k) □ S ⊑ Q □ S› if ‹P ⊑ Q› for P S Q
  proof (unfold le_approx_def, intro conjI impI allI subsetI)
    show ‹s ∈ 𝒟 (Q □ S) ⟹ s ∈ 𝒟 (P □ S)› for s
      apply (simp add: D_Det)
      using le_approx_imp_le_ref le_ref1 that by blast
  next
    show ‹s ∉ 𝒟 (P □ S) ⟹ ℛ⇩a (P □ S) s = ℛ⇩a (Q □ S) s› for s
      apply (cases s; simp add: D_Det Refusals_after_def F_Det set_eq_iff)
       apply (meson front_tickFree_Nil in_mono is_processT9_tick le_approx1 le_approx2T proc_ord2a that)
      using le_approx2 that by auto[1]
  next
    show ‹s ∈ min_elems (𝒟 (P □ S)) ⟹ s ∈ 𝒯 (Q □ S)› for s
      by (simp add: min_elems_def D_Det T_Det)
        (metis D_T UnCI elem_min_elems in_mono le_approx3 min_elems5 order_neq_le_trans that)
  qed

  thus ‹P ⊑ P' ⟹ Q ⊑ Q' ⟹ P □ Q ⊑ P' □ Q'›
    by (metis Det_commute below_trans)
qed


lemma chain_Det : ‹chain Y ⟹ chain (λi. Y i □ S)›
  by (simp add: po_class.chain_def mono_Det)

lemma cont_Det_prem : ‹((⨆ i. Y i) □ S) = (⨆ i. (Y i □ S))› if ‹chain Y›
proof (subst Process_eq_spec, safe)
  show ‹(s, X) ∈ ℱ (Lub Y □ S) ⟹ (s, X) ∈ ℱ (⨆i. Y i □ S)› for s X
    by (auto simp add: limproc_is_thelub F_Det D_LUB F_LUB T_LUB chain_Det ‹chain Y›)
next
  show ‹(s, X) ∈ ℱ (⨆i. Y i □ S) ⟹ (s, X) ∈ ℱ (Lub Y □ S)› for s X
    using le_approx2T[OF is_ub_thelub[OF ‹chain Y›]]
    apply (cases s; simp add: limproc_is_thelub F_Det D_LUB F_LUB T_LUB chain_Det ‹chain Y›)
    by (metis append_Nil is_processT8 is_processT9)
next
  show ‹s ∈ 𝒟 (Lub Y □ S) ⟹ s ∈ 𝒟 (⨆i. Y i □ S)›
    and ‹s ∈ 𝒟 (⨆i. Y i □ S) ⟹ s ∈ 𝒟 (Lub Y □ S)› for s
    by (simp_all add: limproc_is_thelub D_Det D_LUB chain_Det ‹chain Y›)
qed


lemma Det_cont[simp]: ‹cont (λx. f x □ g x)› if ‹cont f› and ‹cont g›
proof (rule cont_apply[where f = ‹λx g. f x □ g›])
  show ‹cont g› by (fact ‹cont g›)
next
  show ‹cont ((□) (f x))› for x
    by (rule contI2, simp add: monofun_def mono_Det)
      (subst (1 2) Det_commute, simp add: cont_Det_prem)
next
  show ‹cont (λx. f x □ y)› for y
    by (rule contI2, simp add: monofun_def mono_Det cont2monofunE ‹cont f›)
      (simp add: ch2ch_cont cont2contlubE cont_Det_prem ‹cont f›)
qed


(*<*)
end
  (*>*)