Theory CSP_New_Laws

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : New laws
 *
 * 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‹ Bonus: powerful new Laws ›

(*<*)
theory  CSP_New_Laws
  imports Initials
begin
(*>*)

section ‹Powerful Results about \<^const>‹Sync››

lemma add_complementary_events_of_in_failure:
  ‹(t, X) ∈ ℱ P ⟹ (t, X ∪ ev ` (- α(P))) ∈ ℱ P›
  by (erule is_processT5) (auto simp add: events_of_def, metis F_T in_set_conv_decomp)

lemma add_complementary_initials_in_refusal: ‹X ∈ ℛ P ⟹ X ∪ - P⇧0 ∈ ℛ P›
  unfolding Refusals_iff by (erule is_processT5) (auto simp add: initials_def F_T)

lemma TickRightSync: 
  ‹✓(r) ∈ S ⟹ ftF u ⟹ t setinterleaves ((u, [✓(r)]), S) ⟹ t = u ∧ last u = ✓(r)›
  by (simp add: TickLeftSync setinterleaving_sym)

  

theorem Sync_is_Sync_restricted_superset_events:
  fixes S A :: ‹'a set› and P Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  assumes superset : ‹α(P) ∪ α(Q) ⊆ A›
  defines ‹S' ≡ S ∩ A›
  shows ‹P ⟦S⟧ Q = P ⟦S'⟧ Q›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 (P ⟦S⟧ Q) ⟹ s ∈ 𝒟 (P ⟦S'⟧ Q)› for s
    by (simp add: D_Sync S'_def)
       (metis Un_UNIV_left Un_commute equals0D events_of_is_strict_events_of_or_UNIV
              inf_top.right_neutral sup.orderE superset)
next
  show ‹s ∈ 𝒟 (P ⟦S'⟧ Q) ⟹ s ∈ 𝒟 (P ⟦S⟧ Q)› for s
    by (simp add: D_Sync S'_def)
       (metis Un_UNIV_left Un_commute equals0D events_of_is_strict_events_of_or_UNIV
              inf_top.right_neutral sup.orderE superset)
next
  let ?S  = ‹range tick ∪ ev ` S  :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  and ?S' = ‹range tick ∪ ev ` S' :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  fix s X
  assume same_div : ‹𝒟 (P ⟦S⟧ Q) = 𝒟 (P ⟦S'⟧ Q)›
  assume ‹(s, X) ∈ ℱ (P ⟦S'⟧ Q)›
  then consider ‹s ∈ 𝒟 (P ⟦S'⟧ Q)›
    | s_P X_P s_Q X_Q where ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                            ‹s setinterleaves ((rev s_P, rev s_Q), ?S')›
                            ‹X = (X_P ∪ X_Q) ∩ ?S' ∪ X_P ∩ X_Q›
    by (simp add: F_Sync D_Sync) (metis rev_rev_ident)
  thus ‹(s, X) ∈ ℱ (P ⟦S⟧ Q)›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 (P ⟦S'⟧ Q) ⟹ (s, X) ∈ ℱ (P ⟦S⟧ Q)› by blast
  next
    fix s_P s_Q and X_P X_Q :: ‹('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
    let ?X_P' = ‹X_P ∪ ev ` (- α(P))› and ?X_Q' = ‹X_Q ∪ ev ` (- α(Q))›
    assume assms : ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                   ‹s setinterleaves ((rev s_P, rev s_Q), ?S')›
                   ‹X = (X_P ∪ X_Q) ∩ ?S' ∪ X_P ∩ X_Q›
    
    from assms(1, 2)[THEN F_T] and assms(3)
    have assms_3_bis : ‹s setinterleaves ((rev s_P, rev s_Q), ?S)›
    proof (induct ‹(s_P, ?S, s_Q)› arbitrary: s_P s_Q s rule: setinterleaving.induct)
      case 1
      thus ‹s setinterleaves ((rev [], rev []), ?S)› by simp
    next
      case (2 y s_Q)
      from "2.prems"(3)[THEN doubleReverse] obtain s' b 
        where * : ‹y = ev b› ‹b ∉ S'› ‹s = rev (y # s')›
                  ‹s' setinterleaves (([], s_Q), ?S')›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "2.prems"(2)[unfolded ‹y = ev b›]
      have ‹b ∈ α(Q)› by (force simp add: events_of_def)
      with ‹b ∉ S'› superset have ‹b ∉ S› by (simp add: S'_def subset_iff)
      from "2.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      have ‹y ∉ ?S› by (simp add: "*"(1) ‹b ∉ S› image_iff)
      have ‹rev s' setinterleaves ((rev [], rev s_Q), ?S)›
        by (fact "2.hyps"[OF ‹y ∉ ?S› "2.prems"(1) ‹rev s_Q ∈ 𝒯 Q› "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹y ∉ ?S›]
      show ‹s setinterleaves ((rev [], rev (y # s_Q)), ?S)›
        by (simp add: ‹s = rev (y # s')›)
    next
      case (3 x s_P)
      from "3.prems"(3)[THEN doubleReverse] obtain s' a 
        where * : ‹x = ev a› ‹a ∉ S'› ‹s = rev (x # s')›
                  ‹s' setinterleaves ((s_P, []), ?S')›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "3.prems"(1)[unfolded ‹x = ev a›]
      have ‹a ∈ α(P)› by (force simp add: events_of_def)
      with ‹a ∉ S'› superset have ‹a ∉ S› by (simp add: S'_def subset_iff)
      from "3.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      have ‹x ∉ ?S› by (simp add: "*"(1) ‹a ∉ S› image_iff)
      have ‹rev s' setinterleaves ((rev s_P, rev []), ?S)›
        by (fact "3.hyps"[OF ‹x ∉ ?S› ‹rev s_P ∈ 𝒯 P› "3.prems"(2) "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹x ∉ ?S›]
      show ‹s setinterleaves ((rev (x # s_P), rev []), ?S)›
        by (simp add: ‹s = rev (x # s')›)
    next
      case (4 x s_P y s_Q)
      from "4.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      from "4.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      from "4.prems"(1) have ‹x ∈ range tick ∪ ev ` α(P)›
        by (cases x; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      from "4.prems"(2) have ‹y ∈ range tick ∪ ev ` α(Q)›
        by (cases y; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      consider ‹x ∈ ?S› and ‹y ∈ ?S› | ‹x ∈ ?S› and ‹y ∉ ?S›
        | ‹x ∉ ?S› and ‹y ∈ ?S› | ‹x ∉ ?S› and ‹y ∉ ?S› by blast
      thus ‹s setinterleaves ((rev (x # s_P), rev (y # s_Q)), ?S)›
      proof cases
        assume ‹x ∈ ?S› and ‹y ∈ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∈ ?S'› and ‹y ∈ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹x = y› ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, s_Q), ?S')›
          by (simp split: if_split_asm) blast

        from "4.hyps"(1)[OF ‹x ∈ ?S› ‹y ∈ ?S› ‹x = y› ‹rev s_P ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, s_Q), ?S')›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev s_P, rev s_Q), ?S)› .
        from this[THEN doubleReverse] ‹x ∈ ?S›
        have ‹(x # s') setinterleaves ((x # s_P, x # s_Q), ?S)› by simp
        from this[THEN doubleReverse] show ?case by (simp add: "*"(1, 2))
      next
        assume ‹x ∈ ?S› and ‹y ∉ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∈ ?S'› and ‹y ∉ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] obtain s'
        where * : ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S')›
          by (simp split: if_split_asm) blast
        from "4.hyps"(2)[OF ‹x ∈ ?S› ‹y ∉ ?S› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((x # s_P, s_Q), ?S')›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S)› .
        from this[THEN doubleReverse] ‹x ∈ ?S› ‹y ∉ ?S›
        have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
      next
        assume ‹x ∉ ?S› and ‹y ∈ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∉ ?S'› and ‹y ∈ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S')›
          by (simp split: if_split_asm) blast
        from "4.hyps"(5)[OF ‹x ∉ ?S› _ ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, y # s_Q), ?S')›[THEN doubleReverse]] ‹y ∈ ?S›
        have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S)› by simp
        from this[THEN doubleReverse] ‹x ∉ ?S› ‹y ∈ ?S›
        have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
      next
        assume ‹x ∉ ?S› and ‹y ∉ ?S›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)›
        have ‹x ∉ ?S'› and ‹y ∉ ?S'› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] consider
          s' where ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S')›
        | s' where ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S')›
          by (simp split: if_split_asm) blast
        thus ?case
        proof cases
          fix s' assume ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S')›
          from "4.hyps"(3)[OF ‹x ∉ ?S› ‹y ∉ ?S› ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                              ‹s' setinterleaves ((s_P, y # s_Q), ?S')›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S)› .
          from this[THEN doubleReverse] ‹x ∉ ?S› ‹y ∉ ?S›
          have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
        next
          fix s' assume ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S')›
          from "4.hyps"(4)[OF ‹x ∉ ?S› ‹y ∉ ?S› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                              ‹s' setinterleaves ((x # s_P, s_Q), ?S')›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S)› .
          from this[THEN doubleReverse] ‹x ∉ ?S› ‹y ∉ ?S›
          have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S)› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
        qed
      qed
    qed
  
    from add_complementary_events_of_in_failure[OF assms(1)]
    have ‹(rev s_P, ?X_P') ∈ ℱ P› .
    moreover from add_complementary_events_of_in_failure[OF assms(2)]
    have ‹(rev s_Q, ?X_Q') ∈ ℱ Q› .
    ultimately have ‹(s, (?X_P' ∪ ?X_Q') ∩ ?S ∪ ?X_P' ∩ ?X_Q') ∈ ℱ (P ⟦S⟧ Q)›
      using assms_3_bis by (simp add: F_Sync) blast
    moreover have ‹X ⊆ (?X_P' ∪ ?X_Q') ∩ ?S ∪ ?X_P' ∩ ?X_Q'›
      by (auto simp add: assms(4) S'_def image_iff)
    ultimately show ‹(s, X) ∈ ℱ (P ⟦S⟧ Q)› by (rule is_processT4)
  qed
next
  let ?S  = ‹range tick ∪ ev ` S  :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  and ?S' = ‹range tick ∪ ev ` S' :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  fix s X
  assume same_div : ‹𝒟 (P ⟦S⟧ Q) = 𝒟 (P ⟦S'⟧ Q)›
  assume ‹(s, X) ∈ ℱ (P ⟦S⟧ Q)›
  then consider ‹s ∈ 𝒟 (P ⟦S⟧ Q)›
    | s_P X_P s_Q X_Q where ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                            ‹s setinterleaves ((rev s_P, rev s_Q), ?S)›
                            ‹X = (X_P ∪ X_Q) ∩ ?S ∪ X_P ∩ X_Q›
    by (simp add: F_Sync D_Sync) (metis rev_rev_ident)
  thus ‹(s, X) ∈ ℱ (P ⟦S'⟧ Q)›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 (P ⟦S⟧ Q) ⟹ (s, X) ∈ ℱ (P ⟦S'⟧ Q)› by blast
  next
    fix s_P s_Q and X_P X_Q :: ‹('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
    let ?X_P' = ‹X_P ∪ ev ` (- α(P))› and ?X_Q' = ‹X_Q ∪ ev ` (- α(Q))›
    assume assms : ‹(rev s_P, X_P) ∈ ℱ P› ‹(rev s_Q, X_Q) ∈ ℱ Q›
                   ‹s setinterleaves ((rev s_P, rev s_Q), ?S)›
                   ‹X = (X_P ∪ X_Q) ∩ ?S ∪ X_P ∩ X_Q›
    
    from assms(1, 2)[THEN F_T] and assms(3)
    have assms_3_bis : ‹s setinterleaves ((rev s_P, rev s_Q), ?S')›
    proof (induct ‹(s_P, ?S', s_Q)› arbitrary: s_P s_Q s rule: setinterleaving.induct)
      case 1
      thus ‹s setinterleaves ((rev [], rev []), ?S')› by simp
    next
      case (2 y s_Q)
      from "2.prems"(3)[THEN doubleReverse] obtain s' b 
        where * : ‹y = ev b› ‹b ∉ S› ‹s = rev (y # s')›
                  ‹s' setinterleaves (([], s_Q), ?S)›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "2.prems"(2)[unfolded ‹y = ev b›]
      have ‹b ∈ α(Q)› by (force simp add: events_of_def)
      with ‹b ∉ S› have ‹b ∉ S'› by (simp add: S'_def)
      from "2.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      have ‹y ∉ ?S'› by (simp add: "*"(1) ‹b ∉ S'› image_iff)
      have ‹rev s' setinterleaves ((rev [], rev s_Q), ?S')›
        by (fact "2.hyps"[OF ‹y ∉ ?S'› "2.prems"(1) ‹rev s_Q ∈ 𝒯 Q› "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹y ∉ ?S'›]
      show ‹s setinterleaves ((rev [], rev (y # s_Q)), ?S')›
        by (simp add: ‹s = rev (y # s')›)
    next
      case (3 x s_P)
      from "3.prems"(3)[THEN doubleReverse] obtain s' a 
        where * : ‹x = ev a› ‹a ∉ S› ‹s = rev (x # s')›
                  ‹s' setinterleaves ((s_P, []), ?S)›
        by (simp add: image_iff split: if_split_asm) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from "3.prems"(1)[unfolded ‹x = ev a›]
      have ‹a ∈ α(P)› by (force simp add: events_of_def)
      with ‹a ∉ S› have ‹a ∉ S'› by (simp add: S'_def)
      from "3.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      have ‹x ∉ ?S'› by (simp add: "*"(1) ‹a ∉ S'› image_iff)
      have ‹rev s' setinterleaves ((rev s_P, rev []), ?S')›
        by (fact "3.hyps"[OF ‹x ∉ ?S'› ‹rev s_P ∈ 𝒯 P› "3.prems"(2) "*"(4)[THEN doubleReverse]])
      from this[THEN addNonSync, OF ‹x ∉ ?S'›]
      show ‹s setinterleaves ((rev (x # s_P), rev []), ?S')›
        by (simp add: ‹s = rev (x # s')›)
    next
      case (4 x s_P y s_Q)
      from "4.prems"(1)[simplified, THEN is_processT3_TR] have ‹rev s_P ∈ 𝒯 P› by auto
      from "4.prems"(2)[simplified, THEN is_processT3_TR] have ‹rev s_Q ∈ 𝒯 Q› by auto
      from "4.prems"(1) have ‹x ∈ range tick ∪ ev ` α(P)›
        by (cases x; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      from "4.prems"(2) have ‹y ∈ range tick ∪ ev ` α(Q)›
        by (cases y; force simp add: events_of_def image_iff split: event⇩p⇩t⇩i⇩c⇩k.split)
      consider ‹x ∈ ?S'› and ‹y ∈ ?S'› | ‹x ∈ ?S'› and ‹y ∉ ?S'›
        | ‹x ∉ ?S'› and ‹y ∈ ?S'› | ‹x ∉ ?S'› and ‹y ∉ ?S'› by blast
      thus ‹s setinterleaves ((rev (x # s_P), rev (y # s_Q)), ?S')›
      proof cases
        assume ‹x ∈ ?S'› and ‹y ∈ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)›
        have ‹x ∈ ?S› and ‹y ∈ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹x = y› ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, s_Q), ?S)›
          by (simp split: if_split_asm) blast

        from "4.hyps"(1)[OF ‹x ∈ ?S'› ‹y ∈ ?S'› ‹x = y› ‹rev s_P ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, s_Q), ?S)›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev s_P, rev s_Q), ?S')› .
        from this[THEN doubleReverse] ‹x ∈ ?S'›
        have ‹(x # s') setinterleaves ((x # s_P, x # s_Q), ?S')› by simp
        from this[THEN doubleReverse] show ?case by (simp add: "*"(1, 2))
      next
        assume ‹x ∈ ?S'› and ‹y ∉ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∈ ?S› and ‹y ∉ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] obtain s'
        where * : ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S)›
          by (simp split: if_split_asm) blast
        from "4.hyps"(2)[OF ‹x ∈ ?S'› ‹y ∉ ?S'› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                            ‹s' setinterleaves ((x # s_P, s_Q), ?S)›[THEN doubleReverse]]
        have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S')› .
        from this[THEN doubleReverse] ‹x ∈ ?S'› ‹y ∉ ?S'›
        have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
      next
        assume ‹x ∉ ?S'› and ‹y ∈ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∉ ?S› and ‹y ∈ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse] obtain s'
        where * : ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S)›
          by (simp split: if_split_asm) blast
        from "4.hyps"(5)[OF ‹x ∉ ?S'› _ ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                            ‹s' setinterleaves ((s_P, y # s_Q), ?S)›[THEN doubleReverse]] ‹y ∈ ?S'›
        have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S')› by simp
        from this[THEN doubleReverse] ‹x ∉ ?S'› ‹y ∈ ?S'›
        have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
        from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
      next
        assume ‹x ∉ ?S'› and ‹y ∉ ?S'›
        with ‹x ∈ range tick ∪ ev ` α(P)› ‹y ∈ range tick ∪ ev ` α(Q)› superset
        have ‹x ∉ ?S› and ‹y ∉ ?S› by (auto simp add: S'_def)
        with "4.prems"(3)[THEN doubleReverse, simplified] consider
          s' where ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S)›
        | s' where ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S)›
          by (simp split: if_split_asm) blast
        thus ?case
        proof cases
          fix s' assume ‹s = rev (x # s')› ‹s' setinterleaves ((s_P, y # s_Q), ?S)›
          from "4.hyps"(3)[OF ‹x ∉ ?S'› ‹y ∉ ?S'› ‹rev s_P ∈ 𝒯 P› ‹rev (y # s_Q) ∈ 𝒯 Q›
                              ‹s' setinterleaves ((s_P, y # s_Q), ?S)›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev s_P, rev (y # s_Q)), ?S')› .
          from this[THEN doubleReverse] ‹x ∉ ?S'› ‹y ∉ ?S'›
          have ‹(x # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (x # s')›)
        next
          fix s' assume ‹s = rev (y # s')› ‹s' setinterleaves ((x # s_P, s_Q), ?S)›
          from "4.hyps"(4)[OF ‹x ∉ ?S'› ‹y ∉ ?S'› ‹rev (x # s_P) ∈ 𝒯 P› ‹rev s_Q ∈ 𝒯 Q›
                              ‹s' setinterleaves ((x # s_P, s_Q), ?S)›[THEN doubleReverse]]
          have ‹rev s' setinterleaves ((rev (x # s_P), rev s_Q), ?S')› .
          from this[THEN doubleReverse] ‹x ∉ ?S'› ‹y ∉ ?S'›
          have ‹(y # s') setinterleaves ((x # s_P, y # s_Q), ?S')› by simp
          from this[THEN doubleReverse] show ?case by (simp add: ‹s = rev (y # s')›)
        qed
      qed
    qed
  
    from add_complementary_events_of_in_failure[OF assms(1)]
    have ‹(rev s_P, ?X_P') ∈ ℱ P› .
    moreover from add_complementary_events_of_in_failure[OF assms(2)]
    have ‹(rev s_Q, ?X_Q') ∈ ℱ Q› .
    ultimately have ‹(s, (?X_P' ∪ ?X_Q') ∩ ?S' ∪ ?X_P' ∩ ?X_Q') ∈ ℱ (P ⟦S'⟧ Q)›
      using assms_3_bis by (simp add: F_Sync) blast
    moreover from superset have ‹X ⊆ (?X_P' ∪ ?X_Q') ∩ ?S' ∪ ?X_P' ∩ ?X_Q'›
      by (auto simp add: assms(4) S'_def image_iff)
    ultimately show ‹(s, X) ∈ ℱ (P ⟦S'⟧ Q)› by (rule is_processT4)
  qed
qed

corollary Sync_is_Sync_restricted_events : ‹P ⟦S⟧ Q = P ⟦S ∩ (α(P) ∪ α(Q))⟧ Q›
  by (simp add: Sync_is_Sync_restricted_superset_events)

text ‹This version is closer to the intuition that we may have, but the first one would be more
useful if we don't want to compute the events of a process but know a superset approximation.›


(* lemma Sync_with_SKIP_eq_itself_if_disjoint_events:
  ‹α(P) ∩ S = {} ⟹ P ⟦S⟧ SKIP r = P›
  oops
  by (metis Int_commute Inter_SKIP Sync_is_Sync_restricted_events events_Inter)

lemma Sync_with_STOP_eq_itself_Seq_STOP_if_disjoint_events:
  ‹α(P) ∩ S = {} ⟹ P ⟦S⟧ STOP = P ❙; (λr. STOP)›
  oops
  by (metis Int_Un_eq(3) Int_commute Inter_STOP_Seq_STOP Sync_is_Sync_restricted_events events_STOP) *)


corollary ‹deadlock_free P ⟹ deadlock_free Q ⟹
           S ∩ (α(P) ∪ α(Q)) = {} ⟹ deadlock_free (P ⟦S⟧ Q)›
  by (subst Sync_is_Sync_restricted_events) (simp add: Inter_deadlock_free)
    (* but we already had this with data_independence_deadlock_free_Sync *)






text ‹This is a result similar to @{thm [source] Hiding_Mprefix_disjoint}
      when we add a @{const [source] Sliding} in the expression.›

theorem Hiding_Mprefix_Sliding_disjoint:
  ‹((□a ∈ A → P a) ⊳ Q) \ S = (□a ∈ A → (P a \ S)) ⊳ (Q \ S)›
  if disjoint: ‹A ∩ S = {}›
proof (subst Hiding_Mprefix_disjoint[OF disjoint, symmetric])
  show ‹((□a ∈ A → P a) ⊳ Q) \ S = (□a ∈ A → P a \ S) ⊳ (Q \ S)›
   (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    hence ‹s ∈ 𝒟 (Mprefix A P ⊓ Q \ S)›
      by (simp add: D_Hiding D_Sliding D_Ndet T_Sliding T_Ndet)
    thus ‹s ∈ 𝒟 ?rhs›
      by (rule set_rev_mp) (simp add: D_Ndet D_Sliding Hiding_distrib_Ndet)
  next
    fix s
    assume ‹s ∈ 𝒟 ?rhs›
    hence ‹s ∈ 𝒟 (Q \ S) ∨ s ∈ 𝒟 (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_disjoint[OF disjoint]
                    D_Ndet D_Sliding) blast
    thus ‹s ∈ 𝒟 ?lhs›
      by (auto simp add: D_Hiding D_Sliding T_Sliding)
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      |‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      assume ‹∃t. s = trace_hide t (ev ` S) ∧
                  (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      then obtain t
        where * : ‹s = trace_hide t (ev ` S)›
                  ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)› by blast
      from "*"(2) consider ‹(t, X ∪ ev ` S) ∈ ℱ Q›
        | ‹t ≠ []› ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Sliding D_Mprefix) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        have ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ (Q \ S)›
          by (auto simp add: F_Hiding "*"(1))
        thus ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Ndet F_Sliding "*"(1))
      next
        assume assms : ‹t ≠ []› ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        with disjoint have ‹trace_hide t (ev ` S) ≠ []›
          by (cases t, auto simp add: F_Mprefix)
        also have ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
          using assms by (auto simp: F_Hiding "*"(1))
        ultimately show ‹(s, X) ∈ ℱ ?rhs›
          by (simp add: F_Sliding "*"(1))
      qed
    qed
  next
    have * : ‹t ∈ 𝒯 (Mprefix A P) ⟹ trace_hide t (ev ` S) = [] ⟷ t = []› for t
      using disjoint by (cases t, auto simp add: T_Mprefix)
    have ** : ‹[] ∉ 𝒟 (Mprefix A P \ S)›
      apply (rule ccontr, simp add: D_Hiding, elim exE conjE disjE)
      by (use "*" D_T Nil_notin_D_Mprefix in blast)
         (metis (no_types, lifting) "*" UNIV_I f_inv_into_f old.nat.distinct(2) strict_mono_on_eqD)
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    with ** consider ‹(s, X) ∈ ℱ (Q \ S)›
      | ‹s ≠ []› ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      by (simp add: Hiding_Mprefix_disjoint[OF disjoint] F_Sliding D_Mprefix) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹(s, X) ∈ ℱ (Q \ S)›
      then consider ‹s ∈ 𝒟 (Q \ S)›
        | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Q \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        thus ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Hiding F_Sliding) blast
      qed
    next
      assume assms : ‹s ≠ []› ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      then consider ‹s ∈ 𝒟 (Mprefix A P \ S)›
        | ‹∃t. t ≠ [] ∧ s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Hiding D_Hiding) (metis filter.simps(1))
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Mprefix A P \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        show ‹∃t. t ≠ [] ∧ s = trace_hide t (ev ` S) ∧
                  (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P) ⟹ (s, X) ∈ ℱ ?lhs›
          by (auto simp add: F_Sliding F_Hiding)
      qed
    qed
  qed
qed



subsection ‹Non-disjoint Sets›

― ‹Just a small lemma to understand why the nonempty hypothesis is necessary.›
lemma ‹∃A :: nat set. ∃P S.
       A ∩ S = {} ∧ □a ∈ A → P a \ S ≠ 
       (□a ∈ (A - S) → (P a \ S)) ⊳ (⊓a ∈ (A ∩ S). (P a \ S))›
proof (intro exI)
  show ‹{0} ∩ {Suc 0} = {} ∧ 
        □a ∈ {0} → SKIP undefined \ {Suc 0} ≠ 
        (□a ∈ ({0} - {Suc 0}) → (SKIP undefined \ {Suc 0})) ⊳ (⊓a ∈ ({0} ∩ {Suc 0}). (SKIP undefined \ {Suc 0}))›
    apply (simp add: write0_def[symmetric] Hiding_write0_disjoint)
    using UNIV_I list.discI by (auto simp add: Process_eq_spec write0_def F_Ndet
                                               F_Mprefix F_Sliding F_STOP set_eq_iff)
qed


text ‹This is a result similar to @{thm [source] Hiding_Mprefix_non_disjoint}
      when we add a @{const [source] Sliding} in the expression.›

lemma Hiding_Mprefix_Sliding_non_disjoint:
  ‹(□a ∈ A → P a) ⊳ Q \ S = (□a ∈ (A - S) → (P a \ S)) ⊳ 
                              (Q \ S) ⊓ (⊓a ∈ (A ∩ S). (P a \ S))›
  if non_disjoint: ‹A ∩ S ≠ {}›
proof (subst Sliding_distrib_Ndet_left,
       subst Hiding_Mprefix_non_disjoint[OF non_disjoint, symmetric])
  show ‹Mprefix A P ⊳ Q \ S =
        ((□a ∈ (A - S) → (P a \ S)) ⊳ (Q \ S)) ⊓ (□a ∈ A → P a \ S)›
   (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    hence ‹s ∈ 𝒟 (Mprefix A P ⊓ Q \ S)›
      by (simp add: D_Hiding D_Sliding D_Ndet T_Sliding T_Ndet)
    thus ‹s ∈ 𝒟 ?rhs›
      by (rule set_rev_mp)
         (simp add: D_Ndet D_Sliding Hiding_distrib_Ndet subsetI)
  next
    fix s
    assume ‹s ∈ 𝒟 ?rhs›
    hence ‹s ∈ 𝒟 (Q \ S) ∨ s ∈ 𝒟 (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_non_disjoint[OF non_disjoint]
                    D_Ndet D_Sliding) blast
    thus ‹s ∈ 𝒟 ?lhs›
      by (auto simp add: D_Hiding D_Sliding T_Sliding)
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      |‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      assume ‹∃t. s = trace_hide t (ev ` S) ∧
                  (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)›
      then obtain t
        where * : ‹s = trace_hide t (ev ` S)›
                  ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P ⊳ Q)› by blast
      from "*"(2) consider ‹(t, X ∪ ev ` S) ∈ ℱ Q›
        | ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Sliding D_Mprefix) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        have ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ (Q \ S)›
          by (auto simp add: F_Hiding "*"(1))
        thus ‹(t, X ∪ ev ` S) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Ndet F_Sliding "*"(1))
      next
        assume ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        hence ‹(s, X) ∈ ℱ (Mprefix A P \ S)› by (auto simp: F_Hiding "*"(1))
        thus ‹(s, X) ∈ ℱ ?rhs› by (simp add: F_Ndet "*"(1))
      qed
    qed
  next
    fix s X
    have * : ‹s ≠ [] ⟹ (s, X) ∈ ℱ (□a ∈ (A - S) → (P a \ S)) ⟹ 
                          (s, X) ∈ ℱ (□a ∈ A → P a \ S)›
      by (simp add: Hiding_Mprefix_non_disjoint[OF non_disjoint] F_Sliding)
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    with "*" consider ‹(s, X) ∈ ℱ (Q \ S)› | ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      by (auto simp add: F_Ndet F_Sliding)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹(s, X) ∈ ℱ (Q \ S)›
      then consider ‹s ∈ 𝒟 (Q \ S)›
        | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Q \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ Q›
        thus ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Hiding F_Sliding) blast
      qed
    next
      assume ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      then consider ‹s ∈ 𝒟 (Mprefix A P \ S)›
        | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: F_Hiding D_Hiding) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Mprefix A P \ S)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Ndet D_Sliding)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        then obtain t where * : ‹s = trace_hide t (ev ` S)›
                                ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)› by blast
        from "*"(2) non_disjoint have ‹t ≠ []› by (simp add: F_Mprefix) blast
        with "*" show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Hiding F_Sliding) blast
      qed
    qed
  qed
qed
       


section ‹\<^const>‹Sliding› behaviour›

text ‹We already proved several laws for the \<^const>‹Sliding› operator.
      Here we give other results in the same spirit as
      @{thm [source] Hiding_Mprefix_Sliding_disjoint} and
      @{thm [source] Hiding_Mprefix_Sliding_non_disjoint}.›

lemma Mprefix_Sliding_Mprefix_Sliding:
  ‹(□a ∈ A → P a) ⊳ (□b ∈ B → Q b) ⊳ R =
   (□ x ∈ (A ∪ B) → (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)) ⊳ R›
  (is ‹(□a ∈ A → P a) ⊳ (□b ∈ B → Q b) ⊳ R = ?term ⊳ R›)
proof (subst Sliding_def, subst Mprefix_Det_Mprefix)
  have ‹Mprefix B Q ⊓ (Mprefix A P □ Mprefix B Q) ⊳ R = Mprefix A P □ Mprefix B Q ⊳ R›
    by (metis (no_types, opaque_lifting) Det_assoc Det_commute Ndet_commute
              Ndet_distrib_Det_left Ndet_id Sliding_Det Sliding_assoc Sliding_def)
  thus ‹?term ⊓ Mprefix B Q ⊳ R = ?term ⊳ R›
    by (simp add: Mprefix_Det_Mprefix Ndet_commute)
qed


lemma Mprefix_Sliding_Seq: 
  ‹(□a ∈ A → P a) ⊳ P' ❙; Q = (□a ∈ A → (P a ❙; Q)) ⊳ (P' ❙; Q)›
proof (subst Mprefix_Seq[symmetric])
  show ‹((□a ∈ A → P a) ⊳ P') ❙; Q = 
        ((□a ∈ A → P a) ❙; Q) ⊳ (P' ❙; Q)› (is ‹?lhs = ?rhs›)
  proof (subst Process_eq_spec, safe)
    show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
      by (simp add: D_Sliding D_Seq T_Sliding) blast
  next
    show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
      by (auto simp add: D_Sliding D_Seq T_Sliding)
  next
    show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
      by (cases s; simp add: F_Sliding D_Sliding T_Sliding F_Seq) metis
  next
    show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
      by (cases s; simp add: F_Sliding D_Sliding T_Sliding
                             F_Seq D_Seq T_Seq D_Mprefix T_Mprefix)
         (metis event⇩p⇩t⇩i⇩c⇩k.simps(4) hd_append list.sel(1), blast)
  qed
qed



lemma Throw_Sliding :
  ‹(□a ∈ A → P a) ⊳ P' Θ b ∈ B. Q b = 
   (□a ∈ A → (if a ∈ B then Q a else P a Θ b ∈ B. Q b)) ⊳ (P' Θ b ∈ B. Q b)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then consider t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (Mprefix A P ⊳ P')›
                            ‹tF t1› ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
    | t1 b t2 where ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                    ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
    by (simp add: D_Throw) blast
  thus ‹s ∈ 𝒟 ?rhs›
  proof cases
    fix t1 t2 assume * : ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (Mprefix A P ⊳ P')› ‹tF t1›
                         ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
    from "*"(2) consider ‹t1 ∈ 𝒟 (Mprefix A P)› | ‹t1 ∈ 𝒟 P'›
      by (simp add: D_Sliding) blast
    thus ‹s ∈ 𝒟 ?rhs›
    proof cases
      assume ‹t1 ∈ 𝒟 (Mprefix A P)›
      then obtain a t1' where ‹t1 = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒟 (P a)›
        by (auto simp add: D_Mprefix image_iff)
      with "*"(1, 3, 4, 5) show ‹s ∈ 𝒟 ?rhs›
        by (simp add: D_Sliding D_Mprefix D_Throw) (metis image_eqI)
    next
      from "*"(1, 3, 4, 5)  show ‹t1 ∈ 𝒟 P' ⟹ s ∈ 𝒟 ?rhs›
        by (simp add: D_Sliding D_Throw) blast
    qed
  next
    fix t1 b t2 assume * : ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                           ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
    from "*"(2) consider ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)› | ‹t1 @ [ev b] ∈ 𝒯 P'›
      by (simp add: T_Sliding) blast
    thus ‹s ∈ 𝒟 ?rhs›
    proof cases
      assume ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)›
      then obtain a t1'
        where ‹t1 @ [ev b] = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒯 (P a)›
        by (auto simp add: T_Mprefix)
      with "*"(1, 3-5) show ‹s ∈ 𝒟 ?rhs›
        by (cases t1; simp add: "*"(1) D_Sliding D_Mprefix D_Throw)
           (metis image_eqI)
    next
      from "*"(1, 3-5) show ‹t1 @ [ev b] ∈ 𝒯 P' ⟹ s ∈ 𝒟 ?rhs›
        by (simp add: D_Sliding D_Mprefix D_Throw) blast
    qed
  qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then consider ‹s ∈ 𝒟 (Throw P' B Q)›
    | ‹s ∈ 𝒟 (□a∈A → (if a ∈ B then Q a else Throw (P a) B Q))›
    by (simp add: D_Sliding) blast
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    show ‹s ∈ 𝒟 (Throw P' B Q) ⟹ s ∈ 𝒟 ?lhs›
      by (simp add: D_Throw D_Sliding T_Sliding) blast
  next
    assume ‹s ∈ 𝒟 (□a∈A → (if a ∈ B then Q a else Throw (P a) B Q))›
    then obtain a s' 
      where * : ‹s = ev a # s'› ‹a ∈ A›
                ‹s' ∈ 𝒟 (if a ∈ B then Q a else Throw (P a) B Q)›
      by (cases s; simp add: D_Mprefix) blast
    show ‹s ∈ 𝒟 ?lhs›
    proof (cases ‹a ∈ B›)
      from "*" show ‹a ∈ B ⟹ s ∈ 𝒟 ?lhs›
        by (simp add: D_Throw T_Sliding T_Mprefix disjoint_iff)
           (metis Nil_elem_T emptyE empty_set self_append_conv2)
    next
      assume ‹a ∉ B›
      with "*"(3) consider 
        t1 t2 where ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tF t1›
                    ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
        | t1 b t2 where ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                        ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
        by (simp add: D_Throw) blast
      thus ‹s ∈ 𝒟 ?lhs›
      proof cases
        fix t1 t2 assume ** : ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tF t1›
                              ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
        have *** : ‹s = (ev a # t1) @ t2 ∧ set (ev a # t1) ∩ ev ` B = {}›
          by (simp add: "*"(1) "**"(1, 4) image_iff ‹a ∉ B›)
        from "*" "**"(1, 2, 3, 5) show ‹s ∈ 𝒟 ?lhs›
          by (simp add: D_Throw D_Sliding D_Mprefix image_iff)
             (metis "***" event⇩p⇩t⇩i⇩c⇩k.disc(1) tickFree_Cons_iff)
      next
        fix t1 b t2 assume ** : ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                                ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
        have *** : ‹s = (ev a # t1 @ [ev b]) @ t2 ∧ set (ev a # t1) ∩ ev ` B = {}›
          by (simp add: "*"(1) "**"(1, 3) image_iff ‹a ∉ B›)
        from "*" "**"(1, 2, 4, 5) show ‹s ∈ 𝒟 ?lhs›
          by (simp add: D_Throw T_Sliding T_Mprefix) (metis "***" Cons_eq_appendI)
      qed
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | ‹(s, X) ∈ ℱ (Mprefix A P ⊳ P')› ‹set s ∩ ev ` B = {}›
    | t1 b t2 where ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                    ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    by (auto simp add: F_Throw D_Throw)
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    show ‹(s, X) ∈ ℱ (Mprefix A P ⊳ P') ⟹ set s ∩ ev ` B = {} ⟹ (s, X) ∈ ℱ ?rhs›
      by (cases s; simp add: F_Sliding F_Mprefix F_Throw) blast
  next
    fix t1 b t2 assume * : ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P')›
                           ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    from "*"(2) consider ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)› | ‹t1 @ [ev b] ∈ 𝒯 P'›
      by (simp add: T_Sliding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      assume ‹t1 @ [ev b] ∈ 𝒯 (Mprefix A P)›
      then obtain a t1'
        where ‹t1 @ [ev b] = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒯 (P a)›
        by (auto simp add: T_Mprefix)
      with "*"(1, 3, 4, 5) show ‹(s, X) ∈ ℱ ?rhs›
        by (cases t1; simp add: "*"(1) F_Sliding F_Mprefix F_Throw) blast
    next
      from "*"(1, 3, 4, 5) show ‹t1 @ [ev b] ∈ 𝒯 P' ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Sliding F_Mprefix F_Throw) blast
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s ∈ 𝒟 ?rhs› | ‹(s, X) ∈ ℱ (Throw P' B Q)›
    | ‹s ≠ []› ‹(s, X) ∈ ℱ (□a ∈ A → (if a ∈ B then Q a else Throw (P a) B Q))›
    by (simp add: F_Sliding D_Sliding) blast
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
  next
    show ‹(s, X) ∈ ℱ (Throw P' B Q) ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: F_Throw F_Sliding D_Sliding T_Sliding) blast
  next
    assume ‹s ≠ []› ‹(s, X) ∈ ℱ (□a ∈ A → (if a ∈ B then Q a else Throw (P a) B Q))›
    then obtain a s'
      where * : ‹s = ev a # s'› ‹a ∈ A› 
                ‹(s', X) ∈ ℱ (if a ∈ B then Q a else Throw (P a) B Q)›
      by (auto simp add: F_Mprefix image_iff)
    show ‹(s, X) ∈ ℱ ?lhs›
    proof (cases ‹a ∈ B›)
      assume ‹a ∈ B›
      have ‹[ev a] ∈ 𝒯 (Mprefix A P ⊳ P')›
        by (simp add: T_Sliding T_Mprefix "*"(2))
      with "*"(1, 3) ‹a ∈ B› show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_Throw) (metis append_Nil empty_set inf_bot_left)
    next
      assume ‹a ∉ B›
      with "*"(3) consider ‹s' ∈ 𝒟 (Throw (P a) B Q)›
        | ‹(s', X) ∈ ℱ (P a)› ‹set s' ∩ ev ` B = {}›
        | t1 b t2 where ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                        ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
        by (auto simp add: F_Throw D_Throw)
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (Throw (P a) B Q)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: "*"(1, 2) D_Sliding D_Mprefix ‹a ∉ B›)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        show ‹(s', X) ∈ ℱ (P a) ⟹ set s' ∩ ev ` B = {} ⟹ (s, X) ∈ ℱ ?lhs›
          using "*"(1, 2) ‹a ∉ B› by (simp add: F_Throw F_Sliding F_Mprefix) blast
      next
        fix t1 b t2 assume ** : ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                                ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
        from "**" have *** : ‹(ev a # t1) @ [ev b] ∈ 𝒯 (Mprefix A P) ∧ 
                              set (ev a # t1) ∩ ev ` B = {}›
          by (simp add: T_Mprefix "*"(2) image_iff ‹a ∉ B›)
        from "*"(1) "**"(1, 4, 5) "**"(5) show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Throw T_Sliding) (metis "***" Cons_eq_appendI)
      qed
    qed
  qed
qed



section ‹Dealing with \<^const>‹SKIP››

lemma Renaming_Mprefix_Det_SKIP:
  ‹Renaming ((□ a ∈ A → P a) □ SKIP r) f g =
   (□y∈f ` A → ⊓ a ∈ {x ∈ A. y = f x}. Renaming (P a) f g) □ SKIP (g r)›
  by (simp add: Renaming_Det Renaming_Mprefix)


lemma Mprefix_Sliding_SKIP_Seq: ‹((□ a ∈ A → P a) ⊳ SKIP r) ❙; Q = (□ a ∈ A → (P a ❙; Q)) ⊳ Q›
  (* TODO: see if we leave Sliding_SKIP in simp *)
  by (simp del: Sliding_SKIP add: Mprefix_Sliding_Seq)

lemma Mprefix_Det_SKIP_Seq: ‹((□ a ∈ A → P a) □ SKIP r) ❙; Q = (□ a ∈ A → (P a ❙; Q)) ⊳ Q›
  by (fold Sliding_SKIP) (fact Mprefix_Sliding_SKIP_Seq)


lemma Sliding_Ndet_pseudo_assoc : ‹(P ⊳ Q) ⊓ R = P ⊳ Q ⊓ R›
  by (metis Ndet_assoc Ndet_distrib_Det_right Ndet_id Sliding_def)

lemma Hiding_Mprefix_Det_SKIP:
  ‹(□ a ∈ A → P a) □ SKIP r \ S =
   (if A ∩ S = {} then (□ a ∈ A → (P a \ S)) □ SKIP r
    else ((□ a ∈ (A - S) → (P a \ S)) □ SKIP r) ⊓ (⊓ a ∈ (A ∩ S). (P a \ S)))›
  by (fold Sliding_SKIP)
     (simp del: Sliding_SKIP add: Hiding_Mprefix_Sliding_disjoint
           Hiding_Mprefix_Sliding_non_disjoint Sliding_Ndet_pseudo_assoc)


lemma ‹s ≠ [] ⟹ (s, X) ∈ ℱ (P □ Q) ⟷ (s, X) ∈ ℱ (P ⊓ Q)›
  by (simp add: F_Det F_Ndet)


lemma Mprefix_Det_SKIP_Sync_SKIP :
  ‹((□ a ∈ A → P a) □ SKIP res) ⟦S⟧ SKIP res' = 
   (if res = res' then (□ a ∈ (A - S) → (P a ⟦S⟧ SKIP res')) □ SKIP res'
    else (□ a ∈ (A - S) → (P a ⟦S⟧ SKIP res')) ⊓ STOP)›
  (is ‹?lhs = (if res = res' then ?rhs1 else ?rhs2)›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then obtain a t u r v
    where * : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v›
              ‹r setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
              ‹a ∈ A› ‹t ∈ 𝒟 (P a)› ‹u ∈ 𝒯 (SKIP res')›
    by (simp add: D_Sync D_SKIP D_Det D_Mprefix T_SKIP image_iff) blast
  from "*"(3, 4, 5, 7) have ** : ‹a ∈ A - S› ‹s = ev a # tl r @ v›
                                 ‹tl r setinterleaves ((t, u), range tick ∪ ev ` S)›
    by (auto simp add: image_iff T_SKIP split: if_split_asm)
  have ‹tl s ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
    by (simp add: D_Sync)
       (metis "*"(1, 2, 6, 7) "**"(2, 3) list.sel(3) tickFree_tl)
  with "**"(1) show ‹s ∈ 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
    by (simp add: D_Det D_Ndet D_Mprefix "**"(2))
next
  fix s
  assume ‹s ∈ 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
  then obtain a s' where * : ‹s = ev a # s'› ‹a ∈ A - S› ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
    by (auto simp add: D_Det D_Ndet D_SKIP D_STOP D_Mprefix image_iff split: if_split_asm)
  then obtain t u r v
    where ** : ‹ftF v› ‹tF r ∨ v = []› ‹s' = r @ v›
               ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
               ‹t ∈ 𝒟 (P a)› ‹u ∈ 𝒯 (SKIP res')›
    by (simp add: D_Sync D_SKIP) blast
  have ‹(ev a # r) setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
    using "*"(2) "**"(4, 6) by (auto simp add: T_SKIP)
  with "*"(2) "**"(1, 2, 3, 5, 6) show ‹s ∈ 𝒟 ?lhs›
    by (simp add: D_Sync D_SKIP D_Det D_Mprefix T_SKIP image_iff)
       (metis (no_types, opaque_lifting) "*"(1) Cons_eq_appendI event⇩p⇩t⇩i⇩c⇩k.disc(1) tickFree_Cons_iff)
next
  fix s Z
  assume same_div : ‹𝒟 ?lhs = 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
  assume ‹(s, Z) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | t u X Y where ‹(t, X) ∈ ℱ (Mprefix A P □ SKIP res)› ‹(u, Y) ∈ ℱ (SKIP res')›
                    ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
                    ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
    by (simp add: F_Sync D_Sync) blast
  thus ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)› by blast
  next
    fix t u X Y
    assume * : ‹(t, X) ∈ ℱ (Mprefix A P □ SKIP res)› ‹(u, Y) ∈ ℱ (SKIP res')›
               ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
               ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›    
    from "*"(1) consider ‹t = []› | ‹t = [✓(res)]› | a t' where ‹t = ev a # t'›
      by (auto simp add: F_Det F_SKIP F_Mprefix)
    thus ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
    proof cases
      assume ‹t = []›
      with "*"(2, 3) have ‹s = []› by (auto simp add: F_SKIP)
      with ‹t = []› "*"(3)[simplified ‹t = []›, THEN emptyLeftProperty] "*"(1, 2, 3, 4)
      show ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
        by (auto simp add: F_Det F_Ndet F_Mprefix F_STOP F_SKIP D_SKIP T_SKIP)
    next
      assume ‹t = [✓(res)]›
      with "*"(2, 3) have ‹res' = res ∧ s = [✓(res)]›
        by (cases u; auto simp add: F_SKIP split: if_split_asm)
      with ‹t = [✓(res)]› show ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
        by (simp add: F_Det F_Ndet F_STOP F_SKIP)      
    next
      fix a t' assume ‹t = ev a # t'›
      with "*"(1, 2, 3) empty_setinterleaving obtain s'
        where ** : ‹s' setinterleaves ((t', u), range tick ∪ ev ` S)›
                   ‹s = ev a # s'› ‹(t', X) ∈ ℱ (P a)› ‹a ∈ A - S›
        by (auto simp add: F_SKIP F_Det F_Mprefix image_iff split: if_split_asm)
      from "*"(2, 4) "**"(1, 3) have ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
        by (simp add: F_Sync) blast  
      with "**"(4) show ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
        by (simp add: F_Det F_Ndet ‹s = ev a # s'› F_SKIP F_Mprefix)
    qed
  qed
next
  fix s Z
  assume same_div : ‹𝒟 ?lhs = 𝒟 (if res = res' then ?rhs1 else ?rhs2)›
  assume ‹(s, Z) ∈ ℱ (if res = res' then ?rhs1 else ?rhs2)›
  then consider ‹res = res'› ‹(s, Z) ∈ ℱ ?rhs1›
    | ‹res ≠ res'› ‹(s, Z) ∈ ℱ ?rhs2› by presburger
  thus ‹(s, Z) ∈ ℱ ?lhs›
  proof cases
    assume ‹res = res'› ‹(s, Z) ∈ ℱ ?rhs1›
    then consider ‹s = []› | ‹s = [✓(res')]› | a s' where ‹s = ev a # s'›
      by (auto simp add: F_Det F_SKIP F_Mprefix)
    thus ‹(s, Z) ∈ ℱ ?lhs›
    proof cases
      assume ‹s = []›
      with ‹(s, Z) ∈ ℱ ?rhs1› have ‹tick res' ∉ Z›
        by (auto simp add: F_Det F_Mprefix F_SKIP D_SKIP T_SKIP)
      with ‹s = []› show ‹(s, Z) ∈ ℱ ?lhs›
        by (simp add: F_Sync F_Det T_SKIP F_SKIP ‹res = res'›)
           (metis Int_Un_eq(3) si_empty1 Un_Int_eq(4) Un_commute insertI1)
    next
      assume ‹s = [✓(res')]›
      hence * : ‹([✓(res')], Z) ∈ ℱ (Mprefix A P □ SKIP res') ∧ 
                 s setinterleaves (([✓(res')], [✓(res')]), range tick ∪ ev ` S) ∧ 
                 ([✓(res')], Z) ∈ ℱ (SKIP res') ∧ Z = (Z ∪ Z) ∩ (range tick ∪ ev ` S) ∪ Z ∩ Z›
        by (simp add: F_Det F_SKIP)
      show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: F_Sync ‹res = res'›) (meson "*")
    next
      fix a s' assume ‹s = ev a # s'›
      with ‹(s, Z) ∈ ℱ ?rhs1› have * : ‹a ∈ A› ‹a ∉ S› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
        by (simp_all add: F_Det F_SKIP F_Mprefix image_iff)
      from "*"(3) consider ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        | t u X Y where ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                        ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        by (simp add: F_Sync D_Sync) blast
      thus ‹(s, Z) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        hence ‹s ∈ 𝒟 ?rhs1›
          by (simp add: D_Det D_Mprefix image_iff "*"(1, 2) ‹s = ev a # s'›)
        with same_div show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: ‹res = res'› is_processT8)
      next
        fix t u X Y assume ** : ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                                ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                                ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        from "**"(2, 3) have ‹(ev a # s') setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
          by (auto simp add: "*"(1, 2) F_SKIP image_iff)
        thus ‹(s, Z) ∈ ℱ ?lhs›
          by (simp add: F_Sync F_Det F_Mprefix image_iff)
             (metis "*"(1) "**"(1, 2, 4) ‹s = ev a # s'› list.distinct(1))
      qed
    qed
  next
    assume ‹res ≠ res'› ‹(s, Z) ∈ ℱ ?rhs2›
    then consider ‹s = []›
      | a s' where ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
      by (auto simp add: F_Ndet F_STOP F_Mprefix)
    thus ‹(s, Z) ∈ ℱ ?lhs›
    proof cases
      have ‹([], UNIV) ∈ ℱ ?lhs›
        apply (simp add: F_Sync, rule disjI1)
        apply (rule_tac x = ‹[]› in exI, simp add: F_Det F_Mprefix F_SKIP T_SKIP D_SKIP)
        apply (rule_tac x = ‹[]› in exI, rule_tac x = ‹UNIV - {✓(res)}› in exI)
        apply (simp, rule_tac x = ‹UNIV - {✓(res')}› in exI)
        using ‹res ≠ res'› by auto
      thus ‹s = [] ⟹ (s, Z) ∈ ℱ ?lhs› by (auto intro: is_processT4)
    next
      fix a s' assume * : ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', Z) ∈ ℱ (P a ⟦S⟧ SKIP res')›
      from "*"(4) consider ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        | t u X Y where ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                        ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        by (auto simp add: F_Sync D_Sync)
      thus ‹(s, Z) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (P a ⟦S⟧ SKIP res')›
        hence ‹s ∈ 𝒟 ?rhs2› by (simp add: "*"(1, 2, 3) D_Ndet D_Mprefix)
        with same_div show ‹(s, Z) ∈ ℱ ?lhs› by (simp add: ‹res ≠ res'› is_processT8)
      next
        fix t u X Y assume ** : ‹(t, X) ∈ ℱ (P a)› ‹(u, Y) ∈ ℱ (SKIP res')›
                                ‹s' setinterleaves ((t, u), range tick ∪ ev ` S)›
                                ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
        show ‹(s, Z) ∈ ℱ ?lhs›
          apply (simp add: F_Sync, rule disjI1)
          apply (rule_tac x = ‹ev a # t› in exI)
          apply (rule_tac x = u in exI)
          apply (rule_tac x = X in exI)
          apply (rule conjI, solves ‹simp add: F_Det F_Mprefix "*"(1) "**"(1)›)
          apply (rule_tac x = Y in exI)
          apply (simp add: "**"(2, 4))
          using "**"(2, 3) by (auto simp add: "*"(1, 2, 3) F_SKIP)
      qed
    qed
  qed
qed


lemma Sliding_def_bis : ‹P ⊳ Q = (P ⊓ Q) □ Q›
  by (simp add: Det_distrib_Ndet_right Sliding_def)





section ‹Powerful Results about \<^const>‹Hiding››

theorem Hiding_is_Hiding_restricted_superset_events:
  fixes S :: ‹'a set› and P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  assumes superset : ‹α(P) ⊆ A›
  defines ‹S' ≡ S ∩ A›
  shows ‹P \ S = P \ S'›
proof -
  have set_trace_subset : ‹t ∈ 𝒯 P ⟹ set t ⊆ range tick ∪ ev ` α(P)› for t
    by (simp add: events_of_def subset_iff image_iff) (metis event⇩p⇩t⇩i⇩c⇩k.exhaust)
  moreover from superset
  have ‹set t ⊆ range tick ∪ ev ` α(P) ⟹
        trace_hide t (ev ` S) = trace_hide t (ev ` S')› for t :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
    by (induct t) (auto simp add: S'_def image_iff subset_iff)
  ultimately have same_trace_hide :
    ‹t ∈ 𝒯 P ⟹ trace_hide t (ev ` S) = trace_hide t (ev ` S')› for t by blast

  have ‹isInfHidden_seqRun_strong x P S t ⟹ seqRun t x i ∈ 𝒯 P› for x t S i by simp
  from this[THEN set_trace_subset]
  have ‹isInfHidden_seqRun_strong x P S t ⟹ x i ∈ ev ` α(P)› for x t S i
    by (simp add: seqRun_def subset_iff image_iff)
      (metis atLeastLessThan_iff event⇩p⇩t⇩i⇩c⇩k.simps(4) le0 lessI)
  moreover have ‹isInfHidden_seqRun_strong x P S t ⟹
                 trace_hide t (ev ` S) = trace_hide t (ev ` S')› for x t
    by (metis same_trace_hide seqRun_0)
  ultimately have IH_strong_iff :
    ‹isInfHidden_seqRun_strong x P S t ⟷ isInfHidden_seqRun_strong x P S' t› for x t
    by (safe, auto simp add: S'_def)
      (metis (no_types, lifting) ext S'_def lessI same_trace_hide trace_hide_seqRun_eq_iff)

  show ‹P \ S = P \ S'›
  proof (subst Process_eq_spec_optimized, safe)
    show ‹t ∈ 𝒟 (P \ S) ⟹ t ∈ 𝒟 (P \ S')› for t
    proof (elim D_Hiding_seqRunE disjE exE)
      fix u v assume ‹ftF v› ‹tF u› ‹t = trace_hide u (ev ` S) @ v› ‹u ∈ 𝒟 P›
      from ‹u ∈ 𝒟 P› D_T same_trace_hide
      have ‹trace_hide u (ev ` S) = trace_hide u (ev ` S')› by blast
      with ‹ftF v› ‹tF u› ‹u ∈ 𝒟 P› ‹t = trace_hide u (ev ` S) @ v›
      show ‹t ∈ 𝒟 (P \ S')› unfolding D_Hiding by blast
    next
      fix u v x assume ‹ftF v› ‹tF u› ‹t = trace_hide u (ev ` S) @ v›
        and IH_strong : ‹isInfHidden_seqRun_strong x P S u›
      have ‹trace_hide u (ev ` S) = trace_hide u (ev ` S')›
        by (metis IH_strong same_trace_hide seqRun_0)
      moreover from IH_strong have ‹isInfHidden_seqRun_strong x P S' u›
        by (simp add: IH_strong_iff)
      ultimately show ‹t ∈ 𝒟 (P \ S')›
        using ‹ftF v› ‹tF u› ‹t = trace_hide u (ev ` S) @ v›
        by (blast intro: D_Hiding_seqRunI)
    qed
  next
    show ‹t ∈ 𝒟 (P \ S') ⟹ t ∈ 𝒟 (P \ S)› for t
    proof (elim D_Hiding_seqRunE disjE exE)
      fix u v assume ‹ftF v› ‹tF u› ‹t = trace_hide u (ev ` S') @ v› ‹u ∈ 𝒟 P›
      from ‹u ∈ 𝒟 P› D_T same_trace_hide
      have ‹trace_hide u (ev ` S') = trace_hide u (ev ` S)› by metis
      with ‹ftF v› ‹tF u› ‹u ∈ 𝒟 P› ‹t = trace_hide u (ev ` S') @ v›
      show ‹t ∈ 𝒟 (P \ S)› unfolding D_Hiding by blast
    next
      fix u v x assume ‹ftF v› ‹tF u› ‹t = trace_hide u (ev ` S') @ v›
        and IH_strong : ‹isInfHidden_seqRun_strong x P S' u›
      have ‹trace_hide u (ev ` S') = trace_hide u (ev ` S)›
        by (metis IH_strong same_trace_hide seqRun_0)
      moreover from IH_strong have ‹isInfHidden_seqRun_strong x P S u›
        by (simp flip: IH_strong_iff)
      ultimately show ‹t ∈ 𝒟 (P \ S)›
        using ‹ftF v› ‹tF u› ‹t = trace_hide u (ev ` S') @ v›
        by (blast intro: D_Hiding_seqRunI)
    qed
  next
    fix t X assume same_div : ‹𝒟 (P \ S) = 𝒟 (P \ S')›
    assume ‹(t, X) ∈ ℱ (P \ S)›
    then consider ‹t ∈ 𝒟 (P \ S)›
      | u where ‹t = trace_hide u (ev ` S)› ‹(u, X ∪ ev ` S) ∈ ℱ P›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(t, X) ∈ ℱ (P \ S')›
    proof cases
      from same_div D_F show ‹t ∈ 𝒟 (P \ S) ⟹ (t, X) ∈ ℱ (P \ S')› by blast
    next
      fix u assume ‹t = trace_hide u (ev ` S)› ‹(u, X ∪ ev ` S) ∈ ℱ P›
      with F_T same_trace_hide have ‹t = trace_hide u (ev ` S')› by blast
      moreover have ‹(u, X ∪ ev ` S') ∈ ℱ P›
      proof (rule is_processT4)
        show ‹(u, X ∪ ev ` S) ∈ ℱ P› by (fact ‹(u, X ∪ ev ` S) ∈ ℱ P›)
      next
        show ‹X ∪ ev ` S' ⊆ X ∪ ev ` S› unfolding S'_def by blast
      qed
      ultimately show ‹(t, X) ∈ ℱ (P \ S')› unfolding F_Hiding by blast
    qed
  next
    fix t X assume same_div : ‹𝒟 (P \ S) = 𝒟 (P \ S')›
    assume ‹(t, X) ∈ ℱ (P \ S')›
    then consider ‹t ∈ 𝒟 (P \ S')›
      | u where ‹t = trace_hide u (ev ` S')› ‹(u, X ∪ ev ` S') ∈ ℱ P›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(t, X) ∈ ℱ (P \ S)›
    proof cases
      from same_div D_F show ‹t ∈ 𝒟 (P \ S') ⟹ (t, X) ∈ ℱ (P \ S)› by blast
    next
      fix u assume ‹t = trace_hide u (ev ` S')› ‹(u, X ∪ ev ` S') ∈ ℱ P›
      with F_T same_trace_hide have ‹t = trace_hide u (ev ` S)› by metis
      moreover have ‹(u, X ∪ ev ` S) ∈ ℱ P›
      proof (rule is_processT4[OF add_complementary_events_of_in_failure])
        show ‹(u, X ∪ ev ` S') ∈ ℱ P› by (fact ‹(u, X ∪ ev ` S') ∈ ℱ P›)
      next
        from superset show ‹X ∪ ev ` S ⊆ X ∪ ev ` S' ∪ ev ` (- α(P))›
          unfolding S'_def by blast
      qed
      ultimately show ‹(t, X) ∈ ℱ (P \ S)› unfolding F_Hiding by blast
    qed
  qed
qed




corollary Hiding_is_Hiding_restricted_events : ‹P \ S = P \ S ∩ α(P)›
  by (simp add: Hiding_is_Hiding_restricted_superset_events)

text ‹This version is closer to the intuition that we may have, but the first one would be more
useful if we don't want to compute the events of a process but know a superset approximation.›



(*<*)
end 
(*>*)