Theory Throw

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

section‹ The Throw Operator ›

(*<*)
theory  Throw
  imports "HOL-CSP.CSP"
begin
  (*>*)


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 :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set, 'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  is ‹λ P A Q. 
  ({(t1, X). (t1, X) ∈ ℱ P ∧ set t1 ∩ ev ` A = {}} ∪
   {(t1 @ t2, X) |t1 t2 X. t1 ∈ 𝒟 P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF 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 ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF 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 ⟹ ftF s› for s X
      apply (simp, elim disjE exE)
        apply (metis is_processT)
       apply (simp add: front_tickFree_append)
      by (metis F_imp_front_tickFree T_nonTickFree_imp_decomp append1_eq_conv event⇩p⇩t⇩i⇩c⇩k.distinct(1)
          front_tickFree_Cons_iff front_tickFree_append tickFree_Cons_iff tickFree_append_iff)
  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 where ‹s @ t @ [b] = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
        | t1 a t2 where ‹s @ t @ [b] = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
          ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, {}) ∈ ℱ (Q a)›
        using snoc.prems by auto
      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
        show ‹⟦s @ t @ [b] = t1 @ t2; t1 ∈ 𝒟 P; tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧
              ⟹ (s, {}) ∈ ?f› for t1 t2
          by (rule snoc.hyps, cases t2 rule: rev_cases, simp_all)
            (metis (no_types, opaque_lifting) Int_Un_distrib2 append_assoc is_processT3
              is_processT8 set_append sup.idem sup_bot.right_neutral,
              metis front_tickFree_dw_closed)
      next
        show ‹⟦s @ t @ [b] = t1 @ ev a # t2; t1 @ [ev a] ∈ 𝒯 P; set t1 ∩ ev ` A = {};
               a ∈ A; (t2, {}) ∈ ℱ (Q a)⟧ ⟹ (s, {}) ∈ ?f› for t1 a t2
          by (rule snoc.hyps, cases t2 rule: rev_cases, simp_all)
            (metis T_F is_processT3, metis is_processT3)
      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   where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | t1 a t2 where ‹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
      show ‹⟦s = t1 @ t2; t1 ∈ 𝒟 P; tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧
            ⟹ (s, X ∪ Y) ∈ ?f› for t1 t2 by blast
    next
      fix t1 a t2
      assume * : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P› 
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q a)›
      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 r. s @ [✓(r)] = t1 @ ev a # t2 ⟹ ∃t2'. t2 = t2' @ [✓(r)]›
      by (simp add: snoc_eq_iff_butlast split: if_split_asm)
        (metis append_butlast_last_id)
    show ‹(s @ [✓(r)], {}) ∈ ?f ⟹ (s, X - {✓(r)}) ∈ ?f› for s r X
      apply (simp, elim disjE exE conjE)
        apply (solves ‹simp add: is_processT6›)
       apply (metis append1_eq_conv append_assoc front_tickFree_dw_closed
          nonTickFree_n_frontTickFree non_tickFree_tick tickFree_append_iff)
      by (frule "*", elim exE, simp, metis is_processT6)
  next
    show ‹⟦s ∈ ?d; tF s; ftF t⟧ ⟹ s @ t ∈ ?d› for s t
      by (simp, elim disjE) 
        (meson append_assoc front_tickFree_append tickFree_append_iff,
          use append_self_conv2 is_processT7 tickFree_append_iff in fastforce)
  next
    show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X
      by simp (metis is_processT8)     
  next
    show ‹s @ [✓(r)] ∈ ?d ⟹ s ∈ ?d› for s r
      by (simp, elim disjE)
        (metis butlast_append butlast_snoc front_tickFree_iff_tickFree_butlast
          non_tickFree_tick tickFree_Nil tickFree_append_iff tickFree_imp_front_tickFree,
          metis (no_types, lifting) append_butlast_last_id butlast.simps(2) butlast_append
          butlast_snoc event⇩p⇩t⇩i⇩c⇩k.distinct(1) is_processT9 last.simps last_appendR list.distinct(1))
  qed
qed


text ‹We add some syntactic sugar.›

syntax "_Throw" :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, pttrn, 'a set, 'a ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹((_) Θ (_∈_)./ (_))› [78,78,78,77] 77)
syntax_consts "_Throw" ⇌ Throw
translations "P Θ a ∈ A. Q" ⇌ "CONST Throw P A (λa. Q)"

(* abbreviation Throw_without_free_var ::
  ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (‹((_) Θ (_)/ (_))› [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). (t1, X) ∈ ℱ P ∧ set t1 ∩ ev ` A = {}} ∪
   {(t1 @ t2, X) |t1 t2 X. t1 ∈ 𝒟 P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF 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.rep_eq FAILURES_def Throw.rep_eq)


lemma D_Throw:
  ‹𝒟 (P Θ a ∈ A. Q a) =
   {t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF 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.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 ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF 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+

lemmas Throw_projs = F_Throw D_Throw T_Throw


lemma Throw_T_third_clause_breaker :
  ‹⟦set t ∩ S = {}; set t' ∩ S = {}; e ∈ S; e' ∈ S⟧ ⟹
   t @ e # u = t' @ e' # u' ⟷ t = t' ∧ e = e' ∧ u = u'›
proof (induct t arbitrary: t')
  case Nil thus ?case
    by (metis append_Nil disjoint_iff hd_append2 list.sel(1, 3) list.set_sel(1))
next
  case (Cons a t)
  show ?case
  proof (rule iffI)
    assume ‹(a # t) @ e # u = t' @ e' # u'›
    then obtain t'' where ‹t' = a # t''›
      by (metis Cons.prems(1, 4) append_Cons append_Nil disjoint_iff
          list.exhaust_sel list.sel(1) list.set_intros(1))
    with Cons.hyps Cons.prems ‹(a # t) @ e # u = t' @ e' # u'›
    show ‹a # t = t' ∧ e = e' ∧ u = u'› by auto
  next
    show ‹a # t = t' ∧ e = e' ∧ u = u' ⟹ (a # t) @ e # u = t' @ e' # u'› by simp
  qed
qed



subsection ‹Monotony›

(* TODO: move this and use it somewhere else ? *)
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 ∈ A ⟹ a ∈ α(P) ⟹ Q a ⊑ Q' a›
proof (unfold le_approx_def Refusals_after_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 events_of_memI in_set_conv_decomp)
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   where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
    | t1 a t2 where ‹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 ‹tF s›, auto simp add: disjoint_iff)
      by (metis "*"(1) D_imp_front_tickFree F_T T_nonTickFree_imp_decomp butlast_snoc
          front_tickFree_append_iff in_set_butlastD is_processT9 list.distinct(1))
    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
    from assms(1) show ‹⟦s = t1 @ t2; t1 ∈ 𝒟 P; tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧
                        ⟹ (s, X) ∈ ℱ (Throw P' A Q')› for t1 t2
      by (simp add: F_Throw D_Throw)
  next
    fix t1 a t2 assume * : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P› 
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q a)›
    from "*"(2) have ** : ‹tF t1› by (simp add: append_T_imp_tickFree)
    have *** : ‹(t2, X) ∈ ℱ (Q' a)›
      using assms(1)[simplified D_Throw, simplified, THEN conjunct2, rule_format, OF "*"(4, 3, 2, 1)]
      by (metis "*"(2, 4, 5) events_of_memI last_in_set le_approx2 snoc_eq_iff_butlast that(2))
    have **** : ‹t1 ∉ 𝒟 P›
      apply (rule ccontr, simp, 
          drule assms(1)[simplified D_Throw, simplified, THEN conjunct1, rule_format,
            OF "*"(3) "**", of ‹ev a # t2›, simplified "*"(1), simplified])
      by (metis "*"(1) F_imp_front_tickFree assms(2) front_tickFree_append_iff list.discI)
    show ‹(s, X) ∈ ℱ (Throw P' A Q')›
      by (simp add: F_Throw D_Throw "*"(1))
        (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
    by (simp add: F_Throw D_Throw subset_eq, safe, simp_all)
      (metis is_processT8, (metis D_T events_of_memI in_set_conv_decomp)+)
next
  define S_left 
    where ‹S_left ≡ {t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tF t1 ∧ 
                     set t1 ∩ ev ` A = {} ∧ ftF 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 less_list_def less_eq_list_def prefix_def
    apply (simp, safe)
        apply (solves ‹meson is_processT7›)
       apply (metis (no_types, lifting) append.right_neutral front_tickFree_Nil front_tickFree_append
        front_tickFree_nonempty_append_imp inf_bot_right inf_sup_absorb inf_sup_aci(2) set_append)
      apply (metis Int_iff Un_iff append.right_neutral front_tickFree_Nil image_eqI set_append)
     apply (metis D_T prefixI same_prefix_nil T_nonTickFree_imp_decomp append.right_neutral front_tickFree_Nil is_processT9 list.distinct(1)) 
    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
      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›
        apply (simp add: S_left_def)
        by (metis D_imp_front_tickFree T_nonTickFree_imp_decomp append1_eq_conv assms(1)
            assms(2, 4) event⇩p⇩t⇩i⇩c⇩k.distinct(1) front_tickFree_Cons_iff tickFree_Cons_iff tickFree_append_iff)
      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 fast

  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 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›
    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
    fix t1 a t2
    assume ***** : ‹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›
    have ‹t1 @ [ev a] ∈ 𝒯 P' ∧ t2 ∈ 𝒯 (Q' a)›
      by (meson "*****"(3-5) D_T events_of_memI in_set_conv_decomp le_approx2T le_approx_def subsetD that)
    with "*****" show ‹s ∈ 𝒯 (Throw P' A Q')›
      by (simp add: T_Throw) blast
  qed
qed


lemma mono_Throw_eq :
  ‹(⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ Q a = Q' a) ⟹
   P Θ a ∈ A. Q a = P Θ a ∈ A. Q' a›
  by (subst Process_eq_spec) (auto simp add: Throw_projs events_of_memI)



subsection ‹Properties›

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

lemma Throw_is_STOP_iff : ‹P Θ a ∈ A. Q a = STOP ⟷ P = STOP›
proof (rule iffI)
  show ‹P = STOP› if ‹P Θ a ∈ A. Q a = STOP›
  proof (rule ccontr)
    assume ‹P ≠ STOP›
    then obtain t where ‹t ≠ []› ‹t ∈ 𝒯 P› by (auto simp add: STOP_iff_T)
    hence ‹[hd t] ∈ 𝒯 P›
      by (metis append_Cons append_Nil is_processT3_TR_append list.sel(1) neq_Nil_conv)
    hence ‹[hd t] ∈ 𝒯 (P Θ a ∈ A. Q a)› by (auto simp add: T_Throw Cons_eq_append_conv)
    with ‹P Θ a ∈ A. Q a = STOP› show False by (simp add: STOP_iff_T)
  qed
next
  show ‹P = STOP ⟹ P Θ a ∈ A. Q a = STOP› by simp
qed

lemma Throw_SKIP [simp] : ‹SKIP r Θ a ∈ A. Q a = SKIP r›
  by (auto simp add: Process_eq_spec F_Throw F_SKIP D_Throw D_SKIP T_SKIP)

lemma Throw_BOT [simp] : ‹⊥ Θ a ∈ A. Q a = ⊥›
  by (simp add: BOT_iff_Nil_D D_Throw D_BOT)

lemma Throw_is_BOT_iff: ‹P Θ a ∈ A. Q a = ⊥ ⟷ P = ⊥›
  by (simp add: BOT_iff_Nil_D D_Throw) 


lemma Throw_empty_set [simp] : ‹P Θ a ∈ {}. Q a = P›
  by (auto simp add: Process_eq_spec F_Throw D_Throw intro: is_processT7 is_processT8)
    (metis append.right_neutral front_tickFree_nonempty_append_imp
      nonTickFree_n_frontTickFree process_charn snoc_eq_iff_butlast)



lemma Throw_is_restrictable_on_events_of :
  ‹P Θ a ∈ A. Q a = P Θ a ∈ (A ∩ α(P)). Q a› (is ‹?lhs = ?rhs›)
  ―‹A stronger version where \<^term>‹α(P)› is replaced by
    \<^term>‹❙α(P) ∪ {a. ∃t. t @ [ev a] ∈ min_elems (𝒟 P)}› is probably true.›
proof (cases ‹𝒟 P = {}›)
  show ‹?lhs = ?rhs› if ‹𝒟 P = {}›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?lhs›
    with ‹𝒟 P = {}› obtain t1 a t2
      where * : ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a)›
      unfolding D_Throw by blast
    from "*"(3) have ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› by blast
    moreover from "*"(2, 4) have ‹a ∈ A ∩ α(P)› by (simp add: events_of_memI)
    ultimately show ‹t ∈ 𝒟 ?rhs› using "*"(1, 2, 5) by (auto simp add: D_Throw)
  next
    fix t assume ‹t ∈ 𝒟 ?rhs›
    with ‹𝒟 P = {}› obtain t1 a t2
      where * : ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› ‹a ∈ A ∩ α(P)› ‹t2 ∈ 𝒟 (Q a)›
      unfolding D_Throw by blast
    from "*"(2, 3) events_of_memI have ‹set t1 ∩ ev ` A = {}› by fastforce
    with "*"(1, 2, 4, 5) show ‹t ∈ 𝒟 ?lhs› by (auto simp add: D_Throw)
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs›
    with ‹𝒟 P = {}› consider ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
      | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q a)›
      unfolding F_Throw by blast
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      show ‹(t, X) ∈ ℱ P ⟹ set t ∩ ev ` A = {} ⟹ (t, X) ∈ ℱ ?rhs›
        by (simp add: F_Throw disjoint_iff image_iff)
    next
      case failR
      from failR(3) have ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› by blast
      moreover from failR(2, 4) have ‹a ∈ A ∩ α(P)› by (simp add: events_of_memI)
      ultimately show ‹(t, X) ∈ ℱ ?rhs› using failR(1, 2, 5) by (auto simp add: F_Throw)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs›
    with ‹𝒟 P = {}› consider ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` (A ∩ α(P)) = {}›
      | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› ‹a ∈ A›
        ‹a ∈ α(P)› ‹(t2, X) ∈ ℱ (Q a)›
      unfolding F_Throw by blast
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` (A ∩ α(P)) = {}›
      from ‹(t, X) ∈ ℱ P› have ‹t ∈ 𝒯 P› by (simp add: F_T)
      with ‹set t ∩ ev ` (A ∩ α(P)) = {}› events_of_memI
      have ‹set t ∩ ev ` A = {}› by fast
      with ‹(t, X) ∈ ℱ P› show ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_Throw)
    next
      case failR
      from failR(2, 3) events_of_memI have ‹set t1 ∩ ev ` A = {}› by fastforce
      with failR(1, 2, 4-6) show ‹(t, X) ∈ ℱ ?lhs› by (auto simp add: F_Throw)
    qed
  qed
next
  assume ‹𝒟 P ≠ {}›
  hence ‹α(P) = UNIV› by (simp add: events_of_is_strict_events_of_or_UNIV)
  thus ‹?lhs = ?rhs› by simp
qed


lemma Throw_disjoint_events_of: ‹A ∩ α(P) = {} ⟹ P Θ a ∈ A. Q a = P›
  by (metis Throw_empty_set Throw_is_restrictable_on_events_of)



subsection ‹Continuity›

context begin

private lemma chain_Throw_left  : ‹chain Y ⟹ chain (λi. Y i Θ a ∈ A. Q a)›
  by (simp add: chain_def)

private lemma chain_Throw_right : ‹chain Y ⟹ chain (λi. P Θ a ∈ A. Y i a)›
  by (simp add: chain_def fun_belowD)


private lemma cont_left_prem_Throw :
  ‹(⨆ i. Y i) Θ a ∈ A. Q a = (⨆ i. Y i Θ a ∈ A. Q a)›
  (is ‹?lhs = ?rhs›) if ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: limproc_is_thelub ‹chain Y› chain_Throw_left 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_Throw_left ‹chain Y›)
  hence ‹S i ≠ {}› for i by (simp add: S_def D_Throw)
      (metis append_T_imp_tickFree not_Cons_self2)
  moreover have ‹finite (S 0)›
    unfolding S_def by (prove_finite_subset_of_prefixes s)
  moreover have ‹S (Suc i) ⊆ S i› for i
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    by (metis in_mono le_approx1 po_class.chainE ‹chain Y›)
      (metis le_approx_lemma_T po_class.chain_def subset_eq ‹chain Y›)
  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)
    with "*" "**"(1, 3, 4) show ‹s ∈ 𝒟 ?lhs›
      by (simp add: S_def D_Throw limproc_is_thelub ‹chain Y› 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 Y› D_LUB) blast
  qed
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (auto simp add: limproc_is_thelub ‹chain Y› chain_Throw_left F_Throw F_LUB T_LUB D_LUB)
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  fix s X assume ‹(s, X) ∈ ℱ ?rhs›
  show ‹(s, X) ∈ ℱ ?lhs›
  proof (cases ‹s ∈ 𝒟 ?rhs›)
    show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ 𝒟 ?rhs›
    have ‹∀a∈A. Q a ⊑ Q a› by simp
    moreover from ‹s ∉ 𝒟 ?rhs› obtain j where ‹s ∉ 𝒟 (Y j Θ a ∈ A. Q a)›
      by (auto simp add: limproc_is_thelub chain_Throw_left ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ ℱ ?rhs› have ‹(s, X) ∈ ℱ (Y j Θ a ∈ A. Q a)›
      by (simp add: limproc_is_thelub chain_Throw_left ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ ℱ ?lhs›
      by (meson is_ub_thelub le_approx2 mono_Throw ‹chain Y›)
  qed
qed



private lemma cont_right_prem_Throw : 
  ‹P Θ a ∈ A. (⨆ i. Y i a) = (⨆ i. P Θ a ∈ A. Y i a)›
  (is ‹?lhs = ?rhs›) if ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (simp add: limproc_is_thelub ‹chain Y› chain_Throw_right ch2ch_fun[OF ‹chain Y›] D_Throw D_LUB) blast
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  define S
    where ‹S i ≡ {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒟 P ∧ tF t1 ∧
                           set t1 ∩ ev ` A = {} ∧ ftF 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_Throw_right ‹chain Y›)
  hence ‹S i ≠ {}› for i by (simp add: S_def D_Throw) metis
  moreover have ‹finite (S 0)›
    unfolding S_def by (prove_finite_subset_of_prefixes s)
  moreover have ‹S (Suc i) ⊆ S i› for i
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    by (metis fun_belowD le_approx1 po_class.chainE subset_iff ‹chain Y›)
  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› ‹tF t1›
    ‹set t1 ∩ ev ` A = {}› ‹∃t2. s = t1 @ t2 ∧ ftF 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 Y› ch2ch_fun D_LUB) blast
  qed
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (simp add: limproc_is_thelub ‹chain Y› chain_Throw_right ch2ch_fun[OF ‹chain Y›] F_Throw F_LUB T_LUB D_LUB) blast
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  fix s X assume ‹(s, X) ∈ ℱ ?rhs›
  show ‹(s, X) ∈ ℱ ?lhs›
  proof (cases ‹s ∈ 𝒟 ?rhs›)
    show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ 𝒟 ?rhs›
    have ‹∀a∈A. Y i a ⊑ (⨆i. Y i a)› for i by (metis ch2ch_fun is_ub_thelub ‹chain Y›)
    moreover from ‹s ∉ 𝒟 ?rhs› obtain j where ‹s ∉ 𝒟 (P Θ a ∈ A. Y j a)›
      by (auto simp add: limproc_is_thelub chain_Throw_right ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ ℱ ?rhs› have ‹(s, X) ∈ ℱ (P Θ a ∈ A. Y j a)›
      by (simp add: limproc_is_thelub chain_Throw_right ‹chain Y› F_LUB)
    find_theorems ‹chain (λa. ?P)›
    ultimately show ‹(s, X) ∈ ℱ ?lhs›
      by (metis (mono_tags, lifting) below_refl le_approx2 mono_Throw)
  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 ‹⋀y. cont (Throw y A)›
    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

(*<*)
end
  (*>*)