Theory Sequential_Composition_Generalized_Cont

(***********************************************************************************
 * 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 ‹Continuity Rules›

(*<*)
theory Sequential_Composition_Generalized_Cont
  imports Multi_Sequential_Composition_Generalized 
begin
  (*>*)


section ‹Sequential Composition›

subsection ‹Monotonicity›

lemma tickFree_mem_min_elems_D : ‹t ∈ min_elems (𝒟 P) ⟹ tF t›
  by (metis D_imp_front_tickFree Prefix_Order.prefixI append_self_conv elem_min_elems
            is_processT9 min_elems_no nonTickFree_n_frontTickFree not_Cons_self2)


lemma mono_Seqptick : ‹P ;✓ R ⊑ Q ;✓ S› if ‹P ⊑ Q› and ‹R ⊑ S›
  for P Q :: ‹('a, 'r) processptick› and R S :: ‹'r ⇒ ('a, 's) processptick›
proof -
  let ?S = ‹λP R. map (ev ∘ of_ev) ` min_elems (𝒟 P) ∪
                  {map (ev ∘ of_ev) t @ u| t r u. t @ [✓(r)] ∈ 𝒯 P ∧ t ∉ 𝒟 P ∧
                                                  tF t ∧ u ∈ min_elems (𝒟 (R r))}›
  { fix P and R :: ‹'r ⇒ ('a, 's) processptick› and t
    assume ‹t ∈ min_elems (𝒟 (P ;✓ R))›
    hence * : ‹t ∈ 𝒟 (P ;✓ R)› and ** : ‹⋀t'. t' ∈ 𝒟 (P ;✓ R) ⟹ ¬ t' < t›
      by (simp_all add: min_elems_def)
    from "*" consider (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      | (D_R) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹tF t'› ‹u ∈ 𝒟 (R r)›
      by (simp add: Seqptick_projs) (metis D_imp_front_tickFree)
    hence ‹t ∈ ?S P R›
    proof cases
      case D_P
      from D_P(1-3) "**"[of ‹map (ev ∘ of_ev) t'›] have ‹u = []›
        by (simp add: Seqptick_projs)
          (metis strict_prefixI' append.right_neutral front_tickFree_Nil neq_Nil_conv)
      have ‹t' ∈ min_elems (𝒟 P)›
      proof (rule ccontr)
        assume ‹t' ∉ min_elems (𝒟 P)›
        with D_P(2) obtain t'' where ‹t'' ∈ 𝒟 P› ‹t'' < t'› unfolding min_elems_def by fast
        with D_P(1, 3) "**"[of ‹map (ev ∘ of_ev) t''›] show False
          by (auto simp add: Seqptick_projs ‹u = []›)
            (metis (no_types, lifting) strict_prefixE' strict_prefix_simps(2) front_tickFree_Nil
              less_append list.simps(9) map_append self_append_conv tickFree_append_iff)
      qed
      thus ‹t ∈ ?S P R› by (simp add: D_P(1) ‹u = []›)
    next
      case D_R
      have ‹u ∈ min_elems (𝒟 (R r))›
      proof (rule ccontr)
        assume ‹u ∉ min_elems (𝒟 (R r))›
        with D_R(5) obtain u' where ‹u' ∈ 𝒟 (R r)› ‹u' < u› unfolding min_elems_def by fast
        with D_R(1, 2, 4) "**"[of ‹map (ev ∘ of_ev) t' @ u'›] show False
          by (simp add: Seqptick_projs) (use less_append in blast)
      qed
      with D_R(1-4) show ‹t ∈ ?S P R› by auto
    qed
  } note "$" = this

  show ‹P ;✓ R ⊑ Q ;✓ S›
  proof (rule below_trans)
    show ‹P ;✓ R ⊑ Q ;✓ R›
    proof (unfold le_approx_def, safe)
      from le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›]
      show ‹t ∈ 𝒟 (Q ;✓ R) ⟹ t ∈ 𝒟 (P ;✓ R)› for t
        unfolding Seqptick_projs by blast
    next
      from le_approx2[OF ‹P ⊑ Q›] le_approx2T[OF ‹P ⊑ Q›]
      show ‹t ∉ 𝒟 (P ;✓ R) ⟹ X ∈ ℛa (P ;✓ R) t ⟹ X ∈ ℛa (Q ;✓ R) t› for t X
        by (simp add: Seqptick_projs Refusals_after_def)
          (metis F_imp_front_tickFree append.right_neutral front_tickFree_Nil is_processT9)
    next
      from le_approx2[OF ‹P ⊑ Q›] le_approx2T[OF ‹P ⊑ Q›] le_approx1[OF ‹P ⊑ Q›]
      show ‹t ∉ 𝒟 (P ;✓ R) ⟹ X ∈ ℛa (Q ;✓ R) t ⟹ X ∈ ℛa (P ;✓ R) t› for t X
        by (simp add: subset_iff Seqptick_projs Refusals_after_def)
          (metis D_T is_processT8)
    next

      show ‹t ∈ min_elems (𝒟 (P ;✓ R)) ⟹ t ∈ 𝒯 (Q ;✓ R)› for t
      proof (rule set_mp[OF _ "$"])
        from le_approx2T[OF ‹P ⊑ Q›] le_approx3[OF ‹P ⊑ Q›] show ‹?S P R ⊆ 𝒯 (Q ;✓ R)›
          by (simp add: subset_iff Seqptick_projs)
            (meson D_T elem_min_elems image_iff is_processT9 tickFree_mem_min_elems_D)
      qed
    qed
  next
    show ‹Q ;✓ R ⊑ Q ;✓ S›
    proof (unfold le_approx_def, safe)
      from le_approx1[OF fun_belowD[OF ‹R ⊑ S›]]
      show ‹t ∈ 𝒟 (Q ;✓ S) ⟹ t ∈ 𝒟 (Q ;✓ R)› for t
        unfolding Seqptick_projs by blast
    next
      from proc_ord2a[OF fun_belowD[OF ‹R ⊑ S›]]
      show ‹t ∉ 𝒟 (Q ;✓ R) ⟹ X ∈ ℛa (Q ;✓ R) t ⟹ X ∈ ℛa (Q ;✓ S) t›
        ‹t ∉ 𝒟 (Q ;✓ R) ⟹ X ∈ ℛa (Q ;✓ S) t ⟹ X ∈ ℛa (Q ;✓ R) t› for t X
        by (simp add: Seqptick_projs Refusals_after_def, metis)+
    next
      show ‹t ∈ min_elems (𝒟 (Q ;✓ R)) ⟹ t ∈ 𝒯 (Q ;✓ S)› for t
      proof (rule set_mp[OF _ "$"])
        from le_approx3[OF fun_belowD[OF ‹R ⊑ S›]] show ‹?S Q R ⊆ 𝒯 (Q ;✓ S)›
          by (simp add: subset_iff Seqptick_projs)
            (meson D_T elem_min_elems image_iff tickFree_mem_min_elems_D)
      qed
    qed
  qed
qed



subsection ‹Preliminaries›

context begin

private lemma chain_Seqptick_left: ‹chain Y ⟹ chain (λi. Y i ;✓ S)›
  by (simp add: mono_Seqptick po_class.chain_def)

private lemma chain_Seqptick_right: ‹chain Y ⟹ chain (λi. S ;✓ Y i)›
  by (simp add: mono_Seqptick po_class.chain_def)


private lemma cont_left_prem_Seqptick :
  ‹(⨆i. Y i) ;✓ S = (⨆i. Y i ;✓ S)› (is ‹?lhs = ?rhs›) if ‹chain Y›
  ― ‹We have to add this hypothesis in the generalization.›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (simp add: Seqptick_projs limproc_is_thelub ch2ch_fun ‹chain Y› lub_fun chain_Seqptick_left LUB_projs) blast
next
  have ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› and ‹tF t› for t
  proof (cases ‹map (ev ∘ of_ev) t ∈ 𝒟 (⨆i. Y i)›)
    show ‹map (ev ∘ of_ev) t ∈ 𝒟 (⨆i. Y i) ⟹ t ∈ 𝒟 ?lhs›
      by (simp add: Seqptick_projs)
        (metis append.right_neutral front_tickFree_Nil ‹tF t› tickFree_map_ev_comp tickFree_map_ev_of_ev_eq_iff)
  next
    define T1 and T2
      where ‹T1 i ≡ {t1. ∃t2. t = map (ev ∘ of_ev) t1 @ t2 ∧ t1 ∈ 𝒟 (Y i) ∧ tF t1 ∧ ftF t2}›
        and ‹T2 i ≡ {t1. ∃t2 r. t = map (ev ∘ of_ev) t1 @ t2 ∧ t1 @ [✓(r)] ∈ 𝒯 (Y i) ∧ tF t1 ∧ t2 ∈ 𝒟 (S r)}› for i
    assume ‹map (ev ∘ of_ev) t ∉ 𝒟 (⨆i. Y i)›
    with ‹t ∈ 𝒟 ?rhs› have ‹T1 i ∪ T2 i ≠ {}› for i
      by (simp add: T1_def T2_def limproc_is_thelub chain_Seqptick_left ‹chain Y›
                    LUB_projs Seqptick_projs) fast
    moreover have ‹finite (T1 0 ∪ T2 0)›
      unfolding T1_def T2_def
      by (rule finite_subset[of _ ‹{u. u ≤ map (ev ∘ of_ev) t}›])
        (use tickFree_map_ev_of_ev_eq_iff in ‹force simp add: prefixes_fin›)+
    moreover have ‹T1 (Suc i) ∪ T2 (Suc i) ⊆ T1 i ∪ T2 i› for i
      unfolding T1_def T2_def by (intro allI subsetI; simp)
        (metis (no_types, lifting) ‹chain Y› po_class.chainE le_approx_lemma_T le_approx1
          subsetD[of ‹𝒟 (Y (Suc i))› ‹𝒟 (Y i)›] subsetD[of ‹𝒯 (Y (Suc i))› ‹𝒯 (Y i)› ‹_ @ [✓(_)]›])
    ultimately have ‹(⋂i. T1 i ∪ T2 i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
    then obtain t1 where * : ‹∀i. t1 ∈ T1 i ∪ T2 i› by auto
    then obtain t2 where ** : ‹t = map (ev ∘ of_ev) t1 @ t2› ‹tF t1› ‹ftF t2›
      by (auto simp add: T1_def T2_def dest: D_imp_front_tickFree)
    show ‹t ∈ 𝒟 ?lhs›
    proof (cases ‹∀i. t1 ∈ 𝒟 (Y i)›)
      from "**" show ‹∀i. t1 ∈ 𝒟 (Y i) ⟹ t ∈ 𝒟 ?lhs›
        by (auto simp add: Seqptick_projs limproc_is_thelub ‹chain Y› LUB_projs)
    next
      assume ‹¬ (∀i. t1 ∈ 𝒟 (Y i))›
      then obtain j where *** : ‹j ≤ i ⟹ t1 ∉ 𝒟 (Y i)› for i
        by (meson ‹chain Y› in_mono le_approx_def po_class.chain_mono)
      hence ‹j ≤ i ⟹ t1 ∉ T1 i› for i by (simp add: T1_def)
      with "*" have ‹j ≤ i ⟹ t1 ∈ T2 i› for i by blast
      then obtain r where ‹t1 @ [✓(r)] ∈ 𝒯 (Y j)› ‹t2 ∈ 𝒟 (S r)›
        unfolding T2_def by (auto simp add: "**"(1))
      from this(1) ‹chain Y› "***" have ‹j ≤ i ⟹ t1 @ [✓(r)] ∈ 𝒯 (Y i)› for i
        by (metis eq_imp_le is_processT9 le_approx2T po_class.chain_mono)
      hence ‹t1 @ [✓(r)] ∈ 𝒯 (⨆i. Y i)›
        by (meson "***" ‹chain Y› dual_order.refl is_processT9 is_ub_thelub le_approx2T)
      with ‹t2 ∈ 𝒟 (S r)› "**"(1, 2) show ‹t ∈ 𝒟 ?lhs›
        by (auto simp add: Seqptick_projs)
    qed
  qed
  thus ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (meson D_imp_front_tickFree div_butlast_when_non_tickFree_iff front_tickFree_iff_tickFree_butlast)
next
  show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    by (simp add: Seqptick_projs limproc_is_thelub ch2ch_fun ‹chain Y› lub_fun chain_Seqptick_left LUB_projs) blast
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  from ‹t ∉ 𝒟 ?rhs› obtain j where ‹t ∉ 𝒟 (Y j ;✓ S)›
    by (auto simp add: limproc_is_thelub chain_Seqptick_left ‹chain Y› LUB_projs)
  moreover from ‹(t, X) ∈ ℱ ?rhs› have ‹(t, X) ∈ ℱ (Y j ;✓ S)›
    by (simp add: limproc_is_thelub chain_Seqptick_left ‹chain Y› F_LUB)
  ultimately show ‹(t, X) ∈ ℱ ?lhs›
    by (fact le_approx2[OF mono_Seqptick[OF is_ub_thelub[OF ‹chain Y›] below_refl], THEN iffD2])
qed



lemma ‹finite R ⟹ chain Y ⟹ ⊓r ∈ R. (⨆i. Y i r) = (⨆i. ⊓r ∈ R. Y i r)›
  by (subst cont2contlubE[of ‹GlobalNdet R›, symmetric])
    (simp_all add: lub_fun)


lemma infinite_GlobalNdet_not_cont :
  ― ‹This is a counter example.›
  defines Y_def : ‹Y ≡ λi r :: nat. if r ≤ i then STOP else ⊥ :: (nat, nat) processptick›
  shows ‹chain Y› ‹⊓r ∈ UNIV. (⨆i. Y i r) ≠ (⨆i. ⊓r ∈ UNIV. Y i r)›
proof -
  show *  : ‹chain Y› unfolding Y_def by (auto intro!: chainI fun_belowI)
  have ** : ‹chain (λi. Y i r)› for r by (simp add: ‹chain Y› ch2ch_fun)

  have ‹(⨆i. Y i) = (λr. STOP)›
    by (rule ext, simp add: STOP_iff_T lub_fun limproc_is_thelub T_LUB "*" "**")
      (auto simp add: Y_def T_STOP split: if_split_asm)
  hence $ : ‹⊓r ∈ UNIV. (⨆i. Y i r) = STOP›
    by (simp add: GlobalNdet_is_STOP_iff "*" lub_fun)

  have ‹⊓r ∈ UNIV. Y i r = ⊥› for i
    by (simp add: BOT_iff_Nil_D D_GlobalNdet Y_def D_BOT)
      (use Suc_n_not_le_n in blast)
  hence $$ : ‹(⨆i. ⊓r ∈ UNIV. Y i r) = ⊥› by simp

  from $ $$ show ‹⊓r ∈ UNIV. (⨆i. Y i r) ≠ (⨆i. ⊓r ∈ UNIV. Y i r)› by simp
qed

text ‹The same counter-example works for @{const [source] Seqptick}.›

lemma infinite_Seqptick_not_cont :
  ― ‹This is a counter example.›
  defines P_def : ‹P ≡ SKIPS UNIV :: (nat, nat) processptick›
    and Y_def : ‹Y ≡ λi r :: nat. if r ≤ i then STOP else ⊥ :: (nat, nat) processptick›
  shows ‹chain Y› ‹P ;✓ (⨆i. Y i) ≠ (⨆i. P ;✓ Y i)›
proof -
  show *  : ‹chain Y› unfolding Y_def by (auto intro!: chainI fun_belowI)
  have ‹P ;✓ (⨆i. Y i) = ⊓r ∈ UNIV. (⨆i. Y i r)›
    by (simp add: P_def "*" lub_fun)
  also have ‹… ≠ (⨆i. ⊓r ∈ UNIV. Y i r)›
    unfolding P_def Y_def by (fact infinite_GlobalNdet_not_cont(2))
  also have ‹(⨆i. ⊓r ∈ UNIV. Y i r) = (⨆i. P ;✓ Y i)›
    by (simp add: P_def)
  finally show ‹P ;✓ (⨆i. Y i) ≠ (⨆i. P ;✓ Y i)› .
qed


text ‹We must therefore find a condition under which @{const [source] Seqptick} is continuous.›

private lemma cont_right_prem_Seqptick :
  ‹S ;✓ (⨆i. Y i) = (⨆i. S ;✓ Y i)› (is ‹?lhs = ?rhs›) if ‹chain Y› and ‹𝔽✓(S)›
  ― ‹We have to add this hypothesis in the generalization.›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (simp add: Seqptick_projs limproc_is_thelub ch2ch_fun ‹chain Y› lub_fun chain_Seqptick_right D_LUB) blast
next
  have ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› and ‹tF t› for t
  proof (cases ‹map (ev ∘ of_ev) t ∈ 𝒟 S›)
    show ‹map (ev ∘ of_ev) t ∈ 𝒟 S ⟹ t ∈ 𝒟 ?lhs›
      by (simp add: Seqptick_projs)
        (metis append.right_neutral front_tickFree_Nil ‹tF t› tickFree_map_ev_comp tickFree_map_ev_of_ev_eq_iff)
  next
    define T where ‹T i ≡ {t1. ∃t2 r. t = map (ev ∘ of_ev) t1 @ t2 ∧ t1 @ [✓(r)] ∈ 𝒯 S ∧ tF t1 ∧ t2 ∈ 𝒟 (Y i r)}› for i
    assume ‹map (ev ∘ of_ev) t ∉ 𝒟 S›
    with ‹t ∈ 𝒟 ?rhs› have ‹T i ≠ {}› for i
      by (fastforce simp add: T_def limproc_is_thelub chain_Seqptick_right ‹chain Y›
                    D_LUB Seqptick_projs is_processT7 tickFree_map_ev_of_ev_same_type_is)
    moreover have ‹finite (T 0)›
      unfolding T_def
      by (rule finite_subset[of _ ‹{u. u ≤ map (ev ∘ of_ev) t}›])
        (use tickFree_map_ev_of_ev_eq_iff in ‹force simp add: prefixes_fin›)+
    moreover have ‹T (Suc i) ⊆ T i› for i
      unfolding T_def by (intro allI Un_mono subsetI; simp)
        (metis ‹chain Y› fun_below_iff subset_iff[of ‹𝒟 (Y (Suc i) _)› ‹𝒟 (Y i _)›]
               po_class.chainE le_approx1)
    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 * : ‹t = map (ev ∘ of_ev) t1 @ t2›
      ‹tF t1› ‹∀i. ∃r. t1 @ [✓(r)] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y i r)›
      by (simp add: T_def) blast
    have ‹t1 ∈ 𝒯 S› by (meson "*"(3) prefixI is_processT3_TR)
    from "*"(1, 2) ‹map (ev ∘ of_ev) t ∉ 𝒟 S›
    have ‹t1 ∉ 𝒟 S› using is_processT7 tickFree_map_ev_of_ev_eq_iff by fastforce
    define U where ‹U i ≡ {r. t1 @ [✓(r)] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y i r)}› for i
    from "*"(3) have ‹U i ≠ {}› for i by (simp add: U_def)
    moreover have ‹finite (U 0)›
    proof (rule finite_subset[of _ ‹{r. t1 @ [✓(r)] ∈ 𝒯 S}›])
      show ‹U 0 ⊆ {r. t1 @ [✓(r)] ∈ 𝒯 S}› unfolding U_def by blast
    next
      show ‹finite {r. t1 @ [✓(r)] ∈ 𝒯 S}›
        by (simp add: ‹𝔽✓(S)› ‹t1 ∉ 𝒟 S› finite_ticksD)
    qed
    moreover have ‹U (Suc i) ⊆ U i› for i
      by (simp add: U_def subset_iff)
        (meson fun_below_iff in_mono le_approx1 chainE ‹chain Y›)
    ultimately have ‹(⋂i. U i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
    then obtain r where ** : ‹∀i. r ∈ U i› by auto
    with "*" show ‹t ∈ 𝒟 ?lhs›
      by (simp add: Seqptick_projs U_def ‹chain Y› ch2ch_fun limproc_is_thelub D_LUB lub_fun) blast
  qed
  thus ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (meson D_imp_front_tickFree div_butlast_when_non_tickFree_iff front_tickFree_iff_tickFree_butlast)
next
  show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    by (simp add: Seqptick_projs limproc_is_thelub ch2ch_fun ‹chain Y› lub_fun chain_Seqptick_right F_LUB) blast
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  from ‹t ∉ 𝒟 ?rhs› obtain j where ‹t ∉ 𝒟 (S ;✓ Y j)›
    by (auto simp add: limproc_is_thelub chain_Seqptick_right ‹chain Y› D_LUB)
  moreover from ‹(t, X) ∈ ℱ ?rhs› have ‹(t, X) ∈ ℱ (S ;✓ Y j)›
    by (simp add: limproc_is_thelub chain_Seqptick_right ‹chain Y› F_LUB)
  ultimately show ‹(t, X) ∈ ℱ ?lhs›
    by (fact le_approx2[OF mono_Seqptick[OF below_refl is_ub_thelub[OF ‹chain Y›]], THEN iffD2])
qed



subsection ‹Continuity›

text ‹
We then spent a lot of time trying to prove the continuity
under the assumption of const‹finite_ticks_fun›.
›


lemma Seqptick_cont [simp] : ‹cont (λx. f x ;✓ g x)›
  if ‹cont f› and ‹cont g› and ‹𝔽✓⇒(f)›
  for g :: ‹_ ⇒ _ ⇒ ('a, 's) processptick›
proof (rule cont_apply[where f = ‹λx y. f x ;✓ y›])
  show ‹cont g› by (fact ‹cont g›)
next
  show ‹cont (λx. f x ;✓ y)› for y :: ‹_ ⇒ ('a, 's) processptick›
  proof (rule contI2)
    show ‹monofun (λx. f x ;✓ y)› by (simp add: cont2monofunE mono_Seqptick 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_Seqptick ‹cont f›)
  qed
next
  show ‹cont (λy :: _ ⇒ ('a, 's) processptick. f x ;✓ y)› for x
  proof (rule contI2)
    show ‹monofun ((;✓) (f x))› by (simp add: mono_Seqptick monofunI)
  next
    show ‹chain Y ⟹ f x ;✓ (⨆i. Y i) ⊑ (⨆i. f x ;✓ Y i)›
    for Y :: ‹_ ⇒ _ ⇒ ('a, 's) processptick›
      oops
        ― ‹Unfortunately here, we cannot use @{thm [source] cont_right_prem_Seqptick}
    since there is no reason for term‹𝔽✓(x)› to hold.
    Actually, we can find a counter example.›


text ‹
We could therefore only prove the weaker following version.
›


lemma Seqptick_cont [simp] : ‹cont (λx. f x ;✓ g x)›
  if ‹cont f› and ‹cont g› and ‹⋀x. 𝔽✓(f x)›
  for g :: ‹_ ⇒ _ ⇒ ('a, 's) processptick›
proof (rule cont_apply[where f = ‹λx y. f x ;✓ y›])
  show ‹cont g› by (fact ‹cont g›)
next
  show ‹cont (λx. f x ;✓ y)› for y :: ‹_ ⇒ ('a, 's) processptick›
  proof (rule contI2)
    show ‹monofun (λx. f x ;✓ y)› by (simp add: cont2monofunE mono_Seqptick 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_Seqptick ‹cont f›)
  qed
next
  show ‹cont (λy :: _ ⇒ ('a, 's) processptick. f x ;✓ y)› for x
  proof (rule contI2)
    show ‹monofun ((;✓) (f x))› by (simp add: mono_Seqptick monofunI)
  next
    show ‹chain Y ⟹ f x ;✓ (⨆i. Y i) ⊑ (⨆i. f x ;✓ Y i)›
      for Y :: ‹_ ⇒ _ ⇒ ('a, 's) processptick›
      by (simp add: cont_right_prem_Seqptick ‹⋀x. 𝔽✓(f x)›)
  qed
qed

end (* private context *)


corollary ‹cont f ⟹ cont g ⟹ cont (λx. f x ;✓ g x)›
  for f :: ‹'b :: cpo ⇒ ('a, 'r :: finite) processptick› 
  by (simp add: finite_ticks_simps(5))




lemma MultiSeqptick_cont[simp]:
  ‹⟦⋀l. l ∈ set L ⟹ cont (f l); ⋀l r x. l ∈ set (butlast L) ⟹ 𝔽✓(f l x r)⟧
   ⟹ cont (λx. (SEQ✓ l ∈@ L. f l x) r)›
proof (induct L arbitrary: r)
  show ‹⋀r. cont (λx. (SEQ✓ l ∈@ []. f l x) r)› by simp
next
  case (Cons l0 L)
  show ‹cont (λx. (SEQ✓ l ∈@ (l0 # L). f l x) r)›
  proof (cases ‹L = []›)
    show ‹L = [] ⟹ cont (λx. (SEQ✓ l ∈@ (l0 # L). f l x) r)›
      by (simp add: Cons.prems(1) cont2cont_fun)
  next
    show ‹cont (λx. (SEQ✓ l ∈@ (l0 # L). f l x) r)› if ‹L ≠ []›
    proof (subst MultiSeqptick_Cons, intro cont2cont_lambda Seqptick_cont)
      show ‹cont (λx. f l0 x r)› by (simp add: Cons.prems(1) cont2cont_fun)
    next
      have ‹cont (λx. (SEQ✓ l ∈@ L. f l x))›
        by (rule cont2cont_lambda, rule Cons.hyps)
          (simp_all add: Cons.prems(1, 2) ‹L ≠ []›)
      thus ‹cont (λx. (SEQ✓ l ∈@ L. f l x) y)› for y
        by (fact cont2cont_fun)
    next
      show ‹𝔽✓(f l0 x r)› for x by (simp add: Cons.prems(2) that)
    qed
  qed
qed



(*<*)
end
  (*>*)