Theory Step_CSP_Laws_Extended

(*<*)
―‹ ********************************************************************
 * 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       : Extension of the step laws
 *
 * 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‹ Extension of the Step-Laws ›

(*<*)
theory Step_CSP_Laws_Extended                                               
  imports Basic_CSP_Laws Step_CSP_Laws Non_Deterministic_CSP_Distributivity
begin 
  (*>*)

subsection ‹Derived step-laws for \<^const>‹Sync››

lemma Mprefix_Inter_Mprefix :
  ‹□a∈A → P a ||| □b∈B → Q b = (□a∈A → (P a ||| □b∈B → Q b)) □ (□b∈B → (□a ∈ A → P a ||| Q b))›
  by (fact Mprefix_Sync_Mprefix[where S = ‹{}›, simplified])

lemma Mprefix_Par_Mprefix : ‹□a∈A → P a || □b∈B → Q b = □x∈(A ∩ B) → (P x || Q x)›
  by (fact Mprefix_Sync_Mprefix[where S = ‹UNIV›, simplified])

lemma Mprefix_Sync_Mprefix_subset :
  ‹⟦A ⊆ S; B ⊆ S⟧ ⟹ Mprefix A P ⟦S⟧ Mprefix B Q = □x∈(A ∩ B) → (P x ⟦S⟧ Q x)›
  by (fact Mprefix_Sync_Mprefix_bis[of ‹{}› S A ‹{}› B, simplified])

lemma Mprefix_Sync_Mprefix_indep :
  ‹A ∩ S = {} ⟹ B ∩ S = {} ⟹
   Mprefix A P ⟦S⟧ Mprefix B Q = (□a∈A → (P a ⟦S⟧ Mprefix B Q)) □ (□b∈B → (Mprefix A P ⟦S⟧ Q b))›
  by (fact Mprefix_Sync_Mprefix_bis[of A S ‹{}› B ‹{}›, simplified])

lemma Mprefix_Sync_Mprefix_left :
  ‹A ∩ S = {} ⟹ B ⊆ S ⟹ Mprefix A P ⟦S⟧ Mprefix B Q = □a∈A → (P a ⟦S⟧ Mprefix B Q)›
  by (fact Mprefix_Sync_Mprefix_bis[of A S ‹{}› ‹{}› B, simplified])

lemma Mprefix_Sync_Mprefix_right :
  ‹A ⊆ S ⟹ B ∩ S = {} ⟹ Mprefix A P ⟦S⟧ Mprefix B Q = □b∈B → (Mprefix A P ⟦S⟧ Q b)›
  by (fact Mprefix_Sync_Mprefix_bis[of ‹{}› S A B ‹{}›, simplified])


lemma Mprefix_Sync_STOP : ‹(□a ∈ A → P a) ⟦S⟧ STOP = □a ∈ (A - S) → (P a ⟦S⟧ STOP)›
  by (subst Mprefix_empty[symmetric], subst Mprefix_Sync_Mprefix, simp)

lemma STOP_Sync_Mprefix : ‹STOP ⟦S⟧ (□b ∈ B → Q b) = □b ∈ (B - S) → (STOP ⟦S⟧ Q b)›
  by (metis (no_types, lifting) Mprefix_Sync_STOP Sync_commute mono_Mprefix_eq)




paragraph ‹Mixing deterministic and non deterministic prefix choices›

lemma Mndetprefix_Sync_Mprefix :
  ‹(⊓a ∈ A → P a) ⟦S⟧ (□b ∈ B → Q b) =
   (  if A = {} then STOP ⟦S⟧ (□b ∈ B → Q b)
    else ⊓a∈A. (if a ∈ S then STOP else (a → (P a ⟦S⟧ (□b ∈ B → Q b)))) □
                (□b∈(B - S) → ((a → P a) ⟦S⟧ Q b)) □
                (if a ∈ B ∩ S then (a → (P a ⟦S⟧ Q a)) else STOP))›
  by (unfold Mndetprefix_GlobalNdet Sync_distrib_GlobalNdet_right
      write0_def Mprefix_Sync_Mprefix)
    (auto simp add: Mprefix_singl insert_Diff_if Int_insert_left
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›] mono_Mprefix_eq)

lemma Mprefix_Sync_Mndetprefix :
  ‹(□a ∈ A → P a) ⟦S⟧ (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a) ⟦S⟧ STOP
    else ⊓b∈B. (if b ∈ S then STOP else (b → ((□a ∈ A → P a) ⟦S⟧ Q b))) □
                (□a∈(A - S) → (P a ⟦S⟧ (b → Q b))) □
                (if b ∈ A ∩ S then (b → (P b ⟦S⟧ Q b)) else STOP))›
  by (subst (1 2 3 4 5) Sync_commute) (simp add: Mndetprefix_Sync_Mprefix)


text ‹In particular, we can obtain the theorem for \<^const>‹Mndetprefix› synchronized with \<^const>‹STOP›.›

lemma Mndetprefix_Sync_STOP :
  ‹(⊓a ∈ A → P a) ⟦S⟧ STOP =
   (  if A ∩ S = {} then ⊓a ∈ A → (P a ⟦S⟧ STOP)
    else (⊓a ∈ (A - S) → (P a ⟦S⟧ STOP)) ⊓ STOP)›
  (is ‹?lhs = (if A ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)›)
proof -
  have ‹(⊓a ∈ A → P a) ⟦S⟧ STOP =
        ⊓a∈A. (if a ∈ S then STOP else (a → (P a ⟦S⟧ STOP)))› (is ‹?lhs = ?rhs'›)
    by (subst Mndetprefix_Sync_Mprefix[where B = ‹{}›, simplified])
      (auto intro: mono_GlobalNdet_eq)
  also have ‹?rhs' = (if A ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)›
  proof (split if_split, intro conjI impI)
    show ‹A ∩ S = {} ⟹ ?rhs' = ?rhs1›
      by (auto simp add: Mndetprefix_GlobalNdet intro!: mono_GlobalNdet_eq)
  next
    show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹A ∩ S ≠ {}›
    proof (cases ‹A - S = {}›)
      show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹A - S = {}›
        by (simp add: ‹A - S = {}› GlobalNdet_is_STOP_iff)
          (use ‹A - S = {}› in blast)
    next
      show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹A - S ≠ {}›
      proof (subst Int_Diff_Un[symmetric],
          subst GlobalNdet_factorization_union
          [OF ‹A ∩ S ≠ {}› ‹A - S ≠ {}›, symmetric])
        have ‹(⊓a∈(A ∩ S). (if a ∈ S then STOP else (a → (P a ⟦S⟧ STOP))))
              = STOP› (is ‹?fact1 = STOP›)
          by (simp add: GlobalNdet_is_STOP_iff)
        moreover have ‹(⊓a∈(A - S). (if a ∈ S then STOP else (a → (P a ⟦S⟧ STOP))))
                       = ?rhs2› (is ‹?fact2 = ?rhs2›)
          by (auto simp add: Mndetprefix_GlobalNdet intro: mono_GlobalNdet_eq)
        ultimately show ‹?fact1 ⊓ ?fact2 = ?rhs2 ⊓ STOP› by (simp add: Ndet_commute)
      qed
    qed
  qed
  finally show ‹?lhs = (if A ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)› .
qed

corollary STOP_Sync_Mndetprefix :
  ‹STOP ⟦S⟧ (⊓b ∈ B → Q b)  =
   (  if B ∩ S = {} then ⊓b ∈ B → (STOP ⟦S⟧ Q b)
    else (⊓b ∈ (B - S) → (STOP ⟦S⟧ Q b)) ⊓ STOP)›
  by (subst (1 2 3) Sync_commute) (simp add: Mndetprefix_Sync_STOP)

(* (  if A = {} then STOP ⟦S⟧ (□b ∈ B → Q b)
    else ⊓a∈A. (if a ∈ B then (a → (P a ⟦S⟧ Q a)) else STOP)) *)

corollary Mndetprefix_Sync_Mprefix_subset :
  ‹(⊓a ∈ A → P a) ⟦S⟧ (□b ∈ B → Q b) =
   (  if A ⊆ B then ⊓ a ∈ A → (P a ⟦S⟧ Q a)
    else (⊓a ∈ (A ∩ B) → (P a ⟦S⟧ Q a)) ⊓ STOP)›
  (is ‹?lhs = (if A ⊆ B then ?rhs1 else ?rhs2)›) if ‹A ⊆ S› ‹B ⊆ S›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?lhs = (if A ⊆ B then ?rhs1 else ?rhs2)›
    by (simp add: Mprefix_is_STOP_iff STOP_Sync_Mprefix ‹B ⊆ S›)
next
  from ‹A ⊆ S› have  * : ‹a ∈ A ⟹ a ∈ S› for a by blast
  from ‹B ⊆ S› have ** : ‹B - S = {}› ‹a ∈ B ∧ a ∈ S ⟷ a ∈ B› for a by auto
  assume ‹A ≠ {}›
  have ‹?lhs = ⊓a∈A. (if a ∈ B then (a → (P a ⟦S⟧ Q a)) else STOP)› (is ‹?lhs = ?rhs'›)
    by (auto simp add: Mndetprefix_Sync_Mprefix "*" "**" ‹A ≠ {}› intro: mono_GlobalNdet_eq)
  also have ‹?rhs' = (if A ⊆ B then ?rhs1 else ?rhs2)›
  proof (split if_split, intro conjI impI)
    show ‹A ⊆ B ⟹ ?rhs' = ⊓a∈A → (P a ⟦S⟧ Q a)›
      by (auto simp add: Mndetprefix_GlobalNdet intro!: mono_GlobalNdet_eq)
  next
    show ‹?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧ Q a)) ⊓ STOP› if ‹¬ A ⊆ B›
    proof (cases ‹A ∩ B = {}›)
      show ‹A ∩ B = {} ⟹ ?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧ Q a)) ⊓ STOP›
        by (auto simp add: GlobalNdet_is_STOP_iff)
    next
      assume ‹A ∩ B ≠ {}›
      from ‹¬ A ⊆ B› have ‹A - B ≠ {}› by blast
      show ‹?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧ Q a)) ⊓ STOP›
        by (auto simp add: Mndetprefix_GlobalNdet GlobalNdet_is_STOP_iff
            simp flip: GlobalNdet_factorization_union
            [OF ‹A ∩ B ≠ {}› ‹A - B ≠ {}›, unfolded Int_Diff_Un]
            intro!: arg_cong2[where f = ‹(⊓)›] mono_GlobalNdet_eq)
    qed
  qed
  finally show ‹?lhs = (if A ⊆ B then ?rhs1 else ?rhs2)› by simp
qed


corollary Mprefix_Sync_Mndetprefix_subset :
  ‹A ⊆ S ⟹ B ⊆ S ⟹
   □a ∈ A → P a ⟦S⟧ ⊓b ∈ B → Q b =
   (  if B ⊆ A then ⊓b ∈ B → (P b ⟦S⟧ Q b)
    else (⊓b ∈ (A ∩ B) → (P b ⟦S⟧ Q b)) ⊓ STOP)›
  by (subst (1 2 3) Sync_commute) (simp add: Mndetprefix_Sync_Mprefix_subset Int_commute)



corollary Mndetprefix_Sync_Mprefix_indep :
  ‹(⊓a ∈ A → P a) ⟦S⟧ (□b ∈ B → Q b) =
   (  if A = {} then □b∈B → (STOP ⟦S⟧ Q b)
    else ⊓a∈A. (a → (P a ⟦S⟧ (□b ∈ B → Q b))) □
                (□b∈B → ((a → P a) ⟦S⟧ Q b)))›
  if ‹A ∩ S = {}› and ‹B ∩ S = {}›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?thesis›
    by (simp add: Diff_triv STOP_Sync_Mprefix ‹B ∩ S = {}›)
next
  from that(1) have   * : ‹a ∈ A ⟹ a ∉ S› for a by blast
  from that(2) have  ** : ‹a ∈ B ∧ a ∈ S ⟷ False› for a by blast
  from that(2) have *** : ‹B - S = B› by blast
  show ?thesis if ‹A ≠ {}›
    by (simp add: Mndetprefix_Sync_Mprefix ‹A ≠ {}›)   
      (rule mono_GlobalNdet_eq, simp add: "*" "**" "***")
qed

corollary Mprefix_Sync_Mndetprefix_indep :
  ‹A ∩ S = {} ⟹ B ∩ S = {} ⟹
   (□a ∈ A → P a) ⟦S⟧ (⊓b ∈ B → Q b) =
   (  if B = {} then □a ∈ A → (P a ⟦S⟧ STOP)
    else ⊓b∈B. (b → ((□a ∈ A → P a) ⟦S⟧ Q b)) □
                (□a∈A → (P a ⟦S⟧ (b → Q b))))›
  by (subst (1 2 3 4) Sync_commute) (simp add: Mndetprefix_Sync_Mprefix_indep)


corollary Mndetprefix_Sync_Mprefix_left :
  ‹(⊓a ∈ A → P a) ⟦S⟧ (□b ∈ B → Q b) =
   (  if A = {} then STOP ⟦S⟧ (□b ∈ B → Q b)
    else ⊓a∈A → (P a ⟦S⟧ (□b ∈ B → Q b)))›
  if ‹A ∩ S = {}› and ‹B ⊆ S›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?thesis› by simp
next
  from that(1) have   * : ‹a ∈ A ⟹ a ∉ S› for a by blast
  from that(2) have  ** : ‹B - S = {}› by blast
  show ?thesis if ‹A ≠ {}›
    by (simp add: Mndetprefix_Sync_Mprefix ‹A ≠ {}›, unfold Mndetprefix_GlobalNdet)
      (rule mono_GlobalNdet_eq, simp add: "*" "**")
qed

corollary Mndetprefix_Sync_Mprefix_right :
  ‹(⊓a ∈ A → P a) ⟦S⟧ (□b ∈ B → Q b) =
   (  if A = {} then STOP ⟦S⟧ (□b ∈ B → Q b)
    else □b∈B → ((⊓a∈A → P a) ⟦S⟧ Q b))›
  if ‹A ⊆ S› and ‹B ∩ S = {}›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?thesis› by simp
next
  from that(1) have   * : ‹a ∈ A ⟹ a ∈ S› for a by blast
  from that(2) have  ** : ‹B - S = B› by blast
  show ?thesis if ‹A ≠ {}›
    by (simp add: Mndetprefix_Sync_Mprefix ‹A ≠ {}›,
        simp add: Mndetprefix_GlobalNdet Sync_distrib_GlobalNdet_right ‹A ≠ {}›
        flip: GlobalNdet_Mprefix_distr)
      (rule mono_GlobalNdet_eq, use "*" "**" in auto)
qed


corollary Mprefix_Sync_Mndetprefix_left :
  ‹A ∩ S = {}  ⟹ B ⊆ S ⟹
   (□a ∈ A → P a) ⟦S⟧ (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a) ⟦S⟧ STOP
    else □a∈A → (P a ⟦S⟧ (⊓b ∈ B → Q b)))›
  by (subst (1 2 3) Sync_commute) (simp add: Mndetprefix_Sync_Mprefix_right)

corollary Mprefix_Sync_Mndetprefix_right :
  ‹A ⊆ S ⟹ B ∩ S = {} ⟹
   (□a ∈ A → P a) ⟦S⟧ (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a) ⟦S⟧ STOP
    else ⊓b∈B → ((□a ∈ A → P a) ⟦S⟧ Q b))›
  by (subst (1 2 3) Sync_commute) (simp add: Mndetprefix_Sync_Mprefix_left)



corollary Mndetprefix_Par_Mprefix :
  ‹⊓a ∈ A → P a || □b ∈ B → Q b =
   (if A ⊆ B then ⊓a ∈ A → (P a || Q a) else (⊓a ∈ (A ∩ B) → (P a || Q a)) ⊓ STOP)›
  by (simp add: Mndetprefix_Sync_Mprefix_subset)

corollary Mprefix_Par_Mndetprefix :
  ‹□a ∈ A → P a || ⊓b ∈ B → Q b =
   (if B ⊆ A then ⊓b ∈ B → (P b || Q b) else (⊓b ∈ (A ∩ B) → (P b || Q b)) ⊓ STOP)›
  by (simp add: Mprefix_Sync_Mndetprefix_subset)


corollary Mndetprefix_Inter_Mprefix :
  ‹(⊓a ∈ A → P a) ||| (□b ∈ B → Q b) =
   (  if A = {} then (□b ∈ B → Q b ❙; STOP)
    else ⊓a∈A. (a → (P a ||| (□b ∈ B → Q b))) □
                (□b∈B → ((a → P a) ||| Q b)))›
  by (simp add: Mndetprefix_Sync_Mprefix_indep Mprefix_Seq)

corollary Mprefix_Inter_Mndetprefix :
  ‹(□a ∈ A → P a) ||| (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a ❙; STOP)
    else ⊓b∈B. (b → ((□a ∈ A → P a) ||| Q b)) □
                (□a∈A → (P a ||| (b → Q b))))›
  by (simp add: Mprefix_Sync_Mndetprefix_indep Mprefix_Seq)



subsection ‹Non deterministic step-laws›

text ‹The \<^const>‹Mndetprefix› operator slightly differs
      from \<^const>‹Mprefix› so we can often adapt the step-laws.›

lemma Mndetprefix_Ndet_Mndetprefix :
  ― ‹We assume \<^term>‹A ∩ B ≠ {}›, otherwise this rewriting rule is not interesting.›
  ‹(⊓a ∈ A → P a) ⊓ (⊓b ∈ B → Q b) =
   (  if A = B then ⊓b ∈ B → P b ⊓ Q b
    else   if A ⊆ B then (⊓b ∈ (B - A) → Q b) ⊓ (⊓x ∈ A → P x ⊓ Q x)
         else   if B ⊆ A then (⊓a ∈ (A - B) → P a) ⊓ (⊓x ∈ B → P x ⊓ Q x)
              else (⊓a ∈ (A - B) → P a) ⊓ (⊓b ∈ (B - A) → Q b) ⊓ (⊓x ∈ (A ∩ B) → P x ⊓ Q x))›
  (is ‹?lhs = (if A = B then ?rhs1 else if A ⊆ B then ?rhs2 else if B ⊆ A then ?rhs3 else ?rhs4)›)
  if ‹A ∩ B ≠ {}›
proof (split if_split, intro conjI impI)
  show ‹A = B ⟹ ?lhs = ?rhs1› by (simp add: Mndetprefix_distrib_Ndet)
next
  show ‹?lhs = (if A ⊆ B then ?rhs2 else if B ⊆ A then ?rhs3 else ?rhs4)› if ‹A ≠ B›
  proof (split if_split, intro conjI impI)
    from ‹A ∩ B ≠ {}› ‹A ≠ B› show ‹A ⊆ B ⟹ ?lhs = ?rhs2›
      by (simp add: Process_eq_spec Ndet_projs STOP_projs Mndetprefix_projs, safe, auto)
  next
    show ‹?lhs = (if B ⊆ A then ?rhs3 else ?rhs4)› if ‹¬ A ⊆ B›
    proof (split if_split, intro conjI impI)
      from ‹A ≠ B› show ‹B ⊆ A ⟹ ?lhs = ?rhs3›
        by (simp add: Process_eq_spec Ndet_projs STOP_projs Mndetprefix_projs, safe, auto)
    next
      from ‹A ∩ B ≠ {}› ‹¬ A ⊆ B› show ‹¬ B ⊆ A ⟹ ?lhs = ?rhs4›
        by (simp add: Process_eq_spec Ndet_projs STOP_projs Mndetprefix_projs, safe, auto)
    qed
  qed
qed

lemma Mndetprefix_Det_Mndetprefix :
  ‹(⊓a∈ A → P a) □ (⊓b ∈ B → Q b) =
   (if A = {} then ⊓b ∈ B → Q b else if B = {} then ⊓a ∈ A → P a
    else ⊓a ∈ A. ⊓b ∈ B. (if a = b then a → P a ⊓ Q a else (a → P a) □ (b → Q b)))›
  (is ‹?lhs = (if A = {} then ?rhs1 else if B = {} then ?rhs2 else ?rhs3)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = ?rhs1› by simp
next
  show ‹?lhs = (if B = {} then ?rhs2 else ?rhs3)› if ‹A ≠ {}›
  proof (split if_split, intro conjI impI)
    show ‹B = {} ⟹ ?lhs = ?rhs2› by simp
  next
    from ‹A ≠ {}› show ‹B ≠ {} ⟹ ?lhs = ?rhs3›
      by (auto simp add: Mndetprefix_GlobalNdet Det_distrib_GlobalNdet_left
          Det_distrib_GlobalNdet_right GlobalNdet_sets_commute[of A]
          intro!: mono_GlobalNdet_eq split: if_split_asm)
        (simp add: Process_eq_spec Det_projs write0_def Mprefix_projs Ndet_projs, safe, auto)
  qed
qed

lemma FD_Mndetprefix_Det_Mndetprefix : 
  ‹⊓x∈(A ∪ B) → (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)
   ⊑⇩F⇩D (⊓a∈ A → P a) □ (⊓b ∈ B → Q b)›
  (is ‹?lhs ⊑⇩F⇩D ?rhs›)
proof (rule failure_divergence_refineI)
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Det D_Ndet D_Mndetprefix')
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s) (auto simp add: F_Det F_Ndet Mndetprefix_projs split: if_split_asm)
qed



lemma FD_Mndetprefix_Sliding_Mndetprefix :
  ‹(⊓x ∈ (A ∪ B) → (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)) ⊓
   (⊓b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b)) ⊑⇩F⇩D
   (⊓a∈ A → P a) ⊳ (⊓b ∈ B → Q b)› (is ‹?lhs ⊑⇩F⇩D ?rhs›)
proof (rule failure_divergence_refineI)
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Sliding D_Ndet D_Mndetprefix')
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s) (auto simp add: F_Sliding F_Ndet Mndetprefix_projs split: if_split_asm)
qed


lemma Mndetprefix_Sliding_superset_Mndetprefix :
  ‹(⊓a∈ A → P a) ⊳ (⊓b ∈ B → Q b) =
   ⊓b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b)›
  (is ‹?lhs = ?rhs›) if ‹A ⊆ B›
proof (subst Process_eq_spec, safe)
  from ‹A ⊆ B› show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Sliding D_Ndet D_Mndetprefix')
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Sliding D_Ndet D_Mndetprefix' split: if_split_asm)
next
  from ‹A ⊆ B› show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s) (auto simp add: F_Sliding F_Ndet Mndetprefix_projs split: if_split_asm)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s) (auto simp add: F_Sliding F_Ndet Mndetprefix_projs split: if_split_asm)
qed

corollary Mndetprefix_Sliding_same_set_Mndetprefix :
  ‹(⊓a∈ A → P a) ⊳ (⊓a ∈ A → Q a) = ⊓a ∈ A → P a ⊓ Q a›
  by (simp add: Mndetprefix_Sliding_superset_Mndetprefix)
    (rule mono_Mndetprefix_eq, simp)





lemma Renaming_Mndetprefix :
  ‹Renaming (⊓a ∈ A → P a) f g = ⊓b ∈ f ` A → ⊓a ∈ {a ∈ A. b = f a}. Renaming (P a) f g›
proof -
  have * : ‹A = (⋃b ∈ f ` A. {a ∈ A. b = f a})› by auto
  have ** : ‹{b ∈ f ` A. {a ∈ A. b = f a} ≠ {}} = f ` A› by auto
  have ‹Renaming (⊓a ∈ A → P a) f g = ⊓a ∈ A. (f a → Renaming (P a) f g)›
    by (auto simp add: Mndetprefix_GlobalNdet Renaming_distrib_GlobalNdet write0_def Renaming_Mprefix
        intro!: mono_GlobalNdet_eq mono_Mprefix_eq)
  also have ‹… = ⊓b ∈ f ` A. ⊓a ∈ {a ∈ A. b = f a}. (f a → Renaming (P a) f g)›
    by (subst "*", subst GlobalNdet_Union, subst "**", fact refl)
  also have ‹… = ⊓b ∈ f ` A. (b → (⊓a ∈ {a ∈ A. b = f a}. Renaming (P a) f g))›
    by (rule mono_GlobalNdet_eq, subst write0_GlobalNdet)
      (auto intro: mono_GlobalNdet_eq)
  also have ‹… = ⊓b ∈ f ` A → ⊓a ∈ {a ∈ A. b = f a}. Renaming (P a) f g›
    by (simp add: Mndetprefix_GlobalNdet)
  finally show ‹Renaming (⊓a ∈ A → P a) f g = …› .
qed


lemma Mndetprefix_Seq : ‹⊓a ∈ A → P a ❙; Q = ⊓a ∈ A → (P a ❙; Q)›
  by (simp add: Mndetprefix_GlobalNdet Seq_distrib_GlobalNdet_right)
    (rule mono_GlobalNdet_eq, simp add: write0_def Mprefix_Seq)



text ‹For \<^const>‹Hiding›, we can not use the distributivity of
      \<^const>‹GlobalNdet› since it is only working for finite non determinism.
      But we can still reuse some previous results in the following proof.›

theorem Hiding_Mndetprefix_disjoint : 
  ‹⊓a ∈ A → P a \ S = ⊓a ∈ A → (P a \ S)› (is ‹?lhs = ?rhs›) if ‹A ∩ S = {}›
proof (subst Process_eq_spec_optimized, safe)
  have ‹𝒟 ?lhs = 𝒟 (□a ∈ A → P a \ S)›
    by (simp add: D_Hiding_seqRun Mndetprefix_projs Mprefix_projs)
  also have ‹… = 𝒟 (□a ∈ A → (P a \ S))› 
    by (simp add: Hiding_Mprefix_disjoint ‹A ∩ S = {}›)
  also have ‹… = 𝒟 ?rhs›
    by (simp add: D_Mndetprefix' D_Mprefix)
  finally show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s by simp_all
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  fix s X assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (⊓a ∈ A → P a)›
    unfolding F_Hiding_seqRun D_Hiding_seqRun by blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    fix t assume * : ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (⊓a ∈ A → P a)›
    show ‹(s, X) ∈ ℱ ?rhs›
    proof (cases ‹t = []›)
      from "*" show ‹t = [] ⟹ (s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Mndetprefix' split: if_split_asm)
    next
      assume ‹t ≠ []›
      with "*"(2) have ‹(t, X ∪ ev ` S) ∈ ℱ (□a ∈ A → P a)›
        by (simp add: F_Mprefix F_Mndetprefix' split: if_split_asm)
      with "*"(1) have ‹(s, X) ∈ ℱ (□a ∈ A → P a \ S)›
        unfolding F_Hiding by blast
      hence ‹(s, X) ∈ ℱ (□a ∈ A → (P a \ S))›
        by (simp add: Hiding_Mprefix_disjoint ‹A ∩ S = {}›)
      thus ‹(s, X) ∈ ℱ ?rhs› by (auto simp add: F_Mprefix F_Mndetprefix')
    qed
  qed
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›    
  show ‹(s, X) ∈ ℱ ?lhs› if ‹(s, X) ∈ ℱ ?rhs› for s X
  proof (cases ‹s = []›)
    assume ‹s = []›
    with ‹(s, X) ∈ ℱ ?rhs› have ‹A = {} ∨ (∃a ∈ A. ev a ∉ X)›
      by (simp add: F_Mndetprefix' split: if_split_asm)
    with ‹A ∩ S = {}› show ‹s = [] ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: Mndetprefix_projs F_Hiding_seqRun disjoint_iff)
        (metis (no_types, lifting) event⇩p⇩t⇩i⇩c⇩k.inject(1) filter.simps(1) imageE)
  next
    assume ‹s ≠ []›
    with ‹(s, X) ∈ ℱ ?rhs› have ‹(s, X) ∈ ℱ (□a ∈ A → (P a \ S))›
      by (simp add: F_Mprefix F_Mndetprefix' split: if_split_asm)
    hence ‹(s, X) ∈ ℱ (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_disjoint ‹A ∩ S = {}›)
    then consider ‹s ∈ 𝒟 (□a ∈ A → P a \ S)›
      | t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (□a ∈ A → P a)›
      unfolding F_Hiding_seqRun D_Hiding_seqRun by blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹s ∈ 𝒟 (□a ∈ A → P a \ S)›
      hence ‹s ∈ 𝒟 ?lhs› by (simp add: D_Hiding_seqRun Mprefix_projs Mndetprefix_projs)
      with D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
    next
      fix t assume * : ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (□a ∈ A → P a)›
      from ‹s ≠ []› "*"(1) filter.simps(1) have ‹t ≠ []› by blast
      with "*" show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_Hiding F_Mprefix F_Mndetprefix') blast
    qed
  qed
qed

theorem Hiding_Mndetprefix_subset : 
  ‹⊓a ∈ A → P a \ S = ⊓a ∈ A. (P a \ S)› (is ‹?lhs = ?rhs›) if ‹A ⊆ S›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?lhs = ?rhs› by simp
next
  assume ‹A ≠ {}›
  hence ‹A ∩ S ≠ {}› by (simp add: inf_absorb1 ‹A ⊆ S›)
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    have ‹𝒟 ?lhs = 𝒟 (□a ∈ A → P a \ S)›
      by (simp add: D_Hiding_seqRun Mndetprefix_projs Mprefix_projs)
    also have ‹… = 𝒟 ((□a ∈ (A - S) → (P a \ S)) ⊳ (⊓a ∈ (A ∩ S). (P a \ S)))› 
      by (simp add: Hiding_Mprefix_non_disjoint ‹A ∩ S ≠ {}›)
    also have ‹… = 𝒟 ?rhs›
      by (use ‹A ⊆ S› in ‹auto simp add: D_GlobalNdet D_Mprefix D_Sliding›)
    finally show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
      and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s by simp_all
  next
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    fix s X assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      | t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (⊓a ∈ A → P a)›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      fix t assume * : ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (⊓a ∈ A → P a)›
      from "*"(2) ‹A ⊆ S› obtain a t' where ‹a ∈ A› ‹t = ev a # t'› ‹(t', X ∪ ev ` S) ∈ ℱ (P a)›
        by (auto simp add: F_Mndetprefix' ‹A ≠ {}› subset_iff)
      hence ‹(t, X ∪ ev ` S) ∈ ℱ (□a ∈ A → P a)› by (simp add: F_Mprefix)
      with "*"(1) have ‹(s, X) ∈ ℱ (□a ∈ A → P a \ S)›
        by (auto simp add: F_Hiding_seqRun)
      hence ‹(s, X) ∈ ℱ ((□a ∈ (A - S) → (P a \ S)) ⊳ (⊓a ∈ (A ∩ S). (P a \ S)))› 
        by (simp add: Hiding_Mprefix_non_disjoint ‹A ∩ S ≠ {}›)
      also have ‹(□a ∈ (A - S) → (P a \ S)) = STOP›
        by (simp add: Mprefix_is_STOP_iff ‹A ⊆ S›)
      also from ‹A ⊆ S› have ‹A ∩ S = A› by blast
      finally show ‹(s, X) ∈ ℱ (⊓a ∈ A. (P a \ S))› by simp
    qed
  next
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    fix s X assume ‹(s, X) ∈ ℱ ?rhs›
    then obtain a where ‹a ∈ A› ‹(s, X) ∈ ℱ (P a \ S)›
      by (auto simp add: F_GlobalNdet ‹A ≠ {}›)
    from ‹(s, X) ∈ ℱ (P a \ S)› consider ‹s ∈ 𝒟 (P a \ S)›
      | t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (P a)›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹s ∈ 𝒟 (P a \ S)›
      with ‹a ∈ A› have ‹s ∈ 𝒟 ?rhs› by (auto simp add: D_GlobalNdet)
      with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
    next
      from ‹a ∈ A› ‹A ⊆ S›
      show ‹s = trace_hide t (ev ` S) ⟹ (t, X ∪ ev ` S) ∈ ℱ (P a)
            ⟹ (s, X) ∈ ℱ ?lhs› for t
        by (simp add: F_Hiding F_Mndetprefix' ‹A ≠ {}› subset_iff)
          (metis (no_types, lifting) filter.simps(2) image_eqI)
    qed
  qed
qed

theorem Hiding_Mndetprefix_non_disjoint_not_subset :
  ‹⊓a ∈ A → P a \ S = (⊓a ∈ (A - S) → (P a \ S)) ⊓ (⊓a ∈ (A ∩ S). (P a \ S))›
  (is ‹?lhs = ?rhs1 ⊓ ?rhs2›) if ‹A ∩ S ≠ {}› and ‹¬ A ⊆ S›
proof -
  from ‹¬ A ⊆ S› have ‹A - S ≠ {}› by blast
  moreover have ‹A - S ∪ A ∩ S = A› by blast
  ultimately have ‹(⊓a ∈ A → P a) = (⊓a ∈ (A - S) → P a) ⊓ (⊓a ∈ (A ∩ S) → P a)›
    by (metis Mndetprefix_Un_distrib ‹A ∩ S ≠ {}›)
  hence ‹?lhs = (⊓a ∈ (A - S) → P a \ S) ⊓ (⊓a ∈ (A ∩ S) → P a \ S)›
    by (simp add: Hiding_distrib_Ndet)
  also have ‹⊓a ∈ (A - S) → P a \ S = ?rhs1›
    by (simp add: Hiding_Mndetprefix_disjoint inf.commute)
  also have ‹⊓a ∈ (A ∩ S) → P a \ S = ?rhs2›
    by (simp add: Hiding_Mndetprefix_subset)
  finally show ‹?lhs = ?rhs1 ⊓ ?rhs2› .
qed


(*<*)
end
  (*>*)