Theory Throw

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : The Throw operator
 *
 * 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.
 ******************************************************************************›
(*>*)

section‹ The Throw Operator ›

theory  Throw
  imports "HOL-CSPM.CSPM"
begin


(*<*)

―‹This result should be in session‹HOL-CSP›.›
lemma Refusals_iff : X   P  ([], X)   P
  by (simp add: Failures.rep_eq REFUSALS_def Refusals.rep_eq)
(*>*)


subsection ‹Definition›

text ‹The Throw operator allows error handling. Whenever an error (or more generally any 
      event termev e  ev ` A) occurs in termP, termP is shut down and termQ e is started.

      This operator can somehow be seen as a generalization of sequential composition constSeq:
      termP terminates on any event in termev ` A rather than consttick
      (however it do not hide these events like constSeq do for consttick,
      but we can use an additional termλP. (P \ A)).

      This is a relatively new addition to CSP 
      (see cite‹p.140› in "Roscoe2010UnderstandingCS").›

lift_definition Throw :: [ process,  set,    process]   process
  is λ P A Q. 
  ({(t1, X)   P. set t1  ev ` A = {}} 
   {(t1 @ t2, X)| t1 t2 X. t1  𝒟 P  tickFree t1  
                           set t1  ev ` A = {}  front_tickFree t2} 
   {(t1 @ ev a # t2, X)| t1 a t2 X. t1 @ [ev a]  𝒯 P  set t1  ev ` A = {} 
                                    a  A  (t2, X)   (Q a)},
   {t1 @ t2| t1 t2. t1  𝒟 P  tickFree t1  
                    set t1  ev ` A = {}  front_tickFree t2}  
   {t1 @ ev a # t2| t1 a t2. t1 @ [ev a]  𝒯 P  set t1  ev ` A = {}  
                             a  A  t2  𝒟 (Q a)})
proof -
  show ?thesis P A Q (is is_process (?f, ?d)) for P A Q
    unfolding is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv
  proof (intro conjI allI impI; (elim conjE)?)
    show ([], {})  ?f by (simp add: is_processT1)
  next
    show (s, X)  ?f  front_tickFree s for s X
      apply (simp, elim disjE exE)
      subgoal by (metis is_processT)
      subgoal by (solves simp add: front_tickFree_append)
      by (metis F_T append_Cons append_Nil append_T_imp_tickFree butlast.simps(2) event.simps(3)
                front_tickFree_append is_processT2_TR last_ConsL not_Cons_self tickFree_butlast)
  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 b t)
      consider (s @ t @ [b], {})   P (set s  set t)  ev ` A = {}
        | t1 t2. s @ t @ [b] = t1 @ t2  t1  𝒟 P  tickFree t1  
                   set t1  ev ` A = {}  front_tickFree t2 
                   (a. s @ t @ [b] = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                        set t1  ev ` A = {}  a  A  (t2, {})   (Q a))
        using snoc.prems by simp blast
      thus (s, {})  ?f
      proof cases
        show (s @ t @ [b], {})   P  (set s  set t)  ev ` A = {}  (s, {})  ?f
          by (drule is_processT3[rule_format]) (simp add: Int_Un_distrib2)
      next
        assume t1 t2. s @ t @ [b] = t1 @ t2  t1  𝒟 P  tickFree t1  
                   set t1  ev ` A = {}  front_tickFree t2 
                   (a. s @ t @ [b] = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                        set t1  ev ` A = {}  a  A  (t2, {})   (Q a))
           (is t1 t2. ?disj t1 t2)
        then obtain t1 t2 where ?disj t1 t2 by blast
        show (s, {})  ?f
        apply (rule snoc.hyps)
          using ?disj t1 t2 apply (elim disjE exE)
           apply (all cases t2 rule: rev_cases, simp_all)
          subgoal by (metis Int_Un_distrib2 T_F D_T Un_empty append.assoc is_processT3_SR set_append)
          subgoal by (metis front_tickFree_dw_closed) 
          subgoal by (meson T_F process_charn)
          by (metis process_charn)
      qed
    qed
  next
    show (s, Y)  ?f  X  Y  (s, X)  ?f for s X Y
      by simp (metis is_processT4)
  next
    fix s X Y
    assume assms : (s, X)  ?f c. c  Y  (s @ [c], {})  ?f
    consider (s, X)   P set s  ev ` A = {}
      | t1 t2. s = t1 @ t2  t1  𝒟 P  tickFree t1  
                 set t1  ev ` A = {}  front_tickFree t2
      | t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                   set t1  ev ` A = {}  a  A  (t2, X)   (Q a)
      using assms(1) by blast
    thus (s, X  Y)  ?f
    proof cases
      assume * : (s, X)   P set s  ev ` A = {}
      have (s @ [c], {})   P if c  Y for c
      proof (cases c  ev ` A)
        from "*"(2) assms(2)[rule_format, OF that]
        show c  ev ` A  (s @ [c], {})   P
          by auto (metis F_T is_processT1)
      next
        from "*"(2) assms(2)[rule_format, OF that]
        show c  ev ` A  (s @ [c], {})   P by simp
      qed
      with "*"(1) is_processT5 have (s, X  Y)   P by blast
      with "*"(2) show (s, X  Y)  ?f by blast
    next
      assume t1 t2. s = t1 @ t2  t1  𝒟 P  tickFree t1  
                      set t1  ev ` A = {}  front_tickFree t2
      hence s  ?d by blast
      thus (s, X  Y)  ?f by simp (metis NF_ND)
    next
      assume t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                        set t1  ev ` A = {}  a  A  (t2, X)   (Q a)
      then obtain t1 a t2
        where * : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 P 
                  set t1  ev ` A = {} a  A (t2, X)   (Q a) by blast
      have (t2 @ [c], {})   (Q a) if c  Y for c
        using assms(2)[rule_format, OF that, simplified, THEN conjunct2,
                       THEN conjunct2, rule_format, of a t1 t2 @ [c]]
        by (simp add: "*"(1, 2, 3, 4))
      with "*"(5) is_processT5 have ** : (t2, X  Y)   (Q a) by blast
      show (s, X  Y)  ?f
        using "*"(1, 2, 3, 4) "**" by blast
    qed
  next
    have * : s t1 a t2. s @ [tick] = t1 @ ev a # t2  t2'. t2 = t2' @ [tick]
      by (simp add: snoc_eq_iff_butlast split: if_split_asm)
         (metis append_butlast_last_id)
    show (s @ [tick], {})  ?f  (s, X - {tick})  ?f for s X
      apply (simp, elim disjE exE conjE)
      subgoal by (solves simp add: is_processT6)
      subgoal by (metis butlast_append butlast_snoc front_tickFree_butlast 
            non_tickFree_tick tickFree_Nil tickFree_append 
            tickFree_implies_front_tickFree)
      by (frule "*", elim exE, simp, metis is_processT6)
  next
    show s  ?d; tickFree s; front_tickFree t  s @ t  ?d for s t
      by auto (metis front_tickFree_append, metis is_processT7)
  next
    show s  ?d  (s, X)  ?f for s X
      by simp (metis NF_ND)
     
  next
    show s @ [tick]  ?d  s  ?d for s 
      apply (simp, elim disjE)
      by (metis butlast_append butlast_snoc front_tickFree_butlast non_tickFree_tick
                tickFree_Nil tickFree_append tickFree_implies_front_tickFree)
         (metis D_T T_nonTickFree_imp_decomp append_single_T_imp_tickFree
                butlast.simps(2) butlast_append butlast_snoc event.distinct(1)
                process_charn tickFree_Cons tickFree_append)
  qed
qed


text ‹We add some syntactic sugar.›

syntax "_Throw" :: [ process, pttrn,  set,    process]   process
                   (((_) Θ (__)./ (_)) [73, 0, 0, 73] 72)
translations "P Θ a  A. Q"  "CONST Throw P A (λa. Q)"

abbreviation Throw_without_free_var :: 
  [ process,  set,  process]   process (((_) Θ (_)/ (_)) [73, 0, 73] 72)
  where P Θ A Q  P Θ a  A. Q

text ‹Now we can write @{term [eta_contract = false] P Θ a  A. Q a}, and when
      we do not want termQ to be parameterized we can just write termP Θ A Q.›

lemma P Θ a  A. Q = P Θ A Q by (fact refl)



subsection ‹Projections›

lemma F_Throw:
   (P Θ a  A. Q a) =
   {(t1, X)   P. set t1  ev ` A = {}} 
   {(t1 @ t2, X)| t1 t2 X.
    t1  𝒟 P  tickFree t1  set t1  ev ` A = {}  front_tickFree t2} 
   {(t1 @ ev a # t2, X)| t1 a t2 X.
    t1 @ [ev a]  𝒯 P  set t1  ev ` A = {}  a  A  (t2, X)   (Q a)}
  by (simp add: Failures_def FAILURES_def Throw.rep_eq)
  (* by (simp add: Failures.rep_eq FAILURES_def Throw.rep_eq) *)


lemma D_Throw:
  𝒟 (P Θ a  A. Q a) =
   {t1 @ t2| t1 t2.
    t1  𝒟 P  tickFree t1  set t1  ev ` A = {}  front_tickFree t2} 
   {t1 @ ev a # t2| t1 a t2.
    t1 @ [ev a]  𝒯 P  set t1  ev ` A = {}  a  A  t2  𝒟 (Q a)}
  by (simp add: Divergences_def DIVERGENCES_def Throw.rep_eq)
  (* by (simp add: Divergences.rep_eq DIVERGENCES_def Throw.rep_eq) *)


lemma T_Throw:
  𝒯 (P Θ a  A. Q a) =
   {t1  𝒯 P. set t1  ev ` A = {}} 
   {t1 @ t2| t1 t2.
    t1  𝒟 P  tickFree t1  set t1  ev ` A = {}  front_tickFree t2} 
   {t1 @ ev a # t2| t1 a t2. 
    t1 @ [ev a]  𝒯 P  set t1  ev ` A = {}  a  A  t2  𝒯 (Q a)}
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Throw) blast+



subsection ‹Monotony›

lemma min_elems_Un_subset:
  min_elems (A  B)  min_elems A  (min_elems B - A)
  by (auto simp add: min_elems_def subset_iff)

lemma mono_Throw[simp] : P Θ a  A. Q a  P' Θ a  A. Q' a 
  if P  P' and a  A. Q a  Q' a
proof (unfold le_approx_def Ra_def, safe)
  from le_approx1[OF that(1)] le_approx_lemma_T[OF that(1)] 
       le_approx1[OF that(2)[rule_format]] 
  show s  𝒟 (P' Θ a  A. Q' a)  s  𝒟 (P Θ a  A. Q a) for s 
    by (simp add: D_Throw subset_iff) metis
next
  fix s X
  assume assms : s  𝒟 (P Θ a  A. Q a) (s, X)   (P Θ a  A. Q a)
  from assms(2) consider (s, X)   P set s  ev ` A = {}
    | t1 t2. s = t1 @ t2  t1  𝒟 P  tickFree t1  
               set t1  ev ` A = {}  front_tickFree t2
    | t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P 
                 set t1  ev ` A = {}  a  A  (t2, X)   (Q a)
    by (simp add: F_Throw) blast
  thus (s, X)   (P' Θ a  A. Q' a)
  proof cases
    assume * : (s, X)   P set s  ev ` A = {}
    from assms(1)[simplified D_Throw, simplified, THEN conjunct1, rule_format, of s]
         assms(1)[simplified D_Throw, simplified, THEN conjunct1, rule_format, of butlast s]
    have ** : s  𝒟 P 
      using "*"(2) apply (cases tickFree s, auto)
      by (metis append_butlast_last_id disjoint_iff front_tickFree_butlast 
          front_tickFree_single in_set_butlastD process_charn tickFree_butlast)
    show (s, X)   P  set s  ev ` A = {}  (s, X)   (Throw P' A Q')
      by (simp add: F_Throw le_approx2[OF that(1) "**"])
  next
    assume t1 t2. s = t1 @ t2  t1  𝒟 P  tickFree t1  
                    set t1  ev ` A = {}  front_tickFree t2
    with assms(1) show (s, X)   (Throw P' A Q') 
      by (simp add: F_Throw D_Throw)
  next
    assume t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                      set t1  ev ` A = {}  a  A  (t2, X)   (Q a)
    then obtain t1 a t2 
      where * : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 P 
                set t1  ev ` A = {} a  A (t2, X)   (Q a) by blast
    from "*"(2) append_single_T_imp_tickFree have ** : tickFree t1 by blast
    have *** : (t2, X)   (Q' a) 
      by (fact assms(1)[simplified D_Throw, simplified, THEN conjunct2, rule_format,
                        OF "*"(4, 3, 2, 1), THEN le_approx2[OF that(2)[rule_format, OF "*"(4)]], 
                        of X, simplified "*"(5), simplified])
    have **** : t1  𝒟 P
      apply (rule notI)
      apply (drule assms(1)[simplified D_Throw, simplified, THEN conjunct1, rule_format,
                            OF "*"(3) "**", of ev a # t2, simplified "*"(1), simplified])
      by (metis "*"(1) assms(2) front_tickFree_mono process_charn)
    show (s, X)   (Throw P' A Q')
      apply (simp add: F_Throw D_Throw "*"(1))
      by (metis "*"(2, 3, 4) "***" "****" T_F_spec le_approx2 min_elems6 that(1))
  qed
next
  from le_approx1[OF that(1)] le_approx2[OF that(1)] le_approx2T[OF that(1)]
       le_approx2[OF that(2)[rule_format]]
  show s  𝒟 (P Θ a  A. Q a)  
        (s, X)   (P' Θ a  A. Q' a)  (s, X)   (P Θ a  A. Q a) for s X
    apply (simp add: F_Throw D_Throw subset_eq, safe, simp_all)
    by (meson NF_ND) (metis D_T)+
next
  define S_left 
    where S_left  {t1 @ t2 |t1 t2. t1  𝒟 P  tickFree t1  
                     set t1  ev ` A = {}  front_tickFree t2}
  define S_right 
    where S_right  {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a]  𝒯 P 
                      set t1  ev ` A = {}  a  A  t2  𝒟 (Q a)}

  have * : min_elems (𝒟 (P Θ a  A. Q a))  min_elems S_left  (min_elems S_right - S_left)
    unfolding S_left_def S_right_def 
    by (simp add: D_Throw min_elems_Un_subset)
  have ** : min_elems S_left = {t1  min_elems (𝒟 P). set t1  ev ` A = {}}
    unfolding S_left_def min_elems_def le_list_def less_list_def
    apply (simp, safe)
    subgoal by (solves meson is_processT7_S) 
    subgoal by (metis Int_Un_distrib2 Un_empty append.right_neutral front_tickFree_Nil
          front_tickFree_append front_tickFree_mono set_append)
    subgoal by (metis IntI append_Nil2 front_tickFree_Nil imageI)  
    subgoal by (metis list.distinct(1) nonTickFree_n_frontTickFree process_charn self_append_conv)
    by (metis Nil_is_append_conv append_eq_appendI self_append_conv) 

  { fix t1 a t2
    assume assms : t1 @ [ev a]  𝒯 P set t1  ev ` A = {} a  A
                   t2  (𝒟 (Q a)) t1 @ ev a # t2  min_elems S_right t1 @ ev a # t2  S_left
    have t2  min_elems (𝒟 (Q a)) 
         t1 @ [ev a]  𝒟 P  t1 @ [ev a]  min_elems (𝒟 P)
    proof (all rule ccontr)
      assume t2  min_elems (𝒟 (Q a))
      with assms(4) obtain t2' where t2' < t2 t2'  𝒟 (Q a) 
        unfolding min_elems_def by blast
      hence t1 @ ev a # t2'  S_right t1 @ ev a # t2' < t1 @ ev a # t2 
        unfolding S_right_def using assms(1, 2, 3) 
        by (auto simp add: less_append less_cons)
      with assms(5) min_elems_no nless_le show False by blast
    next
      assume t1 @ [ev a]  𝒟 P t1 @ [ev a]  min_elems (𝒟 P)
      hence t1  𝒟 P using min_elems1 by blast
      with t1 @ [ev a]  𝒟 P have t1 @ ev a # t2  S_left
        by (simp add: S_left_def)
           (metis D_imp_front_tickFree append_Cons append_Nil assms(2, 4)
                  event.simps(3) front_tickFree_append tickFree_Nil
                  front_tickFree_implies_tickFree tickFree_Cons)
      with assms(6) show False by simp
    qed
  } note *** = this
  have **** : min_elems S_right - S_left  
               {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a]  𝒯 P - 𝒟 P 
                set t1  ev ` A = {}  a  A  t2  min_elems (𝒟 (Q a))} 
               {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a]  min_elems (𝒟 P) 
                set t1  ev ` A = {}  a  A  t2  min_elems (𝒟 (Q a))}
    apply (intro subsetI, simp, elim conjE)
    apply (frule set_mp[OF min_elems_le_self], subst (asm) (2) S_right_def)
    using "***" by fastforce

  fix s
  assume assm: s  min_elems (𝒟 (P Θ a  A. Q a))
  from set_mp[OF "*", OF this] 
  consider s  min_elems (𝒟 P) set s  ev ` A = {}
    | t1 a t2.
       s = t1 @ ev a # t2  set t1  ev ` A = {}  a  A  t2  min_elems (𝒟 (Q a)) 
       (t1 @ [ev a]  min_elems (𝒟 P)  t1 @ [ev a]  𝒯 P  t1 @ [ev a]  𝒟 P)
    using "****" by (simp add: "**") blast 
  thus s  𝒯 (P' Θ a  A. Q' a)
  proof cases
    show s  min_elems (𝒟 P)  set s  ev ` A = {}  s  𝒯 (Throw P' A Q')
      by (drule set_mp[OF le_approx3[OF that(1)]], simp add: T_Throw)
  next
    assume t1 a t2.
            s = t1 @ ev a # t2  set t1  ev ` A = {}  a  A  t2  min_elems (𝒟 (Q a)) 
            (t1 @ [ev a]  min_elems (𝒟 P)  t1 @ [ev a]  𝒯 P  t1 @ [ev a]  𝒟 P)
    then obtain t1 a t2
      where ***** : s = t1 @ ev a # t2 set t1  ev ` A = {}
                    a  A t2  min_elems (𝒟 (Q a))
                    t1 @ [ev a]  min_elems (𝒟 P)  
                     t1 @ [ev a]  𝒯 P  t1 @ [ev a]  𝒟 P by blast
    have t1 @ [ev a]  𝒯 P'  t2  𝒯 (Q' a)
      by (meson "*****"(3, 4, 5) le_approx2T le_approx3 subsetD that)
    with "*****" show s  𝒯 (Throw P' A Q')
      by (simp add: T_Throw) blast
  qed
qed


lemma mono_right_Throw_F :
  a  A. Q a F Q' a  P Θ a  A. Q a F P Θ a  A. Q' a
  unfolding failure_refine_def
  by (simp add: F_Throw subset_iff disjoint_iff) blast

lemma mono_right_Throw_T : 
  a  A. Q a T Q' a  P Θ a  A. Q a T P Θ a  A. Q' a
  unfolding trace_refine_def
  by (simp add: T_Throw subset_iff disjoint_iff) blast

lemma mono_right_Throw_D: 
  a  A. Q a D Q' a  P Θ a  A. Q a D P Θ a  A. Q' a
  unfolding divergence_refine_def
  by (simp add: D_Throw subset_iff disjoint_iff) blast

lemma mono_Throw_FD : P FD P'  a  A. Q a FD Q' a 
                       P Θ a  A. Q a FD P' Θ a  A. Q' a
  apply (rule trans_FD[of _ P' Θ a  A. Q a])
  subgoal by (simp add: failure_divergence_refine_def 
                    le_ref_def F_Throw D_Throw subset_iff; safe;
          metis [[metis_verbose = false]] T_F no_Trace_implies_no_Failure)
  by (meson leFD_imp_leD leFD_imp_leF leF_leD_imp_leFD 
            mono_right_Throw_D mono_right_Throw_F)

lemma mono_Throw_DT : P DT P'  a  A. Q a DT Q' a 
                       P Θ a  A. Q a DT P' Θ a  A. Q' a
  apply (rule trans_DT[of _ P' Θ a  A. Q a])
  subgoal by (simp add: trace_divergence_refine_def trace_refine_def 
                   divergence_refine_def D_Throw T_Throw subset_iff, blast)
  by (simp add: mono_right_Throw_D mono_right_Throw_T trace_divergence_refine_def)



subsection ‹Properties›

lemma Throw_STOP: STOP Θ a  A. Q a = STOP
  by (auto simp add: STOP_iff_T T_Throw T_STOP D_STOP) 

lemma Throw_SKIP: SKIP Θ a  A. Q a = SKIP
  by (auto simp add: Process_eq_spec F_Throw F_SKIP D_Throw D_SKIP T_SKIP)

lemma Throw_BOT:  Θ a  A. Q a = 
  by (simp add: BOT_iff_D D_Throw D_UU)

lemma Throw_is_BOT_iff: P Θ a  A. Q a =   P = 
  by (simp add: BOT_iff_D D_Throw) 


lemma Throw_empty_set: P Θ a  {}. Q a = P
  by (auto simp add: Process_eq_spec F_Throw D_Throw 
                     D_expand[symmetric] is_processT7_S is_processT8_S)


lemma Throw_Ndet:
  P  P' Θ a  A. Q a = (P Θ a  A. Q a)  (P' Θ a  A. Q a)
  P Θ a  A. Q a  Q' a = (P Θ a  A. Q a)  (P Θ a  A. Q' a)
  by (simp add: Process_eq_spec F_Throw F_Ndet D_Throw D_Ndet T_Ndet,
      safe, simp_all; blast)+

lemma Throw_Det:
  P  P' Θ a  A. Q a = (P Θ a  A. Q a)  (P' Θ a  A. Q a)
  P Θ a  A. Q a  Q' a = (P Θ a  A. Q a)  (P Θ a  A. Q' a)
proof -
  show Throw (P  P') A Q = Throw P A Q  Throw P' A Q (is ?lhs = ?rhs)
  proof (subst Process_eq_spec_optimized, safe)
    show s  𝒟 ?lhs  s  𝒟 ?rhs for s
      by (auto simp add: D_Det T_Det D_Throw)
  next
    show s  𝒟 ?rhs  s  𝒟 ?lhs for s
      by (simp add: D_Det T_Det D_Throw) blast
  next
    fix s X
    assume same_div: 𝒟 ?lhs = 𝒟 ?rhs
    assume (s, X)   ?lhs
    hence (s, X)   (P  P')  set s  ev ` A = {}  s  𝒟 ?lhs 
           (t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 (P  P')  
                      set t1  ev ` A = {}  a  A  (t2, X)   (Q a))
      by (simp add: F_Throw D_Throw) blast
    thus (s, X)   ?rhs
      apply (elim disjE exE)
      subgoal by (cases s, auto simp add: F_Det F_Throw T_Throw D_Throw)[1]
      subgoal by (use D_F same_div in blast)
      by (auto simp add: F_Det T_Det F_Throw T_Throw D_Throw)
  next
    show (s, X)   ?rhs  (s, X)   ?lhs for s X
      apply (simp add: F_Det, elim disjE conjE)
      by (auto simp add: F_Det D_Det T_Det F_Throw D_Throw 
                         T_Throw D_T is_processT7_S subset_iff)
         (simp_all add: Cons_eq_append_conv)
  qed
next
  show P Θ a  A. Q a  Q' a = Throw P A Q  Throw P A Q' (is ?lhs Q Q' = ?rhs)
  proof (subst Process_eq_spec_optimized, safe)
    show s  𝒟 (?lhs Q Q')  s  𝒟 ?rhs for s
      by (auto simp add: D_Det D_Throw D_Ndet)
  next
    show s  𝒟 ?rhs  s  𝒟 (?lhs Q Q') for s
      by (simp add: D_Det D_Throw D_Ndet) blast
  next
    fix s X
    assume same_div: 𝒟 (?lhs Q Q') = 𝒟 ?rhs
    assume (s, X)   (?lhs Q Q')
    hence (s, X)   P  set s  ev ` A = {}  s  𝒟 (?lhs Q Q') 
           (t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                      set t1  ev ` A = {}  a  A  (t2, X)   (Q a  Q' a))
      by (simp add: F_Throw D_Throw) blast
    thus (s, X)   ?rhs
      apply (elim disjE exE)
      subgoal by (solves simp add: F_Det F_Throw)
      subgoal by (use D_F same_div in blast)
      by (auto simp add: F_Det F_Ndet F_Throw)
  next
    show (s, X)   ?rhs  (s, X)   (?lhs Q Q') for s X
    proof (cases s)
      show s = []  (s, X)   ?rhs  (s, X)   (?lhs Q Q')
        by (auto simp add: F_Det F_Throw D_Throw T_Throw 
                           is_processT6_S2 Cons_eq_append_conv)
    next
      fix a s'
      have * : (a # s', X)   (Throw P A Q) 
                (a # s', X)   (?lhs Q Q') for Q Q'
        by (auto simp add: F_Throw F_Det F_Ndet)
      show s = a # s'  (s, X)   ?rhs  (s, X)   (?lhs Q Q')
        apply (simp add: F_Det, elim disjE)
        subgoal by (erule "*")
        by (subst Ndet_commute) (erule "*")
    qed
  qed
qed

lemma Throw_GlobalNdet:
  (a  A. P a) Θ b  B. Q b = a  A. (P a Θ b  B. Q b)
  P' Θ a  A. (b  B. Q' a b) = 
   (if B = {} then P' Θ A STOP else b  B. (P' Θ a  A. Q' a b))                
  by (simp add: Process_eq_spec F_Throw D_Throw 
                F_GlobalNdet D_GlobalNdet T_GlobalNdet, safe, simp_all; blast)
     (simp add: Process_eq_spec F_Throw D_Throw 
                 F_GlobalNdet D_GlobalNdet T_GlobalNdet F_STOP D_STOP; blast)


lemma Throw_disjoint_events: A  events_of P = {}  P Θ a  A. Q a = P
proof (subst Process_eq_spec_optimized, safe)
  show A  events_of P = {}  s  𝒟 (Throw P A Q)  s  𝒟 P for s
    by (simp add: D_Throw disjoint_iff events_of_def)
       (meson in_set_conv_decomp is_processT7_S)
next
  show A  events_of P = {}  s  𝒟 P  s  𝒟 (Throw P A Q) for s
    by (simp add: D_Throw disjoint_iff events_of_def image_iff)
       (metis (no_types, lifting) D_T append_Nil2 butlast_snoc front_tickFree_mono
              front_tickFree_butlast process_charn nonTickFree_n_frontTickFree)
next
  show A  events_of P = {}  (s, X)   (Throw P A Q)  (s, X)   P for s X
    by (simp add: F_Throw disjoint_iff events_of_def)
       (meson in_set_conv_decomp process_charn)
next
  show A  events_of P = {}  (s, X)   P  (s, X)   (Throw P A Q) for s X
    by (simp add: F_Throw disjoint_iff events_of_def image_iff) (metis F_T)
qed


lemma events_Throw:
  events_of (P Θ a  A. Q a)  events_of P  (a  (A  events_of P). events_of (Q a))
proof (intro subsetI)
  fix e
  assume e  events_of (P Θ a  A. Q a)
  then obtain s where * : ev e  set s s  𝒯 (P Θ a  A. Q a)
    by (simp add: events_of_def) blast
  from "*"(2) consider s  𝒯 P set s  ev ` A = {}
    | t1 t2. s = t1 @ t2  t1  𝒟 P  tickFree t1 
               set t1  ev ` A = {}  front_tickFree t2
    | t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P 
                 set t1  ev ` A = {}  a  A  t2  𝒯 (Q a)
    by (simp add: T_Throw) blast
  thus e  events_of P  (a  (A  events_of P). events_of (Q a))
  proof cases
    from "*"(1) show s  𝒯 P  set s  ev ` A = {} 
                      e  events_of P  (aA  events_of P. events_of (Q a))
      by (simp add: events_of_def) blast
  next
    show t1 t2. s = t1 @ t2  t1  𝒟 P  tickFree t1 
                  set t1  ev ` A = {}  front_tickFree t2 
          e  events_of P  (a  (A  events_of P). events_of (Q a))
      by (metis UNIV_I UnI1 empty_iff events_div)
  next
    assume t1 a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P 
                      set t1  ev ` A = {}  a  A  t2  𝒯 (Q a)
    then obtain t1 a t2
      where ** : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 P
                 set t1  ev ` A = {} a  A t2  𝒯 (Q a) by blast
    from "*"(1) "**"(1) have ev e  set (t1 @ [ev a])  ev e  set t2 by simp
    thus e  events_of P  (a  (A  events_of P). events_of (Q a))
    proof (elim disjE)
      show ev e  set (t1 @ [ev a]) 
            e  events_of P  (aA  events_of P. events_of (Q a))
        unfolding events_of_def using "**"(2) by blast
    next
      show ev e  set t2  e  events_of P  (aA  events_of P. events_of (Q a))
        unfolding events_of_def using "**"(2, 4, 5) mem_Collect_eq by fastforce
    qed
  qed
qed



subsection ‹Key Property›

lemma Throw_Mprefix: 
  (a  A  P a) Θ b  B. Q b =
    a  A  (if a  B then Q a else P a Θ b  B. Q b)
  (is ?lhs = ?rhs)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume s  𝒟 ?lhs
  then consider t1 t2. s = t1 @ t2  t1  𝒟 (Mprefix A P)  tickFree t1 
                         set t1  ev ` B = {}  front_tickFree t2
  | t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P) 
               set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
    by (simp add: D_Throw) blast
  thus s  𝒟 ?rhs
  proof cases
    assume t1 t2. s = t1 @ t2  t1  𝒟 (Mprefix A P)  tickFree t1 
                    set t1  ev ` B = {}  front_tickFree t2
    then obtain t1 t2
      where * : s = t1 @ t2 t1  𝒟 (Mprefix A P) tickFree t1 
                set t1  ev ` B = {} front_tickFree t2 by blast
    from "*"(2) obtain a t1' where ** : t1 = ev a # t1' a  A t1'  𝒟 (P a)
      by (simp add: D_Mprefix) (metis event.inject image_iff list.collapse)
    from "*"(4) "**"(1) have *** : a  B by (simp add: image_iff)
    have t1' @ t2  𝒟 (Throw (P a) B Q)
      using "*"(3, 4, 5) "**"(1, 3) by (auto simp add: D_Throw)
    with "***" show s  𝒟 ?rhs
      by (simp add: D_Mprefix "*"(1) "**"(1, 2))
  next
    assume t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P) 
                      set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
    then obtain t1 b t2
      where * : s = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (Mprefix A P)
                set t1  ev ` B = {} b  B t2  𝒟 (Q b) by blast
    show s  𝒟 ?rhs
    proof (cases t1)
      from "*"(2) show t1 = []  s  𝒟 ?rhs
        by (simp add: D_Mprefix T_Mprefix "*"(1, 4, 5))
    next
      fix a t1'
      assume t1 = a # t1'
      then obtain a' where t1 = ev a' # t1' (* a = ev a' *)
        by (metis "*"(2) append_single_T_imp_tickFree event.exhaust tickFree_Cons)
      with "*"(2, 3, 4, 5) show s  𝒟 ?rhs
        by (auto simp add: "*"(1) D_Mprefix T_Mprefix D_Throw)
    qed
  qed
next
  fix s
  assume s  𝒟 ?rhs
  then obtain a s' where * : a  A s = ev a # s'
                             s'  𝒟 (if a  B then Q a else Throw (P a) B Q) 
    by (simp add: D_Mprefix) (metis event.inject image_iff list.collapse)
  show s  𝒟 ?lhs
  proof (cases a  B)
    assume a  B
    hence ** :  [] @ [ev a]  𝒯 (Mprefix A P)  set []  ev ` B = {}  s'  𝒟 (Q a)
      using "*"(3) by (simp add: T_Mprefix Nil_elem_T "*"(1))
    show s  𝒟 ?lhs 
      by (simp add: D_Throw) (metis "*"(2) "**" a  B append_Nil)
  next
    assume a  B
    with "*"(2, 3)
    consider t1 t2. s = ev a # t1 @ t2  t1  𝒟 (P a)  tickFree t1 
                      set t1  ev ` B = {}  front_tickFree t2
      | t1 b t2. s = ev a # t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a) 
                   set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
      by (simp add: D_Throw) blast
    thus s  𝒟 ?lhs
    proof cases
      assume t1 t2. s = ev a # t1 @ t2  t1  𝒟 (P a)  tickFree t1 
                      set t1  ev ` B = {}  front_tickFree t2
      then obtain t1 t2
        where ** : s = ev a # t1 @ t2 t1  𝒟 (P a) tickFree t1
                   set t1  ev ` B = {} front_tickFree t2 by blast
      have *** : ev a # t1  𝒟 (Mprefix A P)  tickFree (ev a # t1) 
                  set (ev a # t1)  ev ` B = {}
        by (simp add: D_Mprefix image_iff "*"(1) "**"(2, 3, 4) a  B)
      show s  𝒟 ?lhs
        by (simp add: D_Throw) (metis "**"(1, 5) "***" append_Cons)
    next
      assume t1 b t2. s = ev a # t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a) 
                        set t1  ev ` B = {}  b  B  t2  𝒟 (Q b)
      then obtain t1 b t2
        where ** : s = ev a # t1 @ ev b # t2 t1 @ [ev b]  𝒯 (P a)
                   set t1  ev ` B = {} b  B t2  𝒟 (Q b) by blast
      have *** : (ev a # t1) @ [ev b]  𝒯 (Mprefix A P)  set (ev a # t1)  ev ` B = {}
        by (simp add: T_Mprefix image_iff "*"(1) "**"(2, 3) a  B)
      show s  𝒟 ?lhs
        by (simp add: D_Throw) (metis "**"(1, 4, 5) "***" append_Cons)
    qed
  qed
next
  fix s X
  assume same_div : 𝒟 ?lhs = 𝒟 ?rhs
  assume (s, X)   ?lhs
  then consider (s, X)   (Mprefix A P) set s  ev ` B = {}
      | s  𝒟 ?lhs
      | t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P)  
                   set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
    by (simp add: F_Throw D_Throw) blast
  thus (s, X)   ?rhs
  proof cases
    show (s, X)   (Mprefix A P)  set s  ev ` B = {}  (s, X)   ?rhs
      by (simp add: F_Mprefix F_Throw)
         (metis disjoint_iff hd_in_set imageI list.set_sel(2))
  next
    show s  𝒟 ?lhs  (s, X)   ?rhs
      using same_div D_F by blast
  next
    assume  t1 b t2. s = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (Mprefix A P)  
                       set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
    then obtain t1 b t2
      where * : s = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (Mprefix A P)
                set t1  ev ` B = {} b  B (t2, X)   (Q b) by blast
    show (s, X)   ?rhs
    proof (cases t1) 
      from "*"(2) show t1 = []  (s, X)   ?rhs
        by (auto simp add: F_Mprefix T_Mprefix F_Throw "*"(1, 4, 5))
    next
      fix a t1'
      assume t1 = a # t1'
      then obtain a' where t1 = ev a' # t1' (* a = ev a' *)
        by (metis "*"(2) append_single_T_imp_tickFree event.exhaust tickFree_Cons)
      with "*"(2, 3, 5) show (s, X)   ?rhs
        by (auto simp add: F_Mprefix T_Mprefix F_Throw "*"(1, 4))
    qed
  qed
next
  show (s, X)   ?rhs  (s, X)   ?lhs for s X
  proof (cases s)
    show s = []  (s, X)   ?rhs  (s, X)   ?lhs
      by (simp add: F_Mprefix F_Throw)
  next
    fix a s'
    assume assms : s = a # s' (s, X)   ?rhs
    from assms(2) obtain a'
      where * : a'  A s = ev a' # s'
                (s', X)   (if a'  B then Q a' else Throw (P a') B Q)
      by (simp add: assms(1) F_Mprefix) blast
    show (s, X)   ?lhs
    proof (cases a'  B) 
      assume a'  B
      hence ** : [] @ [ev a']  𝒯 (Mprefix A P) 
                 set []  ev ` B = {}  (s', X)   (Q a')
        using "*"(3) by (simp add: T_Mprefix Nil_elem_T "*"(1))
      show (s, X)   ?lhs
        by (simp add: F_Throw) (metis "*"(2) "**" a'  B append_Nil)
    next
      assume a'  B
      then consider  (s', X)   (P a') set s'  ev ` B = {}
        | t1 t2. s' = t1 @ t2  t1  𝒟 (P a')  tickFree t1 
                      set t1  ev ` B = {}  front_tickFree t2
        | t1 b t2. s' = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a') 
                        set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
        using "*"(3) by (simp add: F_Throw D_Throw) blast
      thus (s, X)   ?lhs
      proof cases
        show (s', X)   (P a')  set s'  ev ` B = {}  (s, X)   ?lhs
          by (simp add: F_Mprefix F_Throw "*"(1, 2) a'  B image_iff)
      next
        assume t1 t2. s' = t1 @ t2  t1  𝒟 (P a')  tickFree t1 
                        set t1  ev ` B = {}  front_tickFree t2
        then obtain t1 t2
          where ** : s' = t1 @ t2 t1  𝒟 (P a') tickFree t1
                     set t1  ev ` B = {} front_tickFree t2 by blast
        have *** : s = (ev a' # t1) @ t2  ev a' # t1  𝒟 (Mprefix A P) 
                    tickFree (ev a' # t1)  set (ev a' # t1)  ev ` B = {}
          by (simp add: D_Mprefix a'  B image_iff "*"(1, 2) "**"(1, 2, 3, 4))
        show (s, X)   ?lhs
          by (simp add: F_Throw F_Mprefix) (metis "**"(5) "***")
      next
        assume t1 b t2. s' = t1 @ ev b # t2  t1 @ [ev b]  𝒯 (P a') 
                          set t1  ev ` B = {}  b  B  (t2, X)   (Q b)
        then obtain t1 b t2
          where ** : s' = t1 @ ev b # t2 t1 @ [ev b]  𝒯 (P a')
                     set t1  ev ` B = {} b  B (t2, X)   (Q b) by blast
        have *** : s = (ev a' # t1) @ ev b # t2  set (ev a' # t1)  ev ` B = {} 
                    (ev a' # t1) @ [ev b]  𝒯 (Mprefix A P)
          by (simp add: T_Mprefix a'  B image_iff "*"(1, 2) "**"(1, 2, 3))
        show (s, X)   ?lhs
          by (simp add: F_Throw F_Mprefix) (metis "**"(4, 5) "***")
      qed
    qed
  qed
qed


corollary Throw_prefix: (a  P) Θ b  B. Q b =
                         (a  (if a  B then Q a else (P Θ b  B. Q b)))
  unfolding write0_def by (auto simp add: Throw_Mprefix intro: mono_Mprefix_eq)

corollary Throw_Mndetprefix:
  (a  A  P a) Θ b  B. Q b =
   a  A  (if a  B then Q a else P a Θ b  B. Q b)
  apply (subst Mndetprefix_GlobalNdet)
  apply (simp add: Throw_GlobalNdet(1) Throw_prefix)
  apply (subst Mndetprefix_GlobalNdet[symmetric])
  by simp


― ‹We may prove some results about deadlock freeness as corollaries›
   
  


subsection ‹Continuity›

lemma chain_left_Throw: chain Y  chain (λi. Y i Θ a  A. Q a)
  by (simp add: chain_def)

lemma chain_right_Throw: chain Y  chain (λi. P Θ a  A. Y i a)
  by (simp add: chain_def fun_belowD)


lemma cont_left_prem_Throw :
  ( i. Y i) Θ a  A. Q a = ( i. Y i Θ a  A. Q a)
  (is ?lhs = ?rhs) if chain : chain Y
proof (subst Process_eq_spec, safe)
 show s  𝒟 ?lhs  s  𝒟 ?rhs for s
   by (auto simp add: limproc_is_thelub chain
                      chain_left_Throw D_Throw T_LUB D_LUB)
next
  fix s
  define S
    where S i  {t1. t2. s = t1 @ t2  t1  𝒟 (Y i)  tickFree t1 
                           set t1  ev ` A = {}  front_tickFree t2} 
                 {t1. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 (Y i)  tickFree t1 
                             set t1  ev ` A = {}  a  A  t2  𝒟 (Q a)} for i
  assume s  𝒟 ?rhs
  hence ftF: front_tickFree s using D_imp_front_tickFree by blast
  from s  𝒟 ?rhs have s  𝒟 (Y i Θ a  A. Q a) for i
    by (simp add: limproc_is_thelub D_LUB chain_left_Throw chain)
  hence i. S i  {}
    by (simp add: S_def D_Throw)
       (metis ftF front_tickFree_mono list.distinct(1))
  moreover have finite (S 0)
    unfolding S_def
    apply (rule finite_subset[of _ {t1. t2. s = t1 @ t2}], blast)
    by (metis prefixes_fin)
  moreover have i. S (Suc i)  S i
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    by (metis in_mono le_approx1 po_class.chainE chain)
       (metis le_approx_lemma_T po_class.chain_def subset_eq chain)
  ultimately have (i. S i)  {}
    by (rule Inter_nonempty_finite_chained_sets)
  then obtain t1 where * : i. t1  S i
    by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
  show s  𝒟 ?lhs
  proof (cases j a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 (Y j)  a  A  t2  𝒟 (Q a))
    case True
    then obtain j a t2 where ** : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 (Y j)
                                  a  A t2  𝒟 (Q a) by blast
    from "*" "**"(1) have i. t1 @ [ev a]  𝒯 (Y i)
      by (simp add: S_def) (meson D_T front_tickFree_single is_processT7_S)
    with "*" "**"(1, 3, 4) show s  𝒟 ?lhs
      by (simp add: S_def D_Throw limproc_is_thelub chain T_LUB) blast
  next
    case False
    with "*" have i. t2. s = t1 @ t2  t1  𝒟 (Y i)  front_tickFree t2
      by (simp add: S_def) blast
    hence t2. s = t1 @ t2  (i. t1  𝒟 (Y i))  front_tickFree t2 by blast
    with "*" show s  𝒟 ?lhs
      by (simp add: S_def D_Throw limproc_is_thelub chain D_LUB) blast
  qed
next
  show (s, X)   ?lhs  (s, X)   ?rhs for s X
    by (auto simp add: limproc_is_thelub chain chain_left_Throw 
                       F_Throw F_LUB T_LUB D_LUB)
next
  fix s X
  define S
    where S i  {t1. s = t1  (t1, X)   (Y i)  set t1  ev ` A = {}} 
                 {t1. t2. s = t1 @ t2  t1  𝒟 (Y i)  tickFree t1 
                           set t1  ev ` A = {}  front_tickFree t2} 
                 {t1. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 (Y i) 
                             set t1  ev ` A = {}  a  A  (t2, X)   (Q a)} for i
  assume (s, X)   ?rhs
  hence ftF: front_tickFree s using is_processT2 by blast
  from (s, X)   ?rhs have (s, X)   (Y i Θ a  A. Q a) for i
    by (simp add: limproc_is_thelub F_LUB chain_left_Throw chain)

  hence i. S i  {} by (simp add: S_def F_Throw, safe; simp, blast)
  moreover have finite (S 0)
    unfolding S_def
    apply (intro finite_UnI)
    apply (all rule finite_subset[of _ {t1. t2. s = t1 @ t2}], blast)
    by (metis prefixes_fin)+
  moreover have i. S (Suc i)  S i
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    subgoal by (meson is_processT8 po_class.chainE proc_ord2a chain)
    subgoal by (metis in_mono le_approx1 po_class.chainE chain)
    by (metis le_approx_lemma_T po_class.chain_def subset_eq chain)
  ultimately have (i. S i)  {}
    by (rule Inter_nonempty_finite_chained_sets)
  then obtain t1 where * : i. t1  S i 
    by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
  show (s, X)   ?lhs
  proof (cases j a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 (Y j) 
                         a  A  (t2, X)   (Q a))
    case True1 : True
    then obtain j a t2 where ** : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 (Y j)
                                  a  A (t2, X)   (Q a) by blast
    from "*" "**"(1) have i. t1 @ [ev a]  𝒯 (Y i)
      by (simp add: S_def) (meson D_T front_tickFree_single is_processT7)
    with "*" "**"(1, 3, 4) show (s, X)   ?lhs
      by (simp add: S_def F_Throw limproc_is_thelub chain T_LUB) blast
  next
    case False1 : False
    show (s, X)   ?lhs
    proof (cases i. t1  𝒟 (Y i))
      case True2 : True
      with "*" show (s, X)   ?lhs
        by (simp add: S_def F_Throw limproc_is_thelub chain)
           (metis D_LUB_2 append_Nil2 front_tickFree_mono ftF process_charn chain)
    next
      case False2 : False
      then obtain j where t1  𝒟 (Y j) by blast
      with False1 "*" have ** : s = t1  (t1, X)   (Y j)  set t1  ev ` A = {}
        by (simp add: S_def) blast
      with "*" D_F have i. (t1, X)   (Y i) by (auto simp add: S_def) 
      with "**" show (s, X)   ?lhs
        by (simp add: F_Throw limproc_is_thelub F_LUB chain)
    qed
  qed
qed
 

lemma cont_right_prem_Throw : 
  P Θ a  A. ( i. Y i a) = ( i. P Θ a  A. Y i a)
  (is ?lhs = ?rhs) if chain : chain Y
proof (subst Process_eq_spec, safe)
  show s  𝒟 ?lhs  s  𝒟 ?rhs for s
    by (simp add: limproc_is_thelub chain chain_right_Throw 
                       ch2ch_fun[OF chain] D_Throw D_LUB) blast
next
  fix s
  assume s  𝒟 ?rhs
  define S
    where S i  {t1. t2. s = t1 @ t2  t1  𝒟 P  tickFree t1 
                           set t1  ev ` A = {}  front_tickFree t2} 
                 {t1. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P 
                             set t1  ev ` A = {}  a  A  t2  𝒟 (Y i a)} for i
  assume s  𝒟 ?rhs
  hence s  𝒟 (P Θ a  A. Y i a) for i
    by (simp add: limproc_is_thelub D_LUB chain_right_Throw chain)
  hence i. S i  {} by (simp add: S_def D_Throw) metis
  moreover have finite (S 0)
    unfolding S_def
    apply (rule finite_subset[of _ {t1. t2. s = t1 @ t2}], blast)
    by (metis prefixes_fin)
  moreover have i. S (Suc i)  S i
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    by (metis fun_belowD le_approx1 po_class.chainE subset_iff chain)
  ultimately have (i. S i)  {}
    by (rule Inter_nonempty_finite_chained_sets)
  then obtain t1 where i. t1  S i 
    by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
  then consider t1  𝒟 P tickFree t1
                set t1  ev ` A = {} t2. s = t1 @ t2  front_tickFree t2
    | set t1  ev ` A = {}
      i. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  a  A  t2  𝒟 (Y i a)
    by (simp add: S_def) blast
  thus s  𝒟 ?lhs
  proof cases
    show t1  𝒟 P  tickFree t1  set t1  ev ` A = {} 
          t2. s = t1 @ t2  front_tickFree t2  s  𝒟 ?lhs
      by (simp add: D_Throw) blast
  next
    assume assms: set t1  ev ` A = {}
                  i. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  
                              a  A  t2  𝒟 (Y i a)
    from assms(2) obtain a t2
      where * : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 P a  A by blast
    with assms(2) have i. t2  𝒟 (Y i a) by blast
    with assms(1) "*"(1, 2, 3) show s  𝒟 ?lhs
      by (simp add: D_Throw limproc_is_thelub chain ch2ch_fun D_LUB) blast
  qed
next
  show (s, X)   ?lhs  (s, X)   ?rhs for s X
    by (simp add: limproc_is_thelub chain chain_right_Throw
                  ch2ch_fun[OF chain] F_Throw F_LUB T_LUB D_LUB) blast
next
  fix s X
  define S
    where S i  {t1. s = t1  (t1, X)   P  set t1  ev ` A = {}} 
                 {t1. t2. s = t1 @ t2  t1  𝒟 P  tickFree t1 
                           set t1  ev ` A = {}  front_tickFree t2} 
                 {t1. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P 
                             set t1  ev ` A = {}  a  A  (t2, X)   (Y i a)} for i
  assume (s, X)   ?rhs
  hence (s, X)   (P Θ a  A. Y i a) for i
    by (simp add: limproc_is_thelub F_LUB chain_right_Throw chain)
  hence i. S i  {} by (simp add: S_def F_Throw, safe; simp, blast)
  moreover have finite (S 0)
    unfolding S_def
    apply (intro finite_UnI)
    apply (all rule finite_subset[of _ {t1. t2. s = t1 @ t2}], blast)
    by (metis prefixes_fin)+
  moreover have i. S (Suc i)  S i
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    by (metis NF_ND fun_below_iff po_class.chain_def proc_ord2a chain)
  ultimately have (i. S i)  {}
    by (rule Inter_nonempty_finite_chained_sets)
  then obtain t1 where i. t1  S i
    by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
  then consider s = t1  (t1, X)   P set t1  ev ` A = {}
    | t2. s = t1 @ t2  t1  𝒟 P  tickFree t1  
            set t1  ev ` A = {}  front_tickFree t2
    | set t1  ev ` A = {} 
      i. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P  a  A  (t2, X)   (Y i a)
    by (simp add: S_def) blast
  thus (s, X)   ?lhs
  proof cases
    show s = t1  (t1, X)   P  set t1  ev ` A = {}  (s, X)   ?lhs
      by (simp add: F_Throw)
  next
    show t2. s = t1 @ t2  t1  𝒟 P  tickFree t1  
               set t1  ev ` A = {}  front_tickFree t2  (s, X)   ?lhs
      by (simp add: F_Throw) blast
  next
    assume assms: set t1  ev ` A = {}
                  i. a t2. s = t1 @ ev a # t2  t1 @ [ev a]  𝒯 P 
                              a  A  (t2, X)   (Y i a)
    from this(2) obtain a t2
      where * : s = t1 @ ev a # t2 t1 @ [ev a]  𝒯 P a  A by blast
    with assms(2) have i. (t2, X)   (Y i a) by blast
    with "*"(1, 2, 3) assms(1) show (s, X)   ?lhs
      by (simp add: F_Throw limproc_is_thelub ch2ch_fun chain F_LUB) blast
  qed
qed


lemma Throw_cont[simp] : 
  assumes cont_f : cont f and cont_g : a. cont (g a)
  shows cont (λx. f x Θ a  A. g a x)
proof -
  have * : cont (λy. y Θ a  A. g a x) for x
    by (rule contI2, rule monofunI, solves simp, simp add: cont_left_prem_Throw)
  have cont (Throw y A) for y
    by (simp add: contI2 cont_right_prem_Throw fun_belowD lub_fun monofunI)
  hence ** : cont (λx. y Θ a  A. g a x) for y
    by (rule cont_compose) (simp add: cont_g)
  show ?thesis by (fact cont_apply[OF cont_f "*" "**"])
qed

end