Theory Hiding
chapter‹Concurrent CSP Operators›
section‹The Hiding Operator›
theory Hiding
imports Process
begin
subsection‹Preliminaries : primitives and lemmas›
abbreviation "trace_hide t A ≡ filter (λx. x ∉ A) t"
lemma Hiding_tickFree : "tickFree s ⟷ tickFree (trace_hide s (ev`A))"
by (auto simp add: tickFree_def)
lemma Hiding_fronttickFree : "front_tickFree s ⟹ front_tickFree (trace_hide s (ev`A))"
apply(auto simp add: front_tickFree_charn tickFree_def split:if_splits)
by (metis Hiding_tickFree list_nonMt_append tickFree_append tickFree_def)
lemma trace_hide_union[simp] : "trace_hide t (ev ` (A ∪ B)) = trace_hide (trace_hide t (ev ` A)) (ev ` B)"
by (subgoal_tac "ev ` (A ∪ B) = (ev ` A) ∪ (ev ` B)") auto
abbreviation "isInfHiddenRun f P A ≡ strict_mono f ∧ (∀ i. f i ∈ 𝒯 P) ∧
(∀ i. trace_hide (f i) (ev ` A) = trace_hide (f (0::nat)) (ev ` A))"
lemma isInfHiddenRun_1: "isInfHiddenRun f P A ⟷ strict_mono f ∧ (∀ i. f i ∈ 𝒯 P) ∧
(∀i. ∃t. f i = f 0 @ t ∧ set t ⊆ (ev ` A))"
(is "?A ⟷ ?B")
proof
assume A: ?A
{
fix i
from A have "f 0 ≤ f i" using strict_mono_less_eq by blast
then obtain t where B:"f i = f 0 @ t" by (metis le_list_def)
hence "trace_hide (f i) (ev ` A) = (trace_hide (f 0) (ev ` A)) @ (trace_hide t (ev ` A))" by simp
with A have "trace_hide t (ev ` A) = []" by (metis append_self_conv)
with B have "∃t. f i = f 0 @ t ∧ set t ⊆ (ev ` A)"
using filter_empty_conv[of "λx. x ∉ (ev ` A)"] by auto
}
with A show ?B by simp
next
assume B: ?B
{
fix i
from B obtain t where B:"f i = f 0 @ t" and "set t ⊆ (ev ` A)" by blast
hence "trace_hide (f i) (ev ` A) = (trace_hide (f 0) (ev ` A))" by (simp add: subset_iff)
}
with B show ?A by simp
qed
abbreviation "div_hide P A ≡ {s. ∃ t u. front_tickFree u ∧
tickFree t ∧ s = trace_hide t (ev ` A) @ u ∧
(t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P A ∧ t ∈ range f))}"
lemma inf_hidden:
assumes as1:"∀t. trace_hide t (ev ` A) = trace_hide s (ev ` A) ⟶ (t, ev ` A) ∉ ℱ P"
and as2:"s ∈ 𝒯 P"
shows "∃f. isInfHiddenRun f P A ∧ s ∈ range f"
proof
define f where A:"f = rec_nat s (λi t. (let e = SOME e. e ∈ ev`A ∧ t @ [e] ∈ 𝒯 P in t @ [e]))"
hence B:"strict_mono f" by (simp add:strict_mono_def lift_Suc_mono_less_iff)
from A have C:"s ∈ range f"
by (metis (mono_tags, lifting) old.nat.simps(6) range_eqI)
{ fix i
have "f i ∈ 𝒯 P ∧ trace_hide (f i) (ev ` A) = (trace_hide s (ev ` A))"
proof(induct i, simp add: A Nil_elem_T as2)
case (Suc i)
with as1[THEN spec, of "f i"] have a:"∃e. e ∈ ev`A ∧ f i @ [e] ∈ 𝒯 P"
using is_processT5_S7 by force
from A have b:"f (Suc i) = (let e = SOME e. e ∈ ev`A ∧ f i @ [e] ∈ 𝒯 P in f i @ [e])"
by simp
with Suc a[THEN someI_ex] show ?case by simp
qed
}
with B C show "isInfHiddenRun f P A ∧ s ∈ range f" by simp
qed
lemma trace_hide_append: "s @ t = trace_hide ta (ev ` A) ⟹ ∃ss tt. ta = ss@tt ∧
s = trace_hide ss (ev ` A) ∧
t = trace_hide tt (ev ` A)"
proof(induct "ta" arbitrary:s t)
case Nil thus ?case by simp
next
case (Cons a ta) thus ?case
proof(cases "a ∈ (ev ` A)")
case True
hence "s @ t = trace_hide ta (ev ` A)" by (simp add: Cons)
with Cons obtain ss tt where "ta = ss @ tt ∧ s = trace_hide ss (ev ` A)
∧ t = trace_hide tt (ev ` A)" by blast
with True Cons show ?thesis by (rule_tac x="a#ss" in exI, rule_tac x=tt in exI, auto)
next
case False thus ?thesis
proof(cases s)
case Nil thus ?thesis using Cons by fastforce
next
case Cons2:(Cons aa tls)
with False have A:"a = aa ∧ tls @ t = trace_hide ta (ev ` A)" using Cons by auto
with Cons obtain ss tt where "ta = ss @ tt ∧ tls = trace_hide ss (ev ` A)
∧ t = trace_hide tt (ev ` A)" by blast
with Cons2 A False show ?thesis by (rule_tac x="a#ss" in exI, rule_tac x=tt in exI, auto)
qed
qed
qed
subsection‹The Hiding Operator Definition›
lift_definition Hiding :: "['α process ,'α set] => 'α process" (‹_ \ _› [57,56] 57) is
‹λP A. ({(s,X). ∃ t. s = trace_hide t (ev`A) ∧ (t,X ∪ (ev`A)) ∈ ℱ P} ∪
{(s,X). s ∈ div_hide P A}, div_hide P A)›
proof -
show "is_process ({(s,X). ∃ t. s = trace_hide t (ev`(A :: 'α set)) ∧ (t,X ∪ (ev`A)) ∈ ℱ P} ∪
{(s,X). s ∈ div_hide P A}, div_hide P A)" (is "is_process(?f, ?d)") for P A
proof (simp only: is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv,
intro conjI, goal_cases)
case 1 thus ?case
proof (auto, rule not_not[THEN iffD1], rule notI, simp, goal_cases)
case 1
from inf_hidden[of A "[]" P] obtain f where A:"isInfHiddenRun f P A ∧ [] ∈ range f"
using "1"(2) Nil_elem_T by auto
from A 1(1)[THEN spec, of "[]"] filter.simps(1) tickFree_Nil show ?case by auto
qed
next
case 2 thus ?case
using is_processT2 Hiding_fronttickFree front_tickFree_append Hiding_tickFree by blast+
next
case 3 thus ?case
proof(auto del:disjE, goal_cases)
case (1 s t ta) show ?case
proof(cases "tickFree s")
case True
from 1(2) obtain ss tt where A:"ta = ss@tt ∧ s = trace_hide ss (ev ` A) ∧ ss ∈ 𝒯 P"
using trace_hide_append[of s t A ta, OF 1(1)] by (metis F_T is_processT3_SR)
with True have B:"tickFree ss"
by (metis event.distinct(1) filter_set imageE member_filter tickFree_def)
show ?thesis
using 1(3) A B inf_hidden[of A ss P] by (metis append_Nil2 front_tickFree_Nil)
next
case False
with 1(1,2) obtain ss tt where A:"s = ss@[tick] ∧ ta = tt@[tick]"
by (metis append_Nil2 contra_subsetD filter_is_subset front_tickFree_mono
Hiding_fronttickFree is_processT nonTickFree_n_frontTickFree tickFree_def)
with 1(1,2) have "ss = trace_hide tt (ev ` A)"
by (metis (no_types, lifting) butlast_append butlast_snoc contra_subsetD
filter.simps(2) filter_append filter_is_subset front_tickFree_implies_tickFree
front_tickFree_single is_processT nonTickFree_n_frontTickFree non_tickFree_tick
self_append_conv2 tickFree_append tickFree_def)
with False 1(1,2) A show ?thesis
by (metis append_Nil2 front_tickFree_mono Hiding_fronttickFree is_processT)
qed
next
case (2 s t ta u) show ?case
proof(cases "length s ≤ length (trace_hide ta (ev ` A))")
case True
with append_eq_append_conv2[THEN iffD1, OF 2(3)]
obtain tt where "s@tt = trace_hide ta (ev ` A)" by auto
with 2(4) obtain ss ttt where A:"ta = ss@ttt ∧ s = trace_hide ss (ev ` A) ∧ ss ∈ 𝒯 P"
using trace_hide_append[of s tt A ta] by (metis D_T imageE is_processT3_ST)
with 2(2) have B:"tickFree ss" using tickFree_append by blast
show ?thesis
using 2(4,5) A B inf_hidden[of A ss P]
by (metis (no_types, lifting) append_Nil2 is_processT)
next
case False
with 2(3) obtain uu uuu where A:"s = trace_hide ta (ev ` A) @ uu ∧ u = uu @ uuu"
by (auto simp add: append_eq_append_conv2, metis le_length_mono le_list_def)
with 2(1,2,4) 2(5)[rule_format, of ta uu] show ?thesis
using front_tickFree_dw_closed by blast
qed
qed
next
case 4 thus ?case
by (auto, metis (mono_tags) Un_subset_iff is_processT4 sup.cobounded2 sup.coboundedI1)
next
case 5 thus ?case
proof(intro impI allI, auto, rule not_not[THEN iffD1], rule notI, simp, goal_cases)
case (1 X Y t)
from 1(3) 1(4)[THEN spec, of t, simplified] obtain c where A1:"c ∈ Y" and A2:"c ∉ (ev`A)"
and A3:"t@[c] ∈ 𝒯 P"
using is_processT5_S7'[of t "X ∪ (ev`A)" P Y] by (metis UnCI sup_commute sup_left_commute)
hence "trace_hide t (ev ` A) @ [c] = trace_hide (t@[c]) (ev ` A)" by simp
thus ?case using 1(1)[rule_format, OF A1] inf_hidden[of A "t@[c]", rotated, OF A3]
by (metis (no_types, lifting) append.right_neutral append_T_imp_tickFree
front_tickFree_Nil is_processT5_S7 not_Cons_self2 rangeE)
qed
next
case 6 thus ?case
proof (auto, goal_cases)
case (1 s X t)
hence "front_tickFree t" by (simp add:is_processT2)
with 1(1) obtain t' where A:"t = t'@[tick]"
by (metis filter_is_subset nonTickFree_n_frontTickFree non_tickFree_tick
subset_iff tickFree_append tickFree_def)
with 1(1,2) have B:"s = trace_hide t' (ev ` A)"
by (auto simp add:tickFree_def split:if_splits)
with A 1(1,2) is_processT6[of P, THEN spec, THEN spec, of t' "X ∪ ev ` A"]
is_processT4_empty[of t "ev ` A" P] show ?case
by (auto simp add: Un_Diff split:if_splits)
next
case (2 s X t u)
then obtain u' where A:"u = u'@[tick]"
by (metis filter_is_subset nonTickFree_n_frontTickFree non_tickFree_tick
subset_iff tickFree_append tickFree_def)
with 2(3) have B:"s = trace_hide t (ev ` A) @ u'"
by (auto simp add:tickFree_def split:if_splits)
with 2(1,2,5) 2(4)[THEN spec, THEN spec, of t u'] show ?case
using front_tickFree_dw_closed A by blast
next
case (3 s X u f x)
then obtain u' where A:"u = u'@[tick]"
by (metis filter_is_subset nonTickFree_n_frontTickFree non_tickFree_tick
subset_iff tickFree_append tickFree_def)
with 3(3) have B:"s = trace_hide (f x) (ev ` A) @ u'"
by (auto simp add:tickFree_def split:if_splits)
with 3(1,2,3,5,6,7) 3(4)[THEN spec, THEN spec, of "f x" u'] show ?case
using front_tickFree_dw_closed[of u' "[tick]"] by auto
qed
next
case 7 thus ?case using front_tickFree_append by (auto, blast +)
next
case 8 thus ?case by simp
next
case 9 thus ?case
proof (intro allI impI, simp, elim exE, goal_cases)
case (1 s t u)
then obtain u' where "u = u'@[tick]"
by (metis Hiding_tickFree nonTickFree_n_frontTickFree non_tickFree_tick tickFree_append)
with 1 show ?case
apply(rule_tac x=t in exI, rule_tac x=u' in exI)
using front_tickFree_dw_closed by auto
qed
qed
qed
subsection‹Projections›
lemma F_Hiding: ‹ℱ (P \ A) = {(s,X). ∃ t. s = trace_hide t (ev`A) ∧ (t,X ∪ (ev`A)) ∈ ℱ P} ∪
{(s,X). s ∈ div_hide P A}›
by (simp add: Failures.rep_eq Hiding.rep_eq FAILURES_def)
lemma D_Hiding: ‹𝒟 (P \ A) = div_hide P A›
by (simp add: Divergences.rep_eq Hiding.rep_eq DIVERGENCES_def)
lemma T_Hiding: ‹𝒯 (P \ A) = {s. ∃t. s = trace_hide t (ev`A) ∧ (t, ev`A) ∈ ℱ P} ∪ div_hide P A›
by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Hiding)
(metis is_processT4 sup_ge2, metis sup_bot_left)
subsection‹Continuity Rule›
lemma mono_Hiding[simp]: ‹(P::'a process) ⊑ Q ⟹ (P \ A) ⊑ (Q \ A)›
proof (auto simp only:le_approx_def D_Hiding Ra_def F_Hiding T_Hiding, goal_cases)
case (1 t u) thus ?case by blast
next
case (2 u f xa) thus ?case
apply(rule_tac x="f xa" in exI, rule_tac x=u in exI)
by (metis D_T Ra_def le_approx2T le_approx_def rangeI)
next
case (3 x t)
hence A:"front_tickFree t" by (meson is_processT2)
show ?case
proof(cases "tickFree t")
case True thus ?thesis
by (metis "3"(2) "3"(4) "3"(5) "3"(6) front_tickFree_charn mem_Collect_eq self_append_conv)
next
case False
with A obtain t' where "t = t'@[tick]" using nonTickFree_n_frontTickFree by blast
with 3 show ?thesis
by (metis (no_types, lifting) filter.simps(1) filter.simps(2) front_tickFree_mono
front_tickFree_Nil filter_append is_processT9 list.distinct(1) local.A mem_Collect_eq)
qed
next
case (4 x t) thus ?case using NF_ND by blast
next
case (5 x t u) thus ?case by blast
next
case (6 x u f xa) thus ?case by (metis D_T Ra_def le_approx2T le_approx_def rangeI)
next
case (7 x)
from 7(4) have A:"x ∈ min_elems (div_hide P A)" by simp
from elem_min_elems[OF 7(4), simplified] obtain t u
where B1:"x = trace_hide t (ev ` A) @ u" and B2:"tickFree t" and B3:"front_tickFree u" and
B4:"(t ∈ 𝒟 P ∨ (∃(f:: nat ⇒ 'a event list). strict_mono f ∧ (∀i. f i ∈ 𝒯 P) ∧
(∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)) ∧ t ∈ range f))" by blast
show ?case proof(cases "t ∈ 𝒟 P")
case True
then obtain t' t'' where C1:"t'@t''=t" and C2:"t' ∈ min_elems (𝒟 P)" by (metis min_elems_charn)
hence C3:"trace_hide t' (ev ` A) ∈ div_hide P A"
apply (simp, rule_tac x=t' in exI, rule_tac x="[]" in exI, simp)
using B2 elem_min_elems tickFree_append by blast
from C1 B1 have D1:"trace_hide t' (ev ` A) @ trace_hide t'' (ev ` A) = trace_hide t (ev ` A)"
by fastforce
from B1 C1 D1 min_elems_no[OF A C3] have E1:"x=trace_hide t' (ev ` A)"
by (metis (no_types, lifting) append.assoc le_list_def)
with B1 B2 B3 C1 D1 7(5)[simplified, rule_format, of "t'" "[]"]
have E2:"(∀(f:: nat ⇒ 'a event list). strict_mono f ⟶ (∃i. f i ∉ 𝒯 Q) ∨
(∃i. trace_hide (f i) (ev ` A) ≠ trace_hide (f 0) (ev ` A)) ∨ t' ∉ range f)"
apply simp
using front_tickFree_append Hiding_tickFree tickFree_append by blast
with E1 7(3) C2 inf_hidden[of A t' Q] show ?thesis
by (metis (no_types, lifting) contra_subsetD)
next
case False
from B1 B2 B3 B4 have C:"trace_hide t (ev ` A) ∈ div_hide P A"
by (simp, rule_tac x=t in exI, rule_tac x="[]" in exI, simp)
from B1 min_elems_no[OF A C] have E1:"x=trace_hide t (ev ` A)"
using le_list_def by auto
from B4 False 7(2)[rule_format, of t, OF False] have "t ∈ 𝒯 Q" using F_T T_F by blast
with E1 7(5)[simplified, rule_format, of t "[]", simplified, OF E1 B2] inf_hidden[of A t Q] show ?thesis
by metis
qed
qed
lemma cont_Hiding1 :‹chain Y ⟹ chain (λ i. (Y i \ A))›
by (simp add: po_class.chain_def)
lemma KoenigLemma:
assumes *:"infinite (Tr::'a list set)" and **:"∀i. finite{t. ∃t'∈Tr. t = take i t'}"
shows "∃(f::nat ⇒ 'a list). strict_mono f ∧ range f ⊆ {t. ∃t'∈Tr. t ≤ t'}"
proof -
define Tr' where "Tr' = {t. ∃t'∈Tr. t ≤ t'}"
have a:"infinite Tr'"
by (metis (mono_tags, lifting) * Tr'_def infinite_super mem_Collect_eq order_refl subsetI)
{ fix i
have "{t ∈ Tr'. length t = i} ⊆ {t. ∃t'∈Tr. t = take i t'}"
by (auto simp add:Tr'_def, metis append_eq_conv_conj le_list_def)
with ** have "finite({t∈Tr'. length t = i})" using infinite_super by blast
} note b=this
{ fix t
define E where "E = {e |e. t@[e]∈ Tr'}"
have aa:"finite E"
proof -
have "inj_on (λe. t @ [e]) E" by (simp add: inj_on_def)
with b[of "Suc (length t)"] inj_on_finite[of "λe. t@[e]" E "{t' ∈ Tr'. length t' = Suc (length t)}"]
show ?thesis by (simp add: E_def image_Collect_subsetI)
qed
hence bb:"finite {t@[e] |e. e∈E}" by simp
have "{t'∈Tr'. t < t'} = {t@[e] |e. e∈E} ∪ (⋃e∈E. {t'∈Tr'. t@[e] < t'})"
proof (auto simp add:Let_def E_def Tr'_def, goal_cases)
case (1 x xa)
then obtain u e where "x = t @ [e] @ u"
by (metis A append_Cons append_Nil append_Nil2 le_list_def list.exhaust)
with 1 1(4)[rule_format, of e] show ?case by (metis append_assoc le_list_def less_list_def)
next
case (2 x xa xb xc)
thus ?case by (meson less_self less_trans)
qed
with aa bb have "infinite {t'∈Tr'. t < t'} ⟹ ∃e. infinite {t'∈Tr'. t@[e] < t'}" by auto
} note c=this
define ff where d:"ff =rec_nat [] (λi t. (let e = SOME e. infinite {t'∈Tr'. t@[e] < t'} in t @ [e]))"
hence dd:"∀n. ff (Suc n) > ff n" by simp
hence e:"strict_mono ff" by (simp add: lift_Suc_mono_less strict_monoI)
{ fix n
have "ff n ∈ Tr' ∧ infinite {t' ∈ Tr'. ff n < t'}"
proof(induct n)
case 0
from a Tr'_def have "Tr' = {t' ∈ Tr'. [] < t'} ∪ {[]}" by (auto simp add: le_neq_trans)
with a have "infinite {t' ∈ Tr'. [] < t'}"
by (metis (no_types, lifting) finite.emptyI finite.insertI finite_UnI)
with d Tr'_def show ?case by auto
next
case (Suc n)
from d have "ff (Suc n) = (let e = SOME e. infinite {t'∈Tr'. ff n@[e] < t'} in ff n @ [e])" by simp
with c[rule_format, of "ff n"] obtain e where
a1:"ff (Suc n) = (ff n) @ [e] ∧ infinite {t' ∈ Tr'. ff n @ [e] < t'}"
by (metis (no_types, lifting) Suc.hyps someI_ex)
then obtain i where "i ∈ Tr' ∧ ff (Suc n) < i" using not_finite_existsD by auto
with Tr'_def have "ff (Suc n) ∈ Tr'" using dual_order.trans less_imp_le by fastforce
with a1 show ?case by simp
qed
} note g=this
hence h:"range ff ⊆ Tr'" by auto
show ?thesis using Tr'_def e h by blast
qed
lemma div_Hiding_lub :
‹finite (A::'a set) ⟹ chain Y ⟹ 𝒟 (⨆ i. (Y i \ A)) ⊆ 𝒟 ((⨆ i. Y i) \ A)›
proof (auto simp add:limproc_is_thelub cont_Hiding1 D_Hiding T_Hiding D_LUB T_LUB, goal_cases)
case (1 x)
{ fix xa t u f
assume a:"front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧
isInfHiddenRun f (Y xa) A ∧ (∀ i. f i ∉ 𝒟 (Y xa)) ∧ t ∈ range f"
hence "(∀i n. f i ∈ 𝒯 (Y n))" using 1(2) NT_ND chain_lemma le_approx2T by blast
with a have ?case by blast
} note aa=this
{ fix xa t u f j
assume a:"front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧
isInfHiddenRun f (Y xa) A ∧ (f j ∈ 𝒟 (Y xa)) ∧ t ∈ range f"
hence "∃t u. front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ 𝒟 (Y xa)"
apply(rule_tac x="f j" in exI, rule_tac x=u in exI)
using Hiding_tickFree[of "f j" A] Hiding_tickFree[of t A] by (metis imageE)
} note bb=this
have cc: "∀xa. ∃t u. front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ 𝒟(Y xa)
⟹ ?case" (is "∀xa. ∃t. ?S t xa ⟹ ?case")
proof -
assume dd:"∀xa. ∃t u. front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ 𝒟(Y xa)"
(is "∀xa. ∃t. ?S t xa")
define f where "f = (λn. SOME t. ?S t n)"
thus ?case
proof (cases "finite(range f)")
case True
obtain t where gg:"infinite (f -` {t})" using f_def True inf_img_fin_dom by blast
then obtain k where "f k = t" using finite_nat_set_iff_bounded_le by blast
then obtain u where uu:"front_tickFree u ∧ x = trace_hide t (ev ` A) @ u ∧ tickFree t"
using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"] by blast
{ fix m
from gg obtain n where gg:"n ≥ m ∧ n ∈ (f -` {t})"
by (meson finite_nat_set_iff_bounded_le nat_le_linear)
hence "t ∈ 𝒟 (Y n)" using f_def dd[rule_format, of n] some_eq_ex[of "λt. ?S t n"] by auto
with gg 1(2) have "t ∈ 𝒟 (Y m)" by (meson contra_subsetD le_approx_def po_class.chain_mono)
}
with gg uu show ?thesis by blast
next
case False
{ fix t
assume "t ∈ range f"
then obtain k where "f k = t" using finite_nat_set_iff_bounded_le by blast
then obtain u where uu:"front_tickFree u ∧ x = trace_hide t (ev ` A) @ u ∧ tickFree t"
using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"] by blast
hence "set t ⊆ set x ∪ (ev ` A)" by auto
} note ee=this
{ fix i
have "finite {(take i t)|t. t ∈ range f}"
proof(induct i, simp)
case (Suc i)
have ff:"{take (Suc i) t|t. t ∈ range f} ⊆ {(take i t)|t. t ∈ range f} ∪
(⋃e∈(set x ∪ (ev ` A)). {(take i t)@[e]|t. t ∈ range f})" (is "?AA ⊆ ?BB")
proof
fix t
assume "t ∈ ?AA"
then obtain t' where hh:"t' ∈ range f ∧ t = take (Suc i) t'"
using finite_nat_set_iff_bounded_le by blast
with ee[of t'] show "t ∈ ?BB"
proof(cases "length t' > i")
case True
hence ii:"take (Suc i) t' = take i t' @ [t'!i]" by (simp add: take_Suc_conv_app_nth)
with ee[of t'] have "t'!i ∈ set x ∪ (ev ` A)"
by (meson True contra_subsetD hh nth_mem)
with ii hh show ?thesis by blast
next
case False
hence "take (Suc i) t' = take i t'" by fastforce
with hh show ?thesis by auto
qed
qed
{ fix e
have "{x @ [e] |x. ∃t. x = take i t ∧ t ∈ range f} = {take i t' @ [e] |t'. t' ∈ range f}"
by auto
hence "finite({(take i t') @ [e] |t'. t'∈range f})"
using finite_image_set[of _ "λt. t@[e]", OF Suc] by auto
} note gg=this
have "finite(set x ∪ (ev ` A))" using 1(1) by simp
with ff gg Suc show ?case by (metis (no_types, lifting) finite_UN finite_Un finite_subset)
qed
} note ff=this
hence "∀i. {take i t |t. t ∈ range f} = {t. ∃t'. t = take i (f t')}" by auto
with KoenigLemma[of "range f", OF False] ff
obtain f' where gg:"strict_mono (f':: nat ⇒ 'a event list) ∧
range f' ⊆ {t. ∃t'∈range f. t ≤ t'}" by auto
{ fix n
define M where "M = {m. f' n ≤ f m }"
assume "finite M"
hence l1:"finite {length (f m)|m. m ∈ M}" by simp
obtain lm where l2:"lm = Max {length (f m)|m. m ∈ M}" by blast
{ fix k
have "length (f' k) ≥ k"
by(induct k, simp, metis (full_types) gg lessI less_length_mono linorder_not_le
not_less_eq_eq order_trans strict_mono_def)
}
with gg obtain m where r1:"length (f' m) > lm" by (meson lessI less_le_trans)
from gg obtain r where r2:"f' (max m n) ≤ f r" by blast
with gg have r3: "r ∈ M"
by (metis (no_types, lifting) M_def max.bounded_iff mem_Collect_eq order_refl
order_trans strict_mono_less_eq)
with l1 l2 have f1:"length (f r) ≤ lm" using Max_ge by blast
from r1 r2 have f2:"length (f r) > lm"
by (meson dual_order.strict_trans1 gg le_length_mono max.bounded_iff order_refl
strict_mono_less_eq)
from f1 f2 have False by simp
} note ii=this
{ fix i n
from ii obtain m where jj:"m ≥ n ∧ f m ≥ f' i"
by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear)
have kk: "(f m) ∈ 𝒟 (Y m)" using f_def dd[rule_format, of m] some_eq_ex[of "λt. ?S t m"] by auto
with jj gg have "(f' i) ∈ 𝒯 (Y m)" by (meson D_T is_processT3_ST_pref)
with jj 1(2) have "(f' i) ∈ 𝒯 (Y n)" using D_T le_approx2T po_class.chain_mono by blast
} note jj=this
from gg have kk:"mono (λn. trace_hide (f' n) (ev ` A))"
unfolding strict_mono_def mono_def
by (metis (no_types, lifting) filter_append gg le_list_def mono_def strict_mono_mono)
{ fix n
from gg obtain k r where "f k = f' n @ r" by (metis ii le_list_def not_finite_existsD)
hence "trace_hide (f' n) (ev ` A) ≤ x"
using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"] le_list_def by auto blast
} note ll=this
{ assume llll:"∀m. ∃n. trace_hide (f' n) (ev ` A) > trace_hide (f' m) (ev ` A)"
hence lll:"∀m. ∃n. length (trace_hide (f' n) (ev ` A)) > length (trace_hide (f' m) (ev ` A))"
using less_length_mono by blast
define ff where lll':"ff = rec_nat (length (trace_hide (f' 0) (ev ` A)))
(λi t. (let n = SOME n. (length (trace_hide (f' n) (ev ` A))) > t
in length (trace_hide (f' n) (ev ` A))))"
{ fix n
from lll' lll[rule_format, of n] have "ff (Suc n) > ff n"
apply simp apply (cases n)
apply (metis (no_types, lifting) old.nat.simps(6) someI_ex)
by (metis (no_types, lifting) llll less_length_mono old.nat.simps(7) someI_ex)
} note lll''=this
with lll'' have "strict_mono ff" by (simp add: lll'' lift_Suc_mono_less strict_monoI)
hence lll''':"infinite(range ff)" using finite_imageD strict_mono_imp_inj_on by auto
from lll lll' have "range ff ⊆ range (λn. length (trace_hide (f' n) (ev ` A)))"
by (auto, metis (mono_tags, lifting) old.nat.exhaust old.nat.simps(6) old.nat.simps(7) range_eqI)
with lll''' have "infinite (range (λn. length (trace_hide (f' n) (ev ` A))))"
using finite_subset by auto
hence "∃m. length (trace_hide (f' m) (ev ` A)) > length x"
using finite_nat_set_iff_bounded_le by (metis (no_types, lifting) not_less rangeE)
with ll have False using le_length_mono not_less by blast
}
then obtain m where mm:"∀n. trace_hide (f' n) (ev ` A) ≤ trace_hide (f' m) (ev ` A)"
by (metis (mono_tags, lifting) A kk le_cases mono_def)
with gg obtain k where nn:"f k ≥ f' m" by blast
then obtain u where oo:"front_tickFree u ∧ x = trace_hide (f' m) (ev ` A) @ u ∧ tickFree (f' m)"
using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"]
by (auto, metis (no_types, lifting) contra_subsetD filter_is_subset front_tickFree_append
front_tickFree_mono le_list_def ll tickFree_Nil tickFree_append
tickFree_def tickFree_implies_front_tickFree)
show ?thesis
apply(rule_tac x="f' m" in exI, rule_tac x=u in exI)
apply(simp add:oo, rule disjI2, rule_tac x="λn. f' (n + m)" in exI)
using gg jj kk mm apply (auto simp add: strict_mono_def dual_order.antisym mono_def)
by (metis plus_nat.add_0 rangeI)
qed
qed
show ?case
proof (cases "∃ xa t u f. front_tickFree u ∧ tickFree t ∧ (∀ i. f i ∉ 𝒟 (Y xa)) ∧ t ∈ range f ∧
x = trace_hide t (ev ` A) @ u ∧ isInfHiddenRun f (Y xa) A")
case True
then show ?thesis using aa by blast
next
case False
have dd:"∀xa. ∃t u. front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧
(t ∈ 𝒟 (Y xa) ∨ (∃f. isInfHiddenRun f (Y xa) A ∧ (∃i. f i ∈ 𝒟 (Y xa)) ∧ t ∈ range f))"
(is "∀xa. ?dd xa")
proof (rule_tac allI)
fix xa
from 1(3) obtain t u where
"front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧
(t ∈ 𝒟 (Y xa) ∨ (∃f. isInfHiddenRun f (Y xa) A ∧ t ∈ range f))"
by blast
thus "?dd xa"
apply(rule_tac x=t in exI, rule_tac x=u in exI, intro conjI, simp_all, elim conjE disjE, simp_all)
using 1(1) False NT_ND chain_lemma le_approx2T by blast
qed
hence ee:"∀xa. ∃t u. front_tickFree u ∧ tickFree t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ 𝒟(Y xa)"
using bb by blast
with cc show ?thesis by simp
qed
qed
lemma cont_Hiding2 : ‹finite A ⟹ chain Y ⟹ ((⨆ i. Y i) \ A) = (⨆ i. (Y i \ A))›
proof(auto simp add:limproc_is_thelub cont_Hiding1 Process_eq_spec
D_Hiding Ra_def F_Hiding T_Hiding F_LUB D_LUB T_LUB, goal_cases)
case (1 b x t u) thus ?case by blast
next
case (2 b x u f xa) thus ?case by blast
next
case (3 s X)
hence ‹s ∉ 𝒟 ((⨆ i. Y i) \ A)›
by (simp add:limproc_is_thelub cont_Hiding1 F_LUB D_LUB T_LUB D_Hiding)
with 3(1,2) obtain n where a: ‹s ∉ 𝒟 (Y n \ A)›
by (metis (no_types, lifting) D_LUB_2 div_Hiding_lub subsetCE limproc_is_thelub cont_Hiding1)
with 3(3) obtain t where b:"s = trace_hide t (ev ` A) ∧ (t, X ∪ ev ` A) ∈ ℱ (Y n)"
unfolding D_Hiding by blast
hence c:"front_tickFree t" using is_processT2 by blast
have d:"t ∉ 𝒟(Y n)"
proof(cases "tickFree t")
case True
with a b show ?thesis using front_tickFree_Nil
by (simp add: D_Hiding)
next
case False
with c obtain t' where "t = t'@[tick]" using nonTickFree_n_frontTickFree by blast
with a b show ?thesis
apply(simp add: D_Hiding, erule_tac x=t' in allE, erule_tac x="[tick]" in allE, simp)
by (metis event.distinct(1) filter.simps(1) front_tickFree_implies_tickFree imageE is_processT)
qed
with b show ?case using 3(2) NF_ND chain_lemma proc_ord2a by blast
next
case (4 xa t u) thus ?case by blast
next
case (5 xa u f xb) thus ?case by blast
next
case (6 s)
hence ‹s ∈ 𝒟 (⨆ i. (Y i \ A))›
by (simp add:limproc_is_thelub cont_Hiding1 6(1) D_Hiding D_LUB)
with div_Hiding_lub[OF 6(1,2)] have ‹s ∈ 𝒟 ((⨆i. Y i) \ A)› by blast
thus ?case by (simp add:limproc_is_thelub 6(2) D_Hiding D_LUB T_LUB)
qed
lemma cont_Hiding_base[simp] : ‹finite A ⟹ cont (λx. x \ A)›
by (simp add: cont_def cont_Hiding1 cont_Hiding2 cpo_lubI)
lemma Hiding_cont[simp]: ‹finite A ⟹ cont f ⟹ cont (λx. f x \ A)›
by (rule_tac f=f in cont_compose, simp_all)
end