Quelle  CSPM_Laws.thy

(*<*)
―‹ ********************************************************************
 * Project : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file : Laws for architectural operators
 *
 * 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 ‹Results for Throw›
(*<*)
theory CSPM_Laws
  imports Global_Deterministic_Choice Multi_Synchronization_Product
    Multi_Sequential_Composition Interrupt Throw
begin
(*>*)


subsection ‹Laws for Throw›

lemma Throw_GlobalDet :
  ‹(◻ a ∈ A. P a) Θ b ∈ B. Q b = ◻ a ∈ A. P a Θ b ∈ B. Q b› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  show ‹t ∈ D ?lhs ==> t ∈ D ?rhs› for t
    by (simp add: D_Throw GlobalDet_projs split: if_split_asm) blast
next
  show ‹t ∈ D ?rhs ==> t ∈ D ?lhs› for t
    by (simp add: D_Throw GlobalDet_projs) (meson empty_iff)
next
  fix t X assume ‹(t, X) ∈ F ?lhs› ‹t ∉ D ?lhs›
  then consider ‹(t, X) ∈ F (◻a ∈ A. P a)› ‹set t ∩ ev ` B = {}›
    | (failR) t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ T (◻a ∈ A. P a)›
      ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ F (Q b)›
    unfolding Throw_projs by blast
  thus ‹(t, X) ∈ F ?rhs›
  proof cases
    show ‹(t, X) ∈ F (◻a ∈ A. P a) ==> set t ∩ ev ` B = {} ==> (t, X) ∈ F ?rhs›
      by (cases t) (auto simp add: F_GlobalDet Throw_projs)
  next
    case failR
    from failR(2) obtain a where ‹a ∈ A› ‹t1 @ [ev b] ∈ T (P a)›
      by (auto simp add: T_GlobalDet split: if_split_asm)
    with failR(3-5) show ‹(t, X) ∈ F ?rhs›
      by (simp add: F_GlobalDet F_Throw failR(1)) blast
  qed
next
  fix t X assume ‹(t, X) ∈ F ?rhs› ‹t ∉ D ?rhs›
  then consider ‹t = []› ‹∀a∈A. (t, X) ∈ F (P a Θ b ∈ B. Q b)›
    | a where ‹a ∈ A› ‹t ≠ []› ‹(t, X) ∈ F (P a Θ b ∈ B. Q b)›
    | a r where ‹a ∈ A› ‹t = []› ‹🍋(r) ∉ X› ‹[🍋(r)] ∈ T (P a Θ b ∈ B. Q b)›
    by (auto simp add: GlobalDet_projs)
  thus ‹(t, X) ∈ F ?lhs›
  proof cases
    show ‹t = [] ==> ∀a∈A. (t, X) ∈ F (P a Θ b ∈ B. Q b) ==> (t, X) ∈ F ?lhs›
      by (auto simp add: F_Throw F_GlobalDet)
  next
    show ‹a ∈ A ==> t ≠ [] ==> (t, X) ∈ F (P a Θ b ∈ B. Q b) ==> (t, X) ∈ F ?lhs› for a
      by (simp add: F_Throw GlobalDet_projs) (metis empty_iff)
  next
    show ‹[a ∈ A; t = []; 🍋(r) ∉ X; [🍋(r)] ∈ T (P a Θ b ∈ B. Q b)] ==> (t, X) ∈ F ?lhs› for a r
      by (simp add: Throw_projs F_GlobalDet Cons_eq_append_conv) (metis is_processT9_tick)
  qed
qed


lemma Throw_GlobalNdetR :
  ‹P Θ a ∈ A. ⊓b ∈ B. Q a b =
 (if B = {} then P Θ a ∈ A. STOP else ◻b ∈ B. P Θ a ∈ A. Q a b)›
  (is ‹?lhs = (if _ then _ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹B = {} ==> ?lhs = P Θ a ∈ A. STOP› by simp
next
  show ‹?lhs = ?rhs› if ‹B ≠ {}›
  proof (subst Process_eq_spec, safe)
    show ‹t ∈ D ?lhs ==> t ∈ D ?rhs› for t
      by (auto simp add: ‹B ≠ {}› D_Throw D_GlobalNdet D_GlobalDet)
  next
    show ‹t ∈ D ?rhs ==> t ∈ D ?lhs› for t
      by (auto simp add: ‹B ≠ {}› D_Throw D_GlobalNdet D_GlobalDet)
  next
    show ‹(t, X) ∈ F ?lhs ==> (t, X) ∈ F ?rhs› for t X
      by (cases t) (auto simp add: ‹B ≠ {}› F_Throw F_GlobalNdet F_GlobalDet)
  next
    show ‹(t, X) ∈ F ?rhs ==> (t, X) ∈ F ?lhs› for t X
      by (auto simp add: ‹B ≠ {}› Throw_projs F_GlobalNdet F_GlobalDet D_T
          is_processT7 Cons_eq_append_conv intro!: is_processT6_TR_notin)
  qed
qed


corollary Throw_Det : ‹P ◻ P' Θ a ∈ A. Q a = (P Θ a ∈ A. Q a) ◻ (P' Θ a ∈ A. Q a)›
proof -
  have ‹P ◻ P' Θ a ∈ A. Q a = (◻a∈{0 :: nat, 1}. (if a = 0 then P else P')) Θ a ∈ A. Q a›
    by (simp add: GlobalDet_distrib_unit)
  also have ‹… = ◻a∈{0 :: nat, 1}. (if a = 0 then P else P') Θ a ∈ A. Q a›
    by (fact Throw_GlobalDet)
  also have ‹… = (P Θ a ∈ A. Q a) ◻ (P' Θ a ∈ A. Q a)›
    by (simp add: GlobalDet_distrib_unit)
  finally show ?thesis .
qed

corollary Throw_NdetR : ‹P Θ a ∈ A. Q a ⊓ Q' a = (P Θ a ∈ A. Q a) ◻ (P Θ a ∈ A. Q' a)›
proof -
  have ‹P Θ a ∈ A. Q a ⊓ Q' a = P Θ a ∈ A. ⊓b ∈ {0 :: nat, 1}. (if b = 0 then Q a else Q' a)›
    by (simp add: GlobalNdet_distrib_unit)
  also have ‹… = ◻b ∈ {0 :: nat, 1}. P Θ a ∈ A. (if b = 0 then Q a else Q' a)›
    by (simp add: Throw_GlobalNdetR)
  also have ‹… = (P Θ a ∈ A. Q a) ◻ (P Θ a ∈ A. Q' a)›
    by (simp add: GlobalDet_distrib_unit)
  finally show ?thesis .
qed



subsection ‹Laws for Sync›

lemma Sync_GlobalNdet_cartprod:
  ‹(⊓ (a, b) ∈ A × B. (P a [S] Q b)) =
 (if A = {} ∨ B = {} then STOP else (⊓a ∈ A. P a) [S] (⊓b ∈ B. Q b))›  
  by (simp add: GlobalNdet_cartprod Sync_distrib_GlobalNdet_left
      Sync_distrib_GlobalNdet_right GlobalNdet_sets_commute[of A])


lemmas Inter_GlobalNdet_cartprod = Sync_GlobalNdet_cartprod[where S = ‹{}›]
  and   Par_GlobalNdet_cartprod = Sync_GlobalNdet_cartprod[where S = UNIV]



lemma MultiSync_Hiding_pseudo_distrib:
  ‹finite A ==> A ∩ S = {} ==> (\[S\] p ∈# M. (P p \ A)) = (\[S\] p ∈# M. P p) \ A›
  by (induct M, simp) (metis MultiSync_add MultiSync_rec1 Hiding_Sync)


lemma MultiSync_prefix_pseudo_distrib:
  ‹M ≠ {#} ==> a ∈ S ==> (\[S\] p ∈# M. (a → P p)) = (a → (\[S\] p ∈# M. P p))›
  by (induct M rule: mset_induct_nonempty) 
    (simp_all add: write0_Sync_write0_subset)

lemmas MultiInter_Hiding_pseudo_distrib =
  MultiSync_Hiding_pseudo_distrib[where S = ‹{}›, simplified]
  and MultiPar_prefix_pseudo_distrib =
  MultiSync_prefix_pseudo_distrib[where S = ‹UNIV›, simplified]


text ‹A result on Mndetprefix and Sync.›

lemma Mndetprefix_Sync_distr: ‹A ≠ {} ==> B ≠ {} ==>
 (⊓ a ∈ A → P a) [S] (⊓ b ∈ B → Q b) =
 ⊓ a∈A. ⊓ b∈B. (◻c ∈ ({a} - S) → (P a [S] (b → Q b))) ◻
 (◻d ∈ ({b} - S) → ((a → P a) [S] Q b)) ◻
 (◻c∈({a} ∩ {b} ∩ S) → (P a [S] Q b))›
  apply (subst (1 2) Mndetprefix_GlobalNdet) 
  apply (subst Sync_distrib_GlobalNdet_right, simp)
  apply (subst Sync_commute)
  apply (subst Sync_distrib_GlobalNdet_right, simp)
  apply (subst Sync_commute)
  apply (unfold write0_def)
  apply (subst Mprefix_Sync_Mprefix)
  by (fold write0_def, rule refl)

lemma ‹A ≠ {} ==> B ≠ {} ==> (⊓ a ∈ A → P a) [S] (⊓ b ∈ B → Q b) =
 ⊓ a∈A. ⊓ b∈B. (if a ∈ S then STOP else (a → (P a [S] (b → Q b)))) ◻
 (if b ∈ S then STOP else (b → ((a → P a) [S] Q b))) ◻
 (if a = b ∧ a ∈ S then (a → (P a [S] Q a)) else STOP)›
  apply (subst Mndetprefix_Sync_distr, assumption+)
  apply (intro mono_GlobalNdet_eq)
  apply (intro arg_cong2[where f = ‹(◻)›])
  by (simp_all add: Mprefix_singl insert_Diff_if Int_insert_left)





subsection ‹GlobalDet, GlobalNdet and write0›

lemma GlobalDet_write0_is_GlobalNdet_write0:
  ‹(◻ p ∈ A. (a → P p)) = ⊓ p ∈ A. (a → P p)› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ D ?lhs ==> s ∈ D ?rhs›
    and ‹s ∈ D ?rhs ==> s ∈ D ?lhs› for s
    by (simp_all add: D_GlobalDet write0_def D_Mprefix D_GlobalNdet)
next
  show ‹(s, X) ∈ F ?lhs ==> (s, X) ∈ F ?rhs›
    and ‹(s, X) ∈ F ?rhs ==> (s, X) ∈ F ?lhs› for s X
    by (auto simp add: F_GlobalDet write0_def F_Mprefix F_GlobalNdet split: if_split_asm)
qed    

lemma write0_GlobalNdet_bis:
  ‹A ≠ {} ==> (a → (⊓ p ∈ A. P p) = ◻ p ∈ A. (a → P p))›
  by (simp add: GlobalDet_write0_is_GlobalNdet_write0 write0_GlobalNdet)






section ‹Some Results on Renaming›

(* TODO: useful ? and rename *)
lemma Renaming_GlobalNdet:
  ‹Renaming (⊓ a ∈ A. P (f a)) f g = ⊓ b ∈ f ` A. Renaming (P b) f g›
  by (metis Renaming_distrib_GlobalNdet mono_GlobalNdet_eq2)

lemma Renaming_GlobalNdet_inj_on:
  ‹Renaming (⊓ a ∈ A. P a) f g =
 ⊓ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
  if inj_on_f: ‹inj_on f A›
  by (smt (verit, ccfv_SIG) Renaming_distrib_GlobalNdet inj_on_def mono_GlobalNdet_eq2 that the_equality)

corollary Renaming_GlobalNdet_inj:
  ‹Renaming (⊓ a ∈ A. P a) f g =
 ⊓ b ∈ f ` A. Renaming (P (THE a. f a = b)) f g› if inj_f: ‹inj f›
  apply (subst Renaming_GlobalNdet_inj_on, metis inj_eq inj_onI inj_f)
  apply (rule mono_GlobalNdet_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])


lemma Renaming_distrib_GlobalDet :
  ‹Renaming (◻a ∈ A. P a) f g = ◻a ∈ A. Renaming (P a) f g› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ D ?lhs ==> s ∈ D ?rhs›
    and ‹s ∈ D ?rhs ==> s ∈ D ?lhs› for s
    by (auto simp add: D_Renaming D_GlobalDet)
next
  assume same_div : ‹D ?lhs = D ?rhs›
  fix s X assume ‹(s, X) ∈ F ?lhs›
  then consider ‹s ∈ D ?lhs›
    | t where ‹s = map (map_event_ptick f g) t› ‹(t, map_event_ptick f g -` X) ∈ F (◻a ∈ A. P a)›
    unfolding Renaming_projs by blast
  thus ‹(s, X) ∈ F ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ D ?lhs ==> (s, X) ∈ F ?rhs› by blast
  next
    show ‹s = map (map_event<sub>ptick</sub> f g) t ==> (t, map_event<sub>ptick</sub> f g -` X) ∈ F (◻a ∈ A. P a)
 ==> (s, X) ∈ F ?rhs› for t
      by (cases t; simp add: F_GlobalDet Renaming_projs)
        (force, metis list.simps(9))
  qed
next
  assume same_div : ‹D ?lhs = D ?rhs›
  fix s X assume ‹(s, X) ∈ F ?rhs›
  then consider ‹s = []› ‹∀a∈A. (s, X) ∈ F (Renaming (P a) f g)›
    | a where ‹a ∈ A› ‹s ≠ []› ‹(s, X) ∈ F (Renaming (P a) f g)›
    | a where ‹a ∈ A› ‹s = []› ‹s ∈ D (Renaming (P a) f g)›
    | a r where ‹a ∈ A› ‹s = []› ‹🍋(r) ∉ X› ‹[🍋(r)] ∈ T (Renaming (P a) f g)›
    unfolding F_GlobalDet by blast
  thus ‹(s, X) ∈ F ?lhs›
  proof cases
    show ‹s = [] ==> ∀a∈A. (s, X) ∈ F (Renaming (P a) f g) ==> (s, X) ∈ F ?lhs›
      by (auto simp add: F_Renaming F_GlobalDet)
  next
    show ‹a ∈ A ==> s ≠ [] ==> (s, X) ∈ F (Renaming (P a) f g) ==> (s, X) ∈ F ?lhs› for a
      by (simp add: F_Renaming GlobalDet_projs) (metis list.simps(8))
  next
    show ‹a ∈ A ==> s = [] ==> s ∈ D (Renaming (P a) f g) ==> (s, X) ∈ F ?lhs› for a
      by (auto simp add: Renaming_projs D_GlobalDet)
  next
    fix a r assume * : ‹a ∈ A› ‹s = []› ‹🍋(r) ∉ X› ‹[🍋(r)] ∈ T (Renaming (P a) f g)›
    from "*"(4) consider s1 where ‹[🍋(r)] = map (map_event_ptick f g) s1› ‹s1 ∈ T (P a)›
      | s1 s2 where ‹[🍋(r)] = map (map_event_ptick f g) s1 @ s2›
        ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ D (P a)›
      by (simp add: T_Renaming) meson
    thus ‹(s, X) ∈ F ?lhs›
    proof cases
      fix s1 assume ‹[🍋(r)] = map (map_event_ptick f g) s1› ‹s1 ∈ T (P a)›
      from ‹[🍋(r)] = map (map_event_ptick f g) s1› obtain r' where ‹r = g r'› ‹s1 = [🍋(r')]›
        by (metis map_map_event_{ptick_eq_tick_iff})
      with "*"(1, 2, 3) ‹s1 ∈ T (P a)›
      show ‹(s, X) ∈ F ?lhs› by (auto simp add: F_Renaming F_GlobalDet)
    next
      fix s1 s2 assume ‹[🍋(r)] = map (map_event_ptick f g) s1 @ s2›
        ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ D (P a)›
      from ‹[🍋(r)] = map (map_event_ptick f g) s1 @ s2› ‹tickFree s1›
      have ‹s1 = [] ∧ s2 = [🍋(r)]›
        by (cases s1; simp) (metis event_ptick.disc(2) event_ptick.map_disc_iff(1))
      with "*"(1, 2) ‹s1 ∈ D (P a)› show ‹(s, X) ∈ F ?lhs›
        by (auto simp add: F_Renaming F_GlobalDet)
    qed
  qed
qed

lemma Renaming_Mprefix_bis :
  ‹Renaming (◻a ∈ A → P a) f g = ◻a ∈ A. (f a → Renaming (P a) f g)›
  by (simp add: Mprefix_GlobalDet Renaming_distrib_GlobalDet Renaming_write0)


(* TODO : useful ? *)
lemma Renaming_GlobalDet_alt:
  ‹Renaming (◻ a ∈ A. P (f a)) f g = ◻ b ∈ f ` A. Renaming (P b) f g›
  (is ‹?lhs = ?rhs›)
  by (simp add: Renaming_distrib_GlobalDet mono_GlobalDet_eq2)


lemma Renaming_GlobalDet_inj_on:
  ‹inj_on f A ==> Renaming (◻ a ∈ A. P a) f g =
 ◻ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
  by (simp add: Renaming_distrib_GlobalDet inj_on_def mono_GlobalDet_eq2 the_equality)


corollary Renaming_GlobalDet_inj:
  ‹inj f ==> Renaming (◻ a ∈ A. P a) f g = ◻ b ∈ f ` A. Renaming (P (THE a. f a = b)) f g›
  by (subst Renaming_GlobalDet_inj_on, metis inj_eq inj_onI)
    (rule mono_GlobalDet_eq, metis imageE inj_eq)


lemma Renaming_Interrupt :
  ‹Renaming (P △ Q) f g = Renaming P f g △ Renaming Q f g› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix t assume ‹t ∈ D ?lhs›
  then obtain t1 t2
    where * : ‹t = map (map_event_ptick f g) t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ D (P △ Q)›
    unfolding D_Renaming by blast
  from "*"(4) consider ‹t1 ∈ D P›
    | u1 u2 where ‹t1 = u1 @ u2› ‹u1 ∈ T P› ‹tF u1› ‹u2 ∈ D Q›
    unfolding D_Interrupt by blast
  thus ‹t ∈ D ?rhs›
  proof cases
    from "*"(1-3) show ‹t1 ∈ D P ==> t ∈ D ?rhs›
      by (auto simp add: D_Interrupt D_Renaming)
  next
    show ‹t1 = u1 @ u2 ==> u1 ∈ T P ==> tF u1 ==> u2 ∈ D Q ==> t ∈ D ?rhs› for u1 u2
      by (simp add: D_Interrupt Renaming_projs "*"(1))
        (metis "*"(2, 3) map_event_{ptick_tickFree} tickFree_append_iff)
  qed
next
  fix t assume ‹t ∈ D ?rhs›
  then consider ‹t ∈ D (Renaming P f g)›
    | t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ T (Renaming P f g)› ‹tF t1› ‹t2 ∈ D (Renaming Q f g)›
    unfolding D_Interrupt by blast
  thus ‹t ∈ D ?lhs›
  proof cases
    show ‹t ∈ D (Renaming P f g) ==> t ∈ D ?lhs›
      by (auto simp add: D_Renaming D_Interrupt)
  next
    show ‹t = t1 @ t2 ==> t1 ∈ T (Renaming P f g) ==> tF t1 ==> t2 ∈ D (Renaming Q f g) ==> t ∈ D ?lhs› for t1 t2
      by (auto simp add: Renaming_projs D_Interrupt append.assoc map_event_{ptick_tickFree})
        (metis (no_types, opaque_lifting) append.assoc map_append tickFree_append_iff,
          metis front_tickFree_append map_event_{ptick_tickFree})
  qed
next
  fix t X assume same_div : ‹D ?lhs = D ?rhs›
  assume ‹(t, X) ∈ F ?lhs›
  then consider ‹t ∈ D ?lhs›
    | u where ‹t = map (map_event_ptick f g) u› ‹(u, map_event_ptick f g -` X) ∈ F (P △ Q)›
    unfolding Renaming_projs by blast
  thus ‹(t, X) ∈ F ?rhs›
  proof cases
    from same_div D_F show ‹t ∈ D ?lhs ==> (t, X) ∈ F ?rhs› by blast
  next
    fix u assume * : ‹t = map (map_event<sub>ptick</sub> f g) u› ‹(u, map_event<sub>ptick</sub> f g -` X) ∈ F (P △ Q)›
    from "*"(2) consider ‹u ∈ D (P △ Q)›
      | u' r  where ‹u = u' @ [🍋(r)]› ‹u' @ [🍋(r)] ∈ T P›
      | X' r  where ‹map_event_ptick f g -` X = X' - {🍋(r)}› ‹u @ [🍋(r)] ∈ T P›
      | ‹(u, map_event<sub>ptick</sub> f g -` X) ∈ F P› ‹tF u› ‹([], map_event_ptick f g -` X) ∈ F Q›
      | u1 u2 where ‹u = u1 @ u2› ‹u1 ∈ T P› ‹tF u1› ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F Q› ‹u2 ≠ []›
      | X' r  where ‹map_event_ptick f g -` X = X' - {🍋(r)}› ‹u ∈ T P› ‹tF u› ‹[🍋(r)] ∈ T Q›
      unfolding Interrupt_projs by safe auto
    thus ‹(t, X) ∈ F ?rhs›
    proof cases
      assume ‹u ∈ D (P △ Q)›
      hence ‹t ∈ D ?lhs›
        by (simp add: "*"(1) D_Renaming)
          (metis (no_types, opaque_lifting) D_imp_front_tickFree append_Nil2 snoc_eq_iff_butlast
            butlast.simps(1) div_butlast_when_non_tickFree_iff front_tickFree_Nil
            front_tickFree_iff_tickFree_butlast front_tickFree_single map_butlast)
      with same_div D_F show ‹(t, X) ∈ F ?rhs› by blast
    next
      show ‹u = u' @ [🍋(r)] ==> u' @ [🍋(r)] ∈ T P ==> (t, X) ∈ F ?rhs› for u' r
        by (auto simp add: "*"(1) F_Interrupt T_Renaming)
    next
      fix X' r assume ** : ‹map_event<sub>ptick</sub> f g -` X = X' - {🍋(r)}› ‹u @ [🍋(r)] ∈ T P›
      from "**" obtain X'' where ‹X = X'' - {🍋(g r)}›
        by (metis DiffD2 Diff_insert_absorb event_ptick.simps(10) insertI1 vimage_eq)
      moreover from "**"(2) have ‹t @ [🍋(g r)] ∈ T (Renaming P f g)›
        by (auto simp add: "*"(1) T_Renaming)
      ultimately show ‹(t, X) ∈ F ?rhs› by (auto simp add: F_Interrupt)
    next
      show ‹(u, map_event_ptick f g -` X) ∈ F P ==> tF u ==>
 ([], map_event<sub>ptick</sub> f g -` X) ∈ F Q ==> (t, X) ∈ F ?rhs›
        using map_event_{ptick_tickFree} by (auto simp add: "*"(1) F_Interrupt F_Renaming)
    next
      fix u1 u2 assume ‹u = u1 @ u2› ‹u1 ∈ T P› ‹tF u1›
        ‹(u2, map_event_ptick f g -` X) ∈ F Q› ‹u2 ≠ []›
      hence ‹t = map (map_event<sub>ptick</sub> f g) u1 @ map (map_event<sub>ptick</sub> f g) u2›
        ‹map (map_event<sub>ptick</sub> f g) u1 ∈ T (Renaming P f g)›
        ‹tF (map (map_event<sub>ptick</sub> f g) u1)›
        ‹(map (map_event<sub>ptick</sub> f g) u2, X) ∈ F (Renaming Q f g)›
        ‹map (map_event<sub>ptick</sub> f g) u2 ≠ []›
        by (auto simp add: "*"(1) Renaming_projs map_event<sub>ptick_tickFree</sub>)
      thus ‹(t, X) ∈ F ?rhs› by (simp add: F_Interrupt) blast
    next
      fix X' r assume ** : ‹map_event<sub>ptick</sub> f g -` X = X' - {🍋(r)}› ‹u ∈ T P› ‹tF u› ‹[🍋(r)] ∈ T Q›
      from "**"(1, 2) obtain X'' where ‹X = X'' - {🍋(g r)}›
        by (metis DiffD2 Diff_insert_absorb event_ptick.simps(10) insertI1 vimage_eq)
      moreover from "**"(2-4) have ‹t ∈ T (Renaming P f g)› ‹tF t›
        ‹[🍋(g r)] ∈ T (Renaming Q f g)›
        by (auto simp add: "*"(1) T_Renaming map_event_{ptick_tickFree})
      ultimately show ‹(t, X) ∈ F ?rhs› by (simp add: F_Interrupt) blast
    qed
  qed
next
  fix t X assume same_div : ‹D ?lhs = D ?rhs›
  assume ‹(t, X) ∈ F ?rhs›
  then consider ‹t ∈ D ?rhs›
    | t' s  where ‹t = t' @ [🍋(s)]› ‹t' @ [🍋(s)] ∈ T (Renaming P f g)›
    | X' s  where ‹X = X' - {🍋(s)}› ‹t @ [🍋(s)] ∈ T (Renaming P f g)›
    | ‹(t, X) ∈ F (Renaming P f g)› ‹tF t› ‹([], X) ∈ F (Renaming Q f g)›
    | t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ T (Renaming P f g)› ‹tF t1›
      ‹(t2, X) ∈ F (Renaming Q f g)› ‹t2 ≠ []›
    | X' s where ‹X = X' - {🍋(s)}› ‹t ∈ T (Renaming P f g)› ‹tF t› ‹[🍋(s)] ∈ T (Renaming Q f g)›
    by (simp add: Interrupt_projs) blast
  thus ‹(t, X) ∈ F ?lhs›
  proof cases
    from same_div D_F show ‹t ∈ D ?rhs ==> (t, X) ∈ F ?lhs› by blast
  next
    show ‹[t = t' @ [🍋(s)]; t' @ [🍋(s)] ∈ T (Renaming P f g)] ==> (t, X) ∈ F ?lhs› for t' s
      by (simp add: Renaming_projs Interrupt_projs)
        (metis T_nonTickFree_imp_decomp map_event_{ptick_tickFree} non_tickFree_tick tickFree_append_iff)
  next
    fix X' s assume * : ‹X = X' - {🍋(s)}› ‹t @ [🍋(s)] ∈ T (Renaming P f g)›
    from "*"(2) consider u1 u2 where
      ‹t @ [🍋(s)] = map (map_event_ptick f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
    | u r where ‹s = g r› ‹t = map (map_event_ptick f g) u› ‹u @ [🍋(r)] ∈ T P›
      by (simp add: T_Renaming)
        (metis (no_types, opaque_lifting) T_nonTickFree_imp_decomp event_ptick.disc(4)
          event_ptick.map_sel(2) event_ptick.sel(2) last_map map_butlast map_event_{ptick_tickFree}
          non_tickFree_tick snoc_eq_iff_butlast tickFree_append_iff)
    thus ‹(t, X) ∈ F ?lhs›
    proof cases
      fix u1 u2 assume ‹t @ [🍋(s)] = map (map_event_ptick f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
      hence ‹t ∈ D ?lhs›
        by (cases u2 rule: rev_cases)
          (auto simp add: D_Interrupt D_Renaming intro: front_tickFree_dw_closed,
            metis map_event_{ptick_tickFree} non_tickFree_tick tickFree_append_iff)
      with D_F show ‹(t, X) ∈ F ?lhs› by blast
    next
      fix u r assume ‹s = g r› ‹t = map (map_event_ptick f g) u› ‹u @ [🍋(r)] ∈ T P›
      moreover from "*"(1) ‹s = g r› obtain X'' where ‹map_event_ptick f g -` X = X'' - {🍋(r)}›
        by (metis Diff_iff Diff_insert_absorb event<sub>ptick</sub>.simps(10) vimage_eq vimage_singleton_eq)
      ultimately show ‹(t, X) ∈ F ?lhs› by (simp add: F_Renaming F_Interrupt) metis
    qed
  next
    show ‹[(t, X) ∈ F (Renaming P f g); tF t; ([], X) ∈ F (Renaming Q f g)] ==> (t, X) ∈ F ?lhs›
      by (simp add: Renaming_projs Interrupt_projs)
        (metis is_processT8 map_event<sub>ptick_tickFree</sub>)
  next
    fix t1 t2 assume * : ‹t = t1 @ t2› ‹t1 ∈ T (Renaming P f g)› ‹tF t1›
      ‹(t2, X) ∈ F (Renaming Q f g)› ‹t2 ≠ []›
    from "*"(2) consider u1 u2 where
      ‹t1 = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
    | u1 where ‹t1 = map (map_event<sub>ptick</sub> f g) u1› ‹u1 ∈ T P›
      unfolding T_Renaming by blast
    thus ‹(t, X) ∈ F ?lhs›
    proof cases
      fix u1 u2 assume ‹t1 = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
      hence ‹t1 ∈ D ?lhs› by (auto simp add: D_Interrupt D_Renaming)
      with "*"(1, 3, 4) F_imp_front_tickFree is_processT7 have ‹t ∈ D ?lhs› by blast
      with D_F show ‹(t, X) ∈ F ?lhs› by blast
    next
      fix u1 assume ** : ‹t1 = map (map_event<sub>ptick</sub> f g) u1› ‹u1 ∈ T P›
      from "*"(4) consider u2 u3 where
        ‹t2 = map (map_event<sub>ptick</sub> f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ D Q›
      | u2 where ‹t2 = map (map_event<sub>ptick</sub> f g) u2› ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F Q›
        unfolding F_Renaming by blast
      thus ‹(t, X) ∈ F ?lhs›
      proof cases
        fix u2 u3 assume ‹t2 = map (map_event_ptick f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ D Q›
        hence ‹t ∈ D ?lhs›
          by (simp add: "*"(1) "**"(1) D_Renaming D_Interrupt flip: map_append append.assoc)
            (metis "*"(3) "**"(1, 2) map_event_{ptick_tickFree} tickFree_append_iff)
        with D_F show ‹(t, X) ∈ F ?lhs› by blast
      next
        show ‹t2 = map (map_event_ptick f g) u2 ==> (u2, map_event_ptick f g -` X) ∈ F Q
 ==> (t, X) ∈ F ?lhs› for u2
          by (simp add: F_Renaming F_Interrupt "*"(1) "**"(1) flip: map_append)
            (metis "*"(3, 5) "**"(1, 2) list.map_disc_iff map_event<sub>ptick_tickFree</sub>)
      qed
    qed
  next
    fix X' s assume * : ‹X = X' - {🍋(s)}› ‹t ∈ T (Renaming P f g)›
      ‹tF t› ‹[🍋(s)] ∈ T (Renaming Q f g)›
    from "*"(2) consider u1 u2 where
      ‹t = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
    | u where ‹t = map (map_event<sub>ptick</sub> f g) u› ‹u ∈ T P›
      by (auto simp add: T_Renaming)
    thus ‹(t, X) ∈ F ?lhs›
    proof cases
      fix u1 u2 assume ‹t = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
      hence ‹t ∈ D ?lhs› by (auto simp add: D_Interrupt D_Renaming)
      with D_F show ‹(t, X) ∈ F ?lhs› by blast
    next
      fix u assume ** : ‹t = map (map_event<sub>ptick</sub> f g) u› ‹u ∈ T P›
      from "*"(4) consider ‹Renaming Q f g = ⊥› | r where ‹s = g r› ‹[🍋(r)] ∈ T Q›
        by (simp add: Renaming_projs BOT_iff_tick_D)
          (metis map_map_event<sub>ptick_eq_tick_iff</sub>)
      thus ‹(t, X) ∈ F ?lhs›
      proof cases
        assume ‹Renaming Q f g = ⊥›
        hence ‹Q = ⊥› by (simp add: Renaming_is_BOT_iff)
        hence ‹Renaming (P △ Q) f g = ⊥› by simp
        thus ‹(t, X) ∈ F ?lhs› by (simp add: F_BOT "*"(3))
      next
        fix r assume ‹s = g r› ‹[🍋(r)] ∈ T Q›
        moreover from "*"(1) ‹s = g r› obtain X''
          where ‹map_event<sub>ptick</sub> f g -` X = X'' - {🍋(r)}›
          by (metis DiffD2 Diff_empty Diff_insert0 event_ptick.simps(10) insertI1 vimage_eq)
        ultimately show ‹(t, X) ∈ F ?lhs›
          by (simp add: "**"(1) F_Renaming F_Interrupt)
            (metis "*"(3) "**"(1, 2) map_event_{ptick_tickFree})
      qed
    qed
  qed
qed


lemma inj_on_Renaming_Throw :
  ‹Renaming (P Θ a ∈ A. Q a) f g =
 Renaming P f g Θ b ∈ f ` A. Renaming (Q (inv_into A f b)) f g›
  (is ‹?lhs = ?rhs›) if inj_on_f : ‹inj_on f (events_of P ∪ A)›
proof -
  have $ : ‹set (map (map_event<sub>ptick</sub> f g) t) ∩ ev ` f ` A = {}
 ⟷ set t ∩ ev ` A = {}› if ‹t ∈ T P› for t
  proof -
    from ‹t ∈ T P› inj_on_f have ‹inj_on f ({a. ev a ∈ set t} ∪ A)›
      by (auto simp add: inj_on_def events_of_memI)
    thus ‹set (map (map_event_ptick f g) t) ∩ ev ` f ` A = {}
 ⟷ set t ∩ ev ` A = {}›
      by (auto simp add: disjoint_iff image_iff inj_on_def map_event<sub>ptick_eq_ev_iff</sub>)
        (metis event<sub>ptick</sub>.simps(9), blast)
  qed
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    fix t assume ‹t ∈ D ?lhs›
    then obtain t1 t2 where * : ‹t = map (map_event<sub>ptick</sub> f g) t1 @ t2› ‹tF t1›
      ‹ftF t2› ‹t1 ∈ D (P Θ a ∈ A. Q a)›
      unfolding D_Renaming by blast
    from "*"(4) consider u1 u2 where ‹t1 = u1 @ u2› ‹u1 ∈ D P› ‹tF u1›
      ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
    | u1 a u2 where ‹t1 = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ T P›
      ‹set u1 ∩ ev ` A = {}› ‹a ∈ A› ‹u2 ∈ D (Q a)›
      unfolding D_Throw by blast
    thus ‹t ∈ D ?rhs›
    proof cases
      fix u1 u2 assume ** : ‹t1 = u1 @ u2› ‹u1 ∈ D P› ‹tF u1›
        ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
      from "$" "**"(2) "**"(4) D_T
      have *** : ‹set (map (map_event_ptick f g) u1) ∩ ev ` f ` A = {}› by blast
      have ‹t = map (map_event_ptick f g) u1 @ (map (map_event_ptick f g) u2 @ t2)›
        by (simp add: "*"(1) "**"(1))
      moreover from "*"(2, 3) "**"(1) have ‹ftF (map (map_event_ptick f g) u2 @ t2)›
        by (simp add: front_tickFree_append map_event_{ptick_tickFree})
      moreover have ‹tF (map (map_event_ptick f g) u1)›
        by (simp add: "**"(3) map_event_{ptick_tickFree})
      ultimately show ‹t ∈ D ?rhs›
        by (simp add: D_Throw D_Renaming)
          (use "**"(2) "**"(3) "***" front_tickFree_Nil in blast)
    next
      fix u1 a u2 assume ** : ‹t1 = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ T P›
        ‹set u1 ∩ ev ` A = {}› ‹a ∈ A› ‹u2 ∈ D (Q a)›
      have *** : ‹set (map (map_event<sub>ptick</sub> f g) u1) ∩ ev ` f ` A = {}›
        by (meson "$" "**"(2) "**"(3) T_F_spec is_processT3)
      have ‹tF u2› using "*"(2) "**"(1) by auto
      moreover have ‹t = map (map_event<sub>ptick</sub> f g) u1 @ ev (f a) # map (map_event<sub>ptick</sub> f g) u2 @ t2›
        by (simp add: "*"(1) "**"(1))
      moreover from "**"(2) have ‹map (map_event<sub>ptick</sub> f g) u1 @ [ev (f a)] ∈ T (Renaming P f g)›
        by (auto simp add: T_Renaming )
      moreover have ‹inv_into A f (f a) = a›
        by (meson "**"(4) inj_on_Un inv_into_f_eq inj_on_f)
      ultimately show ‹t ∈ D ?rhs›
        by (simp add: D_Throw D_Renaming)
          (metis "*"(3) "**"(4) "**"(5) "***" imageI)
    qed
  next
    fix t assume ‹t ∈ D ?rhs›
    then consider t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ D (Renaming P f g)›
      ‹tF t1› ‹set t1 ∩ ev ` f ` A = {}› ‹ftF t2›
    | t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ T (Renaming P f g)›
      ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
      ‹t2 ∈ D (Renaming (Q (inv_into A f b)) f g)›
      unfolding D_Throw by blast
    thus ‹t ∈ D ?lhs›
    proof cases
      fix t1 t2 assume * : ‹t = t1 @ t2› ‹t1 ∈ D (Renaming P f g)›
        ‹tF t1› ‹set t1 ∩ ev ` f ` A = {}› ‹ftF t2›
      from "*"(2) obtain u1 u2
        where ** : ‹t1 = map (map_event_ptick f g) u1 @ u2› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
        unfolding D_Renaming by blast
      from "*"(4) "**"(1) have ‹set u1 ∩ ev ` A = {}› by auto
      moreover have ‹t = map (map_event<sub>ptick</sub> f g) u1 @ (u2 @ t2)›
        by (simp add: "*"(1) "**"(1))
      moreover from "*"(3, 5) "**"(1) front_tickFree_append tickFree_append_iff
      have ‹ftF (u2 @ t2)› by blast
      ultimately show ‹t ∈ D ?lhs›
        by (simp add: D_Renaming D_Throw)
          (use "**"(2, 4) front_tickFree_Nil in blast)
    next
      fix t1 b t2 assume * : ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ T (Renaming P f g)›
        ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
        ‹t2 ∈ D (Renaming (Q (inv_into A f b)) f g)›
      from ‹b ∈ f ` A› obtain a where ‹a ∈ A› ‹b = f a› by blast
      hence ‹inv_into A f b = a› by (meson inj_on_Un inv_into_f_f inj_on_f)
      from "*"(2) consider u1 u2 where
        ‹t1 @ [ev b] = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
      | u1 where ‹t1 @ [ev b] = map (map_event<sub>ptick</sub> f g) u1› ‹u1 ∈ T P›
        by (simp add: D_T T_Renaming)
          (metis (no_types, opaque_lifting) D_T append.right_neutral)
      thus ‹t ∈ D ?lhs›
      proof cases
        fix u1 u2
        assume ** : ‹t1 @ [ev b] = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
        from "**"(1, 2) obtain u2' where *** : ‹t1 = map (map_event<sub>ptick</sub> f g) u1 @ u2'›
          by (metis butlast_append butlast_snoc)
        from "*"(3) "***" have **** : ‹set u1 ∩ ev ` A = {}› by auto
        have ***** : ‹t = map (map_event_ptick f g) u1 @ (u2' @ ev b # t2)› ‹ftF (u2' @ ev b # t2)›
          by (simp_all add: "*"(1) "***" "****" front_tickFree_append_iff)
            (metis "*"(2, 5) "***" D_imp_front_tickFree append_T_imp_tickFree
              event_ptick.disc(1) front_tickFree_Cons_iff not_Cons_self tickFree_append_iff)
        show ‹t ∈ D ?lhs›
          by (simp add: D_Renaming D_Throw)
            (metis "**"(3) "**"(5) "****" "*****" append_Nil2 front_tickFree_Nil)
      next
        fix u1 assume ‹t1 @ [ev b] = map (map_event_ptick f g) u1› ‹u1 ∈ T P›
        then obtain u1' where ** : ‹t1 = map (map_event_ptick f g) u1'› ‹u1' @ [ev a] ∈ T P›
          by (cases u1 rule: rev_cases, simp_all add: ‹b = f a› ev_eq_map_event_{ptick_iff})
            (metis Nil_is_append_conv Un_iff ‹a ∈ A› events_of_memI inj_onD
              inj_on_f last_in_set last_snoc list.distinct(1))
        from "*"(3) "**"(1) have *** : ‹set u1' ∩ ev ` A = {}› by auto
        from "*"(5) ‹inv_into A f b = a› obtain u2 u3 where
          **** : ‹t2 = map (map_event<sub>ptick</sub> f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ D (Q a)›
          unfolding Renaming_projs by blast
        have ***** : ‹t = map (map_event<sub>ptick</sub> f g) (u1' @ ev a # u2) @ u3› ‹tF (u1' @ ev a # u2)›
          by (simp_all add: "*"(1) "**"(1) ‹b = f a› "****"(1))
            (metis "**"(2) "****"(2) T_imp_front_tickFree butlast_snoc
              front_tickFree_iff_tickFree_butlast)
        show ‹t ∈ D ?lhs›
          by (simp add: D_Renaming D_Throw)
            (metis "**"(2) "***" "****"(3, 4) "*****"(1, 2) ‹a ∈ A›)
      qed
    qed
  next
    fix t X assume same_div : ‹D ?lhs = D ?rhs›
    assume ‹(t, X) ∈ F ?lhs›
    then consider ‹t ∈ D ?lhs›
      | u where ‹t = map (map_event<sub>ptick</sub> f g) u› ‹(u, map_event<sub>ptick</sub> f g -` X) ∈ F (P Θ a ∈ A. Q a)›
      unfolding Renaming_projs by blast
    thus ‹(t, X) ∈ F ?rhs›
    proof cases
      from same_div D_F show ‹t ∈ D ?lhs ==> (t, X) ∈ F ?rhs› by blast
    next
      fix u assume * : ‹t = map (map_event_ptick f g) u›
        ‹(u, map_event_ptick f g -` X) ∈ F (P Θ a ∈ A. Q a)›
      then consider ‹(u, map_event<sub>ptick</sub> f g -` X) ∈ F P› ‹set u ∩ ev ` A = {}›
        | u1 u2   where ‹u = u1 @ u2› ‹u1 ∈ D P› ‹tF u1› ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
        | u1 a u2 where ‹u = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ T P› ‹set u1 ∩ ev ` A = {}›
          ‹a ∈ A› ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F (Q a)›
        unfolding F_Throw by blast
      thus ‹(t, X) ∈ F ?rhs›
      proof cases
        show ‹(u, map_event_ptick f g -` X) ∈ F P ==> set u ∩ ev ` A = {} ==> (t, X) ∈ F ?rhs›
          by (simp add: F_Throw F_Renaming) (metis "$" "*"(1) F_T)
      next
        fix u1 u2 assume ‹u = u1 @ u2› ‹u1 ∈ D P› ‹tF u1› ‹set u1 ∩ ev ` A = {}› ‹ftF u2›
        hence ‹t ∈ D ?lhs›
          by (simp add: "*"(1) D_Renaming D_Throw)
            (metis append_Nil2 front_tickFree_Nil map_event<sub>ptick_front_tickFree</sub>)
        with same_div D_F show ‹(t, X) ∈ F ?rhs› by blast
      next
        fix u1 a u2
        assume ** : ‹u = u1 @ ev a # u2› ‹u1 @ [ev a] ∈ T P› ‹set u1 ∩ ev ` A = {}›
          ‹a ∈ A› ‹(u2, map_event_ptick f g -` X) ∈ F (Q a)›
        have *** : ‹set (map (map_event<sub>ptick</sub> f g) u1) ∩ ev ` f ` A = {}›
          by (meson "$" "**"(2, 3) T_F_spec is_processT3)
        have ‹t = map (map_event<sub>ptick</sub> f g) u1 @ ev (f a) # map (map_event<sub>ptick</sub> f g) u2›
          by (simp add: "*"(1) "**"(1))
        moreover from "**"(2) have ‹map (map_event<sub>ptick</sub> f g) u1 @ [ev (f a)] ∈ T (Renaming P f g)›
          by (auto simp add: T_Renaming)
        moreover have ‹inv_into A f (f a) = a›
          by (meson "**"(4) inj_on_Un inv_into_f_f inj_on_f)
        moreover from "**"(5) have ‹(map (map_event<sub>ptick</sub> f g) u2, X) ∈ F (Renaming (Q a) f g)›
          by (auto simp add: F_Renaming)
        ultimately show ‹(t, X) ∈ F ?rhs›
          by (simp add: F_Throw) (metis "**"(4) "***" image_eqI)
      qed
    qed
  next
    fix t X assume same_div : ‹D ?lhs = D ?rhs›
    assume ‹(t, X) ∈ F ?rhs›
    then consider ‹t ∈ D ?rhs›
      | ‹(t, X) ∈ F (Renaming P f g)› ‹set t ∩ ev ` f ` A = {}›
      | t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ T (Renaming P f g)›
        ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
        ‹(t2, X) ∈ F (Renaming (Q (inv_into A f b)) f g)›
      unfolding Throw_projs by auto
    thus ‹(t, X) ∈ F ?lhs›
    proof cases
      from same_div D_F show ‹t ∈ D ?rhs ==> (t, X) ∈ F ?lhs› by blast
    next
      assume * : ‹(t, X) ∈ F (Renaming P f g)› ‹set t ∩ ev ` f ` A = {}›
      from "*"(1) consider ‹t ∈ D (Renaming P f g)›
        | u where ‹t = map (map_event_ptick f g) u› ‹(u, map_event_ptick f g -` X) ∈ F P›
        unfolding Renaming_projs by blast
      thus ‹(t, X) ∈ F ?lhs›
      proof cases
        assume ‹t ∈ D (Renaming P f g)›
        hence ‹t ∈ D ?lhs›
          by (simp add: D_Renaming D_Throw)
            (metis (no_types, lifting) "$" "*"(2) D_T Un_Int_eq(3) append_Nil2
              front_tickFree_Nil inf_bot_right inf_sup_aci(2) set_append)
        with D_F show ‹(t, X) ∈ F ?lhs› by blast
      next
        show ‹t = map (map_event<sub>ptick</sub> f g) u ==> (u, map_event<sub>ptick</sub> f g -` X) ∈ F P
 ==> (t, X) ∈ F ?lhs› for u
          by (simp add: F_Renaming F_Throw) (metis "$" "*"(2) F_T)
      qed
    next
      fix t1 b t2
      assume * : ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ T (Renaming P f g)›
        ‹set t1 ∩ ev ` f ` A = {}› ‹b ∈ f ` A›
        ‹(t2, X) ∈ F (Renaming (Q (inv_into A f b)) f g)›
      from "*"(4) obtain a where ‹a ∈ A› ‹b = f a› by blast
      hence ‹inv_into A f b = a› by (meson inj_on_Un inv_into_f_f inj_on_f)
      from "*"(2) consider u1 u2 where
        ‹t1 @ [ev b] = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
      | u1 where ‹t1 @ [ev b] = map (map_event<sub>ptick</sub> f g) u1› ‹u1 ∈ T P›
        by (simp add: D_T T_Renaming)
          (metis (no_types, opaque_lifting) D_T append.right_neutral)
      thus ‹(t, X) ∈ F ?lhs›
      proof cases
        fix u1 u2
        assume ** : ‹t1 @ [ev b] = map (map_event<sub>ptick</sub> f g) u1 @ u2› ‹u2 ≠ []› ‹tF u1› ‹ftF u2› ‹u1 ∈ D P›
        from "**"(1, 2) obtain u2' where *** : ‹t1 = map (map_event<sub>ptick</sub> f g) u1 @ u2'›
          by (metis butlast_append butlast_snoc)
        from "*"(3) "***" have ‹set u1 ∩ ev ` A = {}› by auto
        with "**"(3-5) "***" have ‹t ∈ D ?rhs›
          by (simp add: D_Renaming D_Throw)
            (metis "*"(1, 3) F_imp_front_tickFree ‹(t, X) ∈ F ?rhs› front_tickFree_Nil
              front_tickFree_append_iff front_tickFree_dw_closed list.discI)
        with same_div D_F show ‹(t, X) ∈ F ?lhs› by blast
      next
        fix u1 assume ‹t1 @ [ev b] = map (map_event_ptick f g) u1› ‹u1 ∈ T P›
        then obtain u1' where ** : ‹t1 = map (map_event_ptick f g) u1'› ‹u1' @ [ev a] ∈ T P›
          by (cases u1 rule: rev_cases, simp_all add: ‹b = f a› ev_eq_map_event_{ptick_iff})
            (metis Nil_is_append_conv Un_iff ‹a ∈ A› events_of_memI inj_onD
              inj_on_f last_in_set last_snoc list.distinct(1))
        from "*"(3) "**"(1) have *** : ‹set u1' ∩ ev ` A = {}› by auto
        from "*"(5) ‹inv_into A f b = a› consider ‹t2 ∈ D (Renaming (Q a) f g)›
          | u2 where ‹t2 = map (map_event<sub>ptick</sub> f g) u2› ‹(u2, map_event<sub>ptick</sub> f g -` X) ∈ F (Q a)›
          unfolding Renaming_projs by blast
        thus ‹(t, X) ∈ F ?lhs›
        proof cases
          assume ‹t2 ∈ D (Renaming (Q a) f g)›
          with "*"(1-4) ‹inv_into A f b = a› have ‹t ∈ D ?rhs›
            by (auto simp add: D_Throw)
          with same_div D_F show ‹(t, X) ∈ F ?lhs› by blast
        next
          fix u2 assume **** : ‹t2 = map (map_event_ptick f g) u2›
            ‹(u2, map_event_ptick f g -` X) ∈ F (Q a)›
          from "****"(1) have ***** : ‹t = map (map_event_ptick f g) (u1' @ ev a # u2)›  
            by (simp add: "*"(1) "**"(1) "****" ‹b = f a›)
          show ‹(t, X) ∈ F ?lhs›
            by (simp add: F_Renaming F_Throw)
              (use "**"(2) "***" "****"(2) "*****" ‹a ∈ A› in blast)
        qed
      qed
    qed
  qed
qed



subsection ‹const‹Renaming› and const‹Hiding››

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

lemma strict_mono_map: ‹strict_mono g ==> strict_mono (λi. map f (g i))›
  unfolding strict_mono_def less_eq_list_def less_list_def prefix_def by fastforce



lemma trace_hide_map_map_event_ptick :
  ‹inj_on (map_event_ptick f g) (set s ∪ ev ` S) ==>
 trace_hide (map (map_event<sub>ptick</sub> f g) s) (ev ` f ` S) =
 map (map_event<sub>ptick</sub> f g) (trace_hide s (ev ` S))›
proof (induct s)
  case Nil
  show ?case by simp
next
  case (Cons e s)
  hence * : ‹trace_hide (map (map_event_ptick f g) s) (ev ` f ` S) =
 map (map_event_ptick f g) (trace_hide s (ev ` S))› by fastforce
  from Cons.prems[unfolded inj_on_def, rule_format, of e, simplified] show ?case
    apply (simp add: "*")
    apply (simp add: image_iff)
    by (metis event_ptick.simps(9))
qed


lemma inj_on_map_event_{ptick_set_T}:
  ‹inj_on (map_event_ptick f g) (set s)› if ‹inj_on f (events_of P)› ‹s ∈ T P›
proof (rule inj_onI)
  show ‹e ∈ set s ==> e' ∈ set s ==> map_event_ptick f g e = map_event_ptick f g e' ==> e = e'› for e e'
    by (cases e; cases e'; simp)
      (meson events_of_memI inj_onD that(1, 2),
        metis T_imp_front_tickFree event_ptick.disc(2) event_ptick.simps(2) front_tickFree_Cons_iff that(2)
        front_tickFree_nonempty_append_imp list.distinct(1) snoc_eq_iff_butlast split_list_last)
qed


theorem bij_Renaming_Hiding: ‹Renaming (P \ S) f g = Renaming P f g \ f ` S›
  (is ‹?lhs = ?rhs›) if bij_f: ‹bij f› and bij_g : ‹bij g›
proof -
  have inj_on_map_event<sub>ptick</sub> : ‹inj_on (map_event<sub>ptick</sub> f g) X› for X
  proof (rule inj_onI)
    show ‹e ∈ X ==> e' ∈ X ==> map_event<sub>ptick</sub> f g e = map_event<sub>ptick</sub> f g e' ==> e = e'› for e e'
      by (cases e; cases e'; simp)
        (metis bij_f bij_pointE, metis bij_g bij_pointE)
  qed
  have inj_on_map_event<sub>ptick_inv</sub> : ‹inj_on (map_event<sub>ptick</sub> (inv f) (inv g)) X› for X
  proof (rule inj_onI)
    show ‹e ∈ X ==> e' ∈ X ==> map_event<sub>ptick</sub> (inv f) (inv g) e = map_event<sub>ptick</sub> (inv f) (inv g) e'
 ==> e = e'› for e e'
      by (cases e; cases e', simp_all)
        (metis bij_f bij_inv_eq_iff, metis bij_g bij_inv_eq_iff)
  qed
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ D ?lhs›
    then obtain s1 s2 where * : ‹tickFree s1› ‹front_tickFree s2›
      ‹s = map (map_event<sub>ptick</sub> f g) s1 @ s2› ‹s1 ∈ D (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 ∈ D P ∨ (∃h. isInfHiddenRun h P S ∧ t ∈ range h)›
      by (simp add: D_Hiding) blast
    from "**"(4) show ‹s ∈ D ?rhs›
    proof (elim disjE)
      assume ‹t ∈ D P›
      hence ‹front_tickFree (map (map_event_ptick f g) u @ s2) ∧ tickFree (map (map_event_ptick f g) t) ∧
 s = trace_hide (map (map_event_ptick f g) t) (ev ` f ` S) @ map (map_event_ptick f g) u @ s2 ∧
 map (map_event_ptick f g) t ∈ D (Renaming P f g)›
        apply (simp add: "*"(3) "**"(2, 3) map_event_{ptick_tickFree}, intro conjI)
          apply (metis "*"(1, 2) "**"(1) "**"(3) front_tickFree_append_iff
            map_event_{ptick_front_tickFree} map_event_{ptick_tickFree} tickFree_append_iff)
         apply (simp add: trace_hide_map_map_event_ptick inj_on_map_event_ptick)
        by (metis (mono_tags, lifting) "**"(2) CollectI D_Renaming append.right_neutral front_tickFree_Nil)
      thus ‹s ∈ D ?rhs› by (simp add: D_Hiding) blast
    next
      assume ‹∃h. isInfHiddenRun h P S ∧ t ∈ range h›
      then obtain h where ‹isInfHiddenRun h P S› ‹t ∈ range h› by blast
      hence ‹front_tickFree (map (map_event_ptick f g) u @ s2) ∧
 tickFree (map (map_event_ptick f g) t) ∧
 s = trace_hide (map (map_event_ptick f g) t) (ev ` f ` S) @ map (map_event_ptick f g) u @ s2 ∧
 isInfHiddenRun (λi. map (map_event_ptick f g) (h i)) (Renaming P f g) (f ` S) ∧
 map (map_event<sub>ptick</sub> f g) t ∈ range (λi. map (map_event<sub>ptick</sub> f g) (h i))›
        apply (simp add: "*"(3) "**"(2, 3) map_event<sub>ptick_tickFree</sub>, intro conjI)
             apply (metis "*"(1, 2) "**"(3) front_tickFree_append map_event<sub>ptick_tickFree</sub> tickFree_append_iff)
            apply (rule trace_hide_map_map_event<sub>ptick</sub>[OF inj_on_map_event<sub>ptick</sub>, symmetric])
           apply (solves ‹rule strict_mono_map, simp›)
          apply (solves ‹auto simp add: T_Renaming›)
         apply (subst (1 2) trace_hide_map_map_event<sub>ptick</sub>[OF inj_on_map_event<sub>ptick</sub>])
        by metis blast
      thus ‹s ∈ D ?rhs› by (simp add: D_Hiding) blast
    qed
  next
    fix s
    assume ‹s ∈ D ?rhs›
    then obtain t u
      where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` f ` S) @ u›
        ‹t ∈ D (Renaming P f g) ∨
 (∃h. isInfHiddenRun h (Renaming P f g) (f ` S) ∧ t ∈ range h)›
      by (simp add: D_Hiding) blast
    from "*"(4) show ‹s ∈ D ?lhs›
    proof (elim disjE)
      assume ‹t ∈ D (Renaming P f g)›
      then obtain t1 t2 where ** : ‹tickFree t1› ‹front_tickFree t2›
        ‹t = map (map_event_ptick f g) t1 @ t2› ‹t1 ∈ D 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 (map_event<sub>ptick</sub> f g) t1) (ev ` f ` S) @ trace_hide t2 (ev ` f ` S) @ u =
 map (map_event<sub>ptick</sub> f g) (trace_hide t1 (ev ` S)) @ trace_hide t2 (ev ` f ` S) @ u ∧
 trace_hide t1 (ev ` S) ∈ D (P \ S)›
        apply (simp, intro conjI)
        using "**"(1) Hiding_tickFree apply blast
        using "*"(1, 2) "**"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff apply blast
         apply (rule trace_hide_map_map_event<sub>ptick</sub>[OF inj_on_map_event<sub>ptick</sub>])
        using "**"(4) mem_D_imp_mem_D_Hiding by blast
      thus ‹s ∈ D ?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 (map_event<sub>ptick</sub> (inv f) (inv g) ∘ map_event<sub>ptick</sub> f g) v = v› for v
        by (induct v, simp_all)
          (metis bij_f bij_g bij_inv_eq_iff event<sub>ptick</sub>.exhaust event<sub>ptick</sub>.simps(9) map_event<sub>ptick_eq_tick_iff</sub>)
      assume ‹∃h. isInfHiddenRun h (Renaming P f g) (f ` S) ∧ t ∈ range h›
      then obtain h
        where *** : ‹isInfHiddenRun h (Renaming P f g) (f ` S)› ‹t ∈ range h› by blast
      then consider t1 where ‹t1 ∈ T P› ‹t = map (map_event<sub>ptick</sub> f g) t1›
        | t1 t2 where ‹tickFree t1› ‹front_tickFree t2›
          ‹t = map (map_event<sub>ptick</sub> f g) t1 @ t2› ‹t1 ∈ D P›
        by (simp add: T_Renaming) blast
      thus ‹s ∈ D ?lhs›
      proof cases
        fix t1 assume **** : ‹t1 ∈ T P› ‹t = map (map_event<sub>ptick</sub> f g) t1›
        have ***** : ‹t1 = map (map_event<sub>ptick</sub> (inv f) (inv g)) t› by (simp add: "****"(2) "**")
        have ****** : ‹trace_hide t1 (ev ` S) = trace_hide t1 (ev ` S) ∧
 isInfHiddenRun (λi. map (map_event_ptick (inv f) (inv g)) (h i)) P S ∧
 t1 ∈ range (λi. map (map_event_ptick (inv f) (inv g)) (h i))›
          apply (simp add: "***"(1) strict_mono_map, intro conjI)
            apply (subst Renaming_inv[where f = f and g = g, symmetric])
              apply (solves ‹simp add: bij_is_inj bij_f›)
             apply (solves ‹simp add: bij_is_inj bij_g›)

          using "***"(1) apply (subst T_Renaming, blast)
           apply (subst (1 2) inv_S, subst (1 2) trace_hide_map_map_event_ptick[OF inj_on_map_event_{ptick_inv}])
           apply (metis "***"(1))
          using "***"(2) "*****" by blast
        have ‹tickFree (trace_hide t1 (ev ` S)) ∧ front_tickFree t1 ∧
 trace_hide (map (map_event<sub>ptick</sub> f g) t1) (ev ` f ` S) @ u =
 map (map_event<sub>ptick</sub> f g) (trace_hide t1 (ev ` S)) @ u ∧
 trace_hide t1 (ev ` S) ∈ D (P \ S)›
          apply (simp, intro conjI)
          using "*"(2) "****"(2) map_event<sub>ptick_tickFree</sub> Hiding_tickFree apply blast
          using "****"(1) is_processT2_TR apply blast
           apply (rule trace_hide_map_map_event<sub>ptick</sub>[OF inj_on_map_event<sub>ptick</sub>])
          apply (simp add: D_Renaming D_Hiding)
          using "*"(2) "*****" "******" map_event<sub>ptick_tickFree</sub> front_tickFree_Nil by blast
        with "*"(1) show ‹s ∈ D ?lhs› by (simp add: D_Renaming "*"(3) "****"(2)) blast
      next
        fix t1 t2 assume **** : ‹tickFree t1› ‹front_tickFree t2›
          ‹t = map (map_event<sub>ptick</sub> f g) t1 @ t2› ‹t1 ∈ D P›
        have ‹tickFree (trace_hide t1 (ev ` S)) ∧
 front_tickFree (trace_hide t2 (ev ` f ` S) @ u) ∧
 trace_hide (map (map_event_ptick f g) t1) (ev ` f ` S) @ trace_hide t2 (ev ` f ` S) @ u =
 map (map_event_ptick f g) (trace_hide t1 (ev ` S)) @ trace_hide t2 (ev ` f ` S) @ u ∧
 trace_hide t1 (ev ` S) ∈ D (P \ S)›
          apply (simp, intro conjI)
          using "****"(1) Hiding_tickFree apply blast
          using "*"(1, 2) "****"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff apply blast
           apply (rule trace_hide_map_map_event_ptick[OF inj_on_map_event_ptick])
          using "****"(4) mem_D_imp_mem_D_Hiding by blast
        thus ‹s ∈ D ?lhs› by (simp add: D_Renaming "*"(3) "****"(3)) blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹D ?lhs = D ?rhs›
    assume ‹(s, X) ∈ F ?lhs›
    then consider ‹s ∈ D ?lhs›
      | s1 where ‹(s1, map_event_ptick f g -` X) ∈ F (P \ S)› ‹s = map (map_event<sub>ptick</sub> f g) s1›
      by (simp add: F_Renaming D_Renaming) blast
    thus ‹ ‹
java.lang.StringIndexOutOfBoundsException: Index 68 out of bounds for length 15
 from D_F same_div show ‹s ∈ D ?lhs ==> (s, X) ∈ F ?rhs› by blast
 next
 fix s1 assume * : ‹(s1, map_event<sub>pdiv_minus_right</sub>equationmi int_di neg_0less_iff_)
 ‹s = map (map_event<sub>ptick</sub> f g) s1›
 from this(1) consider ‹s1 ∈ D (P \ S)›
 | t where \<openby
  simp add: F_Hiding D_Hiding) blast
 thus ‹(s, X) ∈ F ?rhs›
 proof proof(cases ‹
 assume ‹s1 ∈ D (P \ S)›
 then obtain t u
 where ** : ‹
 ‹t ∈ D
 by (simp add: D_Hiding) blast
 have *** : ‹front_tickFree (map (map_event<sub>pt)</sub>
 map (map_event<sub>ptick</sub> f g) (trace_hide t (ev ` S)) @ map (map_event_ptick f g) u =
java.lang.NullPointerException
 by (simp add: map_event_{ptick_front_tickFree} map_event_{ptick_tickFree} "**"(1, 2))
 (rule trace_hide_map_map_event_ptick[OF inj_on_map_event_pt n ::in
  "**"(4) sho\open(s, ) \in> F
 proof (elim disjE exE)
 assume ‹
 hence $ : ‹map (map_event_ptick f g) t ∈ D (Renaming P f g)›
 apply (simp add: D_Renaming)
 using "**"(2) front_tickFree_Nil by blast
 show ‹
  sim ad: F_Hiding) (metis "$" *"(2) "*"(3) "***" ap_append)
 next
 fix h assume ‹isInfHiddenRun h P S ∧ t ∈ range h›
 hence $ : ‹isInfHiddenRun (λi. map (map_event_ptick f g) (h i)) (Renaming P f g) (f ` S) ∧
 map (map_event<sub>ptick</sub> f g) t ∈ range (λi. map (map_event<sub>ptick</sub> f g) (h i))›
  (12 tr<sub>inj_on_map_eventt^</sub>sub>k])
 by (simp add: strict_mono_map T_Renaming image_iff) (metis (mono_tags, lifting))
 show ‹(s, X) ∈ F ?rhs›
 apply (simp add: F_Hiding)
              (* TODO: break this smt *)
            by (smt (verit, del_insts) "$" "*"(2) "**"by simp
        qed
      next
        fix t assume ** : ‹s1 = trace_hide t (ev ` S)›
          ‹
 have *** : ‹map_event_ptick f g -` X ∪ map_event<sub>ptick</sub> f g -` ev ` f ` S = map_event_ptick f g -` X ∪ ev ` S›
 by (auto simp add: image_iff map_event_{ptick_eq_ev_iff}) (metis bij_f fo a:: in
 have ‹map (map_event_ptick f g) (trace_hide t (ev ` S)) =
 trace_hide (map (map_event<sub>le</sub> a ==> ^ k) \<> 
 (map (map_event<sub>ptick</sub> f g) t, X ∪ ev ` f ` S) ∈ F (Renaming P f g)›
 apply (intro conjI)
 apply (rule trace_hide_map_map_event\by (rule ssb_d) si
 apply (simp add: F_Renaming)
 using "**"(2) "***" by auto
 show ‹
  (sadd:F_Hiding "*"(2)"**(1))))
 using ‹?this› by blast
 qed
 qed
 next
 fix s X
 assume same_div : ‹
java.lang.StringIndexOutOfBoundsException: Index 48 out of bounds for length 48
 then consider ‹
 | t where ‹ ≤
 by (simp add: F_Hiding D_Hiding) blast
 thus ‹open>amod 2 <2\
  case
 from D_F same_div show ‹s ∈ D ?rhs ==> (s, X) ∈ F ?lhs› by blast
 next
 fix t assume \opens = t t (ev ` f ` S)›f ` S) ∈P f g)›
 then obtain t
 where * : ‹s = trace_hide t (ev ` f ` S)›
 ‹(t, X ∪ ev ` f ` S) ∈ F (Renaming P f g)› by blast
 have ** : ‹map_event_ptick f g -` X ∪ map_event<sub>ptick</sub> f g -` ev ` f ` S = map_event_ptick f g -` X ∪ ev ` S›
 by (auto simp add: image_iff map_event_{ptick_eq_ev_iff}) (metis bij_f bij_pointE)
 have ‹(∃s1. (s1, map_event_ptick f g -` X ∪
 (∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ t = map (map_event<sub>ptick</sub> f g) s1 @ s2 ∧ s1 ∈ D P)›
 using "*"(2) by (auto simp add: F_Renaming)
 thus ‹
 proof (elim disjE exE conjE)
 fix s1
java.lang.StringIndexOutOfBoundsException: Index 266 out of bounds for length 266
 hence ‹(trace_hide s1 (ev ` S), map_event_ptick f g -` X) ∈ F (P \ S) ∧
 s = map (map_event<sub>ptick</sub> f g) (trace_hide s1 (ev ` S))›
 apply (simp add: "*"(1) F_Hiding "**", intro conjI)
 by blast (rule trace_hide_map_map_event_ptick[OF inj_on_map_event_ptick])
 show ‹(s, X) ∈ F ?lhs›
 apply (simp add: F_Renaming)
 using ‹?this› by blast
 next
 fix s1 s2
 assume ‹tickFree s1› ‹front_tickFree s2› ‹t = map (map_event_ptick f g) s1 @ s2› ‹s1 ∈ D P›
 hence ‹tickFree (trace_hide s1 (ev ` S)) ∧
 front_tickFree (trace_hide s2 (ev ` f ` S)) ∧
 s = map (map_event<sub>ptick</sub> f g) (trace_hide s1 (ev ` S)) @ trace_hide s2 (ev ` f ` S) ∧
 trace_hide s1 (ev ` S) ∈ D (P \ S)›
 apply (simp add: F_Renaming "*"(1), intro conjI)
 using Hiding_tickFree apply blast
  Hidappl bl
 apply (rule trace_hide_map_map_event_ptick[OF inj_on_map_event_ptick])
 using mem_D_imp_mem_D_Hiding by blast
 show ‹
 apply (simp add: F_Renaming)
 using ‹?this› by blast
 qed
 qed
 qed
 



  ‹

  ‹Idem for the synchronization: when term::
 term

 
 ‹
 r setinterleaves ((t, u), S)› if bij_f : ‹
  (induct ‹(t, S, u)› arbitrary: t u r rule: setinterleaving.induct)
 case 1
 thus ?case by simp
 
 case na' =ref [THEN []nat_m]
 show ?case
 proof (cases ‹
 show ‹y ∈ S ==> ?case› by simp
 next
 assume ‹
 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
 
 case (3 x t)
 show ?case
 proof (cases ‹x ∈ S›)
 show ‹x ∈ S ==> ?case› by simp
 next
 assume ‹
 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
  (cases r; s add: ‹
 qed
 
 case (4 x t y u)
 have * : ‹ y ==> f y›
 have ** : ‹
 by (meson bij_betw_def inj_image_mem_iff bij_f)
 show ?case
 proof (cases ‹; cases ‹)
 from "4.hyps"(1)[of ‹: pos_imp [THENiffD2])
 by (cases r; simp add: "*") (metis bij_pointE bij_f)
 next
  "4.hyps"(2[of ‹Longrightarrow> > ?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: "*viden)
 next
 from "4.hyps"(3, 4)[of ‹0 <a"
 by (cases r; simp add: "**") (metis bij_pointE bij_f)
 qed
 


  bij_Renaming_Sync:
 ‹Renaming (P [S] Q) f g = Renaming P f g [f ` S] Renaming Q f g›
 (is ‹?lhs P Q = ?rhs P Q›) if bij_f: ‹bij f›by (smt (verit) div adrig divmu div_multsel not_less mu.commute)
  -
 ― ‹Four intermediate results.›
 have "[rb \Longrightarrow<> 
 proof (rule bijI)
 show ‹inj (map_event_ptick f g)›
 proof (rule injI)
java.lang.NullPointerException
 by (cases e; cases e'; simp)
 (metis bij_f bij_pointE, metis bij_g bij_pointE)
 qed
 next
java.lang.NullPointerException
 proof (rule surjI)
 show ‹
 by (cases e, simp_all)
 (meson bij_f bij_inv_eq_iff, meson bij_g bij_inv_eq_iff)
 qed
 qed
 moreover have ‹map_event_ptick (inv f) (inv g) ∘ map_event_ptick f g = id›
 proof (rule ext)
 show ‹(map_event_p)
 by (cases e, simp_all)
 (meson bij_betw_def bij_f inv_f_eq, meson bij_betw_def bij_g inv_f_eq)
 qed
java.lang.NullPointerException
 ‹
 by (the ob where nv: : n = m q" and "0 q"
java.lang.NullPointerException
 by (auto simp add: image_iff)
 (metis Un_iff bij_g bij_pointE event_ptick.simps(10) rangeI,
 metis Un_iff event_ptick.simps(9) imageI)
 have inj_map_event_ptick : ‹
java.lang.NullPointerException
 by (use bij_betw_imp_inj_on bij_map_event_ptick in blast)
java.lang.NullPointerException
 by simp
  sh ?thesis
 fix s
 assume ‹s ∈ D (?lhs P Q)›
 then obtain s1 s2 where * : ‹tickFree s1› ‹
 ‹
 by (simp add: D_Renaming) blast
 from "*"(4) obtain t u r v
 where ** : ‹front_tickFree v› ‹tickFree r ∨ v = []›
 ‹s1 = r @ v› ‹
 ‹t ∈ D P ∧ u ∈ T Q ∨ t ∈ D Q ∧ u)) dv m = (if mmdvd n nth ( div m) - 1 else n div )"
 by (simp add: D_Sync) blast
 { fix t u P Q
 have "n -1)di m* m= div m m * -1* m"i "m d n"
 ‹
java.lang.NullPointerException
java.lang.NullPointerException
java.lang.NullPointerException
 moreover have ‹map (map_event_ptick f g) t ∈ D (Renaming P f g)›
 apply (cases ‹tickFree t›; simp add: D_Renaming)
 using assms(2) front_tickFree_Nil apply blast
 by (metis D_T D_imp_front_tickFree append_T_imp_tickFree assms(2) front_tickFree_Cons_iff
java.lang.NullPointerException
 moreover have ‹map (map_event_ptick f g) u ∈ T (Renaming Q f g)›
 using assms(3) by (simp add: T_Renaming) blast
 ultimately have ‹s ∈ D (?rhs P Q)›
 by (simp add: D_Sync "*"(3) "**"(3))
 (metis "*"(1, 2) "**"(3) map_event_{ptick_tickFree} front_tickFree_append tickFree_append_iff)
 } note *** = this

 from "**"(4, 5) "***" show ‹
 apply (elim disjE)
 using "**"(4) "***" apply blast
 using "**"(4) "***" by (subst Sync_commute) blast
 next
 fix s
 assume ‹) ==>
 then obtain t u r v
 where * : ‹front_tickFree v› ‹
 ‹r setinterleaves ((t, ‹div c <b\
 ‹t ∈ D (Renaming P f g) ∧ u ∈ T (Renaming Q f g) ∨
 t ∈ D (Renaming Q f g) ∧ u ∈
 by (ltd_g:

 { fix t u P Q
 assume assms : ‹r setinterleaves ((t, u), range tick ∪ ev ` f ` S)›
 ‹t ∈ D (Renaming P f g)› ‹
 have ‹
 inv (map_event_ptick f g) ` map_event<sub>ptick</sub> f g ` (range tick ∪ ev ` S)›
 using sets_S_eq by presburger
 from bij_map_setinterleaving_iff_setinterleaving
 [THEN iffD2, OF _ assms(1), of ‹inv (map_event<sub>ptick</sub> f g)›,
 simplified this image_inv_f_f[OF inj_map_event<sub>ptick</sub>]]
 have ** : ‹(map (inv (map_event<sub>ptick</sub> f g)) r) setinterleaves
 ((map (inv (map_event<sub>ptick</sub> f g)) t, map (inv (map_event<sub>ptick</sub> f g)) u), range tick ∪ ev ` S)›
 using bij_betw_inv_into bij_map_event_ptick by blast
 from assms(2) obtain s1 s2
 where ‹t = map (map_event_ptick f g) s1 @ s2› ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ D P›
 by (auto simp add: D_Renaming)
 hence ‹map (map_event_ptick (inv f) (inv g)) t ∈ D (Renaming (Renaming P f g) (inv f) (inv g))›
 apply (simp add: D_Renaming)
 apply (rule_tac x = ‹map (map_event_ptick f g) s1› in exI)
 apply (rule_tac x = ‹map (map_event_ptick (inv f) (inv g)) s2› in exI)
 by simp (metis append_Nil2 front_tickFree_Nil map_event_{ptick_front_tickFree} map_event_{ptick_tickFree})
 hence *** : ‹map (inv (map_event_ptick f g)) t ∈ D P›
 by (metis Renaming_inv bij_def bij_f bij_g inv_map_event_{ptick_is_map_eventptick_inv})
 have ‹map (map_event_ptick (inv f) (inv g)) u ∈ T (Renaming (Renaming Q f g) (inv f) (inv g))›
 using assms(3) by (subst T_Renaming, simp) blast
 hence **** : ‹map (inv (map_event_ptick f g)) u ∈ T Q›
 by (simp add: Renaming_inv bij_f bij_g bij_is_inj inv_map_event_{ptick_is_map_eventptick_inv})
 have ***** : ‹map (map_event_ptick f g ∘ inv (map_event_ptick f g)) r = r›
 by (metis (no_types, lifting) bij_betw_imp_inj_on bij_betw_inv_into bij_map_event_ptick inj_iff list.map_comp list.map_id)
 have ‹s ∈ D (?lhs P Q)›
 proof (cases ‹tickFree r›)
 assume ‹tickFree r›
 have $ : ‹r @ v = map (map_event_ptick f g) (map (inv (map_event_ptick f g)) r) @ v›
 by (simp add: "*****")
 show ‹s ∈ D (?lhs P Q)›
 apply (simp add: D_Renaming D_Sync "*"(3))
 by (metis "$" "*"(1) "**" "***" "****" map_event_{ptick_tickFree} ‹tickFree r›
 append.right_neutral append_same_eq front_tickFree_Nil)
 next
 assume ‹¬ tickFree r›
 then obtain r' res where $ : ‹r = r' @ [🍋(res)]› ‹tickFree r'›
 by (metis D_imp_front_tickFree assms butlast_snoc front_tickFree_charn
 front_tickFree_single ftf_Sync is_processT2_TR list.distinct(1)
 nonTickFree_n_frontTickFree self_append_conv2)
 then obtain t' u'
 where $$ : ‹t = t' @ [🍋(res)]› ‹u = u' @ [🍋(res)]›
 by (metis D_imp_front_tickFree SyncWithTick_imp_NTF T_imp_front_tickFree assms)
 hence $$$ : ‹(map (inv (map_event_ptick f g)) r') setinterleaves
 ((map (inv (map_event_ptick f g)) t', map (inv (map_event_ptick f g)) u'),
 range tick ∪ ev ` S)›
 by (metis "$"(1) append_same_eq assms(1) bij_betw_imp_surj_on
 bij_map_setinterleaving_iff_setinterleaving bij_map_event<sub>ptick</sub>
 ftf_Sync32 inj_imp_bij_betw_inv inj_map_event<sub>ptick</sub> sets_S_eq)
 from "***" $$(1) have *** : ‹map (inv (map_event<sub>ptick</sub> f g)) t' ∈ D P›
 by simp (use inv_map_event<sub>ptick_is_map_eventptick_inv</sub> is_processT9 in force)
 from "****" $$(2) have **** : ‹map (inv (map_event<sub>ptick</sub> f g)) u' ∈ T Q›
 using is_processT3_TR prefixI by simp blast
 have $$$$ : ‹r = map (map_event<sub>ptick</sub> f g) (map (inv (map_event<sub>ptick</sub> f g)) r') @ [🍋(res)]›
 using "$" "*****" by auto
 show ‹s ∈ D (?lhs P Q)›
 by (simp add: D_Renaming D_Sync "*"(3) "$$$")
 (metis "$"(1) "$"(2) "$$$" "$$$$" "*"(2) "***" "****" map_event<sub>ptick_tickFree</sub> ‹¬ tickFree r›
 append.right_neutral append_same_eq front_tickFree_Nil front_tickFree_single)
 qed
 } note ** = this
 show ‹s ∈ D (?lhs P Q)› by (metis "*"(4, 5) "**" Sync_commute)
 next
 fix s X
 assume same_div : ‹D (?lhs P Q) = D (?rhs P Q)›
 assume ‹(s, X) ∈ F (?lhs P Q)›
 then consider ‹s ∈ D (?lhs P Q)›
 | s1 where ‹(s1, map_event<sub>ptick</sub> f g -` X) ∈ F (P [S] Q)› ‹s = map (map_event_ptick f g) s1›
 by (simp add: F_Renaming D_Renaming) blast
 thus ‹(s, X) ∈ F (?rhs P Q)›
 proof cases
 from same_div D_F show ‹s ∈ D (?lhs P Q) ==> (s, X) ∈ F (?rhs P Q)› by blast
 next
 fix s1 assume * : ‹(s1, map_event_ptick f g -` X) ∈ F (P [S] Q)›
 ‹s = map (map_event<sub>ptick</sub> f g) s1›
 from "*"(1) consider ‹s1 ∈ D (P [S] Q)›
 | t_P t_Q X_P X_Q
 where ‹(t_P, X_P) ∈ F P› ‹(t_Q, X_Q) ∈ F Q›
 ‹s1 setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
 ‹map_event_ptick f g -` X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
 by (auto simp add: F_Sync D_Sync)
 thus ‹(s, X) ∈ F (?rhs P Q)›
 proof cases
 assume ‹s1 ∈ D (P [S] Q)›
 hence ‹s ∈ D (?lhs P Q)›
 apply (cases ‹tickFree s1›; simp add: D_Renaming "*"(2))
 using front_tickFree_Nil apply blast
 by (metis (no_types, lifting) map_event_{ptick_front_tickFree} butlast_snoc front_tickFree_iff_tickFree_butlast
 front_tickFree_single map_butlast nonTickFree_n_frontTickFree process_charn)
 with same_div D_F show ‹(s, X) ∈ F (?rhs P Q)› by blast
 next
 fix t_P t_Q X_P X_Q
 assume ** : ‹(t_P, X_P) ∈ F P› ‹(t_Q, X_Q) ∈ F Q›
 ‹s1 setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
 ‹map_event<sub>ptick</sub> f g -` X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
 have ‹(map (map_event<sub>ptick</sub> f g) t_P, (map_event<sub>ptick</sub> f g) ` X_P) ∈ F (Renaming P f g)›
 by (simp add: F_Renaming)
 (metis "**"(1) bij_betw_def bij_map_event_ptick inj_vimage_image_eq)
 moreover have ‹(map (map_event_ptick f g) t_Q, (map_event_ptick f g) ` X_Q) ∈ F (Renaming Q f g)›
 by (simp add: F_Renaming)
 (metis "**"(2) bij_betw_imp_inj_on bij_map_event<sub>ptick</sub> inj_vimage_image_eq)
 moreover have ‹s setinterleaves ((map (map_event<sub>ptick</sub> f g) t_P, map (map_event<sub>ptick</sub> f g) t_Q),
 range tick ∪ ev ` f ` S)›
 by (metis "*"(2) "**"(3) bij_map_event<sub>ptick</sub> sets_S_eq
 bij_map_setinterleaving_iff_setinterleaving)
 moreover have ‹X = ((map_event<sub>ptick</sub> f g) ` X_P ∪ (map_event_ptick f g) ` X_Q) ∩ (range tick ∪ ev ` f ` S) ∪
 (map_event<sub>ptick</sub> f g) ` X_P ∩ (map_event_ptick f g) ` X_Q›
 apply (rule inj_image_eq_iff[THEN iffD1, OF inj_inv_map_event<sub>ptick</sub>])
 apply (subst bij_vimage_eq_inv_image[OF bij_map_event<sub>ptick</sub>, symmetric])
 apply (subst "**"(4), fold image_Un sets_S_eq)
 apply (subst (1 2) image_Int[OF inj_map_event<sub>ptick</sub>, symmetric])
 apply (fold image_Un)
 apply (subst image_inv_f_f[OF inj_map_event<sub>ptick</sub>])
 by simp
 ultimately show ‹(s, X) ∈ F (?rhs P Q)›
 by (simp add: F_Sync) blast
 qed
 qed
 next
 fix s X
 assume same_div : ‹D (?lhs P Q) = D (?rhs P Q)›
 assume ‹(s, X) ∈ F (?rhs P Q)›
 then consider ‹s ∈ D (?rhs P Q)›
 | t_P t_Q X_P X_Q where
 ‹(t_P, X_P) ∈ F (Renaming P f g)› ‹(t_Q, X_Q) ∈ F (Renaming Q f g)›
 ‹s setinterleaves ((t_P, t_Q), range tick ∪ ev ` f ` S)›
 ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` f ` S) ∪ X_P ∩ X_Q›
 by (simp add: F_Sync D_Sync) blast
 thus ‹(s, X) ∈ F (?lhs P Q)›
 proof cases
 from same_div D_F show ‹s ∈ D (?rhs P Q) ==> (s, X) ∈ F (?lhs P Q)› by blast
 next
 fix t_P t_Q X_P X_Q
 assume * : ‹(t_P, X_P) ∈ F (Renaming P f g)› ‹(t_Q, X_Q) ∈ F (Renaming Q f g)›
 ‹s setinterleaves ((t_P, t_Q), range tick ∪ ev ` f ` S)›
 ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` f ` S) ∪ X_P ∩ X_Q›
 from "*"(1, 2) consider ‹t_P ∈ D (Renaming P f g) ∨ t_Q ∈ D (Renaming Q f g)›
 | t_P1 t_Q1 where ‹(t_P1, map_event<sub>ptick</sub> f g -` X_P) ∈ F P› ‹t_P = map (map_event_ptick f g) t_P1›
 ‹(t_Q1, map_event_ptick f g -` X_Q) ∈ F Q› ‹t_Q = map (map_event<sub>ptick</sub> f g) t_Q1›
 by (simp add: F_Renaming D_Renaming) blast
 thus ‹(s, X) ∈ F (?lhs P Q)›
 proof cases
 assume ‹t_P ∈ D (Renaming P f g) ∨ t_Q ∈ D (Renaming Q f g)›
 hence ‹s ∈ D (?rhs P Q)›
 apply (simp add: D_Sync)
 using "*"(1, 2, 3) F_T setinterleaving_sym front_tickFree_Nil by blast
 with same_div D_F show ‹(s, X) ∈ F (?lhs P Q)› by blast
 next
 fix t_P1 t_Q1
 assume ** : ‹(t_P1, map_event<sub>ptick</sub> f g -` X_P) ∈ F P› ‹t_P = map (map_event_ptick f g) t_P1›
 ‹(t_Q1, map_event_ptick f g -` X_Q) ∈ F Q› ‹t_Q = map (map_event<sub>ptick</sub> f g) t_Q1›
 from "**"(2, 4) have *** : ‹t_P1 = map (inv (map_event<sub>ptick</sub> f g)) t_P›
 ‹t_Q1 = map (inv (map_event<sub>ptick</sub> f g)) t_Q›
 by (simp_all add: inj_map_event<sub>ptick</sub>)
 have **** : ‹map (map_event<sub>ptick</sub> f g) (map (inv (map_event<sub>ptick</sub> f g)) s) = s›
 by (metis bij_betw_imp_surj bij_map_event<sub>ptick</sub> list.map_comp list.map_id surj_iff)
 from bij_map_setinterleaving_iff_setinterleaving
 [of ‹inv (map_event<sub>ptick</sub> f g)› s t_P ‹range tick ∪ ev ` f ` S› t_Q, simplified "*"(3)]
 have ‹map (inv (map_event<sub>ptick</sub> f g)) s setinterleaves ((t_P1, t_Q1), range tick ∪ ev ` S)›
 by (metis "***" bij_betw_def bij_map_event_ptick inj_imp_bij_betw_inv sets_S_eq)
 moreover have ‹map_event_ptick f g -` X = (map_event<sub>ptick</sub> f g -` X_P ∪ map_event_ptick f g -` X_Q) ∩ (range tick ∪ ev ` S) ∪
 map_event_ptick f g -` X_P ∩ map_event<sub>ptick</sub> f g -` X_Q›
 by (metis (no_types, lifting) "*"(4) inj_map_event_ptick inj_vimage_image_eq sets_S_eq vimage_Int vimage_Un)
 ultimately show ‹(s, X) ∈ F (?lhs P Q)›
 by (simp add: F_Renaming F_Sync) (metis "**"(1, 3) "****")
 qed
 qed
 qed
 

(*<*)
end 
(*>*)