Theory Hiding
chapter‹The Hiding Operator›
theory Hiding
imports Process
begin
section‹Preliminaries : primitives and lemmas›
abbreviation ‹trace_hide t A ≡ filter (λx. x ∉ A) t›
lemma Hiding_tickFree : ‹tF (trace_hide s (ev ` A)) ⟷ tF s›
by (auto simp add: tickFree_def)
lemma Hiding_front_tickFree : ‹ftF s ⟹ ftF (trace_hide s (ev ` A))›
apply (induct s; simp add: image_iff front_tickFree_Cons_iff)
by (metis (no_types, lifting) filter.simps(1) front_tickFree_charn)
lemma trace_hide_union: ‹trace_hide t (A ∪ B) = trace_hide (trace_hide t A) B› by simp
lemma trace_hide_ev_union [simp] :
‹trace_hide t (ev ` (A ∪ B)) = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
apply (fold trace_hide_union)
apply (rule arg_cong[where f = ‹λS. trace_hide t S›])
by blast
abbreviation isInfHiddenRun :: ‹[nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set] ⇒ bool›
where ‹isInfHiddenRun f P A ≡ strict_mono f ∧ (∀i. f i ∈ 𝒯 P) ∧
(∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (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)›
proof (intro iffI conjI; elim conjE, assumption?)
assume * : ‹strict_mono f› ‹∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)›
show ‹∀i. ∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A›
proof (rule allI)
fix i
from "*"(1) obtain t where ‹f i = f 0 @ t›
by (meson prefixE less_eq_nat.simps(1) strict_mono_less_eq)
with "*"(2)[THEN spec, of i] have ‹set t ⊆ ev ` A›
by simp (metis empty_filter_conv subset_code(1))
with ‹f i = f 0 @ t› show ‹∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A› by blast
qed
next
assume * : ‹∀i. ∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A›
show ‹∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)›
proof (rule allI)
fix i
from "*"[rule_format, of i] show ‹trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)›
by (elim exE, simp) (meson filter_False in_mono)
qed
qed
abbreviation div_hide :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ 'a set ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list set›
where ‹div_hide P A ≡ {s. ∃t u. ftF u ∧ tF t ∧
s = trace_hide t (ev ` A) @ u ∧
(t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f))}›
lemma inf_hidden:
‹∃f. isInfHiddenRun f P A ∧ s ∈ range f›
if ‹∀t. trace_hide t (ev ` A) = trace_hide s (ev ` A) ⟶ (t, ev ` A) ∉ ℱ P› and ‹s ∈ 𝒯 P›
proof (rule exI)
define f where ‹f ≡ rec_nat s (λi t. let e = SOME e. e ∈ ev ` A ∧ t @ [e] ∈ 𝒯 P in t @ [e])›
have ‹strict_mono f› by (simp add: f_def strict_mono_def lift_Suc_mono_less_iff)
moreover have ‹s ∈ range f› unfolding f_def by (metis (no_types, lifting) nat.rec(1) range_eqI)
moreover have ‹f i ∈ 𝒯 P ∧ trace_hide (f i) (ev ` A) = trace_hide s (ev ` A)› for i
proof (induct i)
show ‹f 0 ∈ 𝒯 P ∧ trace_hide (f 0) (ev ` A) = trace_hide s (ev ` A)›
by (simp add: f_def that(2))
next
fix i
assume hyp : ‹f i ∈ 𝒯 P ∧ trace_hide (f i) (ev ` A) = trace_hide s (ev ` A)›
from is_processT5_S7[OF hyp[THEN conjunct1] that(1)[rule_format, OF hyp[THEN conjunct2]]]
obtain e where $ : ‹e ∈ ev ` A› ‹f i @ [e] ∈ 𝒯 P› by blast
have ‹f (Suc i) = (let e = SOME e. e ∈ ev ` A ∧ f i @ [e] ∈ 𝒯 P in f i @ [e])›
by (simp add: f_def)
thus ‹f (Suc i) ∈ 𝒯 P ∧ trace_hide (f (Suc i)) (ev ` A) = trace_hide s (ev ` A)›
by (simp add: hyp[THEN conjunct2]) (metis (no_types, lifting) "$" someI_ex)
qed
ultimately show ‹isInfHiddenRun f P A ∧ s ∈ range f› by simp
qed
lemma trace_hide_append :
‹s @ t = trace_hide u (ev ` A) ⟹
∃s' t'. u = s' @ t' ∧ s = trace_hide s' (ev ` A) ∧ t = trace_hide t' (ev ` A)›
proof (induct u arbitrary: s t)
case Nil
thus ?case by simp
next
case (Cons e u)
show ?case
proof (cases ‹e ∈ ev ` A›)
assume ‹e ∈ ev ` A›
with Cons.prems have ‹s @ t = trace_hide u (ev ` A)› by simp
with Cons.hyps obtain s' t' where
‹u = s' @ t'› ‹s = trace_hide s' (ev ` A)› ‹t = trace_hide t' (ev ` A)› by blast
hence ‹e # u = (e # s') @ t' ∧ s = trace_hide (e # s') (ev ` A) ∧ t = trace_hide t' (ev ` A)›
by (simp add: ‹e ∈ ev ` A›)
thus ?case by blast
next
assume ‹e ∉ ev ` A›
with Cons.prems consider ‹s = []› ‹t ≠ []› ‹hd t = e› ‹[] @ tl t = trace_hide u (ev ` A)›
| ‹s ≠ []› ‹hd s = e› ‹tl s @ t = trace_hide u (ev ` A)› by (cases s) simp_all
thus ?case
proof cases
show ‹⟦s = []; t ≠ []; hd t = e; [] @ tl t = trace_hide u (ev ` A)⟧ ⟹ ?case›
by (drule Cons.hyps) (metis Cons.prems append_Nil filter.simps(1))
next
show ‹⟦s ≠ []; hd s = e; tl s @ t = trace_hide u (ev ` A)⟧ ⟹ ?case›
by (drule Cons.hyps) (metis Cons.prems Cons_eq_appendI append_same_eq filter_append)
qed
qed
qed
section‹The Hiding Operator Definition›
lift_definition Hiding :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k ,'a set] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (infixl ‹\› 69)
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 ‹?thesis P A› (is ‹is_process(?f, div_hide P A)›) for P and A
proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI allI impI)
from inf_hidden[of A ‹[]› P] show ‹([], {}) ∈ ?f›
by simp (metis filter.simps(1) tickFree_Nil)
next
show ‹(s, X) ∈ ?f ⟹ ftF s› for s X
by simp (metis F_imp_front_tickFree Hiding_front_tickFree Hiding_tickFree
front_tickFree_append_iff tickFree_imp_front_tickFree)
next
show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
proof (induct t rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc e t)
from snoc.prems consider u where ‹s @ t @ [e] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ ℱ P›
| u v where ‹ftF v› ‹tF u› ‹s @ t @ [e] = trace_hide u (ev ` A) @ v›
‹u ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ u ∈ range f)›
by simp blast
thus ?case
proof cases
fix u assume ‹s @ t @ [e] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ ℱ P›
from this(1) obtain u' u'' where ‹u = u' @ u''› ‹s @ t = trace_hide u' (ev ` A)›
by (metis append_assoc trace_hide_append)
have ‹(s @ t, {}) ∈ ?f›
proof (cases ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›)
show ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ ℱ P ⟹
(s @ t, {}) ∈ ?f›
by (simp add: ‹s @ t = trace_hide u' (ev ` A)›) metis
next
assume * : ‹∄t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›
from this[simplified, THEN inf_hidden] obtain f where ‹isInfHiddenRun f P A ∧ u' ∈ range f›
using T_F_spec ‹(u, ev ` A) ∈ ℱ P› ‹u = u' @ u''› is_processT3 is_processT4_empty by blast
hence ‹s @ t ∈ div_hide P A›
by (simp add: ‹s @ t = trace_hide u' (ev ` A)›)
(metis F_imp_front_tickFree ‹(u, ev ` A) ∈ ℱ P› "*" ‹u = u' @ u''›
append.right_neutral front_tickFree_Nil front_tickFree_append_iff)
thus ‹(s @ t, {}) ∈ ?f› by simp
qed
from snoc.hyps[OF this] show ‹(s, {}) ∈ ?f› by blast
next
fix u v assume * : ‹ftF v› ‹tF u› ‹s @ t @ [e] = trace_hide u (ev ` A) @ v›
‹u ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ u ∈ range f)›
show ?case
proof (cases v rule: rev_cases)
assume ‹v = []›
with "*"(3) obtain u' u'' where ‹u = u' @ u''› ‹s @ t = trace_hide u' (ev ` A)›
by simp (metis append_assoc trace_hide_append)
from "*"(4) D_T have ‹u ∈ 𝒯 P› by blast
have ‹(s @ t, {}) ∈ ?f›
proof (cases ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›)
show ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ ℱ P ⟹
(s @ t, {}) ∈ ?f›
by (simp add: ‹s @ t = trace_hide u' (ev ` A)›) metis
next
assume * : ‹∄t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›
from this[simplified, THEN inf_hidden] obtain f where ‹isInfHiddenRun f P A ∧ u' ∈ range f›
by (metis T_F_spec ‹u = u' @ u''› ‹u ∈ 𝒯 P› is_processT3)
hence ‹s @ t ∈ div_hide P A›
by (simp add: ‹s @ t = trace_hide u' (ev ` A)›)
(metis (no_types, lifting) "*" append_Nil2 append_T_imp_tickFree
front_tickFree_Nil is_processT5_S7 list.distinct(1) rangeE)
thus ‹(s @ t, {}) ∈ ?f› by simp
qed
from snoc.hyps[OF this] show ‹(s, {}) ∈ ?f› by blast
next
fix v' e'
assume ‹v = v' @ [e']›
with "*" front_tickFree_dw_closed have ‹s @ t ∈ div_hide P A› by auto
hence ‹(s @ t, {}) ∈ ?f› by simp
from snoc.hyps[OF this] show ‹(s, {}) ∈ ?f› by blast
qed
qed
qed
next
show $ : ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
by simp (metis is_processT4 subset_iff_psubset_eq sup.mono)
next
fix s X Y assume * : ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)›
from "*"[THEN conjunct1] consider ‹s ∈ div_hide P A›
| u where ‹s = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` A) ∈ ℱ P› by simp blast
thus ‹(s, X ∪ Y) ∈ ?f›
proof cases
show ‹s ∈ div_hide P A ⟹ (s, X ∪ Y) ∈ ?f› by simp
next
fix u assume ‹s = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` A) ∈ ℱ P›
show ‹(s, X ∪ Y) ∈ ?f›
proof (cases ‹s ∈ div_hide P A›)
show ‹s ∈ div_hide P A ⟹ (s, X ∪ Y) ∈ ?f› by simp
next
assume ‹s ∉ div_hide P A›
have ‹(u, X ∪ Y ∪ ev ` A) ∈ ℱ P›
proof (rule ccontr)
assume ‹(u, X ∪ Y ∪ ev ` A) ∉ ℱ P›
hence ‹(u, X ∪ ev ` A ∪ Y) ∉ ℱ P› by (metis sup.assoc sup_commute)
from is_processT5_S7'[OF ‹(u, X ∪ ev ` A) ∈ ℱ P› this] obtain c
where ‹c ∈ Y› ‹c ∉ X› ‹c ∉ ev ` A› ‹u @ [c] ∈ 𝒯 P› by blast
show False
proof (cases ‹∃t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›)
show ‹∃t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ ℱ P ⟹ False›
using "*" ‹c ∈ Y› ‹c ∉ ev ` A› ‹s = trace_hide u (ev ` A)› by force
next
assume ‹∄t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›
hence ‹∀t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A)
⟶ (t, ev ` A) ∉ ℱ P› by simp
from inf_hidden[OF this ‹u @ [c] ∈ 𝒯 P›] have ‹s @ [c] ∈ div_hide P A›
by (smt (verit, ccfv_threshold) Prefix_Order.strict_prefix_simps(1)
Prefix_Order.strict_prefix_simps(2)
‹∄t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ ℱ P›
‹s = trace_hide u (ev ` A)› ‹s ∉ div_hide P A› ‹u @ [c] ∈ 𝒯 P› append_Nil2
append_T_imp_tickFree filter.simps(1) filter.simps(2) filter_append
front_tickFree_Nil is_processT5_S7 mem_Collect_eq)
thus False using "*" ‹c ∈ Y› by blast
qed
qed
thus ‹(s, X ∪ Y) ∈ ?f› by (auto simp add: ‹s = trace_hide u (ev ` A)›)
qed
qed
next
{ fix s r assume ‹s @ [✓(r)] ∈ div_hide P A›
then obtain t u where * : ‹ftF u› ‹tF t›
‹s @ [✓(r)] = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f)› by blast
from "*"(2, 3) have ‹u ≠ []›
by (cases u; cases t rule: rev_cases; simp split: if_split_asm)
(metis Hiding_tickFree non_tickFree_tick tickFree_append_iff)
with "*"(2, 3) have ‹s = trace_hide t (ev ` A) @ butlast u›
by (cases u rule: rev_cases; simp)
moreover from "*"(1)front_tickFree_iff_tickFree_butlast tickFree_imp_front_tickFree
have ‹ftF (butlast u)› by blast
ultimately show ‹s ∈ div_hide P A› using "*"(2, 4) by auto
} note local_is_processT9 = this
fix s r X assume ‹(s @ [✓(r)], {}) ∈ ?f›
then consider ‹s @ [✓(r)] ∈ div_hide P A›
| u where ‹s @ [✓(r)] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ ℱ P› by simp blast
thus ‹(s, X - {tick r}) ∈ ?f›
proof cases
assume ‹s @ [✓(r)] ∈ div_hide P A›
with local_is_processT9 have ‹s ∈ div_hide P A› by blast
thus ‹(s, X - {tick r}) ∈ ?f› by simp
next
fix u assume ‹s @ [✓(r)] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ ℱ P›
from this(1) obtain u' where ‹u = u' @ [✓(r)]› ‹s = trace_hide u' (ev ` A)›
by (cases u rule: rev_cases; simp split: if_split_asm)
(metis F_imp_front_tickFree Hiding_tickFree ‹(u, ev ` A) ∈ ℱ P› tickFree_append_iff
front_tickFree_iff_tickFree_butlast non_tickFree_tick snoc_eq_iff_butlast)
have ‹X - {✓(r)} ∪ ev ` A = X ∪ ev ` A - {✓(r)}› by auto
with is_processT6_TR[OF ‹(u, ev ` A) ∈ ℱ P›[THEN F_T, unfolded ‹u = u' @ [✓(r)]›]]
have ‹(u', X - {✓(r)} ∪ ev ` A) ∈ ℱ P› by presburger
thus ‹(s, X - {tick r}) ∈ ?f› by (auto simp add: ‹s = trace_hide u' (ev ` A)›)
qed
next
fix s t :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› assume * : ‹s ∈ div_hide P A ∧ tF s ∧ ftF t›
from "*"[THEN conjunct1] obtain u v
where ** : ‹ftF v› ‹tF u› ‹s = trace_hide u (ev ` A) @ v›
‹u ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ u ∈ range f)› by blast
from "**"(3) have ‹s @ t = trace_hide u (ev ` A) @ v @ t› by simp
moreover from "*" "**"(3) front_tickFree_append have ‹ftF (v @ t)› by auto
ultimately show ‹s @ t ∈ div_hide P A› using "**"(2) "**"(4) by blast
next
show ‹s ∈ div_hide P A ⟹ (s, X) ∈ ?f› for s X by simp
qed
qed
section‹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) = {trace_hide t (ev ` A) |t. (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)
lemma Hiding_empty: ‹P \ {} = P›
by (auto simp add: Process_eq_spec D_Hiding F_Hiding strict_mono_eq
intro: is_processT7 is_processT8)
(metis append.right_neutral front_tickFree_append_iff
list.distinct(1) nonTickFree_n_frontTickFree process_charn)
lemma mem_D_imp_mem_D_Hiding: ‹trace_hide t (ev ` A) ∈ 𝒟 (P \ A)› if ‹t ∈ 𝒟 P›
proof (cases ‹tF t›)
assume ‹tF t›
with ‹t ∈ 𝒟 P› show ‹trace_hide t (ev ` A) ∈ 𝒟 (P \ A)›
by (simp add: D_Hiding) (use front_tickFree_Nil in blast)
next
assume ‹¬ tF t›
with ‹t ∈ 𝒟 P› obtain t' r where ‹t = t' @ [✓(r)]› ‹tF t'› ‹t' ∈ 𝒟 P›
by (metis D_imp_front_tickFree butlast_snoc is_processT9
front_tickFree_iff_tickFree_butlast nonTickFree_n_frontTickFree)
thus ‹trace_hide t (ev ` A) ∈ 𝒟 (P \ A)›
by (simp add: D_Hiding) (use front_tickFree_single in blast)
qed
lemma mem_T_imp_mem_T_Hiding: ‹trace_hide t (ev ` A) ∈ 𝒯 (P \ A)› if ‹t ∈ 𝒯 P›
proof (cases ‹∃t'. trace_hide t (ev ` A) = trace_hide t' (ev ` A) ∧ (t', ev ` A) ∈ ℱ P›)
show ‹∃t'. trace_hide t (ev ` A) = trace_hide t' (ev ` A) ∧ (t', ev ` A) ∈ ℱ P
⟹ trace_hide t (ev ` A) ∈ 𝒯 (P \ A)› by (simp add: T_Hiding)
next
assume ‹∄t'. trace_hide t (ev ` A) = trace_hide t' (ev ` A) ∧ (t', ev ` A) ∈ ℱ P›
with inf_hidden[of A, OF _ ‹t ∈ 𝒯 P›] obtain f
where ‹isInfHiddenRun f P A› ‹t ∈ range f› ‹tF t›
by (metis T_nonTickFree_imp_decomp ‹t ∈ 𝒯 P› tick_T_F)
thus ‹trace_hide t (ev ` A) ∈ 𝒯 (P \ A)›
by (simp add: T_Hiding) (use front_tickFree_Nil in blast)
qed
section‹Continuity Rule›
lemma mono_Hiding : ‹(P \ A) ⊑ (Q \ A)› if ‹(P::('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊑ Q›
proof (unfold le_approx_def, intro conjI allI impI subsetI)
from le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›]
show ‹s ∈ 𝒟 (Q \ A) ⟹ s ∈ 𝒟 (P \ A)› for s
by (simp add: D_Hiding) blast
next
{ fix s t X
assume assms : ‹s ∉ 𝒟 (P \ A)› ‹s = trace_hide t (ev ` A)›
have ‹t ∉ 𝒟 P›
proof (cases ‹ftF t›)
from D_imp_front_tickFree show ‹¬ ftF t ⟹ t ∉ 𝒟 P› by blast
next
assume ‹ftF t›
show ‹t ∉ 𝒟 P›
proof (cases ‹tF t›)
from ‹s ∉ 𝒟 (P \ A)› show ‹tF t ⟹ t ∉ 𝒟 P›
by (simp add: assms(2) D_Hiding)
next
assume ‹¬ tF t›
then obtain t' r where ‹t = t' @ [tick r]›
by (meson ‹ftF t› nonTickFree_n_frontTickFree process_charn)
with ‹s ∉ 𝒟 (P \ A)› show ‹t ∉ 𝒟 P›
by (simp add: assms(2) D_Hiding image_iff)
(metis front_tickFree_append_iff list.distinct(1) process_charn)
qed
qed
} note * = this
fix s
assume ‹s ∉ 𝒟 (P \ A)›
show ‹ℛ⇩a (P \ A) s = ℛ⇩a (Q \ A) s›
proof (intro subset_antisym subsetI)
fix X
assume ‹X ∈ ℛ⇩a (P \ A) s›
with le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›] ‹s ∉ 𝒟 (P \ A)›
obtain t where $ : ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ ℱ P›
by (simp add: Refusals_after_def F_Hiding D_Hiding) blast
from "*"[OF ‹s ∉ 𝒟 (P \ A)› ‹s = trace_hide t (ev ` A)›] have ‹t ∉ 𝒟 P› .
from le_approx2[OF ‹P ⊑ Q› this] "$"
show ‹X ∈ ℛ⇩a (Q \ A) s› by (simp add: Refusals_after_def F_Hiding) blast
next
fix X
assume ‹X ∈ ℛ⇩a (Q \ A) s›
with le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›] ‹s ∉ 𝒟 (P \ A)›
obtain t where $ : ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ ℱ Q›
by (simp add: Refusals_after_def F_Hiding D_Hiding) blast
from "*"[OF ‹s ∉ 𝒟 (P \ A)› ‹s = trace_hide t (ev ` A)›] have ‹t ∉ 𝒟 P› .
from le_approx2[OF ‹P ⊑ Q› this] "$"
show ‹X ∈ ℛ⇩a (P \ A) s› by (simp add: Refusals_after_def F_Hiding) blast
qed
next
fix s
assume ‹s ∈ min_elems (𝒟 (P \ A))›
{ fix t
assume assms : ‹t ∈ 𝒟 P› ‹s = trace_hide t (ev ` A)› ‹tF t›
from assms(1) obtain t' t'' where ‹t = t' @ t''› and ‹t' ∈ min_elems (𝒟 P)›
by (meson min_elems_charn)
with assms(3) elem_min_elems tickFree_append_iff
have ‹trace_hide t' (ev ` A) ∈ 𝒟 (P \ A)›
by (simp add: D_Hiding) (use front_tickFree_Nil in blast)
from filter_append[of ‹(λx. x ∉ ev ` A)› t' t'', folded ‹t = t' @ t''›]
have ‹trace_hide t (ev ` A) = trace_hide t' (ev ` A) @ trace_hide t'' (ev ` A)› .
hence ‹s = trace_hide t' (ev ` A)›
by (metis (no_types, lifting) assms(2) ‹s ∈ min_elems (𝒟 (P \ A))›
min_elems_no ‹trace_hide t' (ev ` A) ∈ 𝒟 (P \ A)› less_eq_list_def prefix_def)
have ‹s ∈ 𝒯 (Q \ A)›
proof (cases ‹∀v. trace_hide v (ev ` A) = trace_hide t' (ev ` A) ⟶ (v, ev ` A) ∉ ℱ Q›)
assume ‹∀v. trace_hide v (ev ` A) = trace_hide t' (ev ` A) ⟶ (v, ev ` A) ∉ ℱ Q›
from inf_hidden[OF this] have ‹∃f. isInfHiddenRun f Q A ∧ t' ∈ range f›
by (meson ‹t' ∈ min_elems (𝒟 P)› in_mono le_approx_def that)
thus ‹s ∈ 𝒯 (Q \ A)›
by (simp add: T_Hiding)
(use assms(3) ‹s = trace_hide t' (ev ` A)› ‹t = t' @ t''›
front_tickFree_Nil tickFree_append_iff in blast)
next
show ‹¬ (∀v. trace_hide v (ev ` A) = trace_hide t' (ev ` A)
⟶ (v, ev ` A) ∉ ℱ Q) ⟹ s ∈ 𝒯 (Q \ A)›
by (simp add: T_Hiding) (metis ‹s = trace_hide t' (ev ` A)›)
qed
} note $ = this
from elem_min_elems[OF ‹s ∈ min_elems (𝒟 (P \ A))›] have ‹s ∈ 𝒟 (P \ A)› .
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f)›
by (simp add: D_Hiding) blast
have ‹u = []›
proof (rule ccontr)
assume ‹u ≠ []›
have ‹ftF (butlast u)› ‹butlast s = trace_hide t (ev ` A) @ butlast u›
by (use "*"(1) front_tickFree_iff_tickFree_butlast tickFree_imp_front_tickFree in blast)
(simp add: "*"(3) ‹u ≠ []› butlast_append)
with "*"(2, 4) have ‹butlast s ∈ 𝒟 (P \ A)› by (simp add: D_Hiding) blast
from min_elems_no[OF ‹s ∈ min_elems (𝒟 (P \ A))› this] "*"(3) ‹u ≠ []›
show False by (metis Nil_is_append_conv append_butlast_last_id less_self nless_le)
qed
from "*"(4) show ‹s ∈ 𝒯 (Q \ A)›
proof (elim disjE exE)
show ‹t ∈ 𝒟 P ⟹ s ∈ 𝒯 (Q \ A)› using "$" "*"(2, 3) ‹u = []› by blast
next
fix f
assume assm : ‹isInfHiddenRun f P A ∧ t ∈ range f›
show ‹s ∈ 𝒯 (Q \ A)›
proof (cases ‹∀i. f i ∈ 𝒯 Q›)
from "*"(1, 2, 3) assm show ‹∀i. f i ∈ 𝒯 Q ⟹ s ∈ 𝒯 (Q \ A)›
by (simp add: T_Hiding) blast
next
assume ‹¬ (∀i. f i ∈ 𝒯 Q)›
then obtain i where ‹f i ∉ 𝒯 Q› by blast
with assm le_approx2T ‹P ⊑ Q› have ‹f i ∈ 𝒟 P› by blast
moreover have ‹s = trace_hide (f i) (ev ` A)›
by (metis "*"(3) ‹u = []› append.right_neutral assm rangeE)
moreover have ‹tF (f i)›
by (metis "*"(2) "*"(3) Hiding_tickFree ‹u = []› append.right_neutral calculation(2))
ultimately show ‹s ∈ 𝒯 (Q \ A)› using "$" by blast
qed
qed
qed
lemma chain_Hiding : ‹chain Y ⟹ chain (λ i. Y i \ A)›
by (simp add: chain_def mono_Hiding)
lemma KoenigLemma:
‹∃(f::nat ⇒ 'a list). strict_mono f ∧ range f ⊆ {t. ∃t'∈Tr. t ≤ t'}›
if * : ‹infinite (Tr::'a list set)› and ** : ‹∀i. finite{t. ∃t'∈Tr. t = take i t'}›
proof -
define Tr' where ‹Tr' = {t. ∃t'∈Tr. t ≤ t'}›
have a : ‹infinite Tr'› by (rule infinite_super[OF _ "*"]) (unfold Tr'_def, blast)
have b : ‹finite {t ∈ Tr'. length t = i}› for i
by (rule finite_subset[OF _ "**"[THEN spec, of i]])
(unfold Tr'_def, simp add: subset_iff, metis prefixE append_eq_conv_conj)
have c : ‹∃e. infinite {t' ∈ Tr'. t @ [e] < t'}› if ‹infinite {t' ∈ Tr'. t < t'}› for t
proof (rule ccontr)
assume ‹∄e. infinite {t' ∈ Tr'. t @ [e] < t'}›
define E where ‹E ≡ {e |e. t @ [e] ∈ Tr'}›
have ‹finite E›
by (rule inj_on_finite[OF _ _ b[of ‹Suc (length t)›], of ‹λe. t @ [e]›])
(simp_all add: inj_on_def E_def image_Collect_subsetI)
hence ‹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'})›
by (auto simp add: E_def Tr'_def less_list_def less_eq_list_def prefix_def)+
(metis append_Cons append_self_conv2 neq_Nil_conv self_append_conv)
with ‹∄e. infinite {t' ∈ Tr'. t @ [e] < t'}› ‹infinite {t' ∈ Tr'. t < t'}› ‹finite E›
show False by auto
qed
define f where ‹f ≡ rec_nat [] (λi t. let e = SOME e. infinite {t' ∈ Tr'. t @ [e] < t'} in t @ [e])›
hence ‹strict_mono f› by (simp add: lift_Suc_mono_less strict_monoI)
moreover have ‹f n ∈ Tr' ∧ infinite {t' ∈ Tr'. f n < t'}› for n
proof (induct n)
show ‹f 0 ∈ Tr' ∧ infinite {t' ∈ Tr'. f 0 < t'}›
proof (rule conjI)
show ‹f 0 ∈ Tr'› by (simp add: f_def Tr'_def "*" not_finite_existsD)
next
show ‹infinite {t' ∈ Tr'. f 0 < t'}›
by (rule infinite_super[of ‹Tr' - {f 0}›])
(simp add: a Tr'_def f_def subset_iff less_list_def, simp add: a)
qed
next
fix n assume hyp : ‹f n ∈ Tr' ∧ infinite {t' ∈ Tr'. f n < t'}›
have ‹f (Suc n) = (let e = SOME e. infinite {t' ∈ Tr'. f n @ [e] < t'} in f n @ [e])›
by (simp add: f_def)
with c[of ‹f n›] obtain e
where $ : ‹f (Suc n) = f n @ [e] ∧ infinite {t' ∈ Tr'. f n @ [e] < t'}›
by (metis (no_types, lifting) hyp someI_ex)
then obtain i where ‹i ∈ Tr' ∧ f (Suc n) < i› using not_finite_existsD by auto
with dual_order.trans order_less_imp_le have ‹f (Suc n) ∈ Tr'›
unfolding Tr'_def by fastforce
thus ‹f (Suc n) ∈ Tr' ∧ infinite {t' ∈ Tr'. f (Suc n) < t'}› by (simp add: "$")
qed
ultimately show ‹∃(f::nat ⇒ 'a list). strict_mono f ∧ range f ⊆ Tr'› by blast
qed
lemma div_Hiding_lub :
‹finite (A::'a set) ⟹ chain Y ⟹ 𝒟 (⨆ i. (Y i \ A)) ⊆ 𝒟 ((⨆ i. Y i) \ A)›
for Y :: ‹nat ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (auto simp add:limproc_is_thelub chain_Hiding D_Hiding T_Hiding D_LUB T_LUB, goal_cases)
case (1 x)
{ fix xa t u f
assume a:"ftF u ∧ tF 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) D_T chain_lemma le_approx2T by blast
with a have ?case by blast
} note aa=this
{ fix xa t u f j
assume a:"ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧
isInfHiddenRun f (Y xa) A ∧ (f j ∈ 𝒟 (Y xa)) ∧ t ∈ range f"
hence "∃t u. ftF u ∧ tF 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)
by (metis Hiding_tickFree rangeE)
} note bb=this
have cc: "∀xa. ∃t u. ftF u ∧ tF 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. ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ 𝒟(Y xa)"
(is "∀xa. ∃t. ?S t xa")
define f :: ‹nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list› 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:"ftF u ∧ x = trace_hide t (ev ` A) @ u ∧ tF 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:"ftF u ∧ x = trace_hide t (ev ` A) @ u ∧ tF 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, 'r) event⇩p⇩t⇩i⇩c⇩k 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_TR)
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 less_eq_list_def prefix_def mono_def strict_mono_mono)
{ fix n
from gg obtain k r where "f k = f' n @ r"
by (metis (lifting) ii less_eq_list_def prefix_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"]
by (metis (no_types, lifting) prefixI prefix_prefix filter_append)
} 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 (no_types, lifting) dual_order.eq_iff le_same_imp_eq_or_less ll order.strict_implies_order)
with gg obtain k where nn:"f k ≥ f' m" by blast
then obtain u where oo:"ftF u ∧ x = trace_hide (f' m) (ev ` A) @ u ∧ tF (f' m)"
using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"]
apply (auto simp add: prefix_def tickFree_def disjoint_iff)
by (smt (z3) Prefix_Order.prefixE append.assoc disjoint_iff filter_append filter_is_subset front_tickFree_append subset_iff tickFree_append_iff tickFree_def)
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. ftF u ∧ tF 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. ftF u ∧ tF 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
"ftF u ∧ tF 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 D_T chain_lemma le_approx2T by blast
qed
hence ee:"∀xa. ∃t u. ftF u ∧ tF 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_Hiding_prem : ‹(⨆ i. Y i) \ A = (⨆ i. (Y i \ A))› if ‹finite A› ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
show ‹s ∈ 𝒟 ((⨆ i. Y i) \ A) ⟹ s ∈ 𝒟 (⨆ i. (Y i \ A))› for s
by (simp add: limproc_is_thelub chain_Hiding ‹chain Y› D_Hiding D_LUB T_LUB) blast
next
show ‹s ∈ 𝒟 (⨆ i. (Y i \ A)) ⟹ s ∈ 𝒟 ((⨆ i. Y i) \ A)› for s
using div_Hiding_lub[OF ‹finite A› ‹chain Y›] by auto
next
show ‹(s, X) ∈ ℱ ((⨆ i. Y i) \ A) ⟹ (s, X) ∈ ℱ (⨆ i. (Y i \ A))› for s X
by (simp add: limproc_is_thelub chain_Hiding ‹chain Y› F_Hiding F_LUB D_LUB T_LUB) blast
next
assume same_div : ‹𝒟 ((⨆ i. Y i) \ A) = 𝒟 (⨆ i. (Y i \ A))›
fix s X assume ‹(s, X) ∈ ℱ (⨆ i. (Y i \ A))›
show ‹(s, X) ∈ ℱ ((⨆ i. Y i) \ A)›
proof (cases ‹s ∈ 𝒟 (⨆ i. (Y i \ A))›)
show ‹s ∈ 𝒟 (⨆i. Y i \ A) ⟹ (s, X) ∈ ℱ ((⨆i. Y i) \ A)›
by (simp add: is_processT8 same_div)
next
assume ‹s ∉ 𝒟 (⨆i. Y i \ A)›
then obtain j where ‹s ∉ 𝒟 (Y j \ A)›
by (auto simp add: limproc_is_thelub chain_Hiding ‹chain Y› D_LUB)
moreover from ‹(s, X) ∈ ℱ (⨆ i. (Y i \ A))› have ‹(s, X) ∈ ℱ (Y j \ A)›
by (simp add: limproc_is_thelub chain_Hiding ‹chain Y› F_LUB)
ultimately show ‹(s, X) ∈ ℱ ((⨆i. Y i) \ A)›
by (fact le_approx2[OF mono_Hiding[OF is_ub_thelub[OF ‹chain Y›]], THEN iffD2])
qed
qed
lemma Hiding_cont[simp]: ‹cont (λa. f a \ A)› if ‹finite A› and ‹cont f›
proof (rule cont_compose[where f = f])
show ‹cont (λa. a \ A)›
proof (rule contI2)
show ‹monofun (λa. a \ A)› by (simp add: mono_Hiding monofunI)
next
show ‹chain Y ⟹ (⨆i. Y i) \ A ⊑ (⨆i. Y i \ A)›
for Y :: ‹nat ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
by (simp add: Cont_Hiding_prem[OF ‹finite A›])
qed
next
from ‹cont f› show ‹cont f› .
qed
lemma length_strict_mono: ‹strict_mono f ⟹ i + length (f 0) ≤ length (f i)›
for f :: ‹nat ⇒ 'a list›
by (induct i)
(simp_all add: Suc_le_eq less_length_mono order_le_less_trans strict_mono_Suc_iff)
lemma mono_trace_hide: ‹a ≤ b ⟹ trace_hide a (ev ` A) ≤ trace_hide b (ev ` A)›
by (metis prefixE prefixI filter_append)
lemma mono_constant:
assumes "mono (f::nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list)" and "∀i. f i ≤ a"
shows "∃i. ∀j≥i. f j = f i"
proof -
from assms(2) have "∀i. length (f i) ≤ length a"
by (simp add: le_length_mono)
hence aa:"finite {length (f i)|i. True}"
using finite_nat_set_iff_bounded_le by auto
define lm where l2:"lm = Max {length (f i)|i. True}"
with aa obtain im where "length (f im) = lm" using Max_in by fastforce
with l2 assms(1) show ?thesis
apply (intro exI[of _ im], intro impI allI)
by (metis (mono_tags, lifting) Max_ge aa antisym le_length_mono le_neq_trans less_length_mono
mem_Collect_eq mono_def order_less_irrefl)
qed
text ‹We can actually optimize the divergences of the \<^const>‹Hiding› operator.›
lemma mono_take : ‹s ≤ t ⟹ take n s ≤ take n t›
unfolding less_eq_list_def prefix_def by auto
lemma shift_isInfHiddenRun : ‹∃f. isInfHiddenRun f P A ∧ t = f 0›
if ‹isInfHiddenRun f P A ∧ t ∈ range f›
proof -
from that obtain i where ‹t = f i› by blast
hence ‹t = f (i + 0)› by simp
moreover have ‹isInfHiddenRun (λj. f (i + j)) P A›
by (metis add_Suc_right strict_mono_Suc_iff that)
ultimately show ‹∃f. isInfHiddenRun f P A ∧ t = f 0› by blast
qed
lemma uniformize_length_isInfHiddenRun :
assumes * : ‹isInfHiddenRun f P A› ‹t = f 0›
defines ‹g ≡ λi. take (i + length t) (f i)›
shows ‹isInfHiddenRun g P A ∧ (∀i. length (g i) = i + length t) ∧ t = g 0›
proof (intro conjI allI)
show ‹strict_mono g›
proof (unfold strict_mono_Suc_iff, rule allI)
fix i
from "*"(1) have ‹strict_mono f› by blast
from length_strict_mono[of f ‹Suc i›, OF ‹strict_mono f›]
have $ : ‹take (i + length (f 0)) (f (Suc i)) < take ((Suc i) + length (f 0)) (f (Suc i))›
by (simp add: take_Suc_conv_app_nth)
from ‹strict_mono f›[THEN strict_monoD, of i ‹Suc i›, simplified]
obtain u where ‹f (Suc i) = f i @ u› by (meson strict_prefixE')
with length_strict_mono[of f i, OF ‹strict_mono f›]
have ‹take (i + length (f 0)) (f i) = take (i + length (f 0)) (f (Suc i))› by simp
with "$" "*"(2) show ‹g i < g (Suc i)› unfolding g_def by presburger
qed
next
show ‹g i ∈ 𝒯 P› for i unfolding g_def
by (metis "*"(1) prefixI append_take_drop_id is_processT3_TR)
next
show ‹trace_hide (g i) (ev ` A) = trace_hide (g 0) (ev ` A)› for i
proof (rule order_antisym)
have ‹f 0 ≤ f i› by (simp add: "*"(1) strict_mono_less_eq)
hence ‹f 0 ≤ take (i + length t) (f i)›
by (metis "*"(2) prefixE prefixI le_add2 take_all_iff take_append)
from mono_trace_hide[OF this]
show ‹trace_hide (g i) (ev ` A) ≤ trace_hide (g 0) (ev ` A)›
unfolding g_def
by (metis "*" prefixI append_take_drop_id filter_append le_add2 take_all_iff)
next
have $ : ‹take (i + length (f 0)) (f i) ≤ f i› by (metis prefixI append_take_drop_id)
have ‹take (length t) (f 0) ≤ take (i + length t) (f 0)›
‹take (i + length t) (f 0) ≤ take (i + length t) (f i)›
by (simp add: "*"(2))
(meson "*"(1) le_add2 le_add_same_cancel2 mono_take strict_mono_less_eq)
from order_trans[OF this] have ‹g 0 ≤ g i› unfolding g_def by simp
thus ‹trace_hide (g 0) (ev ` A) ≤ trace_hide (g i) (ev ` A)› by (fact mono_trace_hide)
qed
next
show ‹length (g i) = i + length t› for i by (simp add: "*" g_def length_strict_mono)
next
show ‹t = g 0› by (simp add: "*"(2) g_def)
qed
abbreviation isInfHiddenRun_optimized ::
‹[nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set, ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k] ⇒ bool›
where ‹isInfHiddenRun_optimized f P A t ≡
strict_mono f ∧ (∀i. f i ∈ 𝒯 P) ∧ (∀i. f i ∉ 𝒟 P) ∧
(∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)) ∧
(∀i. length (f i) = i + length t) ∧ t = f 0›
abbreviation div_hide_optimized :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ 'a set ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list set›
where ‹div_hide_optimized P A ≡
{s. ∃t u. ftF u ∧ tF t ∧
s = trace_hide t (ev ` A) @ u ∧
(t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun_optimized f P A t))}›
lemma D_Hiding_optimized : ‹𝒟 (P \ A) = div_hide_optimized P A›
proof (unfold D_Hiding, intro subset_antisym subsetI)
show ‹s ∈ div_hide_optimized P A ⟹ s ∈ div_hide P A› for s by blast
next
fix s assume ‹s ∈ div_hide P A›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f)› by blast
from "*"(4) show ‹s ∈ div_hide_optimized P A›
proof (elim disjE exE)
from "*"(1, 2, 3) show ‹t ∈ 𝒟 P ⟹ s ∈ div_hide_optimized P A› by blast
next
fix f assume ‹isInfHiddenRun f P A ∧ t ∈ range f›
with shift_isInfHiddenRun obtain f where ** : ‹isInfHiddenRun f P A ∧ t = f 0› by blast
show ‹s ∈ div_hide_optimized P A›
proof (cases ‹∃i. f i ∈ 𝒟 P›)
assume ‹∃i. f i ∈ 𝒟 P›
then obtain i where ‹f i ∈ 𝒟 P› ..
have ‹trace_hide t (ev ` A) = trace_hide (f i) (ev ` A)› by (metis "**")
moreover from calculation have ‹tF (f i)› by (metis "*"(2) Hiding_tickFree)
ultimately show ‹s ∈ div_hide_optimized P A›
using "*"(1, 3) ‹f i ∈ 𝒟 P› by blast
next
assume ‹∄i. f i ∈ 𝒟 P›
from "**" uniformize_length_isInfHiddenRun[of f P A t]
have ‹isInfHiddenRun (λi. take (i + length t) (f i)) P A ∧
(∀i. length (take (i + length t) (f i)) = i + length t) ∧
t = take (0 + length t) (f 0)› by blast
moreover from ‹∄i. f i ∈ 𝒟 P› have ‹∀i. take (i + length t) (f i) ∉ 𝒟 P›
by (metis "**" append_Nil2 append_take_drop_id
front_tickFree_nonempty_append_imp is_processT2_TR is_processT7)
ultimately show ‹s ∈ div_hide_optimized P A› using "*"(1, 2, 3) by blast
qed
qed
qed
lemma T_Hiding_optimized :
‹𝒯 (P \ A) = {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ ℱ P} ∪ div_hide_optimized P A›
by (unfold T_Hiding, fold D_Hiding, unfold D_Hiding_optimized) (fact refl)
text ‹
Actually, \<^term>‹f i› can be rewritten as \<^term>‹t @ map x [0..<i]›
where \<^term>‹x› is the sequence such that \<^term>‹f (Suc i) = f i @ [x i]›.›
definition seqRun :: ‹[('a, 'r) trace⇩p⇩t⇩i⇩c⇩k, nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k] ⇒ nat ⇒ ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
where ‹seqRun t x i ≡ t @ map x [0..<i]›
lemma seqRun_is_rec_nat : ‹seqRun t x = rec_nat t (λi t. t @ [x i])›
proof (rule ext)
show ‹seqRun t x i = rec_nat t (λi t. t @ [x i]) i› for i
by (induct i) (simp_all add: seqRun_def)
qed
lemma seqRun_0 [simp] : ‹seqRun t x 0 = t›
and seqRun_Suc [simp] : ‹seqRun t x (Suc i) = seqRun t x i @ [x i]›
and seqRun_Nil [simp] : ‹seqRun [] x i = map x [0..<i]›
and seqRun_Cons [simp] : ‹seqRun (a # t) x i = a # seqRun t x i›
by (simp_all add: seqRun_def)
lemma strict_mono_seqRun [simp] : ‹strict_mono (seqRun t x)›
by (simp add: strict_mono_Suc_iff)
lemma length_seqRun [simp] : ‹length (seqRun t x i) = i + length t›
by (simp add: seqRun_def)
lemma t_le_seqRun [simp] : ‹t ≤ seqRun t x i› by (simp add: seqRun_def)
lemma take_t_le_seqRun [simp] : ‹take i t ≤ seqRun t x j›
by (induct t, simp_all add: seqRun_def less_eq_list_def prefix_def)
(metis append.assoc append_Cons append_take_drop_id)
lemma nth_seqRun :
‹j < i + length t ⟹
seqRun t x i ! j = (if j < length t then t ! j else x (j - length t))›
by (simp add: seqRun_def nth_append)
lemma take_seqRun [simp] :
‹take j (seqRun t x i) = (if j ≤ length t then take j t else seqRun t x (min i (j - length t)))›
by (simp add: seqRun_def min_def take_map)
lemma seqRun_eq_iff [simp] : ‹seqRun t x i = seqRun t x j ⟷ i = j›
by (metis add_right_cancel length_seqRun)
lemma seqRun_le_iff [simp] : ‹seqRun t x i ≤ seqRun t x j ⟷ i ≤ j›
by (simp add: strict_mono_less_eq)
lemma seqRun_less_iff [simp] : ‹seqRun t x i < seqRun t x j ⟷ i < j›
by (simp add: strict_mono_less)
lemma trace_hide_is_Nil_iff : ‹trace_hide s A = [] ⟷ set s ⊆ A›
by (simp add: filter_empty_conv subset_code(1))
lemma trace_hide_seqRun_eq_iff :
‹trace_hide (seqRun t x i) A = trace_hide t A ⟷ (∀j<i. x j ∈ A)›
by (simp add: seqRun_def trace_hide_is_Nil_iff subset_iff image_iff)
(use atLeastLessThan_iff in blast)
abbreviation isInfHidden_seqRun ::
‹[nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set, ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k] ⇒ bool›
where ‹isInfHidden_seqRun x P A t ≡ ∀i. seqRun t x i ∈ 𝒯 P ∧ x i ∈ ev ` A›
abbreviation isInfHidden_seqRun_strong ::
‹[nat ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set, ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k] ⇒ bool›
where ‹isInfHidden_seqRun_strong x P A t ≡
∀i. seqRun t x i ∈ 𝒯 P ∧ seqRun t x i ∉ 𝒟 P ∧ x i ∈ ev ` A›
abbreviation div_hide_seqRun :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ 'a set ⇒ ('a, 'r) event⇩p⇩t⇩i⇩c⇩k list set›
where ‹div_hide_seqRun P A ≡
{s. ∃t u. ftF u ∧ tF t ∧ s = trace_hide t (ev ` A) @ u ∧
(t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t))}›
lemma D_Hiding_seqRun : ‹𝒟 (P \ A) = div_hide_seqRun P A›
proof (intro subset_antisym subsetI)
fix s assume ‹s ∈ 𝒟 (P \ A)›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun_optimized f P A t)›
unfolding D_Hiding_optimized by blast
show ‹s ∈ div_hide_seqRun P A›
proof (clarify, intro exI conjI)
show ‹ftF u› ‹tF t›
‹s = trace_hide t (ev ` A) @ u› by (fact "*"(1, 2, 3))+
next
from "*"(4) show ‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t)›
proof (elim disjE exE)
show ‹t ∈ 𝒟 P ⟹ t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t)› ..
next
fix f assume $ : ‹isInfHiddenRun_optimized f P A t›
define x where ‹x i ≡ f (Suc i) ! (i + length t)› for i
have $$ : ‹seqRun t x i = f i› for i
proof (induct i)
show ‹seqRun t x 0 = f 0› by (simp add: "$")
next
fix i assume ‹seqRun t x i = f i›
from "$" have ‹length (f (Suc i)) = Suc i + length t›
‹length (f i) = i + length t› ‹f i ≤ f (Suc i)›
by (blast, blast, simp add: strict_mono_less_eq)
then obtain y where ‹f (Suc i) = f i @ [y]›
by (simp add: less_eq_list_def prefix_def)
(metis append_eq_append_conv length_Suc_conv_rev)
with ‹length (f i) = i + length t› have ‹f (Suc i) = f i @ [x i]›
unfolding x_def by (metis nth_append_length)
thus ‹seqRun t x (Suc i) = f (Suc i)› by (simp add: ‹seqRun t x i = f i›)
qed
have ‹isInfHidden_seqRun x P A t›
proof (intro allI conjI)
from "$" "$$" show ‹seqRun t x i ∈ 𝒯 P› for i by presburger+
next
from trace_hide_seqRun_eq_iff[of ‹ev ` A› t x, unfolded "$$"] "$"
show ‹x i ∈ ev ` A› for i by blast
qed
thus ‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t)› by blast
qed
qed
next
fix s assume ‹s ∈ div_hide_seqRun P A›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t)› by blast
show ‹s ∈ 𝒟 (P \ A)›
proof (unfold D_Hiding_optimized)
from "*"(4) show ‹s ∈ div_hide_optimized P A›
proof (elim disjE exE)
from "*"(1, 2, 3) show ‹t ∈ 𝒟 P ⟹ s ∈ div_hide_optimized P A› by blast
next
fix x assume $ : ‹isInfHidden_seqRun x P A t›
show ‹s ∈ div_hide_optimized P A›
proof (cases ‹∃i. seqRun t x i ∈ 𝒟 P›)
assume ‹∃i. seqRun t x i ∈ 𝒟 P›
then obtain i where ‹seqRun t x i ∈ 𝒟 P› ..
show ‹s ∈ div_hide_optimized P A›
proof (clarify, intro exI conjI)
show ‹ftF u› by (fact "*"(1))
next
show ‹tF (seqRun t x i)›
by (metis "$" append_T_imp_tickFree length_Cons n_not_Suc_n seqRun_Suc)
next
show ‹s = trace_hide (seqRun t x i) (ev ` A) @ u›
by (metis "$" "*"(3) trace_hide_seqRun_eq_iff)
next
from ‹seqRun t x i ∈ 𝒟 P›
show ‹seqRun t x i ∈ 𝒟 P ∨ (∃f. isInfHiddenRun_optimized f P A (seqRun t x i))› ..
qed
next
assume ‹∄i. seqRun t x i ∈ 𝒟 P›
hence ‹isInfHiddenRun_optimized (seqRun t x) P A t›
by (simp add: trace_hide_seqRun_eq_iff "$")
with "*"(1, 2, 3) show ‹s ∈ div_hide_optimized P A› by blast
qed
qed
qed
qed
lemma T_Hiding_seqRun :
‹𝒯 (P \ A) = {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ ℱ P} ∪ div_hide_seqRun P A›
by (unfold T_Hiding, fold D_Hiding_seqRun D_Hiding) (fact refl)
lemma F_Hiding_seqRun :
‹ℱ (P \ A) =
{(s, X). ∃t. s = trace_hide t (ev ` A) ∧ (t, X ∪ ev ` A) ∈ ℱ P} ∪
{(s, X). s ∈ div_hide_seqRun P A}›
by (unfold F_Hiding, fold D_Hiding_seqRun D_Hiding) (fact refl)
lemma D_Hiding_seqRunI :
‹⟦ftF u; tF t; s = trace_hide t (ev ` A) @ u;
t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t)⟧ ⟹ s ∈ 𝒟 (P \ A)›
unfolding D_Hiding_seqRun by blast
lemma D_Hiding_seqRunE :
assumes ‹s ∈ 𝒟 (P \ A)›
obtains t u where ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun_strong x P A t)›
proof -
from ‹s ∈ 𝒟 (P \ A)› obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun x P A t)› unfolding D_Hiding_seqRun by blast
from "*"(4) show thesis
proof (elim disjE exE)
from "*"(1, 2, 3) that show ‹t ∈ 𝒟 P ⟹ thesis› by blast
next
fix x assume $ : ‹isInfHidden_seqRun x P A t›
show thesis
proof (cases ‹∃i. seqRun t x i ∈ 𝒟 P›)
assume ‹∃i. seqRun t x i ∈ 𝒟 P›
then obtain i where ‹seqRun t x i ∈ 𝒟 P› ..
show thesis
proof (rule that)
show ‹ftF u› by (fact "*"(1))
next
show ‹tF (seqRun t x i)›
by (metis "$" append_T_imp_tickFree neq_Nil_conv seqRun_Suc)
next
show ‹s = trace_hide (seqRun t x i) (ev ` A) @ u›
by (simp add: "*"(3)) (metis "$" trace_hide_seqRun_eq_iff)
next
from ‹seqRun t x i ∈ 𝒟 P›
show ‹seqRun t x i ∈ 𝒟 P ∨
(∃y. isInfHidden_seqRun_strong y P A (seqRun t x i))› ..
qed
next
from "*"(1, 2, 3) "$" that show ‹∄i. seqRun t x i ∈ 𝒟 P ⟹ thesis› by blast
qed
qed
qed
lemma T_Hiding_seqRunE :
assumes ‹s ∈ 𝒯 (P \ A)›
obtains t where ‹s = trace_hide t (ev ` A)› ‹(t, ev ` A) ∈ ℱ P›
| t u where ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun_strong x P A t)›
proof (cases ‹s ∈ 𝒟 (P \ A)›)
assume ‹s ∉ 𝒟 (P \ A)›
with ‹s ∈ 𝒯 (P \ A)› have ‹s ∈ {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ ℱ P}›
unfolding D_Hiding T_Hiding by blast
with that(1) show thesis by blast
qed (elim D_Hiding_seqRunE, presburger)
lemma butlast_seqRun : ‹butlast (seqRun t x i) = (case i of 0 ⇒ butlast t
| Suc j ⇒ seqRun t x j)›
by (cases i) simp_all
lemma isInfHidden_seqRun_imp_tickFree : ‹isInfHidden_seqRun x P A t ⟹ tF t›
by (metis append_T_imp_tickFree not_Cons_self2 seqRun_0 seqRun_Suc)
lemma tickFree_seqRun_iff : ‹tF (seqRun t x i) ⟷ tF t ∧ (∀j<i. is_ev (x j))›
by (induct i; simp) (metis less_Suc_eq)
lemma front_tickFree_seqRun_iff :
‹ftF (seqRun t x i) ⟷ (case i of 0 ⇒ ftF t | Suc j ⇒ tF t ∧ (∀k<j. is_ev (x k)))›
by (cases i) (simp_all add: front_tickFree_iff_tickFree_butlast tickFree_seqRun_iff)
lemmas Hiding_seqRun_projs = F_Hiding_seqRun D_Hiding_seqRun T_Hiding_seqRun
end