Quelle  Interrupt.thy

(*<*)
―‹ ********************************************************************
 * 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"
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_ptick, ('a, 'r) process_ptick] ==> ('a, 'r) process_ptick› (infixl ‹△› 81)
  is ‹λP Q.
 ({(t @ [🍋(r)], X) |t r X. t @ [🍋(r)] ∈ T P} ∪
 {(t, X - {🍋(r)}) |t r X. t @ [🍋(r)] ∈ T P} ∪
 {(t, X). (t, X) ∈ F P ∧ tF t ∧ ([], X) ∈ F Q} ∪
 {(t @ u, X) |t u X. t ∈ T P ∧ tF t ∧ (u, X) ∈ F Q ∧ u ≠ []} ∪
 {(t, X - {🍋(r)}) |t r X. t ∈ T P ∧ tF t ∧ [🍋(r)] ∈ T Q} ∪
 {(t, X). t ∈ D P} ∪
 {(t @ u, X) |t u X. t ∈ T P ∧ tF t ∧ u ∈ D Q},
 D P ∪ {t @ u |t u. t ∈ T P ∧ tF t ∧ u ∈ D 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' ∈ T P› ‹tF t'› ‹(u' @ [a], {}) ∈ F 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' ∈ T P› ‹tF t'› ‹u' ∈ D 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_ptick.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' ∈ T P› ‹tF t'› ‹(u' @ [🍋(r)], {}) ∈ F 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 ∈ D 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' ∈ T P› ‹tF t'› ‹u' ∈ D Q› by blast
      from "**"(1, 3, 4) obtain u'' where ‹u' = u'' @ [🍋(r)]› ‹u'' @ [🍋(r)] ∈ D Q›
        by (cases u' rule: rev_cases) auto
      with "**"(1) is_processT9 have ‹t = t' @ u'' ∧ u'' ∈ D 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' ∈ T P› ‹tF t'› ‹u' ∈ D Q› by blast
      from "**"(1, 3, 4) obtain u'' where ‹u' = u'' @ [🍋(r)]› ‹u'' @ [🍋(r)] ∈ D Q›
        by (cases u' rule: rev_cases) auto
      with "**"(1) is_processT9 have ‹t = t' @ u'' ∧ u'' ∈ D 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 :
  ‹F (P △ Q) =
 {(t @ [🍋(r)], X) |t r X. t @ [🍋(r)] ∈ T P} ∪
 {(t, X - {🍋(r)}) |t r X. t @ [🍋(r)] ∈ T P} ∪
 {(t, X). (t, X) ∈ F P ∧ tF t ∧ ([], X) ∈ F Q} ∪
 {(t @ u, X) |t u X. t ∈ T P ∧ tF t ∧ (u, X) ∈ F Q ∧ u ≠ []} ∪
 {(t, X - {🍋(r)}) |t r X. t ∈ T P ∧ tF t ∧ [🍋(r)] ∈ T Q} ∪
 {(t, X). t ∈ D P} ∪
 {(t @ u, X) |t u X. t ∈ T P ∧ tF t ∧ u ∈ D Q}›
  by (simp add: Failures.rep_eq FAILURES_def Interrupt.rep_eq)

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

lemma T_Interrupt : 
  ‹T (P △ Q) = T P ∪ {t @ u |t u. t ∈ T P ∧ tF t ∧ u ∈ T 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 ∈ D (P' △ Q') ==> s ∈ D (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 ∉ D (P △ Q) ==> R_a (P △ Q) s = R_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 \<open>P \<sqsubseteq> P'\<close>[THEN le_approx3] \<open>Q \<sqsubseteq> Q'\<close>[THEN le_approx3] *)
  show ‹s ∈ min_elems (D (P △ Q)) ==> s ∈ T (P' △ Q')› for s
    apply (rule set_mp[of ‹min_elems (D P) ∪ {t1 @ t2| t1 t2. t1 ∈ T P' ∧ tickFree t1 ∧ t2 ∈ min_elems (D Q)}›])
      (* apply (use \<open>P \<sqsubseteq> P'\<close>[THEN le_approx3] \<open>Q \<sqsubseteq> Q'\<close>[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 ∈ D (P △ STOP) ==> t ∈ D P› for t
    by (simp add: D_Interrupt D_STOP)
next
  show ‹t ∈ D P ==> t ∈ D (P △ STOP)› for t
    by (simp add: D_Interrupt D_STOP)
next
  show ‹(t, X) ∈ F (P △ STOP) ==> (t, X) ∈ F P› for t X
    by (simp add: F_Interrupt STOP_projs)
      (meson is_processT6_TR is_processT8 tick_T_F)
next
  show ‹(t, X) ∈ F P ==> (t, X) ∈ F (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 ∈ D (STOP △ P) ==> t ∈ D P› for t
    by (simp add: D_Interrupt STOP_projs)
next
  show ‹t ∈ D P ==> t ∈ D (STOP △ P)› for t
    by (simp add: D_Interrupt STOP_projs)
next
  show ‹(t, X) ∈ F (STOP △ P) ==> (t, X) ∈ F P› for t X
    by (simp add: F_Interrupt STOP_projs)
      (metis is_processT6_TR is_processT8 self_append_conv2)
next
  show ‹(t, X) ∈ F P ==> (t, X) ∈ F (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 ∈ D (SKIP r △ P) ==> t ∈ D (SKIP r ◻ P)› for t
    by (auto simp add: D_Interrupt D_Det SKIP_projs)
next
  show ‹t ∈ D (SKIP r ◻ P) ==> t ∈ D (SKIP r △ P)› for t
    by (auto simp add: D_Interrupt D_Det SKIP_projs intro: tickFree_Nil)
next
  show ‹(t, X) ∈ F (SKIP r △ P) ==> (t, X) ∈ F (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) ∈ F (SKIP r ◻ P) ==> (t, X) ∈ F (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 ∈ D ?lhs›
    then consider ‹s ∈ D P›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T P ∧ tickFree t1 ∧ t2 ∈ D (Q △ R)›
      by (simp add: D_Interrupt) blast
    thus ‹s ∈ D ?rhs›
    proof cases
      show ‹s ∈ D P ==> s ∈ D ?rhs› by (simp add: D_Interrupt)
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T P ∧ tickFree t1 ∧ t2 ∈ D (Q △ R)›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ T P›
        ‹tickFree t1› ‹t2 ∈ D (Q △ R)› by blast
      from "*"(4) consider ‹t2 ∈ D Q›
        | ‹∃u1 u2. t2 = u1 @ u2 ∧ u1 ∈ T Q ∧ tickFree u1 ∧ u2 ∈ D R›
        by (simp add: D_Interrupt) blast
      thus ‹s ∈ D ?rhs›
      proof cases
        from "*"(1, 2, 3) show ‹t2 ∈ D Q ==> s ∈ D ?rhs› by (simp add: D_Interrupt) blast
      next
        show ‹∃u1 u2. t2 = u1 @ u2 ∧ u1 ∈ T Q ∧ tickFree u1 ∧ u2 ∈ D R ==> s ∈ D ?rhs›
          by (simp add: "*"(1) D_Interrupt T_Interrupt)
            (metis "*"(2, 3) append_assoc tickFree_append_iff)
      qed
    qed
  next
    fix s
    assume ‹s ∈ D ?rhs›
    then consider ‹s ∈ D (P △ Q)›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T (P △ Q) ∧ tickFree t1 ∧ t2 ∈ D R›
      by (simp add: D_Interrupt) blast
    thus ‹s ∈ D ?lhs›
    proof cases
      show ‹s ∈ D (P △ Q) ==> s ∈ D ?lhs› by (simp add: D_Interrupt) blast
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T (P △ Q) ∧ tickFree t1 ∧ t2 ∈ D R›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ T (P △ Q)›
        ‹tickFree t1› ‹t2 ∈ D R› by blast
      from "*"(2) consider ‹t1 ∈ T P›
        | ‹∃u1 u2. t1 = u1 @ u2 ∧ u1 ∈ T P ∧ tickFree u1 ∧ u2 ∈ T Q›
        by (simp add: T_Interrupt) blast
      thus ‹s ∈ D ?lhs›
      proof cases
        show ‹t1 ∈ T P ==> s ∈ D ?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 ∈ T P ∧ tickFree u1 ∧ u2 ∈ T Q ==> s ∈ D ?lhs›
          by (simp add: D_Interrupt "*"(1)) 
            (metis "*"(3, 4) append.assoc tickFree_append_iff)
      qed
    qed
  next
    fix s X
    assume same_div: ‹D ?lhs = D ?rhs›
    assume ‹(s, X) ∈ F ?lhs›
    then consider ‹s ∈ D ?lhs›
      | ‹∃t1 r. s = t1 @ [🍋(r)] ∧ t1 @ [🍋(r)] ∈ T P›
      | ‹∃r. s @ [🍋(r)] ∈ T P ∧ 🍋(r) ∉ X›
      | ‹(s, X) ∈ F P ∧ tickFree s ∧ ([], X) ∈ F (Q △ R)›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T P ∧ tickFree t1 ∧ (t2, X) ∈ F (Q △ R) ∧ t2 ≠ []›
      | ‹∃r. s ∈ T P ∧ tickFree s ∧ [🍋(r)] ∈ T (Q △ R) ∧ 🍋(r) ∉ X›
      by (subst (asm) F_Interrupt, simp add: D_Interrupt) blast
    thus ‹(s, X) ∈ F ?rhs›
    proof cases
      from same_div D_F show ‹s ∈ D ?lhs ==> (s, X) ∈ F ?rhs› by blast
    next
      show ‹∃t1 r. s = t1 @ [🍋(r)] ∧ t1 @ [🍋(r)] ∈ T P ==> (s, X) ∈ F ?rhs›
        by (auto simp add: F_Interrupt T_Interrupt)
    next
      show ‹∃r. s @ [🍋(r)] ∈ T P ∧ 🍋(r) ∉ X ==> (s, X) ∈ F ?rhs›
        by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
    next
      assume assm : ‹(s, X) ∈ F P ∧ tickFree s ∧ ([], X) ∈ F (Q △ R)›
      with non_BOT(2, 3) consider r where ‹[🍋(r)] ∈ T Q ∧ 🍋(r) ∉ X›
        | ‹([], X) ∈ F Q ∧ ([], X) ∈ F R›
        | r where ‹[] ∈ T Q ∧ [🍋(r)] ∈ T R ∧ 🍋(r) ∉ X›
        by (simp add: F_Interrupt BOT_iff_Nil_D) blast
      thus ‹(s, X) ∈ F ?rhs›
      proof cases
        show ‹[🍋(r)] ∈ T Q ∧ 🍋(r) ∉ X ==> (s, X) ∈ F ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb F_T assm)
      next
        show ‹([], X) ∈ F Q ∧ ([], X) ∈ F R ==> (s, X) ∈ F ?rhs›
          by (simp add: F_Interrupt assm)
      next
        show ‹[] ∈ T Q ∧ [🍋(r)] ∈ T R ∧ 🍋(r) ∉ X ==> (s, X) ∈ F ?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 ∈ T P ∧ tickFree t1 ∧
 (t2, X) ∈ F (Q △ R) ∧ t2 ≠ []›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ T P› ‹tickFree t1›
        ‹(t2, X) ∈ F (Q △ R)› ‹t2 ≠ []› by blast
      from "*"(4) consider ‹t2 ∈ D (Q △ R)›
        | u1 r where ‹t2 = u1 @ [🍋(r)]› ‹u1 @ [🍋(r)] ∈ T Q›
        | r where ‹t2 @ [🍋(r)] ∈ T Q› ‹🍋(r) ∉ X›
        | ‹(t2, X) ∈ F Q› ‹tickFree t2› ‹([], X) ∈ F R›
        | u1 u2 where ‹t2 = u1 @ u2› ‹u1 ∈ T Q› ‹tickFree u1› ‹(u2, X) ∈ F R› ‹u2 ≠ []›
        | r where ‹t2 ∈ T Q› ‹tickFree t2› ‹[🍋(r)] ∈ T R› ‹🍋(r) ∉ X›
        by (simp add: F_Interrupt D_Interrupt) blast
      thus ‹(s, X) ∈ F ?rhs›
      proof cases
        assume ‹t2 ∈ D (Q △ R)›
        with "*"(1, 2, 3) have ‹s ∈ D ?lhs› by (simp add: D_Interrupt) blast
        with same_div D_F show ‹(s, X) ∈ F ?rhs› by blast
      next
        from "*"(1, 2, 3) show ‹t2 = u1 @ [🍋(r)] ==> u1 @ [🍋(r)] ∈ T Q ==> (s, X) ∈ F ?rhs› for u1 r
          by (auto simp add: F_Interrupt T_Interrupt)
      next
        from "*"(1, 2, 3) show ‹t2 @ [🍋(r)] ∈ T Q ==> 🍋(r) ∉ X ==> (s, X) ∈ F ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      next
        from "*"(1) show ‹(t2, X) ∈ F Q ==> tickFree t2 ==> ([], X) ∈ F R ==> (s, X) ∈ F ?rhs›
          by (simp add: F_Interrupt T_Interrupt) (metis "*"(2, 3, 5))
      next
        from "*"(1, 2, 3) show ‹t2 = u1 @ u2 ==> u1 ∈ T Q ==> tickFree u1 ==>
 (u2, X) ∈ F R ==> u2 ≠ [] ==> (s, X) ∈ F ?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 ∈ T Q ==> tickFree t2 ==>
 [🍋(r)] ∈ T R ==> 🍋(r) ∉ X ==> (s, X) ∈ F ?rhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      qed
    next
      show ‹∃r. s ∈ T P ∧ tickFree s ∧ [🍋(r)] ∈ T (Q △ R) ∧ 🍋(r) ∉ X ==> (s, X) ∈ F ?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 : ‹D ?lhs = D ?rhs›
    assume ‹(s, X) ∈ F ?rhs›
    then consider ‹s ∈ D ?rhs›
      | ‹∃t1 r. s = t1 @ [🍋(r)] ∧ t1 @ [🍋(r)] ∈ T (P △ Q)›
      | r where ‹s @ [🍋(r)] ∈ T (P △ Q)› ‹🍋(r) ∉ X›
      | ‹(s, X) ∈ F (P △ Q) ∧ tickFree s ∧ ([], X) ∈ F R›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T (P △ Q) ∧ tickFree t1 ∧ (t2, X) ∈ F R ∧ t2 ≠ []›
      | ‹∃r. s ∈ T (P △ Q) ∧ tickFree s ∧ [🍋(r)] ∈ T R ∧ 🍋(r) ∉ X›
      by (subst (asm) F_Interrupt, simp add: D_Interrupt) blast 
    thus ‹(s, X) ∈ F ?lhs›
    proof cases
      from same_div D_F show ‹s ∈ D ?rhs ==> (s, X) ∈ F ?lhs› by blast
    next
      show ‹∃t1 r. s = t1 @ [🍋(r)] ∧ t1 @ [🍋(r)] ∈ T (P △ Q) ==> (s, X) ∈ F ?lhs›
        by (simp add: F_Interrupt T_Interrupt)
          (metis last_append self_append_conv snoc_eq_iff_butlast)
    next
      fix r assume ‹s @ [🍋(r)] ∈ T (P △ Q)› ‹🍋(r) ∉ X›
      from this(1) consider ‹s @ [🍋(r)] ∈ T P›
        | t1 t2 where ‹s @ [🍋(r)] = t1 @ t2› ‹t1 ∈ T P› ‹tickFree t1› ‹t2 ∈ T Q›
        by (simp add: T_Interrupt) blast
      thus ‹(s, X) ∈ F ?lhs›
      proof cases
        show ‹s @ [🍋(r)] ∈ T P ==> (s, X) ∈ F ?lhs›
          by (simp add: F_Interrupt) (metis Diff_insert_absorb ‹🍋(r) ∉ X›)
      next
        show ‹s @ [🍋(r)] = t1 @ t2 ==> t1 ∈ T P ==> tickFree t1 ==> t2 ∈ T Q ==> (s, X) ∈ F ?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)] ∈ T (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) ∈ F (P △ Q) ∧ tickFree s ∧ ([], X) ∈ F R›
      from assm[THEN conjunct1] consider ‹s ∈ D (P △ Q)›
        | t1 r where ‹s = t1 @ [🍋(r)]› ‹t1 @ [🍋(r)] ∈ T P›
        | r where ‹s @ [🍋(r)] ∈ T P› ‹🍋(r) ∉ X›
        | ‹(s, X) ∈ F P› ‹tickFree s› ‹([], X) ∈ F Q›
        | t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ T P› ‹tickFree t1› ‹(t2, X) ∈ F Q› ‹t2 ≠ []›
        | r where ‹s ∈ T P› ‹tickFree s› ‹[🍋(r)] ∈ T Q› ‹🍋(r) ∉ X›
        by (simp add: F_Interrupt D_Interrupt) blast
      thus ‹(s, X) ∈ F ?lhs›
      proof cases
        assume ‹s ∈ D (P △ Q)›
        hence ‹s ∈ D ?rhs› by (simp add: D_Interrupt)
        with same_div D_F show ‹(s, X) ∈ F ?lhs› by blast
      next
        show ‹s = t1 @ [🍋(r)] ==> t1 @ [🍋(r)] ∈ T P ==> (s, X) ∈ F ?lhs› for t1 r
          by (simp add: F_Interrupt)
      next
        show ‹s @ [🍋(r)] ∈ T P ==> 🍋(r) ∉ X ==> (s, X) ∈ F ?lhs› for r
          by (simp add: F_Interrupt) (metis Diff_insert_absorb)
      next
        show ‹(s, X) ∈ F P ==> tickFree s ==> ([], X) ∈ F Q ==> (s, X) ∈ F ?lhs›
          by (simp add: F_Interrupt assm[THEN conjunct2])
      next
        show ‹s = t1 @ t2 ==> t1 ∈ T P ==> tickFree t1 ==> (t2, X) ∈ F Q ==>
 t2 ≠ [] ==> (s, X) ∈ F ?lhs› for t1 t2
          by (simp add: F_Interrupt) (metis assm[THEN conjunct2] tickFree_append_iff)
      next
        show ‹s ∈ T P ==> tickFree s ==> [🍋(r)] ∈ T Q ==> 🍋(r) ∉ X ==> (s, X) ∈ F ?lhs› for r
          by (simp add: F_Interrupt T_Interrupt) (metis Diff_insert_absorb)
      qed
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ T (P △ Q) ∧
 tickFree t1 ∧ (t2, X) ∈ F R ∧ t2 ≠ []›
      then obtain t1 t2 where * : ‹s = t1 @ t2› ‹t1 ∈ T (P △ Q)›
        ‹tickFree t1› ‹(t2, X) ∈ F R› ‹t2 ≠ []› by blast
      from "*"(2) consider ‹t1 ∈ T P›
        | ‹∃u1 u2. t1 = u1 @ u2 ∧ u1 ∈ T P ∧ tickFree u1 ∧ u2 ∈ T Q›
        by (simp add: T_Interrupt) blast
      thus ‹(s, X) ∈ F ?lhs›
      proof cases
        from "*"(1, 3, 4, 5) show ‹t1 ∈ T P ==> (s, X) ∈ F ?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 ∈ T P ∧
 tickFree u1 ∧ u2 ∈ T Q ==> (s, X) ∈ F ?lhs›
          by (elim exE, simp add: F_Interrupt) (metis append_is_Nil_conv)
      qed
    next
      show ‹∃r. s ∈ T (P △ Q) ∧ tickFree s ∧ [🍋(r)] ∈ T R ∧ 🍋(r) ∉ X ==> (s, X) ∈ F ?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 ∈ D ?lhs ==> s ∈ D ?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 ∈ D (Y i)} ∪
 {t1. ∃t2. s = t1 @ t2 ∧ t1 ∈ T (Y i) ∧ tickFree t1 ∧ t2 ∈ D Q}› for i
  assume ‹s ∈ D ?rhs›
  hence ‹s ∈ D (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 ∈ D ?lhs›
  proof (cases ‹∀i. s ∈ D (Y i)›)
    case True
    thus ‹s ∈ D ?lhs› by (simp add: D_Interrupt limproc_is_thelub D_LUB chain)
  next
    case False
    with "*" obtain j t2 where ** : ‹s = t1 @ t2› ‹t1 ∈ T (Y j)› ‹ tickFree t1› ‹t2 ∈ D Q›
      by (simp add: S_def) blast
    from "*" D_T have ‹∀i. t1 ∈ T (Y i)› by (simp add: S_def) blast
    with "**"(1, 3, 4) show ‹s ∈ D ?lhs›
      by (simp add: D_Interrupt limproc_is_thelub T_LUB chain) blast
  qed
next
  show ‹(s, X) ∈ F ?lhs ==> (s, X) ∈ F ?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 : ‹D ((⊔i. Y i) △ Q) = D (⊔i. Y i △ Q)›
  fix s X assume ‹(s, X) ∈ F (⊔i. Y i △ Q)›
  show ‹(s, X) ∈ F ((⊔i. Y i) △ Q)›
  proof (cases ‹s ∈ D (⊔i. Y i △ Q)›)
    show ‹s ∈ D (⊔i. Y i △ Q) ==> (s, X) ∈ F ((⊔i. Y i) △ Q)›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ D (⊔i. Y i △ Q)›
    then obtain j where ‹s ∉ D (Y j △ Q)›
      by (auto simp add: limproc_is_thelub chain_Interrupt_left ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ F (⊔i. Y i △ Q)› have ‹(s, X) ∈ F (Y j △ Q)›
      by (simp add: limproc_is_thelub chain_Interrupt_left ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ F ((⊔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 ∈ D (S △ (⊔i. Y i)) ==> s ∈ D (⊔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 ∈ D (⊔i. S △ Y i)›
  show ‹s ∈ D (S △ (⊔i. Y i))›
  proof (cases ‹s ∈ D S›)
    show ‹s ∈ D S ==> s ∈ D (S △ (⊔i. Y i))› by (simp add: D_Interrupt)
  next
    assume ‹s ∉ D S›
    define T where ‹T i ≡ {t1. ∃t2 r. s = t1 @ t2 ∧ t1 ∈ T S ∧ tickFree t1 ∧ t2 ∈ D (Y i)}› for i
    from ‹s ∉ D S› ‹s ∈ D (⊔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 ∈ T S› ‹tickFree t1› ‹∀i. t2 ∈ D (Y i)›
      by (simp add: T_def) blast
    thus ‹s ∈ D (S △ (⊔i. Y i))›
      by (simp add: D_Interrupt limproc_is_thelub ‹chain Y› D_LUB) blast
  qed
next
  show ‹(s, X) ∈ F (S △ (⊔i. Y i)) ==> (s, X) ∈ F (⊔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 : ‹D (S △ (⊔i. Y i)) = D (⊔i. S △ Y i)›
  fix s X assume ‹(s, X) ∈ F (⊔i. S △ Y i)›
  show ‹(s, X) ∈ F (S △ (⊔i. Y i))›
  proof (cases ‹s ∈ D (⊔i. S △ Y i)›)
    show ‹s ∈ D (⊔i. S △ Y i) ==> (s, X) ∈ F (S △ (⊔i. Y i))›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ D (⊔i. S △ Y i)›
    then obtain j where ‹s ∉ D (S △ Y j)›
      by (auto simp add: limproc_is_thelub chain_Interrupt_right ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ F (⊔i. S △ Y i)› have ‹(s, X) ∈ F (S △ Y j)›
      by (simp add: limproc_is_thelub chain_Interrupt_right ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ F (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
  (*>*)