Theory Patch

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

chapter ‹Patch for Compatibility›
theory Patch
  imports "HOL-CSP.Assertions"
begin


text ‹\<^session>‹HOL-CSP› significantly changed during the past months, but not all
      the modifications appear in the current version on the AFP.
      This theory fixes the incompatibilities and will be removed in the next release.›


section ‹Results›

―‹This one is very easy›
lemma Mprefix_Det_distr:
  ‹(□ a ∈ A → P a) □ (□ b ∈ B → Q b) = 
   □ x ∈ A ∪ B → (  if x ∈ A ∩ B then P x ⊓ Q x 
                    else if x ∈ A then P x else Q x)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (simp add: F_Det F_Mprefix F_Ndet disjoint_iff, safe, auto)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (auto simp add: F_Mprefix F_Ndet F_Det split: if_split_asm)
next
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (simp add: D_Det D_Mprefix D_Ndet, safe, auto)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Mprefix D_Ndet D_Det split: if_split_asm)
qed 



lemma F_Mndetprefix:
  ‹ℱ (Mndetprefix A P) =
   (if A = {} then {(s, X). s = []} else ⋃x∈A. ℱ (x → P x))›
  by (simp add: F_Mndetprefix F_STOP)

lemma D_Mndetprefix:
  ‹𝒟 (Mndetprefix A P) = (if A = {} then {} else ⋃x∈A. 𝒟 (x → P x))›
  by (simp add: D_Mndetprefix D_STOP)

lemma T_Mndetprefix:
  ‹𝒯 (Mndetprefix A P) = (if A = {} then {[]} else ⋃x∈A. 𝒯 (x → P x))›
  by (simp add: T_Mndetprefix T_STOP)

lemma D_expand : 
  ‹𝒟 P = {t1 @ t2| t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2}›
  (is ‹𝒟 P = ?rhs›)
proof (intro subset_antisym subsetI)
  show ‹s ∈ 𝒟 P ⟹ s ∈ ?rhs› for s
    apply (simp, cases ‹tickFree s›)
     apply (rule_tac x = s in exI, rule_tac x = ‹[]› in exI, simp)
    apply (rule_tac x = ‹butlast s› in exI, rule_tac x = ‹[tick]› in exI, simp)
    by (metis front_tickFree_implies_tickFree nonTickFree_n_frontTickFree
              process_charn snoc_eq_iff_butlast)
next
  show ‹s ∈ ?rhs ⟹ s ∈ 𝒟 P› for s
    using is_processT7 by blast
qed


lemma F_Seq: ‹ℱ (P ❙; Q) = {(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
                          {(t1 @ t2, X) |t1 t2 X. t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
                          {(t1, X) |t1 X. t1 ∈ 𝒟 P}›
proof -
  have * : ‹{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q} ⊆
            {(t1 @ t2, X) |t1 t2 X. t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q}›
    using is_processT8 by blast
  have ** : ‹{(t1, X) |t1 X. t1 ∈ 𝒟 P} =
             {(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2}›
    by (subst D_expand) blast
  show ?thesis
    apply (subst Un_absorb1[OF "*", symmetric], subst "**")
    by (simp add:  F_Seq) blast
qed
   

 
lemma D_Seq:
  ‹𝒟 (P ❙; Q) = 𝒟 P ∪ {t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}›
  by (subst (2) D_expand) (auto simp add: D_Seq)


lemma T_Seq: ‹𝒯 (P ❙; Q) = {t. ∃X. (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪ 
                          {t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q} ∪
                          𝒟 P›
  by (auto simp add: Traces_def TRACES_def Failures_def[symmetric] F_Seq)



lemma tickFree_butlast:
  ‹tickFree s ⟷ tickFree (butlast s) ∧ (s ≠ [] ⟶ last s ≠ tick)›
  by (induct s) simp_all

lemma front_tickFree_butlast: ‹front_tickFree s ⟷ tickFree (butlast s)›
  by (induct s) (auto simp add: front_tickFree_def)


lemma STOP_iff_T: ‹P = STOP ⟷ 𝒯 P = {[]}›
  apply (intro iffI, simp add: T_STOP)
  apply (subst Process_eq_spec, safe, simp_all add: F_STOP D_STOP)
  by (use F_T in force, use is_processT5_S7 in fastforce)
     (metis D_T append_Nil front_tickFree_single is_processT7_S
            list.distinct(1) singletonD tickFree_Nil)

lemma BOT_iff_D: ‹P = ⊥ ⟷ [] ∈ 𝒟 P›
  apply (intro iffI, simp add: D_UU)
  apply (subst Process_eq_spec, safe)
  by (simp_all add: F_UU D_UU is_processT2 D_imp_front_tickFree)
     (metis append_Nil is_processT tickFree_Nil)+


lemma Ndet_is_STOP_iff: ‹P ⊓ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  using Nil_subset_T by (simp add: STOP_iff_T T_Ndet, blast)

lemma Det_is_STOP_iff: ‹P □ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  using Nil_subset_T by (simp add: STOP_iff_T T_Det, blast)


lemma Det_is_BOT_iff: ‹P □ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_D D_Det)

lemma Ndet_is_BOT_iff: ‹P ⊓ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_D D_Ndet)

lemma Sync_is_BOT_iff: ‹P ⟦S⟧ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (rule HOL.sym, intro iffI, metis Sync_BOT Sync_commute)
     (use empty_setinterleaving in ‹auto simp add: BOT_iff_D D_Sync›)


lemma STOP_neq_BOT: ‹STOP ≠ ⊥›
  by (simp add: D_STOP BOT_iff_D)

lemma SKIP_neq_BOT: ‹SKIP ≠ ⊥›
  by (simp add: D_SKIP BOT_iff_D)


lemma Mprefix_neq_BOT: ‹Mprefix A P ≠ ⊥›
  by (simp add: BOT_iff_D)

lemma Mndetprefix_neq_BOT: ‹Mndetprefix A P ≠ ⊥›
  by (cases ‹A = {}›) (simp_all add: D_STOP BOT_iff_D D_Mndetprefix write0_def)


lemma STOP_T_iff: ‹STOP ⊑⇩T P ⟷ P = STOP›
  by auto (metis Nil_elem_T STOP_iff_T empty_iff subset_singletonD trace_refine_def)

lemma STOP_F_iff: ‹STOP ⊑⇩F P ⟷ P = STOP›
  by auto (metis Nil_elem_T STOP_iff_T empty_iff leF_imp_leT
                 subset_singletonD trace_refine_def)

lemma STOP_FD_iff: ‹STOP ⊑⇩F⇩D P ⟷ P = STOP›
  using STOP_F_iff idem_FD leFD_imp_leF by blast

lemma SKIP_FD_iff: ‹SKIP ⊑⇩F⇩D P ⟷ P = SKIP›
  apply (subst Process_eq_spec,
         auto simp: failure_divergence_refine_def le_ref_def F_SKIP D_SKIP subset_iff)
  by (metis F_T insertI1 is_processT5_S6 is_processT6_S2)
     (metis F_T append.left_neutral insertI1 is_processT5_S6 tick_T_F)

lemma SKIP_F_iff: ‹SKIP ⊑⇩F P ⟷ P = SKIP›
  apply (subst Process_eq_spec,
         auto simp: Process_eq_spec failure_refine_def le_ref_def F_SKIP D_SKIP subset_iff)
    apply (metis F_T insertI1 is_processT5_S6 is_processT6_S2)
   apply (metis F_T append.left_neutral insertI1 is_processT5_S6 tick_T_F)
  by (metis append_Nil insertI1 neq_Nil_conv process_charn)


lemma Seq_is_SKIP_iff: ‹P ❙; Q = SKIP ⟷ P = SKIP ∧ Q = SKIP›
proof (intro iffI)
  show ‹P = SKIP ∧ Q = SKIP ⟹ P ❙; Q = SKIP›
    by (simp add: Seq_SKIP)
next
  have ‹P ❙; Q = SKIP ⟹ (Q = SKIP ⟶ P = SKIP) ∧ Q = SKIP›
  proof (intro conjI impI)
    show ‹P ❙; Q = SKIP ⟹ Q = SKIP ⟹ P = SKIP›
      by (simp add: Seq_SKIP)
  next
    show ‹P ❙; Q = SKIP ⟹ Q = SKIP›
      apply (subst (asm) SKIP_F_iff[symmetric], subst SKIP_F_iff[symmetric])
      unfolding failure_refine_def
      apply (subst (asm) subset_iff, subst subset_iff)
      by (auto simp add:F_Seq F_SKIP)
         (metis (no_types, opaque_lifting) F_T append_Nil insert_absorb insert_iff
                                           is_processT5_S6 tickFree_Nil)+
  qed
  thus ‹P ❙; Q = SKIP ⟹ P = SKIP ∧ Q = SKIP› by blast
qed



section ‹The Renaming Operator›

subsection‹Some Preliminaries›


setup_lifting type_definition_process


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


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)›
  by (simp_all add: EvExt_def 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 ‹?thesis P f› (is "is_process(?f, ?d)") for P f
    unfolding is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv
  proof (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)
      show ‹(s @ [], {}) ∈ ?f ⟹ (s, {}) ∈ ?f› by simp
    next
      fix t x
      assume  hyp : ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f›
         and prem : ‹(s @ t @ [x], {}) ∈ ?f›
      from prem consider ‹∃s1. (s1, {}) ∈ ℱ P ∧ s @ t @ [x] = map (EvExt f) s1›
        | ‹∃s1. tickFree s1 ∧ (∃s2. front_tickFree s2 ∧ 
                s @ t @ [x] = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 P)› by fast
      thus ‹(s, {}) ∈ ?f›
      proof cases
        assume ‹∃s1. (s1, {}) ∈ ℱ P ∧ s @ t @ [x] = map (EvExt f) s1›
        then obtain s1 where * : ‹(s1, {}) ∈ ℱ P› ‹s @ t @ [x] = map (EvExt f) s1› by blast
        hence ‹(butlast s1, {}) ∈ ℱ P› ‹s @ t = map (EvExt f) (butlast s1)›
          by (metis append_butlast_last_id butlast.simps(1) is_processT3_SR)
             (metis "*"(2) append.assoc butlast_snoc map_butlast)
        with hyp show ‹(s, {}) ∈ ?f› by auto
      next
        assume ‹∃s1. tickFree s1 ∧ (∃s2. front_tickFree s2 ∧
                     s @ t @ [x] = map (EvExt f) s1 @ s2 ∧ s1 ∈ 𝒟 P)›
        then obtain s1 s2
          where * : ‹tickFree s1› ‹front_tickFree s2›
                    ‹s @ t @ [x] = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 P› by blast
        show ‹(s, {}) ∈ ?f›
        proof (cases s2 rule: rev_cases)
          from "*"(3, 4) show ‹s2 = [] ⟹ (s, {}) ∈ ?f›
            by (simp add: append_eq_map_conv)
               (metis NT_ND T_F is_processT3_ST)
        next
          fix y s2'
          assume ‹s2 = s2' @ [y]›
          with "*" front_tickFree_dw_closed have ‹(s @ t, {}) ∈ ?f› by simp blast
          thus ‹(s, {}) ∈ ?f› by (rule hyp)
        qed
      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 (simp, elim disjE)
      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
    fix s
    assume ‹s @ [tick] ∈ ?d›
    then obtain t1 t2 
      where ‹tickFree t1› ‹front_tickFree t2› 
            ‹s @ [tick] = map (EvExt f) t1 @ t2› ‹t1 ∈ 𝒟 P› by blast
    thus ‹s ∈ ?d›
      apply simp
      apply (rule_tac x = t1 in exI, simp)
      apply (rule_tac x = ‹butlast t2› in exI)
      by (metis EvExt_tF butlast_append butlast_snoc front_tickFree_butlast
                non_tickFree_tick tickFree_append tickFree_butlast)
  qed
qed


text ‹Some syntaxic sugar›

syntax
  "_Renaming"  :: ‹'a process ⇒ updbinds ⇒ 'a process› (‹_⟦_⟧› [100, 100]) (*see the values we need, at least 51*)
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[no_vars] fun_upd_upd[no_vars] fun_upd_twist[no_vars]}.›

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_def 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_def 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}›
  by (auto simp add: Traces_def TRACES_def Failures_def[symmetric] F_Renaming)
     (metis F_T T_F vimage_empty)



subsection‹Continuity Rule›

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

lemma mono_Renaming[simp] : ‹(Renaming P f) ⊑ (Renaming Q f)› if ‹P ⊑ Q›
proof (unfold le_approx_def, intro conjI subset_antisym subsetI allI impI)
  show ‹s ∈ 𝒟 (Renaming Q f) ⟹ s ∈ 𝒟 (Renaming P f)› for s
    using that[THEN le_approx1] by (auto simp add: D_Renaming)
next
  show ‹s ∉ 𝒟 (Renaming P f) ⟹ 
        X ∈ ℛ⇩a (Renaming P f) s ⟹ X ∈ ℛ⇩a (Renaming Q f) s› for s X
    using that[THEN le_approx2] apply (simp add: Ra_def D_Renaming F_Renaming)
    by (metis (no_types, opaque_lifting)  append.right_neutral butlast.simps(2) 
              front_tickFree_butlast front_tickFree_mono list.distinct(1) 
              map_EvExt_tick map_append nonTickFree_n_frontTickFree process_charn)
next
  show ‹s ∉ 𝒟 (Renaming P f) ⟹
        X ∈ ℛ⇩a (Renaming Q f) s ⟹ X ∈ ℛ⇩a (Renaming P f) s› for s X
    using that[THEN le_approx2] that[THEN le_approx1]
    by (simp add: Ra_def D_Renaming F_Renaming subset_iff)
       (metis is_processT8_S)
next
  fix s
  assume * : ‹s ∈ min_elems (𝒟 (Renaming P f))›
  from elem_min_elems[OF "*"] obtain s1 s2
    where ** : ‹tickFree s1› ‹front_tickFree s2›
               ‹s = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 P›
               ‹front_tickFree s›
    using D_imp_front_tickFree D_Renaming by blast
  with min_elems_no[OF "*", of ‹butlast s›] have ‹s2 = []›
    by (cases s rule: rev_cases; simp add: D_Renaming)
       (metis butlast_append butlast_snoc front_tickFree_butlast less_self 
              nless_le tickFree_implies_front_tickFree)
  with "**" min_elems_no[OF "*", of ‹butlast s›] have ‹s1 ∈ min_elems (𝒟 P)›
    apply (cases s; simp add: D_Renaming Nil_min_elems)
    by (metis (no_types, lifting) D_imp_front_tickFree append.right_neutral butlast_snoc
                                  front_tickFree_charn less_self list.discI
                                  list.map_disc_iff map_butlast min_elems1 nless_le)
  hence ‹s1 ∈ 𝒯 Q› using that[THEN le_approx3] by blast
  show ‹s ∈ 𝒯 (Renaming Q f)›
    apply (simp add: "**"(3) ‹s2 = []› T_Renaming)
    using ‹s1 ∈ 𝒯 Q› by blast
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 ‹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 le_snoc_is : ‹t ≤ s @ [x] ⟷ t = s @ [x] ∨ t ≤ s›
  by (metis append_eq_first_pref_spec le_list_def order.trans self_append_conv)


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, OF inj_imp_finitary[OF 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)
    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: ‹finite (⋃t ∈ {t. t ≤ (s :: 'α trace)}. {s. t=map (EvExt f) s})› if ‹finitary f›
  apply (rule finite_UN_I)
   apply (induct s rule: rev_induct)
    apply (simp; fail)
   apply (simp add: le_snoc_is; fail)
  using Cont_RenH2 Cont_RenH4 that 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)
      apply (simp; fail)
     apply (simp add: le_snoc_is; fail)
    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)
  fix s
  define S where ‹S i ≡ {s1. ∃t2. tickFree s1 ∧ front_tickFree t2 ∧
                                   s = map (EvExt f) s1 @ t2 ∧ s1 ∈ 𝒟 (Y i)}› for i
  assume ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f)›
  hence ‹s ∈ 𝒟 (Renaming (Y i) f)› for i
    by (simp add: limproc_is_thelub chain chain_Renaming D_LUB)

  hence ‹∀i. S i ≠ {}› by (simp add: S_def D_Renaming) blast
  moreover have ‹finite (S 0)›
    unfolding S_def 
    by (rule finite_subset[OF _ Cont_RenH7[OF finitary, of s]], blast)
  moreover have ‹∀i. S (Suc i) ⊆ S i›
    unfolding S_def using NF_ND po_class.chainE[OF chain]
                          proc_ord2a le_approx_def by blast
  ultimately have ‹(⋂i. S i) ≠ {}›
    by (rule Inter_nonempty_finite_chained_sets)    
  
  thus ‹s ∈ 𝒟 (Renaming (Lub Y) f)›
    by (simp add: limproc_is_thelub chain D_Renaming
                  D_LUB ex_in_conv[symmetric] S_def) blast
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
  fix s X
  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
  assume ‹(s, X) ∈ ℱ (⨆i. Renaming (Y i) f)›
  hence ‹(s, X) ∈ ℱ (Renaming (Y i) f)› for i
    by (simp add: limproc_is_thelub chain_Renaming[OF chain] F_LUB)

  hence ‹∀i. S i ≠ {}› by (auto simp add: S_def F_Renaming)
  moreover have ‹finite (S 0)›
    unfolding S_def
    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)
    by (rule finite_subset[OF _ Cont_RenH7[OF finitary, of s]], blast)
  moreover have ‹∀i. S (Suc i) ⊆ S i›
    unfolding S_def using NF_ND po_class.chainE[OF chain]
                          proc_ord2a le_approx_def by safe blast+
  ultimately have ‹(⋂i. S i) ≠ {}›
    by (rule Inter_nonempty_finite_chained_sets)
   
  thus ‹(s, X) ∈ ℱ (Renaming (Lub Y) f)›
    by (simp add: F_Renaming limproc_is_thelub chain D_LUB 
                  F_LUB ex_in_conv[symmetric] S_def) (meson NF_ND)
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 ‹Nice Properties›


lemma EvExt_comp: ‹EvExt (g ∘ f) = EvExt g ∘ EvExt f›
  unfolding EvExt_def by (auto split: event.split)  
  


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))›
    by (auto simp add: F_Renaming D_Renaming EvExt_comp EvExt_ftF EvExt_tF front_tickFree_append)
       (metis (no_types, opaque_lifting) EvExt_comp list.map_comp set.compositionality)
next
  show ‹𝒟 (Renaming P (g ∘ f)) ⊆ 𝒟 (Renaming (Renaming P f) g)›
    by (simp add: D_Renaming subset_iff, safe)
       (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))›
    by (auto simp add: D_Renaming subset_iff)
       (metis EvExt_comp EvExt_tF front_tickFree_append)
qed




lemma Renaming_id: ‹Renaming P id = P›
  by (auto simp add: Process_eq_spec 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) 


subsection ‹Renaming Laws›

lemma Renaming_BOT: ‹Renaming ⊥ f = ⊥›
  by (fastforce simp add: F_UU D_UU F_Renaming D_Renaming EvExt_tF EvExt_ftF
                          Process_eq_spec front_tickFree_append intro: tickFree_Nil)+
  

lemma Renaming_STOP: ‹Renaming STOP f = STOP›
  by (subst Process_eq_spec) (simp add: EvExt_ftF F_STOP D_STOP F_Renaming D_Renaming)


lemma Renaming_SKIP: ‹Renaming SKIP f = SKIP›
  by (subst Process_eq_spec) (force simp add: EvExt_def F_SKIP D_SKIP F_Renaming D_Renaming)



lemma Renaming_Ndet:
  ‹Renaming (P ⊓ Q) f = Renaming P f ⊓ Renaming Q f›
  by (subst Process_eq_spec) (auto simp add: F_Renaming D_Renaming F_Ndet D_Ndet)


lemma Renaming_Det:
  ‹Renaming (P □ Q) f = Renaming P f □ Renaming Q f›
proof (subst Process_eq_spec, intro iffI conjI subset_antisym)
  show ‹ℱ (Renaming (P □ Q) f) ⊆ ℱ (Renaming P f □ Renaming Q f)›
    apply (simp add: F_Renaming D_Renaming T_Renaming F_Det D_Det, safe,
           simp_all add: is_processT6_S2)
    by blast+ (metis EvExt_eq_tick, meson map_EvExt_tick)+
next 
  show ‹ℱ (Renaming P f □ Renaming Q f) ⊆ ℱ (Renaming (P □ Q) f)›
    apply (simp add: F_Renaming D_Renaming T_Renaming F_Det D_Det, safe, simp_all)
    by blast+ (metis EvExt_eq_tick, metis Cons_eq_append_conv EvExt_tF 
                     list.map_disc_iff tickFree_Cons)+
next
  show ‹𝒟 (Renaming (P □ Q) f) ⊆ 𝒟 (Renaming P f □ Renaming Q f)›
    by (auto simp add: D_Renaming D_Det)
next
  show ‹𝒟 (Renaming P f □ Renaming Q f) ⊆ 𝒟 (Renaming (P □ Q) f)›
    by (auto simp add: D_Renaming D_Det)
qed


lemma mono_Mprefix_eq: ‹∀a ∈ A. P a = Q a ⟹ Mprefix A P = Mprefix A Q›
  by (auto simp add: Process_eq_spec F_Mprefix D_Mprefix)

lemma mono_Mndetprefix_eq: ‹∀a ∈ A. P a = Q a ⟹ Mndetprefix A P = Mndetprefix A Q›
  by (subst Process_eq_spec, cases ‹A = {}›) (auto simp add: F_Mndetprefix D_Mndetprefix)




lemma Renaming_Mprefix:
  ‹Renaming (□ a ∈ A → P (f a)) f = □ b ∈ f ` A → Renaming (P b) f›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Mprefix D_Renaming hd_map_EvExt) 
       (metis map_tl tickFree_tl)
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then obtain a s' where * : ‹a ∈ A› ‹s = EvExt f (ev a) # s'› ‹s' ∈ 𝒟 (Renaming (P (f a)) f)›
    by (auto simp add: D_Mprefix EvExt_def) (metis list.collapse)
  from "*"(3) obtain t1 t2
    where ** : ‹tickFree t1› ‹front_tickFree t2›
               ‹s' = map (EvExt f) t1 @ t2› ‹t1 ∈ 𝒟 (P (f a))›
    by (simp add: D_Renaming) blast
  show ‹s ∈ 𝒟 ?lhs›
    apply (simp add: D_Renaming "*"(2))
    apply (rule_tac x = ‹ev a # t1› in exI, simp add: "**"(1))
    by (rule_tac x = t2 in exI, simp add: "**"(2, 3, 4) "*"(1) D_Mprefix)
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (□a ∈ A → P (f a)) ∧ s = map (EvExt f) s1›
    by (simp add: F_Renaming D_Renaming) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (□a ∈ A → P (f a)) ∧ s = map (EvExt f) s1›
    then obtain s1 where * : ‹(s1, EvExt f -` X) ∈ ℱ (□a ∈ A → P (f a))›
                             ‹s = map (EvExt f) s1› by blast
    from "*"(1) consider ‹s1 = []› ‹EvExt f -` X ∩ ev ` A = {}›
      | ‹∃a s1'. a ∈ A ∧ s1 = ev a # s1' ∧ (s1', EvExt f -` X) ∈ ℱ (P (f a))›
      by (simp add: F_Mprefix) (metis event.inject imageE list.collapse)
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      show ‹s1 = [] ⟹ EvExt f -` X ∩ ev ` A = {} ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Mprefix "*"(2) disjoint_iff image_iff)
           (metis ev_elem_anteced1 vimage_eq)
    next
      assume ‹∃a s1'. a ∈ A ∧ s1 = ev a # s1' ∧ (s1', EvExt f -` X) ∈ ℱ (P (f a))›
      then obtain a s1' where ** : ‹a ∈ A› ‹s1 = ev a # s1'› 
                                   ‹(s1', EvExt f -` X) ∈ ℱ (P (f a))› by blast
      have *** : ‹EvExt f (ev a) = ev (f a)›
        by (metis hd_map hd_map_EvExt list.discI list.sel(1))
      show ‹(s, X) ∈ ℱ ?rhs›
        apply (simp add: F_Mprefix "*"(2) "**"(2), intro conjI)
        using "**"(1) "***" 
         apply blast
        apply (rule_tac x = ‹f a› in exI, simp add: "***")
        using "**"(3) by (simp add: F_Renaming) blast
    qed
  qed
next
  fix s X 
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹s = []› ‹X ∩ ev ` f ` A = {}›
    | ‹∃a s'. a ∈ A ∧ s = EvExt f (ev a) # s' ∧ (s', X) ∈ ℱ (Renaming (P (f a)) f)›
    by (auto simp add: F_Mprefix EvExt_def) (metis list.collapse)
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    show ‹s = [] ⟹ X ∩ ev ` f ` A = {} ⟹ (s, X) ∈ ℱ ?lhs›
      by (auto simp add: F_Renaming F_Mprefix disjoint_iff EvExt_def)
  next
    assume ‹∃a s'. a ∈ A ∧ s = EvExt f (ev a) # s' ∧ (s', X) ∈ ℱ (Renaming (P (f a)) f)›
    then obtain a s' where * : ‹a ∈ A› ‹s = EvExt f (ev a) # s'›
                               ‹(s', X) ∈ ℱ (Renaming (P (f a)) f)› by blast
    from "*"(3) consider ‹s' ∈ 𝒟 (Renaming (P (f a)) f)›
      | ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P (f a)) ∧ s' = map (EvExt f) s1›
      by (simp add: F_Renaming D_Renaming) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹s' ∈ 𝒟 (Renaming (P (f a)) f)›
      hence ‹s ∈ 𝒟 ?rhs›
        by (simp add: D_Mprefix "*"(2))
           (metis "*"(1) ev_elem_anteced1 imageI singletonI vimage_singleton_eq)
      with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
    next
      assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P (f a)) ∧ s' = map (EvExt f) s1›
      then obtain s1 where ** : ‹(s1, EvExt f -` X) ∈ ℱ (P (f a))›
                                ‹s' = map (EvExt f) s1› by blast
      show ‹(s, X) ∈ ℱ ?lhs›
        apply (simp add: F_Renaming "*"(2) "**"(2), rule disjI1)
        by (rule_tac x = ‹ev a # s1› in exI, simp add: F_Mprefix "*"(1) "**"(1))
    qed
  qed
qed



lemma Renaming_Mprefix_inj_on:
  ‹Renaming (Mprefix A P) f = □ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f› 
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_Mprefix[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›] mono_Mprefix_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)


corollary Renaming_Mprefix_inj:
  ‹Renaming (Mprefix A P) f = □ b ∈ f ` A → Renaming (P (THE a. f a = b)) f› if inj_f: ‹inj f›
  apply (subst Renaming_Mprefix_inj_on, metis inj_eq inj_onI that)
  apply (rule mono_Mprefix_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])



text ‹A smart application (as \<^term>‹f› is of course injective on the singleton \<^term>‹{a}›)›

corollary Renaming_prefix: ‹Renaming (a → P) f = (f a → Renaming P f)›
  unfolding write0_def by (simp add: Renaming_Mprefix_inj_on)

(* TODO: write corollaries on read and write *)



lemma Renaming_Mndetprefix:
  ‹Renaming (⊓ a ∈ A → P (f a)) f = ⊓ b ∈ f ` A → Renaming (P b) f›
  apply (cases ‹A = {}›, simp add: Renaming_STOP)
  by (subst Process_eq_spec)
     (auto simp add: F_Renaming F_Mndetprefix D_Renaming D_Mndetprefix Renaming_prefix[symmetric])


corollary Renaming_Mndetprefix_inj_on:
  ‹Renaming (Mndetprefix A P) f = ⊓ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f› 
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_Mndetprefix[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›] mono_Mndetprefix_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)
  


corollary Renaming_Mndetprefix_inj:
  ‹Renaming (Mndetprefix A P) f = ⊓ b ∈ f ` A →  Renaming (P (THE a. f a = b)) f› 
  if inj_f: ‹inj f›
  apply (subst Renaming_Mndetprefix_inj_on, metis inj_eq inj_onI that)
  apply (rule mono_Mndetprefix_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])



lemma Renaming_Seq: 
  ‹Renaming (P ❙; Q) f = Renaming P f ❙; Renaming Q f› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Seq D_Renaming T_Renaming)
       (metis map_EvExt_tick map_append)
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then consider ‹s ∈ 𝒟 (Renaming P f)›
    | ‹∃s1 s2. s = s1 @ s2 ∧ s1 @ [tick] ∈ 𝒯 (Renaming P f) ∧ s2 ∈ 𝒟 (Renaming Q f)›
    using D_Seq by blast
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    show ‹s ∈ 𝒟 (Renaming P f) ⟹ s ∈ 𝒟 ?lhs›
      by (auto simp add: D_Renaming D_Seq)
  next
    assume ‹∃s1 s2. s = s1 @ s2 ∧ s1 @ [tick] ∈ 𝒯 (Renaming P f) ∧ s2 ∈ 𝒟 (Renaming Q f)›
    then obtain s1 s2
      where * : ‹s = s1 @ s2› ‹s1 @ [tick] ∈ 𝒯 (Renaming P f)› ‹s2 ∈ 𝒟 (Renaming Q f)› by blast
    then obtain t1 t2 u1 u2
      where ** :  ‹t1 ∈ 𝒯 P ∧ s1 @ [tick] = map (EvExt f) t1 ∨
                  tickFree t1 ∧ front_tickFree t2 ∧ 
                  s1 @ [tick] = map (EvExt f) t1 @ t2 ∧ t1 ∈ 𝒟 P›
                 ‹tickFree u1› ‹front_tickFree u2› ‹s2 = map (EvExt f) u1 @ u2› ‹u1 ∈ 𝒟 Q›
      by (simp add: T_Renaming D_Renaming) blast
    have *** : ‹tickFree (butlast t1)›
      using "**"(1) front_tickFree_butlast is_processT2_TR tickFree_butlast by blast
    from "**"(1) show ‹s ∈ 𝒟 ?lhs›
      apply (rule disjE; simp add: D_Renaming D_Seq)
       apply (rule_tac x = ‹butlast t1 @ u1› in exI, simp add: "***" "**"(2))
       apply (rule_tac x = ‹u2› in exI, simp add: "**"(3), intro conjI,
          metis "*"(1) "**"(4) butlast_snoc map_butlast)
       apply (rule disjI2, rule_tac x = ‹butlast t1› in exI, rule_tac x = u1 in exI)
       apply (simp add: "**"(5), metis "***" EvExt_tF snoc_eq_iff_butlast tickFree_butlast)

      apply (rule_tac x = ‹if t2 = [] then butlast t1 else t1› in exI, intro conjI)
      using "***" 
       apply presburger
      apply (rule_tac x = ‹butlast t2 @ s2› in exI, intro conjI)
        apply (meson D_imp_front_tickFree ‹s2 ∈ 𝒟 (Renaming Q f)›
          front_tickFree_append front_tickFree_butlast)
       apply ((cases t1 rule: rev_cases; simp add: "*"(1) snoc_eq_iff_butlast),
          metis butlast.simps(2) butlast_append list.discI tick_eq_EvExt)
      by (metis EvExt_tF non_tickFree_tick tickFree_Nil tickFree_append)
  qed
next
  fix s X
  assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P ❙; Q) ∧ s = map (EvExt f) s1› | ‹s ∈ 𝒟 ?lhs›
    by (simp add: F_Renaming D_Renaming) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P ❙; Q) ∧ s = map (EvExt f) s1›
    then obtain s1 where * : ‹(s1, EvExt f -` X) ∈ ℱ (P ❙; Q)› ‹s = map (EvExt f) s1› by blast
    from this(1)[simplified F_Seq, simplified]
    show ‹(s, X) ∈ ℱ ?rhs›
      apply (elim disjE; simp add: F_Seq)
        apply (rule disjI1, simp add: F_Renaming, 
          metis (no_types, lifting) "*"(2) Diff_insert_absorb 
          EvExt_tF anteced_EvExt_diff_tick insertI1
          insert_Diff insert_absorb tick_elem_anteced1)
       apply (rule disjI2, rule disjI1, simp add: F_Renaming T_Renaming,
          metis (no_types, lifting) "*"(2) map_EvExt_tick map_append)
      apply (rule disjI2, rule disjI2, simp add: D_Renaming)
      apply (rule_tac x = ‹if tickFree s1 then s1 else butlast s1› in exI)
      by (auto simp add: "*"(2),
          metis NF_ND append_butlast_last_id front_tickFree_implies_tickFree
          is_processT2 tickFree_Nil,
          metis EvExt_tF front_tickFree_single map_butlast
          nonTickFree_n_frontTickFree process_charn snoc_eq_iff_butlast)
  next
    from NF_ND same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  qed
next
  fix s X
  assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?rhs›
  then consider ‹(s, insert tick X) ∈ ℱ (Renaming P f) ∧ tickFree s›
    | ‹∃s1 s2. s = s1 @ s2 ∧ s1 @ [tick] ∈ 𝒯 (Renaming P f) ∧ (s2, X) ∈ ℱ (Renaming Q f)›
    | ‹s ∈ 𝒟 ?rhs›
    by (simp add: F_Seq D_Seq) blast
  thus ‹(s, X) ∈ ℱ ?lhs›
  proof cases
    show ‹(s, insert tick X) ∈ ℱ (Renaming P f) ∧ tickFree s ⟹ (s, X) ∈ ℱ ?lhs›
      by (auto simp add: F_Renaming F_Seq D_Seq)
         (metis (no_types, lifting) Diff_insert_absorb EvExt_tF anteced_EvExt_diff_tick
                                    insertCI insert_Diff insert_absorb tick_elem_anteced1)
  next
    assume ‹∃s1 s2. s = s1 @ s2 ∧ s1 @ [tick] ∈ 𝒯 (Renaming P f) ∧ (s2, X) ∈ ℱ (Renaming Q f)›
    then obtain s1 s2 where * : ‹s = s1 @ s2› ‹s1 @ [tick] ∈ 𝒯 (Renaming P f)›
                                ‹(s2, X) ∈ ℱ (Renaming Q f)› by blast
    from "*"(2, 3) obtain t1 u1 where ** : 
      ‹t1 ∈ 𝒯 P ∧ s1 @ [tick] = map (EvExt f) t1 ∨ 
       tickFree t1 ∧ (∃t2. front_tickFree t2 ∧ s1 @ [tick] = map (EvExt f) t1 @ t2 ∧ t1 ∈ 𝒟 P)›
      ‹(u1, EvExt f -` X) ∈ ℱ Q ∧ s2 = map (EvExt f) u1 ∨
       tickFree u1 ∧ (∃u2. front_tickFree u2 ∧ s2 = map (EvExt f) u1 @ u2 ∧ u1 ∈ 𝒟 Q)›
      by (simp add: F_Renaming T_Renaming) blast
    show ‹(s, X) ∈ ℱ ?lhs›
      using "**"(1) 
      apply (elim disjE conjE exE; simp add: "*"(1) F_Renaming D_Seq)
      using "**"(2) 
       apply (elim disjE conjE exE)
        apply (rule disjI1, simp add: F_Seq,
          metis (no_types, lifting) "*"(1) append_eq_map_conv map_EvExt_tick)
       apply (rule disjI2, simp add: D_Seq)
       apply (rule_tac x = ‹butlast t1 @ u1› in exI, intro conjI)
      using front_tickFree_butlast is_processT2_TR tickFree_append 
        apply blast
       apply (rule_tac x = u2 in exI, intro conjI, blast,
          metis append.assoc butlast_snoc map_append map_butlast,
          metis EvExt_tF T_nonTickFree_imp_decomp snoc_eq_iff_butlast tickFree_butlast)
      apply (rule disjI2)
      apply (rule_tac x = ‹if t2 ≠ [] then t1 else tl t1› in exI, intro conjI)
       apply (metis (mono_tags, opaque_lifting) tickFree_tl tl_Nil)
      apply (rule_tac x = ‹(butlast t2) @ s2› in exI, intro conjI)
        apply (meson "*"(3) front_tickFree_append front_tickFree_butlast process_charn)
       apply (simp, metis EvExt_tF butlast_append butlast_snoc non_tickFree_tick tickFree_append)
      by (metis EvExt_tF non_tickFree_tick self_append_conv tickFree_append)
  next
    from NF_ND same_div show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
  qed
qed






lemma mono_Renaming_D: ‹P ⊑⇩D Q ⟹ Renaming P f ⊑⇩D Renaming Q f›
  unfolding divergence_refine_def D_Renaming by blast


lemma mono_Renaming_FD: ‹P ⊑⇩F⇩D Q ⟹ Renaming P f ⊑⇩F⇩D Renaming Q f›
  unfolding failure_divergence_refine_def le_ref_def
  apply (simp add: mono_Renaming_D[unfolded divergence_refine_def])
  unfolding F_Renaming D_Renaming by blast


lemma mono_Renaming_DT: ‹P ⊑⇩D⇩T Q ⟹ Renaming P f ⊑⇩D⇩T Renaming Q f›
  unfolding trace_divergence_refine_def 
  apply (simp add: mono_Renaming_D)
  unfolding trace_refine_def divergence_refine_def T_Renaming by blast






section‹Assertions›

abbreviation deadlock_free⇩S⇩K⇩I⇩P :: "'a process ⇒ bool"
  where   "deadlock_free⇩S⇩K⇩I⇩P ≡ deadlock_free_v2"


lemma deadlock_free_implies_lifelock_free: ‹deadlock_free P ⟹ lifelock_free P›
  unfolding deadlock_free_def lifelock_free_def
  using CHAOS_DF_refine_FD trans_FD by blast

lemmas deadlock_free⇩S⇩K⇩I⇩P_def = deadlock_free_v2_def
   and deadlock_free⇩S⇩K⇩I⇩P_is_right = deadlock_free_v2_is_right
   and deadlock_free⇩S⇩K⇩I⇩P_implies_div_free = deadlock_free_v2_implies_div_free
   and deadlock_free⇩S⇩K⇩I⇩P_FD = deadlock_free_v2_FD
   and deadlock_free⇩S⇩K⇩I⇩P_is_right_wrt_events = deadlock_free_v2_is_right_wrt_events
   and deadlock_free_is_deadlock_free⇩S⇩K⇩I⇩P = deadlock_free_is_deadlock_free_v2
   and deadlock_free⇩S⇩K⇩I⇩P_SKIP = deadlock_free_v2_SKIP
   and non_deadlock_free⇩S⇩K⇩I⇩P_STOP = non_deadlock_free_v2_STOP


section ‹Non-terminating Runs›

definition non_terminating  :: "'a process ⇒ bool"
  where   "non_terminating P ≡ RUN UNIV ⊑⇩T P"

corollary non_terminating_refine_DF: "non_terminating P = DF UNIV ⊑⇩T P"
  and non_terminating_refine_CHAOS: "non_terminating P = CHAOS UNIV ⊑⇩T P"
  by (simp_all add: DF_all_tickfree_traces1 RUN_all_tickfree_traces1 CHAOS_all_tickfree_traces1 
                    non_terminating_def trace_refine_def)

lemma non_terminating_is_right: "non_terminating P ⟷ (∀s ∈ 𝒯 P. tickFree s)"
  apply (rule iffI)
  by (auto simp add:non_terminating_def trace_refine_def tickFree_def RUN_all_tickfree_traces1)[1]
     (auto simp add:non_terminating_def trace_refine_def RUN_all_tickfree_traces2)

lemma nonterminating_implies_div_free: "non_terminating P ⟹ 𝒟 P = {}"
  unfolding non_terminating_is_right
  by (metis NT_ND equals0I front_tickFree_charn process_charn tickFree_Cons tickFree_append) 

lemma non_terminating_implies_F: "non_terminating P ⟹ CHAOS UNIV ⊑⇩F P"
  using CHAOS_has_all_tickFree_failures F_T 
  by (auto simp add: non_terminating_is_right failure_refine_def) blast


corollary non_terminating_F: "non_terminating P = CHAOS UNIV ⊑⇩F P"
  by (auto simp add:non_terminating_implies_F non_terminating_refine_CHAOS leF_imp_leT)

corollary non_terminating_FD: "non_terminating P = CHAOS UNIV ⊑⇩F⇩D P"
  unfolding non_terminating_F
  using div_free_CHAOS nonterminating_implies_div_free leFD_imp_leF
        leF_leD_imp_leFD divergence_refine_def non_terminating_F 
  by fastforce 


section ‹Lifelock Freeness›

corollary lifelock_free_is_non_terminating: "lifelock_free P = non_terminating P"
  unfolding lifelock_free_def non_terminating_FD by simp

lemma div_free_divergence_refine:
  "𝒟 P = {} ⟷ CHAOS⇩S⇩K⇩I⇩P UNIV ⊑⇩D P" 
  "𝒟 P = {} ⟷ CHAOS UNIV    ⊑⇩D P" 
  "𝒟 P = {} ⟷ RUN UNIV      ⊑⇩D P" 
  "𝒟 P = {} ⟷ DF⇩S⇩K⇩I⇩P UNIV    ⊑⇩D P" 
  "𝒟 P = {} ⟷ DF UNIV       ⊑⇩D P" 
  by (simp_all add: div_free_CHAOS⇩S⇩K⇩I⇩P div_free_CHAOS div_free_RUN div_free_DF 
                    div_free_DF⇩S⇩K⇩I⇩P divergence_refine_def)

definition lifelock_free⇩S⇩K⇩I⇩P :: "'a process ⇒ bool"
  where   "lifelock_free⇩S⇩K⇩I⇩P P ≡ CHAOS⇩S⇩K⇩I⇩P UNIV ⊑⇩F⇩D P"

lemma div_free_is_lifelock_free⇩S⇩K⇩I⇩P: "lifelock_free⇩S⇩K⇩I⇩P P ⟷ 𝒟 P = {}"
  using CHAOS⇩S⇩K⇩I⇩P_has_all_failures_Un leFD_imp_leD leF_leD_imp_leFD
        div_free_divergence_refine(1) lifelock_free⇩S⇩K⇩I⇩P_def 
  by blast
  
lemma lifelock_free_is_lifelock_free⇩S⇩K⇩I⇩P: "lifelock_free P ⟹ lifelock_free⇩S⇩K⇩I⇩P P"
  by (simp add: leFD_imp_leD div_free_divergence_refine(2) div_free_is_lifelock_free⇩S⇩K⇩I⇩P lifelock_free_def)

corollary deadlock_free⇩S⇩K⇩I⇩P_is_lifelock_free⇩S⇩K⇩I⇩P: "deadlock_free⇩S⇩K⇩I⇩P P ⟹ lifelock_free⇩S⇩K⇩I⇩P P"
  by (simp add: deadlock_free⇩S⇩K⇩I⇩P_implies_div_free div_free_is_lifelock_free⇩S⇩K⇩I⇩P)


section ‹New Laws›

lemma non_terminating_Seq: 
  ‹non_terminating P ⟹ (P ❙; Q) = P›
  unfolding non_terminating_is_right apply (subst Process_eq_spec, intro conjI)
  apply (auto simp add: F_Seq is_processT7 F_T)[1]
  using is_processT4 apply blast
  using process_charn apply blast
   apply (metis F_T Un_commute insert_is_Un is_processT5_S2 non_tickFree_tick tickFree_append)
  by (auto simp add: D_Seq)
 

lemma non_terminating_Sync: 
  ‹non_terminating P ⟹ lifelock_free⇩S⇩K⇩I⇩P Q ⟹ non_terminating (P ⟦A⟧ Q)›
  apply (simp add: non_terminating_is_right div_free_is_lifelock_free⇩S⇩K⇩I⇩P T_Sync)
  apply (intro ballI, simp add: non_terminating_is_right nonterminating_implies_div_free)
  by (metis empty_iff ftf_Sync1 ftf_Sync21 insertI1 tickFree_def)


lemmas non_terminating_Par = non_terminating_Sync[where A = ‹UNIV›]
   and non_terminating_Inter = non_terminating_Sync[where A = ‹{}›]





syntax
  "_writeS"  :: "['b ⇒ 'a, pttrn, 'b set, 'a process] => 'a process"  ("(4(_❙!_❙|_) /→ _)" [0,0,50,78] 50)
translations
  "_writeS c p b P"  => "CONST Mndetprefix (c ` {p. b}) (λ_. P)"





end