Theory CSP_PTick_Laws

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Other Laws›


(*<*)
theory CSP_PTick_Laws
  imports Multi_Sequential_Composition_Generalized
    Multi_Synchronization_Product_Generalized
    "HOL-CSP_RS" Step_CSP_PTick_Laws_Extended CSP_PTick_Monotonicities
begin
  (*>*)


declare [[metis_instantiate]]


section ‹Laws of Renaming›

subsection ‹Renaming and Sequential Composition›

lemma FD_Renaming_Seqptick :
  ‹Renaming P f g ;✓ (λg_r. ⊓r ∈ {r ∈ ✓s(P). g_r = g r}. Renaming (Q r) f g')
   ⊑FD Renaming (P ;✓ Q) f g'› (is ‹?lhs ⊑FD ?rhs›)
proof (rule failure_divergence_refine_optimizedI)
  fix s assume ‹s ∈ 𝒟 ?rhs›
  then obtain s1 s2 where * : ‹s = map (map_eventptick f g') s1 @ s2› ‹tF s1›
    ‹ftF s2› ‹s1 ∈ 𝒟 (P ;✓ Q)›
    unfolding D_Renaming by blast
  from "*"(4) consider (D_P) t1 t2 where ‹s1 = map (ev ∘ of_ev) t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹ftF t2›
    | (D_Q) t1 r t2 where ‹s1 = map (ev ∘ of_ev) t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t1 ∉ 𝒟 P› ‹tF t1› ‹t2 ∈ 𝒟 (Q r)›
    by (simp add: Seqptick_projs) (metis D_imp_front_tickFree)
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    case D_P
    from D_P(2, 3) have ‹map (map_eventptick f g) t1 ∈ 𝒟 (Renaming P f g)›
      by (auto simp add: D_Renaming intro: front_tickFree_Nil)
    hence ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) ∈ 𝒟 ?lhs›
      unfolding Seqptick_projs
      by (metis (mono_tags, lifting) front_tickFree_Nil D_P(3)
          map_eventptick_tickFree append.right_neutral mem_Collect_eq Un_iff)
    also have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) =
               map (map_eventptick f g') (map (ev ∘ of_ev) t1)›
      by (simp add: ‹tF t1› tickFree_map_map_eventptick_is)
    finally show ‹s ∈ 𝒟 ?lhs›
      by (auto simp add: "*"(1) D_P(1) intro!: is_processT7)
        (metis list.map_comp map_eventptick_tickFree tickFree_map_ev_comp,
          use "*"(2, 3) D_P(1) front_tickFree_append map_eventptick_tickFree tickFree_append_iff in blast)
  next
    case D_Q
    from "*"(2) D_Q(1, 5) have ‹map (map_eventptick f g') t2 ∈ 𝒟 (Renaming (Q r) f g')›
      by (auto simp add: D_Renaming intro: front_tickFree_Nil)
    hence ‹map (map_eventptick f g') t2 ∈ 𝒟 (⊓r' ∈ {r' ∈ ✓s(P). g r = g r'}. Renaming (Q r') f g')›
      by (simp add: D_GlobalNdet)
        (metis D_Q(2, 3) is_processT9 strict_ticks_of_memI)
    moreover from D_Q(2) have ‹map (map_eventptick f g) t1 @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
      by (auto simp add: T_Renaming)
    moreover have ‹tF (map (map_eventptick f g) t1)›
      by (simp add: D_Q(4) map_eventptick_tickFree)
    ultimately have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                     map (map_eventptick f g') t2 ∈ 𝒟 ?lhs›
      unfolding Seqptick_projs by blast
    with "*"(2, 3) have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                         map (map_eventptick f g') t2 @ s2 ∈ 𝒟 ?lhs›
      by (auto simp add: D_Q(1) comp_assoc map_eventptick_tickFree
          intro!: is_processT7[of ‹_ @ _›, simplified])
    also from D_Q(4) have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                           map (map_eventptick f g') t2 @ s2 = s›
      by (simp add: "*"(1) D_Q(1))
        (metis eventptick.map_sel(1) in_set_conv_decomp tickFree_Cons_iff tickFree_append_iff)
    finally show ‹s ∈ 𝒟 ?lhs› .
  qed
next
  assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
  fix s X assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s ∈ 𝒟 ?rhs›
    | (fail) s1 where ‹s = map (map_eventptick f g') s1›
      ‹(s1, map_eventptick f g' -` X) ∈ ℱ (P ;✓ Q)› ‹s1 ∉ 𝒟 (P ;✓ Q)›
    by (simp add: Renaming_projs)
      (metis (no_types, opaque_lifting) front_tickFree_Nil front_tickFree_iff_tickFree_butlast
        front_tickFree_Cons_iff[of ‹last s› ‹[]›] map_butlast[of ‹map_eventptick f g'›]
        map_is_Nil_conv[of ‹map_eventptick f g'› ‹[]›] map_is_Nil_conv[of ‹map_eventptick f g'›]
        append_self_conv[of ‹map (map_eventptick f g') _› ‹[]›] F_imp_front_tickFree
        snoc_eq_iff_butlast[of ‹butlast s› ‹last s› s]
        div_butlast_when_non_tickFree_iff non_tickFree_imp_not_Nil)
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    from subset_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
  next
    case fail
    from fail(2, 3)
    consider (F_P) t1 where ‹s1 = map (ev ∘ of_ev) t1› ‹(t1, ref_Seqptick (map_eventptick f g' -` X)) ∈ ℱ P› ‹tF t1›
      | (F_Q) t1 r t2 where ‹s1 = map (ev ∘ of_ev) t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹tF t1› ‹t1 ∉ 𝒟 P› ‹(t2, map_eventptick f g' -` X) ∈ ℱ (Q r)›
      by (simp add: Seqptick_projs) (metis F_imp_front_tickFree)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      case F_P
      have ‹map_eventptick f g -` (ref_Seqptick X) = ref_Seqptick (map_eventptick f g' -` X)› for X
      proof (rule set_eqI)
        show ‹e ∈ map_eventptick f g -` (ref_Seqptick X) ⟷
                  e ∈ ref_Seqptick (map_eventptick f g' -` X)› for e
          by (cases e, auto simp add: ref_Seqptick_def image_iff)
            (metis Int_iff eventptick.sel(1) eventptick.simps(9) rangeI vimage_eq,
              metis IntI UNIV_I eventptick.sel(1) image_eqI)
      qed
      with F_P(2) have ‹(map (map_eventptick f g) t1, ref_Seqptick X) ∈ ℱ (Renaming P f g)›
        by (auto simp add: F_Renaming)
      with F_P(3) have ‹(map (ev ∘ of_ev) (map (map_eventptick f g) t1), X) ∈ ℱ ?lhs›
        by (fastforce simp add: Seqptick_projs map_eventptick_tickFree)
      also have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) = s›
        by (simp add: fail(1) F_P(1))
          (metis F_P(3) eventptick.map_sel(1) in_set_conv_decomp tickFree_Cons_iff tickFree_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    next
      case F_Q
      with F_Q(4) have ‹(map (map_eventptick f g') t2, X) ∈ ℱ (Renaming (Q r) f g')›
        by (auto simp add: F_Renaming)
      hence ‹(map (map_eventptick f g') t2, X) ∈
             ℱ (⊓r' ∈ {r' ∈ ✓s(P). g r = g r'}. Renaming (Q r') f g')›
        by (simp add: F_GlobalNdet)
          (metis F_Q(2, 4) is_processT9 strict_ticks_of_memI)
      moreover from F_Q(2) have ‹map (map_eventptick f g) t1 @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
        by (auto simp add: T_Renaming)
      moreover have ‹tF (map (map_eventptick f g) t1)›
        by (simp add: F_Q(3) map_eventptick_tickFree)
      ultimately have ‹(map (ev ∘ of_ev) (map (map_eventptick f g) t1) @
                        map (map_eventptick f g') t2, X) ∈ ℱ ?lhs›
        unfolding Seqptick_projs by fast
      also have ‹map (ev ∘ of_ev) (map (map_eventptick f g) t1) @ map (map_eventptick f g') t2 = s›
        by (simp add: fail(1) F_Q(1))
          (metis F_Q(3) eventptick.map_sel(1) in_set_conv_decomp
            tickFree_Cons_iff tickFree_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    qed
  qed
qed



lemma inj_on_Renaming_Seqptick :
  ‹Renaming (P ;✓ Q) f g' =
   Renaming P f g ;✓ (λg_r. Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
  (is ‹?lhs = ?rhs›) if ‹inj_on g ✓s(P)›
  ―‹This assumption is necessary, otherwise we cannot know which tick triggered term‹Q›.›
proof (rule FD_antisym)
  show ‹?lhs ⊑FD ?rhs›
  proof (rule failure_divergence_refine_optimizedI)
    fix s assume ‹s ∈ 𝒟 ?rhs›
    then consider (D_P) s1 s2 where ‹s = map (ev ∘ of_ev) s1 @ s2› ‹s1 ∈ 𝒟 (Renaming P f g)› ‹tF s1› ‹ftF s2›
      | (D_Q) s1 g_r s2 where ‹s = map (ev ∘ of_ev) s1 @ s2› ‹s1 @ [✓(g_r)] ∈ 𝒯 (Renaming P f g)›
        ‹s1 ∉ 𝒟 (Renaming P f g)› ‹tF s1› ‹s2 ∈ 𝒟 (Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
      by (simp add: Seqptick_projs) (use D_imp_front_tickFree in blast)
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      case D_P
      from D_P(2) obtain t1 t2
        where * : ‹s1 = map (map_eventptick f g) t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 P›
        unfolding D_Renaming by blast
      from "*"(2, 4) have ‹map (ev ∘ of_ev) t1 ∈ 𝒟 (P ;✓ Q)›
        by (auto simp add: Seqptick_projs intro: front_tickFree_Nil)
      hence ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1) ∈ 𝒟 ?lhs›
        unfolding D_Renaming mem_Collect_eq
        by (metis (mono_tags, lifting) front_tickFree_Nil tickFree_map_ev_comp append.right_neutral)
      also have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1) =
                 map (ev ∘ of_ev) (map (map_eventptick f g) t1)›
        by simp (metis "*"(2) eventptick.map_sel(1) in_set_conv_decomp tickFree_Cons_iff tickFree_append_iff)
      finally show ‹s ∈ 𝒟 ?lhs›
        by (auto simp add: D_P(1, 4) "*"(1) front_tickFree_append comp_assoc intro!: is_processT7)
    next
      case D_Q
      have ‹s1 @ [✓(g_r)] ∉ 𝒟 (Renaming P f g)› by (meson D_Q(3) is_processT9)
      with D_Q(2-4) obtain t1 r
        where * : ‹g_r = g r› ‹r ∈ ✓s(P)› ‹s1 = map (map_eventptick f g) t1› ‹t1 @ [✓(r)] ∈ 𝒯 P›
        by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_eventptick_iff)
          (metis append_Nil2 front_tickFree_Nil is_processT9 map_eventptick_tickFree strict_ticks_of_memI)
      from "*"(1, 2) ‹inj_on g ✓s(P)› have ‹(THE r. r ∈ ✓s(P) ∧ g_r = g r) = r›
        by (auto dest: inj_onD)
      with D_Q(5) have ‹s2 ∈ 𝒟 (Renaming (Q r) f g')› by simp
      then obtain t2 t3
        where ** : ‹s2 = map (map_eventptick f g') t2 @ t3› ‹tF t2› ‹ftF t3› ‹t2 ∈ 𝒟 (Q r)›
        unfolding D_Renaming by blast
      from "*"(4) "**"(4) have ‹map (ev ∘ of_ev) t1 @ t2 ∈ 𝒟 (P ;✓ Q)›
        by (simp add: Seqptick_projs) (metis append_T_imp_tickFree not_Cons_self)
      with "**"(2) have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2) ∈ 𝒟 ?lhs›
        unfolding D_Renaming mem_Collect_eq
        by (metis append.right_neutral front_tickFree_Nil tickFree_append_iff tickFree_map_ev_comp)
      moreover have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2) @ t3 = s›
        by (simp add: D_Q(1) "*"(3) "**"(1))
          (metis "*"(3) D_Q(4) eventptick.map_sel(1) in_set_conv_decomp
            map_eventptick_tickFree tickFree_Cons_iff tickFree_append_iff)
      ultimately show ‹s ∈ 𝒟 ?lhs›
        by (auto simp add: "**"(3) intro!: is_processT7[of ‹_ @ _›, simplified])
          (use "**"(1) D_Q(1) in force, use "**"(2) map_eventptick_tickFree in blast)
    qed
  next
    assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
    fix s X assume ‹(s, X) ∈ ℱ ?rhs›
    then consider ‹s ∈ 𝒟 ?rhs›
      | (F_P) s1 where ‹s = map (ev ∘ of_ev) s1› ‹(s1, ref_Seqptick X) ∈ ℱ (Renaming P f g)› ‹s1 ∉ 𝒟 (Renaming P f g)› ‹tF s1›
      | (F_Q) s1 g_r s2 where ‹s = map (ev ∘ of_ev) s1 @ s2› ‹s1 @ [✓(g_r)] ∈ 𝒯 (Renaming P f g)›
        ‹s1 ∉ 𝒟 (Renaming P f g)› ‹tF s1› ‹(s2, X) ∈ ℱ (Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
        ‹s2 ∉ 𝒟 (Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g')›
      by (simp add: Seqptick_projs)
        (metis (no_types, lifting) F_imp_front_tickFree front_tickFree_charn self_append_conv)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      from subset_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
    next
      case F_P
      from F_P(2, 3) obtain t1
        where * : ‹s1 = map (map_eventptick f g) t1› ‹(t1, map_eventptick f g -` ref_Seqptick X) ∈ ℱ P›
        unfolding Renaming_projs by blast
      have ‹map_eventptick f g -` (ref_Seqptick X) = ref_Seqptick (map_eventptick f g' -` X)› for X
      proof (rule set_eqI)
        show ‹e ∈ map_eventptick f g -` (ref_Seqptick X) ⟷
              e ∈ ref_Seqptick (map_eventptick f g' -` X)› for e
          by (cases e, auto simp add: ref_Seqptick_def image_iff)
            (metis Int_iff eventptick.sel(1) eventptick.simps(9) rangeI vimage_eq,
              metis IntI UNIV_I eventptick.sel(1) image_eqI)
      qed
      with "*"(2) have ‹(t1, ref_Seqptick (map_eventptick f g' -` X)) ∈ ℱ P› by simp
      hence ‹(map (ev ∘ of_ev) t1, map_eventptick f g' -` X) ∈ ℱ (P ;✓ Q)›
        by (simp add: Seqptick_projs)
          (metis "*"(1) F_P(4) map_eventptick_tickFree)
      hence ‹(map (map_eventptick f g') (map (ev ∘ of_ev) t1), X) ∈ ℱ ?lhs›
        unfolding F_Renaming by blast
      also have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1) = s›
        by (simp add: F_P(1) "*"(1))
          (metis "*"(1) F_P(4) eventptick.map_sel(1) in_set_conv_decomp
            map_eventptick_tickFree tickFree_Cons_iff tickFree_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    next
      case F_Q
      have ‹s1 @ [✓(g_r)] ∉ 𝒟 (Renaming P f g)› by (meson F_Q(3) is_processT9)
      with F_Q(2-4) obtain t1 r
        where * : ‹g_r = g r› ‹r ∈ ✓s(P)› ‹s1 = map (map_eventptick f g) t1› ‹t1 @ [✓(r)] ∈ 𝒯 P›
        by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_eventptick_iff)
          (metis append_Nil2 front_tickFree_Nil is_processT9 map_eventptick_tickFree strict_ticks_of_memI)
      from "*"(1, 2) ‹inj_on g ✓s(P)› have ‹(THE r. r ∈ ✓s(P) ∧ g_r = g r) = r›
        by (auto dest: inj_onD)
      with F_Q(5, 6) have ‹(s2, X) ∈ ℱ (Renaming (Q r) f g')›
        ‹s2 ∉ 𝒟 (Renaming (Q r) f g')› by simp_all
      then obtain t2 where ** : ‹s2 = map (map_eventptick f g') t2› ‹(t2, map_eventptick f g' -` X) ∈ ℱ (Q r)›
        unfolding Renaming_projs by blast
      from "*"(4) "**"(2) have ‹(map (ev ∘ of_ev) t1 @ t2, map_eventptick f g' -` X) ∈ ℱ (P ;✓ Q)›
        by (simp add: Seqptick_projs) (metis append_T_imp_tickFree not_Cons_self2)
      hence ‹(map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2), X) ∈ ℱ ?lhs›
        unfolding F_Renaming by blast
      also have ‹map (map_eventptick f g') (map (ev ∘ of_ev) t1 @ t2) = s›
        by (simp add: F_Q(1) "*"(3) "**"(1))
          (metis "*"(3) F_Q(4) eventptick.map_sel(1) in_set_conv_decomp
            map_eventptick_tickFree tickFree_Cons_iff tickFree_append_iff)
      finally show ‹(s, X) ∈ ℱ ?lhs› .
    qed
  qed
next

  have ‹?rhs = Renaming P f g ;✓ (λg_r. ⊓r ∈ {r ∈ ✓s(P). g_r = g r}. Renaming (Q r) f g')›
  proof (rule mono_Seqptick_eq)
    show ‹Renaming P f g = Renaming P f g› ..
  next
    fix g_r assume ‹g_r ∈ ✓s(Renaming P f g)›
    then obtain s s1 where ‹s @ [✓(g_r)] = map (map_eventptick f g) s1› ‹s1 ∈ 𝒯 P› ‹s1 ∉ 𝒟 P›
      by (simp add: strict_ticks_of_def Renaming_projs)
        (metis (no_types, opaque_lifting) T_imp_front_tickFree append_Nil2 butlast_snoc
          div_butlast_when_non_tickFree_iff front_tickFree_Nil
          front_tickFree_iff_tickFree_butlast front_tickFree_single map_butlast)
    from this(1) obtain s1' r where ‹g_r = g r› ‹s1 = s1' @ [✓(r)]›
      by (cases s1 rule: rev_cases) (auto simp add: tick_eq_map_eventptick_iff)
    with ‹s1 ∈ 𝒯 P› ‹s1 ∉ 𝒟 P› have ‹s1' @ [✓(r)] ∈ 𝒯 P› ‹s1' @ [✓(r)] ∉ 𝒟 P› by simp_all
    hence ‹r ∈ ✓s(P)› unfolding strict_ticks_of_def by blast
    have ‹{r ∈ ✓s(P). g_r = g r} = {r}›
      by (auto simp add: ‹r ∈ ✓s(P)› ‹g_r = g r› intro: inj_onD[OF ‹inj_on g ✓s(P)›])
    moreover have ‹(THE r. r ∈ ✓s(P) ∧ g_r = g r) = r›
      using calculation by blast
    ultimately have ‹Q (THE r. r ∈ ✓s(P) ∧ g_r = g r) =
                     GlobalNdet {r ∈ ✓s(P). g_r = g r} Q› by simp
    thus ‹Renaming (Q (THE r. r ∈ ✓s(P) ∧ g_r = g r)) f g' =
          (⊓r ∈ {r ∈ ✓s(P). g_r = g r}. Renaming (Q r) f g')›
      by (simp flip: Renaming_distrib_GlobalNdet)
  qed
  thus ‹?rhs ⊑FD ?lhs› by (simp add: FD_Renaming_Seqptick)
qed


text ‹When typ‹'r› is set on typ‹unit›, we recover the version that we had before the generalization.›
lemma ‹Renaming (P ;✓ Q) f g = Renaming P f g ;✓ (λr. Renaming (Q ()) f g)›
  by (subst inj_on_Renaming_Seqptick[where g = g]) (auto intro: inj_onI)


lemma TickSwap_Seqptick [simp] :
  ‹TickSwap (P ;✓ Q) = TickSwap P ;✓ (λ(s, r). TickSwap (Q (r, s)))› (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = Renaming (P ;✓ Q) id prod.swap› by (simp add: TickSwap_is_Renaming)
  also have ‹… = Renaming P id prod.swap ;✓
                  (λs_r. Renaming (Q (THE r_s. r_s ∈ strict_ticks_of P ∧
                                               s_r = prod.swap r_s)) id prod.swap)›
    (is ‹_ = _ ;✓ ?rhs'›) by (simp add: inj_on_Renaming_Seqptick)
  also have ‹… = ?rhs›
  proof (rule mono_Seqptick_eq, unfold TickSwap_is_Renaming)
    show ‹Renaming P id prod.swap = Renaming P id prod.swap› ..
  next
    fix s_r assume ‹s_r ∈ strict_ticks_of (Renaming P id prod.swap)›
    then obtain r s where ‹(r, s) ∈ strict_ticks_of P› ‹s_r = (s, r)›
      by (auto simp flip: TickSwap_is_Renaming)
    hence ‹(THE r_s. r_s ∈ strict_ticks_of P ∧ s_r = prod.swap r_s) = (r, s)› by auto
    thus ‹Renaming (Q (THE r_s. r_s ∈ strict_ticks_of P ∧ s_r = prod.swap r_s)) id prod.swap =
          (case s_r of (s, r) ⇒ Renaming (Q (r, s)) id prod.swap)›
      by (simp add: ‹s_r = (s, r)›)
  qed
  finally show ‹?lhs = ?rhs› .
qed

lemma TickSwap_is_Seqptick_iff [simp] :
  ‹TickSwap P = Q ;✓ R ⟷ P = TickSwap Q ;✓ (λ(r, s). TickSwap (R (s, r)))›
  by (simp add: TickSwap_eq_iff_eq_TickSwap)




subsection ‹Renaming and Synchronization Product›

theorem (in Syncptick_locale) inj_RenamingEv_Syncptick :
  ‹RenamingEv (P ⟦S⟧✓ Q) f = RenamingEv P f ⟦f ` S⟧✓ RenamingEv Q f›
  (is ‹?lhs = ?rhs›) if ‹inj f›
proof -
  let ?fun = ‹map_eventptick f id›
  let ?map = ‹map ?fun›
  let ?R   = ‹λP. RenamingEv P f›
  show ‹?lhs = ?rhs›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    then obtain t1 t2 where * : ‹t = ?map t1 @ t2›
      ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P ⟦S⟧✓ Q)› unfolding D_Renaming by blast
    from "*"(4) obtain u v t_P t_Q where ** : ‹t1 = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      unfolding D_Syncptick by blast
    from setinterleavesptick_inj_map_map_eventptick_iff_weak [THEN iffD2, OF ‹inj f› "**"(4)]
    have ‹?map u setinterleaves✓⇘(⊗✓)⇙ ((?map t_P, ?map t_Q), f ` S)› .
    moreover from "**"(5) have ‹?map t_P ∈ 𝒟 (?R P) ∧ ?map t_Q ∈ 𝒯 (?R Q) ∨
                              ?map t_P ∈ 𝒯 (?R P) ∧ ?map t_Q ∈ 𝒟 (?R Q)›
      by (auto simp add: Renaming_projs dest: D_T)
        (metis "**"(2,4) append_self_conv front_tickFree_map_tick_iff
          list.map_disc_iff tickFree_setinterleavesptick_iff)+
    moreover have ‹t = ?map u @ (?map v @ t2)› by (simp add: "*"(1) "**"(1))
    moreover have ‹tF (?map u)› by (simp add: "**"(2) map_eventptick_tickFree)
    moreover from "*"(2,3) "**"(1) have ‹ftF (?map v @ t2)›
      using front_tickFree_append map_eventptick_tickFree tickFree_append_iff by blast
    ultimately show ‹t ∈ 𝒟 ?rhs› unfolding D_Syncptick by blast
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain u v t_P t_Q where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), f ` S)›
      ‹t_P ∈ 𝒟 (?R P) ∧ t_Q ∈ 𝒯 (?R Q) ∨ t_P ∈ 𝒯 (?R P) ∧ t_Q ∈ 𝒟 (?R Q)›
      unfolding D_Syncptick by blast
    from "*"(5) show ‹t ∈ 𝒟 ?lhs›
    proof (elim disjE conjE)
      assume ‹t_P ∈ 𝒟 (?R P)› ‹t_Q ∈ 𝒯 (?R Q)›
      from ‹t_P ∈ 𝒟 (?R P)› obtain t_P1 t_P2
        where ** : ‹t_P = ?map t_P1 @ t_P2› ‹tF t_P1› ‹ftF t_P2› ‹t_P1 ∈ 𝒟 P›
        unfolding D_Renaming by blast
      from ‹t_Q ∈ 𝒯 (?R Q)› consider (T_Q) t_Q1 where ‹t_Q = ?map t_Q1› ‹t_Q1 ∈ 𝒯 Q›
        | (D_Q) t_Q1 t_Q2 where ‹t_Q = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹ftF t_Q2› ‹t_Q1 ∈ 𝒟 Q›
        unfolding T_Renaming by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case T_Q
        from "*"(4)[unfolded "**"(1) T_Q(1), THEN setinterleavesptick_appendL]
        obtain u1 u2 t_Q11 t_Q12 where *** : ‹u = u1 @ u2› ‹?map t_Q1 = t_Q11 @ t_Q12›
          ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?map t_P1, t_Q11), f ` S)› by blast
        obtain t_Q11' where ‹t_Q11' ≤ t_Q1› ‹t_Q11 = ?map t_Q11'› 
          by (metis "***"(2) map_eq_append_conv Prefix_Order.prefixI)
        from setinterleavesptick_inj_map_map_eventptick_iff_strong
          [THEN iffD1, OF ‹inj f› "***"(3)[unfolded this]]
        obtain u1' where **** : ‹u1 = ?map u1'›
          ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q11'), S)› by blast
        from "*"(2) "***"(1) "****"(1) map_eventptick_tickFree
          T_Q(2) ‹t_Q11' ≤ t_Q1› is_processT3_TR
        have ‹u1' = u1' @ []› ‹tF u1'› ‹ftF []› ‹t_Q11' ∈ 𝒯 Q› by simp_all blast
        with "****"(2) "**"(4) have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          unfolding D_Syncptick by blast
        moreover have ‹t = ?map u1' @ (u2 @ v)› by (simp add: "*"(1) "***"(1) "****"(1))
        moreover have ‹ftF (u2 @ v)›
          using "*"(2,3) "***"(1) front_tickFree_append tickFree_append_iff by blast
        ultimately show ‹t ∈ 𝒟 ?lhs› unfolding D_Renaming using ‹tF u1'› by blast
      next
        case D_Q
        have ‹?map t_P1 ≤ t_P› ‹?map t_Q1 ≤ t_Q›
          by (simp_all add: "**"(1) D_Q(1))
        from setinterleavesptick_le_prefixLR[OF "*"(4) this] show ‹t ∈ 𝒟 ?lhs›
        proof (elim disjE exE conjE)
          fix u1 t_Q1' assume *** : ‹u1 ≤ u› ‹t_Q1' ≤ ?map t_Q1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?map t_P1, t_Q1'), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_Q1'' where ‹t_Q1' = ?map t_Q1''› ‹t_Q1'' ≤ t_Q1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_Q1' = ?map t_Q1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from "**"(2) "****"(2) setinterleavesptick_tickFree_imp
          have ‹tF u1'› by blast
          moreover from D_Q(4) D_T ‹t_Q1'' ≤ t_Q1› is_processT3_TR
          have ‹t_Q1'' ∈ 𝒯 Q› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_P1 ∈ 𝒟 P› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› front_tickFree_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        next
          fix u1 t_P1' assume *** : ‹u1 ≤ u› ‹t_P1' ≤ ?map t_P1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P1', ?map t_Q1), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_P1'' where ‹t_P1' = ?map t_P1''› ‹t_P1'' ≤ t_P1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_P1' = ?map t_P1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1'', t_Q1), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from D_Q(2) "****"(2) setinterleavesptick_tickFree_imp
          have ‹tF u1'› by blast
          moreover from "**"(4) D_T ‹t_P1'' ≤ t_P1› is_processT3_TR
          have ‹t_P1'' ∈ 𝒯 P› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_Q1 ∈ 𝒟 Q› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› front_tickFree_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        qed
      qed
    next
      assume ‹t_Q ∈ 𝒟 (?R Q)› ‹t_P ∈ 𝒯 (?R P)›
      from ‹t_Q ∈ 𝒟 (?R Q)› obtain t_Q1 t_Q2
        where ** : ‹t_Q = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹ftF t_Q2› ‹t_Q1 ∈ 𝒟 Q›
        unfolding D_Renaming by blast
      from ‹t_P ∈ 𝒯 (?R P)› consider (T_P) t_P1 where ‹t_P = ?map t_P1› ‹t_P1 ∈ 𝒯 P›
        | (D_P) t_P1 t_P2 where ‹t_P = ?map t_P1 @ t_P2› ‹tF t_P1› ‹ftF t_P2› ‹t_P1 ∈ 𝒟 P›
        unfolding T_Renaming by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        case T_P
        from "*"(4)[unfolded "**"(1) T_P(1), THEN setinterleavesptick_appendR]
        obtain u1 u2 t_P11 t_P12 where *** : ‹u = u1 @ u2› ‹?map t_P1 = t_P11 @ t_P12›
          ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P11, ?map t_Q1), f ` S)› by blast
        obtain t_P11' where ‹t_P11' ≤ t_P1› ‹t_P11 = ?map t_P11'› 
          by (metis "***"(2) map_eq_append_conv Prefix_Order.prefixI)
        from setinterleavesptick_inj_map_map_eventptick_iff_strong
          [THEN iffD1, OF ‹inj f› "***"(3)[unfolded this]]
        obtain u1' where **** : ‹u1 = ?map u1'›
          ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P11', t_Q1), S)› by blast
        from "*"(2) "***"(1) "****"(1) map_eventptick_tickFree
          T_P(2) ‹t_P11' ≤ t_P1› is_processT3_TR
        have ‹u1' = u1' @ []› ‹tF u1'› ‹ftF []› ‹t_P11' ∈ 𝒯 P› by simp_all blast
        with "****"(2) "**"(4) have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          unfolding D_Syncptick by blast
        moreover have ‹t = ?map u1' @ (u2 @ v)› by (simp add: "*"(1) "***"(1) "****"(1))
        moreover have ‹ftF (u2 @ v)›
          using "*"(2,3) "***"(1) front_tickFree_append tickFree_append_iff by blast
        ultimately show ‹t ∈ 𝒟 ?lhs› unfolding D_Renaming using ‹tF u1'› by blast
      next
        case D_P
        have ‹?map t_P1 ≤ t_P› ‹?map t_Q1 ≤ t_Q›
          by (simp_all add: "**"(1) D_P(1))
        from setinterleavesptick_le_prefixLR[OF "*"(4) this] show ‹t ∈ 𝒟 ?lhs›
        proof (elim disjE exE conjE)
          fix u1 t_Q1' assume *** : ‹u1 ≤ u› ‹t_Q1' ≤ ?map t_Q1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?map t_P1, t_Q1'), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_Q1'' where ‹t_Q1' = ?map t_Q1''› ‹t_Q1'' ≤ t_Q1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_Q1' = ?map t_Q1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from D_P(2) "****"(2) setinterleavesptick_tickFree_imp
          have ‹tF u1'› by blast
          moreover from "**"(4) D_T ‹t_Q1'' ≤ t_Q1› is_processT3_TR
          have ‹t_Q1'' ∈ 𝒯 Q› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_P1 ∈ 𝒟 P› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› front_tickFree_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        next
          fix u1 t_P1' assume *** : ‹u1 ≤ u› ‹t_P1' ≤ ?map t_P1›
            ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P1', ?map t_Q1), f ` S)›
          obtain u2 where ‹u = u1 @ u2› using "***"(1) prefixE by blast
          obtain t_P1'' where ‹t_P1' = ?map t_P1''› ‹t_P1'' ≤ t_P1›
            by (metis "***"(2) prefixE prefixI map_eq_append_conv)
          from setinterleavesptick_inj_map_map_eventptick_iff_strong
            [THEN iffD1, OF ‹inj f› "***"(3)[unfolded ‹t_P1' = ?map t_P1''›]]
          obtain u1' where **** : ‹u1 = ?map u1'›
            ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1'', t_Q1), S)› by blast
          have ‹u1' = u1' @ []› ‹ftF []› by simp_all
          moreover from "**"(2) "****"(2) setinterleavesptick_tickFree_imp
          have ‹tF u1'› by blast
          moreover from D_P(4) D_T ‹t_P1'' ≤ t_P1› is_processT3_TR
          have ‹t_P1'' ∈ 𝒯 P› by blast
          ultimately have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)›
            unfolding D_Syncptick using ‹t_Q1 ∈ 𝒟 Q› "****"(2) by blast
          moreover from "*"(1-3) "****"(1)
          have ‹t = ?map u1' @ (u2 @ v)› ‹ftF (u2 @ v)›
            by (auto simp add: ‹u = u1 @ u2› front_tickFree_append)
          ultimately show ‹t ∈ 𝒟 ?lhs›
            unfolding D_Renaming using ‹tF u1'› by blast
        qed
      qed
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    then obtain t' where ‹t = ?map t'›
      and * : ‹(t', ?fun -` X) ∈ ℱ (P ⟦S⟧✓ Q)›
      unfolding Renaming_projs by blast
    have ‹t' ∉ 𝒟 (P ⟦S⟧✓ Q)›
    proof (rule notI)
      assume ‹t' ∈ 𝒟 (P ⟦S⟧✓ Q)›
      hence ‹t ∈ 𝒟 ?lhs›
        by (simp add: ‹t = ?map t'› D_Syncptick D_Renaming)
          (metis (no_types) append_Nil2 front_tickFree_Nil map_append map_eventptick_front_tickFree)
      with ‹t ∉ 𝒟 ?lhs› show False ..
    qed
    with "*" obtain t_P t_Q X_P X_Q
      where ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        ‹?fun -` X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
      unfolding Syncptick_projs by fast
    from "**"(2, 3) F_T ‹t' ∉ 𝒟 (P ⟦S⟧✓ Q)› append_Nil2 front_tickFree_Nil
    have ‹t_P ∉ 𝒟 P› unfolding D_Syncptick' by blast
    from "**"(1, 3) F_T ‹t' ∉ 𝒟 (P ⟦S⟧✓ Q)› append_Nil2 front_tickFree_Nil
    have ‹t_Q ∉ 𝒟 Q› unfolding D_Syncptick' by blast
    have *** : ‹?fun -` ?fun ` X_P = X_P› ‹?fun -` ?fun ` X_Q = X_Q›
      by (simp add: set_eq_iff image_iff,
          metis (mono_tags, opaque_lifting) eventptick.inj_map_strong id_apply injD ‹inj f›)+
    from "**"(1) have ‹(?map t_P, ?fun ` X_P) ∈ ℱ (?R P)›
      by (subst (asm) "***"(1)[symmetric]) (auto simp add: F_Renaming)
    moreover {
      fix a assume ‹?map t_P @ [ev a] ∈ 𝒯 (?R P)› ‹a ∉ range f›
      then consider t_P1 where ‹?map t_P @ [ev a] = ?map t_P1› ‹t_P1 ∈ 𝒯 P›
        | t_P1 t_P2 where ‹?map t_P @ [ev a] = ?map t_P1 @ t_P2› ‹tF t_P1› ‹t_P1 ∈ 𝒟 P›
        unfolding T_Renaming by blast
      hence False
      proof cases
        from ‹a ∉ range f› show ‹?map t_P @ [ev a] = ?map t_P1 ⟹ False› for t_P1
          by (auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
      next
        fix t_P1 t_P2 assume ‹?map t_P @ [ev a] = ?map t_P1 @ t_P2› ‹tF t_P1› ‹t_P1 ∈ 𝒟 P›
        from this(1) ‹a ∉ range f› have ‹t_P1 ≤ t_P›
          by (cases t_P2 rule: rev_cases, auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
            (metis prefixI eventptick.inj_map inj_map_eq_map inj_on_id map_eq_append_conv ‹inj f›)
        with ‹t_P1 ∈ 𝒟 P› have ‹t_P ∈ 𝒟 P›
          by (metis "**"(1) F_imp_front_tickFree prefixE ‹tF t_P1› front_tickFree_append_iff
              is_processT7 tickFree_Nil tickFree_imp_front_tickFree)
        with ‹t_P ∉ 𝒟 P› show False ..
      qed
    }
    ultimately have $ : ‹(?map t_P, ?fun ` X_P ∪ {ev a | a. a ∉ range f}) ∈ ℱ (?R P)›
      using is_processT5_S7' by blast
    from "**"(2) have ‹(?map t_Q, ?fun ` X_Q) ∈ ℱ (?R Q)›
      by (subst (asm) "***"(2)[symmetric]) (auto simp add: F_Renaming)
    moreover {
      fix a assume ‹?map t_Q @ [ev a] ∈ 𝒯 (?R Q)› ‹a ∉ range f›
      then consider t_Q1 where ‹?map t_Q @ [ev a] = ?map t_Q1› ‹t_Q1 ∈ 𝒯 Q›
        | t_Q1 t_Q2 where ‹?map t_Q @ [ev a] = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹t_Q1 ∈ 𝒟 Q›
        unfolding T_Renaming by blast
      hence False
      proof cases
        from ‹a ∉ range f› show ‹?map t_Q @ [ev a] = ?map t_Q1 ⟹ False› for t_Q1
          by (auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
      next
        fix t_Q1 t_Q2 assume ‹?map t_Q @ [ev a] = ?map t_Q1 @ t_Q2› ‹tF t_Q1› ‹t_Q1 ∈ 𝒟 Q›
        from this(1) ‹a ∉ range f› have ‹t_Q1 ≤ t_Q›
          by (cases t_Q2 rule: rev_cases, auto simp add: append_eq_map_conv ev_eq_map_eventptick_iff)
            (metis prefixI eventptick.inj_map inj_map_eq_map inj_on_id map_eq_append_conv ‹inj f›)
        with ‹t_Q1 ∈ 𝒟 Q› have ‹t_Q ∈ 𝒟 Q›
          by (metis "**"(2) F_imp_front_tickFree prefixE ‹tF t_Q1› front_tickFree_append_iff
              is_processT7 tickFree_Nil tickFree_imp_front_tickFree)
        with ‹t_Q ∉ 𝒟 Q› show False ..
      qed
    }
    ultimately have $$ : ‹(?map t_Q, ?fun ` X_Q ∪ {ev a | a. a ∉ range f}) ∈ ℱ (?R Q)›
      using is_processT5_S7' by blast
    from "**"(3) have $$$ : ‹t setinterleaves✓⇘(⊗✓)⇙ ((?map t_P, ?map t_Q), f ` S)›
      by (simp add: ‹t = ?map t'› setinterleavesptick_inj_map_map_eventptick_iff_weak ‹inj f›)
    have ‹e ∈ X ⟹ e ∈ super_ref_Syncptick (⊗✓) (?fun ` X_P ∪ {ev a | a. a ∉ range f}) (f ` S)
                         (?fun ` X_Q ∪ {ev a | a. a ∉ range f})› for e
      using "**"(4)[THEN set_mp, of ‹map_eventptick (inv f) id e›] ‹inj f›
      unfolding super_ref_Syncptick_def
      by (cases e, simp_all add: image_iff tick_eq_map_eventptick_iff) force
    hence $$$$ : ‹X ⊆ super_ref_Syncptick (⊗✓) (?fun ` X_P ∪ {ev a | a. a ∉ range f}) (f ` S)
                       (?fun ` X_Q ∪ {ev a | a. a ∉ range f})› by blast
    from "$" "$$" "$$$" "$$$$" show ‹(t, X) ∈ ℱ ?rhs› unfolding F_Syncptick by fast
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ (?R P)› ‹(t_Q, X_Q) ∈ ℱ (?R Q)›
        ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), f ` S)›
        ‹X ⊆ super_ref_Syncptick (⊗✓) X_P (f ` S) X_Q›
      unfolding Syncptick_projs by blast
    have ‹¬ (t_P ∈ 𝒟 (?R P) ∨ t_Q ∈ 𝒟 (?R Q))›
    proof (rule notI)
      assume ‹t_P ∈ 𝒟 (?R P) ∨ t_Q ∈ 𝒟 (?R Q)›
      hence ‹t ∈ 𝒟 ?rhs›
        by (simp add: D_Syncptick')
          (metis "*"(1-3) F_T append_Nil2 front_tickFree_Nil)
      with ‹t ∉ 𝒟 ?rhs› show False ..
    qed
    with "*"(1, 2) obtain t_P' t_Q'
      where ** : ‹t_P = ?map t_P'› ‹(t_P', ?fun -` X_P) ∈ ℱ P›
        ‹t_Q = ?map t_Q'› ‹(t_Q', ?fun -` X_Q) ∈ ℱ Q›
      unfolding Renaming_projs by blast
    from setinterleavesptick_inj_map_map_eventptick_iff_strong
      [THEN iffD1, OF ‹inj f› "*"(3)[unfolded "**"(1, 3)]] obtain t'
      where *** : ‹t = ?map t'› ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)› by blast
    have ‹e ∈ ?fun -` X ⟹ e ∈ super_ref_Syncptick (⊗✓) (?fun -` X_P) S (?fun -` X_Q)› for e
      using "*"(4)[THEN set_mp, of ‹?fun e›]
      by (cases e) (auto simp add: super_ref_Syncptick_def dest: injD[OF ‹inj f›])
    hence ‹?fun -` X ⊆ super_ref_Syncptick (⊗✓) (?fun -` X_P) S (?fun -` X_Q)› by blast
    with "**"(2, 4) "***"(2) have ‹(t', ?fun -` X) ∈ ℱ (P ⟦S⟧✓ Q)›
      unfolding F_Syncptick by auto
    thus ‹(t, X) ∈ ℱ ?lhs› by (auto simp add: "***"(1) F_Renaming)
  qed
qed




section ‹Laws of Hiding›

section ‹Hiding and Sequential Composition›

text ‹We start by giving a counter example when the assumption term‹𝔽✓(P)› is not satisfied.›

notepad begin
  define Q :: ‹nat ⇒ ('a, 'r) processptick›
    where ‹Q r ≡ (((→) undefined) ^^ r) STOP› for r
  have ‹SKIPS UNIV \ {undefined} = (SKIPS UNIV :: ('a, nat) processptick)›
    by (simp add: Hiding_SKIPS)
  moreover have ‹Q r \ {undefined} = STOP› for r
    by (induct r) (simp_all add: Q_def Hiding_write0_non_disjoint)
  ultimately have * : ‹(SKIPS UNIV \ {undefined}) ;✓ (λr. Q r \ {undefined}) = STOP›
    by (simp only: SKIPS_Seqptick) simp

  have ‹SKIPS UNIV ;✓ Q = ⊓r ∈ UNIV. Q r› by simp
  moreover have ‹[] ∈ 𝒟 (… \ {undefined})›
  proof (rule D_Hiding_seqRunI)
    show ‹ftF []› ‹tF []› ‹[] = trace_hide [] (ev ` {undefined}) @ []› by simp_all
  next
    { fix r
      have ‹replicate r (ev undefined) ∈ 𝒯 (Q r)›
        by (induct r) (simp_all add: Q_def T_write0)
      also have ‹replicate r (ev undefined) = map (λi. ev undefined) [0..<r]›
        by (simp add: map_replicate_trivial)
      finally have ‹map (λi. ev undefined) [0..<r] ∈ 𝒯 (Q r)› .
    }
    hence ‹∃r. map (λi. ev undefined) [0..<i] ∈ 𝒯 (Q r)› for i by blast
    thus ‹[] ∈ 𝒟 (⊓r ∈ UNIV. Q r) ∨ (∃x. isInfHidden_seqRun x (⊓r ∈ UNIV. Q r) {undefined} [])›
      by (auto simp add: T_GlobalNdet)
  qed
  ultimately have ** : ‹(SKIPS UNIV ;✓ Q) \ {undefined} = ⊥›
    by (simp add: BOT_iff_Nil_D)

  have ‹(SKIPS UNIV \ {undefined}) ;✓ (λr. Q r \ {undefined}) ≠ (SKIPS UNIV ;✓ Q) \ {undefined}›
    unfolding "*" "**" by simp

  hence ‹∃P (Q :: nat ⇒ ('a, 'r) processptick) S.
         (P \ S) ;✓ (λr. Q r \ S) ≠ (P ;✓ Q) \ S› by blast

end



text ‹In general, only one refinement is holding.›

theorem Hiding_Seq_FD_Seq_Hiding :
  ‹(P ;✓ Q) \ S ⊑FD (P \ S) ;✓ (λr. Q r \ S)› (is ‹?lhs ⊑FD ?rhs›)
proof (rule failure_divergence_refine_optimizedI)
  let ?th = ‹λt. trace_hide t (ev ` S)› and ?map = ‹λt. map (ev ∘ of_ev) t›
  fix t assume ‹t ∈ 𝒟 ?rhs›
  with D_imp_front_tickFree is_processT9
  consider (D_P) u v where ‹t = ?map u @ v› ‹u ∈ 𝒟 (P \ S)› ‹tF u› ‹ftF v›
    | (D_Q) u r v where ‹t = ?map u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P \ S)›
      ‹u @ [✓(r)] ∉ 𝒟 (P \ S)› ‹tF u› ‹v ∈ 𝒟 (Q r \ S)›
    by (fastforce simp add: Seqptick_projs)
  thus ‹t ∈ 𝒟 ?lhs›
  proof cases
    case D_P
    from D_P(2) obtain u' v' x where * : ‹u = ?th u' @ v'› ‹tF u'› ‹ftF v'›
      ‹u' ∈ 𝒟 P ∨ isInfHidden_seqRun x P S u'›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) have ‹?th (?map u') ∈ 𝒟 ?lhs›
    proof (elim disjE)
      assume ‹u' ∈ 𝒟 P›
      with "*"(2) have ‹?map u' ∈ 𝒟 (P ;✓ Q)›
        by (auto simp add: Seqptick_projs intro: front_tickFree_Nil)
      with mem_D_imp_mem_D_Hiding show ‹?th (?map u') ∈ 𝒟 ?lhs› .
    next
      assume ‹isInfHidden_seqRun x P S u'›
      from this isInfHidden_seqRun_imp_tickFree_seqRun[OF this]
      have ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ;✓ Q) S (?map u')›
        by (simp add: Seqptick_projs image_iff)
          (metis eventptick.sel(1) list.map_comp map_append seqRun_def)
      thus ‹?th (?map u') ∈ 𝒟 ?lhs›
        by (simp add: D_Hiding_seqRun)
          (metis (no_types) append.right_neutral comp_apply
            front_tickFree_Nil tickFree_map_ev_comp)
    qed
    also have ‹?th (?map u') = ?map (?th u')›
      by (fact tickFree_trace_hide_map_ev_comp_of_ev[OF ‹tF u'›])
    finally show ‹t ∈ 𝒟 ?lhs›
      by (simp add: D_P(1, 4) "*"(1) front_tickFree_append is_processT7)
  next
    case D_Q
    from D_Q(2, 3) obtain u' where ‹u @ [✓(r)] = ?th u'› ‹(u', ev ` S) ∈ ℱ P›
      unfolding T_Hiding D_Hiding by fast
    then obtain u' where ‹u = ?th u'› ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P›
      by (cases u' rule: rev_cases, simp_all split: if_split_asm)
        (metis F_imp_front_tickFree Hiding_tickFree butlast_snoc
          front_tickFree_iff_tickFree_butlast non_tickFree_tick tickFree_append_iff)
    from D_Q(5) obtain v' w' x where * : ‹v = ?th v' @ w'› ‹tF v'› ‹ftF w'›
      ‹v' ∈ 𝒟 (Q r) ∨ isInfHidden_seqRun x (Q r) S v'›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) have ‹?th (?map u' @ v') ∈ 𝒟 ?lhs›
    proof (elim disjE)
      assume ‹v' ∈ 𝒟 (Q r)›
      hence ‹?map u' @ v' ∈ 𝒟 (P ;✓ Q)›
        by (simp add: Seqptick_projs)
          (metis F_T ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P› append_T_imp_tickFree not_Cons_self)
      with mem_D_imp_mem_D_Hiding show ‹?th (?map u' @ v') ∈ 𝒟 ?lhs› .
    next
      assume ‹isInfHidden_seqRun x (Q r) S v'›
      hence ‹isInfHidden_seqRun x (P ;✓ Q) S (?map u' @ v')›
        by (simp add: seqRun_def image_iff Seqptick_projs)
          (metis F_T ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P› append_T_imp_tickFree list.discI)
      thus ‹?th (?map u' @ v') ∈ 𝒟 ?lhs›
        by (simp add: D_Hiding_seqRun)
          (metis append.right_neutral filter_append
            front_tickFree_Nil isInfHidden_seqRun_imp_tickFree)
    qed
    also have ‹?th (?map u' @ v') = ?map (?th u') @ ?th v'›
      using D_Q(4) Hiding_tickFree ‹u = ?th u'› tickFree_trace_hide_map_ev_comp_of_ev by auto
    finally have ‹?map (?th u') @ ?th v' ∈ 𝒟 ?lhs› .
    moreover have ‹tF (?map (?th u') @ ?th v')›
      by (simp add: "*"(2) Hiding_tickFree)
    ultimately show ‹t ∈ 𝒟 ?lhs›
      unfolding "*"(1) D_Q(1) ‹u = ?th u'› using ‹ftF w'›
      by (metis append.assoc is_processT7)
  qed
next

  assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
  let ?th = ‹λt. trace_hide t (ev ` S)› and ?map = ‹λt. map (ev ∘ of_ev) t›
  fix t X assume ‹(t, X) ∈ ℱ ?rhs›
  then consider (div) ‹t ∈ 𝒟 ?rhs›
    | (F_P) u where ‹t = ?map u› ‹(u, ref_Seqptick X) ∈ ℱ (P \ S)› ‹u ∉ 𝒟 (P \ S)› ‹tF u›
    | (F_Q) u r v where ‹t = ?map u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P \ S)› ‹u @ [✓(r)] ∉ 𝒟 (P \ S)›
      ‹tF u› ‹(v, X) ∈ ℱ (Q r \ S)› ‹v ∉ 𝒟 (Q r \ S)›
    by (simp add: Seqptick_projs)
      (metis F_T T_imp_front_tickFree front_tickFree_Nil is_processT9 self_append_conv)
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    case div with subset_div show ‹(t, X) ∈ ℱ ?lhs›
      by (simp add: in_mono is_processT8)
  next
    case F_P
    from F_P(2, 3) obtain u' where * : ‹u = ?th u'› ‹(u', ref_Seqptick X ∪ ev ` S) ∈ ℱ P›
      unfolding F_Hiding D_Hiding by fast
    have ‹tF u'› using "*"(1) F_P(4) Hiding_tickFree by blast
    have $ : ‹ref_Seqptick (X ∪ ev ` S) = ref_Seqptick X ∪ ev ` S›
      by (auto simp add: image_iff ref_Seqptick_def)
        (metis Int_iff Un_iff eventptick.sel(1) image_eqI rangeI)
    from ‹tF u'› "*"(2) have ‹(?map u', X ∪ ev ` S) ∈ ℱ (P ;✓ Q)›
      by (auto simp add: Seqptick_projs "$")
    thus ‹(t, X) ∈ ℱ ?lhs›
      by (simp add: F_Hiding)
        (metis "*"(1) F_P(1) ‹tF u'› tickFree_trace_hide_map_ev_comp_of_ev)
  next
    case F_Q
    from F_Q(2, 3) obtain u' where ‹u @ [✓(r)] = ?th u'› ‹(u', ev ` S) ∈ ℱ P›
      unfolding T_Hiding D_Hiding by fast
    then obtain u' where * : ‹u = ?th u'› ‹(u' @ [✓(r)], ev ` S) ∈ ℱ P›
      by (cases u' rule: rev_cases, simp_all split: if_split_asm)
        (metis F_imp_front_tickFree Hiding_tickFree butlast_snoc
          front_tickFree_iff_tickFree_butlast non_tickFree_tick tickFree_append_iff)
    from F_Q(5, 6) obtain v' where ** : ‹v = ?th v'› ‹(v', X ∪ ev ` S) ∈ ℱ (Q r)›
      unfolding F_Hiding D_Hiding by blast
    have ‹(?map u' @ v', X ∪ ev ` S) ∈ ℱ (P ;✓ Q)›
      by (simp add: Seqptick_projs)
        (metis "*"(2) "**"(2) F_T append_T_imp_tickFree list.distinct(1))
    with F_Q(4) show ‹(t, X) ∈ ℱ ?lhs›
      by (simp add: F_Hiding F_Q(1) "*"(1) "**"(1))
        (metis Hiding_tickFree filter_append tickFree_trace_hide_map_ev_comp_of_ev)
  qed
qed



section ‹Hiding and Synchronization Product›

lemma setinterleavesptick_imp_superset_ev :
  ‹t setinterleaves✓⇘tick_join⇙ ((u, v), A) ⟹
   {ev a |a. ev a ∈ set u} ∪ {ev a |a. ev a ∈ set v} ⊆ {ev a |a. ev a ∈ set t}›
proof (induct t arbitrary: u v)
  case Nil thus ?case by (auto dest: Nil_setinterleavesptick)
next
  case (Cons e t)
  from Cons.prems consider (mv_left) a u' where ‹e = ev a› ‹u = ev a # u'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v), A)›
  | (mv_right) a v' where ‹e = ev a› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u, v'), A)›
  | (mv_both_ev) a u' v' where ‹e = ev a› ‹u = ev a # u'› ‹v = ev a # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
  | (mv_both_tick) r s u' v' where ‹u = ✓(r) # u'› ‹v = ✓(s) # v'›
    ‹t setinterleaves✓⇘tick_join⇙ ((u', v'), A)›
    by (cases e) (auto elim: Cons_ev_setinterleavesptickE Cons_tick_setinterleavesptickE)
  thus ?case by cases (auto dest!: Cons.hyps)
qed


lemma (in Syncptick_locale) disjoint_isInfHidden_seqRunL_to_Syncptick :
  assumes ‹A ∩ S = {}› and ‹isInfHidden_seqRun x P A t_P›
    and ‹t_Q ∈ 𝒯 Q› and ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
  shows ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ⟦S⟧✓ Q) A t›
proof -
  have tF_x : ‹tF (map x [0..<i])› for i
    by (metis assms(2) imageE is_ev_def seqRun_def tickFree_append_iff
        tickFree_map_tick_comp_iff tickFree_seqRun_iff)
  define t' where ‹t' i ≡ t @ map (ev ∘ of_ev) (map x [0..<i])› for i
  from assms(1, 2) have ‹{a. ev a ∈ set (map x [0..<i])} ∩ S = {}› for i
    by (simp add: disjoint_iff image_iff) (metis eventptick.inject(1))
  from tickFree_disjoint_setinterleavesptick_append_tailL[OF tF_x this assms(4)]
  have ‹seqRun t (ev ∘ of_ev ∘ x) i setinterleaves✓⇘(⊗✓)⇙ ((seqRun t_P x i, t_Q), S)› for i
    by (simp add: seqRun_def)
  moreover have ‹of_ev (x i) ∈ A› for i
    by (metis assms(2) eventptick.sel(1) image_iff)
  ultimately show ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ⟦S⟧✓ Q) A t›
    using assms(2, 3) by (auto simp add: T_Syncptick)
qed

lemma (in Syncptick_locale) disjoint_isInfHidden_seqRunR_to_Syncptick :
  ‹⟦A ∩ S = {}; isInfHidden_seqRun x Q A t_Q; t_P ∈ 𝒯 P;
    t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)⟧ ⟹
   isInfHidden_seqRun (ev ∘ of_ev ∘ x) (P ⟦S⟧✓ Q) A t›
  by (fold Syncptick_sym, rule Syncptick_locale.disjoint_isInfHidden_seqRunL_to_Syncptick)
    (use setinterleavesptick_sym in ‹blast intro: Syncptick_locale_sym.Syncptick_locale_axioms›)+



lemma (in Syncptick_locale) disjoint_Hiding_Syncptick_FD_Syncptick_Hiding_aux :
  ― ‹This lemma avoids duplication of the proof work.›
  assumes ‹A ∩ S = {}› ‹tF u› ‹ftF v› ‹t_P ∈ 𝒟 (P \ A)› ‹t_Q ∈ 𝒯 (Q \ A)›
    and * : ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
  shows ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
proof -
  let ?th_A = ‹λt. trace_hide t (ev ` A)›
  from ‹t_P ∈ 𝒟 (P \ A)› obtain t_P1 t_P2 
    where D_P : ‹tF t_P1› ‹ftF t_P2› ‹t_P = ?th_A t_P1 @ t_P2›
      ‹t_P1 ∈ 𝒟 P ∨ (∃t_P_x. isInfHidden_seqRun_strong t_P_x P A t_P1)›
    by (blast elim: D_Hiding_seqRunE)
  from setinterleavesptick_appendL[OF "*"[unfolded D_P(3)]] obtain u1 u2 t_Q1 t_Q2
    where ** : ‹u = u1 @ u2› ‹t_Q = t_Q1 @ t_Q2›
      ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P1, t_Q1), S)›
      ‹u2 setinterleaves✓⇘(⊗✓)⇙ ((t_P2, t_Q2), S)› by blast
  from ‹t_Q ∈ 𝒯 (Q \ A)› consider t_Q1' where ‹t_Q = ?th_A t_Q1'› ‹(t_Q1', ev ` A) ∈ ℱ Q›
    | (D_Q) t_Q1' t_Q2' where ‹tF t_Q1'› ‹ftF t_Q2'› ‹t_Q = ?th_A t_Q1' @ t_Q2'›
      ‹t_Q1' ∈ 𝒟 Q ∨ (∃t_Q_x. isInfHidden_seqRun_strong t_Q_x Q A t_Q1')›
    by (elim T_Hiding_seqRunE)
  thus ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
  proof cases
    fix t_Q1' assume ‹t_Q = ?th_A t_Q1'› ‹(t_Q1', ev ` A) ∈ ℱ Q›
    from ‹t_Q = ?th_A t_Q1'› "**"(2) obtain t_Q1''
      where ‹t_Q1 = ?th_A t_Q1''› ‹t_Q1'' ≤ t_Q1'›
      by (metis Prefix_Order.prefixI le_trace_hide)
    from F_T ‹(t_Q1', ev ` A) ∈ ℱ Q› ‹t_Q1'' ≤ t_Q1'› is_processT3_TR
    have ‹t_Q1'' ∈ 𝒯 Q› by blast
    from "**"(3)[unfolded ‹t_Q1 = ?th_A t_Q1''›,
        THEN disjoint_trace_hide_setinterleavesptick[OF ‹A ∩ S = {}›]]
    obtain u1' where ‹u1 = ?th_A u1'› ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
    from D_P(4) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
    proof (elim disjE exE)
      assume ‹t_P1 ∈ 𝒟 P›
      with ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› D_P(1) setinterleavesptick_tickFree_imp
      have ‹u1' = u1' @ []› ‹tF u1'› ‹ftF []›
        ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› ‹t_P1 ∈ 𝒟 P›
        by simp_all (blast intro: is_processT3_TR)+
      with ‹t_Q1'' ∈ 𝒯 Q› have ‹u1' ∈ 𝒟 (P ⟦S⟧✓ Q)› unfolding D_Syncptick by blast
      moreover have ‹u @ v = ?th_A u1' @ (u2 @ v)›
        by (simp add: "*"(1) "**"(1) ‹u1 = ?th_A u1'›)
      ultimately show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
        unfolding D_Hiding using ‹tF u› ‹ftF v› "**"(1) ‹tF u1'›
        by (auto intro: front_tickFree_append)
    next
      fix t_P_x assume ‹isInfHidden_seqRun_strong t_P_x P A t_P1›
      hence ‹isInfHidden_seqRun (ev ∘ of_ev ∘ t_P_x) (P ⟦S⟧✓ Q) A u1'›
        by (intro disjoint_isInfHidden_seqRunL_to_Syncptick
            [OF ‹A ∩ S = {}› _ ‹t_Q1'' ∈ 𝒯 Q› ‹u1' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)›]) simp
      with "**"(1) ‹u1 = ?th_A u1'› assms(2, 3) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
        unfolding D_Hiding_seqRun by clarify
          (metis append_eq_append_conv2[of u1 ‹u2 @ v› ‹u1 @ u2› v]
            isInfHidden_seqRun_imp_tickFree[of u1' ‹ev ∘ of_ev ∘ t_P_x› ‹P ⟦S⟧✓ Q› A]
            front_tickFree_append[of u2 v] tickFree_append_iff[of u1 u2])
    qed
  next
    case D_Q
    from setinterleavesptick_le_prefixLR
      [OF "*"[unfolded D_P(3) D_Q(3)], of ‹?th_A t_P1› ‹?th_A t_Q1'›]
    consider (left) u' t_Q1'' where ‹u' ≤ u› ‹t_Q1'' ≤ t_Q1'›
      ‹u' setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P1, ?th_A t_Q1''), S)›
    | (right) u' t_P1' where ‹u' ≤ u› ‹t_P1' ≤ t_P1›
      ‹u' setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P1', ?th_A t_Q1'), S)›
      by (auto dest!: le_trace_hide)
    thus ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
    proof cases
      case left
      have ‹t_Q1'' ∈ 𝒯 Q› by (meson D_Q(4) D_T is_processT3_TR left(2) t_le_seqRun)
      from disjoint_trace_hide_setinterleavesptick[OF ‹A ∩ S = {}› left(3)]
      obtain u'' where $ : ‹u' = ?th_A u''›
        ‹u'' setinterleaves✓⇘(⊗✓)⇙ ((t_P1, t_Q1''), S)› by blast
      from D_P(4) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      proof (elim disjE exE)
        assume ‹t_P1 ∈ 𝒟 P›
        hence ‹u'' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          by (simp add: D_Syncptick)
            (metis "$"(2) D_P(1) ‹t_Q1'' ∈ 𝒯 Q› append.right_neutral
              front_tickFree_Nil setinterleavesptick_tickFree_imp)
        with left(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding "$"(1))
            (metis Hiding_tickFree assms(2, 3) front_tickFree_append tickFree_append_iff)
      next
        fix t_P_x assume ‹isInfHidden_seqRun_strong t_P_x P A t_P1›
        hence ‹isInfHidden_seqRun (ev ∘ of_ev ∘ t_P_x) (P ⟦S⟧✓ Q) A u''›
          by (intro disjoint_isInfHidden_seqRunL_to_Syncptick
              [OF ‹A ∩ S = {}› _ ‹t_Q1'' ∈ 𝒯 Q› "$"(2)]) simp
        from left(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding_seqRun "$"(1))
            (metis ‹?this› assms(2, 3) front_tickFree_append
              isInfHidden_seqRun_imp_tickFree tickFree_append_iff)
      qed
    next
      case right
      have ‹t_P1' ∈ 𝒯 P› by (meson D_P(4) D_T is_processT3_TR right(2) t_le_seqRun)
      from disjoint_trace_hide_setinterleavesptick[OF ‹A ∩ S = {}› right(3)]
      obtain u'' where $ : ‹u' = ?th_A u''›
        ‹u'' setinterleaves✓⇘(⊗✓)⇙ ((t_P1', t_Q1'), S)› by blast
      from D_Q(4) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      proof (elim disjE exE)
        assume ‹t_Q1' ∈ 𝒟 Q›
        hence ‹u'' ∈ 𝒟 (P ⟦S⟧✓ Q)›
          by (simp add: D_Syncptick)
            (metis "$"(2) D_Q(1) ‹t_P1' ∈ 𝒯 P› append.right_neutral
              front_tickFree_Nil setinterleavesptick_tickFree_imp)
        with right(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding "$"(1))
            (metis Hiding_tickFree assms(2, 3) front_tickFree_append tickFree_append_iff)
      next
        fix t_Q_x assume ‹isInfHidden_seqRun_strong t_Q_x Q A t_Q1'›
        hence ‹isInfHidden_seqRun (ev ∘ of_ev ∘ t_Q_x) (P ⟦S⟧✓ Q) A u''›
          by (intro disjoint_isInfHidden_seqRunR_to_Syncptick
              [OF ‹A ∩ S = {}› _ ‹t_P1' ∈ 𝒯 P› "$"(2)]) simp
        from right(1) show ‹u @ v ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (elim Prefix_Order.prefixE, simp add: D_Hiding_seqRun "$"(1))
            (metis ‹?this› assms(2, 3) front_tickFree_append
              isInfHidden_seqRun_imp_tickFree tickFree_append_iff)
      qed
    qed
  qed
qed



theorem (in Syncptick_locale) disjoint_Hiding_Syncptick_FD_Syncptick_Hiding :
  ‹P ⟦S⟧✓ Q \ A ⊑FD (P \ A) ⟦S⟧✓ (Q \ A)› if ‹A ∩ S = {}›
proof (rule failure_divergence_refine_optimizedI)
  let ?th_A = ‹λt. trace_hide t (ev ` A)›
  fix t assume ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
  from this obtain u v t_P t_Q
    where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 (P \ A) ∧ t_Q ∈ 𝒯 (Q \ A) ∨ t_P ∈ 𝒯 (P \ A) ∧ t_Q ∈ 𝒟 (Q \ A)›
    unfolding D_Syncptick by blast
  from "*"(5) show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
  proof (elim disjE conjE)
    show ‹t_P ∈ 𝒟 (P \ A) ⟹ t_Q ∈ 𝒯 (Q \ A) ⟹ t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      by (simp add: "*"(1-4) disjoint_Hiding_Syncptick_FD_Syncptick_Hiding_aux ‹A ∩ S = {}›)
  next
    assume ‹t_P ∈ 𝒯 (P \ A)› ‹t_Q ∈ 𝒟 (Q \ A)›
    have ‹u setinterleaves✓⇘λs r. r ⊗✓ s⇙ ((t_Q, t_P), S)›
      using "*"(4) setinterleavesptick_sym by blast
    from Syncptick_locale_sym.disjoint_Hiding_Syncptick_FD_Syncptick_Hiding_aux
      [OF ‹A ∩ S = {}› "*"(2, 3) ‹t_Q ∈ 𝒟 (Q \ A)› ‹t_P ∈ 𝒯 (P \ A)› this]
    have ‹u @ v ∈ 𝒟 (Syncptick_locale_sym.Syncptick Q S P \ A)› .
    also have ‹Syncptick_locale_sym.Syncptick Q S P = P ⟦S⟧✓ Q› by (fact Syncptick_sym)
    finally show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)› unfolding "*"(1) .
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
    and subset_div : ‹𝒟 ((P \ A) ⟦S⟧✓ (Q \ A)) ⊆ 𝒟 (P ⟦S⟧✓ Q \ A)›
  from this(1) consider ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
    | (fail_Sync) t_P t_Q X_P X_Q where ‹(t_P, X_P) ∈ ℱ (P \ A)› ‹(t_Q, X_Q) ∈ ℱ (Q \ A)›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› ‹X ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
    unfolding Syncptick_projs by blast
  thus ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
  proof cases
    from subset_div show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A)) ⟹ (t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
      by (simp add: in_mono is_processT8)
  next
    case fail_Sync
    from fail_Sync(1, 2) consider ‹t_P ∈ 𝒟 (P \ A) ∨ t_Q ∈ 𝒟 (Q \ A)›
      | (fail_Hiding) t_P' t_Q' where
        ‹t_P = trace_hide t_P' (ev ` A)› ‹(t_P', X_P ∪ ev ` A) ∈ ℱ P›
        ‹t_Q = trace_hide t_Q' (ev ` A)› ‹(t_Q', X_Q ∪ ev ` A) ∈ ℱ Q›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
    proof cases
      assume ‹t_P ∈ 𝒟 (P \ A) ∨ t_Q ∈ 𝒟 (Q \ A)›
      with fail_Sync(1-3) have ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
        by (simp add: D_Syncptick')
          (metis F_T append_self_conv front_tickFree_Nil)
      with subset_div show ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
        by (simp add: in_mono is_processT8)
    next
      case fail_Hiding
      from disjoint_trace_hide_setinterleavesptick
        [OF ‹A ∩ S = {}› fail_Sync(3)[unfolded fail_Hiding(1, 3)]]
      obtain t' where * : ‹t = trace_hide t' (ev ` A)›
        ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)› by blast
      from fail_Sync(4) have ‹X ∪ ev ` A ⊆ super_ref_Syncptick (⊗✓) (X_P ∪ ev ` A) S (X_Q ∪ ev ` A)›
        by (auto simp add: super_ref_Syncptick_def image_iff)
      with "*"(2) fail_Hiding(2, 4) have ‹(t', X ∪ ev ` A) ∈ ℱ (P ⟦S⟧✓ Q)›
        by (auto simp add: F_Syncptick)
      with "*"(1) show ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)› unfolding F_Hiding by blast
    qed
  qed
qed



theorem (in Syncptick_locale) disjoint_finite_Hiding_Syncptick :
  ‹P ⟦S⟧✓ Q \ A = (P \ A) ⟦S⟧✓ (Q \ A)› if ‹A ∩ S = {}› and ‹finite A›
  ― ‹Monster theorem!›
proof (rule FD_antisym)
  from disjoint_Hiding_Syncptick_FD_Syncptick_Hiding[OF ‹A ∩ S = {}›]
  show ‹P ⟦S⟧✓ Q \ A ⊑FD (P \ A) ⟦S⟧✓ (Q \ A)› .
next
  let ?th_A = ‹λt. trace_hide t (ev ` A)›
  show ‹(P \ A) ⟦S⟧✓ (Q \ A) ⊑FD P ⟦S⟧✓ Q \ A›
  proof (rule failure_divergence_refine_optimizedI)
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q \ A)›
      and subset_div : ‹𝒟 (P ⟦S⟧✓ Q \ A) ⊆ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
    from this(1) consider ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
      | t' where ‹t = ?th_A t'› ‹(t', X ∪ ev ` A) ∈ ℱ (P ⟦S⟧✓ Q)›
      unfolding F_Hiding D_Hiding by blast
    thus ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
    proof cases
      show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A) ⟹ (t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
        using subset_div is_processT8 by blast
    next
      fix t' assume ‹t = ?th_A t'› ‹(t', X ∪ ev ` A) ∈ ℱ (P ⟦S⟧✓ Q)›
      from this(2) consider ‹t' ∈ 𝒟 (P ⟦S⟧✓ Q)›
        | (fail) t_P X_P t_Q X_Q where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t' setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
          ‹X ∪ ev ` A ⊆ super_ref_Syncptick (⊗✓) X_P S X_Q›
        unfolding Syncptick_projs by auto
      thus ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
      proof cases
        assume ‹t' ∈ 𝒟 (P ⟦S⟧✓ Q)›
        with ‹t = ?th_A t'› have ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
          by (metis mem_D_imp_mem_D_Hiding)
        with subset_div is_processT8 show ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))› by blast
      next
        case fail
        from ‹A ∩ S = {}› fail(4) have ‹X_P = X_P ∪ ev ` A› ‹X_Q = X_Q ∪ ev ` A›
          ― ‹i.e. term‹ev ` A ⊆ X_P› and term‹ev ` A ⊆ X_Q››
          by (auto simp add: super_ref_Syncptick_def)
        with fail(1, 2) have ‹(?th_A t_P, X_P) ∈ ℱ (P \ A)›
          ‹(?th_A t_Q, X_Q) ∈ ℱ (Q \ A)›
          by (auto simp add: F_Hiding)
        moreover from fail(3) have ‹t setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P, ?th_A t_Q), S)›
          unfolding ‹t = ?th_A t'› by (fact setinterleavesptick_trace_hide)
        ultimately show ‹(t, X) ∈ ℱ ((P \ A) ⟦S⟧✓ (Q \ A))›
          using fail(4) unfolding F_Syncptick by fast
      qed
    qed
  next
    fix t assume ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)›
    then obtain u v where * : ‹ftF v› ‹tF u› ‹t = ?th_A u @ v›
      ‹u ∈ 𝒟 (P ⟦S⟧✓ Q) ∨ (∃x. isInfHidden_seqRun_strong x (P ⟦S⟧✓ Q) A u)›
      by (blast elim: D_Hiding_seqRunE)
    from "*"(4) show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
    proof (elim disjE exE)
      assume ‹u ∈ 𝒟 (P ⟦S⟧✓ Q)›
      then obtain u1 u2 t_P t_Q where ** : ‹u = u1 @ u2› ‹tF u1› ‹ftF u2›
        ‹u1 setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
        unfolding D_Syncptick by blast
      have ‹t = ?th_A u1 @ (?th_A u2 @ v)›
        by (simp add: "*"(3) "**"(1))
      moreover from "**"(2) have ‹tF (?th_A u1)› using Hiding_tickFree by blast
      moreover have ‹ftF (?th_A u2 @ v)›
        by (metis D_imp_front_tickFree ‹t ∈ 𝒟 (P ⟦S⟧✓ Q \ A)› calculation(1)
            front_tickFree_append_iff front_tickFree_charn)
      moreover from "**"(4) have ‹?th_A u1 setinterleaves✓⇘(⊗✓)⇙ ((?th_A t_P, ?th_A t_Q), S)›
        by (fact setinterleavesptick_trace_hide)
      moreover from "**"(5) have ‹?th_A t_P ∈ 𝒟 (P \ A) ∧ ?th_A t_Q ∈ 𝒯 (Q \ A) ∨
                                  ?th_A t_P ∈ 𝒯 (P \ A) ∧ ?th_A t_Q ∈ 𝒟 (Q \ A)›
        by (metis mem_D_imp_mem_D_Hiding mem_T_imp_mem_T_Hiding)
      ultimately show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
        unfolding D_Syncptick by blast
    next
      fix x assume ** : ‹isInfHidden_seqRun_strong x (P ⟦S⟧✓ Q) A u›
      from "**" have *** : ‹∃t_P t_Q. t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧
        seqRun u x i setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› for i
        unfolding Syncptick_projs by blast

      define t_P_t_Q where ‹t_P_t_Q i ≡ SOME (t_P, t_Q). t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧
      seqRun u x i setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› for i
      define t_P where ‹t_P ≡ fst ∘ t_P_t_Q›
      define t_Q where ‹t_Q ≡ snd ∘ t_P_t_Q›
      have **** : ‹t_P i ∈ 𝒯 P› ‹t_Q i ∈ 𝒯 Q›
        ‹seqRun u x i setinterleaves✓⇘(⊗✓)⇙ ((t_P i, t_Q i), S)› for i
        by (use "***"[of i] in ‹simp add: t_P_def t_Q_def,
                              cases ‹t_P_t_Q i›, simp add: t_P_t_Q_def,
                              metis (mono_tags, lifting) case_prod_conv someI_ex›)+
      from "*"(2) "**" have ‹set (seqRun u x i) ⊆ {ev a |a. ev a ∈ set u} ∪ ev ` A› for i
        by (simp add: seqRun_def subset_iff)
          (metis image_iff list.set_map tickFree_iff_is_map_ev)
      have ***** : ‹{ev a |a. ev a ∈ set (t_P i)} ∪ {ev a |a. ev a ∈ set (t_Q i)} ⊆
                      {ev a |a. ev a ∈ set u} ∪ ev ` A› for i
        by (rule subset_trans[OF setinterleavesptick_imp_superset_ev[OF "****"(3)]])
          (use ‹set (seqRun u x i) ⊆ {ev a |a. ev a ∈ set u} ∪ ev ` A› in blast)
      have ****** : ‹tF (t_P i)› ‹tF (t_Q i)› for i
        using tickFree_setinterleavesptick_iff[OF "****"(3)[of i]]
        by (metis "*"(2) "**" eventptick.disc(1) imageE tickFree_seqRun_iff)+

      { fix i
        have ‹{w. tF w ∧ {ev a |a. ev a ∈ set w} ⊆ set u ∪ ev ` A ∧ length w ≤ i} ⊆
                  map (ev ∘ of_ev) ` {w. set w ⊆ set u ∪ ev ` A ∧ length w ≤ i}›
          (is ‹?S1 ⊆ map (ev ∘ of_ev) ` ?S2›)
        proof (rule subsetI)
          fix w assume ‹w ∈ ?S1›
          hence ‹map (ev ∘ of_ev) (map (ev ∘ of_ev) w) = w›
            by (induct w) (auto simp add: subset_iff)
          moreover from ‹w ∈ ?S1› have ‹map (ev ∘ of_ev) w ∈ ?S2›
            by (induct w) (auto simp add: subset_iff)
          ultimately show ‹w ∈ map (ev ∘ of_ev) ` ?S2›
            by (metis (lifting) image_eqI)
        qed
        moreover have ‹finite {w. set w ⊆ set u ∪ ev ` A ∧ length w ≤ i}›
          by (rule finite_lists_length_le) (simp add: ‹finite A›)
        ultimately have ‹finite {w. tF w ∧ {ev a |a. ev a ∈ set w} ⊆ set u ∪ ev ` A ∧ length w ≤ i}›
          using finite_subset[OF _ finite_imageI] by blast
      } note £ = this

      have ‹inj t_P_t_Q›
      proof (rule injI)
        fix i j assume ‹t_P_t_Q i = t_P_t_Q j›
        with "****"(3) have ‹seqRun u x i setinterleaves✓⇘tick_join⇙ ((t_P i, t_Q i), S) ∧
        seqRun u x j setinterleaves✓⇘tick_join⇙ ((t_P i, t_Q i), S)›
          unfolding t_P_t_Q_def t_P_def t_Q_def by fastforce
        with setinterleavesptick_eq_length
        have ‹length (seqRun u x i) = length (seqRun u x j)› by blast
        thus ‹i = j› by simp
      qed
      hence ‹infinite (range t_P_t_Q)› using finite_imageD by blast
      moreover have ‹range t_P_t_Q ⊆ range t_P × range t_Q›
        by (simp add: t_P_def t_Q_def subset_iff image_iff) (metis fst_conv snd_conv)
      ultimately have ‹infinite (range t_P) ∨ infinite (range t_Q)› 
        by (meson finite_SigmaI infinite_super)

      thus ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))›
      proof (elim disjE)
        assume ‹infinite (range t_P)›
        have ‹finite {w. ∃t'∈range t_P. w = take i t'}› for i
          using "******"(1) "*****"
          by (auto intro!: finite_subset[OF _ "£"[of i]] simp add: image_iff subset_iff)
            (metis append_take_drop_id tickFree_append_iff, metis eventptick.inject(1) in_set_takeD)
        with ‹infinite (range t_P)› obtain t_P' :: ‹nat ⇒ _›
          where $ : ‹strict_mono t_P'› ‹range t_P' ⊆ {w. ∃t'∈range t_P. w ≤ t'}›
          using KoenigLemma by blast
        from "$"(2) "****"(1) is_processT3_TR have ‹range t_P' ⊆ 𝒯 P› by blast
        define t_P'' where ‹t_P'' i ≡ t_P' (i + length u)› for i
        from ‹range t_P' ⊆ 𝒯 P› have ‹range t_P'' ⊆ 𝒯 P› and ‹strict_mono t_P''›
          by (auto simp add: t_P''_def "$"(1) strict_monoD strict_monoI)
        have $$ : ‹?th_A (t_P'' i) = ?th_A (t_P'' 0)› for i
        proof -
          have ‹length u ≤ length (t_P'' 0)›
            by (metis "$"(1) add_0 add_leD1 t_P''_def length_strict_mono)
          obtain t' where ‹t_P'' i = t_P'' 0 @ t'›
            by (meson prefixE ‹strict_mono t_P''› strict_mono_less_eq zero_order(1))
          moreover from "$"(2) obtain j where ‹t_P'' i ≤ t_P j› by (auto simp add: t_P''_def)
          ultimately obtain t'' where ‹t_P j = t_P'' 0 @ t' @ t''› by (metis prefixE append.assoc)

          have ‹tF (t' @ t'')›
            by (metis "******"(1) ‹t_P j = t_P'' 0 @ t' @ t''› tickFree_append_iff)
          with setinterleavesptick_set_subsetL
            [OF "****"(3)[of j], where n = ‹length (t_P'' 0)›, unfolded ‹t_P j = t_P'' 0 @ t' @ t''›]
          have ‹e ∈ set (t' @ t'') ⟹ e ∈ {ev a |a. ev a ∈ set (drop (length (t_P'' 0)) (seqRun u x j))}› for e
            by (cases e) (auto simp add: tickFree_def)
          moreover have ‹{a. ev a ∈ set (drop (length (t_P'' 0)) (seqRun u x j))} ⊆
                       {a. ev a ∈ set (drop (length u) (seqRun u x j))}›
            by (simp add: subset_iff)
              (meson ‹length u ≤ length (t_P'' 0)› in_mono set_drop_subset_set_drop)
          moreover from "**" have ‹set (drop (length u) (seqRun u x j)) ⊆ ev ` A›
            by (auto simp add: seqRun_def)
          ultimately have ‹set (t' @ t'') ⊆ ev ` A› by blast
          thus ‹?th_A (t_P'' i) = ?th_A (t_P'' 0)›
            by (simp add: ‹t_P'' i = t_P'' 0 @ t'› subset_iff)
        qed
        from "$"(2) obtain i where ‹t_P'' 0 ≤ t_P i› by (auto simp add: t_P''_def)
        with prefixE obtain w where ‹t_P i = t_P'' 0 @ w› by blast
        have ‹ftF v› by (fact "*"(1))
        moreover have ‹tF (?th_A (seqRun u x i))›
          by (metis "*"(2) "**" Hiding_tickFree trace_hide_seqRun_eq_iff)
        moreover have ‹t = ?th_A (seqRun u x i) @ v›
          by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
        moreover have ‹?th_A (seqRun u x i) setinterleaves✓⇘(⊗✓)⇙ ((?th_A (t_P i), ?th_A (t_Q i)), S)›
          by (intro setinterleavesptick_trace_hide "****"(3))
        moreover have ‹?th_A (t_P i) ∈ 𝒟 (P \ A)›
        proof (unfold D_Hiding, clarify, intro exI conjI)
          show ‹ftF (?th_A w)›
            by (metis "******"(1) Hiding_front_tickFree ‹t_P i = t_P'' 0 @ w›
                tickFree_append_iff tickFree_imp_front_tickFree)
        next
          show ‹tF (t_P'' 0)›
            by (metis "******"(1) ‹t_P i = t_P'' 0 @ w› tickFree_append_iff)
        next
          show ‹?th_A (t_P i) = ?th_A (t_P'' 0) @ ?th_A w›
            by (simp add: ‹t_P i = t_P'' 0 @ w›)
        next
          show ‹t_P'' 0 ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ t_P'' 0 ∈ range f)›
            using "$$" ‹range t_P'' ⊆ 𝒯 P› ‹strict_mono t_P''› by blast
        qed
        moreover have ‹?th_A (t_Q i) ∈ 𝒯 (Q \ A)›
        proof (cases ‹∃t'. ?th_A t' = ?th_A (t_Q i) ∧ (t', ev ` A) ∈ ℱ Q›)
          assume ‹∃t'. ?th_A t' = ?th_A (t_Q i) ∧ (t', ev ` A) ∈ ℱ Q›
          then obtain t' where ‹?th_A (t_Q i) = ?th_A t'› ‹(t', ev ` A) ∈ ℱ Q› by metis
          thus ‹?th_A (t_Q i) ∈ 𝒯 (Q \ A)› unfolding T_Hiding by blast
        next
          assume ‹∄t'. ?th_A t' = ?th_A (t_Q i) ∧ (t', ev ` A) ∈ ℱ Q›
          with inf_hidden[OF _ "****"(2)] obtain t_Q' j
            where ‹isInfHiddenRun t_Q' Q A› ‹t_Q i = t_Q' j› by blast
          thus ‹?th_A (t_Q i) ∈ 𝒯 (Q \ A)›
            unfolding T_Hiding using "******"(2) front_tickFree_Nil by blast
        qed
        ultimately show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))› unfolding D_Syncptick by blast
      next
        assume ‹infinite (range t_Q)›
        have ‹finite {w. ∃t'∈range t_Q. w = take i t'}› for i
          using "******"(2) "*****"
          by (auto intro!: finite_subset[OF _ "£"[of i]] simp add: image_iff subset_iff)
            (metis append_take_drop_id tickFree_append_iff, metis eventptick.inject(1) in_set_takeD)
        with ‹infinite (range t_Q)› obtain t_Q' :: ‹nat ⇒ _›
          where $ : ‹strict_mono t_Q'› ‹range t_Q' ⊆ {w. ∃t'∈range t_Q. w ≤ t'}›
          using KoenigLemma by blast
        from "$"(2) "****"(2) is_processT3_TR have ‹range t_Q' ⊆ 𝒯 Q› by blast
        define t_Q'' where ‹t_Q'' i ≡ t_Q' (i + length u)› for i
        from ‹range t_Q' ⊆ 𝒯 Q› have ‹range t_Q'' ⊆ 𝒯 Q› and ‹strict_mono t_Q''›
          by (auto simp add: t_Q''_def "$"(1) strict_monoD strict_monoI)
        have $$ : ‹?th_A (t_Q'' i) = ?th_A (t_Q'' 0)› for i
        proof -
          have ‹length u ≤ length (t_Q'' 0)›
            by (metis "$"(1) add_0 add_leD1 t_Q''_def length_strict_mono)
          obtain t' where ‹t_Q'' i = t_Q'' 0 @ t'›
            by (meson prefixE ‹strict_mono t_Q''› strict_mono_less_eq zero_order(1))
          moreover from "$"(2) obtain j where ‹t_Q'' i ≤ t_Q j› by (auto simp add: t_Q''_def)
          ultimately obtain t'' where ‹t_Q j = t_Q'' 0 @ t' @ t''› by (metis prefixE append.assoc)
          have ‹tF (t' @ t'')›
            by (metis "******"(2) ‹t_Q j = t_Q'' 0 @ t' @ t''› tickFree_append_iff)
          with setinterleavesptick_set_subsetR
            [OF "****"(3)[of j], where n = ‹length (t_Q'' 0)›, unfolded ‹t_Q j = t_Q'' 0 @ t' @ t''›]
          have ‹e ∈ set (t' @ t'') ⟹ e ∈ {ev a |a. ev a ∈ set (drop (length (t_Q'' 0)) (seqRun u x j))}› for e
            by (cases e) (auto simp add: tickFree_def)
          moreover have ‹{a. ev a ∈ set (drop (length (t_Q'' 0)) (seqRun u x j))} ⊆
                         {a. ev a ∈ set (drop (length u) (seqRun u x j))}›
            by (simp add: subset_iff)
              (meson ‹length u ≤ length (t_Q'' 0)› in_mono set_drop_subset_set_drop)
          moreover from "**" have ‹set (drop (length u) (seqRun u x j)) ⊆ ev ` A›
            by (auto simp add: seqRun_def)
          ultimately have ‹set (t' @ t'') ⊆ ev ` A› by blast
          thus ‹?th_A (t_Q'' i) = ?th_A (t_Q'' 0)›
            by (simp add: ‹t_Q'' i = t_Q'' 0 @ t'› subset_iff)
        qed
        from "$"(2) obtain i where ‹t_Q'' 0 ≤ t_Q i› by (auto simp add: t_Q''_def)
        with prefixE obtain w where ‹t_Q i = t_Q'' 0 @ w› by blast
        have ‹ftF v› by (fact "*"(1))
        moreover have ‹tF (?th_A (seqRun u x i))›
          by (metis "*"(2) "**" Hiding_tickFree trace_hide_seqRun_eq_iff)
        moreover have ‹t = ?th_A (seqRun u x i) @ v›
          by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
        moreover have ‹?th_A (seqRun u x i) setinterleaves✓⇘(⊗✓)⇙ ((?th_A (t_P i), ?th_A (t_Q i)), S)›
          by (intro setinterleavesptick_trace_hide "****"(3))
        moreover have ‹?th_A (t_Q i) ∈ 𝒟 (Q \ A)›
        proof (unfold D_Hiding, clarify, intro exI conjI)
          show ‹ftF (?th_A w)›
            by (metis "******"(2) Hiding_front_tickFree ‹t_Q i = t_Q'' 0 @ w›
                tickFree_append_iff tickFree_imp_front_tickFree)
        next
          show ‹tF (t_Q'' 0)›
            by (metis "******"(2) ‹t_Q i = t_Q'' 0 @ w› tickFree_append_iff)
        next
          show ‹?th_A (t_Q i) = ?th_A (t_Q'' 0) @ ?th_A w›
            by (simp add: ‹t_Q i = t_Q'' 0 @ w›)
        next
          show ‹t_Q'' 0 ∈ 𝒟 Q ∨ (∃f. isInfHiddenRun f Q A ∧ t_Q'' 0 ∈ range f)›
            using "$$" ‹range t_Q'' ⊆ 𝒯 Q› ‹strict_mono t_Q''› by blast
        qed
        moreover have ‹?th_A (t_P i) ∈ 𝒯 (P \ A)›
        proof (cases ‹∃t'. ?th_A t' = ?th_A (t_P i) ∧ (t', ev ` A) ∈ ℱ P›)
          assume ‹∃t'. ?th_A t' = ?th_A (t_P i) ∧ (t', ev ` A) ∈ ℱ P›
          then obtain t' where ‹?th_A (t_P i) = ?th_A t'› ‹(t', ev ` A) ∈ ℱ P› by metis
          thus ‹?th_A (t_P i) ∈ 𝒯 (P \ A)› unfolding T_Hiding by blast
        next
          assume ‹∄t'. ?th_A t' = ?th_A (t_P i) ∧ (t', ev ` A) ∈ ℱ P›
          with inf_hidden[OF _ "****"(1)] obtain t_P' j
            where ‹isInfHiddenRun t_P' P A› ‹t_P i = t_P' j› by blast
          thus ‹?th_A (t_P i) ∈ 𝒯 (P \ A)›
            unfolding T_Hiding using "******"(1) front_tickFree_Nil by blast
        qed
        ultimately show ‹t ∈ 𝒟 ((P \ A) ⟦S⟧✓ (Q \ A))› unfolding D_Syncptick by blast
      qed
    qed
  qed
qed



lemma disjoint_Hiding_MultiSyncptick_FD_MultiSyncptick_Hiding :
  ‹⟦S⟧✓ l ∈@ L. P l \ A ⊑FD ⟦S⟧✓ l ∈@ L. (P l \ A)› if ‹A ∩ S = {}›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0)
  show ?case by (simp add: RenamingTick_Hiding)
next
  case (3 l0 l1 L)
  have ‹⟦S⟧✓ l ∈@ (l0 # l1 # L). P l \ A =
        P l0 ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). P l \ A› by simp
  also have ‹… ⊑FD (P l0 \ A) ⟦S⟧✓Rlist (⟦S⟧✓ l ∈@ (l1 # L). P l \ A)›
    by (simp add: SyncRlist.disjoint_Hiding_Syncptick_FD_Syncptick_Hiding ‹A ∩ S = {}›)
  also have ‹… ⊑FD (P l0 \ A) ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). (P l \ A)›
    by (simp add: "3.hyps"(2) SyncRlist.mono_Syncptick_FD)
  also have ‹… = ⟦S⟧✓ l ∈@ (l0 # l1 # L). (P l \ A)› by simp
  finally show ?case .
qed


lemma disjoint_finite_Hiding_MultiSyncptick :
  ‹⟦S⟧✓ l ∈@ L. P l \ A = ⟦S⟧✓ l ∈@ L. (P l \ A)› if ‹A ∩ S = {}› and ‹finite A›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0)
  show ?case by (simp add: RenamingTick_Hiding)
next
  case (3 l0 l1 L)
  have ‹⟦S⟧✓ l ∈@ (l0 # l1 # L). P l \ A =
        P l0 ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). P l \ A› by simp
  also have ‹… = (P l0 \ A) ⟦S⟧✓Rlist (⟦S⟧✓ l ∈@ (l1 # L). P l \ A)›
    by (simp add: SyncRlist.disjoint_finite_Hiding_Syncptick ‹A ∩ S = {}› ‹finite A›)
  also have ‹… = (P l0 \ A) ⟦S⟧✓Rlist ⟦S⟧✓ l ∈@ (l1 # L). (P l \ A)›
    by (simp add: "3.hyps"(2) SyncRlist.mono_Syncptick_FD)
  also have ‹… = ⟦S⟧✓ l ∈@ (l0 # l1 # L). (P l \ A)› by simp
  finally show ?case .
qed



section ‹Other Laws of Synchronization Product›

subsection ‹Synchronization Set can be restricted›

lemma setinterleavesptick_is_restrictable_on_superset_events_of :
  ‹{a. ev a ∈ set u ∨ ev a ∈ set v} ⊆ A ⟹
   t setinterleaves✓⇘tick_join⇙ ((u, v), S) ⟷
   t setinterleaves✓⇘tick_join⇙ ((u, v), S ∩ A)›
  by (induct ‹(tick_join, u, S, v)› arbitrary: t u v)
    (auto simp add: subset_iff split: option.split_asm)

lemma (in Syncptick_locale) Syncptick_is_restrictable_on_events_of :
  ‹P ⟦S⟧✓ Q = P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q›
proof -
  have * : ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q ⟹
            {a. ev a ∈ set t_P ∨ ev a ∈ set t_Q} ⊆ α(P) ∪ α(Q)›
    ‹(t_P, X_P) ∈ ℱ P ⟹ (t_Q, X_Q) ∈ ℱ Q ⟹
     {a. ev a ∈ set t_P ∨ ev a ∈ set t_Q} ⊆ α(P) ∪ α(Q)› for t_P t_Q X_P X_Q
    by (auto intro: events_of_memI dest: F_T D_T)
  show ‹P ⟦S⟧✓ Q = P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 (P ⟦S⟧✓ Q) ⟹ t ∈ 𝒟 (P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q)› for t
      using setinterleavesptick_is_restrictable_on_superset_events_of[OF "*"(1)]
      unfolding D_Syncptick by blast
  next
    show ‹t ∈ 𝒟 (P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q) ⟹ t ∈ 𝒟 (P ⟦S⟧✓ Q)› for t
      using setinterleavesptick_is_restrictable_on_superset_events_of[OF "*"(1)]
      unfolding D_Syncptick by blast
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)›
    then obtain t_P t_Q X_P X_Q
      where $ : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Syncptick tick_join X_P S X_Q›
      unfolding Syncptick_projs by blast
    from "$"(1) have ‹(t_P, X_P ∪ {ev a |a. a ∉ α(P)}) ∈ ℱ P›
      by (rule is_processT5) (auto intro: events_of_memI dest!: F_T)
    moreover from "$"(2) have ‹(t_Q, X_Q ∪ {ev a |a. a ∉ α(Q)}) ∈ ℱ Q›
      by (rule is_processT5) (auto intro: events_of_memI dest!: F_T)
    moreover from setinterleavesptick_is_restrictable_on_superset_events_of
      [OF "*"(2)[OF "$"(1, 2)]] "$"(3)
    have ‹t setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), S ∩ (α(P) ∪ α(Q)))› by blast
    moreover from "$"(4)
    have ‹X ⊆ super_ref_Syncptick
              tick_join (X_P ∪ {ev a |a. a ∉ α(P)})
              (S ∩ (α(P) ∪ α(Q))) (X_Q ∪ {ev a |a. a ∉ α(Q)})›
      by (auto simp add: super_ref_Syncptick_def)
    ultimately show ‹(t, X) ∈ ℱ (P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q)›
      by (auto simp add: F_Syncptick)
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q)›
      ‹t ∉ 𝒟 (P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q)›
    then obtain t_P t_Q X_P X_Q
      where $ : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), S ∩ (α(P) ∪ α(Q)))›
        ‹X ⊆ super_ref_Syncptick tick_join X_P (S ∩ (α(P) ∪ α(Q))) X_Q›
      unfolding Syncptick_projs by blast
    from setinterleavesptick_is_restrictable_on_superset_events_of
      [OF "*"(2)[OF "$"(1, 2)]] "$"(3)
    have ‹t setinterleaves✓⇘tick_join⇙ ((t_P, t_Q), S)› by blast
    moreover from "$"(4) have ‹X ⊆ super_ref_Syncptick tick_join X_P S X_Q›
      by (meson Int_lower1 in_mono subsetI super_ref_Syncptick_mono)
    ultimately show ‹(t, X) ∈ ℱ (P ⟦S⟧✓ Q)›
      using "$"(1, 2) by (auto simp add: F_Syncptick)
  qed
qed

corollary (in Syncptick_locale) Syncptick_is_restrictable_on_superset_events_of :
  ‹P ⟦S⟧✓ Q = P ⟦S ∩ A⟧✓ Q› if ‹α(P) ∪ α(Q) ⊆ A›
proof (rule trans[OF Syncptick_is_restrictable_on_events_of],
    rule trans[OF _ Syncptick_is_restrictable_on_events_of[symmetric]])
  show ‹P ⟦S ∩ (α(P) ∪ α(Q))⟧✓ Q = P ⟦S ∩ A ∩ (α(P) ∪ α(Q))⟧✓ Q›
    using ‹α(P) ∪ α(Q) ⊆ A› by (auto intro: arg_cong[where f = ‹λS. P ⟦S⟧✓ Q›])
qed


lemma ‹tF t ⟹ {a. ev a ∈ set u} ∩ S = {} ⟹ a ∈ S ⟹
       ¬ t setinterleaves✓⇘tick_join⇙ ((u, ev a # v), S)›
proof (induct ‹(tick_join, u, S, v)› arbitrary: t u v)
  case (ev_setinterleavingptick_Nil a u)
  thus ?case by (simp add: disjoint_iff) (meson tickFree_Cons_iff)
next
  case (ev_setinterleavingptick_ev a u b v)
  then show ?case by (simp add: disjoint_iff) (meson tickFree_Cons_iff)
next
  case (ev_setinterleavingptick_tick a u s v)
  thus ?case
    by (simp add: disjoint_iff)
      (metis empty_iff list.set_intros(1)
        ev_notin_both_sets_imp_empty_setinterleavingptick) 
qed simp_all



subsection ‹Some Refinements›

context Syncptick_locale begin

lemma Mndetprefix_Syncptick_Det_distr_FD :
  ‹(⊓ a ∈ A → (P a ⟦ C ⟧✓ (⊓ b ∈ B → Q b))) □
   (⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧✓ Q b))
   ⊑FD (⊓ a ∈ A → P a) ⟦ C ⟧✓ (⊓ b ∈ B → Q b)›
  (is ‹?lhs1 □ ?lhs2 ⊑FD ?rhs›)
  if ‹A ≠ {}› ‹B ≠ {}› ‹A ∩ C = {}› ‹B ∩ C = {}›
proof -
  have ‹?lhs1 = ⊓ b∈B. ⊓ a∈A. (a → (P a ⟦C⟧✓ (b → Q b)))› (is ‹_ = ?lhs1'›)
    by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
        Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right
        write0_def GlobalNdet_Mprefix_distr[OF ‹B ≠ {}›, symmetric])
      (subst GlobalNdet_sets_commute, simp)
  moreover have ‹?lhs2 = ⊓ b∈B. ⊓ a∈A. (b → (a → P a ⟦C⟧✓ Q b))› (is ‹_ = ?lhs2'›)
    by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
        Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right
        write0_def GlobalNdet_Mprefix_distr[OF ‹A ≠ {}›, symmetric])
  ultimately have ‹?lhs1 □ ?lhs2 = ?lhs1' □ ?lhs2'› by simp
  moreover have ‹?lhs1' □ ?lhs2' ⊑FD ⊓ b∈B. ⊓ a∈A.   (a → (P a ⟦C⟧✓ (b → Q b)))
                                                    □ (b → ((a → P a) ⟦C⟧✓ Q b))›
    by (auto simp add: ‹A ≠ {}› ‹B ≠ {}› refine_defs GlobalNdet_projs Det_projs write0_def)
  moreover have ‹… = ⊓ b∈B. ⊓ a∈A. ((a → P a) ⟦C⟧✓ (b → Q b))›
    by (rule mono_GlobalNdet_eq, rule mono_GlobalNdet_eq,
        simp add: write0_def, subst Mprefix_Syncptick_Mprefix_indep)
      (use ‹A ∩ C = {}› ‹B ∩ C = {}› in auto)
  moreover have ‹… = ?rhs›
    by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
        Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right)
  ultimately show ‹?lhs1 □ ?lhs2 ⊑FD ?rhs› by argo
qed


lemmas Mndetprefix_Syncptick_Det_distr_F =
  Mndetprefix_Syncptick_Det_distr_FD[THEN leFD_imp_leF]

lemmas Mndetprefix_Syncptick_Det_distr_D =
  Mndetprefix_Syncptick_Det_distr_FD[THEN leFD_imp_leD]

lemmas Mndetprefix_Syncptick_Det_distr_T =
  Mndetprefix_Syncptick_Det_distr_F[THEN leF_imp_leT]

lemma Mndetprefix_Syncptick_Det_distr_DT :
  ‹⟦A ≠ {}; B ≠ {}; A ∩ C = {}; B ∩ C = {}⟧ ⟹
   (⊓ a ∈ A → (P a ⟦ C ⟧✓ (⊓ b ∈ B → Q b))) □
   (⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧✓ Q b))
   ⊑DT (⊓ a ∈ A → P a) ⟦ C ⟧✓ (⊓ b ∈ B → Q b)›
  by (simp add: Mndetprefix_Syncptick_Det_distr_D
      Mndetprefix_Syncptick_Det_distr_T leD_leT_imp_leDT)


end

(*<*)
end
  (*>*)