Quelle  Renaming.thy

(*<*)
―‹ ********************************************************************
 * 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 :: \<open>('a \<Rightarrow> ('b, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k) \<Rightarrow> bool\<close> 
  where \<open>finitaryExt f \<equiv> \<forall>x. finite(f -` {ev x})\<close>

 *)

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_{ptick_eq_ev_iff}   : ‹map_event_ptick f g e = ev b ⟷ (∃a. e = ev a ∧ b = f a)›
  and map_event_{ptick_eq_tick_iff} : ‹map_event_ptick f g e = 🍋(s) ⟷ (∃r. e = 🍋(r) ∧ s = g r)›
  and ev_eq_map_event_{ptick_iff}   : ‹ev b = map_event_ptick f g e ⟷ (∃a. e = ev a ∧ b = f a)›
  and tick_eq_map_event_{ptick_iff} : ‹🍋(s) = map_event_ptick f g e ⟷ (∃r. e = 🍋(r) ∧ s = g r)›
  by (cases e; auto)+


lemma inj_left_map_event_ptick: ‹inj (λf. map_event_ptick f g)›
proof (intro injI ext)
  show ‹map_event_ptick f1 g = map_event_ptick 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_ptick: ‹inj (map_event_ptick f)›
proof (intro injI ext)
  show ‹map_event_ptick f g1 = map_event_ptick 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_{ptick_tickFree} : ‹tickFree (map (map_event_ptick f g) s) ⟷ tickFree s›
  by (induct s) (simp_all add: event_ptick.case_eq_if)

lemma map_event_{ptick_front_tickFree} : ‹front_tickFree (map (map_event_ptick f g) s) ⟷ front_tickFree s›
  by (simp add: front_tickFree_iff_tickFree_butlast map_butlast[symmetric] map_event_{ptick_tickFree})


lemma map_map_event_{ptick_eq_tick_iff} :
  ‹map (map_event_ptick f g) t = [🍋(s)] ⟷ (∃r. s = g r ∧ t = [🍋(r)])›
  and tick_eq_map_map_event_{ptick_iff} :
  ‹[🍋(s)] = map (map_event_ptick f g) t ⟷ (∃r. s = g r ∧ t = [🍋(r)])›
  by (auto simp add: map_event_{ptick_eq_tick_iff} tick_eq_map_event_{ptick_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_ptick, 'a ==> 'b, 'r ==> 's] ==> ('b, 's) process_ptick›
  is ‹λP f g. ({( map (map_event_ptick f g) s1, X)| s1 X. (s1, (map_event_ptick f g) -` X) ∈ F P} ∪
 {((map (map_event<sub>ptick</sub> f g) s1) @ s2, X)| s1 s2 X. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ D P},
 {( map (map_event<sub>ptick</sub> f g) s1) @ s2| s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ D 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<sub>ptick_front_tickFree</sub>
          map_event<sub>ptick_tickFree</sub> 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<sub>ptick</sub> f g) s1› ‹(s1, {}) ∈ F P›
        | (div) s1 s2 where ‹s @ t @ [e] = map (map_event<sub>ptick</sub> f g) s1 @ s2› ‹s2 ≠ []›
          ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ D 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<sub>ptick</sub> 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', {}) ∈ F P› by blast
        with ‹s @ t = map (map_event<sub>ptick</sub> 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<sub>ptick</sub> f g) s1› ‹(s1, {}) ∈ F P›
      | (div) s1 s2 where ‹s @ [🍋(r)] = map (map_event<sub>ptick</sub> f g) s1 @ s2› ‹s2 ≠ []›
        ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ D 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<sub>ptick</sub> f g) s1'› ‹s1 = s1' @ [🍋(r')]› ‹r = g r'›
        by (simp add: append_eq_map_conv) (metis (mono_tags, opaque_lifting) map_map_event<sub>ptick_eq_tick_iff</sub>)
      from this(2) fail(2) have ‹(s1', map_event<sub>ptick</sub> f g -` X - {🍋(r')}) ∈ F P›
        by (simp add: is_processT6)
      hence  ‹(s1', map_event_ptick f g -` (X - {🍋(r)})) ∈ F 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_ptick 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_ptick f g) s1 @ s2›
      ‹tickFree s1› ‹front_tickFree s2› ‹s1 ∈ D 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_{ptick_tickFree} tickFree_append_iff)
    from this(1) "*"(1) have ‹s = map (map_event_ptick 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_ptick ==> updbinds ==> updbinds ==> ('a, 'r) process_ptick› (‹_ [_] [_]› [100, 100, 100]) (*see the values we need, at least 51*)
  "_Renaming_left"   :: ‹('a, 'r) process_ptick ==> updbinds ==> ('a, 'r) process_ptick› (‹_ [_] []› [100, 100])
  "_Renaming_right"  :: ‹('a, 'r) process_ptick ==> updbinds ==> ('a, 'r) process_ptick› (‹_ [] [_]› [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 🍋‹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: ‹F (Renaming P f g) =
 {( map (map_event_ptick f g) s1, X)| s1 X. (s1, (map_event_ptick f g) -` X) ∈ F P} ∪
 {((map (map_event_ptick f g) s1) @ s2, X)| s1 s2 X. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ D P}›
  by (simp add: Failures.rep_eq FAILURES_def Renaming.rep_eq)

lemma D_Renaming: ‹D (Renaming P f g) =
 {(map (map_event_ptick f g) s1) @ s2| s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ D P}›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Renaming.rep_eq)

lemma T_Renaming: ‹T (Renaming P f g) =
 { map (map_event_ptick f g) s1| s1. s1 ∈ T P} ∪
 {(map (map_event_ptick f g) s1) @ s2| s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s1 ∈ D 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 ∈ D (Renaming Q f g) ==> s ∈ D (Renaming P f g)› for s
    unfolding D_Renaming using le_approx1 ‹P ⊑ Q› by blast
next
  show ‹s ∉ D (Renaming P f g) ==> X ∈ R_a (Renaming P f g) s ==> X ∈ R_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_{ptick_eq_tick_iff} nonTickFree_n_frontTickFree non_tickFree_tick proc_ord2a ‹P ⊑ Q›)
next
  show ‹s ∉ D (Renaming P f g) ==> X ∈ R_a (Renaming Q f g) s ==> X ∈ R_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 (D (Renaming P f g)) ==> s ∈ T (Renaming Q f g)› for s
    apply (rule set_mp[of ‹{map (map_event_ptick f g) s1 |s1. s1 ∈ min_elems (D P)}›])
     apply (simp add: T_Renaming, use le_approx3 ‹P ⊑ Q› in blast)
    apply (drule set_rev_mp[of _ _ ‹min_elems {map (map_event_ptick f g) s1 |s1. tickFree s1 ∧ s1 ∈ D 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_{ptick_subset_vimage}: ‹map_event_ptick f g -` (ev ` A) ⊆ range tick ∪ (ev ` (f -` A))›
  and vimage_subset_vimage_map_event_ptick: ‹(ev ` (f -` A)) ⊆ (map_event_ptick f g -` (ev ` A)) - range tick›
  by (auto simp add: image_def vimage_def)
    (metis event_ptick.exhaust_sel event_ptick.sel(1) event_ptick.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_ptick f g) :: ('a, 'r) event_ptick ==> ('b, 's) event_ptick) ⟷ finitary f ∧ finitary g›
proof (intro iffI conjI)
  show ‹finitary f› if ‹finitary (map_event_ptick f g)›
  proof (unfold finitary_def, rule allI)
    fix b :: 'b
    have ‹finite ((map_event_ptick f g) -` {ev b})›
      by (fact ‹finitary (map_event<sub>ptick</sub> f g)›[unfolded finitary_def, rule_format])
    also have ‹map_event<sub>ptick</sub> f g -` {ev b} = ev ` (f -` {b})›
      by (unfold vimage_def image_def) (auto simp add: map_event_{ptick_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<sub>ptick</sub> f g)›
  proof (unfold finitary_def, rule allI)
    fix s :: 's
    have ‹finite ((map_event<sub>ptick</sub> f g) -` {tick s})›
      by (fact ‹finitary (map_event_ptick f g)›[unfolded finitary_def, rule_format])
    also have ‹map_event_ptick f g -` {tick s} = tick ` (g -` {s})›
      by (unfold vimage_def image_def) (auto simp add: map_event<sub>ptick_eq_tick_iff</sub>)
    finally show ‹finite (g -` {s})› by (simp add: inj_on_def finite_image_iff)
  qed
next
  show ‹finitary (map_event_ptick f g)› if ‹finitary f ∧ finitary g›
  proof (unfold finitary_def, rule allI)
    fix e :: ‹('b, 's) event_ptick›
    show ‹finite (map_event_ptick f g -` {e})›
    proof (cases e)
      fix b assume ‹e = ev b›
      have ‹map_event<sub>ptick</sub> f g -` {ev b} = ev ` (f -` {b})›
        by (unfold vimage_def image_def) (auto simp add: map_event_{ptick_eq_ev_iff})
      thus ‹finite (map_event_ptick 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<sub>ptick</sub> f g -` {tick s} = tick ` (g -` {s})›
        by (unfold vimage_def image_def) (auto simp add: map_event_{ptick_eq_tick_iff})
      thus ‹finite (map_event_ptick 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_ptick 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_ptick f g) t @ t2}
 ⊆ {y. ∃xa. xa ∈ {t. t ≤ x} ∧ y ∈ {s. xa = map (map_event_ptick f g) s}}›
  by auto


lemma Cont_RenH7: ‹finite {t. ∃t2. tickFree t ∧ front_tickFree t2 ∧ s = map (map_event_ptick f g) t @ t2}›
  if ‹finitary f› and ‹finitary g›
proof -
  have f1: ‹{y. map (map_event_ptick f g) y ≤ s} = (∪z ∈ {z. z ≤ s}. {y. z = map (map_event_ptick 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 ∈ D (⊔i. Renaming (Y i) f g)›
  define S where ‹S i ≡ {s1. ∃t2. tickFree s1 ∧ front_tickFree t2
 ∧ s = map (map_event_ptick f g) s1 @ t2 ∧ s1 ∈ D (Y i)}› for i
  have ‹(∩i. S i) ≠ {}›
    apply (rule Inter_nonempty_finite_chained_sets, unfold S_def)
    apply (use ‹s ∈ D (⊔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 ∈ D (Renaming (Lub Y) f g)›
    by (simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB S_def) blast
next
  show ‹s ∈ D (Renaming (Lub Y) f g) ==> s ∈ D (⊔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 : ‹D (⊔i. Renaming (Y i) f g) = D (Renaming (⊔i. Y i) f g)›
  fix s X assume ‹(s, X) ∈ F (⊔i. Renaming (Y i) f g)›
  show ‹(s, X) ∈ F (Renaming (⊔i. Y i) f g)›
  proof (cases ‹s ∈ D (⊔i. Renaming (Y i) f g)›)
    show ‹s ∈ D (⊔i. Renaming (Y i) f g) ==> (s, X) ∈ F (Renaming (⊔i. Y i) f g)›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ D (⊔i. Renaming (Y i) f g)›
    then obtain j where ‹s ∉ D (Renaming (Y j) f g)›
      by (auto simp add: limproc_is_thelub chain_Renaming ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ F (⊔i. Renaming (Y i) f g)› have ‹(s, X) ∈ F (Renaming (Y j) f g)›
      by (simp add: limproc_is_thelub chain_Renaming ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ F (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) ∈ F (Renaming (Lub Y) f g) ==> (s, X) ∈ F (⊔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_{ptick_comp}: ‹map_event_ptick (f2 ∘ f1) (g2 ∘ g1) = map_event_ptick f2 g2 ∘ map_event_ptick f1 g1›
  by (rule ext) (simp add: event_ptick.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 ‹F (Renaming P (f2 ∘ f1) (g2 ∘ g1)) ⊆ F (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_{ptick_comp} list.map_comp set.compositionality)
      (metis (no_types, opaque_lifting) map_event_{ptick_comp} map_event_{ptick_tickFree} append.right_neutral 
        front_tickFree_Nil list.map_comp)
next
  show ‹F (Renaming (Renaming P f1 g1) f2 g2) ⊆ F (Renaming P (f2 ∘ f1) (g2 ∘ g1))›
    apply (simp add: F_Renaming D_Renaming map_event_{ptick_comp}, safe)
    subgoal by simp (metis (no_types, lifting) vimage_comp)
    subgoal using map_event_{ptick_front_tickFree} by simp blast
    subgoal by simp (metis front_tickFree_append map_event_{ptick_tickFree}) .
next
  show ‹D (Renaming P (f2 ∘ f1) (g2 ∘ g1)) ⊆ D (Renaming (Renaming P f1 g1) f2 g2)›
    by (simp add: D_Renaming subset_iff, safe)
      (metis (no_types, opaque_lifting) map_event_{ptick_comp} map_event_{ptick_tickFree} append.right_neutral 
        front_tickFree_Nil list.map_comp)
next
  show ‹D (Renaming (Renaming P f1 g1) f2 g2) ⊆ D (Renaming P (f2 ∘ f1) (g2 ∘ g1))›
    by (auto simp add: D_Renaming subset_iff)
      (metis map_event_{ptick_comp} map_event_{ptick_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_ptick.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
  (*>*)