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

section‹ Non Deterministic Choice ›

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

subsection‹The Ndet Operator Definition›

lift_definition Ndet :: ‹[('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 ‹|-|› 83)
  is ‹λP Q. (ℱ P ∪ ℱ Q , 𝒟 P ∪ 𝒟 Q)›
proof -
  show ‹is_process (ℱ P ∪ ℱ Q , 𝒟 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 ‹([], {}) ∈ ℱ P ∪ ℱ Q›
      by (simp add: is_processT1)
  next
    show ‹(s, X) ∈ ℱ P ∪ ℱ Q ⟹ front_tickFree s› for s X
      by (auto intro: is_processT2)
  next
    show ‹(s @ t, {}) ∈ ℱ P ∪ ℱ Q ⟹ (s, {}) ∈ ℱ P ∪ ℱ Q› for s t
      by (auto intro: is_processT3)
  next
    show ‹(s, Y) ∈ ℱ P ∪ ℱ Q ∧ X ⊆ Y  ⟹  (s, X) ∈ ℱ P ∪ ℱ Q› for s X Y
      by (auto intro: is_processT4)
  next
    show ‹(s, X) ∈ ℱ P ∪ ℱ Q ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ℱ P ∪ ℱ Q)
          ⟹ (s, X ∪ Y) ∈ ℱ P ∪ ℱ Q› for s X Y by (auto intro: is_processT5)
  next
    show ‹(s @ [✓(r)], {}) ∈ ℱ P ∪ ℱ Q ⟹ (s, X - {✓(r)}) ∈ ℱ P ∪ ℱ Q› for s r X
      by (auto intro: is_processT6)
  next
    show ‹s ∈ 𝒟 P ∪ 𝒟 Q ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ 𝒟 P ∪ 𝒟 Q› for s t
      by (auto intro: is_processT7)
  next
    show ‹s ∈ 𝒟 P ∪ 𝒟 Q ⟹ (s, X) ∈ ℱ P ∪ ℱ Q› for s X
      by (auto intro: is_processT8) 
  next
    show ‹s @ [✓(r)] ∈ 𝒟 P ∪ 𝒟 Q ⟹ s ∈ 𝒟 P ∪ 𝒟 Q› for s r
      by (auto intro: is_processT9)
  qed
qed


notation Ndet (infixl ‹⊓› 83)


subsection ‹The Projections›

lemma F_Ndet : ‹ℱ (P ⊓ Q) = ℱ P ∪ ℱ Q›
  by (simp add: FAILURES_def Failures.rep_eq Ndet.rep_eq)

lemma D_Ndet : ‹𝒟 (P ⊓ Q) = 𝒟 P ∪ 𝒟 Q›
  by (simp add: DIVERGENCES_def Divergences.rep_eq Ndet.rep_eq)

lemma T_Ndet : ‹𝒯 (P ⊓ Q) = 𝒯 P ∪ 𝒯 Q›
  by (subst Traces.rep_eq)
    (use T_F_spec in ‹auto simp: TRACES_def Failures.rep_eq[symmetric] F_Ndet F_T›)

lemmas Ndet_projs = F_Ndet D_Ndet T_Ndet



subsection‹Basic Laws›

text ‹The commutativity of the operator helps to simplify the subsequent
      continuity proof and is therefore developed here: ›

lemma Ndet_commute: ‹P ⊓ Q = Q ⊓ P›
  by (auto simp: Process_eq_spec F_Ndet D_Ndet)

lemma Ndet_id [simp] : ‹P ⊓ P = P› by (simp add: Process_eq_spec F_Ndet D_Ndet)


subsection‹The Continuity Rule›

lemma mono_Ndet : ‹P ⊓ Q ⊑ P' ⊓ Q'› if ‹P ⊑ P'› and ‹Q ⊑ Q'›
proof (unfold le_approx_def, intro conjI allI impI)
  show ‹𝒟 (P' ⊓ Q') ⊆ 𝒟 (P ⊓ Q)› by (metis D_Ndet Un_mono le_approx1 that)
next
  show ‹s ∉ 𝒟 (P ⊓ Q) ⟹ ℛ⇩a (P ⊓ Q) s = ℛ⇩a (P' ⊓ Q') s› for s
    using that[THEN le_approx2] by (simp add: D_Ndet Refusals_after_def F_Ndet)
next
  show ‹min_elems (𝒟 (P ⊓ Q)) ⊆ 𝒯 (P' ⊓ Q')›
    using that[THEN le_approx3] by (auto simp add: min_elems_def D_Ndet T_Ndet)
qed


lemma cont_Ndet_prem : ‹(⨆ i. Y i) ⊓ S = (⨆ i. Y i ⊓ S)› if ‹chain Y›
proof -
  have ‹chain (λi. Y i ⊓ S)›
    by (rule chainI) (simp add: ‹chain Y› chainE mono_Ndet)
  with ‹chain Y› show ?thesis
    by (simp add: limproc_is_thelub Process_eq_spec D_Ndet F_Ndet F_LUB D_LUB)
qed


lemma Ndet_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_Ndet)
      (subst (1 2) Ndet_commute, simp add: cont_Ndet_prem)
next
  show ‹cont (λx. f x ⊓ y)› for y
    by (rule contI2, simp add: monofun_def mono_Ndet cont2monofunE ‹cont f›)
      (simp add: ch2ch_cont cont2contlubE cont_Ndet_prem ‹cont f›)
qed


(*<*)
end
  (*>*)