Theory Seq
section‹The Sequence Operator›
theory Seq
imports Process
begin
subsection‹Definition›
abbreviation "div_seq P Q ≡ {t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2}
∪ {t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}"
definition Seq :: "['a process,'a process] ⇒ 'a process" (infixl "❙;" 74)
where "P ❙; Q ≡ Abs_process
({(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
{(t, X). t ∈ div_seq P Q},
div_seq P Q)"
lemma Seq_maintains_is_process:
"is_process ({(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
{(t, X). t ∈ div_seq P Q},
div_seq P Q)"
(is "is_process(?f, ?d)")
proof(simp only: fst_conv snd_conv Failures_def is_process_def FAILURES_def DIVERGENCES_def,
fold FAILURES_def DIVERGENCES_def,fold Failures_def,intro conjI)
show "([], {}) ∈ ?f"
apply(cases "[tick] ∈ 𝒯 P", simp_all add: is_processT1)
using F_T is_processT5_S6 by blast
next
show " ∀s X. (s, X) ∈ ?f ⟶ front_tickFree s"
by (auto simp:is_processT2 append_T_imp_tickFree front_tickFree_append D_imp_front_tickFree)
next
show "∀s t. (s @ t, {}) ∈ ?f ⟶ (s, {}) ∈ ?f"
apply auto
apply (metis F_T append_Nil2 is_processT is_processT3_SR is_processT5_S3)
apply(simp add:append_eq_append_conv2)
apply (metis T_F_spec append_Nil2 is_processT is_processT5_S4)
apply (metis append_self_conv front_tickFree_append front_tickFree_mono is_processT2_TR
no_Trace_implies_no_Failure non_tickFree_implies_nonMt non_tickFree_tick)
apply (metis (mono_tags, lifting) F_T append_Nil2 is_processT5_S3 process_charn)
apply (metis front_tickFree_append front_tickFree_mono self_append_conv)
apply(simp add:append_eq_append_conv2)
apply (metis T_F_spec append_Nil2 is_processT is_processT5_S4)
by (metis D_imp_front_tickFree append_T_imp_tickFree front_tickFree_append
front_tickFree_mono not_Cons_self2 self_append_conv)
next
show "∀s X Y. (s, Y) ∈ ?f ∧ X ⊆ Y ⟶ (s, X) ∈ ?f"
apply auto
apply (metis insert_mono is_processT4_S1 prod.sel(1) prod.sel(2))
apply (metis is_processT4)
apply (simp add: append_T_imp_tickFree)
by (metis process_charn)
next
{ fix sa X Y
have "(sa, X ∪ {tick}) ∈ ℱ P ⟹
tickFree sa ⟹
∀c. c ∈ Y ∧ c ≠ tick ⟶ (sa @ [c], {}) ∉ ℱ P ⟹
(sa, X ∪ Y ∪ {tick}) ∈ ℱ P ∧ tickFree sa"
apply(rule_tac t="X ∪ Y ∪ {tick}" and s="X ∪ {tick} ∪ (Y-{tick})" in subst,auto)
by (metis DiffE Un_insert_left is_processT5 singletonI)
} note is_processT5_SEQH3 = this
have is_processT5_SEQH4 :
"⋀ sa X Y. (sa, X ∪ {tick}) ∈ ℱ P
⟹ tickFree sa
⟹ ∀c. c ∈ Y ⟶ (sa@[c],{tick}) ∉ ℱ P ∨ ¬ tickFree(sa@[c])
⟹ ∀c. c ∈ Y ⟶ (∀t1 t2. sa@[c]≠t1@t2 ∨ t1@[tick]∉𝒯 P ∨ (t2,{})∉ℱ Q)
⟹ (sa, X ∪ Y ∪ {tick}) ∈ ℱ P ∧ tickFree sa"
by (metis append_Nil2 is_processT1 is_processT5_S3 is_processT5_SEQH3
no_Trace_implies_no_Failure tickFree_Cons tickFree_append)
let ?f1 = "{(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q}"
have is_processT5_SEQ2: "⋀ sa X Y. (sa, X) ∈ ?f1
⟹ (∀c. c ∈ Y ⟶ (sa@[c], {})∉?f)
⟹ (sa, X∪Y) ∈ ?f1"
apply (clarsimp,rule is_processT5_SEQH4[simplified])
by (auto simp: is_processT5)
show "∀s X Y. (s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟶ (s, X ∪ Y) ∈ ?f"
apply(intro allI impI, elim conjE UnE)
apply(rule rev_subsetD)
apply(rule is_processT5_SEQ2)
apply auto
using is_processT5_S1 apply force
apply (simp add: append_T_imp_tickFree)
using is_processT5[rule_format, OF conjI] by force
next
show "∀s X. (s @ [tick], {}) ∈ ?f ⟶ (s, X - {tick}) ∈ ?f"
apply auto
apply (metis (no_types, lifting) append_T_imp_tickFree butlast_append
butlast_snoc is_processT2 is_processT6 nonTickFree_n_frontTickFree
non_tickFree_tick tickFree_append)
apply (metis append_T_imp_tickFree front_tickFree_append front_tickFree_mono
is_processT2 non_tickFree_implies_nonMt non_tickFree_tick)
apply (metis process_charn)
apply (metis front_tickFree_append front_tickFree_implies_tickFree)
apply (metis D_T T_nonTickFree_imp_decomp append_T_imp_tickFree append_assoc
append_same_eq non_tickFree_implies_nonMt non_tickFree_tick process_charn
tickFree_append)
by (metis D_imp_front_tickFree append_T_imp_tickFree front_tickFree_append
front_tickFree_mono non_tickFree_implies_nonMt non_tickFree_tick)
next
show "∀s t. s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ ?d"
apply auto
using front_tickFree_append apply blast
by (metis process_charn)
next
show "∀s X. s ∈ ?d ⟶ (s, X) ∈ ?f"
by blast
next
show "∀s. s @ [tick] ∈ ?d ⟶ s ∈ ?d"
apply auto
apply (metis append_Nil2 front_tickFree_implies_tickFree process_charn)
by (metis append1_eq_conv append_assoc front_tickFree_implies_tickFree is_processT2_TR
nonTickFree_n_frontTickFree non_tickFree_tick process_charn tickFree_append)
qed
subsection‹The Projections›
lemmas Rep_Abs_Seq[simp] = Abs_process_inverse[simplified, OF Seq_maintains_is_process]
lemma
F_Seq : "ℱ (P ❙; Q) = {(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}"
unfolding Seq_def by(subst Failures_def, simp only:Rep_Abs_Seq, auto simp: FAILURES_def)
lemma
D_Seq : "𝒟 (P ❙; Q) = {t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2} ∪
{t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}"
unfolding Seq_def by(subst D_def,simp only:Rep_Abs_Seq, simp add:DIVERGENCES_def)
lemma
T_Seq : "𝒯 (P ❙; Q) = {t. ∃ X. (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
{t. ∃ t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q} ∪
{t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2} ∪
{t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q} ∪
{t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2} ∪
{t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}"
unfolding Seq_def
apply(subst Traces_def, simp only: Rep_Abs_Seq, auto simp: TRACES_def FAILURES_def)
using F_T apply fastforce
apply (simp add: append_T_imp_tickFree)
using F_T apply fastforce
using T_F by blast
subsection‹ Continuity Rule ›
lemma mono_Seq_D11:
"P ⊑ Q ⟹ 𝒟 (Q ❙; S) ⊆ 𝒟 (P ❙; S)"
apply(auto simp: D_Seq)
using le_approx1 apply blast
using le_approx_lemma_T by blast
lemma mono_Seq_D12:
assumes ordered: "P ⊑ Q"
shows "(∀ s. s ∉ 𝒟 (P ❙; S) ⟶ Ra (P ❙; S) s = Ra (Q ❙; S) s)"
proof -
have mono_SEQI2a:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (P ❙; S) ⟶ Ra (Q ❙; S) s ⊆ Ra (P ❙; S) s"
apply(simp add: Ra_def D_Seq F_Seq)
apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q], auto)
using le_approx1 by blast+
have mono_SEQI2b:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (P ❙; S) ⟶ Ra (P ❙; S) s ⊆ Ra (Q ❙; S) s"
apply(simp add: Ra_def D_Seq F_Seq)
apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q]
le_approx1[of P Q] le_approx2T[of P Q], auto)
using le_approx2 apply fastforce
apply (metis front_tickFree_implies_tickFree is_processT2_TR process_charn)
apply (simp add: append_T_imp_tickFree)
by (metis front_tickFree_implies_tickFree is_processT2_TR process_charn)
show ?thesis
using ordered mono_SEQI2a mono_SEQI2b by(blast)
qed
lemma minSeqInclu:
"min_elems(𝒟 (P ❙; S))
⊆ min_elems(𝒟 P) ∪ {t1@t2|t1 t2. t1@[tick]∈𝒯 P∧t1∉𝒟 P∧t2∈min_elems(𝒟 S)}"
apply(auto simp: D_Seq min_elems_def)
apply (meson process_charn)
apply (metis append_Nil2 front_tickFree_Nil front_tickFree_append front_tickFree_mono
le_list_def less_list_def)
apply (metis (no_types, lifting) D_imp_front_tickFree Nil_is_append_conv append_T_imp_tickFree
append_butlast_last_id butlast_append process_charn less_self lim_proc_is_lub3a
list.distinct(1) nil_less)
by (metis D_imp_front_tickFree append_Nil2 front_tickFree_Nil front_tickFree_mono process_charn
list.distinct(1) nonTickFree_n_frontTickFree)
lemma mono_Seq_D13 :
assumes ordered: "P ⊑ Q"
shows "min_elems (𝒟 (P ❙; S)) ⊆ 𝒯 (Q ❙; S)"
apply (insert ordered, frule le_approx3, rule subset_trans [OF minSeqInclu])
apply (auto simp: F_Seq T_Seq min_elems_def append_T_imp_tickFree)
apply(rule_tac x="{}" in exI, rule is_processT5_S3)
apply (metis (no_types, lifting) T_F elem_min_elems le_approx3 less_list_def min_elems5 subset_eq)
using Nil_elem_T no_Trace_implies_no_Failure apply fastforce
apply (metis (no_types, lifting) less_self nonTickFree_n_frontTickFree process_charn)
apply(rule_tac x="{}" in exI, metis (no_types, lifting) le_approx2T process_charn)
by (metis (no_types, lifting) less_self nonTickFree_n_frontTickFree process_charn)
lemma mono_Seq[simp] : "P ⊑ Q ⟹ (P ❙; S) ⊑ (Q ❙; S)"
by (auto simp: le_approx_def mono_Seq_D11 mono_Seq_D12 mono_Seq_D13)
lemma mono_Seq_D21:
"P ⊑ Q ⟹ 𝒟 (S ❙; Q) ⊆ 𝒟 (S ❙; P)"
apply(auto simp: D_Seq)
using le_approx1 by blast
lemma mono_Seq_D22:
assumes ordered: "P ⊑ Q"
shows "(∀ s. s ∉ 𝒟 (S ❙; P) ⟶ Ra (S ❙; P) s = Ra (S ❙; Q) s)"
proof -
have mono_SEQI2a:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (S ❙; P) ⟶ Ra (S ❙; Q) s ⊆ Ra (S ❙; P) s"
apply(simp add: Ra_def D_Seq F_Seq)
apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q], auto)
using le_approx1 by fastforce+
have mono_SEQI2b:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (S ❙; P) ⟶ Ra (S ❙; P) s ⊆ Ra (S ❙; Q) s"
apply(simp add: Ra_def D_Seq F_Seq)
apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q]
le_approx1[of P Q] le_approx2T[of P Q], auto)
using le_approx2 by fastforce+
show ?thesis
using ordered mono_SEQI2a mono_SEQI2b by(blast)
qed
lemma mono_Seq_D23 :
assumes ordered: "P ⊑ Q"
shows "min_elems (𝒟 (S ❙; P)) ⊆ 𝒯 (S ❙; Q)"
apply (insert ordered, frule le_approx3, auto simp: D_Seq T_Seq min_elems_def)
apply (metis (no_types, lifting) D_imp_front_tickFree Nil_elem_T append.assoc below_refl
front_tickFree_charn less_self min_elems2 no_Trace_implies_no_Failure)
apply (simp add: append_T_imp_tickFree)
by (metis (no_types, lifting) D_def D_imp_front_tickFree append_butlast_last_id append_is_Nil_conv
butlast_append butlast_snoc is_process9 is_process_Rep less_self nonTickFree_n_frontTickFree)
lemma mono_Seq_sym[simp] : "P ⊑ Q ⟹ (S ❙; P) ⊑ (S ❙; Q)"
by (auto simp: le_approx_def mono_Seq_D21 mono_Seq_D22 mono_Seq_D23)
lemma chain_Seq1: "chain Y ⟹ chain (λi. Y i ❙; S)"
by(simp add: chain_def)
lemma chain_Seq2: "chain Y ⟹ chain (λi. S ❙; Y i)"
by(simp add: chain_def)
lemma limproc_Seq_D1: "chain Y ⟹ 𝒟 (lim_proc (range Y) ❙; S) = 𝒟 (lim_proc (range (λi. Y i ❙; S)))"
apply(auto simp:Process_eq_spec D_Seq F_Seq F_LUB D_LUB T_LUB chain_Seq1)
apply(blast)
proof -
fix x
assume A:"∀xa. (∃t1 t2. x = t1 @ t2 ∧ t1 ∈ 𝒟 (Y xa) ∧ tickFree t1 ∧ front_tickFree t2) ∨
(∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y xa) ∧ t2 ∈ 𝒟 S)"
and B: "∀t1 t2. x = t1 @ t2 ⟶ (∃x. t1 @ [tick] ∉ 𝒯 (Y x)) ∨ t2 ∉ 𝒟 S"
and C: "chain Y"
thus "∃t1 t2. x = t1 @ t2 ∧ (∀x. t1 ∈ 𝒟 (Y x)) ∧ tickFree t1 ∧ front_tickFree t2"
proof (cases "∃n. ∀t1 ≤ x. t1 ∉ 𝒟 (Y n)")
case True
then obtain n where "∀t1 ≤ x. t1 ∉ 𝒟 (Y n)" by blast
with A B C show ?thesis
apply(erule_tac x=n in allE, elim exE disjE, auto simp add:le_list_def)
by (metis D_T chain_lemma is_processT le_approx2T)
next
case False
from False obtain t1 where D:"t1 ≤ x ∧ (∀n. ∀t ≤ x. t ∈ 𝒟 (Y n) ⟶ t ≤ t1)" by blast
with False have E:"∀n. t1 ∈ 𝒟 (Y n)"
by (metis append_Nil2 append_T_imp_tickFree front_tickFree_append front_tickFree_mono
is_processT le_list_def local.A not_Cons_self2)
from A B C D E show ?thesis
by (metis D_imp_front_tickFree Traces_def append_Nil2 front_tickFree_append
front_tickFree_implies_tickFree front_tickFree_mono is_processT
is_process_Rep le_list_def nonTickFree_n_frontTickFree
trace_with_Tick_implies_tickFree_front)
qed
qed
lemma limproc_Seq_F1: "chain Y ⟹ ℱ (lim_proc (range Y) ❙; S) = ℱ (lim_proc (range (λi. Y i ❙; S)))"
apply(auto simp add:Process_eq_spec D_Seq F_Seq F_LUB D_LUB T_LUB chain_Seq1)
proof (auto, goal_cases)
case (1 a b x)
then show ?case
apply(erule_tac x=x in allE, elim disjE exE, auto simp add: is_processT7 is_processT8_S)
apply(rename_tac t1 t2, erule_tac x=t1 in allE, erule_tac x=t1 in allE, erule_tac x=t1 in allE)
apply (metis D_T append_T_imp_tickFree chain_lemma is_processT le_approx2T not_Cons_self2)
by (metis D_T append_T_imp_tickFree chain_lemma is_processT le_approx2T not_Cons_self2)
next
case (2 a b)
assume A1:"∀t1 t2. a = t1 @ t2 ⟶ (∃x. t1 @ [tick] ∉ 𝒯 (Y x)) ∨ t2 ∉ 𝒟 S"
and A2:"∀t1. tickFree t1 ⟶ (∀t2. a = t1 @ t2 ⟶ (∃x. t1 ∉ 𝒟 (Y x)) ∨ ¬ front_tickFree t2)"
and A3:"∀t1 t2. a = t1 @ t2 ⟶ (∃x. t1 @ [tick] ∉ 𝒯 (Y x)) ∨ (t2, b) ∉ ℱ S"
and B: "∀x. (a, insert tick b) ∈ ℱ (Y x) ∧ tickFree a ∨
(∃t1 t2. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y x) ∧ (t2, b) ∈ ℱ S) ∨
(∃t1 t2. a = t1 @ t2 ∧ t1 ∈ 𝒟 (Y x) ∧ tickFree t1 ∧ front_tickFree t2) ∨
(∃t1 t2. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y x) ∧ t2 ∈ 𝒟 S)"
and C:"chain Y"
have E:"¬ tickFree a ⟹ False"
proof -
assume F:"¬ tickFree a"
from A obtain f
where D:"f = (λt2. {n. ∃t1. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y n) ∧ (t2, b) ∈ ℱ S}
∪ {n. ∃t1. a = t1 @ t2 ∧ t1 ∈ 𝒟 (Y n) ∧ tickFree t1 ∧ front_tickFree t2})"
by simp
with B F have "∀n. n ∈ (⋃x∈{t. ∃t1. a = t1 @ t}. f x)"
(is "∀n. n ∈ ?S f") using NF_ND by fastforce
hence "infinite (?S f)" by (simp add: Sup_set_def)
then obtain t2 where E:"t2∈{t. ∃t1. a = t1 @ t} ∧ infinite (f t2)" using suffixes_fin by blast
{ assume E1:"infinite{n. ∃t1. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y n) ∧ (t2, b) ∈ ℱ S}"
(is "infinite ?E1")
with E obtain t1 where F:"a = t1 @ t2 ∧ (t2, b) ∈ ℱ S" using D not_finite_existsD by blast
with A3 obtain m where G:"t1@ [tick] ∉ 𝒯 (Y m)" by blast
with E1 obtain n where "n ≥ m ∧ n ∈ ?E1" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
with D have "n ≥ m ∧ t1@ [tick] ∈ 𝒯 (Y n)" by (simp add: F)
with G C have False using le_approx_lemma_T chain_mono by blast
} note E1 = this
{ assume E2:"infinite{n. ∃t1. a = t1 @ t2 ∧ t1 ∈ 𝒟 (Y n) ∧ tickFree t1 ∧ front_tickFree t2}"
(is "infinite ?E2")
with E obtain t1 where F:"a = t1 @ t2 ∧ tickFree t1 ∧ front_tickFree t2"
using D not_finite_existsD by blast
with A2 obtain m where G:"t1 ∉ 𝒟 (Y m)" by blast
with E2 obtain n where "n ≥ m ∧ n ∈ ?E2" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
with D have "n ≥ m ∧ t1 ∈ 𝒟 (Y n)" by (simp add: F)
with G C have False using le_approx1 chain_mono by blast
} note E2 = this
from D E E1 E2 show False by blast
qed
from E show "tickFree a" by blast
qed
lemma cont_left_D_Seq : "chain Y ⟹ ((⨆ i. Y i) ❙; S) = (⨆ i. (Y i ❙; S))"
by (simp add: Process_eq_spec chain_Seq1 limproc_Seq_D1 limproc_Seq_F1 limproc_is_thelub)
lemma limproc_Seq_D2: "chain Y ⟹ 𝒟 (S ❙; lim_proc (range Y)) = 𝒟 (lim_proc (range (λi. S ❙; Y i )))"
apply(auto simp add:Process_eq_spec D_Seq F_Seq F_LUB D_LUB T_LUB chain_Seq2)
apply(blast)
proof -
fix x
assume A:"∀t1. t1 @ [tick] ∈ 𝒯 S ⟶ (∀t2. x = t1 @ t2 ⟶ (∃x. t2 ∉ 𝒟 (Y x)))"
and B: "∀n. ∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y n)"
and C: "chain Y"
from A obtain f where D:"f = (λt2. {n. ∃t1. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y n)})"
by simp
with B have "∀n. n ∈ (⋃x∈{t. ∃t1. x = t1 @ t}. f x)" (is "∀n. n ∈ ?S f") by fastforce
hence "infinite (?S f)" by (simp add: Sup_set_def)
then obtain t2 where E:"t2∈{t. ∃t1. x = t1 @ t} ∧ infinite (f t2)" using suffixes_fin by blast
then obtain t1 where F:"x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S" using D not_finite_existsD by blast
from A F obtain m where G:"t2 ∉ 𝒟 (Y m)" by blast
with E obtain n where "n ≥ m ∧ n ∈ (f t2)" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
with D have "n ≥ m ∧ t2 ∈ 𝒟 (Y n)" by blast
with G C have False using le_approx1 po_class.chain_mono by blast
thus "∃t1 t2. x = t1 @ t2 ∧ t1 ∈ 𝒟 S ∧ tickFree t1 ∧ front_tickFree t2" ..
qed
lemma limproc_Seq_F2:
"chain Y ⟹ ℱ (S ❙; lim_proc (range Y)) = ℱ (lim_proc (range (λi. S ❙; Y i )))"
apply(auto simp:Process_eq_spec D_Seq F_Seq T_Seq F_LUB D_LUB D_LUB_2 T_LUB T_LUB_2 chain_Seq2 del:conjI)
apply(auto)[1]
apply(auto)[1]
proof-
fix x X
assume A:"∀t1. t1 @ [tick] ∈ 𝒯 S ⟶ (∀t2. x = t1 @ t2 ⟶ (∃m. (t2, X) ∉ ℱ (Y m)))"
and B: "∀n. (∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (t2, X) ∈ ℱ (Y n)) ∨
(∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y n))"
and C: "chain Y"
hence D:"∀n. (∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (t2, X) ∈ ℱ (Y n))" by (meson NF_ND)
from A obtain f where D:"f = (λt2. {n. ∃t1. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (t2, X) ∈ ℱ (Y n)})"
by simp
with D have "∀n. n ∈ (⋃x∈{t. ∃t1. x = t1 @ t}. f x)" using B NF_ND by fastforce
hence "infinite (⋃x∈{t. ∃t1. x = t1 @ t}. f x)" by (simp add: Sup_set_def)
then obtain t2 where E:"t2∈{t. ∃t1. x = t1 @ t} ∧ infinite (f t2)" using suffixes_fin by blast
then obtain t1 where F:"x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S" using D not_finite_existsD by blast
from A F obtain m where G:"(t2, X) ∉ ℱ (Y m)" by blast
with E obtain n where "n ≥ m ∧ n ∈ (f t2)" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
with D have "n ≥ m ∧ (t2, X) ∈ ℱ (Y n)" by blast
with G C have False using is_processT8 po_class.chain_mono proc_ord2a by blast
thus "(x, insert tick X) ∈ ℱ S ∧ tickFree x" ..
qed
lemma cont_right_D_Seq : "chain Y ⟹ (S ❙; (⨆ i. Y i)) = (⨆ i. (S ❙; Y i))"
by (simp add: Process_eq_spec chain_Seq2 limproc_Seq_D2 limproc_Seq_F2 limproc_is_thelub)
lemma Seq_cont[simp]:
assumes f:"cont f"
and g:"cont g"
shows "cont (λx. f x ❙; g x)"
proof -
have A : "⋀x. cont g ⟹ cont (λy. y ❙; g x)"
apply (rule contI2, rule monofunI)
apply (auto)
by (simp add: cont_left_D_Seq)
have B : "⋀y. cont g ⟹ cont (λx. y ❙; g x)"
apply (rule_tac c="(λ x. y ❙; x)" in cont_compose)
apply (rule contI2,rule monofunI)
by (auto simp add: chain_Seq2 cont_right_D_Seq)
show ?thesis using f g
apply(rule_tac f="(λx. (λ f. f ❙; g x))" in cont_apply)
by(auto intro:contI2 monofunI simp:A B)
qed
end