Theory Interrupt

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : The Interrupt 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 Interrupt Operator ›

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

subsection ‹Definition›

text ‹We want to add the binary operator of interruption of \<^term>‹P› by \<^term>‹Q›: 
      it behaves like \<^term>‹P› except that at any time \<^term>‹Q› can take over.›

text ‹The definition provided by Roscoe \<^cite>‹‹p.239› in "Roscoe2010UnderstandingCS"› does
      not respect the invariant \<^const>‹is_process›: it seems like \<^const>‹tick› is not handled.›

text ‹We propose here our corrected version.›

lift_definition Interrupt :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (infixl ‹△› 81)
  is ‹λP Q. 
  ({(t @ [✓(r)], X) |t r X. t @ [✓(r)] ∈ 𝒯 P} ∪
   {(t, X - {✓(r)}) |t r X. t @ [✓(r)] ∈ 𝒯 P} ∪
   {(t, X). (t, X) ∈ ℱ P ∧ tF t ∧ ([], X) ∈ ℱ Q} ∪
   {(t @ u, X) |t u X. t ∈ 𝒯 P ∧ tF t ∧ (u, X) ∈ ℱ Q ∧ u ≠ []} ∪
   {(t, X - {✓(r)}) |t r X. t ∈ 𝒯 P ∧ tF t ∧ [✓(r)] ∈ 𝒯 Q} ∪
   {(t, X). t ∈ 𝒟 P} ∪
   {(t @ u, X) |t u X. t ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒟 Q},
   𝒟 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒟 Q})›
proof -
  show ‹?thesis P Q› 
    (is ‹is_process (?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7, ?d1 ∪ ?d2)›) for P Q
    unfolding is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv
  proof (intro conjI allI impI)
    have ‹([], {}) ∈ ?f3› by (simp add: is_processT1)
    thus ‹([], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by fast
  next
    show ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹ ftF t› for t X
      by (simp add: is_processT2 D_imp_front_tickFree front_tickFree_append)
        (meson front_tickFree_append front_tickFree_dw_closed is_processT2_TR process_charn)
  next
    fix t u
    show ‹(t @ u, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹
              (t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (induct u rule: rev_induct)
      show ‹(t @ [], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹
                 (t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by simp
    next
      fix a u
      assume assm : ‹(t @ u @ [a], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
        and  hyp : ‹(t @ u, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹
                         (t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
      from assm have ‹(t @ u @ [a], {}) ∈ ?f1 ∨ (t @ u @ [a], {}) ∈ ?f2 ∨
        (t @ u @ [a], {}) ∈ ?f3 ∨ (t @ u @ [a], {}) ∈ ?f4 ∨ (t @ u @ [a], {}) ∈ ?f5 ∨ 
        (t @ u @ [a], {}) ∈ ?f6 ∨ (t @ u @ [a], {}) ∈ ?f7› by fast
      thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
      proof (elim disjE)
        assume ‹(t @ u @ [a], {}) ∈ ?f1›
        hence ‹(t, {}) ∈ ?f3›
          by simp (meson T_F append_T_imp_tickFree is_processT snoc_eq_iff_butlast) 
        thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(t @ u @ [a], {}) ∈ ?f2›
        hence ‹(t, {}) ∈ ?f3›
          by simp (metis T_F Nil_is_append_conv append_T_imp_tickFree is_processT list.discI)
        thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(t @ u @ [a], {}) ∈ ?f3›
        with is_processT3 have ‹(t, {}) ∈ ?f3› by simp blast
        thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(t @ u @ [a], {}) ∈ ?f4›
        then obtain t' u'
          where * : ‹t @ u = t' @ u'› ‹t' ∈ 𝒯 P› ‹tF t'› ‹(u' @ [a], {}) ∈ ℱ Q›
          by simp (metis butlast_append last_appendR snoc_eq_iff_butlast)
        show ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
        proof (cases ‹u' = []›)
          assume ‹u' = []›
          with "*"(1, 2, 3) have ‹(t, {}) ∈ ?f3›
            by simp (metis T_F process_charn tickFree_append_iff)
          thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
        next
          assume ‹u' ≠ []›
          with "*" is_processT3 have ‹(t @ u, {}) ∈ ?f4› by simp blast
          thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by (intro hyp) blast
        qed
      next
        assume ‹(t @ u @ [a], {}) ∈ ?f5›
        hence ‹(t, {}) ∈ ?f3› by simp (metis T_F process_charn)
        thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(t @ u @ [a], {}) ∈ ?f6›
        hence ‹(t, {}) ∈ ?f3›
          by simp (meson D_T append_T_imp_tickFree process_charn snoc_eq_iff_butlast)
        thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(t @ u @ [a], {}) ∈ ?f7›
        then obtain t' u'
          where * : ‹t @ u @ [a] = t' @ u'› ‹t' ∈ 𝒯 P› ‹tF t'› ‹u' ∈ 𝒟 Q› by blast
        hence ‹(t @ u, {}) ∈ (if length u' ≤ 1 then ?f3 else ?f4)›
          apply (cases u' rule: rev_cases; simp)
          by (metis T_F append_assoc process_charn tickFree_append_iff)
            (metis D_T T_F is_processT3)
        thus ‹(t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
          by (intro hyp) (meson UnI1 UnI2)
      qed
    qed
  next
    fix t X Y
    assume assm : ‹(t, Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ∧ X ⊆ Y›
    hence ‹(t, Y) ∈ ?f1 ∨ (t, Y) ∈ ?f2 ∨ (t, Y) ∈ ?f3 ∨ (t, Y) ∈ ?f4 ∨
           (t, Y) ∈ ?f5 ∨ (t, Y) ∈ ?f6 ∨ (t, Y) ∈ ?f7› by fast
    thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (elim disjE)
      assume ‹(t, Y) ∈ ?f1›
      hence ‹(t, X) ∈ ?f1› by simp
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, Y) ∈ ?f2›
      with assm[THEN conjunct2] have ‹(t, X) ∈ ?f2› by simp blast
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, Y) ∈ ?f3›
      with assm[THEN conjunct2] is_processT4 have ‹(t, X) ∈ ?f3› by simp blast
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, Y) ∈ ?f4›
      with assm[THEN conjunct2] is_processT4 have ‹(t, X) ∈ ?f4› by simp blast
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, Y) ∈ ?f5›
      with assm[THEN conjunct2] have ‹(t, X) ∈ ?f5› by simp blast
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, Y) ∈ ?f6›
      hence ‹(t, X) ∈ ?f6› by simp
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, Y) ∈ ?f7›
      hence ‹(t, X) ∈ ?f7› by simp
      thus ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    qed
  next
    fix t X Y
    assume assm : ‹(t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ∧
                   (∀c. c ∈ Y ⟶ (t @ [c], {}) ∉ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7)›
    have ‹(t, X) ∈ ?f1 ∨ (t, X) ∈ ?f2 ∨ (t, X) ∈ ?f3 ∨ (t, X) ∈ ?f4 ∨
          (t, X) ∈ ?f5 ∨ (t, X) ∈ ?f6 ∨ (t, X) ∈ ?f7› using assm[THEN conjunct1] by fast
    thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (elim disjE)
      assume ‹(t, X) ∈ ?f1›
      hence ‹(t, X ∪ Y) ∈ ?f1› by simp
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, X) ∈ ?f2›
      with assm[THEN conjunct2] have ‹(t, X ∪ Y) ∈ ?f2›
        by simp (metis Diff_insert_absorb Un_Diff)
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, X) ∈ ?f3›
      with assm[THEN conjunct2] have ‹(t, X ∪ Y) ∈ ?f3›
        by simp (metis F_T T_F T_nonTickFree_imp_decomp append1_eq_conv append_Nil event⇩p⇩t⇩i⇩c⇩k.distinct_disc(2)
            is_processT5_S7' list.distinct(1) tickFree_Cons_iff tickFree_append_iff)
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, X) ∈ ?f4›
      with assm[THEN conjunct2] have ‹(t, X ∪ Y) ∈ ?f4›
        by simp (metis append.assoc append_is_Nil_conv is_processT5)
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, X) ∈ ?f5›
      with assm[THEN conjunct2] have ‹(t, X ∪ Y) ∈ ?f5›
        by simp (metis Diff_empty Diff_insert0 T_F Un_Diff not_Cons_self)
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, X) ∈ ?f6›
      hence ‹(t, X ∪ Y) ∈ ?f6› by simp
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t, X) ∈ ?f7›
      hence ‹(t, X ∪ Y) ∈ ?f7› by simp
      thus ‹(t, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    qed
  next
    fix t r X
    have * : ‹(t @ [✓(r)], {}) ∉ ?f2 ∪ ?f3 ∪ ?f5›
      by simp (metis T_imp_front_tickFree front_tickFree_Cons_iff front_tickFree_append_iff
          non_tickFree_tick tickFree_Cons_iff tickFree_Nil)
    assume ‹(t @ [✓(r)], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    with "*" have ‹(t @ [✓(r)], {}) ∈ ?f1 ∨ (t @ [✓(r)], {}) ∈ ?f4 ∨
                   (t @ [✓(r)], {}) ∈ ?f6 ∨ (t @ [✓(r)], {}) ∈ ?f7› by fast
    thus ‹(t, X - {✓(r)}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (elim disjE)
      assume ‹(t @ [✓(r)], {}) ∈ ?f1›
      hence ‹(t, X - {✓(r)}) ∈ ?f2› by blast
      thus ‹(t, X - {✓(r)}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t @ [✓(r)], {}) ∈ ?f4›
      then obtain t' u'
        where ** : ‹t = t' @ u'› ‹t' ∈ 𝒯 P› ‹tF t'› ‹(u' @ [✓(r)], {}) ∈ ℱ Q› 
        by simp (metis butlast_append last_appendR snoc_eq_iff_butlast)
      hence ‹(t, X - {✓(r)}) ∈ (if u' = [] then ?f5 else ?f4)›
        by simp (metis F_T process_charn self_append_conv2)
      thus ‹(t, X - {✓(r)}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by (meson UnCI)
    next
      assume ‹(t @ [✓(r)], {}) ∈ ?f6›
      with is_processT9 have ‹t ∈ 𝒟 P› by fast
      thus ‹(t, X - {✓(r)}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(t @ [✓(r)], {}) ∈ ?f7›
      then obtain t' u'
        where ** : ‹t @ [✓(r)] = t' @ u'› ‹t' ∈ 𝒯 P› ‹tF t'› ‹u' ∈ 𝒟 Q› by blast
      from "**"(1, 3, 4) obtain u'' where ‹u' = u'' @ [✓(r)]› ‹u'' @ [✓(r)] ∈ 𝒟 Q›
        by (cases u' rule: rev_cases) auto
      with "**"(1) is_processT9 have ‹t = t' @ u'' ∧ u'' ∈ 𝒟 Q› by force
      with "**"(2, 3) have ‹(t, X - {✓(r)}) ∈ ?f7› by simp blast
      thus ‹(t, X - {✓(r)}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    qed
  next
    show ‹t ∈ ?d1 ∪ ?d2 ∧ tF t ∧ ftF u ⟹ t @ u ∈ ?d1 ∪ ?d2› for t u
      apply (simp, elim conjE disjE exE)
      by (solves ‹simp add: is_processT7›)      
        (meson append.assoc is_processT7 tickFree_append_iff)
  next
    show ‹t ∈ ?d1 ∪ ?d2 ⟹ (t, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› for t X
      by blast
  next
    fix t r
    assume ‹t @ [✓(r)] ∈ ?d1 ∪ ?d2›
    then consider ‹t @ [✓(r)] ∈ ?d1› | ‹t @ [✓(r)] ∈ ?d2› by blast
    thus ‹t ∈ ?d1 ∪ ?d2›
    proof cases
      assume ‹t @ [✓(r)] ∈ ?d1›
      hence ‹t ∈ ?d1› by (fact is_processT9)
      thus ‹t ∈ ?d1 ∪ ?d2› by blast
    next
      assume ‹t @ [✓(r)] ∈ ?d2›
      then obtain t' u'
        where ** : ‹t @ [✓(r)] = t' @ u'› ‹t' ∈ 𝒯 P› ‹tF t'› ‹u' ∈ 𝒟 Q› by blast
      from "**"(1, 3, 4) obtain u'' where ‹u' = u'' @ [✓(r)]› ‹u'' @ [✓(r)] ∈ 𝒟 Q›
        by (cases u' rule: rev_cases) auto
      with "**"(1) is_processT9 have ‹t = t' @ u'' ∧ u'' ∈ 𝒟 Q› by force
      with "**"(2, 3) have ‹t ∈ ?d2› by simp blast
      thus ‹t ∈ ?d1 ∪ ?d2› by blast
    qed
  qed
qed



subsection ‹Projections›

lemma F_Interrupt :
  ‹ℱ (P △ Q) = 
   {(t @ [✓(r)], X) |t r X. t @ [✓(r)] ∈ 𝒯 P} ∪
   {(t, X - {✓(r)}) |t r X. t @ [✓(r)] ∈ 𝒯 P} ∪
   {(t, X). (t, X) ∈ ℱ P ∧ tF t ∧ ([], X) ∈ ℱ Q} ∪
   {(t @ u, X) |t u X. t ∈ 𝒯 P ∧ tF t ∧ (u, X) ∈ ℱ Q ∧ u ≠ []} ∪
   {(t, X - {✓(r)}) |t r X. t ∈ 𝒯 P ∧ tF t ∧ [✓(r)] ∈ 𝒯 Q} ∪
   {(t, X). t ∈ 𝒟 P} ∪
   {(t @ u, X) |t u X. t ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒟 Q}›
  by (simp add: Failures.rep_eq FAILURES_def Interrupt.rep_eq)

lemma D_Interrupt : 
  ‹𝒟 (P △ Q) = 𝒟 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒟 Q}›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Interrupt.rep_eq)

lemma T_Interrupt : 
  ‹𝒯 (P △ Q) = 𝒯 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒯 Q}›
  apply (simp add: Traces.rep_eq TRACES_def F_Interrupt flip: Failures.rep_eq)
  apply (safe, simp_all add: is_processT8)
       apply (meson is_processT4_empty is_processT6)
      apply auto[2]
    apply (metis is_processT8)
   apply (metis is_processT4_empty nonTickFree_n_frontTickFree process_charn)
  by (metis append.right_neutral is_processT4_empty tickFree_Nil)

lemmas Interrupt_projs = F_Interrupt D_Interrupt T_Interrupt



subsection ‹Monotony›

lemma mono_Interrupt : ‹P △ Q ⊑ P' △ Q'› if ‹P ⊑ P'› and ‹Q ⊑ Q'›
proof (unfold le_approx_def, intro conjI allI impI subsetI)
  show ‹s ∈ 𝒟 (P' △ Q') ⟹ s ∈ 𝒟 (P △ Q)› for s
    using ‹P ⊑ P'›[THEN le_approx1] ‹Q ⊑ Q'›[THEN le_approx1]
      ‹P ⊑ P'›[THEN le_approx2T] D_T by (simp add: D_Interrupt) blast
next
  show ‹s ∉ 𝒟 (P △ Q) ⟹ ℛ⇩a (P △ Q) s = ℛ⇩a (P' △ Q') s› for s
    apply (simp add: D_Interrupt Refusals_after_def F_Interrupt,
        intro subset_antisym subsetI; simp, elim disjE)
                apply (metis le_approx2T ‹P ⊑ P'›)
               apply (metis is_processT9 le_approx2T ‹P ⊑ P'›)
              apply (metis F_T append.right_neutral le_approx2 ‹P ⊑ P'› ‹Q ⊑ Q'›)
             apply (metis is_processT2 is_processT7 le_approx2T proc_ord2a ‹P ⊑ P'› ‹Q ⊑ Q'›)
            apply (metis append_Nil2 is_processT9 le_approx2T self_append_conv2 ‹P ⊑ P'› ‹Q ⊑ Q'›)
           apply metis
          apply (metis le_approx2T ‹P ⊑ P'›)
         apply (metis le_approx_lemma_T subset_eq ‹P ⊑ P'›)
        apply (metis is_processT8 le_approx2 ‹P ⊑ P'› ‹Q ⊑ Q'›)
       apply (metis is_processT2 is_processT7 le_approx2 le_approx2T ‹P ⊑ P'› ‹Q ⊑ Q'›) 
      apply (metis D_T le_approx2T ‹P ⊑ P'› ‹Q ⊑ Q'›)
     apply (metis in_mono le_approx1 ‹P ⊑ P'›)
    by (metis le_approx1 le_approx2T process_charn subsetD ‹P ⊑ P'› ‹Q ⊑ Q'›)
next
  (* from ‹P ⊑ P'›[THEN le_approx3] ‹Q ⊑ Q'›[THEN le_approx3] *)
  show ‹s ∈ min_elems (𝒟 (P △ Q)) ⟹ s ∈ 𝒯 (P' △ Q')› for s
    apply (rule set_mp[of ‹min_elems (𝒟 P) ∪ {t1 @ t2| t1 t2. t1 ∈ 𝒯 P' ∧ tickFree t1 ∧ t2 ∈ min_elems (𝒟 Q)}›])
      (* apply (use ‹P ⊑ P'›[THEN le_approx3] ‹Q ⊑ Q'›[THEN le_approx3] in simp) *)
     apply (rule Un_least)
      apply (simp add: T_Interrupt le_approx3 le_supI1 ‹P ⊑ P'›)
     apply (simp add: T_Interrupt subset_iff, metis le_approx_def subset_iff ‹Q ⊑ Q'›)
    apply (simp add: min_elems_def D_Interrupt less_list_def)
      (* TODO: break this smt *)
    by (smt (verit, ccfv_threshold) D_imp_front_tickFree same_prefix_prefix Un_iff is_processT7 le_approx2T mem_Collect_eq same_append_eq that(1))
qed




subsection ‹Properties›

lemma Interrupt_STOP [simp] : ‹P △ STOP = P›
proof (subst Process_eq_spec, safe)
  show ‹t ∈ 𝒟 (P △ STOP) ⟹ t ∈ 𝒟 P› for t
    by (simp add: D_Interrupt D_STOP)
next
  show ‹t ∈ 𝒟 P ⟹ t ∈ 𝒟 (P △ STOP)› for t
    by (simp add: D_Interrupt D_STOP)
next
  show ‹(t, X) ∈ ℱ (P △ STOP) ⟹ (t, X) ∈ ℱ P› for t X
    by (simp add: F_Interrupt STOP_projs)
      (meson is_processT6_TR is_processT8 tick_T_F)
next
  show ‹(t, X) ∈ ℱ P ⟹ (t, X) ∈ ℱ (P △ STOP)› for t X
    by (simp add: F_Interrupt STOP_projs)
      (metis F_T T_nonTickFree_imp_decomp)
qed

lemma STOP_Interrupt [simp] : ‹STOP △ P = P›
proof (subst Process_eq_spec, safe)
  show ‹t ∈ 𝒟 (STOP △ P) ⟹ t ∈ 𝒟 P› for t
    by (simp add: D_Interrupt STOP_projs)
next
  show ‹t ∈ 𝒟 P ⟹ t ∈ 𝒟 (STOP △ P)› for t
    by (simp add: D_Interrupt STOP_projs)
next
  show ‹(t, X) ∈ ℱ (STOP △ P) ⟹ (t, X) ∈ ℱ P› for t X
    by (simp add: F_Interrupt STOP_projs)
      (metis is_processT6_TR is_processT8 self_append_conv2)
next
  show ‹(t, X) ∈ ℱ P ⟹ (t, X) ∈ ℱ (STOP △ P)› for t X
    by (auto simp add: F_Interrupt STOP_projs)
qed

lemma Interrupt_is_STOP_iff : ‹P △ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  by (simp add: STOP_iff_T T_Interrupt set_eq_iff)
    (metis append_self_conv2 is_processT1_TR tickFree_Nil)


lemma Interrupt_BOT [simp] : ‹P △ ⊥ = ⊥›
  and BOT_Interrupt [simp] : ‹⊥ △ P = ⊥›
  by (simp_all add: BOT_iff_Nil_D D_Interrupt D_BOT)

lemma Interrupt_is_BOT_iff : ‹P △ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: BOT_iff_Nil_D D_Interrupt)


lemma SKIP_Interrupt_is_SKIP_Det : ‹SKIP r △ P = SKIP r □ P›
proof (subst Process_eq_spec, safe)
  show ‹t ∈ 𝒟 (SKIP r △ P) ⟹ t ∈ 𝒟 (SKIP r □ P)› for t
    by (auto simp add: D_Interrupt D_Det SKIP_projs)
next
  show ‹t ∈ 𝒟 (SKIP r □ P) ⟹ t ∈ 𝒟 (SKIP r △ P)› for t
    by (auto simp add: D_Interrupt D_Det SKIP_projs intro: tickFree_Nil)
next
  show ‹(t, X) ∈ ℱ (SKIP r △ P) ⟹ (t, X) ∈ ℱ (SKIP r □ P)› for t X
    by (cases t) (auto simp add: F_Interrupt SKIP_projs F_Det intro: is_processT8)
next
  show ‹(t, X) ∈ ℱ (SKIP r □ P) ⟹ (t, X) ∈ ℱ (SKIP r △ P)› for t X
    by (cases t) (auto simp add: F_Interrupt SKIP_projs F_Det intro: tickFree_Nil)
qed



lemma Interrupt_assoc: ‹P △ (Q △ R) = P △ Q △ R› (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = ?rhs› if non_BOT : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹R ≠ ⊥›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    then consider ‹s ∈ 𝒟 P›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 (Q △ R)›
      by (simp add: D_Interrupt) blast
    thus ‹s ∈ 𝒟 ?rhs›
    proof cases
      show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 ?rhs› by (simp add: D_Interrupt)
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 (Q △ R)›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 P›
        ‹tickFree t1› ‹t2 ∈ 𝒟 (Q △ R)› by blast
      from "*"(4) consider ‹t2 ∈ 𝒟 Q›
        | ‹∃u1 u2. t2 = u1 @ u2 ∧ u1 ∈ 𝒯 Q ∧ tickFree u1 ∧ u2 ∈ 𝒟 R›
        by (simp add: D_Interrupt) blast
      thus ‹s ∈ 𝒟 ?rhs›
      proof cases
        from "*"(1, 2, 3) show ‹t2 ∈ 𝒟 Q ⟹ s ∈ 𝒟 ?rhs› by (simp add: D_Interrupt) blast
      next
        show ‹∃u1 u2. t2 = u1 @ u2 ∧ u1 ∈ 𝒯 Q ∧ tickFree u1 ∧ u2 ∈ 𝒟 R ⟹ s ∈ 𝒟 ?rhs›
          by (simp add: "*"(1) D_Interrupt T_Interrupt)
            (metis "*"(2, 3) append_assoc tickFree_append_iff)
      qed
    qed
  next
    fix s
    assume ‹s ∈ 𝒟 ?rhs›
    then consider ‹s ∈ 𝒟 (P △ Q)›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P △ Q) ∧ tickFree t1 ∧ t2 ∈ 𝒟 R›
      by (simp add: D_Interrupt) blast
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      show ‹s ∈ 𝒟 (P △ Q) ⟹ s ∈ 𝒟 ?lhs› by (simp add: D_Interrupt) blast
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P △ Q) ∧ tickFree t1 ∧ t2 ∈ 𝒟 R›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (P △ Q)›
        ‹tickFree t1› ‹t2 ∈ 𝒟 R› by blast
      from "*"(2) consider ‹t1 ∈ 𝒯 P›
        | ‹∃u1 u2. t1 = u1 @ u2 ∧ u1 ∈ 𝒯 P ∧ tickFree u1 ∧ u2 ∈ 𝒯 Q›
        by (simp add: T_Interrupt) blast
      thus ‹s ∈ 𝒟 ?lhs›
      proof cases
        show ‹t1 ∈ 𝒯 P ⟹ s ∈ 𝒟 ?lhs›
          by (simp add: D_Interrupt "*"(1))
            (metis "*"(3, 4) Nil_elem_T append_Nil tickFree_Nil)
      next
        show ‹∃u1 u2. t1 = u1 @ u2 ∧ u1 ∈ 𝒯 P ∧ tickFree u1 ∧ u2 ∈ 𝒯 Q ⟹ s ∈ 𝒟 ?lhs›
          by (simp add: D_Interrupt "*"(1)) 
            (metis "*"(3, 4) append.assoc tickFree_append_iff)
      qed
    qed
  next
    fix s X
    assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      | ‹∃t1 r. s = t1 @ [✓(r)] ∧ t1 @ [✓(r)] ∈ 𝒯 P›
      | ‹∃r. s @ [✓(r)] ∈ 𝒯 P ∧ ✓(r) ∉ X›
      | ‹(s, X) ∈ ℱ P ∧ tickFree s ∧ ([], X) ∈ ℱ (Q △ R)›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ (Q △ R) ∧ t2 ≠ []›
      | ‹∃r. s ∈ 𝒯 P ∧ tickFree s ∧ [✓(r)] ∈ 𝒯 (Q △ R) ∧ ✓(r) ∉ X›
      by (subst (asm) F_Interrupt, simp add: D_Interrupt) blast
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
    next
      show ‹∃t1 r. s = t1 @ [✓(r)] ∧ t1 @ [✓(r)] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Interrupt T_Interrupt)
    next
      show ‹∃r. s @ [✓(r)] ∈ 𝒯 P ∧ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
    next
      assume assm : ‹(s, X) ∈ ℱ P ∧ tickFree s ∧ ([], X) ∈ ℱ (Q △ R)›
      with non_BOT(2, 3) consider r where ‹[✓(r)] ∈ 𝒯 Q ∧ ✓(r) ∉ X›
        | ‹([], X) ∈ ℱ Q ∧ ([], X) ∈ ℱ R›
        | r where ‹[] ∈ 𝒯 Q ∧ [✓(r)] ∈ 𝒯 R ∧ ✓(r) ∉ X›
        by (simp add: F_Interrupt BOT_iff_Nil_D) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        show ‹[✓(r)] ∈ 𝒯 Q ∧ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb F_T assm)
      next
        show ‹([], X) ∈ ℱ Q ∧ ([], X) ∈ ℱ R ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Interrupt assm)
      next
        show ‹[] ∈ 𝒯 Q ∧ [✓(r)] ∈ 𝒯 R ∧ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb F_T assm)
      qed
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧
                      (t2, X) ∈ ℱ (Q △ R) ∧ t2 ≠ []›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹tickFree t1› 
        ‹(t2, X) ∈ ℱ (Q △ R)› ‹t2 ≠ []› by blast
      from "*"(4) consider ‹t2 ∈ 𝒟 (Q △ R)›
        | u1 r where ‹t2 = u1 @ [✓(r)]› ‹u1 @ [✓(r)] ∈ 𝒯 Q›
        | r where ‹t2 @ [✓(r)] ∈ 𝒯 Q› ‹✓(r) ∉ X›
        | ‹(t2, X) ∈ ℱ Q› ‹tickFree t2› ‹([], X) ∈ ℱ R›
        | u1 u2 where ‹t2 = u1 @ u2› ‹u1 ∈ 𝒯 Q› ‹tickFree u1› ‹(u2, X) ∈ ℱ R› ‹u2 ≠ []›
        | r where ‹t2 ∈ 𝒯 Q› ‹tickFree t2› ‹[✓(r)] ∈ 𝒯 R› ‹✓(r) ∉ X›
        by (simp add: F_Interrupt D_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        assume ‹t2 ∈ 𝒟 (Q △ R)›
        with "*"(1, 2, 3) have ‹s ∈ 𝒟 ?lhs› by (simp add: D_Interrupt) blast
        with same_div D_F show ‹(s, X) ∈ ℱ ?rhs› by blast
      next
        from "*"(1, 2, 3) show ‹t2 = u1 @ [✓(r)] ⟹ u1 @ [✓(r)] ∈ 𝒯 Q ⟹ (s, X) ∈ ℱ ?rhs› for u1 r
          by (auto simp add: F_Interrupt T_Interrupt)
      next
        from "*"(1, 2, 3) show ‹t2 @ [✓(r)] ∈ 𝒯 Q ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      next
        from "*"(1) show ‹(t2, X) ∈ ℱ Q ⟹ tickFree t2 ⟹ ([], X) ∈ ℱ R ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Interrupt T_Interrupt) (metis "*"(2, 3, 5))
      next
        from "*"(1, 2, 3) show ‹t2 = u1 @ u2 ⟹ u1 ∈ 𝒯 Q ⟹ tickFree u1 ⟹
                                (u2, X) ∈ ℱ R ⟹ u2 ≠ [] ⟹ (s, X) ∈ ℱ ?rhs› for u1 u2
          by (simp add: F_Interrupt T_Interrupt)
            (metis (mono_tags, lifting) append_assoc tickFree_append_iff)
      next
        from "*"(1, 2, 3) show ‹t2 ∈ 𝒯 Q ⟹ tickFree t2 ⟹
          [✓(r)] ∈ 𝒯 R ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      qed
    next
      show ‹∃r. s ∈ 𝒯 P ∧ tickFree s ∧ [✓(r)] ∈ 𝒯 (Q △ R) ∧ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Interrupt T_Interrupt)
          (metis Diff_insert_absorb append_eq_Cons_conv non_tickFree_tick tickFree_append_iff)
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    then consider ‹s ∈ 𝒟 ?rhs›
      | ‹∃t1 r. s = t1 @ [✓(r)] ∧ t1 @ [✓(r)] ∈ 𝒯 (P △ Q)›
      | r where ‹s @ [✓(r)] ∈ 𝒯 (P △ Q)› ‹✓(r) ∉ X›
      | ‹(s, X) ∈ ℱ (P △ Q) ∧ tickFree s ∧ ([], X) ∈ ℱ R›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P △ Q) ∧ tickFree t1 ∧ (t2, X) ∈ ℱ R ∧ t2 ≠ []›
      | ‹∃r. s ∈ 𝒯 (P △ Q) ∧ tickFree s ∧ [✓(r)] ∈ 𝒯 R ∧ ✓(r) ∉ X›
      by (subst (asm) F_Interrupt, simp add: D_Interrupt) blast 
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 ?rhs ⟹ (s, X) ∈ ℱ ?lhs› by blast
    next
      show ‹∃t1 r. s = t1 @ [✓(r)] ∧ t1 @ [✓(r)] ∈ 𝒯 (P △ Q) ⟹ (s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt T_Interrupt)
          (metis last_append self_append_conv snoc_eq_iff_butlast)
    next
      fix r assume ‹s @ [✓(r)] ∈ 𝒯 (P △ Q)› ‹✓(r) ∉ X›
      from this(1) consider ‹s @ [✓(r)] ∈ 𝒯 P›
        | t1 t2 where ‹s @ [✓(r)] = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹tickFree t1› ‹t2 ∈ 𝒯 Q›
        by (simp add: T_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        show ‹s @ [✓(r)] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt) (metis Diff_insert_absorb ‹✓(r) ∉ X›)
      next
        show ‹s @ [✓(r)] = t1 @ t2 ⟹ t1 ∈ 𝒯 P ⟹ tickFree t1 ⟹ t2 ∈ 𝒯 Q ⟹ (s, X) ∈ ℱ ?lhs› for t1 t2

(* TODO: break the smts *)
          apply (simp add: F_Interrupt T_Interrupt, safe, simp_all)
             apply (smt (z3) Diff_insert_absorb T_nonTickFree_imp_decomp ‹✓(r) ∉ X› append.assoc append1_eq_conv append_self_conv2 non_tickFree_tick tickFree_append_iff) 
            apply (metis ‹s @ [✓(r)] ∈ 𝒯 (P △ Q)› append_T_imp_tickFree list.discI)
           apply (smt (z3) Diff_insert_absorb T_nonTickFree_imp_decomp ‹✓(r) ∉ X› append1_eq_conv append_assoc is_processT6_TR non_tickFree_tick tickFree_append_iff)
          apply (smt (z3) Diff_insert_absorb T_nonTickFree_imp_decomp ‹✓(r) ∉ X› append1_eq_conv append_assoc non_tickFree_tick self_append_conv2 tickFree_append_iff)
          done
      qed
    next
      assume assm : ‹(s, X) ∈ ℱ (P △ Q) ∧ tickFree s ∧ ([], X) ∈ ℱ R›
      from assm[THEN conjunct1] consider ‹s ∈ 𝒟 (P △ Q)›
        | t1 r where ‹s = t1 @ [✓(r)]› ‹t1 @ [✓(r)] ∈ 𝒯 P›
        | r where ‹s @ [✓(r)] ∈ 𝒯 P› ‹✓(r) ∉ X›
        | ‹(s, X) ∈ ℱ P› ‹tickFree s› ‹([], X) ∈ ℱ Q›
        | t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹tickFree t1› ‹(t2, X) ∈ ℱ Q› ‹t2 ≠ []›
        | r where ‹s ∈ 𝒯 P› ‹tickFree s› ‹[✓(r)] ∈ 𝒯 Q› ‹✓(r) ∉ X›
        by (simp add: F_Interrupt D_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (P △ Q)›
        hence ‹s ∈ 𝒟 ?rhs› by (simp add: D_Interrupt)
        with same_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        show ‹s = t1 @ [✓(r)] ⟹ t1 @ [✓(r)] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?lhs› for t1 r
          by (simp add: F_Interrupt)
      next
        show ‹s @ [✓(r)] ∈ 𝒯 P ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?lhs› for r
          by (simp add: F_Interrupt) (metis Diff_insert_absorb)
      next
        show ‹(s, X) ∈ ℱ P ⟹ tickFree s ⟹ ([], X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt assm[THEN conjunct2])
      next
        show ‹s = t1 @ t2 ⟹ t1 ∈ 𝒯 P ⟹ tickFree t1 ⟹ (t2, X) ∈ ℱ Q ⟹
              t2 ≠ [] ⟹ (s, X) ∈ ℱ ?lhs› for t1 t2
          by (simp add: F_Interrupt) (metis assm[THEN conjunct2] tickFree_append_iff)
      next
        show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ [✓(r)] ∈ 𝒯 Q ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?lhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      qed
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P △ Q) ∧ 
                      tickFree t1 ∧ (t2, X) ∈ ℱ R ∧ t2 ≠ []›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (P △ Q)›
        ‹tickFree t1› ‹(t2, X) ∈ ℱ R› ‹t2 ≠ []› by blast
      from "*"(2) consider ‹t1 ∈ 𝒯 P›
        | ‹∃u1 u2. t1 = u1 @ u2 ∧ u1 ∈ 𝒯 P ∧ tickFree u1 ∧ u2 ∈ 𝒯 Q›
        by (simp add: T_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        from "*"(1, 3, 4, 5) show ‹t1 ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt T_Interrupt)
            (metis Nil_elem_T append_Nil tickFree_Nil)
      next
        from "*"(1, 3, 4, 5) show ‹∃u1 u2. t1 = u1 @ u2 ∧ u1 ∈ 𝒯 P ∧
                                           tickFree u1 ∧ u2 ∈ 𝒯 Q ⟹ (s, X) ∈ ℱ ?lhs›
          by (elim exE, simp add: F_Interrupt) (metis append_is_Nil_conv)
      qed
    next
      show ‹∃r. s ∈ 𝒯 (P △ Q) ∧ tickFree s ∧ [✓(r)] ∈ 𝒯 R ∧ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt T_Interrupt)
          (metis Diff_insert_absorb Nil_elem_T append.right_neutral
            append_Nil tickFree_append_iff)
    qed
  qed

  thus ‹?lhs = ?rhs›
    by (cases ‹P = ⊥›; cases ‹Q = ⊥›; cases ‹R = ⊥›) simp_all
qed



subsection ‹Continuity›

context begin

private lemma chain_Interrupt_left: ‹chain Y ⟹ chain (λi. Y i △ Q)›
  by (simp add: chain_def mono_Interrupt)

private lemma chain_Interrupt_right: ‹chain Y ⟹ chain (λi. P △ Y i)›
  by (simp add: chain_def mono_Interrupt)  


private lemma cont_left_prem_Interrupt : ‹(⨆ i. Y i) △ Q = (⨆ i. Y i  △ Q)›
  (is ‹?lhs = ?rhs›) if chain : ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (simp add: limproc_is_thelub chain chain_Interrupt_left
        D_Interrupt T_LUB D_LUB) blast
next
  fix s
  define S
    where ‹S i ≡ {t1. s = t1 ∧ t1 ∈ 𝒟 (Y i)} ∪
                  {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Y i) ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q}› for i
  assume ‹s ∈ 𝒟 ?rhs›
  hence ‹s ∈ 𝒟 (Y i △ Q)› for i
    by (simp add: limproc_is_thelub D_LUB chain_Interrupt_left chain)
  hence ‹S i ≠ {}› for i by (simp add: S_def D_Interrupt) blast
  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)
      (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 ‹∀i. s ∈ 𝒟 (Y i)›)
    case True
    thus ‹s ∈ 𝒟 ?lhs› by (simp add: D_Interrupt limproc_is_thelub D_LUB chain)
  next
    case False
    with "*" obtain j t2 where ** : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (Y j)› ‹ tickFree t1› ‹t2 ∈ 𝒟 Q›
      by (simp add: S_def) blast
    from "*" D_T have ‹∀i. t1 ∈ 𝒯 (Y i)› by (simp add: S_def) blast
    with "**"(1, 3, 4) show ‹s ∈ 𝒟 ?lhs›
      by (simp add: D_Interrupt limproc_is_thelub T_LUB chain) blast
  qed
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (simp add: limproc_is_thelub chain chain_Interrupt_left
        F_Interrupt F_LUB T_LUB D_LUB, safe; simp; metis)
next
  assume same_div : ‹𝒟 ((⨆i. Y i) △ Q) = 𝒟 (⨆i. Y i △ Q)›
  fix s X assume ‹(s, X) ∈ ℱ (⨆i. Y i △ Q)›
  show ‹(s, X) ∈ ℱ ((⨆i. Y i) △ Q)›
  proof (cases ‹s ∈ 𝒟 (⨆i. Y i △ Q)›)
    show ‹s ∈ 𝒟 (⨆i. Y i △ Q) ⟹ (s, X) ∈ ℱ ((⨆i. Y i) △ Q)›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ 𝒟 (⨆i. Y i △ Q)›
    then obtain j where ‹s ∉ 𝒟 (Y j △ Q)›
      by (auto simp add: limproc_is_thelub chain_Interrupt_left ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ ℱ (⨆i. Y i △ Q)› have ‹(s, X) ∈ ℱ (Y j △ Q)›
      by (simp add: limproc_is_thelub chain_Interrupt_left ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ ℱ ((⨆i. Y i) △ Q)›
      by (fact le_approx2[OF mono_Interrupt[OF is_ub_thelub[OF ‹chain Y›] below_refl], THEN iffD2])
  qed
qed



private lemma cont_right_prem_Interrupt : ‹S △ (⨆i. Y i) = (⨆i. S △ Y i)› if ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 (S △ (⨆i. Y i)) ⟹ s ∈ 𝒟 (⨆i. S △ Y i)› for s
    by (auto simp add: D_Interrupt limproc_is_thelub ‹chain Y› chain_Interrupt_right D_LUB)
next
  fix s assume ‹s ∈ 𝒟 (⨆i. S △ Y i)›
  show ‹s ∈ 𝒟 (S △ (⨆i. Y i))›
  proof (cases ‹s ∈ 𝒟 S›)
    show ‹s ∈ 𝒟 S ⟹ s ∈ 𝒟 (S △ (⨆i. Y i))› by (simp add: D_Interrupt)
  next
    assume ‹s ∉ 𝒟 S›
    thm D_Interrupt
    define T where ‹T i ≡ {t1. ∃t2 r. s = t1 @ t2 ∧ t1 ∈ 𝒯 S ∧ tickFree t1 ∧ t2 ∈ 𝒟 (Y i)}› for i
    from ‹s ∉ 𝒟 S› ‹s ∈ 𝒟 (⨆i. S △ Y i)› have ‹T i ≠ {}› for i
      by (simp add: T_def limproc_is_thelub chain_Interrupt_right ‹chain Y› D_LUB D_Interrupt) blast
    moreover have ‹finite (T 0)›
      unfolding T_def by (prove_finite_subset_of_prefixes s)
    moreover have ‹T (Suc i) ⊆ T i› for i
      unfolding T_def apply (intro allI Un_mono subsetI; simp)
      by (metis le_approx1 po_class.chainE subset_iff ‹chain Y›)
    ultimately have ‹(⋂i. T i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
    then obtain t1 where ‹∀i. t1 ∈ T i› by auto
    then obtain t2 where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 S› ‹tickFree t1› ‹∀i. t2 ∈ 𝒟 (Y i)›
      by (simp add: T_def) blast
    thus ‹s ∈ 𝒟 (S △ (⨆i. Y i))›
      by (simp add: D_Interrupt limproc_is_thelub ‹chain Y› D_LUB) blast
  qed
next
  show ‹(s, X) ∈ ℱ (S △ (⨆i. Y i)) ⟹ (s, X) ∈ ℱ (⨆i. S △ Y i)› for s X
    by (simp add: F_Interrupt limproc_is_thelub ‹chain Y› chain_Interrupt_right F_LUB T_LUB D_LUB)
      (elim disjE exE conjE; metis)
next
  assume same_div : ‹𝒟 (S △ (⨆i. Y i)) = 𝒟 (⨆i. S △ Y i)›
  fix s X assume ‹(s, X) ∈ ℱ (⨆i. S △ Y i)›
  show ‹(s, X) ∈ ℱ (S △ (⨆i. Y i))›
  proof (cases ‹s ∈ 𝒟 (⨆i. S △ Y i)›)
    show ‹s ∈ 𝒟 (⨆i. S △ Y i) ⟹ (s, X) ∈ ℱ (S △ (⨆i. Y i))›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ 𝒟 (⨆i. S △ Y i)›
    then obtain j where ‹s ∉ 𝒟 (S △ Y j)›
      by (auto simp add: limproc_is_thelub chain_Interrupt_right ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ ℱ (⨆i. S △ Y i)› have ‹(s, X) ∈ ℱ (S △ Y j)›
      by (simp add: limproc_is_thelub chain_Interrupt_right ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ ℱ (S △ (⨆i. Y i))›
      by (fact le_approx2[OF mono_Interrupt[OF below_refl is_ub_thelub[OF ‹chain Y›]], THEN iffD2])
  qed
qed



lemma Interrupt_cont [simp] :
  ‹cont (λx. f x △ g x)› if ‹cont f› and ‹cont g›
proof (rule cont_apply[where f = ‹λx y. f x △ y›])
  show ‹cont g› by (fact ‹cont g›)
next
  show ‹cont ((△) (f x))› for x
  proof (rule contI2)
    show ‹monofun ((△) (f x))› by (simp add: mono_Interrupt monofunI)
  next
    show ‹chain Y ⟹ f x △ (⨆i. Y i) ⊑ (⨆i. f x △ Y i)› for Y
      by (simp add: cont_right_prem_Interrupt)
  qed
next
  show ‹cont (λx. f x △ y)› for y
  proof (rule contI2)
    show ‹monofun (λx. f x △ y)› by (simp add: cont2monofunE mono_Interrupt monofunI ‹cont f›)
  next
    show ‹chain Y ⟹ f (⨆i. Y i) △ y ⊑ (⨆i. f (Y i) △ y)› for Y
      by (simp add: ch2ch_cont cont2contlubE cont_left_prem_Interrupt ‹cont f›)
  qed
qed


end

(*<*)
end
  (*>*)