Theory Interrupt

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

section‹ The Interrupt Operator ›


theory  Interrupt
  imports "HOL-CSPM.CSPM"
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 :: ‹['α process, 'α process] ⇒ 'α process› (infixl ‹△› 75)
  is ‹λP Q. 
  ({(t1 @ [tick], X)| t1 X. t1 @ [tick] ∈ 𝒯 P} ∪
   {(t1, X - {tick})| t1 X. t1 @ [tick] ∈ 𝒯 P} ∪
   {(t1, X) ∈ ℱ P. tickFree t1 ∧ ([], X) ∈ ℱ Q} ∪
   {(t1 @ t2, X)| t1 t2 X. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []} ∪
   {(t1, X - {tick})| t1 X. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ [tick] ∈ 𝒯 Q} ∪
   {(t1, X). t1 ∈ 𝒟 P} ∪ 
   {(t1 @ t2, X)| t1 t2 X. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q},
   𝒟 P ∪ {t1 @ t2| t1 t2. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 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 ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹ front_tickFree s› for s 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 s t
    show ‹(s @ t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹
              (s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (induct t rule: rev_induct)
      show ‹(s @ [], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹
                 (s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by simp
    next
      fix a t
      assume assm : ‹(s @ t @ [a], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
         and  hyp : ‹(s @ t, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ⟹
                         (s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
      from assm have ‹(s @ t @ [a], {}) ∈ ?f1 ∨ (s @ t @ [a], {}) ∈ ?f2 ∨
        (s @ t @ [a], {}) ∈ ?f3 ∨ (s @ t @ [a], {}) ∈ ?f4 ∨ (s @ t @ [a], {}) ∈ ?f5 ∨ 
        (s @ t @ [a], {}) ∈ ?f6 ∨ (s @ t @ [a], {}) ∈ ?f7› by fast
      thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
      proof (elim disjE)
        assume ‹(s @ t @ [a], {}) ∈ ?f1›
        hence ‹(s, {}) ∈ ?f3›
          by simp (meson NF_NT append_T_imp_tickFree is_processT snoc_eq_iff_butlast) 
        thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(s @ t @ [a], {}) ∈ ?f2›
        hence ‹(s, {}) ∈ ?f3›
          by simp (metis NF_NT Nil_is_append_conv append_T_imp_tickFree is_processT list.discI)
        thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(s @ t @ [a], {}) ∈ ?f3›
        with is_processT3 have ‹(s, {}) ∈ ?f3› by simp blast
        thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(s @ t @ [a], {}) ∈ ?f4›
        then obtain t1 t2 where * : ‹s @ t = t1 @ t2› ‹t1 ∈ 𝒯 P›
                                    ‹tickFree t1› ‹(t2 @ [a], {}) ∈ ℱ Q›
          by simp (metis butlast_append last_appendR snoc_eq_iff_butlast)
        show ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
        proof (cases ‹t2 = []›)
          assume ‹t2 = []›
          with "*"(1, 2, 3) have ‹(s, {}) ∈ ?f3›
            by simp (metis T_F process_charn tickFree_append)
          thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
        next
          assume ‹t2 ≠ []›
          with "*" is_processT3 have ‹(s @ t, {}) ∈ ?f4› by simp blast
          thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by (intro hyp) blast
        qed
      next
        assume ‹(s @ t @ [a], {}) ∈ ?f5›
        hence ‹(s, {}) ∈ ?f3› by simp (metis T_F process_charn)
        thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(s @ t @ [a], {}) ∈ ?f6›
        hence ‹(s, {}) ∈ ?f3›
          by simp (meson front_tickFree_mono is_processT snoc_eq_iff_butlast)
        thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
      next
        assume ‹(s @ t @ [a], {}) ∈ ?f7›
        then obtain t1 t2 where * : ‹s @ t @ [a] = t1 @ t2› ‹t1 ∈ 𝒯 P›
                                    ‹tickFree t1› ‹t2 ∈ 𝒟 Q› by blast
        hence ‹(s @ t, {}) ∈ (if length t2 ≤ 1 then ?f3 else ?f4)›
          apply (cases t2 rule: rev_cases; simp)
          by (metis T_F append_assoc process_charn tickFree_append)
             (metis D_T T_F is_processT3_ST)
        thus ‹(s, {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
          by (intro hyp) (meson UnI1 UnI2)
      qed
    qed
  next
    fix s X Y
    assume assm : ‹(s, Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ∧ X ⊆ Y›
    hence ‹(s, Y) ∈ ?f1 ∨ (s, Y) ∈ ?f2 ∨ (s, Y) ∈ ?f3 ∨ (s, Y) ∈ ?f4 ∨
           (s, Y) ∈ ?f5 ∨ (s, Y) ∈ ?f6 ∨ (s, Y) ∈ ?f7› by fast
    thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (elim disjE)
      assume ‹(s, Y) ∈ ?f1›
      hence ‹(s, X) ∈ ?f1› by simp
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, Y) ∈ ?f2›
      with assm[THEN conjunct2] have ‹(s, X) ∈ ?f2› by simp blast
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, Y) ∈ ?f3›
      with assm[THEN conjunct2] is_processT4 have ‹(s, X) ∈ ?f3› by simp blast
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, Y) ∈ ?f4›
      with assm[THEN conjunct2] is_processT4 have ‹(s, X) ∈ ?f4› by simp blast
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, Y) ∈ ?f5›
      with assm[THEN conjunct2] have ‹(s, X) ∈ ?f5› by simp blast
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, Y) ∈ ?f6›
      hence ‹(s, X) ∈ ?f6› by simp
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, Y) ∈ ?f7›
      hence ‹(s, X) ∈ ?f7› by simp
      thus ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    qed
  next
    fix s X Y
    assume assm : ‹(s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7 ∧
                   (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7)›
    have ‹(s, X) ∈ ?f1 ∨ (s, X) ∈ ?f2 ∨ (s, X) ∈ ?f3 ∨ (s, X) ∈ ?f4 ∨
          (s, X) ∈ ?f5 ∨ (s, X) ∈ ?f6 ∨ (s, X) ∈ ?f7› using assm[THEN conjunct1] by fast
    thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (elim disjE)
      assume ‹(s, X) ∈ ?f1›
      hence ‹(s, X ∪ Y) ∈ ?f1› by simp
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, X) ∈ ?f2›
      with assm[THEN conjunct2] have ‹(s, X ∪ Y) ∈ ?f2› by simp blast
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, X) ∈ ?f3›
      with assm[THEN conjunct2] have ‹(s, X ∪ Y) ∈ ?f3›
        by simp (metis F_T T_F append_Nil is_processT5_S7' list.distinct(1))
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, X) ∈ ?f4›
      with assm[THEN conjunct2] have ‹(s, X ∪ Y) ∈ ?f4›
        by simp (metis append.assoc append_is_Nil_conv is_processT5_S1)
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, X) ∈ ?f5›
      with assm[THEN conjunct2] have ‹(s, X ∪ Y) ∈ ?f5›
        by simp (metis Diff_empty Diff_insert0 T_F Un_Diff not_Cons_self)
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, X) ∈ ?f6›
      hence ‹(s, X ∪ Y) ∈ ?f6› by simp
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s, X) ∈ ?f7›
      hence ‹(s, X ∪ Y) ∈ ?f7› by simp
      thus ‹(s, X ∪ Y) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    qed
  next
    fix s X
    have * : ‹(s @ [tick], {}) ∉ ?f2 ∪ ?f3 ∪ ?f5›
      by simp (metis Cons_eq_appendI append_self_conv2 front_tickFree_mono 
                     is_processT2_TR list.distinct(1) non_tickFree_tick)
    assume ‹(s @ [tick], {}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    with "*" have ‹(s @ [tick], {}) ∈ ?f1 ∨ (s @ [tick], {}) ∈ ?f4 ∨
                   (s @ [tick], {}) ∈ ?f6 ∨ (s @ [tick], {}) ∈ ?f7› by fast
    thus ‹(s, X - {tick}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7›
    proof (elim disjE)
      assume ‹(s @ [tick], {}) ∈ ?f1›
      hence ‹(s, X - {tick}) ∈ ?f2› by blast
      thus ‹(s, X - {tick}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s @ [tick], {}) ∈ ?f4›
      then obtain t1 t2
        where ** : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹tickFree t1› ‹(t2 @ [tick], {}) ∈ ℱ Q› 
        by simp (metis butlast_append last_appendR snoc_eq_iff_butlast)
      hence ‹(s, X - {tick}) ∈ (if t2 = [] then ?f5 else ?f4)›
        by simp (metis F_T process_charn self_append_conv2)
      thus ‹(s, X - {tick}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by (meson UnCI)
    next
      assume ‹(s @ [tick], {}) ∈ ?f6›
      with is_processT9 have ‹s ∈ 𝒟 P› by simp blast
      thus ‹(s, X - {tick}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    next
      assume ‹(s @ [tick], {}) ∈ ?f7›
      then obtain t1 t2 where ** : ‹s @ [tick] = t1 @ t2› ‹t1 ∈ 𝒯 P›
                                   ‹tickFree t1› ‹t2 ∈ 𝒟 Q› by blast
      from "**"(1, 3, 4) obtain t2' where ‹t2 = t2' @ [tick]› ‹t2' @ [tick] ∈ 𝒟 Q›
        by (cases t2 rule: rev_cases) auto
      with "**"(1) is_processT9 have ‹s = t1 @ t2' ∧ t2' ∈ 𝒟 Q› by simp blast
      with "**"(2, 3) have ‹(s, X - {tick}) ∈ ?f7› by simp blast
      thus ‹(s, X - {tick}) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› by blast
    qed
  next
    show ‹s ∈ ?d1 ∪ ?d2 ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ ?d1 ∪ ?d2› for s t
      apply (simp, elim conjE disjE exE)
      by (solves ‹simp add: is_processT7›)      
         (meson append.assoc is_processT7 tickFree_append)
  next
    show ‹s ∈ ?d1 ∪ ?d2 ⟹ (s, X) ∈ ?f1 ∪ ?f2 ∪ ?f3 ∪ ?f4 ∪ ?f5 ∪ ?f6 ∪ ?f7› for s X
      by blast
  next
    fix s
    assume ‹s @ [tick] ∈ ?d1 ∪ ?d2›
    then consider ‹s @ [tick] ∈ ?d1› | ‹s @ [tick] ∈ ?d2› by blast
    thus ‹s ∈ ?d1 ∪ ?d2›
    proof cases
      assume ‹s @ [tick] ∈ ?d1›
      with is_processT have ‹s ∈ ?d1› by blast
      thus ‹s ∈ ?d1 ∪ ?d2› by blast
    next
      assume ‹s @ [tick] ∈ ?d2›
      then obtain t1 t2 where ** : ‹s @ [tick] = t1 @ t2› ‹t1 ∈ 𝒯 P›
                                   ‹tickFree t1› ‹t2 ∈ 𝒟 Q› by blast
      from "**"(1, 3, 4) obtain t2' where ‹t2 = t2' @ [tick]› ‹t2' @ [tick] ∈ 𝒟 Q›
        by (cases t2 rule: rev_cases) auto
      with "**"(1) is_processT9 have ‹s = t1 @ t2' ∧ t2' ∈ 𝒟 Q› by simp blast
      with "**"(2, 3) have ‹s ∈ ?d2› by simp blast
      thus ‹s ∈ ?d1 ∪ ?d2› by blast
    qed
  qed
qed



subsection ‹Projections›

lemma F_Interrupt :
  ‹ℱ (P △ Q) = 
   {(t1 @ [tick], X)| t1 X. t1 @ [tick] ∈ 𝒯 P} ∪
   {(t1, X - {tick})| t1 X. t1 @ [tick] ∈ 𝒯 P} ∪
   {(t1, X) ∈ ℱ P. tickFree t1 ∧ ([], X) ∈ ℱ Q} ∪
   {(t1 @ t2, X)| t1 t2 X. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []} ∪
   {(t1, X - {tick})| t1 X. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ [tick] ∈ 𝒯 Q} ∪
   {(t1, X). t1 ∈ 𝒟 P} ∪ 
   {(t1 @ t2, X)| t1 t2 X. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q}›
  by (simp add: Failures_def FAILURES_def Interrupt.rep_eq)
  (* by (simp add: Failures.rep_eq FAILURES_def Interrupt.rep_eq) *)

lemma D_Interrupt : 
  ‹𝒟 (P △ Q) = 𝒟 P ∪ {t1 @ t2| t1 t2. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q}›
  by (simp add: Divergences_def DIVERGENCES_def Interrupt.rep_eq)
  (* by (simp add: Divergences.rep_eq DIVERGENCES_def Interrupt.rep_eq) *)

lemma T_Interrupt : 
  ‹𝒯 (P △ Q) = 𝒯 P ∪ {t1 @ t2| t1 t2. t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒯 Q}›
  apply (simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Interrupt)
  apply (safe, simp_all add: is_processT8)
  subgoal by (metis is_processT3_SR)
  subgoal by auto
  subgoal by auto
  subgoal by (metis is_processT8_S)
  subgoal by (metis is_processT4_empty nonTickFree_n_frontTickFree process_charn)
  by (metis append.right_neutral is_processT4_empty tickFree_Nil)
  



subsection ‹Monotony›

lemma mono_Interrupt[simp]: ‹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 that[THEN le_approx1] D_T that(1)[THEN le_approx2T]
    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 Ra_def F_Interrupt,
           intro subset_antisym subsetI; simp, elim disjE)
    subgoal by (metis le_approx2T that(1))
    subgoal by (metis is_processT9 le_approx2T that(1))
    subgoal by (metis F_T append.right_neutral le_approx2 that)
    subgoal by (metis is_processT2 is_processT7 le_approx2T proc_ord2a that)
    subgoal by (metis (no_types, lifting) append_Nil2 le_approx2T min_elems6
          no_Trace_implies_no_Failure self_append_conv2 that)
    subgoal by metis
    subgoal by (metis le_approx2T that(1))
    subgoal by (metis le_approx_lemma_T subset_eq that(1))
    subgoal by (metis is_processT8_S le_approx2 that)
    subgoal by (metis is_processT2 is_processT7_S le_approx2 le_approx2T that) 
    subgoal by (metis D_T le_approx2T that)
    subgoal by (metis in_mono le_approx1 that(1))
    by (metis le_approx1 le_approx2T process_charn subsetD that)
next
  from that[THEN le_approx3]
  show ‹s ∈ min_elems (𝒟 (P △ Q)) ⟹ s ∈ 𝒯 (P' △ Q')› for s
    by (auto simp add: min_elems_def D_Interrupt T_Interrupt subset_iff)
       (metis le_approx2T le_list_def less_append order_le_imp_less_or_eq that(1))
qed


lemma mono_Interrupt_T: ‹P ⊑⇩T P' ⟹ Q ⊑⇩T Q' ⟹ P △ Q ⊑⇩T P' △ Q'›
  unfolding trace_refine_def by (auto simp add: T_Interrupt)

lemma mono_right_Interrupt_D: ‹Q ⊑⇩D Q' ⟹ P △ Q ⊑⇩D P △ Q'›
  unfolding divergence_refine_def by (auto simp add: D_Interrupt) 

―‹We have no monotony, even partial, with \<^term>‹(⊑⇩F)›.›

lemma mono_Interrupt_FD:
  ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P △ Q ⊑⇩F⇩D P' △ Q'›
  unfolding failure_divergence_refine_def le_ref_def
  by (simp add: D_Interrupt F_Interrupt, safe;
      metis [[metis_verbose = false]] F_subset_imp_T_subset subsetD)

lemma mono_Interrupt_DT:
  ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P △ Q ⊑⇩D⇩T P' △ Q'›
  unfolding trace_divergence_refine_def trace_refine_def divergence_refine_def
  by (auto simp add: T_Interrupt D_Interrupt subset_iff)



subsection ‹Properties›


lemma Interrupt_STOP_neutral : ‹P △ STOP = P› ‹STOP △ P = P›
   apply (all ‹subst Process_eq_spec›, safe)
         apply (simp_all add: Process_eq_spec F_Interrupt D_Interrupt F_STOP T_STOP
      D_STOP T_F is_processT6 is_processT8_S tick_T_F)
  subgoal by (meson process_charn tick_T_F)
  subgoal by (metis F_T T_nonTickFree_imp_decomp)
  subgoal by (meson DiffE insertI1 is_processT6_S2 is_processT8_S)
  by blast

lemma Interrupt_BOT_absorb : ‹P △ ⊥ = ⊥› ‹⊥ △ P = ⊥›
  by (simp_all add: BOT_iff_D D_Interrupt D_UU Nil_elem_T)

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


lemma events_Interrupt: ‹events_of (P △ Q) = events_of P ∪ events_of Q›
  apply (intro subset_antisym subsetI; simp add: events_of_def T_Interrupt)
  by (metis UnE set_append) (metis Nil_elem_T append_Nil tickFree_Nil)


lemma Interrupt_Ndet_distrib : ‹P △ Q1 ⊓ Q2 = (P △ Q1) ⊓ (P △ Q2)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Interrupt D_Ndet)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Interrupt D_Ndet)
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 (P △ Q1 ⊓ Q2)›
    | ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P›
    | ‹s @ [tick] ∈ 𝒯 P ∧ tick ∉ X›
    | ‹(s, X) ∈ ℱ P ∧ tickFree s ∧ ([], X) ∈ ℱ (Q1 ⊓ Q2)›
    | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ (Q1 ⊓ Q2) ∧ t2 ≠ []›
    | ‹s ∈ 𝒯 P ∧ tickFree s ∧ [tick] ∈ 𝒯 (Q1 ⊓ Q2) ∧ tick ∉ X›
    by (simp add: F_Interrupt 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. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Ndet F_Interrupt)
  next
    show ‹s @ [tick] ∈ 𝒯 P ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Ndet F_Interrupt) (metis Diff_insert_absorb)
  next
    show ‹(s, X) ∈ ℱ P ∧ tickFree s ∧ ([], X) ∈ ℱ (Q1 ⊓ Q2) ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Ndet F_Interrupt) blast
  next
    show ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ 
                  (t2, X) ∈ ℱ (Q1 ⊓ Q2) ∧ t2 ≠ [] ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Ndet F_Interrupt) metis
  next
    show ‹s ∈ 𝒯 P ∧ tickFree s ∧ [tick] ∈ 𝒯 (Q1 ⊓ Q2) ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Interrupt F_Ndet T_Ndet) (metis Diff_insert_absorb)
  qed
next
  have ‹(s, X) ∈ ℱ (P △ Q1) ⟹ (s, X) ∈ ℱ (P △ Q1 ⊓ Q2)› for s X Q1 Q2
    by (simp add: F_Interrupt F_Ndet D_Ndet T_Ndet) blast
  thus ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (simp add: F_Ndet) (metis Ndet_commute)
qed


lemma Ndet_Interrupt_distrib : ‹P1 ⊓ P2 △ Q = (P1 △ Q) ⊓ (P2 △ Q)›
  (is ‹?lhs = ?rhs›) 
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (auto simp add: D_Ndet T_Ndet D_Interrupt)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Ndet T_Ndet D_Interrupt)
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs›
    | ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (P1 ⊓ P2)›
    | ‹s @ [tick] ∈ 𝒯 (P1 ⊓ P2) ∧ tick ∉ X›
    | ‹(s, X) ∈ ℱ (P1 ⊓ P2) ∧ tickFree s ∧ ([], X) ∈ ℱ Q›
    | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P1 ⊓ P2) ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []›
    | ‹s ∈ 𝒯 (P1 ⊓ P2) ∧ tickFree s ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X›
    by (simp add: F_Interrupt 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. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (P1 ⊓ P2) ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: T_Ndet F_Ndet F_Interrupt) metis
  next
    show ‹s @ [tick] ∈ 𝒯 (P1 ⊓ P2) ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: T_Ndet F_Ndet F_Interrupt) (metis Diff_insert_absorb)
  next
    show ‹(s, X) ∈ ℱ (P1 ⊓ P2) ∧ tickFree s ∧ ([], X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Ndet F_Interrupt) blast
  next
    show ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P1 ⊓ P2) ∧ tickFree t1 ∧
                  (t2, X) ∈ ℱ Q ∧ t2 ≠ [] ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: T_Ndet F_Ndet F_Interrupt) metis
  next
    show ‹s ∈ 𝒯 (P1 ⊓ P2) ∧ tickFree s ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: T_Ndet F_Ndet F_Interrupt) (metis Diff_insert_absorb)
  qed
next
  have ‹(s, X) ∈ ℱ (P1 △ Q) ⟹ (s, X) ∈ ℱ (P1 ⊓ P2 △ Q)› for s X P1 P2
    by (simp add: F_Interrupt F_Ndet D_Ndet T_Ndet) blast
  thus ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (simp add: F_Ndet) (metis Ndet_commute)
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)
      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)
      qed
    qed
  next
    fix s X
    assume same_div: ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹s ∈ 𝒟 ?lhs›
      | ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P›
      | ‹s @ [tick] ∈ 𝒯 P ∧ tick ∉ X›
      | ‹(s, X) ∈ ℱ P ∧ tickFree s ∧ ([], X) ∈ ℱ (Q △ R)›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ (Q △ R) ∧ t2 ≠ []›
      | ‹s ∈ 𝒯 P ∧ tickFree s ∧ [tick] ∈ 𝒯 (Q △ R) ∧ tick ∉ 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. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Interrupt T_Interrupt)
    next
      show ‹s @ [tick] ∈ 𝒯 P ∧ tick ∉ 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 ‹[tick] ∈ 𝒯 Q ∧ tick ∉ X›
        | ‹([], X) ∈ ℱ Q ∧ ([], X) ∈ ℱ R›
        | ‹[] ∈ 𝒯 Q ∧ [tick] ∈ 𝒯 R ∧ tick ∉ X›
        by (simp add: F_Interrupt Nil_elem_T BOT_iff_D) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        show ‹[tick] ∈ 𝒯 Q ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
          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 ∧ [tick] ∈ 𝒯 R ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
          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. t2 = u1 @ [tick] ∧ u1 @ [tick] ∈ 𝒯 Q›
        | ‹t2 @ [tick] ∈ 𝒯 Q ∧ tick ∉ X›
        | ‹(t2, X) ∈ ℱ Q ∧ tickFree t2 ∧ ([], X) ∈ ℱ R›
        | ‹∃u1 u2. t2 = u1 @ u2 ∧ u1 ∈ 𝒯 Q ∧ tickFree u1 ∧ (u2, X) ∈ ℱ R ∧ u2 ≠ []›
        | ‹t2 ∈ 𝒯 Q ∧ tickFree t2 ∧ [tick] ∈ 𝒯 R ∧ tick ∉ 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 ‹∃u1. t2 = u1 @ [tick] ∧ u1 @ [tick] ∈ 𝒯 Q ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Interrupt T_Interrupt) (metis append_assoc)
      next
        from "*"(1, 2, 3) show ‹t2 @ [tick] ∈ 𝒯 Q ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
          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 ‹∃u1 u2. t2 = u1 @ u2 ∧ u1 ∈ 𝒯 Q ∧ tickFree u1 ∧
                                        (u2, X) ∈ ℱ R ∧ u2 ≠ [] ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Interrupt T_Interrupt)
             (metis (mono_tags, lifting) append_assoc tickFree_append)
      next
        from "*"(1, 2, 3) show ‹t2 ∈ 𝒯 Q ∧ tickFree t2 ∧ [tick] ∈ 𝒯 R ∧ 
                                tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      qed
    next
      show ‹s ∈ 𝒯 P ∧ tickFree s ∧ [tick] ∈ 𝒯 (Q △ R) ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: F_Interrupt T_Interrupt)
           (metis Diff_insert_absorb append_Nil hd_append2 hd_in_set list.sel(1) tickFree_def)
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›
    then consider ‹s ∈ 𝒟 ?rhs›
      | ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (P △ Q)›
      | ‹s @ [tick] ∈ 𝒯 (P △ Q) ∧ tick ∉ X›
      | ‹(s, X) ∈ ℱ (P △ Q) ∧ tickFree s ∧ ([], X) ∈ ℱ R›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (P △ Q) ∧ tickFree t1 ∧ (t2, X) ∈ ℱ R ∧ t2 ≠ []›
      | ‹s ∈ 𝒯 (P △ Q) ∧ tickFree s ∧ [tick] ∈ 𝒯 R ∧ tick ∉ 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. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (P △ Q) ⟹ (s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt T_Interrupt)
           (metis last_append self_append_conv snoc_eq_iff_butlast)
    next
      assume assm : ‹s @ [tick] ∈ 𝒯 (P △ Q) ∧ tick ∉ X›
      from assm[THEN conjunct1] consider ‹s @ [tick] ∈ 𝒯 P›
        | ‹∃t1 t2. s @ [tick] = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒯 Q›
        by (simp add: T_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        show ‹s @ [tick] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt) (metis Diff_insert_absorb assm[THEN conjunct2])
      next
        show ‹∃t1 t2. s @ [tick] = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧
                      tickFree t1 ∧ t2 ∈ 𝒯 Q ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt T_Interrupt)
             (metis Diff_insert_absorb T_nonTickFree_imp_decomp
                    append.right_neutral append_Nil assm[THEN conjunct2]
                    butlast.simps(2) butlast_append non_tickFree_tick tickFree_append)
      qed
    next
      assume assm : ‹(s, X) ∈ ℱ (P △ Q) ∧ tickFree s ∧ ([], X) ∈ ℱ R›
      from assm[THEN conjunct1] consider ‹s ∈ 𝒟 (P △ Q)›
        | ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P›
        | ‹s @ [tick] ∈ 𝒯 P ∧ tick ∉ X›
        | ‹(s, X) ∈ ℱ P ∧ tickFree s ∧ ([], X) ∈ ℱ Q›
        | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []›
        | ‹s ∈ 𝒯 P ∧ tickFree s ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ 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 ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt)
      next
        show ‹s @ [tick] ∈ 𝒯 P ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?lhs›
          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 ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧
                      (t2, X) ∈ ℱ Q ∧ t2 ≠ [] ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt) (metis assm[THEN conjunct2] tickFree_append)
      next
        show ‹s ∈ 𝒯 P ∧ tickFree s ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?lhs›
          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 ‹s ∈ 𝒯 (P △ Q) ∧ tickFree s ∧ [tick] ∈ 𝒯 R ∧ tick ∉ 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)
    qed
  qed

  thus ‹?lhs = ?rhs›
    apply (cases ‹P = ⊥›, solves ‹simp add: Interrupt_BOT_absorb›)
    apply (cases ‹Q = ⊥›, solves ‹simp add: Interrupt_BOT_absorb›)
    apply (cases ‹R = ⊥›, solves ‹simp add: Interrupt_BOT_absorb›)
    by blast
qed



subsection ‹Key Property›


lemma Interrupt_Mprefix:
  ‹(□a ∈ A → P a) △ Q = Q □ (□a ∈ A → P a △ Q)› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then consider ‹s ∈ 𝒟 (□a ∈ A → P a)›
    | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (□a ∈ A → P a) ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q›
    by (simp add: D_Interrupt) blast
  thus ‹s ∈ 𝒟 ?rhs›
  proof cases
    show ‹s ∈ 𝒟 (□a ∈ A → P a) ⟹ s ∈ 𝒟 ?rhs›
      by (simp add: D_Det D_Mprefix D_Interrupt) blast
  next
    assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (□a ∈ A → P a) ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q›
    then obtain t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (□a ∈ A → P a)›
                            ‹tickFree t1› ‹t2 ∈ 𝒟 Q› by blast
    thus ‹s ∈ 𝒟 ?rhs›
      by (simp add: D_Det D_Mprefix T_Mprefix D_Interrupt)
         (metis (no_types, opaque_lifting) hd_append2 imageI
                self_append_conv2 tickFree_tl tl_append2)
  qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then consider ‹s ∈ 𝒟 Q› | ‹∃a s'. s = ev a # s' ∧ a ∈ A ∧ s' ∈ 𝒟 (P a △ Q)›
    by (simp add: D_Det D_Mprefix image_iff) (metis event.inject list.exhaust_sel)
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    show ‹s ∈ 𝒟 Q ⟹ s ∈ 𝒟 ?lhs›
      apply (simp add: D_Interrupt)
      using Nil_elem_T tickFree_Nil by blast
  next
    assume ‹∃a s'. s = ev a # s' ∧ a ∈ A ∧ s' ∈ 𝒟 (P a △ Q)›
    then obtain a s'
      where * : ‹s = ev a # s'› ‹a ∈ A›
                ‹s' ∈ 𝒟 (P a) ∨ (∃t1 t2. s' = t1 @ t2 ∧ t1 ∈ 𝒯 (P a) ∧ 
                                          tickFree t1 ∧ t2 ∈ 𝒟 Q)›
      by (simp add: D_Interrupt) blast
    from "*"(3) show ‹s ∈ 𝒟 ?lhs›
      apply (elim disjE exE)
      subgoal by (solves ‹simp add: "*"(1, 2) D_Interrupt D_Mprefix image_iff›)
      by (simp add: "*"(1) D_Interrupt T_Mprefix)
         (metis "*"(2) Cons_eq_appendI event.distinct(1) list.sel(1, 3) tickFree_Cons)
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs› 
    | ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (Mprefix A P)›
    | ‹s @ [tick] ∈ 𝒯 (Mprefix A P) ∧ tick ∉ X›
    | ‹(s, X) ∈ ℱ (Mprefix A P) ∧ tickFree s ∧ ([], X) ∈ ℱ Q›
    | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Mprefix A P) ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []›
    | ‹s ∈ 𝒯 (Mprefix A P) ∧ tickFree s ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X›
    by (simp add: F_Interrupt D_Interrupt) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from D_F same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    show ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (Mprefix A P) ⟹ (s, X) ∈ ℱ ?rhs› 
      by (elim exE, simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
         (metis event.distinct(1) hd_append list.sel(1) tl_append2)
  next
    show ‹s @ [tick] ∈ 𝒯 (Mprefix A P) ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
         (metis Diff_insert_absorb event.simps(3) hd_append list.sel(1) tl_append_if)
  next
    show ‹(s, X) ∈ ℱ (Mprefix A P) ∧ tickFree s ∧ ([], X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Det F_Mprefix F_Interrupt image_iff) (metis tickFree_tl)
  next
    show ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Mprefix A P) ∧
                  tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ [] ⟹ (s, X) ∈ ℱ ?rhs›
      by (elim exE, simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
         (metis hd_append2 self_append_conv2 tickFree_tl tl_append2)
  next
    show ‹s ∈ 𝒯 (Mprefix A P) ∧ tickFree s ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
         (metis Diff_insert_absorb tickFree_tl)
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume assm : ‹(s, X) ∈ ℱ ?rhs›
  show ‹(s, X) ∈ ℱ ?lhs›
  proof (cases ‹s = []›)
    from assm show ‹s = [] ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: F_Det F_Mprefix F_Interrupt Nil_elem_T) blast
  next 
    assume ‹s ≠ []›
    with assm consider ‹(s, X) ∈ ℱ Q›
      | ‹∃a s'. s = ev a # s' ∧ a ∈ A ∧ (s', X) ∈ ℱ (P a △ Q)›
      by (simp add: F_Det F_Mprefix image_iff) (metis event.inject list.exhaust_sel)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      show ‹(s, X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt)
           (metis Nil_elem_T ‹s ≠ []› append_Nil tickFree_Nil)
    next
      assume ‹∃a s'. s = ev a # s' ∧ a ∈ A ∧ (s', X) ∈ ℱ (P a △ Q)›
      then obtain a s'
        where * : ‹s = ev a # s'› ‹a ∈ A› ‹(s', X) ∈ ℱ (P a △ Q)› by blast
      from "*"(3) consider ‹s' ∈ 𝒟 (P a △ Q)›
        | ‹∃t1. s' = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (P a)›
        | ‹s' @ [tick] ∈ 𝒯 (P a) ∧ tick ∉ X›
        | ‹(s', X) ∈ ℱ (P a) ∧ tickFree s' ∧ ([], X) ∈ ℱ Q›
        | ‹∃t1 t2. s' = t1 @ t2 ∧ t1 ∈ 𝒯 (P a) ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []›
        | ‹s' ∈ 𝒯 (P a) ∧ tickFree s' ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X›
        by (simp add: F_Interrupt D_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (P a △ Q)›
        hence ‹s ∈ 𝒟 ?lhs›
          by (simp add: D_Interrupt D_Mprefix T_Mprefix "*"(1, 2) image_iff)
             (metis "*"(2) append_Cons event.distinct(1) list.sel(1, 3) tickFree_Cons)
        with D_F same_div show ‹(s, X) ∈ ℱ ?lhs› by blast 
      next
        show ‹∃t1. s' = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (P a) ⟹ (s, X) ∈ ℱ ?lhs›
          by (elim exE, simp add: "*"(1, 2) F_Interrupt T_Mprefix)
      next
        show ‹s' @ [tick] ∈ 𝒯 (P a) ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: "*"(1, 2) F_Interrupt T_Mprefix) blast
      next
        show ‹(s', X) ∈ ℱ (P a) ∧ tickFree s' ∧ ([], X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: "*"(1, 2) F_Interrupt F_Mprefix)
      next
        show ‹∃t1 t2. s' = t1 @ t2 ∧ t1 ∈ 𝒯 (P a) ∧ tickFree t1 ∧
                      (t2, X) ∈ ℱ Q ∧ t2 ≠ [] ⟹ (s, X) ∈ ℱ ?lhs›
          by (elim exE, simp add: F_Interrupt T_Mprefix "*"(1))
             (metis "*"(2) Cons_eq_appendI event.distinct(1) list.sel(1, 3) tickFree_Cons)
      next
        show ‹s' ∈ 𝒯 (P a) ∧ tickFree s' ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt T_Mprefix "*"(1, 2) image_iff) blast
      qed
    qed
  qed
qed


corollary ‹(□a ∈ A → P a) △ (□b ∈ B → Q b) = 
   □x ∈ A ∪ B → (     if x ∈ A ∩ B then (P x △ (□b ∈ B → Q b)) ⊓ Q x
                   else if   x ∈ A   then  P x △ (□b ∈ B → Q b)
                   else                     Q x)›
  apply (subst Interrupt_Mprefix, subst Mprefix_Det_distr)
  by (metis Det_commute Mprefix_Det_distr)


subsection ‹Continuity›

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

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


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, safe)
 show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
   by (simp add: limproc_is_thelub chain chain_left_Interrupt
                 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_left_Interrupt chain)
  hence ‹∀i. S i ≠ {}› by (simp add: S_def D_Interrupt) blast
  moreover have ‹finite (S 0)›
    unfolding S_def
    apply (rule finite_subset[of _ ‹{t1. ∃t2. s = t1 @ t2}›], blast)
    by (metis prefixes_fin)
  moreover have ‹∀i. S (Suc i) ⊆ S i›
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    by (metis in_mono le_approx1 po_class.chainE chain)
       (metis le_approx_lemma_T po_class.chain_def subset_eq chain)
  ultimately have ‹(⋂i. S i) ≠ {}›
    by (rule Inter_nonempty_finite_chained_sets)
  then obtain t1 where * : ‹∀i. t1 ∈ S i›
    by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
  show ‹s ∈ 𝒟 ?lhs›
  proof (cases ‹∀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_left_Interrupt
                  F_Interrupt F_LUB T_LUB D_LUB) blast
next
  fix s X
  define S
    where ‹S i ≡ {t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (Y i)} ∪
                 {t1. s = t1 ∧ t1 @ [tick] ∈ 𝒯 (Y i) ∧ tick ∉ X} ∪
                 {t1. s = t1 ∧ (t1, X) ∈ ℱ (Y i) ∧ tickFree t1 ∧ ([], X) ∈ ℱ Q} ∪
                 {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Y i) ∧ tickFree t1 ∧ (t2, X) ∈ ℱ Q ∧ t2 ≠ []} ∪
                 {t1. s = t1 ∧ t1 ∈ 𝒯 (Y i) ∧ tickFree t1 ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X} ∪
                 {t1. s = t1 ∧ t1 ∈ 𝒟 (Y i)} ∪
                 {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Y i) ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q}› for i
  assume ‹(s, X) ∈ ℱ ?rhs›
  hence ‹(s, X) ∈ ℱ (Y i △ Q)› for i
    by (simp add: limproc_is_thelub F_LUB chain_left_Interrupt chain)
  hence ‹∀i. S i ≠ {}› by (simp add: S_def F_Interrupt, safe; simp, blast)
  moreover have ‹finite (S 0)›
    unfolding S_def
    apply (intro finite_UnI)
    apply (all ‹rule finite_subset[of _ ‹{t1. ∃t2. s = t1 @ t2}›], blast›)
    by (metis prefixes_fin)+
  moreover have ‹∀i. S (Suc i) ⊆ S i› (* Try to improve this. *)
    unfolding S_def apply (intro allI Un_mono subsetI; simp)
    subgoal using D_T le_approx2T po_class.chain_def chain by blast
    subgoal using D_T le_approx2T po_class.chain_def chain by blast
    subgoal using is_processT8_S le_approx2 po_class.chainE chain by blast
    subgoal by (metis NT_ND le_approx2T po_class.chainE chain) 
    subgoal using D_T le_approx2T po_class.chain_def chain by blast 
    subgoal by (meson in_mono le_approx1 po_class.chainE chain)
    by (metis NT_ND le_approx2T po_class.chainE chain)
  ultimately have ‹(⋂i. S i) ≠ {}›
    by (rule Inter_nonempty_finite_chained_sets)
  then obtain t1 where * : ‹∀i. t1 ∈ S i› 
    by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
  show ‹(s, X) ∈ ℱ ?lhs›
  proof (cases ‹∃j t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Y j) ∧ tickFree t1 ∧ t2 ∈ 𝒟 Q›)
    case True1 : True
    then obtain j t2 where ** : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (Y j)›
                                ‹tickFree t1› ‹t2 ∈ 𝒟 Q› by blast
    from "*" F_T NT_ND is_processT3_ST have ‹∀i. t1 ∈ 𝒯 (Y i)›
      by (simp add: S_def) blast
    with "**"(1, 3, 4) show ‹(s, X) ∈ ℱ ?lhs›
      by (simp add: F_Interrupt limproc_is_thelub chain T_LUB) blast
  next
    case False1 : False
    show ‹(s, X) ∈ ℱ ?lhs›
    proof (cases ‹∃j t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (Y j) ∧ tickFree t1 ∧
                         (t2, X) ∈ ℱ Q ∧ t2 ≠ []›)
      case True2 : True
      then obtain j t2 where ** : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (Y j)› ‹tickFree t1›
                                  ‹(t2, X) ∈ ℱ Q› ‹t2 ≠ []› by blast
      from "*" F_T NT_ND is_processT3_ST have ‹∀i. t1 ∈ 𝒯 (Y i)›
        by (simp add: S_def) blast
      with "**"(1, 3, 4, 5) False1 show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt limproc_is_thelub chain T_LUB) blast
    next
      case False2: False
      show ‹(s, X) ∈ ℱ ?lhs›
      proof (cases ‹∃j. s = t1 ∧ t1 ∈ 𝒯 (Y j) ∧ tickFree t1 ∧ [tick] ∈ 𝒯 Q ∧ tick ∉ X›)
        case True3 : True
        then obtain j where ** : ‹s = t1› ‹t1 ∈ 𝒯 (Y j)› ‹tickFree t1›
                                 ‹[tick] ∈ 𝒯 Q› ‹tick ∉ X› by blast
        from "*" F_T NT_ND is_processT3_ST have ‹∀i. t1 ∈ 𝒯 (Y i)›
          by (simp add: S_def) blast
        with "**"(1, 3, 4, 5) False1 show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt limproc_is_thelub chain T_LUB) blast
      next
        case False3: False
        show ‹(s, X) ∈ ℱ ?lhs›
        proof (cases ‹∃j. s = t1 ∧ (t1, X) ∈ ℱ (Y j) ∧ tickFree t1 ∧ ([], X) ∈ ℱ Q›)
          case True4 : True
          then obtain j where ** : ‹s = t1› ‹(t1, X) ∈ ℱ (Y j)› ‹tickFree t1› ‹([], X) ∈ ℱ Q› by blast
          have ‹(t1, X) ∈ ℱ (Y i)› for i
            using "*"[rule_format, of i] apply (simp add: S_def "**"(1), elim disjE)
            subgoal by (solves ‹simp add: T_F_spec is_processT6_S1›)
            subgoal by (solves ‹simp add: T_F_spec is_processT6_S1›)
            subgoal using "**"(1) False3 by blast
            subgoal by (solves ‹simp add: is_processT8›)
            using "**"(1) False1 by blast
          with "**"(1, 3, 4) show ‹(s, X) ∈ ℱ ?lhs›
            by (simp add: F_Interrupt limproc_is_thelub chain F_LUB)
        next
          case False4: False
          show ‹(s, X) ∈ ℱ ?lhs›
          proof (cases ‹∃j. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 (Y j)›)
            case True5 : True
            then obtain j where ** : ‹s = t1 @ [tick]› ‹t1 @ [tick] ∈ 𝒯 (Y j)› by blast
            from "*" False1 False2 have ‹∀i. t1 @ [tick] ∈ 𝒯 (Y i)›
              by (auto simp add: S_def "**"(1))
            with "**"(1) show ‹(s, X) ∈ ℱ ?lhs›
              by (simp add: F_Interrupt limproc_is_thelub chain T_LUB)
          next
            case False5 : False
            show ‹(s, X) ∈ ℱ ?lhs›
            proof (cases ‹∃j. s = t1 ∧ t1 @ [tick] ∈ 𝒯 (Y j) ∧ tick ∉ X›)
              case True6 : True
              then obtain j where ** : ‹s = t1› ‹t1 @ [tick] ∈ 𝒯 (Y j)› ‹tick ∉ X› by blast
              have ‹t1 @ [tick] ∈ 𝒯 (Y i)› for i
                using "*"[rule_format, of i] apply (simp add: S_def "**"(1), elim disjE)
                subgoal by (solves simp)
                subgoal using "**"(1) False4 by blast
                subgoal using "**"(1) False3 by blast
                subgoal using "**"(2) D_T front_tickFree_mono is_processT2_TR is_processT7 by blast
                subgoal using "**"(1) False1 by blast
                done
              with "**"(1, 3) show ‹(s, X) ∈ ℱ ?lhs›
                by (simp add: F_Interrupt limproc_is_thelub chain T_LUB)
                   (metis Diff_insert_absorb)
            next
              case False6: False
              have ‹s = t1 ∧ t1 ∈ 𝒟 (Y i)› for i
                using "*"[rule_format, of i] apply (simp add: S_def, elim disjE)
                subgoal using False5 by blast
                subgoal using False6 by blast
                subgoal using False4 by blast
                subgoal using False2 by blast
                subgoal using False3 by blast
                subgoal by (solves simp)
                subgoal using False1 by blast
                done
              thus ‹(s, X) ∈ ℱ ?lhs›
                by (simp add: F_Interrupt limproc_is_thelub chain D_LUB)
            qed
          qed
        qed
      qed
    qed
  qed
qed


lemma cont_right_prem_Interrupt : ‹P △ (⨆ i. Y i) = (⨆ i. P △ Y i)›
  (is ‹?lhs = ?rhs›) if chain : ‹chain Y›
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (simp add: limproc_is_thelub chain chain_right_Interrupt
                  D_Interrupt D_LUB) blast
next
  fix s
  define S where ‹S i ≡ {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ 
                                  tickFree t1 ∧ t2 ∈ 𝒟 (Y i)}› for i
  assume assm : ‹s ∈ 𝒟 ?rhs›
  show ‹s ∈ 𝒟 ?lhs›
  proof (cases ‹s ∈ 𝒟 P›)
    show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 ?lhs› by (simp add: D_Interrupt)
  next
    assume ‹s ∉ 𝒟 P›
    with assm have ‹∀i. S i ≠ {}›
      by (simp add: limproc_is_thelub chain chain_right_Interrupt
                    S_def D_Interrupt D_LUB) blast
    moreover have ‹finite (S 0)›
      unfolding S_def
      apply (rule finite_subset[of _ ‹{t1. ∃t2. s = t1 @ t2}›], blast)
      by (metis prefixes_fin)
    moreover have ‹∀i. S (Suc i) ⊆ S i›
      unfolding S_def apply (intro allI Un_mono subsetI; simp)
      by (metis in_mono le_approx1 po_class.chainE chain)
    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)
    thus ‹s ∈ 𝒟 ?lhs›
      by (simp add: D_Interrupt limproc_is_thelub chain D_LUB S_def) blast
  qed
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (simp add: limproc_is_thelub chain chain_right_Interrupt
                  F_Interrupt F_LUB T_LUB D_LUB) blast
next
  fix s X
  define S
    where ‹S i ≡ {t1. s = t1 ∧ (t1, X) ∈ ℱ P ∧ tickFree t1 ∧ ([], X) ∈ ℱ (Y i)} ∪
                 {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ (t2, X) ∈ ℱ (Y i) ∧ t2 ≠ []} ∪
                 {t1. s = t1 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ [tick] ∈ 𝒯 (Y i) ∧ tick ∉ X} ∪
                 {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 (Y i)}› for i
  assume assm : ‹(s, X) ∈ ℱ ?rhs›
  show ‹(s, X) ∈ ℱ ?lhs›
  proof (cases ‹∃t1. s = t1 @ [tick] ∧ t1 @ [tick] ∈ 𝒯 P ∨
                     s = t1 ∧ t1 @ [tick] ∈ 𝒯 P ∧ tick ∉ X ∨
                     s = t1 ∧ t1 ∈ 𝒟 P›)
    case True
    thus ‹(s, X) ∈ ℱ ?lhs›
      by (simp add: F_Interrupt) (metis Diff_insert_absorb)
  next
    case False
    with assm have ‹∀i. S i ≠ {}›
      by (simp add: limproc_is_thelub chain chain_right_Interrupt
                    S_def F_Interrupt F_LUB) blast
    moreover have ‹finite (S 0)›
      unfolding S_def
      apply (rule finite_subset[of _ ‹{t1. ∃t2. s = t1 @ t2}›], blast)
      by (metis prefixes_fin)
    moreover have ‹∀i. S (Suc i) ⊆ S i›
      unfolding S_def apply (intro allI Un_mono subsetI; simp)
      subgoal by (meson le_approx2 po_class.chainE process_charn chain)
      subgoal by (metis le_approx2 po_class.chainE process_charn chain)
      subgoal by (metis insert_absorb insert_subset le_approx_lemma_T po_class.chainE chain)
      by (metis in_mono le_approx1 po_class.chainE chain)
    ultimately have ‹(⋂i. S i) ≠ {}›
      by (rule Inter_nonempty_finite_chained_sets)
    then obtain t1 where * : ‹∀i. t1 ∈ S i›
      by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
    
    show ‹(s, X) ∈ ℱ ?lhs›
    proof (cases ‹∃j t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧
                         (t2, X) ∈ ℱ (Y j) ∧ t2 ≠ []›)
      case True1 : True
      then obtain j t2
        where ** : ‹s = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹tickFree t1› 
                   ‹(t2, X) ∈ ℱ (Y j)› ‹t2 ≠ []› by blast
      from "*" "**"(1, 5) D_F have ‹∀i. (t2, X) ∈ ℱ (Y i)› by (simp add: S_def) blast
      with "**"(1, 2, 3, 5) show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt limproc_is_thelub chain F_LUB) blast
    next
      case False1: False
      show ‹(s, X) ∈ ℱ ?lhs›
      proof (cases ‹∃j. s = t1 ∧ (t1, X) ∈ ℱ P ∧ tickFree t1 ∧ ([], X) ∈ ℱ (Y j)›)
        case True2 : True
        then obtain j where ** : ‹s = t1› ‹(t1, X) ∈ ℱ P› 
                                 ‹tickFree t1› ‹([], X) ∈ ℱ (Y j)› by blast
        from "*" "**"(1) D_F is_processT6_S2 have ‹∀i. ([], X) ∈ ℱ (Y i)›
          by (simp add: S_def) blast
        with "**"(1, 2, 3) show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Interrupt limproc_is_thelub chain F_LUB)
      next
        case False2: False
        show ‹(s, X) ∈ ℱ ?lhs› 
        proof (cases ‹∃j. s = t1 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧
                          [tick] ∈ 𝒯 (Y j) ∧ tick ∉ X›)
          case True3 : True
          then obtain j where ** : ‹s = t1› ‹t1 ∈ 𝒯 P› ‹tickFree t1›
                                   ‹[tick] ∈ 𝒯 (Y j)› ‹tick ∉ X› by blast
          from "*" "**"(1) False2 have ‹∀i. [tick] ∈ 𝒯 (Y i)›
            by (simp add: S_def) 
              (metis BOT_iff_D D_UU NT_ND front_tickFree_single mem_Collect_eq)
          with "**"(1, 2, 3, 5) show ‹(s, X) ∈ ℱ ?lhs›
            by (simp add: F_Interrupt limproc_is_thelub chain T_LUB) blast
        next
          case False3 : False
          have ‹∃t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 P ∧ tickFree t1 ∧ t2 ∈ 𝒟 (Y i)› for i
            using "*"[rule_format, of i] apply (simp add: S_def, elim disjE)
            using False1 False2 False3 by blast+
           
          thus ‹(s, X) ∈ ℱ ?lhs›
            by (simp add: F_Interrupt limproc_is_thelub chain D_LUB)
               (metis same_append_eq)
        qed
      qed
    qed
  qed
qed
  

lemma Interrupt_cont[simp] : 
  assumes cont_f : ‹cont f› and cont_g : ‹cont g›
  shows ‹cont (λx. f x △ g x)›
proof -
  have * : ‹cont (λy. y △ g x)› for x
    by (rule contI2, rule monofunI, solves simp, simp add: cont_left_prem_Interrupt)
  have ‹⋀y. cont (Interrupt y)›
    by (simp add: contI2 cont_right_prem_Interrupt fun_belowD lub_fun monofunI)
  hence ** : ‹cont (λx. y △ g x)› for y
    by (rule cont_compose) (simp add: cont_g)
  show ?thesis by (fact cont_apply[OF cont_f "*" "**"])
qed


end