Theory Mndetprefix
theory Mndetprefix
imports Process Stop Mprefix Ndet
begin
section‹Multiple non deterministic operator›
lift_definition Mndetprefix :: "['α set, 'α ⇒ 'α process] ⇒ 'α process"
is "λA P. if A = {} then Rep_process STOP
else (⋃ x∈A. ℱ(x → P x), ⋃ x∈A. 𝒟(x → P x))"
apply auto
using Rep_process apply blast
unfolding is_process_def FAILURES_def DIVERGENCES_def
apply auto
using is_processT1 apply auto[1]
using is_processT2 apply blast
using is_processT3_SR apply blast
using is_processT4 apply blast
using is_processT5_S1 apply blast
using is_processT6 apply blast
using is_processT7 apply blast
using NF_ND apply auto[1]
using is_processT9 by blast
syntax
"_Mndetprefix" :: "pttrn ⇒ 'a set ⇒ 'a process ⇒ 'a process"
(‹(3⊓_∈_ → / _)› [0, 0, 70] 70)
syntax_consts
"_Mndetprefix" ⇌ Mndetprefix
translations
"⊓x∈A→ P" ⇌ "CONST Mndetprefix A (λx. P)"
lemma mt_Mndetprefix[simp] : "Mndetprefix {} P = STOP"
by (simp add: Mndetprefix_def Rep_process_inverse)
lemma rep_abs_Mndetprefix: "A ≠ {} ⟹
(Rep_process (Abs_process(⋃x∈A. ℱ(x → P x),⋃x∈A. 𝒟 (x → P x)))) =
(⋃x∈A. ℱ(x → P x), ⋃x∈A. 𝒟 (x → P x))"
by (metis (mono_tags, lifting) Abs_process_inverse Mndetprefix.rep_eq Rep_process)
lemma F_Mndetprefix:
"ℱ (Mndetprefix A P) = (if A = {} then {(s, X). s = []} else ⋃ x∈A. ℱ (x → P x))"
by (simp add: Failures.rep_eq FAILURES_def STOP.rep_eq Mndetprefix.rep_eq)
lemma D_Mndetprefix : "𝒟 (Mndetprefix A P) = (if A = {} then {} else ⋃ x∈A. 𝒟 (x → P x))"
by (simp add: Divergences.rep_eq DIVERGENCES_def STOP.rep_eq Mndetprefix.rep_eq)
lemma T_Mndetprefix: "𝒯 (Mndetprefix A P) = (if A = {} then {[]} else ⋃ x∈A. 𝒯 (x → P x))"
by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Mndetprefix)
text‹ Thus we know now, that Mndetprefix yields processes. Direct consequences are the following
distributivities: ›
lemma Mndetprefix_unit : "(⊓ x ∈ {a} → P x) = (a → P a)"
by(auto simp : Process.Process_eq_spec F_Mndetprefix D_Mndetprefix)
lemma Mndetprefix_Un_distrib : "A ≠{} ⟹ B ≠{} ⟹ (⊓ x ∈ A∪B → P x) = ((⊓ x ∈ A → P x) ⊓ (⊓ x ∈ B → P x))"
by(auto simp : Process.Process_eq_spec F_Ndet D_Ndet F_Mndetprefix D_Mndetprefix)
text‹ The two lemmas @{thm Mndetprefix_unit} and @{thm Mndetprefix_Un_distrib} together give us that @{const Mndetprefix}
can be represented by a fold in the finite case. ›
lemma Mndetprefix_distrib_unit : "A-{a} ≠ {} ⟹ (⊓ x ∈ insert a A → P x) = ((a → P a) ⊓ (⊓ x ∈ A-{a} → P x))"
by (metis Un_Diff_cancel insert_is_Un insert_not_empty Mndetprefix_Un_distrib Mndetprefix_unit)
subsection‹Finite case Continuity›
text‹ This also implies that Mndetprefix is continuous for the
finite @{term A} and an arbitrary body @{term f}: ›
lemma Mndetprefix_cont_finite[simp]:
assumes "finite A"
and "⋀x. cont (f x)"
shows "cont (λy. ⊓ z ∈ A → f z y)"
proof(rule Finite_Set.finite_induct[OF `finite A`])
show "cont (λy. ⊓z∈{} → f z y)" by auto
next
fix A fix a
assume "cont (λy. ⊓z∈A → f z y)" and "a ∉ A"
show "cont (λy. ⊓z∈insert a A → f z y)"
proof(cases "A={}")
case True
then show ?thesis by(simp add: Mndetprefix_unit True `⋀x. cont (f x)`)
next
case False
have * : "A-{a} ≠ {}" by (simp add: False ‹a ∉ A›)
have ** : "A-{a} = A" by (simp add: ‹a ∉ A›)
show ?thesis
apply(simp only: Mndetprefix_distrib_unit[OF *], simp only: **)
by (simp add: ‹cont (λy. ⊓z∈A → f z y)› assms(2))
qed
qed
subsection‹General case Continuity›
lemma mono_Mndetprefix[simp] : "monofun (Mndetprefix (A::'a set))"
proof(cases "A={}")
case True
then show ?thesis by(auto simp: monofun_def)
next
case False
then show ?thesis apply(simp add: monofun_def, intro allI impI)
unfolding le_approx_def
proof(simp add:T_Mndetprefix F_Mndetprefix D_Mndetprefix, intro conjI)
fix x::"'a ⇒ 'a process" and y::"'a ⇒ 'a process"
assume "A ≠ {}" and "x ⊑ y"
show "(⋃x∈A. 𝒟 (x→ y x)) ⊆ (⋃xa∈A. 𝒟 (xa → x xa))"
by (metis (mono_tags, lifting) SUP_mono ‹x ⊑ y› fun_below_iff le_approx1 mono_Mprefix0 write0_def)
next
fix x::"'a ⇒ 'a process" and y::"'a ⇒ 'a process"
assume *:"A ≠ {}" and **:"x ⊑ y"
have *** : "⋀z. z ∈ A ⟹ x z ⊑ y z " by (simp add: ‹x ⊑ y› fun_belowD)
with * show "∀s. (∀xa∈A. s ∉ 𝒟 (xa → x xa)) ⟶ Ra (Mndetprefix A x) s = Ra (Mndetprefix A y) s"
unfolding Ra_def
by (auto simp:proc_ord2a mono_Mprefix0 write0_def F_Mndetprefix)
(meson le_approx2 mono_Mprefix0 write0_def)+
next
fix x::"'a ⇒ 'a process" and y::"'a ⇒ 'a process"
assume *:"A ≠ {}" and "x ⊑ y"
have *** : "⋀z. z ∈ A ⟹ (z → x z) ⊑ (z → y z) "
by (metis ‹x ⊑ y› fun_below_iff mono_Mprefix0 write0_def)
with * show "min_elems (⋃xa∈A. 𝒟 (xa → x xa)) ⊆ (⋃x∈A. 𝒯 (x → y x))"
unfolding min_elems_def apply auto
by (metis Set.set_insert elem_min_elems insert_subset le_approx3 le_less min_elems5)
qed
qed
lemma Mndetprefix_chainpreserving: "chain Y ⟹ chain (λi. (⊓ z ∈ A → Y i z))"
apply(rule chainI, rename_tac i)
apply(frule_tac i="i" in chainE)
by (simp add: below_fun_def mono_Mprefix0 write0_def monofunE)
lemma contlub_Mndetprefix : "contlub (Mndetprefix A)"
proof(cases "A={}")
case True
then show ?thesis by(auto simp: contlub_def)
next
case False
show ?thesis
proof(rule contlubI, rule proc_ord_proc_eq_spec)
fix Y :: "nat ⇒ 'a ⇒ 'a process"
assume a:"chain Y"
show "(⊓x∈A → (⨆i. Y i) x) ⊑ (⨆i. ⊓x∈A → Y i x)"
proof(simp add:le_approx_def, intro conjI allI impI)
show "𝒟 (⨆i. ⊓x∈A → Y i x) ⊆ 𝒟 (⊓x∈A → Lub Y x)"
using a False D_LUB[OF Mndetprefix_chainpreserving[OF a], of A]
limproc_is_thelub[OF Mndetprefix_chainpreserving[OF a], of A]
apply (auto simp add:write0_def D_Mprefix D_LUB[OF ch2ch_fun[OF a]]
limproc_is_thelub_fun[OF a] D_Mndetprefix)
by (metis (mono_tags, opaque_lifting) event.inject)
next
fix s :: "'a event list"
assume "s ∉ 𝒟 (⊓x∈A → Lub Y x)"
show "Ra (⊓x∈A → Lub Y x) s = Ra (⨆i. ⊓x∈A → Y i x) s"
unfolding Ra_def
using a False F_LUB[OF Mndetprefix_chainpreserving[OF a], of A]
limproc_is_thelub[OF Mndetprefix_chainpreserving[OF a], of A]
apply (auto simp add:write0_def F_Mprefix F_LUB[OF ch2ch_fun[OF a]]
limproc_is_thelub_fun[OF a] F_Mndetprefix)
by (metis (mono_tags, opaque_lifting) event.inject)
next
show "min_elems (𝒟 (⊓x∈A → Lub Y x)) ⊆ 𝒯 (⨆i. ⊓x∈A → Y i x)"
unfolding min_elems_def
using a False limproc_is_thelub[OF Mndetprefix_chainpreserving[OF a], of A]
D_LUB[OF Mndetprefix_chainpreserving[OF a], of A]
F_LUB[OF Mndetprefix_chainpreserving[OF a], of A]
by (auto simp add:D_T write0_def D_Mprefix F_Mprefix D_Mndetprefix F_Mndetprefix
D_LUB[OF ch2ch_fun[OF a]] F_LUB[OF ch2ch_fun[OF a]]
limproc_is_thelub_fun[OF a])
qed
next
fix Y :: "nat ⇒ 'a ⇒ 'a process"
assume a:"chain Y"
show "𝒟 (⊓x∈A → (⨆i. Y i) x) ⊆ 𝒟 (⨆i. ⊓x∈A → Y i x)"
using a False D_LUB[OF Mndetprefix_chainpreserving[OF a], of A]
limproc_is_thelub[OF Mndetprefix_chainpreserving[OF a], of A]
by (auto simp add:write0_def D_Mprefix D_Mndetprefix D_LUB[OF ch2ch_fun[OF a]]
limproc_is_thelub_fun[OF a])
qed
qed
lemma Mndetprefix_cont[simp]: "(⋀x. cont (f x)) ⟹ cont (λy. (⊓ z ∈ A → (f z y)))"
apply(rule_tac f = "λz y. (f y z)" in Cont.cont_compose, rule monocontlub2cont)
by (auto intro: mono_Mndetprefix contlub_Mndetprefix Fun_Cpo.cont2cont_lambda)
end