Theory NewLaws

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

chapter‹ Bonus: powerful new Laws ›

theory  NewLaws
  imports Interrupt Sliding Throw
begin

section ‹Powerful Results about constRenaming

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

subsection ‹Some Generalizations›

text ‹For constRenaming, we can obtain generalizations of the following results:

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

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


lemma Renaming_Mprefix_Sliding:
  Renaming ((a  A  P a)  Q) f = 
   (y  f ` A  a  {x  A. y = f x}. Renaming (P a) f)  Renaming Q f
  unfolding Sliding_def
  by (simp add: Renaming_Ndet Renaming_Det Renaming_Mprefix)


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


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



subsection constRenaming and constHiding

text ‹When termf is one to one, termRenaming (P \ S) f will behave like we expect it to do.›

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


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

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

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


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

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



subsection constRenaming and constSync

text ‹Idem for the synchronization: when termf is one to one, 
      termRenaming (P S Q) will behave as expected.›

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


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


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

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

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

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


section constHiding and constMprefix

text ‹We already have a way to distribute the constHiding operator on the
      constMprefix operator with @{thm Hiding_Mprefix_distr[of S A]}.
      But this is only usable when termA  S = {}. With the constSliding
      operator, we can now handle the case termA  S  {}.›


subsection ‹Two intermediate Results›

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


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



subsection constHiding and constMprefix for disjoint Sets›

text ‹Now we can give a more readable proof of the following result 
      (already proven in theoryHOL-CSP.CSP_Laws).›

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


text ‹And we obtain a similar result when adding a constSliding in the expression.›

theorem Hiding_Mprefix_Sliding_disjoint:
  ((a  A  P a)  Q) \ S = (a  A  (P a \ S))  (Q \ S)
  if disjoint: A  S = {}
proof (subst Hiding_Mprefix_disjoint[OF disjoint, symmetric])
  show ((a  A  P a)  Q) \ S = (a  A  P a \ S)  (Q \ S)
   (is ?lhs = ?rhs)
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume s  𝒟 ?lhs
    hence s  𝒟 (Mprefix A P  Q \ S)
      by (simp add: D_Hiding D_Sliding D_Ndet T_Sliding T_Ndet)
    thus s  𝒟 ?rhs
      by (rule set_rev_mp)
         (simp add: D_Ndet D_Sliding Hiding_Ndet subsetI)
  next
    fix s
    assume s  𝒟 ?rhs
    hence s  𝒟 (Q \ S)  s  𝒟 (a  A  P a \ S)
      by (simp add: Hiding_Mprefix_disjoint[OF disjoint]
                    D_Ndet D_Sliding) blast
    thus s  𝒟 ?lhs
      by (auto simp add: D_Hiding D_Sliding T_Sliding)
  next
    fix s X
    assume same_div : 𝒟 ?lhs = 𝒟 ?rhs
    assume (s, X)   ?lhs
    then consider s  𝒟 ?lhs
      |t. s = trace_hide t (ev ` S)  (t, X  ev ` S)   (Mprefix A P  Q)
      by (simp add: F_Hiding D_Hiding) blast
    thus (s, X)   ?rhs
    proof cases
      from same_div D_F show s  𝒟 ?lhs  (s, X)   ?rhs by blast
    next
      assume t. s = trace_hide t (ev ` S) 
                  (t, X  ev ` S)   (Mprefix A P  Q)
      then obtain t
        where * : s = trace_hide t (ev ` S)
                  (t, X  ev ` S)   (Mprefix A P  Q) by blast
      from "*"(2) consider (t, X  ev ` S)   Q
        | t  [] (t, X  ev ` S)   (Mprefix A P)
        by (simp add: F_Sliding D_Mprefix) blast
      thus (s, X)   ?rhs
      proof cases
        have (t, X  ev ` S)   Q  (s, X)   (Q \ S)
          by (auto simp add: F_Hiding "*"(1))
        thus (t, X  ev ` S)   Q  (s, X)   ?rhs
          by (simp add: F_Ndet F_Sliding "*"(1))
      next
        assume assms : t  [] (t, X  ev ` S)   (Mprefix A P)
        with disjoint have trace_hide t (ev ` S)  []
          by (cases t, auto simp add: F_Mprefix)
        also have (s, X)   (Mprefix A P \ S)
          using assms by (auto simp: F_Hiding "*"(1))
        ultimately show (s, X)   ?rhs
          by (simp add: F_Sliding "*"(1))
      qed
    qed
  next
    have * : t  𝒯 (Mprefix A P)  trace_hide t (ev ` S) = []  t = [] for t
      using disjoint by (cases t, auto simp add: T_Mprefix)
    have ** : []  𝒟 (Mprefix A P \ S)
      apply (rule ccontr, simp add: D_Hiding)
      by (metis (mono_tags, lifting) "*" NT_ND Nil_Nin_D_Mprefix  
                UNIV_I f_inv_into_f lessI nless_le strict_mono_on_eqD)
    fix s X
    assume same_div : 𝒟 ?lhs = 𝒟 ?rhs
    assume (s, X)   ?rhs
    with ** consider (s, X)   (Q \ S)
      | s  [] (s, X)   (Mprefix A P \ S)
      by (simp add: Hiding_Mprefix_disjoint[OF disjoint] F_Sliding D_Mprefix) blast
    thus (s, X)   ?lhs
    proof cases
      assume (s, X)   (Q \ S)
      then consider s  𝒟 (Q \ S)
        | t. s = trace_hide t (ev ` S)  (t, X  ev ` S)   Q
        by (simp add: F_Hiding D_Hiding) blast
      thus (s, X)   ?lhs
      proof cases
        assume s  𝒟 (Q \ S)
        hence s  𝒟 ?rhs by (simp add: D_Ndet D_Sliding)
        with same_div D_F show (s, X)   ?lhs by blast
      next
        assume t. s = trace_hide t (ev ` S)  (t, X  ev ` S)   Q
        thus (s, X)   ?lhs
          by (simp add: F_Hiding F_Sliding) blast
      qed
    next
      assume assms : s  [] (s, X)   (Mprefix A P \ S)
      then consider s  𝒟 (Mprefix A P \ S)
        | t. t  []  s = trace_hide t (ev ` S)  (t, X  ev ` S)   (Mprefix A P)
        by (simp add: F_Hiding D_Hiding) (metis filter.simps(1))
      thus (s, X)   ?lhs
      proof cases
        assume s  𝒟 (Mprefix A P \ S)
        hence s  𝒟 ?rhs by (simp add: D_Ndet D_Sliding)
        with same_div D_F show (s, X)   ?lhs by blast
      next
        show t. t  []  s = trace_hide t (ev ` S) 
                  (t, X  ev ` S)   (Mprefix A P)  (s, X)   ?lhs
          by (auto simp add: F_Sliding F_Hiding)
      qed
    qed
  qed
qed




subsection constHiding and constMprefix for non-disjoint Sets›

text ‹Finally the new version, when termA  S  {}.›

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

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


text ‹And we obtain a similar result when adding a constSliding in the expression.›

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


section constSliding behaviour›

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

lemma Mprefix_Sliding_Mprefix_Sliding:
  (a  A  P a)  (b  B  Q b)  R =
   ( x  A  B  (if x  A  B then P x  Q x else if x  A then P x else Q x))  R
  (is (a  A  P a)  (b  B  Q b)  R = ?term  R)
proof (subst Sliding_def, subst Mprefix_Det_distr)
  have Mprefix B Q  (Mprefix A P  Mprefix B Q)  R = Mprefix A P  Mprefix B Q  R
    by (metis Det_STOP Ndet_commute Ndet_distrib Sliding_STOP_Det Sliding_assoc Sliding_def) 
  thus ?term  Mprefix B Q  R = ?term  R
    by (simp add: Mprefix_Det_distr Ndet_commute)
qed


lemma Mprefix_Sliding_Seq: 
  ((a  A  P a)  P') ; Q = (a  A  P a ; Q)  (P' ; Q)
proof (subst Mprefix_Seq[symmetric])
  show ((a  A  P a)  P') ; Q = 
        ((a  A  P a) ; Q)  (P' ; Q) (is ?lhs = ?rhs)
  proof (subst Process_eq_spec, safe)
    show s  𝒟 ?lhs  s  𝒟 ?rhs for s
      by (auto simp add: D_Sliding D_Seq T_Sliding)
  next
    show s  𝒟 ?rhs  s  𝒟 ?lhs for s
      by (auto simp add: D_Sliding D_Seq T_Sliding)
  next
    show (s, X)   ?lhs  (s, X)   ?rhs for s X
      apply (simp add: F_Seq, elim disjE exE)
        apply (solves auto simp add: F_Sliding F_Seq D_Mprefix)
       apply (solves auto simp add: F_Sliding T_Sliding F_Seq)
      by (solves auto simp add: D_Sliding D_Seq F_Sliding F_Seq)
  next
    show (s, X)   ?rhs  (s, X)   ?lhs for s X
      apply (simp add: F_Sliding, elim disjE)
        apply (solves auto simp add: F_Seq D_Sliding F_Sliding T_Sliding)
       apply (solves auto simp add: F_Seq D_Sliding F_Sliding T_Sliding)
      by (simp add: D_Seq D_Mprefix T_Seq T_Mprefix)
         (metis append_is_Nil_conv event.simps(3) hd_append list.sel(1))
  qed
qed



lemma Throw_Sliding :
  (a  A  P a)  P' Θ b  B. Q b = 
   (a  A  (if a  B then Q a else (P a Θ b  B. Q b)))  (P' Θ b  B. Q b)
  (is ?lhs = ?rhs)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume s  𝒟 ?lhs
  then consider t1 t2. s = t1 @ t2  t1  𝒟 (Mprefix A P  P') 
                         tickFree t1  set t1  ev ` B = {}  front_tickFree t2
    | t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P  P') 
                 set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
    by (simp add: D_Throw) blast
  thus s  𝒟 ?rhs
  proof cases
    assume t1 t2. s = t1 @ t2  t1  𝒟 (Mprefix A P  P') 
                    tickFree t1  set t1  ev ` B = {}  front_tickFree t2
    then obtain t1 t2
      where * : s = t1 @ t2 t1  𝒟 (Mprefix A P  P') tickFree t1
                set t1  ev ` B = {} front_tickFree t2 by blast
    from "*"(2) consider t1  𝒟 (Mprefix A P) | t1  𝒟 P'
      by (simp add: D_Sliding) blast
    thus s  𝒟 ?rhs
    proof cases
      assume t1  𝒟 (Mprefix A P)
      then obtain a t1' where t1 = ev a # t1' a  A t1'  𝒟 (P a)
        by (simp add: D_Mprefix image_iff)
           (metis event.inject list.collapse)
      with "*"(1, 3, 4, 5) show s  𝒟 ?rhs
        by (simp add: D_Sliding D_Mprefix D_Throw) (metis image_eqI)
    next
      from "*"(1, 3, 4, 5)  show t1  𝒟 P'  s  𝒟 ?rhs
        by (simp add: D_Sliding D_Throw) blast
    qed
  next
    assume t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P  P') 
                      set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
    then obtain t1 b t2
      where * : s = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (Mprefix A P  P')
                set t1  ev ` B = {} b  B t2  𝒟 (Q b) by blast
    from "*"(2) consider t1 @ [ev b]  𝒯 (Mprefix A P) | t1 @ [ev b]  𝒯 P'
      by (simp add: T_Sliding) blast
    thus s  𝒟 ?rhs
    proof cases
      assume t1 @ [ev b]  𝒯 (Mprefix A P)
      then obtain a t1'
        where t1 @ [ev b] = ev a # t1' a  A t1'  𝒯 (P a)
        by (simp add: T_Mprefix)
           (metis list.exhaust_sel snoc_eq_iff_butlast)
      with "*"(1, 3, 4, 5) show s  𝒟 ?rhs
        by (cases t1; simp add: "*"(1) D_Sliding D_Mprefix D_Throw)
           (metis image_eqI)
    next
      from "*"(1, 3, 4, 5) show t1 @ [ev b]  𝒯 P'  s  𝒟 ?rhs
        by (simp add: D_Sliding D_Mprefix D_Throw) blast
    qed
  qed
next
  fix s
  assume s  𝒟 ?rhs
  then consider s  𝒟 (Throw P' B Q)
    | s  𝒟 (aA  (if a  B then Q a else Throw (P a) B Q))
    by (simp add: D_Sliding) blast
  thus s  𝒟 ?lhs
  proof cases
    show s  𝒟 (Throw P' B Q)  s  𝒟 ?lhs
      by (simp add: D_Throw D_Sliding T_Sliding) blast
  next
    assume s  𝒟 (aA  (if a  B then Q a else Throw (P a) B Q))
    then obtain a s' 
      where * : s = ev a # s' a  A
                s'  𝒟 (if a  B then Q a else Throw (P a) B Q)
      by (cases s; simp add: D_Mprefix) blast
    show s  𝒟 ?lhs
    proof (cases a  B)
      from "*" show a  B  s  𝒟 ?lhs
        by (simp add: D_Throw T_Sliding T_Mprefix disjoint_iff)
           (metis Nil_elem_T emptyE empty_set list.sel(1, 3) self_append_conv2)
    next
      assume a  B
      with "*"(3) consider 
        t1 t2. s' = t1 @ t2  t1  𝒟 (P a)  tickFree t1 
                 set t1  ev ` B = {}  front_tickFree t2
        | t1 b t2. s' = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a) 
                     set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
        by (simp add: D_Throw) blast
      thus s  𝒟 ?lhs
      proof cases
        assume t1 t2. s' = t1 @ t2  t1  𝒟 (P a)  tickFree t1 
                        set t1  ev ` B = {}  front_tickFree t2
        then obtain t1 t2
          where ** : s' = t1 @ t2 t1  𝒟 (P a) tickFree t1
                     set t1  ev ` B = {} front_tickFree t2
          by blast
        have *** : s = (ev a # t1) @ t2  set (ev a # t1)  ev ` B = {}
          by (simp add: "*"(1) "**"(1, 4) image_iff a  B)
        from "*" "**"(1, 2, 3, 5) show s  𝒟 ?lhs
          by (simp add: D_Throw D_Sliding D_Mprefix image_iff)
             (metis "***" event.distinct(1) list.discI list.sel(1, 3) tickFree_Cons)
      next
        assume t1 b t2. s' = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a) 
                          set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
        then obtain t1 b t2
          where ** : s' = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (P a)
                     set t1  ev ` B = {} b  B t2  𝒟 (Q b) by blast
        have *** : s = (ev a # t1 @ [ev b]) @ t2  set (ev a # t1)  ev ` B = {}
          by (simp add: "*"(1) "**"(1, 3) image_iff a  B)
        from "*" "**"(1, 2, 4, 5) show s  𝒟 ?lhs
          by (simp add: D_Throw T_Sliding T_Mprefix)
             (metis "***" Cons_eq_appendI list.sel(1, 3))
      qed
    qed
  qed
next
  fix s X
  assume same_div : 𝒟 ?lhs = 𝒟 ?rhs
  assume (s, X)   ?lhs
  then consider s  𝒟 ?lhs
    | (s, X)   (Mprefix A P  P') set s  ev ` B = {}
    | t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P  P') 
                 set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
    by (simp add: F_Throw D_Throw) blast
  thus (s, X)   ?rhs
  proof cases
    from same_div D_F show s  𝒟 ?lhs  (s, X)   ?rhs by blast
  next
    show (s, X)   (Mprefix A P  P')  set s  ev ` B = {}  (s, X)   ?rhs
      by (cases s; simp add: F_Sliding F_Mprefix F_Throw) blast
  next
    assume t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P  P') 
                      set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
    then obtain t1 b t2 
      where * : s = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (Mprefix A P  P')
                set t1  ev ` B = {} b  B (t2, X)   (Q b) by blast
    from "*"(2) consider t1 @ [ev b]  𝒯 (Mprefix A P) | t1 @ [ev b]  𝒯 P'
      by (simp add: T_Sliding) blast
    thus (s, X)   ?rhs
    proof cases
      assume t1 @ [ev b]  𝒯 (Mprefix A P)
      then obtain a t1'
        where t1 @ [ev b] = ev a # t1' a  A t1'  𝒯 (P a)
        by (simp add: T_Mprefix)
           (metis list.exhaust_sel snoc_eq_iff_butlast)
      with "*"(1, 3, 4, 5) show (s, X)   ?rhs
        by (cases t1; simp add: "*"(1) F_Sliding F_Mprefix F_Throw) blast
    next
      from "*"(1, 3, 4, 5) show t1 @ [ev b]  𝒯 P'  (s, X)   ?rhs
        by (simp add: F_Sliding F_Mprefix F_Throw) blast
    qed
  qed
next
  fix s X
  assume same_div : 𝒟 ?lhs = 𝒟 ?rhs
  assume (s, X)   ?rhs
  then consider s  𝒟 ?rhs | (s, X)   (Throw P' B Q)
    | s  [] (s, X)   (a  A  (if a  B then Q a else Throw (P a) B Q))
    by (simp add: F_Sliding D_Sliding) blast
  thus (s, X)   ?lhs
  proof cases
    from same_div D_F show s  𝒟 ?rhs  (s, X)   ?lhs by blast
  next
    show (s, X)   (Throw P' B Q)  (s, X)   ?lhs
      by (simp add: F_Throw F_Sliding D_Sliding T_Sliding) blast
  next
    assume s  [] (s, X)   (a  A  (if a  B then Q a else Throw (P a) B Q))
    then obtain a s'
      where * : s = ev a # s' a  A 
                (s', X)   (if a  B then Q a else Throw (P a) B Q)
      by (simp add: F_Mprefix image_iff) (metis event.inject list.collapse)
    show (s, X)   ?lhs
    proof (cases a  B)
      assume a  B
      have [ev a]  𝒯 (Mprefix A P  P')
        by (simp add: T_Sliding T_Mprefix "*"(2) Nil_elem_T)
        
      with "*"(1, 3) a  B show (s, X)   ?lhs
        by (simp add: F_Throw) (metis append_Nil empty_set inf_bot_left)
    next
      assume a  B
      with "*"(3) consider s'  𝒟 (Throw (P a) B Q)
        | (s', X)   (P a) set s'  ev ` B = {}
        | t1 b t2. s' = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a)  
                     set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
        by (simp add: F_Throw D_Throw) blast
      thus (s, X)   ?lhs
      proof cases
        assume s'  𝒟 (Throw (P a) B Q)
        hence s  𝒟 ?rhs by (simp add: "*"(1, 2) D_Sliding D_Mprefix a  B)
        with same_div D_F show (s, X)   ?lhs by blast
      next
        show (s', X)   (P a)  set s'  ev ` B = {}  (s, X)   ?lhs
          using "*"(1, 2) a  B by (simp add: F_Throw F_Sliding F_Mprefix) blast
      next
        assume t1 b t2. s' = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a)  
                          set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
        then obtain t1 b t2
          where ** : s' = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (P a)
                     set t1  ev ` B = {} b  B (t2, X)   (Q b) by blast
        from "**" have *** : (ev a # t1) @ [ev b]  𝒯 (Mprefix A P)  
                              set (ev a # t1)  ev ` B = {}
          by (simp add: T_Mprefix "*"(2) image_iff a  B)
        from "*"(1) "**"(1, 4, 5) "**"(5) show (s, X)   ?lhs
          by (simp add: F_Throw T_Sliding) (metis "***" Cons_eq_appendI)
      qed
    qed
  qed
qed



end