Theory Sequential_Composition_Generalized

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Generalization of the Sequential Composition›


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


section ‹Definition›

text ‹
For the sequential composition, the generalization seems quite straightforward.
In a nutshell, we just replace term‹Q› with term‹Q r› in the definition
of term‹P ; Q› since term‹Q› is now of type typ‹'r ⇒ ('a, 'r) processptick›
(instead of typ‹('a, 'r) processptick›).
›

lift_definition Seqptick ::
  ‹[('a, 'r) processptick, 'r ⇒ ('a, 'r) processptick] ⇒ ('a, 'r) processptick› (infixl ‹;✓› 74)
  is ‹λP Q. ({(t, X) |t X. (t, X ∪ range tick) ∈ ℱ P ∧ tF t} ∪
             {(t @ u, X) |t u r X. t @ [✓(r)] ∈ 𝒯 P ∧ (u, X) ∈ ℱ (Q r)} ∪
             {(t, X). t ∈ 𝒟 P},
             𝒟 P ∪ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒟 (Q r)})›
  oops


text ‹
Except that this is not a fully satisfactory definition yet. Indeed, here, the right-hand
side argument must produce processes whose terminations keep the same type.
In other words, term‹Q› is of type typ‹'r ⇒ ('a, 'r) processptick› while
we would like to have in full generality typ‹'r ⇒ ('a, 's) processptick›.
The final definition given below is not immediate, and involves a precise
understanding of the behaviour of the sequential composition.
›

subsection ‹Preliminaries›

text ‹
The first key for generalizing the definition is to see that term‹map (ev ∘ of_ev)›
allows for changing the type of termination in tick-free traces.
›

lemma tickFree_map_ev_of_ev_same_type_is : ‹tF t ⟹ map (ev ∘ of_ev) t = t›
  ― ‹In this case the type of termination remains unchanged.›
  by (induct t) simp_all


lemma tickFree_map_ev_of_ev_eq_iff :
  ‹tF t ⟹ map (ev ∘ of_ev) t = t' ⟹ t = map (ev ∘ of_ev) t'›
  by (induct t arbitrary: t') auto

lemma tickFree_map_ev_of_ev_inj :
  ‹tF t ⟹ tF t' ⟹ map (ev ∘ of_ev) t = map (ev ∘ of_ev) t' ⟷ t = t'›
  by (induct t arbitrary: t') (use eventptick.expand in auto)+

lemma map_ev_of_ev_map_ev_of_ev [simp] :
  ‹map (ev ∘ of_ev) (map (ev ∘ of_ev) t) = map (ev ∘ of_ev) t› by simp

lemma map_ev_of_ev_map_ev_of_ev_simplified [simp] :
  ‹map (ev ∘ of_ev ∘ (ev ∘ of_ev)) t = map (ev ∘ of_ev) t› by simp

lemma tickFree_map_ev_of_ev_eq_imp_ev_mem_iff :
  ‹tF t' ⟹ t = map (ev ∘ of_ev) t' ⟹ ev a ∈ set t ⟷ ev a ∈ set t'›
  by (induct t' arbitrary: t) auto



text ‹
The second key is to understand that term‹X ∪ range tick›
can be rewritten as term‹(ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick›,
and that this second expression also allows for changing the type of termination.
›

definition ref_Seqptick :: ‹('a, 'r) eventptick set ⇒ ('a, 's) eventptick set›
  where ‹ref_Seqptick X ≡ (ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick›

lemma ref_Seqptick_same_type_is : ‹ref_Seqptick X = X ∪ range tick›
  ― ‹In this case the type of termination remains unchanged.›
  by (auto simp add: ref_Seqptick_def set_eq_iff image_iff)
    (metis Int_iff eventptick.exhaust eventptick.sel(1) rangeI)


lemma mono_ref_Seqptick : ‹X ⊆ Y ⟹ ref_Seqptick X ⊆ ref_Seqptick Y›
  unfolding ref_Seqptick_def by fast


lemma ref_Seqptick_idem : ‹ref_Seqptick (ref_Seqptick X) = ref_Seqptick X›
  by (auto simp add: image_iff ref_Seqptick_def) 
    (metis Int_iff eventptick.sel(1) rangeI,
      metis (lifting) Int_iff Un_iff eventptick.sel(1) image_eqI rangeI)


lemma ref_Seqptick_comp_ref_Seqptick : ‹ref_Seqptick ∘ ref_Seqptick = ref_Seqptick›
  by (rule ext) (simp add: ref_Seqptick_idem)


lemma ref_Seqptick_eq_iff :
  ‹ref_Seqptick X = ref_Seqptick Y ⟷ X ∩ range ev = Y ∩ range ev›
proof (rule iffI)
  show ‹X ∩ range ev = Y ∩ range ev ⟹ ref_Seqptick X = ref_Seqptick Y›
    by (auto simp add: ref_Seqptick_def)
next
  show ‹X ∩ range ev = Y ∩ range ev› if ‹ref_Seqptick X = ref_Seqptick Y›
  proof (rule set_eqI)
    show ‹e ∈ X ∩ range ev ⟷ e ∈ Y ∩ range ev› for e
      using that[unfolded set_eq_iff, THEN spec, of ‹(ev ∘ of_ev) e›]
      by (auto simp add: ref_Seqptick_def)
  qed
qed


lemma ref_Seqptick_is_map_eventptick_image :
  ‹ref_Seqptick X = map_eventptick id g ` (X ∩ range ev) ∪ range tick›
  ― ‹Note that term‹g› is free here and does not matter.›
  by (auto simp add: ref_Seqptick_def image_iff)
    (metis Int_iff eq_id_iff map_eventptick_eq_ev_iff rangeI,
      metis Int_iff eventptick.sel(1) rangeI)


lemma ref_Seqptick_union_image_ev :
  ‹ref_Seqptick (X ∪ ev ` S) = ref_Seqptick X ∪ ev ` S›
  by (auto simp add: ref_Seqptick_def image_iff)
    (metis Int_iff Un_iff eventptick.sel(1) image_eqI rangeI)

lemma ref_Seqptick_UNIV : ‹ref_Seqptick UNIV = UNIV›
  by (simp add: set_eq_iff ref_Seqptick_def image_iff)
    (meson eventptick.exhaust)



subsection ‹Formal Definition›



definition div_Seqptick ::
  ‹[('a, 'r) processptick, 'r ⇒ ('a, 's) processptick] ⇒ ('a, 's) traceptick set›
  where ‹div_Seqptick P Q ≡
         {map (ev ∘ of_ev) t @ u |t u. t ∈ 𝒟 P ∧ tF t ∧ ftF u} ∪
         {map (ev ∘ of_ev) t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒟 (Q r)}›

definition fail_Seqptick ::
  ‹[('a, 'r) processptick, 'r ⇒ ('a, 's) processptick] ⇒ ('a, 's) failureptick set›
  where ‹fail_Seqptick P Q ≡
         {(map (ev ∘ of_ev) t, X) |t X. (t, ref_Seqptick X) ∈ ℱ P ∧ tF t} ∪
         {(map (ev ∘ of_ev) t @ u, X) |t u r X. t @ [✓(r)] ∈ 𝒯 P ∧ tF t ∧ (u, X) ∈ ℱ (Q r)} ∪
         {(map (ev ∘ of_ev) t @ u, X) |t u X. t ∈ 𝒟 P ∧ tF t ∧ ftF u}›
    ― ‹term‹tF t› is trivial when term‹t @ [✓(r)] ∈ 𝒯 P›, but we add it for proof automation›

lift_definition Seqptick ::
  ‹[('a, 'r) processptick, 'r ⇒ ('a, 's) processptick] ⇒ ('a, 's) processptick› (infixl ‹;✓› 74)
  is ‹λP Q. (fail_Seqptick P Q, div_Seqptick P Q)›
proof -
  show ‹?thesis P Q› (is ‹is_process(?f, ?d)›) for P and Q
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI allI impI)
    show ‹([], {}) ∈ ?f›
      by (simp add: fail_Seqptick_def ref_Seqptick_def)
        (metis append_Nil is_processT1 trace_tick_continuation_or_all_tick_failuresE)
  next
    show ‹(t, X) ∈ ?f ⟹ ftF t› for t X
      by (auto simp add: fail_Seqptick_def div_Seqptick_def
          F_imp_front_tickFree D_imp_front_tickFree
          intro: front_tickFree_append)
  next
    show ‹(t @ u, {}) ∈ ?f ⟹ (t, {}) ∈ ?f› for t u
    proof (induct u arbitrary: t)
      show ‹(t @ [], {}) ∈ ?f ⟹ (t, {}) ∈ ?f› for t by simp
    next
      fix t e u assume prem : ‹(t @ e # u, {}) ∈ ?f›
      assume hyp : ‹(t @ u, {}) ∈ ?f ⟹ (t, {}) ∈ ?f› for t
      from prem have ‹((t @ [e]) @ u, {}) ∈ ?f› by simp
      with hyp have ‹(t @ [e], {}) ∈ ?f› by presburger
      then consider (D_P) t' u where ‹t @ [e] = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
        | (F_P) t' where ‹t @ [e] = map (ev ∘ of_ev) t'› ‹(t', range tick) ∈ ℱ P› ‹tF t'›
        | (F_Q) t' r u where ‹t @ [e] = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹(u, {}) ∈ ℱ (Q r)›
        by (auto simp add: fail_Seqptick_def div_Seqptick_def ref_Seqptick_def)
      thus ‹(t, {}) ∈ ?f›
      proof cases
        case D_P
        show ?thesis
        proof (cases u rule: rev_cases)
          assume ‹u = []›
          have ‹(butlast t', {}) ∈ ℱ P› 
            by (metis D_P(2) D_T prefixI T_F_spec append_butlast_last_id
                butlast.simps(1) is_processT3_TR)
          thus ‹(t, {}) ∈ ?f›
            by (elim trace_tick_continuation_or_all_tick_failuresE, simp_all add: fail_Seqptick_def ref_Seqptick_def)
              (metis (no_types, opaque_lifting) D_P(1) ‹u = []› append.right_neutral
                append_T_imp_tickFree butlast_snoc is_processT1 map_butlast not_Cons_self2,
                metis D_P(1,3) ‹u = []› append.right_neutral butlast_snoc
                front_tickFree_iff_tickFree_butlast map_butlast tickFree_imp_front_tickFree)
        next
          fix e' u' assume ‹u = u' @ [e']›
          with D_P have ‹t = map (ev ∘ of_ev) t' @ u'› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u'›  
            by (simp_all add: front_tickFree_append_iff)
          thus ‹(t, {}) ∈ ?f› by (auto simp add: fail_Seqptick_def)
        qed
      next
        case F_P
        have ‹(butlast t', {}) ∈ ℱ P›
          by (metis F_P(1, 2) is_processT3 is_processT4_empty list.map_disc_iff snoc_eq_iff_butlast)
        with F_P(2) show ‹(t, {}) ∈ ?f›
          by (elim trace_tick_continuation_or_all_tick_failuresE, simp_all add: fail_Seqptick_def ref_Seqptick_def)
            (metis (no_types, lifting) F_P(1) T_imp_front_tickFree append.right_neutral butlast_snoc
              front_tickFree_iff_tickFree_butlast is_processT1 map_butlast,
              metis F_P(1) F_imp_front_tickFree butlast_snoc front_tickFree_iff_tickFree_butlast map_butlast)
      next
        case F_Q
        show ‹(t, {}) ∈ ?f›
        proof (cases u rule: rev_cases)
          assume ‹u = []›
          have ‹(butlast t', {}) ∈ ℱ P›
            by (metis F_Q(2) T_F_spec append_butlast_last_id butlast.simps(1) is_processT3_TR_append)
          thus ‹(t, {}) ∈ ?f›
            by (elim trace_tick_continuation_or_all_tick_failuresE, simp_all add: fail_Seqptick_def ref_Seqptick_def)
              (metis (no_types, lifting) F_Q(1) ‹u = []› append_T_imp_tickFree butlast_snoc
                is_processT1 map_butlast not_Cons_self2 self_append_conv,
                metis F_Q(1, 2) T_imp_front_tickFree ‹u = []› append_self_conv butlast_snoc
                front_tickFree_iff_tickFree_butlast is_processT3_TR_append map_butlast)
        next
          from F_Q show ‹u = u' @ [e'] ⟹ (t, {}) ∈ ?f› for u' e'
            by (simp add: fail_Seqptick_def) 
              (metis append_T_imp_tickFree is_processT3 list.distinct(1))
        qed
      qed
    qed
  next
    fix t X Y assume ‹(t, Y) ∈ ?f ∧ X ⊆ Y›
    hence ‹(t, Y)∈ ?f› ‹X ⊆ Y› by simp_all
    from ‹(t, Y)∈ ?f› consider (F_P) t' where ‹t = map (ev ∘ of_ev) t'›
      ‹(t', (ev ∘ of_ev) ` (Y ∩ range ev) ∪ range tick) ∈ ℱ P› ‹tF t'›
    | (F_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹(u, Y) ∈ ℱ (Q r)›
    | (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      by (auto simp add: fail_Seqptick_def ref_Seqptick_def)
    thus ‹(t, X) ∈ ?f›
    proof cases
      case F_P
      from ‹X ⊆ Y› have ‹(ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick ⊆
                         (ev ∘ of_ev) ` (Y ∩ range ev) ∪ range tick› by blast
      with F_P(2) have ‹(t', (ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick) ∈ ℱ P›
        by (metis is_processT4)
      with F_P(1, 3) show ‹(t, X) ∈ ?f›
        by (auto simp add: fail_Seqptick_def ref_Seqptick_def)
    next
      case F_Q thus ‹(t, X) ∈ ?f›
        by (simp add: fail_Seqptick_def) (metis ‹X ⊆ Y› is_processT4)
    next
      case D_P thus ‹(t, X) ∈ ?f› by (auto simp add: fail_Seqptick_def)
    qed
  next
    fix t X Y assume * : ‹(t, X) ∈ ?f ∧ (∀e. e ∈ Y ⟶ (t @ [e], {}) ∉ ?f)›
    from "*" consider ‹t ∈ ?d›
      | (F_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹(t', (ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick) ∈ ℱ P› ‹tF t'›
      | (F_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
      unfolding fail_Seqptick_def div_Seqptick_def ref_Seqptick_def by auto
    thus ‹(t, X ∪ Y) ∈ ?f›
    proof cases
      show ‹t ∈ ?d ⟹ (t, X ∪ Y) ∈ ?f›
        by (simp add: div_Seqptick_def fail_Seqptick_def) (metis is_processT8)
    next
      case F_P
      have ‹(t', (ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick ∪ (ev ∘ of_ev) ` (Y ∩ range ev)) ∈ ℱ P›
      proof (intro is_processT5[OF F_P(2)] allI impI)
        fix e :: ‹('a, 'r) eventptick› assume ‹e ∈ (ev ∘ of_ev) ` (Y ∩ range ev)›
        then obtain a where ‹e = ev a› ‹ev a ∈ Y› by auto
        from "*"[THEN conjunct2, rule_format, OF this(2), unfolded fail_Seqptick_def] F_P(1, 3)
        show ‹(t' @ [e], {}) ∉ ℱ P›
          apply (simp add: fail_Seqptick_def ‹e = ev a› append_eq_map_conv ref_Seqptick_def)
          by (smt (verit, del_insts) append_Nil2 comp_apply eventptick.sel(1) is_processT1
                  list.simps(8, 9) map_append tickFree_append_iff
                  tickFree_map_ev_comp trace_tick_continuation_or_all_tick_failuresE)
      qed
      also have ‹(ev ∘ of_ev) ` (X ∩ range ev) ∪ range tick ∪ (ev ∘ of_ev) ` (Y ∩ range ev) =
                 ref_Seqptick (X ∪ Y)› unfolding ref_Seqptick_def by blast
      finally show ‹(t, X ∪ Y) ∈ ?f›
        using F_P(1, 3) by (auto simp add: fail_Seqptick_def)
    next
      case F_Q
      from "*" have ‹∀e. e ∈ Y ⟶ (u @ [e], {}) ∉ ℱ (Q r)›
        by (simp add: fail_Seqptick_def F_Q(1, 2))
          (metis F_Q(2) append_T_imp_tickFree not_Cons_self2)
      with F_Q(3, 4) have ‹(u, X ∪ Y) ∈ ℱ (Q r)› by (simp add: is_processT5)
      with F_Q(1-3) show ‹(t, X ∪ Y) ∈ ?f› by (auto simp add: fail_Seqptick_def)
    qed
  next
    show ‹t ∈ ?d ∧ tF t ∧ ftF u ⟹ t @ u ∈ ?d› for t u
      by (simp add: div_Seqptick_def, elim conjE disjE exE)
        (solves ‹use front_tickFree_append in auto›,
          meson append.assoc is_processT7 tickFree_append_iff)
  next  
    show ‹t ∈ ?d ⟹ (t, X) ∈ ?f› for t X
      by (simp add: div_Seqptick_def fail_Seqptick_def) (metis is_processT8)
  next
    show * : ‹t @ [✓(r')] ∈ ?d ⟹ t ∈ ?d› for t r'
      by (simp add: div_Seqptick_def, elim disjE exE conjE)
        (metis butlast_append butlast_snoc front_tickFree_iff_tickFree_butlast non_tickFree_tick
          tickFree_append_iff tickFree_imp_front_tickFree tickFree_map_ev_comp,
          metis D_imp_front_tickFree butlast_append butlast_snoc
          div_butlast_when_non_tickFree_iff non_tickFree_tick
          tickFree_append_iff tickFree_map_ev_comp)

    fix t r' X assume ‹(t @ [✓(r')], {}) ∈ ?f›
    then consider ‹t @ [✓(r')] ∈ ?d›
      | (F_Q) t' r u where ‹t @ [✓(r')] = map (ev ∘ of_ev) t' @ u›
        ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
      by (auto simp add: fail_Seqptick_def div_Seqptick_def)
        (metis non_tickFree_tick tickFree_append_iff tickFree_map_ev_comp,
          metis F_T F_imp_front_tickFree nonTickFree_n_frontTickFree
                non_tickFree_tick tickFree_append_iff tickFree_map_ev_comp tick_T_F)
    thus ‹(t, X - {✓(r')}) ∈ ?f›
    proof cases
      assume ‹t @ [✓(r')] ∈ ?d›
      with "*" have ‹t ∈ ?d› .
      thus ‹(t, X - {✓(r')}) ∈ ?f›
        by (simp add: fail_Seqptick_def div_Seqptick_def) (metis is_processT8)
    next
      case F_Q
      from F_Q(1, 2) obtain u' where ‹u = u' @ [✓(r')]›
        by (cases u rule: rev_cases, simp_all)
          (metis non_tickFree_tick tickFree_append_iff tickFree_map_ev_comp)
      with F_Q(4) have ‹(u', X - {✓(r')}) ∈ ℱ (Q r)› by (simp add: F_T is_processT6_TR)
      with F_Q(1-3) ‹u = u' @ [✓(r')]› show ‹(t, X - {✓(r')}) ∈ ?f›
        by (auto simp add: fail_Seqptick_def)
    qed
  qed
qed




section ‹Projections›

lemma F_Seqptick : ‹ℱ (P ;✓ Q) = fail_Seqptick P Q›
  by (simp add: Failures.rep_eq FAILURES_def Seqptick.rep_eq)


lemma D_Seqptick : ‹𝒟 (P ;✓ Q) = div_Seqptick P Q›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Seqptick.rep_eq)


lemma T_Seqptick_bis :
  ‹𝒯 (P ;✓ Q) = {map (ev ∘ of_ev) t |t. (t, range tick) ∈ ℱ P ∧ tF t} ∪
                {map (ev ∘ of_ev) t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒯 (Q r)} ∪
                {map (ev ∘ of_ev) t @ u |t u. t ∈ 𝒟 P ∧ tF t ∧ ftF u}›
  by (auto simp add: Traces.rep_eq TRACES_def F_Seqptick fail_Seqptick_def ref_Seqptick_def
      intro: is_processT4 simp flip: Failures.rep_eq)
    (metis, metis (lifting) image_empty inf_bot_left sup_bot_left, blast)


lemma T_Seqptick :
  ‹𝒯 (P ;✓ Q) = {map (ev ∘ of_ev) t |t. t ∈ 𝒯 P ∧ tF t} ∪
                {map (ev ∘ of_ev) t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒯 (Q r)} ∪
                {map (ev ∘ of_ev) t @ u |t u. t ∈ 𝒟 P ∧ tF t ∧ ftF u}›
  ―‹Often easier to use›
  by (auto simp add: T_Seqptick_bis F_T)
    (metis T_F_spec append.right_neutral is_processT1_TR
      trace_tick_continuation_or_all_tick_failuresE)

lemmas Seqptick_projs = F_Seqptick D_Seqptick T_Seqptick fail_Seqptick_def div_Seqptick_def


lemma mono_Seqptick_eq : ‹P ;✓ Q = P' ;✓ Q'› if * : ‹P = P'› ‹⋀r. r ∈ ✓s(P) ⟹ Q r = Q' r›
  for P P' :: ‹('a, 'r) processptick› and Q Q' :: ‹'r ⇒ ('a, 's) processptick›
proof (fold "*"(1), subst Process_eq_spec_optimized, safe)
  { fix t and Q Q' :: ‹'r ⇒ ('a, 's) processptick›
    assume ‹t ∈ 𝒟 (P ;✓ Q)› and * : ‹r ∈ ✓s(P) ⟹ Q r = Q' r› for r
    from ‹t ∈ 𝒟 (P ;✓ Q)› consider (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      | (D_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒟 (Q r)›
      unfolding Seqptick_projs by blast
    hence ‹t ∈ 𝒟 (P ;✓ Q')›
    proof cases
      case D_P thus ‹t ∈ 𝒟 (P ;✓ Q')› by (auto simp add: Seqptick_projs)
    next
      case D_Q thus ‹t ∈ 𝒟 (P ;✓ Q')›
        by (simp add: Seqptick_projs)
          (metis "*" D_imp_front_tickFree is_processT9 strict_ticks_of_memI)
    qed
  } note $ = this
  show ‹t ∈ 𝒟 (P ;✓ Q) ⟹ t ∈ 𝒟 (P ;✓ Q')›
    and ‹t ∈ 𝒟 (P ;✓ Q') ⟹ t ∈ 𝒟 (P ;✓ Q)› for t
    by (erule "$", simp add: "*"(2))+
next
  { fix t X and Q Q' :: ‹'r ⇒ ('a, 's) processptick›
    assume ‹(t, X) ∈ ℱ (P ;✓ Q)› and same_div : ‹𝒟 (P ;✓ Q) = 𝒟 (P ;✓ Q')›
      and * : ‹r ∈ ✓s(P) ⟹ Q r = Q' r› for r
    from ‹(t, X) ∈ ℱ (P ;✓ Q)›
    consider (F_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹(t', ref_Seqptick X) ∈ ℱ P› ‹tF t'›
      | (F_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P›  ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
      | (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      unfolding Seqptick_projs  by blast
    hence ‹(t, X) ∈ ℱ (P ;✓ Q')›
    proof cases
      case F_P thus ‹(t, X) ∈ ℱ (P ;✓ Q')› by (auto simp add: Seqptick_projs)
    next
      case F_Q thus ‹(t, X) ∈ ℱ (P ;✓ Q')›
        by (simp add: Seqptick_projs)
          (metis "*" F_imp_front_tickFree is_processT9 strict_ticks_of_memI)
    next
      case D_P thus ‹(t, X) ∈ ℱ (P ;✓ Q')› by (auto simp add: Seqptick_projs)
    qed
  } note $ = this
  show ‹𝒟 (P ;✓ Q) = 𝒟 (P ;✓ Q') ⟹ (t, X) ∈ ℱ (P ;✓ Q) ⟹ (t, X) ∈ ℱ (P ;✓ Q')›
    and ‹𝒟 (P ;✓ Q) = 𝒟 (P ;✓ Q') ⟹ (t, X) ∈ ℱ (P ;✓ Q') ⟹ (t, X) ∈ ℱ (P ;✓ Q)› for t X
    by (erule "$"; simp add: "*"(2))+
qed




text ‹
Note that this definition allowing for changing the type of termination is actually
a generalization of the first idea that we mentioned at the beginning.
Indeed, when we enforce the type of term‹P› and term‹Q› to be
typ‹('a, 'r) processptick› and typ‹'r ⇒ ('a, 's) processptick› respectively,
the projections can be rewritten as follows.
›



lemma F_Seqptick_same_type :
  ‹ℱ (P ;✓ Q) = {(t, X) |t X. (t, X ∪ range tick) ∈ ℱ P ∧ tF t} ∪
                {(t @ u, X) |t u r X. t @ [✓(r)] ∈ 𝒯 P ∧ (u, X) ∈ ℱ (Q r)} ∪
                {(t, X). t ∈ 𝒟 P}›
  by (auto simp add: Seqptick_projs tickFree_map_ev_of_ev_same_type_is ref_Seqptick_same_type_is is_processT7)
    (metis tickFree_map_ev_of_ev_same_type_is,
      metis append_T_imp_tickFree not_Cons_self2,
      metis D_T T_imp_front_tickFree T_nonTickFree_imp_decomp append.right_neutral
            front_tickFree_nonempty_append_imp is_processT9 not_Cons_self2
            tickFree_Nil tickFree_imp_front_tickFree)


lemma D_Seqptick_same_type : ‹𝒟 (P ;✓ Q) = 𝒟 P ∪ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒟 (Q r)}›
  by (auto simp add: Seqptick_projs tickFree_map_ev_of_ev_same_type_is is_processT7)
    (blast,
      metis D_imp_front_tickFree butlast_snoc div_butlast_when_non_tickFree_iff
            front_tickFree_charn front_tickFree_nonempty_append_imp
            self_append_conv tickFree_Nil tickFree_map_ev_of_ev_same_type_is,
      metis append_T_imp_tickFree not_Cons_self2)


lemma T_Seqptick_same_type_bis :
  ‹𝒯 (P ;✓ Q) = {t. (t, range tick) ∈ ℱ P ∧ tF t} ∪
                {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒯 (Q r)} ∪
                𝒟 P›
  by (auto simp add: Traces.rep_eq TRACES_def F_Seqptick_same_type simp flip: Failures.rep_eq)
    (meson is_processT4 sup_ge2, meson is_processT5_S7', blast)


lemma T_Seqptick_same_type :
  ‹𝒯 (P ;✓ Q) = {t ∈ 𝒯 P. tF t} ∪ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒯 (Q r)} ∪ 𝒟 P›
  ―‹Often easier to use›
  by (auto simp add: T_Seqptick_same_type_bis F_T)
    (metis T_F_spec append.right_neutral is_processT1_TR
      trace_tick_continuation_or_all_tick_failuresE)

lemmas Seqptick_same_type_projs = F_Seqptick_same_type D_Seqptick_same_type T_Seqptick_same_type



(*<*)
end
  (*>*)