Theory Renaming

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

section‹ The Renaming Operator ›

theory  Renaming
  imports Process
begin

subsection‹Some preliminaries›

definition EvExt where ‹EvExt f x ≡ case_event (ev o f) tick x›


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

definition finitary :: ‹('a ⇒ 'b) ⇒ bool› 
  where ‹finitary f ≡ ∀x. finite(f -` {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 EvExt_id: ‹EvExt id = id›
  unfolding id_def EvExt_def by (metis comp_apply event.exhaust event.simps(4, 5))

lemma EvExt_eq_tick: ‹EvExt f a = tick ⟷ a = tick›
  by (metis EvExt_def comp_apply event.exhaust event.simps(3, 4, 5))

lemma tick_eq_EvExt: ‹tick = EvExt f a ⟷ a = tick›
  by (metis EvExt_eq_tick)

lemma EvExt_ev1: ‹EvExt f b = ev a ⟷ (∃c. b = ev c ∧ EvExt f (ev c) = ev a)›
  by (metis event.exhaust event.simps(3) tick_eq_EvExt)

lemma EvExt_tF: ‹tickFree (map (EvExt f) s) ⟷ tickFree s› 
  unfolding tickFree_def by (auto simp add: tick_eq_EvExt image_iff)

lemma inj_EvExt: ‹inj EvExt›
  unfolding inj_on_def EvExt_def
  by auto (metis comp_eq_dest_lhs event.simps(4, 5) ext)




lemma EvExt_ftF: ‹front_tickFree (map (EvExt f) s) ⟷ front_tickFree s› 
  unfolding front_tickFree_def by safe (metis (no_types, opaque_lifting) EvExt_tF map_tl rev_map)+
 

lemma map_EvExt_tick: ‹[tick] = map (EvExt f) t ⟷ t = [tick]›
  using tick_eq_EvExt by fastforce


lemma anteced_EvExt_diff_tick: ‹EvExt f -` (X - {tick}) = EvExt f -` X - {tick}›
  by (rule subset_antisym) (simp_all add: EvExt_eq_tick subset_Diff_insert subset_vimage_iff)
  


lemma   ev_elem_anteced1: ‹ev a ∈ EvExt f -` A ⟷ ev (f a) ∈ A›
  and tick_elem_anteced1: ‹tick ∈ EvExt f -` A ⟷ tick ∈ A›
  unfolding EvExt_def by simp_all
  

lemma hd_map_EvExt: ‹t ≠ [] ⟹ hd t = ev a ⟹ hd (map (EvExt f) t) = ev (f a)›
  and tl_map_EvExt: ‹t ≠ [] ⟹ tl (map (EvExt f) t) = map (EvExt f) (tl t)›
  unfolding EvExt_def by (simp_all add:  list.map_sel(1) map_tl)



subsection‹The Renaming Operator Definition›

lift_definition Renaming :: ‹['a process, 'a ⇒ 'b] ⇒ 'b process›
  is ‹λP f. ({(s, R). ∃ s1. (s1, (EvExt f) -` R) ∈ ℱ P ∧ s = map (EvExt f) s1} ∪
             {(s ,R). ∃ s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s = (map (EvExt f) s1) @ s2 ∧ s1 ∈ 𝒟 P},
             {t. ∃ s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ t = (map (EvExt f) s1) @ s2 ∧ s1 ∈ 𝒟 P})›
proof -
  show "is_process ({(s, R). ∃ s1. (s1, (EvExt f) -` R) ∈ ℱ P ∧ s = map (EvExt f) s1} ∪
              {(s ,R). ∃ s1 s2.   tickFree s1 ∧ front_tickFree s2 
                                ∧ s = (map (EvExt (f :: 'a ⇒ 'b)) s1) @ s2 ∧ s1 ∈ 𝒟 P},
              {t.      ∃ s1 s2. tickFree s1 ∧ front_tickFree s2 
                                ∧ t = (map (EvExt f) s1) @ s2 ∧ s1 ∈ 𝒟 P})"
              (is "is_process(?f, ?d)") for P f
unfolding is_process_def FAILURES_def DIVERGENCES_def
  proof (simp only: 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: EvExt_ftF is_processT2 EvExt_tF front_tickFree_append)
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
    proof (induct t rule: rev_induct, simp, auto,
           metis (no_types, lifting) is_processT3_SR map_eq_append_conv, goal_cases)
      case (1 x t s1 s2)
      show ?case
      proof (rule "1"(1), auto)
        assume a1: ‹∀s1. tickFree s1 ⟶ 
                           (∀s2. s @ t = map (EvExt f) s1 @ s2 ⟶ front_tickFree s2 ⟶ s1 ∉ 𝒟 P)›
        have ‹(if s2 = [] then butlast s1 else s1) ∉ 𝒟 P›
          apply (rule a1[rule_format, of _ ‹butlast s2›])
          using "1"(3, 4, 5) apply (auto simp add: tickFree_def front_tickFree_def 
                                              intro: in_set_butlastD)
             apply ((metis append_assoc butlast_snoc map_butlast)+)[2]
           apply (metis append_assoc butlast_append butlast_snoc)
          by (metis butlast_rev list.set_sel(2) rev_is_Nil_conv rev_rev_ident)
        with ‹s1 ∈ 𝒟 P› have ‹s2 = []› by presburger
        with "1"(5, 6) show ‹∃s1. (s1, {}) ∈ ℱ P ∧ s @ t = map (EvExt f) s1›
          apply (rule_tac x = ‹butlast s1› in exI, intro conjI)
          by (metis append_butlast_last_id butlast.simps(1) process_charn)
             (metis butlast_append map_butlast snoc_eq_iff_butlast)
      qed
    qed
  next
    show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
      apply (induct s rule: rev_induct, simp_all)
      by (meson is_processT4 vimage_mono)
         (metis process_charn 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
    show ‹(s @ [tick], {}) ∈ ?f ⟹ (s, X - {tick}) ∈ ?f› for s X
      apply auto
      by (metis (no_types, lifting) anteced_EvExt_diff_tick is_processT6 map_EvExt_tick 
                                    map_eq_append_conv)
         (metis EvExt_tF append.assoc butlast_snoc front_tickFree_charn non_tickFree_tick
                tickFree_Nil tickFree_append tickFree_implies_front_tickFree)
  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
    show ‹s @ [tick] ∈ ?d ⟹ s ∈ ?d› for s
      apply (induct s, auto)
      by (metis EvExt_tF Nil_is_map_conv hd_append2 list.exhaust_sel list.sel(1) tickFree_Cons)
         (metis Cons_eq_appendI EvExt_tF append.assoc butlast_snoc front_tickFree_charn 
                non_tickFree_tick tickFree_Nil tickFree_append tickFree_implies_front_tickFree)
  qed
qed


text ‹Some syntaxic sugar›

syntax
  "_Renaming"  :: ‹'a process ⇒ updbinds ⇒ 'a process› (‹_⟦_⟧› [100, 100]) (*see the values we need, at least 51*)
syntax_consts
  "_Renaming" ⇌ Renaming
translations
  "_Renaming P updates" ⇌ "CONST Renaming P (_Update (CONST id) updates)"


text ‹Now we can write \<^term>‹P⟦a := b⟧›. But 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⟧›.
      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⟧ = P⟦c := d, a := b⟧› by (simp add: fun_upd_twist)




subsection‹The Projections›

lemma F_Renaming: ‹ℱ (Renaming P f) = 
  {(s, R). ∃s1. (s1, EvExt f -` R) ∈ ℱ P ∧ s = map (EvExt f) s1} ∪
  {(s, R). ∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ s = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 P}›
  by (simp add: Failures.rep_eq FAILURES_def Renaming.rep_eq)

lemma D_Renaming: ‹𝒟 (Renaming P f) = {t. ∃s1 s2. tickFree s1 ∧ front_tickFree s2 ∧ 
                                                   t = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 P}›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Renaming.rep_eq)

lemma T_Renaming: ‹𝒯 (Renaming P f) = 
  {t. ∃ t1. t1 ∈ 𝒯 P ∧ t = map (EvExt f) t1} ∪ 
  {t.∃ t1 t2. tickFree t1 ∧ front_tickFree t2 ∧ t = map (EvExt f) t1 @ t2 ∧ t1 ∈ 𝒟 P}›
  apply (subst Traces.rep_eq, auto simp add: TRACES_def Failures.rep_eq[symmetric] F_Renaming)
  by (use F_T in blast) (metis T_F vimage_empty)



subsection‹Continuity Rule›

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

lemma mono_Renaming[simp] : ‹P ⊑ Q ⟹ (Renaming P f) ⊑ (Renaming Q f)›
proof (subst le_approx_def, intro conjI)
  show ‹P ⊑ Q ⟹ 𝒟 (Renaming Q f) ⊆ 𝒟 (Renaming P f)›
    unfolding D_Renaming using le_approx1 by blast
next 
  show ‹P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (Renaming P f) ⟶ ℛ⇩a (Renaming P f) s = ℛ⇩a (Renaming Q f) s›
    apply (auto simp add: Ra_def D_Renaming F_Renaming)
      apply (metis EvExt_ftF append.right_neutral front_tickFree_charn front_tickFree_single
                   le_approx2 map_append process_charn tickFree_Cons tickFree_Nil tickFree_append)
    using le_approx_lemma_F by blast (metis le_approx_def subset_eq)
next
  show ‹P ⊑ Q ⟹ min_elems (𝒟 (Renaming P f)) ⊆ 𝒯 (Renaming Q f)›
  proof (unfold min_elems_def, auto simp add: D_Renaming T_Renaming, goal_cases)
    case (1 s1 s2)
    obtain t2 where f1: ‹map (EvExt f) t2 = s2›
      by (metis "1"(3, 4, 5, 6) front_tickFree_charn less_append map_is_Nil_conv nil_less2)
    with "1" show ?case 
      apply (rule_tac x = ‹s1 @ t2› in exI, simp)
      apply (rule le_approx3[simplified subset_iff, OF "1"(1), rule_format])
      apply (induct s2 rule: rev_induct, induct s1 rule: rev_induct, auto)
        apply (simp add: Nil_min_elems)
       apply (metis "1"(5) append.right_neutral f1 less_self list.simps(8) min_elems3)
      by (metis append.assoc front_tickFree_dw_closed less_self)
  qed
qed

  


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


lemma vimage_EvExt_subset_vimage: ‹EvExt f -` (ev ` A) ⊆ insert tick (ev ` (f -` A))›
  and vimage_subset_vimage_EvExt: ‹(ev ` (f -` A)) ⊆ (EvExt f -` (ev ` A)) - {tick}›
  unfolding EvExt_def by auto (metis comp_apply event.exhaust event.simps(4) image_iff vimage_eq)



subsubsection ‹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 (EvExt f) ⟷ finitary f›
proof -
  have inj_ev: ‹inj ev› by (simp add: inj_def)
  show ‹finitary (EvExt f) ⟷ finitary f›
    apply (subst finitary_comp_iff[of ev f, symmetric], simp add: inj_ev)
  proof (intro iffI; subst finitary_def, intro allI)
    have inj_ev: ‹inj ev› by (simp add: inj_def)
    show ‹finite ((ev ∘ f) -` {x})› if ‹finitary (EvExt f)› for x
      apply (fold vimage_comp)
    proof (cases ‹x = tick›, (insert finite.simps)[1], blast) 
      assume ‹x ≠ tick›
      with subset_singletonD[OF inj_vimage_singleton[OF inj_ev, of x]] obtain y 
        where f1: ‹ev -` {x} = {y}› by auto (metis empty_iff event.exhaust vimage_singleton_eq)
      have f2: ‹(f -` {y}) = ev -` ev ` f -` {y}› by (simp add: inj_ev inj_vimage_image_eq)
      show ‹finite (f -` ev -` {x})› 
        apply (subst f1, subst f2)
        apply (rule finite_vimageI[OF _ inj_ev]) 
        apply (rule finite_subset[OF vimage_subset_vimage_EvExt])
        apply (rule finite_Diff)
        using finitary_def that by fastforce
    qed
  next
    show ‹finite (EvExt f -` {x})› if ‹finitary (ev ∘ f)› for x
    proof (cases ‹x = tick›,
           metis Diff_cancel anteced_EvExt_diff_tick finite.emptyI infinite_remove vimage_empty)
      assume ‹x ≠ tick›
      with subset_singletonD[OF inj_vimage_singleton[OF inj_ev, of x]] obtain y 
        where f1: ‹{x} = ev ` {y}› using event.exhaust by auto
      show ‹finite (EvExt f -` {x})›
        apply (subst f1)
        apply (rule finite_subset[OF vimage_EvExt_subset_vimage])
        apply (subst finite_insert)
        apply (rule finite_imageI)
        by (fact finitary_comp_iff[OF inj_imp_finitary[OF inj_ev], of f, 
                                   simplified that, simplified, unfolded finitary_def, rule_format])
    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, simp)
    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 ⟹ finite (⋃t ∈ {t. t ≤ s}. {s. t=map (EvExt f) s})›
  apply (rule finite_UN_I)
  unfolding le_list_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)
   apply (metis butlast_append butlast_snoc self_append_conv)
  using Cont_RenH2 Cont_RenH4 by blast



lemma Cont_RenH6: ‹{t. ∃ t2. tickFree t ∧ front_tickFree t2 ∧ x = map (EvExt f) t @ t2} 
                   ⊆ {y. ∃xa. xa ∈ {t. t <= x} ∧ y ∈ {s. xa = map (EvExt f) s}}›
  by (auto simp add: le_list_def)



lemma Cont_RenH7: ‹finite {t. ∃t2. tickFree t ∧ front_tickFree t2 ∧ s = map (EvExt f) t @ t2}›
  if ‹finitary f›
proof -
  have f1: ‹{y. map (EvExt f) y ≤ s} = (⋃z ∈ {z. z ≤ s}. {y. z = map (EvExt f) 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)
      apply (metis append_eq_first_pref_spec append_self_conv le_list_def)
     apply (meson le_list_def order_trans)
    using Cont_RenH2 Cont_RenH4 that by blast
qed


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



text ‹A key lemma for the continuity.›

lemma Inter_nonempty_finite_chained_sets:
  ‹∀i. S i ≠ {} ⟹ finite (S 0) ⟹ ∀i. S (Suc i) ⊆ S i ⟹ (⋂i. S i) ≠ {}›
proof (induct ‹card (S 0)› arbitrary: S rule: nat_less_induct)
  case 1
  show ?case
  proof (cases ‹∀i. S i = S 0›)
    case True
    thus ?thesis by (metis "1.prems"(1) INT_iff ex_in_conv)
  next 
    case False
    have f1: ‹i ≤ j ⟹ S j ⊆ S i› for i j by (simp add: "1.prems"(3) lift_Suc_antimono_le)
    with False obtain j m where f2: ‹m < card (S 0)› and f3: ‹m = card (S j)›
      by (metis "1.prems"(2) psubsetI psubset_card_mono zero_le)
    define T where ‹T i ≡ S (i + j)› for i
    have f4: ‹m = card (T 0)› unfolding T_def by (simp add: f3)
    from f1 have f5: ‹(⋂i. S i) = (⋂i. T i)› unfolding T_def by (auto intro: le_add1)
    show ?thesis
      apply (subst f5)
      apply (rule "1.hyps"[rule_format, OF f2, of T, OF f4], unfold T_def)
      by (simp_all add: "1.prems"(1, 3) lift_Suc_antimono_le)
         (metis "1.prems"(2) add_0 f1 finite_subset le_add1)
  qed
qed



subsubsection ‹Finally, continuity !›

lemma Cont_Renaming_prem:
  ‹(⨆ i. Renaming (Y i) f) = (Renaming (⨆ i. Y i) f)› if finitary: ‹finitary f› 
   and chain: ‹chain Y›
proof (subst Process_eq_spec, safe, goal_cases)
  show ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f) ⟹ s ∈ 𝒟 (Renaming (Lub Y) f)› for s
  proof (simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB)
    assume a1: ‹∀i. ∃s1.    tickFree s1 
                         ∧ (∃s2. front_tickFree s2 
                                  ∧ s = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 (Y i))›
    define S where ‹S i ≡ {s1. ∃t2.   tickFree s1 ∧ front_tickFree t2 
                                    ∧ s = map (EvExt f) s1 @ t2 ∧ s1 ∈ 𝒟 (Y i)}› for i

    have ‹(⋂i. S i) ≠ {}› 
      apply (rule Inter_nonempty_finite_chained_sets, unfold S_def)
        apply (insert a1, blast)[1]
       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 ‹∃s1. tickFree s1 ∧ (∃s2.   front_tickFree s2 
                                   ∧ s = map (EvExt f) s1 @ s2 
                                   ∧ (∀i. s1 ∈ 𝒟 (Y i)))›
      by (rule_tac x = s1 in exI, unfold S_def) auto
  qed
next
  show ‹s ∈ 𝒟 (Renaming (Lub Y) f) ⟹ s ∈ 𝒟 (⨆i. Renaming (Y i) f)› for s
    by (auto simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB)
next
  show ‹(s, X) ∈ ℱ (⨆i. Renaming (Y i) f) ⟹ (s, X) ∈ ℱ (Renaming (Lub Y) f)› for s X
  proof (auto simp add: limproc_is_thelub chain chain_Renaming F_Renaming D_LUB F_LUB)
    assume a1: ‹∀i. (∃s1. (s1, EvExt f -` X) ∈ ℱ (Y i) ∧ s = map (EvExt f) s1) ∨
                    (∃s1. tickFree s1 ∧ 
                          (∃s2.   front_tickFree s2 
                                ∧ s = map (EvExt f) s1 @ s2 
                                ∧ s1 ∈ 𝒟 (Y i)))›
       and a2: ‹∀s1. tickFree s1 ⟶ 
                     (∀s2. s = map (EvExt f) s1 @ s2
                             ⟶ front_tickFree s2
                             ⟶ (∃i. s1 ∉ 𝒟 (Y i)))›
    define S where ‹S i ≡ {s1. (s1, EvExt f -` X) ∈ ℱ (Y i) ∧ s = map (EvExt f) s1} ∪
                           {s1. ∃t2. tickFree s1 
                                     ∧ front_tickFree t2 
                                     ∧ s = map (EvExt f) s1 @ t2 
                                     ∧ s1 ∈ 𝒟 (Y i)}› for i

    have ‹s1 ∈ (⋂i. S i) ⟹ (∀i. (s1, EvExt f -` X) ∈ ℱ (Y i) ∧ s = map (EvExt f) s1) 
                              ∨ tickFree s1 ∧ (∃s2.    front_tickFree s2 
                                                     ∧ s = map (EvExt f) s1 @ s2 
                                                     ∧ (∀i. s1 ∈ 𝒟 (Y i)))› for s1
      unfolding S_def by auto (meson NF_ND)
    hence f1: ‹s1 ∈ (⋂i. S i) ⟹ (∀i. (s1, EvExt f -` X) ∈ ℱ(Y i) ∧ s = map(EvExt f) s1)› for s1
      by (meson a2)
    have ‹(⋂i. S i) ≠ {}›
      apply (rule Inter_nonempty_finite_chained_sets, unfold S_def)
        apply (insert a1, blast)[1]
       apply (subst finite_Un, intro conjI)
        apply (rule finite_subset[of _ ‹{s1. s = map (EvExt f) s1}›], blast)
        apply (insert Cont_RenH2 Cont_RenH4 finitary, blast)[1]
       apply (rule finite_subset[OF _ Cont_RenH7[OF finitary, of s]], blast)
      using NF_ND chain po_class.chainE proc_ord2a chain le_approx_def by safe blast+

    then obtain s1 where ‹s1 ∈ (⋂i. S i)› by blast
    thus ‹∃s1. (∀x. (s1, EvExt f -` X) ∈ ℱ (Y x)) ∧ s = map (EvExt f) s1› 
      using f1 by (rule_tac x = s1 in exI) blast
  qed
next
  show ‹(s, X) ∈ ℱ (Renaming (Lub Y) f) ⟹ (s, X) ∈ ℱ (⨆i. Renaming (Y i) f)› 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 ⟹ cont (λx. (Renaming (P x) f))›
  by (rule contI2)
     (simp add: cont2monofunE monofunI, simp add: Cont_Renaming_prem ch2ch_cont cont2contlubE)


lemma RenamingF_cont : ‹cont P ⟹ cont (λx. (P x)⟦a := b⟧)›
  (* 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⟧)›
  (* by simp *)
  apply (erule Renaming_cont)
  apply (simp only: finitary_updated_iff)
  apply (rule inj_imp_finitary)
  by (rule inj_on_id)
  
 



subsection ‹Some nice properties›


lemma EvExt_comp: ‹EvExt (g ∘ f) = EvExt g ∘ EvExt f›
  unfolding EvExt_def by (rule ext, auto) (metis comp_apply event.exhaust event.simps(4, 5))



lemma Renaming_comp : ‹Renaming P (g o f) = Renaming (Renaming P f) g›
proof (subst Process_eq_spec, intro conjI subset_antisym)
  show ‹ℱ (Renaming P (g ∘ f)) ⊆ ℱ (Renaming (Renaming P f) g)›
    apply (simp add: F_Renaming D_Renaming subset_iff, safe)
    by (metis (no_types, opaque_lifting) EvExt_comp list.map_comp set.compositionality)
       (metis (no_types, opaque_lifting) EvExt_comp EvExt_tF append.right_neutral 
                                         front_tickFree_Nil list.map_comp)
next
  show ‹ℱ (Renaming (Renaming P f) g) ⊆ ℱ (Renaming P (g ∘ f))›
    apply (auto simp add: F_Renaming D_Renaming EvExt_comp EvExt_ftF EvExt_tF front_tickFree_append)
    by (metis (no_types, opaque_lifting) EvExt_comp list.map_comp set.compositionality)
next
  show ‹𝒟 (Renaming P (g ∘ f)) ⊆ 𝒟 (Renaming (Renaming P f) g)›
    apply (simp add: D_Renaming subset_iff, safe)
    by (metis (no_types, opaque_lifting) EvExt_comp EvExt_tF append.right_neutral 
                                         front_tickFree_Nil list.map_comp)
next
  show ‹𝒟 (Renaming (Renaming P f) g) ⊆ 𝒟 (Renaming P (g ∘ f))›
    apply (auto simp add: D_Renaming subset_iff)
    by (metis EvExt_comp EvExt_tF front_tickFree_append)
qed




lemma Renaming_id: ‹Renaming P id = P›
  by (subst Process_eq_spec, auto simp add: F_Renaming D_Renaming EvExt_id 
                                            is_processT7_S is_processT8_S)
     (metis append.right_neutral front_tickFree_mono list.distinct(1) 
            nonTickFree_n_frontTickFree process_charn)
  

lemma Renaming_inv: ‹Renaming (Renaming P f) (inv f) = P› if ‹inj f›
  apply (subst Renaming_comp[symmetric])
  apply (subst inv_o_cancel[OF that])
  by (fact Renaming_id)


end