Theory Step_CSP_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Step laws
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)


section‹ The Step-Laws ›

(*<*)
theory Step_CSP_Laws                                               
  imports Constant_Processes Deterministic_Choice Non_Deterministic_Choice
    Global_Non_Deterministic_Choice Sliding_Choice
    Multi_Deterministic_Prefix_Choice Multi_Non_Deterministic_Prefix_Choice
    Sequential_Composition Synchronization_Product Hiding Renaming
begin 
  (*>*)

text ‹The step-laws describe the behaviour of the operators wrt. the multi-prefix choice.›

subsection ‹Deterministic Choice›

lemma Mprefix_Det_Mprefix:
  ‹(□a ∈ A → P a) □ (□b ∈ B → Q b) =
   □x ∈ (A ∪ B) → (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (cases s) (auto simp add: D_Det D_Ndet D_Mprefix)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Det D_Ndet D_Mprefix split: if_split_asm)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s) (auto simp add: F_Det F_Ndet F_Mprefix)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s) (auto simp add: F_Det F_Ndet F_Mprefix split: if_split_asm)
qed

corollary Mprefix_Un_distrib:
  ‹□a ∈ (A ∪ B) → P a = (□a ∈ A → P a) □ (□b ∈ B → P b)›
  by (simp add: Mprefix_Det_Mprefix) (rule mono_Mprefix_eq, simp)


subsection ‹Non-Deterministic Choice›

lemma Mprefix_Ndet_Mprefix :
  ‹(□a ∈ A → P a) ⊓ (□b ∈ B → Q b) =
   (□a ∈ (A - B) → P a) ⊓ (□b ∈ (B - A) → Q b) □ (□x ∈ (A ∩ B) → P x ⊓ Q x)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Ndet D_Mprefix D_Det)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs›
    and ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s; auto simp add: F_Ndet F_Det F_Mprefix D_Mprefix D_Ndet T_Ndet)+
qed



subsection ‹Sliding Choice›

lemma Mprefix_Sliding_Mprefix :
  ‹(□a∈ A → P a) ⊳ (□b ∈ B → Q b) =
   (□x ∈ (A ∪ B) → (if x ∈ A ∩ B then P x ⊓ Q x else if x ∈ A then P x else Q x)) ⊓
   (□b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b))›
  (is ‹?lhs = ?rhs›)
  ― ‹It is not so much a ``step law'' as a rewriting.›
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Sliding D_Mprefix D_Ndet split: if_split_asm)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s) (auto simp add: F_Sliding F_Mprefix F_Ndet)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (cases s) (auto simp add: F_Sliding F_Mprefix F_Ndet split: if_split_asm)
qed


corollary Mprefix_Sliding_superset_Mprefix :
  ‹(□a∈ A → P a) ⊳ (□b ∈ B → Q b) =
   □b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b)› if ‹A ⊆ B›
  ― ‹This one (with the additional assumption \<^term>‹A ⊆ B›) is a ``step law''.›
proof -
  have ‹(□a∈ A → P a) ⊳ (□b ∈ B → Q b) =
        (□b ∈ B → (if b ∈ A ∩ B then P b ⊓ Q b else if b ∈ A then P b else Q b)) ⊓
        (□b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b))›
    by (simp add: Mprefix_Sliding_Mprefix Un_absorb1 ‹A ⊆ B›)
  also have ‹(□b ∈ B → (if b ∈ A ∩ B then P b ⊓ Q b else if b ∈ A then P b else Q b)) =
              □b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b)›
    by (rule mono_Mprefix_eq) simp
  finally show ‹(□a∈ A → P a) ⊳ (□b ∈ B → Q b) =
                □b ∈ B → (if b ∈ A then P b ⊓ Q b else Q b)› by simp
qed

corollary Mprefix_Sliding_same_set_Mprefix :
  ‹(□a∈ A → P a) ⊳ (□a ∈ A → Q a) = □a ∈ A → P a ⊓ Q a›
  by (simp add: Mprefix_Sliding_superset_Mprefix)
    (rule mono_Mprefix_eq, simp)



subsection ‹Sequential Composition›

lemma Mprefix_Seq: ‹□a ∈ A → P a ❙; Q = □a ∈ A → (P a ❙; Q)›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 (□a ∈ A → P a ❙; Q) ⟹ s ∈ 𝒟 (□a ∈ A → (P a ❙; Q))› for s
    by (cases s; simp add: D_Seq D_Mprefix T_Mprefix image_iff)
      (metis event⇩p⇩t⇩i⇩c⇩k.distinct(1) hd_append list.sel(1, 3) tl_append2)
next
  show ‹s ∈ 𝒟 (□a∈A → (P a ❙; Q)) ⟹ s ∈ 𝒟 (□a ∈ A → P a ❙; Q)› for s
    by (cases s; simp add: D_Seq D_Mprefix T_Mprefix image_iff) (metis append_Cons)
next
  show ‹(s, X) ∈ ℱ (□a∈A → (P a ❙; Q)) ⟹ (s, X) ∈ ℱ (□a ∈ A → P a ❙; Q)› for s X
    apply (cases s; simp add: F_Mprefix T_Mprefix D_Mprefix F_Seq disjoint_iff image_iff)
    by blast (metis Cons_eq_appendI event⇩p⇩t⇩i⇩c⇩k.disc(1))
next
  assume same_div: ‹𝒟 (□a ∈ A → P a ❙; Q) = 𝒟 (□a ∈ A → (P a ❙; Q))›
  show ‹(s, X) ∈ ℱ (□a ∈ A → P a ❙; Q) ⟹ (s, X) ∈ ℱ (□a ∈ A → (P a ❙; Q))› for s X
    apply (simp add: F_Seq, elim disjE exE conjE)
    subgoal by (cases s; simp add: F_Mprefix image_iff F_Seq; blast)
    subgoal by (cases s; simp add: F_Mprefix T_Mprefix F_Seq image_iff)
        (metis append_self_conv2 event⇩p⇩t⇩i⇩c⇩k.simps(4) hd_append2 list.sel(1, 3) tl_append_if)
    using same_div D_F D_Seq by blast
qed



subsection ‹Hiding›

text ‹We use a context to hide the intermediate results.›

context begin

subsubsection ‹Two intermediate Results›

private lemma D_Hiding_Mprefix_dir2:
  ‹s ∈ 𝒟 (□a ∈ A → P a \ S)› if ‹s ∈ 𝒟 (□a ∈ (A - S) → (P a \ S))›
proof -
  from that obtain a s'
    where * : ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹s' ∈ 𝒟 (P a \ S)›
    by (auto simp add: D_Mprefix)
  from "*"(4) obtain t u 
    where ** : ‹ftF u› ‹tF 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 ‹tF (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)›
      unfolding 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 ‹tF (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 strict_mono_Suc_iff)
    show ‹s ∈ 𝒟 (Mprefix A P \ S)›
      unfolding D_Hiding using "**"(1) ‹?this› by blast
  qed
qed


private lemma F_Hiding_Mprefix_dir2: 
  ‹(s, X) ∈ ℱ (□a ∈ A → P a \ S)› if ‹s ≠ []› and ‹(s, X) ∈ ℱ (□a ∈ (A - S) → (P a \ S))›
proof -
  from that obtain a s'
    where * : ‹a ∈ A› ‹a ∉ S› ‹s = ev a # s'› ‹(s', X) ∈ ℱ (P a \ S)›
    by (auto simp add: F_Mprefix)
  from "*"(4) consider ‹s' ∈ 𝒟 (P a \ S)›
    | t where ‹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 ** : ‹ftF u› ‹tF 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 ‹tF (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)›
        unfolding 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 ‹tF (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) monotone_on_def T_Mprefix)
      show ‹(s, X) ∈ ℱ (Mprefix A P \ S)›
        unfolding F_Hiding using "**"(1) ‹?this› by blast
    qed
  next
    fix t assume ** : ‹s' = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (P a)›
    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)›
      unfolding F_Hiding using ‹?this› by blast
  qed
qed



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

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 * : ‹ftF u› ‹tF 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 (simp add: D_Mprefix) (metis disjoint_iff disjoint)
    have ‹ftF u ∧ tF 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_iff 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 disjoint_iff list.sel(1) 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 ‹tF 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)
      using "*"(2) tickFree_Cons_iff apply blast
      apply (meson "**"(1) "****" less_tail strict_mono_Suc_iff)
      using "**"(1) apply (simp add: T_Mprefix "****") 
      apply (metis "****" event⇩p⇩t⇩i⇩c⇩k.inject(1) list.sel(1, 3))
      apply (subst (1 2) list.collapse[OF "****"[THEN conjunct1], symmetric])
      apply (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 where ‹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
    fix t assume * : ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
    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⇩p⇩t⇩i⇩c⇩k.inject(1) filter.simps(1) imageE)
    by (simp add: Diff_triv F_Hiding_Mprefix_dir2)
qed



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

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 * : ‹ftF u› ‹tF 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 (auto simp add: D_Mprefix) 
    have ‹tF 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 (auto simp add: T_Mprefix)
      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 (meson strict_prefixE')
        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⇩p⇩t⇩i⇩c⇩k.inject(1)
            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 (auto simp add: T_Mprefix)
        thus ‹(if i = 0 ∧ t = [] then [] else tl (f (Suc i))) ∈ 𝒯 (P a)› by simp
      qed
      hence ****** :
        ‹ftF u ∧ tF (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)
        apply (use "*"(1) in blast)
        apply (metis "*"(2) tickFree_tl)
        apply (metis "*"(3) "**"(1) ‹f 0 = []› ‹t = f k› empty_filter_conv
            filter.simps(1) list.sel(2) list.set_sel(2))
        apply (simp add: monotone_on_def,
            metis "**"(1) strict_prefix_simps(1) Suc_less_eq less_tail
            nil_le nless_le not_less_less_Suc_eq strict_monoD)
        apply blast
        apply (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 (auto simp add: T_Mprefix)
      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 (meson strict_prefixE')
        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 ‹tF (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)
          apply (metis "*"(2) tickFree_tl)
          apply (cases t; simp; metis "****" ‹a ∈ S› ‹t = f k› image_iff list.sel(1))
          apply (meson "**"(1) "****" less_tail strict_mono_Suc_iff)
          using "**"(1) apply (simp add: T_Mprefix "****")
          apply (metis "****" event⇩p⇩t⇩i⇩c⇩k.inject(1) list.sel(1, 3))
          apply (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 ‹tF (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)
          apply (metis "*"(2) tickFree_tl)
          apply (meson "**"(1) "****" less_tail strict_mono_Suc_iff)
          using "**"(1) apply (simp add: T_Mprefix "****")
          apply (metis "****" event⇩p⇩t⇩i⇩c⇩k.inject(1) list.sel(1, 3))
          apply (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 (auto simp add: D_GlobalNdet)
    from "*"(3) obtain t u 
      where ** : ‹ftF u› ‹tF 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 $ : ‹tF (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 $ : ‹tF (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) 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 where ‹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
    fix t assume * : ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (Mprefix A P)›
    from "*"(2) consider ‹t = []› ‹(X ∪ ev ` S) ∩ ev ` A = {}›
      | a t' where ‹a ∈ A› ‹t = ev a # t'› ‹(t', X ∪ ev ` S) ∈ ℱ (P a)›
      by (auto simp add: F_Mprefix)
    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
      fix a t' assume ** : ‹a ∈ A› ‹t = ev a # t'› ‹(t', X ∪ ev ` S) ∈ ℱ (P a)›
      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 where ‹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 ** : ‹ftF u› ‹tF 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 $ : ‹tF (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 $ : ‹tF (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›] monotone_on_def) blast
        show ‹(s, X) ∈ ℱ ?lhs›
          apply (simp add: F_Hiding)
          using "$" "**"(1) by blast
      qed
    next
      fix t assume ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (P a)›
      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

end



subsection ‹Synchronization›

lemma Mprefix_Sync_Mprefix_bis :
  ‹Mprefix (A ∪ A') P ⟦S⟧ Mprefix (B ∪ B') Q =
     (□a∈A → (P a ⟦S⟧ Mprefix (B ∪ B') Q))
   □ (□b∈B → (Mprefix (A ∪ A') P ⟦S⟧ Q b))
   □ (□x∈(A' ∩ B') → (P x ⟦S⟧ Q x))›
  (is ‹?lhs A A' P B B' Q = ?rhs A A' P B B' Q›) 
  if sets_assms: ‹A ∩ S = {}› ‹A' ⊆ S› ‹B ∩ S = {}› ‹B' ⊆ S›
  for P Q :: ‹'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (subst Process_eq_spec_optimized, safe)
  fix s X
  assume ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)›
    and same_div : ‹𝒟 (?lhs A A' P B B' Q) = 𝒟 (?rhs A A' P B B' Q)›
  from this(1) consider (fail) s_P s_Q X_P X_Q
    where ‹(s_P, X_P) ∈ ℱ (Mprefix (A ∪ A') P)› ‹(s_Q, X_Q) ∈ ℱ (Mprefix (B ∪ B') Q)›
      ‹s setinterleaves ((s_P, s_Q), range tick ∪ (ev ` S))›
      ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ (ev ` S)) ∪ X_P ∩ X_Q›
    | ‹s ∈ 𝒟 (?lhs A A' P B B' Q)›
    by (simp add: F_Sync D_Sync) blast
  thus ‹(s, X) ∈ ℱ (?rhs A A' P B B' Q)›
  proof cases
    case fail
    show ‹(s, X) ∈ ℱ (?rhs A A' P B B' Q)›
    proof (cases ‹∃r. s = [] ∨ hd s = tick r›)
      case True
      with fail(1, 2, 3) have ** : ‹s = [] ∧ s_P = [] ∧ s_Q = []›
        by (cases s_P; cases s_Q; force simp add: F_Mprefix subset_iff split: if_split_asm)
      with fail(1, 2, 4) sets_assms(1, 3) show ‹(s, X) ∈ ℱ (?rhs A A' P B B' Q)›
        by (auto simp add: subset_iff F_Det D_Det T_Det F_Mprefix image_Un)
    next
      case False
      then obtain e where *** : ‹s ≠ []› ‹hd s = ev e› by (meson event⇩p⇩t⇩i⇩c⇩k.exhaust)
      from fail(1, 2, 3) *** sets_assms consider
        ‹e ∈ A ∧ s_P ≠ [] ∧ hd s_P = ev e ∧ (tl s_P, X_P) ∈ ℱ (P e) ∧ 
         tl s setinterleaves ((tl s_P, s_Q), range tick ∪ (ev ` S))› | 
        ‹e ∈ B ∧ s_Q ≠ [] ∧ hd s_Q = ev e ∧ (tl s_Q, X_Q) ∈ ℱ (Q e) ∧ 
         tl s setinterleaves ((s_P, tl s_Q), range tick ∪ (ev ` S))› | 
        ‹e ∈ A' ∧ e ∈ B' ∧ s_P ≠ [] ∧ s_Q ≠ [] ∧ hd s_P = ev e ∧ hd s_Q = ev e ∧ (tl s_P, X_P) ∈ ℱ (P e) ∧ 
         (tl s_Q, X_Q) ∈ ℱ (Q e) ∧ tl s setinterleaves ((tl s_P, tl s_Q), range tick ∪ (ev ` S))›
        by (cases s_P; cases s_Q) (simp_all add: F_Mprefix split: if_split_asm, safe, auto)
      thus ‹(s, X) ∈ ℱ (?rhs A A' P B B' Q)›
        apply cases
        apply (simp_all add: F_Det ***(1))
        apply (rule disjI1, simp add: F_Mprefix ***, simp add: F_Sync)
        apply (rule exI[of _ e], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis "***"(1) "***"(2) list.exhaust_sel)
        using fail(2, 4) apply blast
        apply (rule disjI2, rule disjI1, simp add: F_Mprefix ***, simp add: F_Sync)
        apply (rule exI[of _ e], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis "***"(1) "***"(2) list.exhaust_sel)
        using fail(1, 4) apply blast

        apply (rule disjI2, rule disjI2, simp add: F_Mprefix *** F_Sync)
        apply (rule exI[of _ e], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis "***"(1) "***"(2) list.exhaust_sel)
        using fail(4) by blast
    qed
  next
    show ‹s ∈ 𝒟 (?lhs A A' P B B' Q) ⟹ (s, X) ∈ ℱ (?rhs A A' P B B' Q)› 
      using same_div D_F by blast
  qed
next

  fix s X
  { fix P Q A A' B B'
    assume assms : ‹s ≠ []› ‹(s, X) ∈ ℱ (□x ∈ A → (P x ⟦S⟧ Mprefix (B ∪ B') Q))›
      ‹A ∩ S = {}› ‹A' ⊆ S› ‹B ∩ S = {}› ‹B' ⊆ S›
      and same_div : ‹𝒟 (?lhs A A' P B B' Q) = 𝒟 (?rhs A A' P B B' Q)›
    from assms(1, 2) obtain e 
      where * : ‹e ∈ A› ‹hd s = ev e› ‹(tl s, X) ∈ ℱ (P e ⟦S⟧ Mprefix (B ∪ B') Q)›
      by (auto simp add: F_Mprefix)
    from "*" assms(1) consider (fail) s_P s_Q X_P X_Q
      where ‹(s_P, X_P) ∈ ℱ (P e)› ‹(s_Q, X_Q) ∈ ℱ (Mprefix (B ∪ B') Q)›
        ‹tl s setinterleaves ((s_P, s_Q), range tick ∪ (ev ` S))›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ (ev ` S)) ∪ X_P ∩ X_Q›
      | ‹s ∈ 𝒟 (□x ∈ A → (P x ⟦S⟧ Mprefix (B ∪ B') Q))› 
      by (simp add: F_Sync D_Mprefix D_Sync) (metis (no_types) list.collapse)
    hence ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)›
    proof cases
      case fail
      show ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)›
        apply (simp add: F_Sync, rule disjI1)
        apply (rule exI[of _ ‹ev e # s_P›], rule exI[of _ s_Q],
            rule exI[of _ X_P], intro conjI)
        apply (simp add: F_Mprefix image_iff "*"(1) fail(1))
        apply (rule exI[of _ X_Q], simp add: fail(2, 4))
        apply (subst list.collapse[OF assms(1), symmetric])
        using "*"(1, 2) fail(3) assms(3) by (cases s_Q) auto 
    next
      assume ‹s ∈ 𝒟 (□x∈A → (P x ⟦S⟧ Mprefix (B ∪ B') Q))›
      hence ‹s ∈ 𝒟 (?lhs A A' P B B' Q)› by (simp add: same_div D_Det)
      thus ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)› using D_F by blast
    qed
  } note * = this

  { assume assms : ‹s ≠ []› ‹(s, X) ∈ ℱ (□x∈(A' ∩ B') → (P x ⟦S⟧ Q x))›
      and same_div : ‹𝒟 (?lhs A A' P B B' Q) = 𝒟 (?rhs A A' P B B' Q)›
    then obtain e where * : ‹e ∈ A'› ‹e ∈ B'› ‹hd s = ev e› ‹(tl s, X) ∈ ℱ (P e ⟦S⟧ Q e)›
      by (auto simp add: F_Mprefix)
    have inside: ‹e ∈ S› using "*"(2) that(4) by blast
    from "*" assms(1) consider (fail) s_P s_Q X_P X_Q where
      ‹(s_P, X_P) ∈ ℱ (P e)› ‹(s_Q, X_Q) ∈ ℱ (Q e)›
      ‹tl s setinterleaves ((s_P, s_Q), range tick ∪ (ev ` S))›
      ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ (ev ` S)) ∪ X_P ∩ X_Q›
    | ‹s ∈ 𝒟 (□x∈(A' ∩ B') → (P x ⟦S⟧ Q x))›
      by (simp add: F_Sync D_Mprefix D_Sync) (metis (no_types) list.collapse)
    hence ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)›
    proof cases
      case fail
      show ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)›
        apply (subst list.collapse[OF assms(1), symmetric], simp add: F_Sync "*"(3), rule disjI1)
        apply (rule exI[of _ ‹ev e # s_P›], rule exI[of _ ‹ev e # s_Q›])
        apply (rule exI[of _ X_P], intro conjI, simp add: F_Mprefix "*"(1) fail(1))
        by (rule exI[of _ X_Q]) (use fail(3) in ‹simp add: "*"(2) fail(2, 4) inside F_Mprefix›)
    next
      assume ‹s ∈ 𝒟 (□x∈(A' ∩ B') → (P x ⟦S⟧ Q x))›
      hence ‹s ∈ 𝒟 (?lhs A A' P B B' Q)› by (simp add: same_div D_Det)
      thus ‹(s, X) ∈ ℱ (?lhs A A' P B B' Q)› using D_F by blast
    qed
  } note ** = this

  have *** : ‹X ∩ ev ` (A' ∩ B') = {} ⟹ X ∩ ev ` A = {} ⟹ X ∩ ev ` B = {} ⟹ 
              ([], X) ∈ ℱ (?lhs A A' P B B' Q)›
    apply (simp add: F_Sync, rule disjI1)
    apply (rule exI[of _ ‹[]›], rule exI[of _ ‹[]›], simp add: F_Mprefix)
    apply (rule exI[of _ ‹X - (ev ` (A' - B'))›], intro conjI, fastforce)
    apply (rule exI[of _ ‹X - (ev ` (B' - A'))›], intro conjI, fastforce)
    using sets_assms(2, 4) by auto

  assume same_div : ‹𝒟 (?lhs A A' P B B' Q) = 𝒟 (?rhs A A' P B B' Q)›
  hence same_div_sym : ‹𝒟 (?lhs B B' Q A A' P) = 𝒟 (?rhs B B' Q A A' P)›
    by (subst Sync_commute, subst Int_commute, subst Det_commute, simp add: Sync_commute)
  show ‹(s, X) ∈ ℱ (?rhs A A' P B B' Q) ⟹ (s, X) ∈ ℱ (?lhs A A' P B B' Q)›
    apply (unfold F_Det, safe, simp_all)
    apply (rule "***"; simp add: F_Mprefix)
    apply (rule "*"; simp add: sets_assms same_div)
    apply (subst (asm) Sync_commute, subst Sync_commute)
    apply (rule "*"; simp add: sets_assms same_div_sym)
    apply (erule "**", assumption, rule same_div)
    apply (simp add: D_Mprefix D_Det)[1]
    by (simp add: T_Mprefix T_Det)
next

  { fix s t u r v and P Q :: ‹'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and A A' B B'
    assume assms : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v› 
      ‹r setinterleaves ((t, u), range tick ∪ (ev ` S))› 
      ‹t ∈ 𝒟 (Mprefix (A ∪ A') P)› ‹u ∈ 𝒯 (Mprefix (B ∪ B') Q)›
      ‹A ∩ S = {}› ‹A' ⊆ S› ‹B ∩ S = {}› ‹B' ⊆ S›
    from assms(5) obtain e where * : ‹t ≠ []› ‹hd t = ev e› ‹tl t ∈ 𝒟 (P e)› ‹e ∈ A ∨ e ∈ A'›
      by (force simp add: D_Mprefix)
    have nonNil: ‹r ≠ [] ∧ s ≠ []›
      using *(1) assms(3, 4) empty_setinterleaving by blast
    have ‹s ∈ 𝒟 (?rhs A A' P B B' Q)›
    proof (cases ‹u = []›)
      case True
      hence ‹hd s = ev e› by (metis "*"(2) EmptyLeftSync setinterleaving_sym assms(3, 4) hd_append nonNil)
      also from "*"(1, 2, 4) setinterleaving_sym assms(4, 8)[simplified True] have ‹e ∈ A› 
        using emptyLeftNonSync hd_in_set by fastforce
      ultimately show ‹s ∈ 𝒟 (?rhs A A' P B B' Q)›
        apply (simp add: D_Det)
        apply (rule disjI1, simp add: D_Mprefix nonNil D_Sync)
        apply (rule exI[of _ e], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis list.collapse nonNil)
        apply (rule exI[of _ ‹tl t›], rule exI[of _ ‹[]›],
            rule exI[of _ ‹tl r›], rule exI[of _ v])
        apply (auto simp add: assms(1, 3, 6)[simplified True] * nonNil)[1]
        apply (metis assms(2) tickFree_tl)
        using setinterleaving_sym SyncTlEmpty True assms(4) by blast
    next
      case False
      with assms(6) obtain e' where ** : ‹hd u = ev e'› ‹tl u ∈ 𝒯 (Q e')› ‹e' ∈ B ∨ e' ∈ B'›
        by (auto simp add: T_Mprefix)
      consider ‹e  ∈ A ∧ hd s = ev e  ∧ tl r setinterleaves ((tl t, u), range tick ∪ ev ` S)› | 
        ‹e' ∈ B ∧ hd s = ev e' ∧ tl r setinterleaves ((t, tl u), range tick ∪ ev ` S)› | 
        ‹e = e' ∧ e ∈ A' ∧ e ∈ B' ∧ hd s = ev e ∧ 
                tl r setinterleaves ((tl t, tl u), range tick ∪ ev ` S)›
        using assms(4) 
        apply (subst (asm) list.collapse[OF nonNil[THEN conjunct1], symmetric],
            subst (asm) list.collapse[OF *(1), symmetric, simplified *(2)],
            subst (asm) list.collapse[OF False, symmetric, simplified **(1)])
        apply (simp add: assms(3) nonNil image_iff split: if_split_asm)
        apply (metis (no_types, opaque_lifting) *(4) **(3) Int_iff 
            assms(7, 9) empty_iff list.sel(1, 3))
        apply (metis (no_types, opaque_lifting) *(1, 2) **(3) Int_iff 
            assms(10) inf.order_iff list.exhaust_sel list.sel(1, 3))
        apply (metis (no_types, opaque_lifting) *(1, 2, 4) **(1, 3) Int_iff
            False assms(8, 10) inf.order_iff list.exhaust_sel list.sel(1, 3))
        by (metis (no_types, opaque_lifting) *(4) **(1) False assms(8) 
            list.collapse list.sel(1, 3) subsetD)
      thus ‹s ∈ 𝒟 (?rhs A A' P B B' Q)›
        apply cases
        apply (simp_all add: D_Det)
        apply (rule disjI1, simp add: D_Mprefix nonNil D_Sync)
        apply (rule exI[of _ e], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis list.exhaust_sel nonNil)
        apply (rule exI[of _ ‹tl t›], rule exI[of _ u],
            rule exI[of _ ‹tl r›], rule exI[of _ v])
        apply (simp add: assms(1, 3, 6) *(3) nonNil, use assms(2) nonNil tickFree_tl in blast)
        apply (rule disjI2, rule disjI1, simp add: D_Mprefix nonNil D_Sync)
        apply (rule exI[of _ e'], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis list.exhaust_sel nonNil)
        apply (rule exI[of _ t], rule exI[of _ ‹tl u›],
            rule exI[of _ ‹tl r›], rule exI[of _ v])
        apply (metis "*" "**"(2) assms(1, 2, 3) list.exhaust_sel nonNil tickFree_tl tl_append2)
        apply (rule disjI2, rule disjI2, auto simp add: D_Mprefix nonNil image_iff)
        apply (simp add: D_Sync)
        apply (rule exI[of _ e'], rule exI[of _ ‹tl s›], simp, intro conjI)
        apply (metis list.collapse nonNil)
        apply (rule exI[of _ ‹tl t›], rule exI[of _ ‹tl u›],
            rule exI[of _ ‹tl r›], rule exI[of _ v])
        by (use *(3) **(2) assms(1, 2, 3) nonNil tickFree_tl in ‹auto simp add: nonNil›)
    qed
  } note * = this

  fix s
  assume ‹s ∈ 𝒟 (?lhs A A' P B B' Q)›
  then obtain t u r v
    where ** : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v› 
      ‹r setinterleaves ((t, u), range tick ∪ ev ` S)› 
      ‹t ∈ 𝒟 (Mprefix (A ∪ A') P) ∧ u ∈ 𝒯 (Mprefix (B ∪ B') Q) ∨
                t ∈ 𝒟 (Mprefix (B ∪ B') Q) ∧ u ∈ 𝒯 (Mprefix (A ∪ A') P)› 
    by (simp add: D_Sync) blast
  have same_div : ‹𝒟 (?rhs A A' P B B' Q) = 𝒟 (?rhs B B' Q A A' P)›
    by (subst Det_commute, subst Int_commute, simp add: Sync_commute)
  from **(5) show ‹s ∈ 𝒟 (?rhs A A' P B B' Q)›
    apply (rule disjE)
    by (rule *[OF **(1, 2, 3, 4)]; simp add: sets_assms)
      (subst same_div, rule *[OF **(1, 2, 3, 4)]; simp add: sets_assms)
next

  { fix A A' B B' P Q s
    assume set_assm : ‹A ∩ S = {}›
    have ‹s ∈ 𝒟 (?lhs A A' P B B' Q)› if ‹s ∈ 𝒟 (□x∈A → (P x ⟦S⟧ Mprefix (B ∪ B') Q))›
    proof -
      from that obtain e s' where assms: ‹s = ev e # s'› ‹e ∈ A› ‹s' ∈ 𝒟 (P e ⟦S⟧ Mprefix (B ∪ B') Q)›
        by (simp add: D_Mprefix) blast
      from assms(3) obtain t u r v 
        where * : ‹ftF v› ‹tF r ∨ v = []› ‹s' = r @ v›
          ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
          ‹t ∈ 𝒟 (P e) ∧ u ∈ 𝒯 (Mprefix (B ∪ B') Q) ∨ 
                   t ∈ 𝒟 (Mprefix (B ∪ B') Q) ∧ u ∈ 𝒯 (P e)› by (simp add: D_Sync) blast
      have notin: ‹e ∉ S› using assms(2) set_assm by blast
      show ‹s ∈ 𝒟 (?lhs A A' P B B' Q)›
        apply (simp add: assms(1) D_Sync)
        using *(5) apply (elim disjE)

        apply (rule exI[of _ ‹ev e # t›], rule exI[of _ u], 
            rule exI[of _ ‹ev e # r›], rule exI[of _ v])
        apply (simp add: *(1, 2, 3, 4))
        apply (cases u; simp add: notin image_iff T_Mprefix D_Mprefix)
        using "*"(4) assms(2) apply (blast+)[2]

        apply (rule exI[of _ t], rule exI[of _ ‹ev e # u›],
            rule exI[of _ ‹ev e # r›], rule exI[of _ v])
        apply (simp add: *(1, 2, 3, 4))
        apply (cases t; simp add: notin image_iff T_Mprefix D_Mprefix)
        using "*"(4) assms(2) by blast
    qed
  } note * = this

  show ‹s ∈ 𝒟 (?rhs A A' P B B' Q) ⟹ s ∈ 𝒟 (?lhs A A' P B B' Q)› for s
    apply (simp add: D_Det)
    apply (erule disjE, rule *, simp_all add: sets_assms(1))
    apply (erule disjE, subst Sync_commute, rule *, simp_all add: sets_assms(3) Sync_commute)
    subgoal
    proof -
      assume ‹s ∈ 𝒟 (□x ∈ (A' ∩ B') → (P x ⟦S⟧ Q x))›
      then obtain e t u r v
        where * : ‹e ∈ A'› ‹e ∈ B'› ‹s ≠ []› ‹hd s = ev e› ‹ftF v› ‹tF r ∨ v = []›
          ‹tl s = r @ v› ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
          ‹t ∈ 𝒟 (P e) ∧ u ∈ 𝒯 (Q e) ∨ t ∈ 𝒟 (Q e) ∧ u ∈ 𝒯 (P e)› 
        by (simp add: D_Mprefix D_Sync) force
      have inside: ‹e ∈ S› using *(1) sets_assms(2) by blast
      show ‹s ∈ 𝒟 (?lhs A A' P B B' Q)›
        apply (subst list.collapse[OF *(3), symmetric], simp add: D_Sync)
        apply (rule exI[of _ ‹ev e # t›], rule exI[of _ ‹ev e # u›],
            rule exI[of _ ‹ev e # r›], rule exI[of _ v])
        by (simp add: * inside D_Mprefix T_Mprefix image_iff)
    qed .
qed

corollary Mprefix_Sync_Mprefix:
  ―‹This version is easier to use.›
  ‹□a∈A → P a ⟦S⟧ □b∈B → Q b =
   (□a∈(A - S) → (P a ⟦S⟧ □b∈B → Q b)) □
   (□b∈(B - S) → (□a∈A → P a ⟦S⟧ Q b)) □
   (□x∈(A ∩ B ∩ S) → (P x ⟦S⟧ Q x))›
  by (subst Mprefix_Sync_Mprefix_bis[of ‹A - S› S ‹A ∩ S› ‹B - S› ‹B ∩ S›, simplified Un_Diff_Int])
    (simp_all add: Int_commute inf_left_commute)



subsubsection ‹Renaming›

lemma Renaming_Mprefix:
  ‹Renaming (□a ∈ A → P a) f g = 
   □y ∈ f ` A → ⊓a ∈ {x ∈ A. y = f x}. Renaming (P a) f g› (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)
      (use list.map_sel(2) tickFree_tl in blast)
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then obtain a s' where * : ‹a ∈ A› ‹s = map_event⇩p⇩t⇩i⇩c⇩k f g (ev a) # s'›
    ‹s' ∈ 𝒟 (Renaming (P a) f g)›
    by (auto simp add: D_Mprefix D_GlobalNdet split: if_split_asm)
  from "*"(3) obtain s1 s2 
    where ** : ‹tF s1› ‹ftF s2› 
      ‹s' = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 (P a)›
    by (simp add: D_Renaming) blast
  have *** : ‹tF (ev a # s1) ∧ 
              s = map_event⇩p⇩t⇩i⇩c⇩k f g (ev a) # map (map_event⇩p⇩t⇩i⇩c⇩k f g) 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 where ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Mprefix A P)› ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) 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
    fix t assume * : ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Mprefix A P)› 
      ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t›
    show ‹(s, X) ∈ ℱ ?rhs›
    proof (cases ‹t = []›)
      from "*" show ‹t = [] ⟹ (s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Mprefix disjoint_iff_not_equal)
    next
      assume ‹t ≠ []›
      with "*"(1) obtain a t'
        where ** : ‹a ∈ A› ‹t = ev a # t'› ‹(t', map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P a)›
        by (auto simp add: F_Mprefix)
      have *** : ‹s ≠ [] ∧ hd s ∈ ev ` f ` A›
        using "*"(2) "**"(1, 2) by simp 
      with "**" have ‹ev (f a) = hd s ∧ 
                     (tl s, X) ∈ ℱ (⊓a ∈ {x ∈ A. f a = f x}. Renaming (P a) f g)›
        by (auto simp add: F_GlobalNdet "*"(2) F_Renaming)
      with "***" show ‹(s, X) ∈ ℱ ?rhs›
        by (simp add: F_Mprefix image_iff) (metis (no_types, lifting) "**"(1) list.collapse)
    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 (auto simp add: F_Mprefix F_Renaming)
  next
    fix b s'
    assume ‹s = b # s'› ‹(s, X) ∈ ℱ ?rhs›
    then obtain a
      where * : ‹a ∈ A› ‹s = (map_event⇩p⇩t⇩i⇩c⇩k f g) (ev a) # s'› (* ‹b = ev (f a)› *)
        ‹(s', X) ∈ ℱ (⊓a ∈ {x ∈ A. f a = f x}. Renaming (P a) f g)›
      by (auto simp add: F_Mprefix)
    from "*"(1, 3) obtain a'
      where ** : ‹a' ∈ A› ‹f a' = f a› ‹(s', X) ∈ ℱ (Renaming (P a') f g)›
      by (auto simp add: F_GlobalNdet split: if_split_asm)
    from "**"(3) consider 
      t where ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P a')› ‹s' = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t›
    | s1 s2 where ‹tF s1› ‹ftF s2›
      ‹s' = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 (P a')›
      by (simp add: F_Renaming) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      fix t assume *** : ‹(t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P a')›
        ‹s' = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t›
      have **** : ‹(ev a' # t, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (Mprefix A P) ∧ 
                   s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) (ev a' # t)›
        by (auto simp add: F_Mprefix "*"(2) "**"(1, 2) "***"(1, 2))
      with "****" show ‹(s, X) ∈ ℱ ?lhs› by (auto simp add: F_Renaming)
    next
      fix s1 s2 assume *** : ‹tF s1› ‹ftF s2› 
        ‹s' = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s1 ∈ 𝒟 (P a')›
      have ‹tF (ev a' # s1) ∧ 
            s = map_event⇩p⇩t⇩i⇩c⇩k f g (ev a') # map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2 ∧ 
            ev a' # s1 ∈ 𝒟 (Mprefix A P)›
        by (auto simp add: "*"(2) "**"(1, 2) "***" D_Mprefix) 
      with "***"(2) show ‹(s, X) ∈ ℱ ?lhs› by (auto simp add: F_Renaming)
    qed
  qed
qed


(*<*)
end
  (*>*)