Theory NewLaws

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : New laws
 *
 * Copyright (c) 2023 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  NewLaws
  imports Interrupt Sliding Throw
begin

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

text ‹In this section we will provide laws about the \<^const>‹Renaming› operator.
      In the first subsection we will give slight generalizations of previous results,
      but in the other we prove some very powerful theorems.›

subsection ‹Some Generalizations›

text ‹For \<^const>‹Renaming›, we can obtain generalizations of the following results:

      @{thm Renaming_Mprefix[no_vars] Renaming_Mndetprefix[no_vars]}›

lemma Renaming_Mprefix:
  ‹Renaming (□a ∈ A → P a) f = 
   □y ∈ f ` A → ⊓a ∈ {x ∈ A. y = f x}. Renaming (P a) f› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Renaming D_Mprefix D_GlobalNdet hd_map_EvExt)
       (use list.map_sel(2) tickFree_tl in blast)
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then obtain a s' where * : ‹a ∈ A› ‹s = EvExt f (ev a) # s'›
                             ‹s' ∈ 𝒟 (Renaming (P a) f)›
    by (simp add: D_Mprefix EvExt_def D_GlobalNdet split: if_split_asm)
       (metis list.collapse)
  from "*"(3) obtain s1 s2 
    where ** : ‹tickFree s1› ‹front_tickFree s2› 
               ‹s' = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 (P a)›
    by (simp add: D_Renaming) blast
  have *** : ‹tickFree (ev a # s1) ∧ 
              s = EvExt f (ev a) # map (EvExt f) s1 @ s2 ∧ ev a # s1 ∈ 𝒟 (Mprefix A P)›
    by (simp add: D_Mprefix "*"(1, 2) "**"(1, 3, 4))
  show ‹s ∈ 𝒟 ?lhs›
    by (simp add: D_Renaming )
       (metis "**"(2) "***" append_Cons list.simps(9))
next
  fix s X
  assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | ‹∃t. (t, EvExt f -` X) ∈ ℱ (Mprefix A P) ∧ s = map (EvExt f) t›
    by (simp add: F_Renaming D_Renaming) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from D_F same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    assume ‹∃t. (t, EvExt f -` X) ∈ ℱ (Mprefix A P) ∧ s = map (EvExt f) t›
    then obtain t where * : ‹(t, EvExt f -` X) ∈ ℱ (Mprefix A P)› 
                            ‹s = map (EvExt f) t› by blast
    show ‹(s, X) ∈ ℱ ?rhs›
    proof (cases ‹t = []›)
      from "*" show ‹t = [] ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Mprefix disjoint_iff_not_equal)
           (metis ev_elem_anteced1)
    next
      assume ‹t ≠ []›
      with "*"(1) obtain a t'
        where ** : ‹a ∈ A› ‹t = ev a # t'› ‹(t', EvExt f -` X) ∈ ℱ (P a)›
        by (simp add: F_Mprefix) (metis event.inject imageE list.exhaust_sel)
      have *** : ‹s ≠ [] ∧ hd s ∈ ev ` f ` A›
        using "*"(2) "**"(1, 2) hd_map_EvExt by fastforce
      with "**" have ‹ev (f a) = hd s ∧ 
                     (tl s, X) ∈ ℱ (⊓a ∈ {x ∈ A. f a = f x}. Renaming (P a) f)›
        by (simp add: F_GlobalNdet "*"(2) F_Renaming)
           (metis (no_types, opaque_lifting) ‹t ≠ []› hd_map hd_map_EvExt list.sel(1))
      with "***" show ‹(s, X) ∈ ℱ ?rhs› by (simp add: F_Mprefix) blast
    qed
  qed
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
  proof (cases s)
    show ‹s = [] ⟹ (s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: F_Mprefix F_Renaming disjoint_iff_not_equal)
         (metis ev_elem_anteced1)
  next
    fix b s'
    assume ‹s = b # s'› ‹(s, X) ∈ ℱ ?rhs›
    then obtain a
      where * : ‹a ∈ A› ‹s = (EvExt f) (ev a) # s'› (* ‹b = ev (f a)› *)
                ‹(s', X) ∈ ℱ (⊓a ∈ {x ∈ A. f a = f x}. Renaming (P a) f)›
      by (auto simp add: F_Mprefix EvExt_def)
    from "*"(1, 3) obtain a'
      where ** : ‹a' ∈ A› ‹f a' = f a› ‹(s', X) ∈ ℱ (Renaming (P a') f)›
      by (auto simp add: F_GlobalNdet split: if_split_asm)
    from "**"(3) consider 
      ‹∃t. (t, EvExt f -` X) ∈ ℱ (P a') ∧ s' = map (EvExt f) t›
      | ‹∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ 
                 s' = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 (P a')›
      by (simp add: F_Renaming) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹∃t. (t, EvExt f -` X) ∈ ℱ (P a') ∧ s' = map (EvExt f) t›
      then obtain t where *** : ‹(t, EvExt f -` X) ∈ ℱ (P a')›
                                ‹s' = map (EvExt f) t› by blast
      have **** : ‹(ev a' # t, EvExt f -` X) ∈ ℱ (Mprefix A P) ∧ 
                   s = map (EvExt f) (ev a' # t)›
        by (simp add: F_Mprefix "*"(2) "**"(1) "***"(1, 2))
           (metis "**"(2) ev_elem_anteced1 vimage_singleton_eq)
      show ‹(s, X) ∈ ℱ ?lhs›
        apply (simp add: F_Renaming)
        using "****" by blast
    next
      assume ‹∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ 
                      s' = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 (P a')›
      then obtain s1 s2
        where *** : ‹tickFree s1› ‹front_tickFree s2› 
                    ‹s' = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 (P a')› by blast
      have ‹tickFree (ev a' # s1) ∧ 
            s = EvExt f (ev a') # map (EvExt f) s1 @ s2 ∧ 
            ev a' # s1 ∈ 𝒟 (Mprefix A P)›
        by (simp add: "*"(2) "**"(1) "***" D_Mprefix) 
           (metis "**"(2) ev_elem_anteced1 vimage_singleton_eq)
      thus ‹(s, X) ∈ ℱ ?lhs› by (auto simp add: "***"(2) F_Renaming)   
    qed
  qed
qed


lemma Renaming_Mprefix_Sliding:
  ‹Renaming ((□a ∈ A → P a) ⊳ Q) f = 
   (□y ∈ f ` A → ⊓a ∈ {x ∈ A. y = f x}. Renaming (P a) f) ⊳ Renaming Q f›
  unfolding Sliding_def
  by (simp add: Renaming_Ndet Renaming_Det Renaming_Mprefix)


lemma Renaming_GlobalNdet:
  ‹Renaming (⊓a ∈ A. P a) f = ⊓b ∈ f ` A. ⊓a ∈ {a ∈ A. b = f a}. Renaming (P a) f›
  by (simp add: Process_eq_spec F_Renaming
                F_GlobalNdet D_Renaming D_GlobalNdet) blast


lemma Renaming_Mndetprefix:
  ‹Renaming (⊓a ∈ A → P a) f = 
   ⊓y ∈ f ` A → ⊓a ∈ {x ∈ A. y = f x}. Renaming (P a) f› (is ‹?lhs = ?rhs›)
  apply (subst (1 2) Mndetprefix_GlobalNdet)
  apply (simp add: Renaming_GlobalNdet Renaming_prefix)
  apply (intro mono_GlobalNdet_eq ballI)
  apply (subst write0_GlobalNdet[symmetric], blast)
  by (simp add: mono_GlobalNdet_eq) 



subsection ‹\<^const>‹Renaming› and \<^const>‹Hiding››

text ‹When \<^term>‹f› is one to one, \<^term>‹Renaming (P \ S) f› will behave like we expect it to do.›

lemma strict_mono_map: ‹strict_mono g ⟹ strict_mono (λi. map f (g i))›
  unfolding strict_mono_def less_list_def le_list_def
  by (metis list.map_disc_iff map_append self_append_conv)


lemma trace_hide_map_EvExt :
  ‹inj_on (EvExt f) (set s ∪ ev ` S) ⟹
   trace_hide (map (EvExt f) s) (ev ` f ` S) = 
   map (EvExt f) (trace_hide s (ev ` S))›
proof (induct s)
  case Nil
  show ?case by simp
next
  case (Cons a s)
  hence * : ‹trace_hide (map (EvExt f) s) (ev ` f ` S) = 
             map (EvExt f) (trace_hide s (ev ` S))› by fastforce
  from Cons.prems[unfolded inj_on_def, rule_format, of a, simplified] show ?case
    apply (simp add: "*")
    apply (simp add: image_iff split: event.split)
    by (metis ev_elem_anteced1 singletonI vimage_singleton_eq)
qed
  

lemma inj_on_EvExt_iff: ‹inj_on (EvExt f) (insert tick (ev ` S)) ⟷ inj_on f S›
  unfolding inj_on_def EvExt_def by (auto split: event.split)

lemma inj_on_EvExt_set_T:
  ‹inj_on f (events_of P) ⟹ s ∈ 𝒯 P ⟹ inj_on (EvExt f) (insert tick (set s))›
  unfolding inj_on_def EvExt_def events_of_def by (auto split: event.split)


theorem bij_Renaming_Hiding: ‹Renaming (P \ S) f = Renaming P f \ f ` S›
  (is ‹?lhs = ?rhs›) if bij_f: ‹bij f›
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then obtain s1 s2 where * : ‹tickFree s1› ‹front_tickFree s2›
                              ‹s = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 (P \ S)›
    by (simp add: D_Renaming) blast
  from "*"(4) obtain t u
    where ** : ‹front_tickFree u› ‹tickFree t› ‹s1 = trace_hide t (ev ` S) @ u›
               ‹t ∈ 𝒟 P ∨ (∃g. isInfHiddenRun g P S ∧ t ∈ range g)›
    by (simp add: D_Hiding) blast
  from "**"(4) show ‹s ∈ 𝒟 ?rhs›
  proof (elim disjE)
    assume ‹t ∈ 𝒟 P›
    hence ‹front_tickFree (map (EvExt f) u @ s2) ∧ tickFree (map (EvExt f) t) ∧
           s = trace_hide (map (EvExt f) t) (ev ` f ` S) @ map (EvExt f) u @ s2 ∧
           map (EvExt f) t ∈ 𝒟 (Renaming P f)›
      apply (simp add: "*"(3) "**"(2, 3) EvExt_tF, intro conjI)
      subgoal using "*"(1, 2) "**"(3) EvExt_tF front_tickFree_append tickFree_append by blast
      subgoal by (rule trace_hide_map_EvExt[symmetric];
              use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto split: event.split›)
      using "**"(2) D_Renaming front_tickFree_Nil by blast
    thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Hiding) blast
  next
    assume ‹∃g. isInfHiddenRun g P S ∧ t ∈ range g›
    then obtain g where ‹isInfHiddenRun g P S› ‹t ∈ range g› by blast
    hence ‹front_tickFree (map (EvExt f) u @ s2) ∧
           tickFree (map (EvExt f) t) ∧
           s = trace_hide (map (EvExt f) t) (ev ` f ` S) @ map (EvExt f) u @ s2 ∧
           isInfHiddenRun (λi. map (EvExt f) (g i)) (Renaming P f) (f ` S) ∧ 
           map (EvExt f) t ∈ range (λi. map (EvExt f) (g i))›
      apply (simp add: "*"(3) "**"(2, 3) EvExt_tF, intro conjI)
      subgoal using "*"(1, 2) "**"(3) EvExt_tF front_tickFree_append tickFree_append by blast
      subgoal by (rule trace_hide_map_EvExt[symmetric];
                 use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto split: event.split›)
      subgoal using strict_mono_map by blast
      subgoal by (solves ‹auto simp add: T_Renaming›)
      subgoal apply (subst (1 2) trace_hide_map_EvExt)
        by (use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto split: event.split›) metis
      subgoal by blast
      done
    thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Hiding) blast
  qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then obtain t u
    where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` f ` S) @ u›
              ‹t ∈ 𝒟 (Renaming P f) ∨ 
               (∃g. isInfHiddenRun g (Renaming P f) (f ` S) ∧ t ∈ range g)›
    by (simp add: D_Hiding) blast
  from "*"(4) show ‹s ∈ 𝒟 ?lhs›
  proof (elim disjE)
    assume ‹t ∈ 𝒟 (Renaming P f)›
    then obtain t1 t2 where ** : ‹tickFree t1› ‹front_tickFree t2› 
                                 ‹t = map (EvExt f) t1 @ t2› ‹t1 ∈ 𝒟 P›
      by (simp add: D_Renaming) blast
    have ‹tickFree (trace_hide t1 (ev ` S)) ∧ 
          front_tickFree (trace_hide t2 (ev ` f ` S) @ u) ∧
          trace_hide (map (EvExt f) t1) (ev ` f ` S) @ trace_hide t2 (ev ` f ` S) @ u =
          map (EvExt f) (trace_hide t1 (ev ` S)) @ trace_hide t2 (ev ` f ` S) @ u ∧
          trace_hide t1 (ev ` S) ∈ 𝒟 (P \ S)›
      apply (simp, intro conjI)
      subgoal using "**"(1) Hiding_tickFree by blast
      subgoal using "*"(1, 2) "**"(3) Hiding_tickFree front_tickFree_append tickFree_append by blast
      subgoal by (rule trace_hide_map_EvExt;
              use bij_f in ‹unfold bij_def inj_on_def EvExt_def, simp split: event.split›)
      subgoal using "**"(4) elemDIselemHD by blast
      done
    thus ‹s ∈ 𝒟 ?lhs› by (simp add: D_Renaming "*"(3) "**"(3)) blast
  next
    have inv_S: ‹S = inv f ` f ` S› by (simp add: bij_is_inj bij_f)
    have inj_inv_f: ‹inj (inv f)› 
      by (simp add: bij_imp_bij_inv bij_is_inj bij_f)
    have ** : ‹map (EvExt (inv f) ∘ EvExt f) v = v› for v
        by (induct v, unfold EvExt_def, auto split: event.split)
           (metis bij_inv_eq_iff bij_f)
    assume ‹∃g. isInfHiddenRun g (Renaming P f) (f ` S) ∧ t ∈ range g›
    then obtain g
      where *** : ‹isInfHiddenRun g (Renaming P f) (f ` S)› ‹t ∈ range g› by blast
    then consider ‹∃t1. t1 ∈ 𝒯 P ∧ t = map (EvExt f) t1›
      | ‹∃t1 t2. tickFree t1 ∧ front_tickFree t2 ∧ 
                 t = map (EvExt f) t1 @ t2 ∧ t1 ∈ 𝒟 P›
      by (simp add: T_Renaming) blast
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      assume ‹∃t1. t1 ∈ 𝒯 P ∧ t = map (EvExt f) t1›
      then obtain t1 where **** : ‹t1 ∈ 𝒯 P› ‹t = map (EvExt f) t1› by blast
      have ***** : ‹t1 = map (EvExt (inv f)) t› by (simp add: "****"(2) "**")
      have ****** : ‹trace_hide t1 (ev ` S) = trace_hide t1 (ev ` S) ∧
                     isInfHiddenRun (λi. map (EvExt (inv f)) (g i)) P S ∧ 
                     t1 ∈ range (λi. map (EvExt (inv f)) (g i))›
        apply (simp add: "***"(1) strict_mono_map, intro conjI)
        subgoal apply (subst Renaming_inv[where f = f, symmetric])
           apply (solves ‹simp add: bij_is_inj bij_f›)
          using "***"(1) by (subst T_Renaming, blast)
        subgoal apply (subst (1 2) inv_S, subst (1 2) trace_hide_map_EvExt)
          by (use bij_f in ‹unfold bij_def inj_on_def EvExt_def, 
                                auto simp add: inj_eq inj_inv_f split: event.split›)
              (metis "***"(1))
        subgoal using "***"(2) "*****" by blast
        done
      have ‹tickFree (trace_hide t1 (ev ` S)) ∧ front_tickFree t1 ∧
            trace_hide (map (EvExt f) t1) (ev ` f ` S) @ u = 
            map (EvExt f) (trace_hide t1 (ev ` S)) @ u ∧ 
            trace_hide t1 (ev ` S) ∈ 𝒟 (P \ S)›
        apply (simp, intro conjI)
        subgoal using "*"(2) "****"(2) EvExt_tF Hiding_tickFree by blast

        subgoal using "****"(1) is_processT2_TR by blast
        apply (rule trace_hide_map_EvExt,
                use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto split: event.split›)[1]
        apply (simp add: D_Renaming D_Hiding)
        using "*"(2) "*****" "******" EvExt_tF front_tickFree_Nil by blast
      with "*"(1) show ‹s ∈ 𝒟 ?lhs› by (simp add: D_Renaming "*"(3) "****"(2)) blast
    next
      assume ‹∃t1 t2. tickFree t1 ∧ front_tickFree t2 ∧ 
                      t = map (EvExt f) t1 @ t2 ∧ t1 ∈ 𝒟 P›
      then obtain t1 t2
        where **** : ‹tickFree t1› ‹front_tickFree t2›
                     ‹t = map (EvExt f) t1 @ t2› ‹t1 ∈ 𝒟 P› by blast
      have ‹tickFree (trace_hide t1 (ev ` S)) ∧
            front_tickFree (trace_hide t2 (ev ` f ` S) @ u) ∧
            trace_hide (map (EvExt f) t1) (ev ` f ` S) @ trace_hide t2 (ev ` f ` S) @ u =
            map (EvExt f) (trace_hide t1 (ev ` S)) @ trace_hide t2 (ev ` f ` S) @ u ∧
            trace_hide t1 (ev ` S) ∈ 𝒟 (P \ S)›
        apply (simp, intro conjI)
        subgoal using "****"(1) Hiding_tickFree by blast
        subgoal using "*"(1, 2) "****"(3) Hiding_tickFree front_tickFree_append tickFree_append by blast
        subgoal by (rule trace_hide_map_EvExt;
                use bij_f in ‹unfold bij_def inj_on_def EvExt_def, simp split: event.split›)
        subgoal using "****"(4) elemDIselemHD by blast
        done
      thus ‹s ∈ 𝒟 ?lhs› by (simp add: D_Renaming "*"(3) "****"(3)) blast
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P \ S) ∧ s = map (EvExt f) s1›
    by (simp add: F_Renaming D_Renaming) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from D_F same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P \ S) ∧ s = map (EvExt f) s1›
    then obtain s1 where * : ‹(s1, EvExt f -` X) ∈ ℱ (P \ S)›
                             ‹s = map (EvExt f) s1› by blast
    from this(1) consider ‹s1 ∈ 𝒟 (P \ S)›
      | ‹∃t. s1 = trace_hide t (ev ` S) ∧ (t, EvExt f -` X ∪ ev ` S) ∈ ℱ P›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      assume ‹s1 ∈ 𝒟 (P \ S)›
      then obtain t u
        where ** : ‹front_tickFree u› ‹tickFree t› ‹s1 = trace_hide t (ev ` S) @ u›
                   ‹t ∈ 𝒟 P ∨ (∃g. isInfHiddenRun g P S ∧ t ∈ range g)›
        by (simp add: D_Hiding) blast
      have *** : ‹front_tickFree (map (EvExt f) u) ∧ tickFree (map (EvExt f) t) ∧
                  map (EvExt f) (trace_hide t (ev ` S)) @ map (EvExt f) u = 
                  trace_hide (map (EvExt f) t) (ev ` f ` S) @ (map (EvExt f) u)›
        by (simp add: EvExt_ftF EvExt_tF "**"(1, 2))
           (rule trace_hide_map_EvExt[symmetric];
            use bij_f in ‹unfold bij_def inj_on_def EvExt_def, simp split: event.split›)
      from "**"(4) show ‹(s, X) ∈ ℱ ?rhs›
      proof (elim disjE)
        assume ‹t ∈ 𝒟 P›
        hence $ : ‹map (EvExt f) t ∈ 𝒟 (Renaming P f)›
          apply (simp add: D_Renaming)
          using "**"(2) front_tickFree_Nil by blast
        show ‹(s, X) ∈ ℱ ?rhs›
          by (simp add: F_Hiding) (metis "$" "*"(2) "**"(3) "***" map_append)
      next
        assume ‹∃g. isInfHiddenRun g P S ∧ t ∈ range g›
        then obtain g where ‹isInfHiddenRun g P S› ‹t ∈ range g› by blast
        hence $ : ‹isInfHiddenRun (λi. map (EvExt f) (g i)) (Renaming P f) (f ` S) ∧ 
                   map (EvExt f) t ∈ range (λi. map (EvExt f) (g i))›
          apply (subst (1 2) trace_hide_map_EvExt,
                 (use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto split: event.split›)[2])
          by (simp add: strict_mono_map T_Renaming image_iff) (metis (mono_tags, lifting))
        show ‹(s, X) ∈ ℱ ?rhs›
          by (simp add: F_Hiding) 
             (metis (mono_tags, lifting) "$" "*"(2) "**"(3) "***" map_append)
      qed
    next
      assume ‹∃t. s1 = trace_hide t (ev ` S) ∧ (t, EvExt f -` X ∪ ev ` S) ∈ ℱ P›
      then obtain t where ** : ‹s1 = trace_hide t (ev ` S)› 
                               ‹(t, EvExt f -` X ∪ ev ` S) ∈ ℱ P› by blast
      have *** : ‹EvExt f -` X ∪ EvExt f -` ev ` f ` S = EvExt f -` X ∪ ev ` S›
        by (use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto simp add: image_iff split: event.split›)
           (metis (no_types, opaque_lifting) event.distinct(1) event.exhaust event.simps(4, 5) o_apply)
      have ‹map (EvExt f) (trace_hide t (ev ` S)) = 
            trace_hide (map (EvExt f) t) (ev ` f ` S) ∧
            (map (EvExt f) t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f)›
        apply (intro conjI)
         apply (rule trace_hide_map_EvExt[symmetric];
                use bij_f in ‹unfold bij_def inj_on_def EvExt_def, simp split: event.split›)
        apply (simp add: F_Renaming)
        using "**"(2) "***" by auto
      show ‹(s, X) ∈ ℱ ?rhs›
        apply (simp add: F_Hiding "*"(2) "**"(1))
        using ‹?this› by blast
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s ∈ 𝒟 ?rhs›
    | ‹∃t. s = trace_hide t (ev ` f ` S) ∧ 
           (t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f)›
    by (simp add: F_Hiding D_Hiding) blast
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    from D_F same_div show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
  next
    assume ‹∃t. s = trace_hide t (ev ` f ` S) ∧
                (t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f)›
    then obtain t
      where * : ‹s = trace_hide t (ev ` f ` S)›
                ‹(t, X ∪ ev ` f ` S) ∈ ℱ (Renaming P f)› by blast
    have ** : ‹EvExt f -` X ∪ EvExt f -` ev ` f ` S = EvExt f -` X ∪ ev ` S›
        by (use bij_f in ‹unfold bij_def inj_on_def EvExt_def, auto simp add: image_iff split: event.split›)
           (metis (no_types, opaque_lifting) event.distinct(1) event.exhaust event.simps(4, 5) o_apply)
    have ‹(∃s1. (s1, EvExt f -` X ∪ EvExt f -` ev ` f ` S) ∈ ℱ P ∧ t = map (EvExt f) s1) ∨ 
          (∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ t = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 P)›
      using "*"(2) by (simp add: F_Renaming)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof (elim disjE exE conjE)
      fix s1
      assume ‹(s1, EvExt f -` X ∪ EvExt f -` ev ` f ` S) ∈ ℱ P› ‹t = map (EvExt f) s1›
      hence ‹(trace_hide s1 (ev ` S), EvExt f -` X) ∈ ℱ (P \ S) ∧
             s = map (EvExt f) (trace_hide s1 (ev ` S))›
        apply (simp add: "*"(1) F_Hiding "**", intro conjI)
         apply blast
        by (rule trace_hide_map_EvExt;
            use bij_f in ‹unfold bij_def inj_on_def EvExt_def, simp split: event.split›)
      show ‹(s, X) ∈ ℱ ?lhs›
        apply (simp add: F_Renaming)
        using ‹?this› by blast
    next
      fix s1 s2
      assume ‹tickFree s1› ‹front_tickFree s2› ‹t = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 P›
      hence ‹tickFree (trace_hide s1 (ev ` S)) ∧ 
             front_tickFree (trace_hide s2 (ev ` f ` S)) ∧ 
             s = map (EvExt f) (trace_hide s1 (ev ` S)) @ trace_hide s2 (ev ` f ` S) ∧ 
             trace_hide s1 (ev ` S) ∈ 𝒟 (P \ S)›
        apply (simp add: F_Renaming "*"(1), intro conjI)
        subgoal using Hiding_tickFree by blast
        subgoal using Hiding_fronttickFree by blast
         apply (rule trace_hide_map_EvExt;
                use bij_f in ‹unfold bij_def inj_on_def EvExt_def, simp split: event.split›)
        using elemDIselemHD by blast
      show ‹(s, X) ∈ ℱ ?lhs›
        apply (simp add: F_Renaming)
        using ‹?this› by blast
    qed
  qed
qed



subsection ‹\<^const>‹Renaming› and \<^const>‹Sync››

text ‹Idem for the synchronization: when \<^term>‹f› is one to one, 
      \<^term>‹Renaming (P ⟦S⟧ Q)› will behave as expected.›

lemma exists_map_antecedent_if_subset_range:
  ‹set u ⊆ range f ⟹ ∃t. u = map f t›
  ― ‹In particular, when \<^term>‹f› is surjective or bijective.›
proof (induct u)
  show ‹∃t. [] = map f t› by simp
next
  fix a u
  assume prem : ‹set (a # u) ⊆ range f›
     and  hyp : ‹set u ⊆ range f ⟹ ∃t. u = map f t›
  then obtain t where * : ‹u = map f t› 
    by (meson set_subset_Cons subset_trans)
  from prem obtain x where ** : ‹f x = a› by auto
  show ‹∃t. a # u = map f t›
  proof (intro exI)
    show ‹a # u = map f (x # t)› by (simp add: "*" "**")
  qed
qed


lemma bij_map_setinterleaving_iff_setinterleaving :
  ‹map f r setinterleaves ((map f t, map f u), f ` S) ⟷
   r setinterleaves ((t, u), S)› if bij_f : ‹bij f›
proof (induct ‹(t, S, u)› arbitrary: t u r rule: setinterleaving.induct)
  case 1
  thus ?case by simp
next
  case (2 y u)
  show ?case
  proof (cases ‹y ∈ S›)
    show ‹y ∈ S ⟹ ?case› by simp
  next
    assume ‹y ∉ S›
    hence ‹f y ∉ f ` S› by (metis bij_betw_imp_inj_on inj_image_mem_iff bij_f)
    with "2.hyps"[OF ‹y ∉ S›, of ‹tl r›] show ?case
      by (cases r; simp add: ‹y ∉ S›) (metis bij_pointE bij_f)
  qed
next
  case (3 x t)
  show ?case
  proof (cases ‹x ∈ S›)
    show ‹x ∈ S ⟹ ?case› by simp
  next
    assume ‹x ∉ S›
    hence ‹f x ∉ f ` S› by (metis bij_betw_imp_inj_on inj_image_mem_iff bij_f)
    with "3.hyps"[OF ‹x ∉ S›, of ‹tl r›] show ?case
      by (cases r; simp add: ‹x ∉ S›) (metis bij_pointE bij_f)
  qed
next
  case (4 x t y u)
  have  * : ‹x ≠ y ⟹ f x ≠ f y› by (metis bij_pointE bij_f)
  have ** : ‹f z ∈ f ` S ⟷ z ∈ S› for z
    by (meson bij_betw_def inj_image_mem_iff bij_f)
  show ?case
  proof (cases ‹x ∈ S›; cases ‹y ∈ S›)
    from "4.hyps"(1)[of ‹tl r›] show ‹x ∈ S ⟹ y ∈ S ⟹ ?case›
      by (cases r; simp add: "*") (metis bij_pointE bij_f)
  next
    from "4.hyps"(2)[of ‹tl r›] show ‹x ∈ S ⟹ y ∉ S ⟹ ?case›
      by (cases r; simp add: "**") (metis bij_pointE bij_f)
  next
    from "4.hyps"(5)[of ‹tl r›] show ‹x ∉ S ⟹ y ∈ S ⟹ ?case›
      by (cases r; simp add: "**") (metis bij_pointE bij_f)
  next
    from "4.hyps"(3, 4)[of ‹tl r›] show ‹x ∉ S ⟹ y ∉ S ⟹ ?case›
      by (cases r; simp add: "**") (metis bij_pointE bij_f)
  qed
qed


theorem bij_Renaming_Sync:
  ‹Renaming (P ⟦S⟧ Q) f = Renaming P f ⟦f ` S⟧ Renaming Q f›
  (is ‹?lhs P Q = ?rhs P Q›) if bij_f: ‹bij f›
proof -
  ― ‹Three intermediate results.›
  have bij_EvExt_f : ‹bij (EvExt f)›
  proof (unfold bij_iff EvExt_def, intro allI ex1I)
    show ‹(case (EvExt (inv f)) e of ev x ⇒ (ev ∘ f) x | tick ⇒ tick) = e› for e
      by (simp add: EvExt_def split: event.split)
         (meson bij_inv_eq_iff bij_f)
  next
    show ‹(case e' of ev x ⇒ (ev ∘ f) x | tick ⇒ tick) = e ⟹
          e' = EvExt (inv f) e› for e e'
      by (simp add: EvExt_def split: event.splits)
         (metis bij_inv_eq_iff event.inject event.simps(3) bij_f)
  qed
  have EvExt_inv_f_is_inv_EvExt_f : ‹inv (EvExt f) = EvExt (inv f)›
  proof -
    have ‹EvExt (inv f) ∘ EvExt f = id›
      by (rule ext, simp add: EvExt_def split: event.split)
         (meson bij_betw_imp_inj_on inv_f_eq bij_f)
    thus ‹inv (EvExt f) = EvExt (inv f)›  
      by (metis EvExt_comp EvExt_id bij_betw_def inv_unique_comp surj_iff that)
  qed
  have sets_S_eq : ‹(EvExt f) ` (insert tick (ev ` S)) = insert tick (ev ` f ` S)›
    unfolding EvExt_def image_def by auto

  show ‹?lhs P Q = ?rhs P Q›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 (?lhs P Q)›
    then obtain s1 s2 where * : ‹tickFree s1› ‹front_tickFree s2›
                                ‹s = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: D_Renaming) blast
    from "*"(4) obtain t u r v 
      where ** : ‹front_tickFree v› ‹tickFree r ∨ v = []› 
                 ‹s1 = r @ v› ‹r setinterleaves ((t, u), insert tick (ev ` S))›
                 ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› 
      by (simp add: D_Sync) blast
    { fix t u P Q
      assume assms : ‹r setinterleaves ((t, u), insert tick (ev ` S))› 
                     ‹t ∈ 𝒟 P› ‹u ∈ 𝒯 Q›
      have ‹map (EvExt f) r setinterleaves 
            ((map (EvExt f) t, map (EvExt f) u), insert tick (ev ` f ` S))›
        by (metis assms(1) bij_EvExt_f 
                  bij_map_setinterleaving_iff_setinterleaving sets_S_eq)
      moreover have ‹map (EvExt f) t ∈ 𝒟 (Renaming P f)›
        apply (cases ‹tickFree t›; simp add: D_Renaming)
        using assms(2) front_tickFree_Nil apply blast
        by (metis (no_types, lifting) assms(2) butlast_snoc front_tickFree_butlast
                                      front_tickFree_single map_EvExt_tick map_append 
                                      nonTickFree_n_frontTickFree process_charn)
      moreover have ‹map (EvExt f) u ∈ 𝒯 (Renaming Q f)›
        using assms(3) by (simp add: T_Renaming) blast
      ultimately have ‹s ∈ 𝒟 (?rhs P Q)›
        by (simp add: D_Sync "*"(3) "**"(3))
           (metis "*"(1, 2) "**"(3) EvExt_tF front_tickFree_append tickFree_append)
    } note *** = this

    from "**"(4, 5) "***" show ‹s ∈ 𝒟 (?rhs P Q)›
      apply (elim disjE)
      using "**"(4) "***" apply blast
      using "**"(4) "***" by (subst Sync_commute) blast
  next
    fix s
    assume ‹s ∈ 𝒟 (?rhs P Q)›
    then obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v› 
                ‹r setinterleaves ((t, u), insert tick (ev ` f ` S))›
                ‹t ∈ 𝒟 (Renaming P f) ∧ u ∈ 𝒯 (Renaming Q f) ∨
                 t ∈ 𝒟 (Renaming Q f) ∧ u ∈ 𝒯 (Renaming P f)›
      by (simp add: D_Sync) blast

    { fix t u P Q
      assume assms : ‹r setinterleaves ((t, u), insert tick (ev ` f ` S))› 
                     ‹t ∈ 𝒟 (Renaming P f)› ‹u ∈ 𝒯 (Renaming Q f)›
      have ** : ‹(map (inv (EvExt f)) r) setinterleaves
                 ((map (inv (EvExt f)) t, map (inv (EvExt f)) u), insert tick (ev ` S))›
        by (metis (no_types) assms(1) bij_EvExt_f bij_betw_imp_inj_on
                             bij_betw_inv_into  image_inv_f_f sets_S_eq
                             bij_map_setinterleaving_iff_setinterleaving)
      have ‹map (EvExt (inv f)) t ∈ 𝒟 (Renaming (Renaming P f) (inv f))›
        by (subst D_Renaming, simp)
           (metis EvExt_ftF append.right_neutral assms(2) front_tickFree_implies_tickFree 
                  front_tickFree_single map_append nonTickFree_n_frontTickFree process_charn)
      hence *** : ‹map (inv (EvExt f)) t ∈ 𝒟 P›
        by (simp add: Renaming_inv bij_is_inj bij_f EvExt_inv_f_is_inv_EvExt_f)
      have ‹map (EvExt (inv f)) u ∈ 𝒯 (Renaming (Renaming Q f) (inv f))›
        using assms(3) by (subst T_Renaming, simp) blast
      hence **** : ‹map (inv (EvExt f)) u ∈ 𝒯 Q›
        by (simp add: Renaming_inv bij_is_inj bij_f EvExt_inv_f_is_inv_EvExt_f)
      have ***** : ‹map (EvExt f ∘ inv (EvExt f)) r = r›
        by (metis bij_EvExt_f bij_betw_imp_surj list.map_id surj_iff)
      have ‹s ∈ 𝒟 (?lhs P Q)›
      proof (cases ‹tickFree r›)
        assume ‹tickFree r›
        have $ : ‹r @ v = map (EvExt f) (map (inv (EvExt f)) r) @ v›
          by (simp add: "*****")
        show ‹s ∈ 𝒟 (?lhs P Q)›
          apply (simp add: D_Renaming D_Sync "*"(3))
          by (metis "$" "*"(1) "**" "***" "****" EvExt_tF ‹tickFree r› 
                    append.right_neutral append_same_eq front_tickFree_Nil)
      next
        assume ‹¬ tickFree r›
        then obtain r' where $ : ‹r = r' @ [tick]› ‹tickFree r'›
          by (metis D_imp_front_tickFree assms front_tickFree_implies_tickFree ftf_Sync
                    is_processT2_TR nonTickFree_n_frontTickFree)
        then obtain t' u'
          where $$ : ‹t = t' @ [tick]› ‹u = u' @ [tick]›
          using SyncWithTick_imp_NTF D_T assms by blast
        hence $$$ : ‹(map (inv (EvExt f)) r') setinterleaves
                     ((map (inv (EvExt f)) t', map (inv (EvExt f)) u'),
                      insert tick (ev ` S))›
          by (metis "$"(1) assms(1) bij_EvExt_f bij_betw_imp_inj_on 
                    bij_betw_inv_into bij_map_setinterleaving_iff_setinterleaving
                    butlast_snoc ftf_Sync32 image_inv_f_f sets_S_eq)
        from "***" $$(1) have *** : ‹map (inv (EvExt f)) t' ∈ 𝒟 P› 
          by simp (metis EvExt_inv_f_is_inv_EvExt_f is_processT9 tick_eq_EvExt)
        from "****" $$(2) have **** : ‹map (inv (EvExt f)) u' ∈ 𝒯 Q›
          using is_processT3_ST by simp blast
        have $$$$ : ‹r = map (EvExt f) (map (inv (EvExt f)) r') @ [tick]›
          using "$" "*****" by auto
        show ‹s ∈ 𝒟 (?lhs P Q)›
          by (simp add: D_Renaming D_Sync "*"(3) "$$$")
             (metis "$"(1) "$"(2) "$$$" "$$$$" "*"(2) "***" "****" EvExt_tF ‹¬ tickFree r›
                    append.right_neutral append_same_eq front_tickFree_Nil front_tickFree_single)
      qed
    } note ** = this
    show ‹s ∈ 𝒟 (?lhs P Q)› by (metis "*"(4, 5) "**" Sync_commute)
  next
    fix s X
    assume same_div : ‹𝒟 (?lhs P Q) = 𝒟 (?rhs P Q)›
    assume ‹(s, X) ∈ ℱ (?lhs P Q)›
    then consider ‹s ∈ 𝒟 (?lhs P Q)›
      | ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P ⟦S⟧ Q) ∧ s = map (EvExt f) s1›
      by (simp add: F_Renaming D_Renaming) blast
    thus ‹(s, X) ∈ ℱ (?rhs P Q)›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 (?lhs P Q) ⟹ (s, X) ∈ ℱ (?rhs P Q)› by blast
    next
      assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P ⟦S⟧ Q) ∧ s = map (EvExt f) s1›
      then obtain s1 where * : ‹(s1, EvExt f -` X) ∈ ℱ (P ⟦S⟧ Q)› 
                               ‹s = map (EvExt f) s1› by blast
      from "*"(1) consider ‹s1 ∈ 𝒟 (P ⟦S⟧ Q)›
        | ‹∃t_P t_Q X_P X_Q. 
           (t_P, X_P) ∈ ℱ P ∧ (t_Q, X_Q) ∈ ℱ Q ∧
           s1 setinterleaves ((t_P, t_Q), insert tick (ev ` S)) ∧
           EvExt f -` X = (X_P ∪ X_Q) ∩ insert tick (ev ` S) ∪ X_P ∩ X_Q›
        by (simp add: F_Sync D_Sync) blast
      thus ‹(s, X) ∈ ℱ (?rhs P Q)›
      proof cases
        assume ‹s1 ∈ 𝒟 (P ⟦S⟧ Q)›
        hence ‹s ∈ 𝒟 (?lhs P Q)›
          apply (cases ‹tickFree s1›; simp add: D_Renaming "*"(2)) 
          using front_tickFree_Nil apply blast
          by (metis (no_types, lifting) EvExt_ftF butlast_snoc front_tickFree_butlast
                    front_tickFree_single map_butlast nonTickFree_n_frontTickFree process_charn)
        with same_div D_F show ‹(s, X) ∈ ℱ (?rhs P Q)› by blast
      next
        assume ‹∃t_P t_Q X_P X_Q. 
                (t_P, X_P) ∈ ℱ P ∧ (t_Q, X_Q) ∈ ℱ Q ∧
                s1 setinterleaves ((t_P, t_Q), insert tick (ev ` S)) ∧
                EvExt f -` X = (X_P ∪ X_Q) ∩ insert tick (ev ` S) ∪ X_P ∩ X_Q›
        then obtain t_P t_Q X_P X_Q
          where ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
                     ‹s1 setinterleaves ((t_P, t_Q), insert tick (ev ` S))›
                     ‹EvExt f -` X = (X_P ∪ X_Q) ∩ insert tick (ev ` S) ∪ X_P ∩ X_Q› by blast
        have ‹(map (EvExt f) t_P, (EvExt f) ` X_P) ∈ ℱ (Renaming P f)›
          by (simp add: F_Renaming)
             (metis "**"(1) bij_EvExt_f bij_betw_imp_inj_on inj_vimage_image_eq)
        moreover have ‹(map (EvExt f) t_Q, (EvExt f) ` X_Q) ∈ ℱ (Renaming Q f)›
          by (simp add: F_Renaming)
             (metis "**"(2) bij_EvExt_f bij_betw_imp_inj_on inj_vimage_image_eq)
        moreover have ‹s setinterleaves ((map (EvExt f) t_P, map (EvExt f) t_Q),
                                         insert tick (ev ` f ` S))›
          by (metis "*"(2) "**"(3) bij_EvExt_f sets_S_eq
                    bij_map_setinterleaving_iff_setinterleaving)
        moreover have ‹X = ((EvExt f) ` X_P ∪ (EvExt f) ` X_Q) ∩ insert tick (ev ` f ` S) ∪
                           (EvExt f) ` X_P ∩ (EvExt f) ` X_Q›
          by (metis "**"(4) bij_EvExt_f bij_betw_def image_Int image_Un 
                    image_vimage_eq inf_top.right_neutral sets_S_eq)
        ultimately show ‹(s, X) ∈ ℱ (?rhs P Q)›
          by (simp add: F_Sync) blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 (?lhs P Q) = 𝒟 (?rhs P Q)›
    assume ‹(s, X) ∈ ℱ (?rhs P Q)›
    then consider ‹s ∈ 𝒟 (?rhs P Q)›
      | ‹∃t_P t_Q X_P X_Q.
         (t_P, X_P) ∈ ℱ (Renaming P f) ∧ (t_Q, X_Q) ∈ ℱ (Renaming Q f) ∧
         s setinterleaves ((t_P, t_Q), insert tick (ev ` f ` S)) ∧
         X = (X_P ∪ X_Q) ∩ insert tick (ev ` f ` S) ∪ X_P ∩ X_Q›
      by (simp add: F_Sync D_Sync) blast
    thus ‹(s, X) ∈ ℱ (?lhs P Q)›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 (?rhs P Q) ⟹ (s, X) ∈ ℱ (?lhs P Q)› by blast
    next
      assume ‹∃t_P t_Q X_P X_Q.
              (t_P, X_P) ∈ ℱ (Renaming P f) ∧ (t_Q, X_Q) ∈ ℱ (Renaming Q f) ∧
              s setinterleaves ((t_P, t_Q), insert tick (ev ` f ` S)) ∧
              X = (X_P ∪ X_Q) ∩ insert tick (ev ` f ` S) ∪ X_P ∩ X_Q›
      then obtain t_P t_Q X_P X_Q
        where * : ‹(t_P, X_P) ∈ ℱ (Renaming P f)› ‹(t_Q, X_Q) ∈ ℱ (Renaming Q f)›
                  ‹s setinterleaves ((t_P, t_Q), insert tick (ev ` f ` S))›
                  ‹X = (X_P ∪ X_Q) ∩ insert tick (ev ` f ` S) ∪ X_P ∩ X_Q› by blast
      from "*"(1, 2) consider ‹t_P ∈ 𝒟 (Renaming P f) ∨ t_Q ∈ 𝒟 (Renaming Q f)›
        | ‹∃t_P1 t_Q1. (t_P1, EvExt f -` X_P) ∈ ℱ P ∧ t_P = map (EvExt f) t_P1 ∧
                       (t_Q1, EvExt f -` X_Q) ∈ ℱ Q ∧ t_Q = map (EvExt f) t_Q1›
        by (simp add: F_Renaming D_Renaming) blast
      thus ‹(s, X) ∈ ℱ (?lhs P Q)›
      proof cases
        assume ‹t_P ∈ 𝒟 (Renaming P f) ∨ t_Q ∈ 𝒟 (Renaming Q f)›
        hence ‹s ∈ 𝒟 (?rhs P Q)›
          apply (simp add: D_Sync)
          using "*"(1, 2, 3) F_T Sync.sym front_tickFree_Nil by blast
        with same_div D_F show ‹(s, X) ∈ ℱ (?lhs P Q)› by blast
      next
        assume ‹∃t_P1 t_Q1. (t_P1, EvExt f -` X_P) ∈ ℱ P ∧ t_P = map (EvExt f) t_P1 ∧
                            (t_Q1, EvExt f -` X_Q) ∈ ℱ Q ∧ t_Q = map (EvExt f) t_Q1›
        then obtain t_P1 t_Q1
          where ** : ‹(t_P1, EvExt f -` X_P) ∈ ℱ P› ‹t_P = map (EvExt f) t_P1›
                     ‹(t_Q1, EvExt f -` X_Q) ∈ ℱ Q› ‹t_Q = map (EvExt f) t_Q1› by blast
        from "**"(2, 4) have *** : ‹t_P1 = map (inv (EvExt f)) t_P›
                                   ‹t_Q1 = map (inv (EvExt f)) t_Q›
          by (simp, metis bij_EvExt_f bij_betw_imp_inj_on inv_o_cancel list.map_id)+
        have **** : ‹map (EvExt f) (map (inv (EvExt f)) s) = s›
          by (metis bij_EvExt_f bij_betw_imp_surj list.map_comp list.map_id surj_iff)
        from bij_map_setinterleaving_iff_setinterleaving
                [of ‹inv (EvExt f)› s t_P ‹insert tick (ev ` f ` S)› t_Q, simplified "*"(3)]
        have ‹map (inv (EvExt f)) s setinterleaves ((t_P1, t_Q1), insert tick (ev ` S))›
          by (metis "***" bij_EvExt_f bij_betw_imp_inj_on
                    bij_betw_inv_into image_inv_f_f sets_S_eq)
        moreover have ‹EvExt f -` X = (EvExt f -` X_P ∪ EvExt f -` X_Q) ∩ insert tick (ev ` S) ∪ 
                      EvExt f -` X_P ∩ EvExt f -` X_Q›
          by (metis "*"(4) bij_EvExt_f bij_betw_imp_inj_on
                    inj_vimage_image_eq sets_S_eq vimage_Int vimage_Un)
        ultimately show ‹(s, X) ∈ ℱ (?lhs P Q)›
          by (simp add: F_Renaming F_Sync)
             (metis "**"(1, 3) "****")
      qed
    qed
  qed
qed


section ‹\<^const>‹Hiding› and \<^const>‹Mprefix››

text ‹We already have a way to distribute the \<^const>‹Hiding› operator on the
      \<^const>‹Mprefix› operator with @{thm Hiding_Mprefix_distr[of S A]}.
      But this is only usable when \<^term>‹A ∩ S = {}›. With the \<^const>‹Sliding›
      operator, we can now handle the case \<^term>‹A ∩ S ≠ {}›.›


subsection ‹Two intermediate Results›

lemma D_Hiding_Mprefix_dir2:
  assumes ‹s ∈ 𝒟 (□a ∈ A - S → (P a \ S))›
  shows ‹s ∈ 𝒟 (□a ∈ A → P a \ S)›
proof -
  from assms obtain a s'
    where * : ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹s' ∈ 𝒟 (P a \ S)›
    by (auto simp add: D_Mprefix) (metis list.collapse)
  from "*"(4) obtain t u 
    where ** : ‹front_tickFree u› ‹tickFree t› ‹s' = trace_hide t (ev ` S) @ u›
               ‹t ∈ 𝒟 (P a) ∨ (∃ f. isInfHiddenRun f (P a) S ∧ t ∈ range f)›
    by (simp add: D_Hiding) blast
  from "**"(4) show ‹s ∈ 𝒟 (□a ∈ A → P a \ S)›
  proof (elim disjE)
    assume ‹t ∈ 𝒟 (P a)›
    hence ‹tickFree (ev a # t) ∧ s = trace_hide (ev a # t) (ev ` S) @ u ∧
           ev a # t ∈ 𝒟 (Mprefix A P)›
      by (simp add: "*"(1, 2, 3) "**"(2, 3) image_iff[of ‹ev a›] D_Mprefix)
    show ‹s ∈ 𝒟 (Mprefix A P \ S)›
      apply (simp add: D_Hiding)
      using "**"(1) ‹?this› by blast
  next
    assume ‹∃f. isInfHiddenRun f (P a) S ∧ t ∈ range f›
    then obtain f where *** : ‹isInfHiddenRun f (P a) S› ‹t ∈ range f› by blast
    hence ‹tickFree (ev a # t) ∧ s = trace_hide (ev a # t) (ev ` S) @ u ∧
           isInfHiddenRun (λi. ev a # f i) (Mprefix A P) S ∧ 
           ev a # t ∈ range (λi. ev a # f i)›
      by (auto simp add: "*"(1, 2, 3) "**"(2, 3) image_iff[of ‹ev a›] 
                         T_Mprefix less_cons strict_mono_Suc_iff)
    show ‹s ∈ 𝒟 (Mprefix A P \ S)›
      apply (simp add: D_Hiding)
      using "**"(1) ‹?this› by blast
  qed
qed


lemma F_Hiding_Mprefix_dir2: 
  assumes ‹s ≠ []› and ‹(s, X) ∈ ℱ (□a ∈ A - S → (P a \ S))›
  shows ‹(s, X) ∈ ℱ (□a ∈ A → P a \ S)›
proof -
  from assms obtain a s'
    where * : ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', X) ∈ ℱ (P a \ S)›
    by (auto simp add: F_Mprefix) (metis list.collapse)
  from "*"(4) consider ‹s' ∈ 𝒟 (P a \ S)›
    | ‹∃t. s' = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (P a)›
    by (simp add: F_Hiding D_Hiding) blast
  thus ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
  proof cases
    assume ‹s' ∈ 𝒟 (P a \ S)›
    then obtain t u
      where ** : ‹front_tickFree u› ‹tickFree t› 
                 ‹s' = trace_hide t (ev ` S) @ u› 
                 ‹t ∈ 𝒟 (P a) ∨ (∃ f. isInfHiddenRun f (P a) S ∧ t ∈ range f)›
      by (simp add: D_Hiding) blast
    from "**"(4) show ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (P a)›
      hence ‹tickFree (ev a # t) ∧ s = trace_hide (ev a # t) (ev ` S) @ u ∧
             ev a # t ∈ 𝒟 (Mprefix A P)›
        by (simp add: "*"(1, 2, 3) "**"(2, 3) D_Mprefix image_iff[of ‹ev a›])
      show ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
        apply (simp add: F_Hiding)
        using "**"(1) ‹?this› by blast
    next
      assume ‹∃f. isInfHiddenRun f (P a) S ∧ t ∈ range f›
      then obtain f where ‹isInfHiddenRun f (P a) S› ‹t ∈ range f› by blast
      hence ‹tickFree (ev a # t) ∧ s = trace_hide (ev a # t) (ev ` S) @ u ∧
             (isInfHiddenRun (λi. ev a # f i) (Mprefix A P) S ∧ 
             ev a # t ∈ range (λi. ev a # f i))›
        by (auto simp add: "*"(1, 2, 3) "**"(2, 3) less_cons monotone_on_def T_Mprefix)
      show ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
        apply (simp add: F_Hiding)
        using "**"(1) ‹?this› by blast
    qed
  next
    assume ‹∃t. s' = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (P a)›
    then obtain t where ** : ‹s' = trace_hide t (ev ` S)›
                             ‹(t, X ∪ ev ` S) ∈ ℱ (P a)› by blast
    have ‹s = trace_hide (ev a # t) (ev ` S) ∧ (ev a # t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
      by (simp add: "*"(1, 2, 3) "**" F_Mprefix image_iff)
    show ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
      apply (simp add: F_Hiding)
      using ‹?this› by blast
  qed
qed



subsection ‹\<^const>‹Hiding› and \<^const>‹Mprefix› for disjoint Sets›

text ‹Now we can give a more readable proof of the following result 
      (already proven in \<^theory>‹HOL-CSP.CSP_Laws›).›

theorem Hiding_Mprefix_disjoint: 
  ‹□a ∈ A → P a \ S = □a ∈ A → (P a \ S)› 
  (is ‹?lhs = ?rhs›) if disjoint: ‹A ∩ S = {}›
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then obtain t u 
    where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` S) @ u›
              ‹t ∈ 𝒟 (Mprefix A P) ∨ 
               (∃ f. isInfHiddenRun f (Mprefix A P) S ∧ t ∈ range f)›
  by (simp add: D_Hiding) blast
  from "*"(4) show ‹s ∈ 𝒟 ?rhs›
  proof (elim disjE)
    assume ‹t ∈ 𝒟 (Mprefix A P)›
    then obtain a t' where ** : ‹a ∈ A› ‹a ∉ S› ‹t = ev a # t'› ‹t' ∈ 𝒟 (P a)›
      by (auto simp add: D_Mprefix) 
         (metis list.exhaust_sel disjoint_iff disjoint)
    have ‹front_tickFree u ∧ tickFree t' ∧
          trace_hide t' (ev ` S) @ u = trace_hide t' (ev ` S) @ u ∧ t' ∈ 𝒟 (P a)›
      apply (simp add: "*"(1) "**"(4))
      using "*"(2) "**"(3) tickFree_Cons by blast
    show ‹s ∈ 𝒟 ?rhs›
      apply (simp add: D_Mprefix "*"(3) "**"(1, 2, 3) image_iff[of ‹ev _›] D_Hiding)
      using ‹?this› by blast
  next
    assume ‹∃ f. isInfHiddenRun f (Mprefix A P) S ∧ t ∈ range f›
    then obtain f where ** : ‹isInfHiddenRun f (Mprefix A P) S›
                             ‹t ∈ range f› by blast
    from "**"(1) T_Mprefix obtain a
      where *** : ‹a ∈ A› ‹a ∉ S› ‹f (Suc 0) ≠ []› ‹hd (f (Suc 0)) = ev a›
      by (simp add: T_Mprefix) 
         (metis disjoint_iff disjoint nil_less strict_mono_Suc_iff)
    from "**"(1)[THEN conjunct2, THEN conjunct2, rule_format, of 1]
         "**"(1)[simplified isInfHiddenRun_1] "***"(1, 4) disjoint
    have **** : ‹f j ≠ [] ∧ hd (f j) = ev a› for j
      using "**"(1)[THEN conjunct2, THEN conjunct1, rule_format, of j]
      apply (cases ‹f 1›; simp add: T_Mprefix "***"(3) split: if_split_asm)
      by (metis Nil_is_append_conv filter.simps(1)
                hd_append2 list.distinct(1) list.sel(1)) blast
    then obtain t' where ‹t = ev a # t'›
      by (metis "**"(2) list.exhaust_sel rangeE)
    hence ‹tickFree t' ∧ trace_hide t' (ev ` S) @ u = trace_hide t' (ev ` S) @ u ∧
           isInfHiddenRun (λi. tl (f i)) (P a) S ∧ t' ∈ range (λi. tl (f i))›
      apply (simp, intro conjI)
      subgoal using "*"(2) tickFree_Cons by blast
      subgoal by (meson "**"(1) "****" less_tail strict_mono_Suc_iff)
      subgoal using "**"(1) by (simp add: T_Mprefix "****") 
      subgoal by (metis (no_types, lifting) "**"(1) "****" filter.simps(2) list.exhaust_sel list.sel(3))
      by (metis (no_types, lifting) "**"(2) image_iff list.sel(3))
    show ‹s ∈ 𝒟 ?rhs›
      apply (simp add: D_Mprefix "*"(3) image_iff[of ‹ev a›] "***"(1, 2) D_Hiding ‹t = ev a # t'›)
      using "*"(1) ‹?this› by blast
  qed
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (simp add: D_Hiding_Mprefix_dir2 Diff_triv that)
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)›
    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)›
    then obtain t where * : ‹s = trace_hide t (ev ` S)›
                            ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)› by blast
    show ‹(s, X) ∈ ℱ ?rhs›
    proof (cases ‹t = []›)
      from "*" show ‹t = [] ⟹ (s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Mprefix)
    next
      assume ‹t ≠ []›
      with "*"(2) disjoint obtain a t'
        where ** : ‹a ∈ A› ‹a ∉ S› ‹t = ev a # t'› ‹(t', X ∪ ev ` S) ∈ ℱ (P a)›
        by (cases t, auto simp add: F_Mprefix)
      show ‹(s, X) ∈ ℱ ?rhs›
        apply (simp add: F_Mprefix "*"(1) "**"(1, 2, 3) image_iff[of ‹ev a›])
        by (simp add: F_Hiding, rule disjI1, auto simp add: "**"(4))
    qed
  qed
next
  from disjoint show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    apply (cases ‹s = []›)
     apply (simp add: F_Mprefix F_Hiding disjoint_iff,
            metis event.inject filter.simps(1) imageE)
    by (simp add: Diff_triv F_Hiding_Mprefix_dir2)
qed


text ‹And we obtain a similar result when adding a \<^const>‹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_Ndet subsetI)
  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)
      by (metis (mono_tags, lifting) "*" NT_ND Nil_Nin_D_Mprefix  
                UNIV_I f_inv_into_f lessI nless_le 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 ‹\<^const>‹Hiding› and \<^const>‹Mprefix› for non-disjoint Sets›

text ‹Finally the new version, when \<^term>‹A ∩ S ≠ {}›.›

theorem Hiding_Mprefix_non_disjoint:
― ‹Rework this proof›
  ‹□a ∈ A → P a \ S = (□a ∈ A - S → (P a \ S)) ⊳ (⊓a ∈ A ∩ S. (P a \ S))›
  (is ‹?lhs = ?rhs›) if non_disjoint: ‹A ∩ S ≠ {}›
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then obtain t u 
    where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` S) @ u›
              ‹t ∈ 𝒟 (Mprefix A P) ∨ 
               (∃ f. isInfHiddenRun f (Mprefix A P) S ∧ t ∈ range f)›
    by (simp add: D_Hiding) blast
  from "*"(4) show ‹s ∈ 𝒟 ?rhs›
  proof (elim disjE)
    assume ‹t ∈ 𝒟 (Mprefix A P)›
    then obtain a t' where ** : ‹a ∈ A› ‹t = ev a # t'› ‹t' ∈ 𝒟 (P a)›
      by (simp add: D_Mprefix) 
         (metis event.inject image_iff list.exhaust_sel)
    have ‹tickFree t' ∧
          (if a ∈ S then s else tl s) = trace_hide t' (ev ` S) @ u ∧
          (t' ∈ 𝒟 (P a) ∨ (∃f. isInfHiddenRun f (P a) S ∧ t' ∈ range f))›
      using "*"(2) "**"(2, 3) by (auto simp add: "*"(1, 3) "**"(2) image_iff)
    with "*"(1) have *** : ‹(if a ∈ S then s else tl s) ∈ 𝒟 (P a \ S)› 
      by (simp add: D_Hiding) blast
    show ‹s ∈ 𝒟 ?rhs›
    proof (cases ‹a ∈ S›)
      assume ‹a ∈ S›
      hence ‹a ∈ A ∩ S› by (simp add: "**"(1))
      with "***" show ‹s ∈ 𝒟 ?rhs›
        by (auto simp add: D_Sliding D_GlobalNdet)
    next
      assume ‹a ∉ S›
      hence ‹a ∈ A - S› by (simp add: "**"(1))
      with "***" show ‹s ∈ 𝒟 ?rhs›
        by (auto simp add: D_Sliding D_Mprefix "*"(3) "**"(2) image_iff)
    qed
  next
    assume ‹∃ f. isInfHiddenRun f (Mprefix A P) S ∧ t ∈ range f›
    then obtain f  
      where ** : ‹isInfHiddenRun f (Mprefix A P) S› ‹t ∈ range f› by blast
    obtain k where ‹t = f k› using "**"(2) by blast
    show ‹s ∈ 𝒟 ?rhs›
    proof (cases ‹f 0 = []›)
      assume ‹f 0 = []›
      hence ‹f 1 ≠ []›
        by (metis "**"(1) One_nat_def monotoneD nil_less zero_less_Suc)
      with "**"(1)[THEN conjunct2, THEN conjunct1, rule_format, of 1]
      obtain a where *** : ‹a ∈ A› ‹f 1 ≠ []› ‹hd (f 1) = ev a›
        by (simp add: T_Mprefix) blast
      have **** : ‹0 < j ⟹ f j ≠ [] ∧ hd (f j) = ev a› for j
      proof (induct j rule: nat_induct_non_zero)
        from "***"(2, 3) show ‹f 1 ≠ [] ∧ hd (f 1) = ev a› by blast
      next
        case (Suc j)
        have ‹j < Suc j› by simp
        from "**"(1)[THEN conjunct1, THEN strict_monoD, OF this]
        obtain v where ‹f (Suc j) = f j @ v›
          by (metis le_list_def order_less_imp_le)
        thus ?case by (simp add: Suc.hyps(2))
      qed
      from "***"(1) have *****: ‹a ∈ A ∩ S›
        by simp (metis (no_types, lifting) "**"(1) "***"(2, 3)
                       ‹f 0 = []› empty_filter_conv event.inject
                       filter.simps(1) image_iff list.set_sel(1))
      have ‹(if i = 0 ∧ t = [] then [] else tl (f (Suc i))) ∈ 𝒯 (P a)› for i
      proof -
        from "**"(1) "****"[of ‹Suc i›] have ‹tl (f (Suc i)) ∈ 𝒯 (P a)›
          by (simp add: T_Mprefix) (metis event.inject)
        thus ‹(if i = 0 ∧ t = [] then [] else tl (f (Suc i))) ∈ 𝒯 (P a)›
          by (simp add: Nil_elem_T)
      qed
      hence ****** :
        ‹front_tickFree u ∧ tickFree (tl t) ∧
         s = trace_hide (tl t) (ev ` S) @ u ∧
         isInfHiddenRun (λi. if i = 0 ∧ t = [] then [] else tl (f (Suc i))) (P a) S ∧ 
         tl t ∈ range (λi. if i = 0 ∧ t = [] then [] else tl (f (Suc i)))›
        apply (intro conjI)
        subgoal by (solves ‹simp add: "*"(1)›)
        subgoal by (metis "*"(2) list.sel(2) tickFree_tl)
        subgoal by (metis "*"(3) "**"(1) ‹f 0 = []› ‹t = f k› empty_filter_conv
              filter.simps(1) list.sel(2) list.set_sel(2))
        subgoal by (simp add: monotone_on_def,
              metis "**"(1) Suc_less_eq less_list_def less_tail monotoneD
              nil_le nil_less zero_less_Suc)
        subgoal by blast
        subgoal by (simp, metis "**"(1) "****" ‹f 0 = []› empty_filter_conv
              filter.simps(1) list.set_sel(2) zero_less_Suc)
        by (simp add: image_iff,
            metis Suc_pred ‹f 0 = []› ‹t = f k› bot_nat_0.not_eq_extremum)
      have ‹a ∈ A ∩ S ∧ s ∈ 𝒟 (P a \ S)›
        apply (simp add: D_Hiding "*****"[simplified])
        using ****** by blast
      hence ‹s ∈ 𝒟 (⊓a ∈ A ∩ S. (P a \ S))› by (simp add: D_GlobalNdet) blast
      thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Sliding)
    next
      assume ‹f 0 ≠ []›
      with "**"(1)[THEN conjunct2, THEN conjunct1, rule_format, of 0]
      obtain a where *** : ‹a ∈ A› ‹f 0 ≠ []› ‹hd (f 0) = ev a›
        by (simp add: T_Mprefix) blast
      have **** : ‹f j ≠ [] ∧ hd (f j) = ev a› for j
      proof (induct j)
        from "***"(2, 3) show ‹f 0 ≠ [] ∧ hd (f 0) = ev a› by blast
      next
        case (Suc j)
        have ‹j < Suc j› by simp
        from "**"(1)[THEN conjunct1, THEN strict_monoD, OF this]
        obtain v where ‹f (Suc j) = f j @ v›
          by (metis le_list_def order_less_imp_le)
        thus ?case by (simp add: Suc.hyps(1))
      qed
      show ‹s ∈ 𝒟 ?rhs›
      proof (cases ‹a ∈ S›)
        assume ‹a ∈ S›
        hence ‹a ∈ A ∩ S› by (simp add: "***"(1))
        have ‹tickFree (tl t) ∧ s = trace_hide (tl t) (ev ` S) @ u ∧
              isInfHiddenRun (λi. tl (f i)) (P a) S ∧ tl t ∈ range (λi. tl (f i))›
          apply (simp add: "*"(3), intro conjI)
          subgoal by (metis "*"(2) list.sel(2) tickFree_tl)
          subgoal by (cases t; simp; metis "****" ‹a ∈ S› ‹t = f k› image_iff list.sel(1))
          subgoal by (meson "**"(1) "****" less_tail strict_mono_Suc_iff)
          subgoal using "**"(1) by (simp add: T_Mprefix "****")
          subgoal by (metis (no_types, lifting) "**"(1) "****" filter.simps(2) list.exhaust_sel list.sel(3))
          using "**"(2) by blast
        have ‹s ∈ 𝒟 (⊓a ∈ A ∩ S. (P a \ S))›
          apply (simp add: D_GlobalNdet D_Hiding)
          using "*"(1) ‹a ∈ A ∩ S› ‹?this› by blast
        thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Sliding)
      next
        assume ‹a ∉ S›
        have ‹tickFree (tl t) ∧ 
              trace_hide (tl t) (ev ` S) @ u = trace_hide (tl t) (ev ` S) @ u ∧
              isInfHiddenRun (λi. tl (f i)) (P a) S ∧ tl t ∈ range (λi. tl (f i))›
          apply (simp add: "*"(3), intro conjI)
          subgoal by (metis "*"(2) list.sel(2) tickFree_tl)
          subgoal by (meson "**"(1) "****" less_tail strict_mono_Suc_iff)
          subgoal using "**"(1) by (simp add: T_Mprefix "****")
          subgoal by (metis (no_types, lifting) "**"(1) "****" filter.simps(2) list.exhaust_sel list.sel(3))
          using "**"(2) by blast
        from ‹a ∉ S› have ‹s ∈ 𝒟 (□a∈A - S → (P a \ S))›
          apply (simp add: D_Mprefix "*"(3) ‹t = f k›)
          using "***"(1) "****"[of k]
          apply (cases ‹f k›; simp add: ‹a ∉ S› image_iff[of ‹ev a›] D_Hiding)
          using ‹?this› by (metis "*"(1) ‹t = f k› list.sel(3))
        thus ‹s ∈ 𝒟 ?rhs› by (simp add: D_Sliding)
        qed
      qed
    qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then consider ‹s ∈ 𝒟 (□a ∈ A - S → (P a \ S))› 
    | ‹s ∈ 𝒟 (⊓a ∈ A ∩ S. (P a \ S))› by (simp add: D_Sliding) blast
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    show ‹s ∈ 𝒟 (□a ∈ A - S → (P a \ S)) ⟹ s ∈ 𝒟 ?lhs›
      by (rule D_Hiding_Mprefix_dir2)
  next
    assume ‹s ∈ 𝒟 (⊓a ∈ A ∩ S. (P a \ S))›
    then obtain a where * : ‹a ∈ A› ‹a ∈ S› ‹s ∈ 𝒟 (P a \ S)›
      by (simp add: D_GlobalNdet)
         (metis (no_types, lifting) IntD1 IntD2 UN_iff empty_iff)
    from "*"(3) obtain t u 
       where ** : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` S) @ u›
                 ‹t ∈ 𝒟 (P a) ∨ (∃ f. isInfHiddenRun f (P a) S ∧ t ∈ range f)›
      by (simp add: D_Hiding) blast
    from "**"(4) show ‹s ∈ 𝒟 ?lhs›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (P a)›
      hence $ : ‹tickFree (ev a # t) ∧ ev a # t ∈ 𝒟 (Mprefix A P) ∧
                 s = trace_hide (ev a # t) (ev ` S) @ u›
        by (simp add: "*"(1, 2) "**"(2, 3) D_Mprefix)
      show ‹s ∈ 𝒟 ?lhs›
        apply (simp add: D_Hiding)
        using "$" "**"(1) by blast
    next
      assume ‹∃f. isInfHiddenRun f (P a) S ∧ t ∈ range f›
      then obtain f where ‹isInfHiddenRun f (P a) S› ‹t ∈ range f› by blast
      hence $ : ‹tickFree (ev a # t) ∧ 
                 s = trace_hide (ev a # t) (ev ` S) @ u ∧
                 isInfHiddenRun (λi. ev a # f i) (Mprefix A P) S ∧ 
                 ev a # t ∈ range (λi. ev a # f i)›
        by (auto simp add: "*"(1, 2) "**"(2, 3) less_cons monotone_on_def T_Mprefix)
      show ‹s ∈ 𝒟 ?lhs›
        apply (simp add: D_Hiding)
        using "$" "**"(1) by blast
    qed
  qed
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)›
    by (simp add: F_Hiding D_Hiding) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from D_F same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› 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) consider ‹t = []› ‹(X ∪ ev ` S) ∩ ev ` A = {}›
      | ‹∃a t'. a ∈ A ∧ t = ev a # t' ∧ (t', X ∪ ev ` S) ∈ ℱ (P a)›
      by (simp add: F_Mprefix) (metis event.inject image_iff list.collapse)
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      show ‹t = [] ⟹ (X ∪ ev ` S) ∩ ev ` A = {} ⟹ (s, X) ∈ ℱ ?rhs›
        using "*"(1) by (auto simp add: F_Sliding F_GlobalNdet)
    next
      assume ‹∃a t'. a ∈ A ∧ t = ev a # t' ∧ (t', X ∪ ev ` S) ∈ ℱ (P a)›
      then obtain a t' where ** : ‹a ∈ A› ‹t = ev a # t'›
                                  ‹(t', X ∪ ev ` S) ∈ ℱ (P a)› by blast
      show ‹(s, X) ∈ ℱ ?rhs›
      proof (cases ‹a ∈ S›)
        show ‹a ∈ S ⟹ (s, X) ∈ ℱ ?rhs›
          using "*"(1) "**" by (auto simp add: F_Sliding F_GlobalNdet F_Hiding)
      next
        show ‹a ∉ S ⟹ (s, X) ∈ ℱ ?rhs›
          using "*"(1) "**"(1, 2, 3) by (auto simp add: F_Sliding F_Mprefix F_Hiding)
      qed
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹(s, X) ∈ ℱ (⊓a ∈ A ∩ S. (P a \ S))›
    | ‹s ≠ []› ‹(s, X) ∈ ℱ (□a ∈ A - S → (P a \ S))›
    by (auto simp add: F_Sliding)
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    assume ‹(s, X) ∈ ℱ (⊓a ∈ A ∩ S. (P a \ S))›
    then obtain a where * : ‹a ∈ A› ‹a ∈ S› ‹(s, X) ∈ ℱ (P a \ S)›
      by (simp add: F_GlobalNdet non_disjoint) blast
    from "*"(3) consider ‹s ∈ 𝒟 (P a \ S)›
      | ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (P a)›
      by (simp add: F_Hiding D_Hiding) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹s ∈ 𝒟 (P a \ S)›
      then obtain t u
        where ** : ‹front_tickFree u› ‹tickFree t› 
                   ‹s = trace_hide t (ev ` S) @ u› 
                   ‹t ∈ 𝒟 (P a) ∨ (∃ f. isInfHiddenRun f (P a) S ∧ t ∈ range f)›
        by (simp add: D_Hiding) blast
      from "**"(4) show ‹(s, X) ∈ ℱ ?lhs›
      proof (elim disjE)
        assume ‹t ∈ 𝒟 (P a)›
        hence $ : ‹tickFree (ev a # t) ∧ s = trace_hide (ev a # t) (ev ` S) @ u ∧ 
                   ev a # t ∈ 𝒟 (Mprefix A P)›
          by (simp add: D_Mprefix "*"(1, 2) "**"(2, 3) image_iff[of ‹ev a›])
        show ‹(s, X) ∈ ℱ ?lhs›
          apply (simp add: F_Hiding)
          using "$" "**"(1) by blast
      next
        assume ‹∃f. isInfHiddenRun f (P a) S ∧ t ∈ range f›
        then obtain f where ‹isInfHiddenRun f (P a) S› ‹t ∈ range f› by blast
        hence $ : ‹tickFree (ev a # t) ∧ s = trace_hide (ev a # t) (ev ` S) @ u ∧
                   isInfHiddenRun (λi. ev a # f i) (Mprefix A P) S ∧ 
                   ev a # t ∈ range (λi. ev a # f i)›
          by (simp add: T_Mprefix "*"(1, 2) "**"(2, 3) 
                        image_iff[of ‹ev a›] less_cons monotone_on_def) blast
        show ‹(s, X) ∈ ℱ ?lhs›
          apply (simp add: F_Hiding)
          using "$" "**"(1) by blast
      qed
    next
      assume ‹∃t. s = trace_hide t (ev ` S) ∧ (t, X ∪ ev ` S) ∈ ℱ (P a)›
      then obtain t where ‹s = trace_hide t (ev ` S)›
                          ‹(t, X ∪ ev ` S) ∈ ℱ (P a)› by blast
      hence ‹s = trace_hide (ev a # t) (ev ` S) ∧ 
             (ev a # t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
        by (simp add: "*"(1, 2) F_Mprefix)
      show ‹(s, X) ∈ ℱ ?lhs›
        apply (simp add: F_Hiding, rule disjI1)
        using ‹?this› by blast
    qed
  next
    show ‹s ≠ [] ⟹ (s, X) ∈ ℱ (□a∈A - S → (P a \ S)) ⟹ (s, X) ∈ ℱ ?lhs›
      by (rule F_Hiding_Mprefix_dir2)
  qed
qed

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


text ‹And we obtain a similar result when adding a \<^const>‹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_Ndet(2),
       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_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_distr)
  have ‹Mprefix B Q ⊓ (Mprefix A P □ Mprefix B Q) ⊳ R = Mprefix A P □ Mprefix B Q ⊳ R›
    by (metis Det_STOP Ndet_commute Ndet_distrib Sliding_STOP_Det Sliding_assoc Sliding_def) 
  thus ‹?term ⊓ Mprefix B Q ⊳ R = ?term ⊳ R›
    by (simp add: Mprefix_Det_distr 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 (auto simp add: D_Sliding D_Seq T_Sliding)
  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
      apply (simp add: F_Seq, elim disjE exE)
        apply (solves ‹auto simp add: F_Sliding F_Seq D_Mprefix›)
       apply (solves ‹auto simp add: F_Sliding T_Sliding F_Seq›)
      by (solves ‹auto simp add: D_Sliding D_Seq F_Sliding F_Seq›)
  next
    show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
      apply (simp add: F_Sliding, elim disjE)
        apply (solves ‹auto simp add: F_Seq D_Sliding F_Sliding T_Sliding›)
       apply (solves ‹auto simp add: F_Seq D_Sliding F_Sliding T_Sliding›)
      by (simp add: D_Seq D_Mprefix T_Seq T_Mprefix)
         (metis append_is_Nil_conv event.simps(3) hd_append list.sel(1))
  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. s = t1 @ t2 ∧ t1 ∈ 𝒟 (Mprefix A P ⊳ P') ∧
                         tickFree t1 ∧ set t1 ∩ ev ` B = {} ∧ front_tickFree t2›
    | ‹∃t1 b t2. 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
    assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒟 (Mprefix A P ⊳ P') ∧
                    tickFree t1 ∧ set t1 ∩ ev ` B = {} ∧ front_tickFree t2›
    then obtain t1 t2
      where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (Mprefix A P ⊳ P')› ‹tickFree t1›
                ‹set t1 ∩ ev ` B = {}› ‹front_tickFree t2› by blast
    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 (simp add: D_Mprefix image_iff)
           (metis event.inject list.collapse)
      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
    assume ‹∃t1 b t2. s = t1 @ ev b # t2 ∧ t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P') ∧
                      set t1 ∩ ev ` B = {} ∧ b ∈ B ∧ t2 ∈ 𝒟 (Q b)›
    then obtain 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 blast
    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 (simp add: T_Mprefix)
           (metis list.exhaust_sel snoc_eq_iff_butlast)
      with "*"(1, 3, 4, 5) show ‹s ∈ 𝒟 ?rhs›
        by (cases t1; simp add: "*"(1) D_Sliding D_Mprefix D_Throw)
           (metis image_eqI)
    next
      from "*"(1, 3, 4, 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 list.sel(1, 3) self_append_conv2)
    next
      assume ‹a ∉ B›
      with "*"(3) consider 
        ‹∃t1 t2. s' = t1 @ t2 ∧ t1 ∈ 𝒟 (P a) ∧ tickFree t1 ∧
                 set t1 ∩ ev ` B = {} ∧ front_tickFree t2›
        | ‹∃t1 b t2. 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
        assume ‹∃t1 t2. s' = t1 @ t2 ∧ t1 ∈ 𝒟 (P a) ∧ tickFree t1 ∧
                        set t1 ∩ ev ` B = {} ∧ front_tickFree t2›
        then obtain t1 t2
          where ** : ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tickFree t1›
                     ‹set t1 ∩ ev ` B = {}› ‹front_tickFree t2›
          by blast
        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.distinct(1) list.discI list.sel(1, 3) tickFree_Cons)
      next
        assume ‹∃t1 b t2. s' = t1 @ ev b # t2 ∧ t1 @ [ev b] ∈ 𝒯 (P a) ∧
                          set t1 ∩ ev ` B = {} ∧ b ∈ B ∧ t2 ∈ 𝒟 (Q b)›
        then obtain t1 b t2
          where ** : ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
                     ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)› by blast
        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 list.sel(1, 3))
      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. s = t1 @ ev b # t2 ∧ t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P') ∧
                 set t1 ∩ ev ` B = {} ∧ b ∈ B ∧ (t2, X) ∈ ℱ (Q b)›
    by (simp add: F_Throw D_Throw) blast
  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
    assume ‹∃t1 b t2. s = t1 @ ev b # t2 ∧ t1 @ [ev b] ∈ 𝒯 (Mprefix A P ⊳ P') ∧
                      set t1 ∩ ev ` B = {} ∧ b ∈ B ∧ (t2, X) ∈ ℱ (Q b)›
    then obtain 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 blast
    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 (simp add: T_Mprefix)
           (metis list.exhaust_sel snoc_eq_iff_butlast)
      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 (simp add: F_Mprefix image_iff) (metis event.inject list.collapse)
    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) Nil_elem_T)
        
      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. s' = t1 @ ev b # t2 ∧ t1 @ [ev b] ∈ 𝒯 (P a) ∧ 
                     set t1 ∩ ev ` B = {} ∧ b ∈ B ∧ (t2, X) ∈ ℱ (Q b)›
        by (simp add: F_Throw D_Throw) blast
      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
        assume ‹∃t1 b t2. s' = t1 @ ev b # t2 ∧ t1 @ [ev b] ∈ 𝒯 (P a) ∧ 
                          set t1 ∩ ev ` B = {} ∧ b ∈ B ∧ (t2, X) ∈ ℱ (Q b)›
        then obtain 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 blast
        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



end