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


(*<*)
hide_const R
text ‹We need to hide this because we want to be allowed to use the letter R in our lemmas.
      We can still access this notion via the notation \<^term>‹ℛ P›.
      In further versions of \<^theory>‹HOL-CSP.Process›, R will be renamed in Refusals 
      and we will remove this paragraph.›

―‹This result should be in \<^session>‹HOL-CSP›.›
lemma Refusals_iff : ‹X ∈ ℛ P ⟷ ([], X) ∈ ℱ P›
  by (simp add: Failures_def R_def REFUSALS_def)
(*>*)


subsection ‹Definition›

text ‹The Throw operator allows error handling. Whenever an error (or more generally any 
      event \<^term>‹ev e ∈ ev ` A›) occurs in \<^term>‹P›, \<^term>‹P› is shut down and \<^term>‹Q e› is started.

      This operator can somehow be seen as a generalization of sequential composition \<^const>‹Seq›:
      \<^term>‹P› terminates on any event in \<^term>‹ev ` A› rather than \<^const>‹tick›
      (however it do not hide these events like \<^const>‹Seq› do for \<^const>‹tick›,
      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 \<^term>‹Q› to be parameterized we can just write \<^term>‹P Θ 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_def TRACES_def Failures_def[symmetric] F_Throw) blast+
  (* 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 ⊑⇩F⇩D P' ⟹ ∀a ∈ A. Q a ⊑⇩F⇩D Q' a ⟹
                       P Θ a ∈ A. Q a ⊑⇩F⇩D 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 ⊑⇩D⇩T P' ⟹ ∀a ∈ A. Q a ⊑⇩D⇩T Q' a ⟹
                       P Θ a ∈ A. Q a ⊑⇩D⇩T 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 ∪ (⋃a∈A ∩ 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 ∪ (⋃a∈A ∩ 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 ∪ (⋃a∈A ∩ 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