Theory Renaming

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

chapter‹ The Renaming Operator ›

(*<*)
theory  Renaming
  imports Process
begin
  (*>*)

section‹Some preliminaries›

term ‹f -` B› (* instead of defining our own antecedent function *)

definition finitary :: ‹('a ⇒ 'b) ⇒ bool› 
  where ‹finitary f ≡ ∀x. finite(f -` {x})›

(* 
definition finitaryExt :: ‹('a ⇒ ('b, 'r) event⇩p⇩t⇩i⇩c⇩k) ⇒ bool› 
  where ‹finitaryExt f ≡ ∀x. finite(f -` {ev x})›

 *)

text ‹We start with some simple results.›

lemma ‹f -` {} = {}› by simp

lemma ‹X ⊆ Y ⟹ f -` X ⊆ f -` Y› by (rule vimage_mono)

lemma ‹f -`(X ∪ Y) = f -` X ∪ f -` Y› by (rule vimage_Un)


lemma map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff   : ‹map_event⇩p⇩t⇩i⇩c⇩k f g e = ev b ⟷ (∃a. e = ev a   ∧ b = f a)›
  and map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff : ‹map_event⇩p⇩t⇩i⇩c⇩k f g e = ✓(s) ⟷ (∃r. e = ✓(r) ∧ s = g r)›
  and ev_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff   : ‹ev b = map_event⇩p⇩t⇩i⇩c⇩k f g e ⟷ (∃a. e = ev a   ∧ b = f a)›
  and tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff : ‹✓(s) = map_event⇩p⇩t⇩i⇩c⇩k f g e ⟷ (∃r. e = ✓(r) ∧ s = g r)›
  by (cases e; auto)+


lemma inj_left_map_event⇩p⇩t⇩i⇩c⇩k: ‹inj (λf. map_event⇩p⇩t⇩i⇩c⇩k f g)›
proof (intro injI ext)
  show ‹map_event⇩p⇩t⇩i⇩c⇩k f1 g = map_event⇩p⇩t⇩i⇩c⇩k f2 g ⟹ f1 a = f2 a› for f1 f2 :: ‹'a ⇒ 'b› and a :: 'a
    by (drule fun_cong[where x = ‹ev a›]) simp
qed

lemma inj_right_map_event⇩p⇩t⇩i⇩c⇩k: ‹inj (map_event⇩p⇩t⇩i⇩c⇩k f)›
proof (intro injI ext)
  show ‹map_event⇩p⇩t⇩i⇩c⇩k f g1 = map_event⇩p⇩t⇩i⇩c⇩k f g2 ⟹ g1 r = g2 r› for g1 g2 :: ‹'r ⇒ 's› and r :: 'r
    by (drule fun_cong[where x = ‹✓(r)›]) simp
qed


lemma map_event⇩p⇩t⇩i⇩c⇩k_tickFree : ‹tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) s) ⟷ tickFree s›
  by (induct s) (simp_all add: event⇩p⇩t⇩i⇩c⇩k.case_eq_if)

lemma map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree : ‹front_tickFree (map (map_event⇩p⇩t⇩i⇩c⇩k f g) s) ⟷ front_tickFree s›
  by (simp add: front_tickFree_iff_tickFree_butlast map_butlast[symmetric] map_event⇩p⇩t⇩i⇩c⇩k_tickFree)


lemma map_map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff :
  ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) t = [✓(s)] ⟷ (∃r. s = g r ∧ t = [✓(r)])›
  and tick_eq_map_map_event⇩p⇩t⇩i⇩c⇩k_iff :
  ‹[✓(s)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t ⟷ (∃r. s = g r ∧ t = [✓(r)])› 
  by (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)


section‹The Renaming Operator Definition›

text ‹Our new renaming operator does not only deal with events but also with termination.›

lift_definition Renaming :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a ⇒ 'b, 'r ⇒ 's] ⇒ ('b, 's) process⇩p⇩t⇩i⇩c⇩k›
  is ‹λP f g. ({( map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1, X)| s1 X. (s1, (map_event⇩p⇩t⇩i⇩c⇩k f g) -` X) ∈ ℱ P} ∪
               {((map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1) @ s2, X)| s1 s2 X. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ 𝒟 P},
               {( map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1) @ s2| s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ 𝒟 P})›
proof -
  show ‹?thesis P f g› (is ‹is_process(?f, ?d)›) for P f g
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI allI impI)
    show ‹([], {}) ∈ ?f›
      by (simp add: process_charn)
  next
    show ‹(s, X) ∈ ?f ⟹ front_tickFree s› for s X
      by (auto simp add: F_imp_front_tickFree map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree
          map_event⇩p⇩t⇩i⇩c⇩k_tickFree front_tickFree_append)
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
    proof (induct t rule: rev_induct)
      case Nil thus ‹(s, {}) ∈ ?f› by simp
    next
      case (snoc e t)
      from snoc.prems is_processT8 
      consider (fail) s1 where ‹s @ t @ [e] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1› ‹(s1, {}) ∈ ℱ P›
        | (div) s1 s2 where ‹s @ t @ [e] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s2 ≠ []›
          ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ 𝒟 P› by auto blast
      thus ‹(s, {}) ∈ ?f›
      proof cases
        case fail
        from fail(1) obtain s1' e' where ‹s1 = s1' @ [e']› ‹s @ t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1'›
          by (metis Nil_is_append_conv butlast_append list.map_disc_iff map_butlast snoc_eq_iff_butlast)
        from this(1) fail(2) is_processT3 have ‹(s1', {}) ∈ ℱ P› by blast
        with ‹s @ t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1'› have ‹(s @ t, {}) ∈ ?f› by auto
        with snoc.hyps show ‹(s, {}) ∈ ?f› by presburger
      next
        case div
        from div(2) obtain s2' e' where ‹s2 = s2' @ [e']› by (meson rev_exhaust)
        with div(1, 3, 4, 5) ‹s2 = s2' @ [e']› front_tickFree_dw_closed 
        have ‹(s @ t, {}) ∈ ?f› by simp blast
        with snoc.hyps show ‹(s, {}) ∈ ?f› by presburger
      qed
    qed
  next
    show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
      by (induct s rule: rev_induct, simp_all)
        (meson is_processT4 vimage_mono)+
  next
    show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟹ (s, X ∪ Y) ∈ ?f› for s X Y
      by auto (metis (no_types, lifting) is_processT5 list.simps(8, 9) map_append vimageE)
  next
    fix s r X assume ‹(s @ [✓(r)], {}) ∈ ?f›
    then consider (fail) s1 where ‹s @ [✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1› ‹(s1, {}) ∈ ℱ P›
      | (div) s1 s2 where ‹s @ [✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2› ‹s2 ≠ []›
        ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ 𝒟 P›
      using is_processT8 by auto blast
    thus ‹(s, X - {✓(r)}) ∈ ?f›
    proof cases
      case fail
      from fail(1) obtain s1' r' where * : ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1'› ‹s1 = s1' @ [✓(r')]› ‹r = g r'›
        by (simp add: append_eq_map_conv) (metis (mono_tags, opaque_lifting) map_map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
      from this(2) fail(2) have ‹(s1', map_event⇩p⇩t⇩i⇩c⇩k f g -` X - {✓(r')}) ∈ ℱ P› 
        by (simp add: is_processT6)
      hence  ‹(s1', map_event⇩p⇩t⇩i⇩c⇩k f g -` (X - {✓(r)})) ∈ ℱ P›
        by (rule is_processT4) (auto simp add: ‹r = g r'›)
      thus ‹(s, X - {✓(r)}) ∈ ?f› by (unfold "*"(1)) blast
    next
      case div
      from div(2, 4) front_tickFree_charn tickFree_imp_front_tickFree
      obtain s2' e' where ‹s2 = s2' @ [e']› ‹front_tickFree s2'› by blast
      from ‹s2 = s2' @ [e']› div(1) have ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2'› by simp
      with div(3, 5) ‹front_tickFree s2'› show ‹(s, X - {✓(r)}) ∈ ?f› by blast
    qed
  next
    show ‹s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ ?d› for s t
      using front_tickFree_append by safe auto
  next
    show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X by blast

  next
    fix s r assume ‹s @ [✓(r)] ∈ ?d›
    then obtain s1 s2 where * : ‹s @ [✓(r)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2›
      ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ 𝒟 P› by blast
    from "*"(1, 2, 3) obtain s2' e where ‹s2 = s2' @ [e]› ‹front_tickFree s2'›
      by (metis append_self_conv front_tickFree_charn front_tickFree_dw_closed
          non_tickFree_tick map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
    from this(1) "*"(1) have ‹s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ s2'› by simp
    with "*"(2, 4) ‹front_tickFree s2'› show ‹s ∈ ?d› by blast
  qed
qed



text ‹Some syntactic sugar.›

syntax
  "_Renaming"  :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ updbinds ⇒ updbinds ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (‹_ ⟦_⟧ ⟦_⟧› [100, 100, 100]) (*see the values we need, at least 51*)
  "_Renaming_left"   :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ updbinds ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (‹_ ⟦_⟧ ⟦⟧› [100, 100])
  "_Renaming_right"  :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ updbinds ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (‹_ ⟦⟧ ⟦_⟧› [100, 100])
syntax_consts "_Renaming" ⇌ Renaming
  and         "_Renaming_left" ⇌ Renaming
  and         "_Renaming_right" ⇌ Renaming
translations
  "_Renaming P f_updates g_updates" ⇌ "CONST Renaming P (_Update (CONST id) f_updates) (_Update (CONST id) g_updates)"
  "_Renaming_left  P f_updates" ⇌ "CONST Renaming P (_Update (CONST id) f_updates) (CONST id)"
  "_Renaming_right P g_updates" ⇌ "CONST Renaming P (CONST id) (_Update (CONST id) g_updates)"

text ‹Now we can write \<^term>‹P ⟦a := b⟧ ⟦c := d⟧›.
      If we only want to rename events, or results, we use respectively
      \<^term>‹P ⟦a := b⟧ ⟦⟧› and  \<^term>‹P ⟦⟧ ⟦c := d⟧›. 
      Like in \<^theory>‹HOL.Fun›, we can write this kind of expression with as many
      updates we want: \<^term>‹P⟦a := b, c := d, e := f, g := h⟧ ⟦r1 := r2, r3 := r4⟧›.
      By construction we also inherit all the results about \<^const>‹fun_upd›, for example
      @{thm fun_upd_other fun_upd_upd fun_upd_twist}.›

lemma ‹P ⟦x := y, x := z⟧ ⟦⟧ = P⟦x := z⟧ ⟦⟧› by simp

lemma ‹a ≠ c ⟹ P ⟦a := b, c := d⟧ ⟦r1 := r2⟧ = P ⟦c := d, a := b⟧ ⟦r1 := r2⟧› by (simp add: fun_upd_twist)




section‹The Projections›

lemma F_Renaming: ‹ℱ (Renaming P f g) = 
  {( map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1, X)| s1 X. (s1, (map_event⇩p⇩t⇩i⇩c⇩k f g) -` X) ∈ ℱ P} ∪
  {((map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1) @ s2, X)| s1 s2 X. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ 𝒟 P}›
  by (simp add: Failures.rep_eq FAILURES_def Renaming.rep_eq)

lemma D_Renaming: ‹𝒟 (Renaming P f g) =
  {(map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1) @ s2| s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ 𝒟 P}›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Renaming.rep_eq)

lemma T_Renaming: ‹𝒯 (Renaming P f g) = 
  { map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1| s1. s1 ∈ 𝒯 P} ∪
  {(map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1) @ s2| s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ 𝒟 P}›
  by (subst set_eq_iff, fold T_F_spec, simp add: F_Renaming)

lemmas Renaming_projs = F_Renaming D_Renaming T_Renaming



section‹Continuity Rule›

subsection ‹Monotonicity of \<^const>‹Renaming›.›

lemma mono_Renaming : ‹Renaming P f g ⊑ Renaming Q f g› if ‹P ⊑ Q›
proof (subst le_approx_def, intro conjI subset_antisym allI impI subsetI)
  show ‹s ∈ 𝒟 (Renaming Q f g) ⟹ s ∈ 𝒟 (Renaming P f g)› for s
    unfolding D_Renaming using le_approx1 ‹P ⊑ Q› by blast
next
  show ‹s ∉ 𝒟 (Renaming P f g) ⟹ X ∈ ℛ⇩a (Renaming P f g) s ⟹ X ∈ ℛ⇩a (Renaming Q f g) s› for s X
    by (simp add: D_Renaming Refusals_after_def F_Renaming)
      (metis (no_types, opaque_lifting) F_imp_front_tickFree append.right_neutral front_tickFree_Nil
        front_tickFree_append_iff front_tickFree_single is_processT9 map_append tickFree_Nil
        map_map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff nonTickFree_n_frontTickFree non_tickFree_tick proc_ord2a ‹P ⊑ Q›)
next
  show ‹s ∉ 𝒟 (Renaming P f g) ⟹ X ∈ ℛ⇩a (Renaming Q f g) s ⟹ X ∈ ℛ⇩a (Renaming P f g) s› for s X
    by (simp add: D_Renaming Refusals_after_def F_Renaming)
      (metis (no_types, lifting) is_processT8 le_approx1 proc_ord2a subset_eq ‹P ⊑ Q›) 
next
  show ‹s ∈ min_elems (𝒟 (Renaming P f g)) ⟹ s ∈ 𝒯 (Renaming Q f g)› for s
    apply (rule set_mp[of ‹{map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 |s1. s1 ∈ min_elems (𝒟 P)}›])
     apply (simp add: T_Renaming, use le_approx3 ‹P ⊑ Q› in blast)
    apply (drule set_rev_mp[of _ _ ‹min_elems {map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 |s1. tickFree s1 ∧ s1 ∈ 𝒟 P}›])
     apply (simp_all add: D_Renaming min_elems_def subset_iff)
    by (metis prefixI antisym_conv2 append.right_neutral front_tickFree_Nil)
      (metis (no_types, lifting) antisym_conv2 append_butlast_last_id 
        front_tickFree_iff_tickFree_butlast less_self list.map_disc_iff map_butlast
        min_elems1 min_elems_no nil_less order_less_imp_le tickFree_imp_front_tickFree)
qed


lemma ‹{ev c |c. f c = a} = ev`{c . f c = a}› by (rule setcompr_eq_image)


lemma vimage_map_event⇩p⇩t⇩i⇩c⇩k_subset_vimage: ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` (ev ` A) ⊆ range tick ∪ (ev ` (f -` A))›
  and vimage_subset_vimage_map_event⇩p⇩t⇩i⇩c⇩k: ‹(ev ` (f -` A)) ⊆ (map_event⇩p⇩t⇩i⇩c⇩k f g -` (ev ` A)) - range tick›
  by (auto simp add: image_def vimage_def)
    (metis event⇩p⇩t⇩i⇩c⇩k.exhaust_sel event⇩p⇩t⇩i⇩c⇩k.sel(1) event⇩p⇩t⇩i⇩c⇩k.simps(9))




subsection ‹Some useful results about \<^const>‹finitary›, and preliminaries lemmas for continuity.›

lemma inj_imp_finitary[simp] : ‹inj f ⟹ finitary f› by (simp add: finitary_def finite_vimageI)

lemma finitary_comp_iff : ‹finitary g ⟹ finitary (g o f) ⟷ finitary f›
proof (unfold finitary_def, intro iffI allI;
    (subst vimage_comp[symmetric] | subst (asm) vimage_comp[symmetric]))
  have f1: ‹f -` g -` {x} = (⋃y ∈ g -` {x}. f -` {y})› for x by blast
  show ‹finite (f -` g -` {x})› if  ‹∀x. finite (f -` {x})› and ‹∀x. finite (g -` {x})› for x
    apply (subst f1, subst finite_UN)
    by (rule that(2)[unfolded finitary_def, rule_format])
      (intro ballI that(1)[rule_format])
qed (metis finite_Un insert_absorb vimage_insert vimage_singleton_eq)



lemma finitary_updated_iff[simp] : ‹finitary (f (a := b)) ⟷ finitary f›
proof (unfold fun_upd_def finitary_def vimage_def, intro iffI allI)
  show ‹finite {x. (if x = a then b else f x) ∈ {y}}› if ‹∀y. finite {x. f x ∈ {y}}› for y
    apply (rule finite_subset[of _ ‹{x. x = a} ∪ {x. f x ∈ {y}}›], (auto)[1])
    apply (rule finite_UnI)
    by simp (fact that[rule_format]) 
next
  show ‹finite {x. f x ∈ {y}}› if ‹∀y. finite {x. (if x = a then b else f x) ∈ {y}}› for y
    apply (rule finite_subset[of _ ‹{x. x = a ∧ f x ∈ {y}} ∪ {x. x ≠ a ∧ f x ∈ {y}}›], (auto)[1])
    apply (rule finite_UnI)
    using that[rule_format, of y] by (simp_all add: Collect_mono rev_finite_subset)
qed

text ‹By declaring this simp, we automatically obtain this kind of result.›

lemma ‹finitary f ⟷ finitary (f (a := b, c := d, e:= g, h := i))› by simp


lemma Cont_RenH2:
  ‹finitary ((map_event⇩p⇩t⇩i⇩c⇩k f g) :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k ⇒ ('b, 's) event⇩p⇩t⇩i⇩c⇩k) ⟷ finitary f ∧ finitary g›
proof (intro iffI conjI)
  show ‹finitary f› if ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)›
  proof (unfold finitary_def, rule allI)
    fix b :: 'b
    have ‹finite ((map_event⇩p⇩t⇩i⇩c⇩k f g) -` {ev b})›
      by (fact ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)›[unfolded finitary_def, rule_format])
    also have ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` {ev b} = ev ` (f -` {b})›
      by (unfold vimage_def image_def) (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff)
    finally show ‹finite (f -` {b})› by (simp add: inj_on_def finite_image_iff)
  qed
next
  show ‹finitary g› if ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)›
  proof (unfold finitary_def, rule allI)
    fix s :: 's
    have ‹finite ((map_event⇩p⇩t⇩i⇩c⇩k f g) -` {tick s})›
      by (fact ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)›[unfolded finitary_def, rule_format])
    also have ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` {tick s} = tick ` (g -` {s})›
      by (unfold vimage_def image_def) (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
    finally show ‹finite (g -` {s})› by (simp add: inj_on_def finite_image_iff)
  qed
next
  show ‹finitary (map_event⇩p⇩t⇩i⇩c⇩k f g)› if ‹finitary f ∧ finitary g›
  proof (unfold finitary_def, rule allI)
    fix e :: ‹('b, 's) event⇩p⇩t⇩i⇩c⇩k›
    show ‹finite (map_event⇩p⇩t⇩i⇩c⇩k f g -` {e})›
    proof (cases e)
      fix b assume ‹e = ev b›
      have ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` {ev b} = ev ` (f -` {b})›
        by (unfold vimage_def image_def) (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff)
      thus ‹finite (map_event⇩p⇩t⇩i⇩c⇩k f g -` {e})›
        by (simp add: ‹e = ev b›) (meson finitary_def finite_imageI that)
    next
      fix s assume ‹e = tick s›
      have ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` {tick s} = tick ` (g -` {s})›
        by (unfold vimage_def image_def) (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
      thus ‹finite (map_event⇩p⇩t⇩i⇩c⇩k f g -` {e})›
        by (simp add: ‹e = tick s›) (meson finitary_def finite_imageI that)
    qed
  qed
qed



lemma Cont_RenH3:
  ‹{s1 @ t1 |s1 t1. (∃ b. s1 = [b] & f b = a) ∧ list = map f t1} = 
   (⋃ b ∈ f -`{a}. (λt. b # t) ` {t. list = map f t})›
  by auto (metis append_Cons append_Nil)


lemma Cont_RenH4: ‹finitary f ⟷ (∀s. finite {t. s = map f t})›
proof (unfold finitary_def, intro iffI allI)
  show ‹finite {t. s = map f t}› if ‹∀x. finite (f -` {x})› for s
  proof (induct s)
    show ‹finite {t. [] = map f t}› by simp
  next
    case (Cons a s)
    have ‹{t. a # s = map f t} = (⋃b ∈ f -` {a}. {b # t |t. s = map f t})›
      by (subst Cons_eq_map_conv) blast
    thus ?case by (simp add: finite_UN[OF that[rule_format]] local.Cons)
  qed
next
  have map1: ‹[a] = map f s = (∃b. s = [b] ∧ f b = a)› for a s by fastforce
  show ‹finite (f -` {x}) › if ‹∀s. finite {t. s = map f t}› for x
    by (simp add: vimage_def)
      (fact finite_vimageI[OF that[rule_format, of ‹[x]›, simplified map1], 
          of ‹λx. [x]›, unfolded inj_on_def, simplified])
qed



lemma Cont_RenH5: ‹finitary f ⟹ finitary g ⟹ finite (⋃t ∈ {t. t ≤ s}. {s. t=map (map_event⇩p⇩t⇩i⇩c⇩k f g) s})›
  apply (rule finite_UN_I)
  unfolding less_eq_list_def prefix_def
   apply (induct s rule: rev_induct, simp)
   apply (subgoal_tac ‹{t. ∃r. t @ r = xs @ [x]} = insert (xs @ [x]) {t. ∃r. t @ r = xs}›, auto)
    (* TODO: break this smt *)
  apply (smt (verit, ccfv_SIG) Collect_cong finite_insert)
  apply (metis Sublist.prefix_snoc prefix_def)
  using Cont_RenH2 Cont_RenH4 apply blast
  done



lemma Cont_RenH6: ‹{t. ∃t2. tickFree t ∧ front_tickFree t2 ∧ x = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t @ t2}
                   ⊆ {y. ∃xa. xa ∈ {t. t ≤ x} ∧ y ∈ {s. xa = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s}}›
  by auto


lemma Cont_RenH7: ‹finite {t. ∃t2. tickFree t ∧ front_tickFree t2 ∧ s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) t @ t2}›
  if ‹finitary f› and ‹finitary g›
proof -
  have f1: ‹{y. map (map_event⇩p⇩t⇩i⇩c⇩k f g) y ≤ s} = (⋃z ∈ {z. z ≤ s}. {y. z = map (map_event⇩p⇩t⇩i⇩c⇩k f g) y})› by fast
  show ?thesis
    apply (rule finite_subset[OF Cont_RenH6])
    apply (simp add: f1)
    apply (rule finite_UN_I)
    apply (induct s rule: rev_induct, simp)
    apply (subgoal_tac ‹{z. z ≤ xs @ [x]} = insert (xs @ [x]) {z. z ≤ xs}›, auto)
    using Cont_RenH2 Cont_RenH4 that by blast
qed


lemma chain_Renaming: ‹chain Y ⟹ chain (λi. Renaming (Y i) f g)›
  by (simp add: mono_Renaming chain_def)





subsection ‹Finally, continuity !›

lemma Cont_Renaming_prem:
  ‹(⨆ i. Renaming (Y i) f g) = Renaming (⨆ i. Y i) f g›
  if finitary: ‹finitary f› ‹finitary g› and chain: ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f g)›
  define S where ‹S i ≡ {s1. ∃t2.   tickFree s1 ∧ front_tickFree t2 
                                    ∧ s = map (map_event⇩p⇩t⇩i⇩c⇩k f g) s1 @ t2 ∧ s1 ∈ 𝒟 (Y i)}› for i
  have ‹(⋂i. S i) ≠ {}› 
    apply (rule Inter_nonempty_finite_chained_sets, unfold S_def)
    apply (use ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f g)› in
        ‹simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB, blast›)
    apply (rule finite_subset[OF _ Cont_RenH7[OF finitary, of s]], blast)
    using chain unfolding chain_def le_approx_def by blast
  then obtain s1 where f5: ‹s1 ∈ (⋂i. S i)› by blast
  thus ‹s ∈ 𝒟 (Renaming (Lub Y) f g)›
    by (simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB S_def) blast
next
  show ‹s ∈ 𝒟 (Renaming (Lub Y) f g) ⟹ s ∈ 𝒟 (⨆i. Renaming (Y i) f g)› for s
    by (auto simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB)
next
next
  assume same_div : ‹𝒟 (⨆i. Renaming (Y i) f g) = 𝒟 (Renaming (⨆i. Y i) f g)›
  fix s X assume ‹(s, X) ∈ ℱ (⨆i. Renaming (Y i) f g)›
  show ‹(s, X) ∈ ℱ (Renaming (⨆i. Y i) f g)›
  proof (cases ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f g)›)
    show ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f g) ⟹ (s, X) ∈ ℱ (Renaming (⨆i. Y i) f g)›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ 𝒟 (⨆i. Renaming (Y i) f g)›
    then obtain j where ‹s ∉ 𝒟 (Renaming (Y j) f g)›
      by (auto simp add: limproc_is_thelub chain_Renaming ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ ℱ (⨆i. Renaming (Y i) f g)› have ‹(s, X) ∈ ℱ (Renaming (Y j) f g)›
      by (simp add: limproc_is_thelub chain_Renaming ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ ℱ (Renaming (⨆i. Y i) f g)›
      by (fact le_approx2[OF mono_Renaming[OF is_ub_thelub[OF ‹chain Y›]], THEN iffD2])
  qed
next
  show ‹(s, X) ∈ ℱ (Renaming (Lub Y) f g) ⟹ (s, X) ∈ ℱ (⨆i. Renaming (Y i) f g)› for s X
    by (auto simp add: limproc_is_thelub chain chain_Renaming F_Renaming D_LUB F_LUB)  
qed


lemma Renaming_cont[simp] : ‹cont P ⟹ finitary f ⟹ finitary g ⟹ cont (λx. (Renaming (P x) f g))›
  by (rule contI2)
    (simp add: cont2monofunE mono_Renaming monofun_def,
      simp add: Cont_Renaming_prem ch2ch_cont cont2contlubE)



lemma RenamingF_cont : ‹cont P ⟹ cont (λx. (P x) ⟦a := b⟧ ⟦c := d⟧)›
  (* by simp *)
  by (simp only: Renaming_cont finitary_updated_iff inj_imp_finitary inj_on_id)


lemma ‹cont P ⟹ cont (λx. (P x)⟦a := b, c := d, e := f, g := a⟧ ⟦r1 := r2, r3:= r4, r5:= r6⟧)›
  by simp



section ‹Some nice properties›

lemma map_event⇩p⇩t⇩i⇩c⇩k_comp: ‹map_event⇩p⇩t⇩i⇩c⇩k (f2 ∘ f1) (g2 ∘ g1) = map_event⇩p⇩t⇩i⇩c⇩k f2 g2 ∘ map_event⇩p⇩t⇩i⇩c⇩k f1 g1›
  by (rule ext) (simp add: event⇩p⇩t⇩i⇩c⇩k.map_comp)


lemma Renaming_comp : ‹Renaming P (f2 ∘ f1) (g2 ∘ g1) = Renaming (Renaming P f1 g1) f2 g2›
proof (subst Process_eq_spec, intro conjI subset_antisym)
  show ‹ℱ (Renaming P (f2 ∘ f1) (g2 ∘ g1)) ⊆ ℱ (Renaming (Renaming P f1 g1) f2 g2)›
    apply (simp add: F_Renaming D_Renaming subset_iff, safe)
    by (metis (no_types, opaque_lifting) map_event⇩p⇩t⇩i⇩c⇩k_comp list.map_comp set.compositionality)
      (metis (no_types, opaque_lifting) map_event⇩p⇩t⇩i⇩c⇩k_comp map_event⇩p⇩t⇩i⇩c⇩k_tickFree append.right_neutral 
        front_tickFree_Nil list.map_comp)
next
  show ‹ℱ (Renaming (Renaming P f1 g1) f2 g2) ⊆ ℱ (Renaming P (f2 ∘ f1) (g2 ∘ g1))›
    apply (simp add: F_Renaming D_Renaming map_event⇩p⇩t⇩i⇩c⇩k_comp, safe)
    subgoal by simp (metis (no_types, lifting) vimage_comp)
    subgoal using map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree by simp blast
    subgoal by simp (metis front_tickFree_append map_event⇩p⇩t⇩i⇩c⇩k_tickFree) .
next
  show ‹𝒟 (Renaming P (f2 ∘ f1) (g2 ∘ g1)) ⊆ 𝒟 (Renaming (Renaming P f1 g1) f2 g2)›
    by (simp add: D_Renaming subset_iff, safe)
      (metis (no_types, opaque_lifting) map_event⇩p⇩t⇩i⇩c⇩k_comp map_event⇩p⇩t⇩i⇩c⇩k_tickFree append.right_neutral 
        front_tickFree_Nil list.map_comp)
next
  show ‹𝒟 (Renaming (Renaming P f1 g1) f2 g2) ⊆ 𝒟 (Renaming P (f2 ∘ f1) (g2 ∘ g1))›
    by (auto simp add: D_Renaming subset_iff)
      (metis map_event⇩p⇩t⇩i⇩c⇩k_comp map_event⇩p⇩t⇩i⇩c⇩k_tickFree front_tickFree_append)
qed




lemma Renaming_id: ‹Renaming P id id = P›
  by (subst Process_eq_spec, auto simp add: F_Renaming D_Renaming event⇩p⇩t⇩i⇩c⇩k.map_id0
      is_processT7 is_processT8)
    (metis append.right_neutral front_tickFree_append_iff
      nonTickFree_n_frontTickFree not_Cons_self2 process_charn)


lemma Renaming_inv: ‹Renaming (Renaming P f g) (inv f) (inv g) = P› if ‹inj f› and ‹inj g›
proof -
  have ‹  Renaming (Renaming P f g) (inv f) (inv g)
        = Renaming P (inv f ∘ f) (inv g ∘ g)› by (simp add: Renaming_comp)
  also have ‹… = Renaming P id id› by (simp add: ‹inj f› ‹inj g›)
  also have ‹… = P› by (fact Renaming_id)
  finally show ‹Renaming (Renaming P f g) (inv f) (inv g) = P› .
qed


lemma inv_Renaming: ‹Renaming (Renaming P (inv f) (inv g)) f g = P›
  if ‹bij f› and ‹bij g›
proof -
  have ‹  Renaming (Renaming P (inv f) (inv g)) f g
        = Renaming P (f ∘ inv f) (g ∘  inv g)› by (simp add: Renaming_comp)
  also have ‹… = Renaming P id id›
    by (metis bij_betw_def surj_iff ‹bij f› ‹bij g›)
  also have ‹… = P› by (fact Renaming_id)
  finally show ‹Renaming (Renaming P (inv f) (inv g)) f g = P› .
qed


(*<*)
end
  (*>*)