(*<*)
―‹ ********************************************************************
 * 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"
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_ptick, 'a set, 'a → ('a, 'r) process_ptick] → ('a, 'r) process_ptick›
  is ‹λ P A Q.
 ({(t1, X). (t1, X) ∈ F P ∧ set t1 ∩ ev ` A = {}} ∪
 {(t1 @ t2, X) |t1 t2 X. t1 ∈ D P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF t2} ∪
 {(t1 @ ev a # t2, X) |t1 a t2 X.
 t1 @ [ev a] ∈ T P ∧ set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ (t2, X) ∈ F (Q a)},
 {t1 @ t2 |t1 t2. t1 ∈ D P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF t2} ∪
 {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a] ∈ T P ∧ set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ D (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<sub>ptick</sub>.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], {}) ∈ F P› ‹(set s ∪ set t) ∩ ev ` A = {}›
        | t1 t2 where ‹s @ t @ [b] = t1 @ t2› ‹t1 ∈ D P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
        | t1 a t2 where ‹s @ t @ [b] = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P›
          ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, {}) ∈ F (Q a)›
        using snoc.prems by auto
      thus ‹(s, {}) ∈ ?f›
      proof cases
        show ‹(s @ t @ [b], {}) ∈ F 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 ∈ D 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] ∈ T P; set t1 ∩ ev ` A = {};
 a ∈ A; (t2, {}) ∈ F (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) ∈ F P› ‹set s ∩ ev ` A = {}›
      | t1 t2   where ‹s = t1 @ t2› ‹t1 ∈ D P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
      | t1 a t2 where ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P› ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ F (Q a)›
      using assms(1) by blast
    thus ‹(s, X ∪ Y) ∈ ?f›
    proof cases
      assume * : ‹(s, X) ∈ F P› ‹set s ∩ ev ` A = {}›
      have ‹(s @ [c], {}) ∉ F 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], {}) ∉ F P›
          by auto (metis F_T is_processT1)
      next
        from "*"(2) assms(2)[rule_format, OF that]
        show ‹c ∉ ev ` A ==> (s @ [c], {}) ∉ F P› by simp
      qed
      with "*"(1) is_processT5 have ‹(s, X ∪ Y) ∈ F P› by blast
      with "*"(2) show ‹(s, X ∪ Y) ∈ ?f› by blast
    next
      show ‹[s = t1 @ t2; t1 ∈ D 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] ∈ T P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ F (Q a)›
      have ‹(t2 @ [c], {}) ∉ F (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) ∈ F (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_ptick.distinct(1) is_processT9 last.simps last_appendR list.distinct(1))
  qed
qed


text ‹We add some syntactic sugar.›

syntax "_Throw" :: ‹[('a, 'r) process_ptick, pttrn, 'a set, 'a → ('a, 'r) process_ptick] → ('a, 'r) process_ptick›
  (‹((_) Θ (_∈_)./ (_))› [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 ::
  \<open>[('a, 'r) process\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k, 'a set, ('a, 'r) process\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k] \<Rightarrow> ('a, 'r) process\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k\<close> (\<open>((_) \<Theta> (_)/ (_))\<close> [73, 0, 73] 72)
  where \<open>P \<Theta> A Q \<equiv> P \<Theta> a \<in> A. Q\<close>

text \<open>Now we can write @{term [eta_contract = false] \<open>P \<Theta> a \<in> A. Q a\<close>}, and when
      we do not want \<^term>\<open>Q\<close> to be parameterized we can just write \<^term>\<open>P \<Theta> A Q\<close>.\<close>

lemma \<open>P \<Theta> a \<in> A. Q = P \<Theta> A Q\<close> by (fact refl) *)



subsection ‹Projections›

lemma F_Throw:
  ‹F (P Θ a ∈ A. Q a) =
 {(t1, X). (t1, X) ∈ F P ∧ set t1 ∩ ev ` A = {}} ∪
 {(t1 @ t2, X) |t1 t2 X. t1 ∈ D P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF t2} ∪
 {(t1 @ ev a # t2, X) |t1 a t2 X.
 t1 @ [ev a] ∈ T P ∧ set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ (t2, X) ∈ F (Q a)}›
  by (simp add: Failures.rep_eq FAILURES_def Throw.rep_eq)


lemma D_Throw:
  ‹D (P Θ a ∈ A. Q a) =
 {t1 @ t2 |t1 t2. t1 ∈ D P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF t2} ∪
 {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a] ∈ T P ∧ set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ D (Q a)}›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Throw.rep_eq)


lemma T_Throw:
  ‹T (P Θ a ∈ A. Q a) =
 {t1 ∈ T P. set t1 ∩ ev ` A = {}} ∪
 {t1 @ t2 |t1 t2. t1 ∈ D P ∧ tF t1 ∧ set t1 ∩ ev ` A = {} ∧ ftF t2} ∪
 {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a] ∈ T P ∧ set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ T (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 ∈ D (P' Θ a ∈ A. Q' a) ==> s ∈ D (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 ∉ D (P Θ a ∈ A. Q a)› ‹(s, X) ∈ F (P Θ a ∈ A. Q a)›
  from assms(2) consider ‹(s, X) ∈ F P› ‹set s ∩ ev ` A = {}›
    | t1 t2   where ‹s = t1 @ t2› ‹t1 ∈ D P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
    | t1 a t2 where ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P› ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ F (Q a)›
    by (simp add: F_Throw) blast
  thus ‹(s, X) ∈ F (P' Θ a ∈ A. Q' a)›
  proof cases
    assume * : ‹(s, X) ∈ F 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 ∉ D 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) ∈ F P ==> set s ∩ ev ` A = {} ==> (s, X) ∈ F (Throw P' A Q')›
      by (simp add: F_Throw le_approx2[OF that(1) "**"])
  next
    from assms(1) show ‹[s = t1 @ t2; t1 ∈ D P; tF t1; set t1 ∩ ev ` A = {}; ftF t2]
 ==> (s, X) ∈ F (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] ∈ T P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ F (Q a)›
    from "*"(2) have ** : ‹tF t1› by (simp add: append_T_imp_tickFree)
    have *** : ‹(t2, X) ∈ F (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 ∉ D 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) ∈ F (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 ∉ D (P Θ a ∈ A. Q a) ==> (s, X) ∈ F (P' Θ a ∈ A. Q' a)
 ==> (s, X) ∈ F (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 ∈ D 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] ∈ T P ∧
 set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ D (Q a)}›

  have * : ‹min_elems (D (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 (D 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] ∈ T P› ‹set t1 ∩ ev ` A = {}› ‹a ∈ A›
      ‹t2 ∈ (D (Q a))› ‹t1 @ ev a # t2 ∈ min_elems S_right› ‹t1 @ ev a # t2 ∉ S_left›
    have ‹t2 ∈ min_elems (D (Q a))›
      ‹t1 @ [ev a] ∈ D P ==> t1 @ [ev a] ∈ min_elems (D P)›
    proof (all ‹rule ccontr›)
      assume ‹t2 ∉ min_elems (D (Q a))›
      with assms(4) obtain t2' where ‹t2' < t2 › ‹t2' ∈ D (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] ∈ D P› ‹t1 @ [ev a] ∉ min_elems (D P)›
      hence ‹t1 ∈ D P› using min_elems1 by blast
      with ‹t1 @ [ev a] ∈ D 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<sub>ptick</sub>.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] ∈ T P - D P ∧
 set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ min_elems (D (Q a))} ∪
 {t1 @ ev a # t2 |t1 a t2. t1 @ [ev a] ∈ min_elems (D P) ∧
 set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ min_elems (D (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 (D (P Θ a ∈ A. Q a))›
  from set_mp[OF "*", OF this] 
  consider ‹s ∈ min_elems (D P)› ‹set s ∩ ev ` A = {}›
    | t1 a t2 where ‹s = t1 @ ev a # t2› ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ min_elems (D (Q a))›
      ‹t1 @ [ev a] ∈ min_elems (D P) ∨ t1 @ [ev a] ∈ T P ∧ t1 @ [ev a] ∉ D P›
    using "****" by (simp add: "**") blast 
  thus ‹s ∈ T (P' Θ a ∈ A. Q' a)›
  proof cases
    show ‹s ∈ min_elems (D P) ==> set s ∩ ev ` A = {} ==> s ∈ T (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 (D (Q a))›
      ‹t1 @ [ev a] ∈ min_elems (D P) ∨ t1 @ [ev a] ∈ T P ∧ t1 @ [ev a] ∉ D P›
    have ‹t1 @ [ev a] ∈ T P' ∧ t2 ∈ T (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 ∈ T (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 ∈ T P› by (auto simp add: STOP_iff_T)
    hence ‹[hd t] ∈ T P›
      by (metis append_Cons append_Nil is_processT3_TR_append list.sel(1) neq_Nil_conv)
    hence ‹[hd t] ∈ 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 (D P)}› is probably true.›
proof (cases ‹D P = {}›)
  show ‹?lhs = ?rhs› if ‹D P = {}›
  proof (rule Process_eq_optimizedI)
    fix t assume ‹t ∈ D ?lhs›
    with ‹D P = {}› obtain t1 a t2
      where * : ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ D (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 ∈ D ?rhs› using "*"(1, 2, 5) by (auto simp add: D_Throw)
  next
    fix t assume ‹t ∈ D ?rhs›
    with ‹D P = {}› obtain t1 a t2
      where * : ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P›
        ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› ‹a ∈ A ∩ α(P)› ‹t2 ∈ D (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 ∈ D ?lhs› by (auto simp add: D_Throw)
  next
    fix t X assume ‹(t, X) ∈ F ?lhs›
    with ‹D P = {}› consider ‹(t, X) ∈ F P› ‹set t ∩ ev ` A = {}›
      | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ F (Q a)›
      unfolding F_Throw by blast
    thus ‹(t, X) ∈ F ?rhs›
    proof cases
      show ‹(t, X) ∈ F P ==> set t ∩ ev ` A = {} ==> (t, X) ∈ F ?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) ∈ F ?rhs› using failR(1, 2, 5) by (auto simp add: F_Throw)
    qed
  next
    fix t X assume ‹(t, X) ∈ F ?rhs›
    with ‹D P = {}› consider ‹(t, X) ∈ F P› ‹set t ∩ ev ` (A ∩ α(P)) = {}›
      | (failR) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P›
        ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› ‹a ∈ A›
        ‹a ∈ α(P)› ‹(t2, X) ∈ F (Q a)›
      unfolding F_Throw by blast
    thus ‹(t, X) ∈ F ?lhs›
    proof cases
      assume ‹(t, X) ∈ F P› ‹set t ∩ ev ` (A ∩ α(P)) = {}›
      from ‹(t, X) ∈ F P› have ‹t ∈ 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) ∈ F P› show ‹(t, X) ∈ F ?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) ∈ F ?lhs› by (auto simp add: F_Throw)
    qed
  qed
next
  assume ‹D 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 ∈ D ?lhs ==> s ∈ D ?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 ∈ D (Y i) ∧ tickFree t1 ∧
 set t1 ∩ ev ` A = {} ∧ front_tickFree t2} ∪
 {t1. ∃a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ T (Y i) ∧ tickFree t1 ∧
 set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ D (Q a)}› for i
  assume ‹s ∈ D ?rhs›
  hence ftF: ‹front_tickFree s› using D_imp_front_tickFree by blast
  from ‹s ∈ D ?rhs› have ‹s ∈ D (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 ∈ D ?lhs›
  proof (cases ‹∃j a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ T (Y j) ∧ a ∈ A ∧ t2 ∈ D (Q a)›)
    case True
    then obtain j a t2 where ** : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T (Y j)›
      ‹a ∈ A› ‹t2 ∈ D (Q a)› by blast
    from "*" "**"(1) have ‹∀i. t1 @ [ev a] ∈ T (Y i)›
      by (simp add: S_def) (meson D_T front_tickFree_single is_processT7)
    with "*" "**"(1, 3, 4) show ‹s ∈ D ?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 ∈ D (Y i) ∧ front_tickFree t2›
      by (simp add: S_def) blast
    hence ‹∃t2. s = t1 @ t2 ∧ (∀i. t1 ∈ D (Y i)) ∧ front_tickFree t2› by blast
    with "*" show ‹s ∈ D ?lhs›
      by (simp add: S_def D_Throw limproc_is_thelub ‹chain Y› D_LUB) blast
  qed
next
  show ‹(s, X) ∈ F ?lhs ==> (s, X) ∈ F ?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 : ‹D ?lhs = D ?rhs›
  fix s X assume ‹(s, X) ∈ F ?rhs›
  show ‹(s, X) ∈ F ?lhs›
  proof (cases ‹s ∈ D ?rhs›)
    show ‹s ∈ D ?rhs ==> (s, X) ∈ F ?lhs› by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ D ?rhs›
    have ‹∀a∈A. Q a ⊑ Q a› by simp
    moreover from ‹s ∉ D ?rhs› obtain j where ‹s ∉ D (Y j Θ a ∈ A. Q a)›
      by (auto simp add: limproc_is_thelub chain_Throw_left ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ F ?rhs› have ‹(s, X) ∈ F (Y j Θ a ∈ A. Q a)›
      by (simp add: limproc_is_thelub chain_Throw_left ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ F ?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 ∈ D ?lhs ==> s ∈ D ?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 ∈ D ?rhs›
  define S
    where ‹S i ≡ {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ D P ∧ tF t1 ∧
 set t1 ∩ ev ` A = {} ∧ ftF t2} ∪
 {t1. ∃a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ T P ∧
 set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ D (Y i a)}› for i
  assume ‹s ∈ D ?rhs›
  hence ‹s ∈ D (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 ∈ D 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] ∈ T P ∧ a ∈ A ∧ t2 ∈ D (Y i a)›
    by (simp add: S_def) blast
  thus ‹s ∈ D ?lhs›
  proof cases
    show ‹t1 ∈ D P ==> tickFree t1 ==> set t1 ∩ ev ` A = {} ==>
 ∃t2. s = t1 @ t2 ∧ front_tickFree t2 ==> s ∈ D ?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] ∈ T P ∧
 a ∈ A ∧ t2 ∈ D (Y i a)›
    from assms(2) obtain a t2
      where * : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ T P› ‹a ∈ A› by blast
    with assms(2) have ‹∀i. t2 ∈ D (Y i a)› by blast
    with assms(1) "*"(1, 2, 3) show ‹s ∈ D ?lhs›
      by (simp add: D_Throw limproc_is_thelub ‹chain Y› ch2ch_fun D_LUB) blast
  qed
next
  show ‹(s, X) ∈ F ?lhs ==> (s, X) ∈ F ?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 : ‹D ?lhs = D ?rhs›
  fix s X assume ‹(s, X) ∈ F ?rhs›
  show ‹(s, X) ∈ F ?lhs›
  proof (cases ‹s ∈ D ?rhs›)
    show ‹s ∈ D ?rhs ==> (s, X) ∈ F ?lhs› by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ D ?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 ∉ D ?rhs› obtain j where ‹s ∉ D (P Θ a ∈ A. Y j a)›
      by (auto simp add: limproc_is_thelub chain_Throw_right ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ F ?rhs› have ‹(s, X) ∈ F (P Θ a ∈ A. Y j a)›
      by (simp add: limproc_is_thelub chain_Throw_right ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ F ?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
  (*>*)