Theory Ndet
section‹ Nondeterministic Choice Operator Definition ›
theory Ndet
imports Process
begin
subsection‹The Ndet Operator Definition›
lift_definition
Ndet :: "['α process,'α process] ⇒ 'α process" (infixl ‹|-|› 80)
is "λP Q. (ℱ P ∪ ℱ Q , 𝒟 P ∪ 𝒟 Q)"
proof(simp only: fst_conv snd_conv Rep_process is_process_def DIVERGENCES_def FAILURES_def,
intro conjI)
show "⋀P Q. ([], {}) ∈ (ℱ P ∪ ℱ Q)"
by(simp add: is_processT1)
next
show "⋀P Q. ∀s X. (s, X) ∈ (ℱ P ∪ ℱ Q) ⟶ front_tickFree s"
by(auto simp: is_processT2)
next
show "⋀P Q. ∀s t. (s @ t, {}) ∈(ℱ P ∪ ℱ Q) ⟶ (s, {}) ∈ (ℱ P ∪ ℱ Q)"
by (auto simp: is_processT1 dest!: is_processT3[rule_format])
next
show "⋀P Q. ∀s X Y. (s, Y) ∈ (ℱ P ∪ ℱ Q) ∧ X ⊆ Y ⟶ (s, X) ∈ (ℱ P ∪ ℱ Q)"
by(auto dest: is_processT4[rule_format,OF conj_commute[THEN iffD1], OF conjI])
next
show "⋀P Q. ∀sa X Y. (sa, X) ∈ (ℱ P ∪ ℱ Q) ∧ (∀c. c ∈ Y ⟶ (sa @ [c], {}) ∉ (ℱ P ∪ ℱ Q))
⟶ (sa, X ∪ Y) ∈ (ℱ P ∪ ℱ Q)"
by(auto simp: is_processT5 T_F)
next
show "⋀P Q. ∀s X. (s @ [tick], {}) ∈ (ℱ P ∪ ℱ Q) ⟶ (s, X - {tick}) ∈ (ℱ P ∪ ℱ Q)"
apply((rule allI)+, rule impI)
apply(rename_tac s X, case_tac "s=[]", simp_all add: is_processT6[rule_format] T_F_spec)
apply(erule disjE,simp_all add: is_processT6[rule_format] T_F_spec)
apply(erule disjE,simp_all add: is_processT6[rule_format] T_F_spec)
done
next
show "⋀P Q. ∀s t. s ∈ 𝒟 P ∪ 𝒟 Q ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ 𝒟 P ∪ 𝒟 Q"
by(auto simp: is_processT7)
next
show "⋀P Q. ∀s X. s ∈ 𝒟 P ∪ 𝒟 Q ⟶ (s, X) ∈ (ℱ P ∪ ℱ Q)"
by(auto simp: is_processT8[rule_format])
next
show "⋀P Q. ∀s. s @ [tick] ∈ 𝒟 P ∪ 𝒟 Q ⟶ s ∈ 𝒟 P ∪ 𝒟 Q"
by(auto intro!:is_processT9[rule_format])
qed
notation
Ndet (infixl ‹⊓› 80)
subsection ‹The Projections›
lemma F_Ndet : "ℱ (P ⊓ Q) = ℱ P ∪ ℱ Q"
by (simp add: FAILURES_def Failures.rep_eq Ndet.rep_eq)
lemma D_Ndet : "𝒟 (P ⊓ Q) = 𝒟 P ∪ 𝒟 Q"
by (simp add: DIVERGENCES_def Divergences.rep_eq Ndet.rep_eq)
lemma T_Ndet : "𝒯 (P ⊓ Q) = 𝒯 P ∪ 𝒯 Q"
apply (subst Traces.rep_eq, simp add: TRACES_def Failures.rep_eq[symmetric] F_Ndet)
apply(auto simp: T_F F_T is_processT1 Nil_elem_T)
by(rule_tac x="{}" in exI, simp add: T_F F_T is_processT1 Nil_elem_T)+
subsection‹Basic Laws›
text ‹The commutativity of the operator helps to simplify the subsequent
continuity proof and is therefore developed here: ›
lemma Ndet_commute: "(P ⊓ Q) = (Q ⊓ P)"
by(auto simp: Process_eq_spec F_Ndet D_Ndet)
subsection‹The Continuity Rule›
lemma mono_Ndet1: "P ⊑ Q ⟹ 𝒟 (Q ⊓ S) ⊆ 𝒟 (P ⊓ S)"
apply(drule le_approx1)
by (auto simp: Process_eq_spec F_Ndet D_Ndet)
lemma mono_Ndet2: "P ⊑ Q ⟹ (∀ s. s ∉ 𝒟 (P ⊓ S) ⟶ Ra (P ⊓ S) s = Ra (Q ⊓ S) s)"
apply(subst (asm) le_approx_def)
by (auto simp: Process_eq_spec F_Ndet D_Ndet Ra_def)
lemma mono_Ndet3: "P ⊑ Q ⟹ min_elems (𝒟 (P ⊓ S)) ⊆ 𝒯 (Q ⊓ S)"
apply(auto dest!:le_approx3 simp: min_elems_def subset_iff F_Ndet D_Ndet T_Ndet)
apply(erule_tac x="t" in allE, auto)
by (erule_tac x="[]" in allE, auto simp: less_list_def Nil_elem_T D_T)
lemma mono_Ndet[simp] : "P ⊑ Q ⟹ (P ⊓ S) ⊑ (Q ⊓ S)"
by(auto simp:le_approx_def mono_Ndet1 mono_Ndet2 mono_Ndet3)
lemma mono_Ndet_sym[simp] : "P ⊑ Q ⟹ (S ⊓ P) ⊑ (S ⊓ Q)"
by (auto simp: Ndet_commute)
lemma cont_Ndet1:
assumes chain:"chain Y"
shows "((⨆ i. Y i) ⊓ S) = (⨆ i. (Y i ⊓ S))"
proof -
have A : "chain (λi. Y i ⊓ S)"
apply(insert chain,rule chainI)
apply(frule_tac i="i" in chainE)
by(simp)
show ?thesis using chain
by(auto simp add: limproc_is_thelub Process_eq_spec D_Ndet F_Ndet F_LUB D_LUB A)
qed
lemma Ndet_cont[simp]:
assumes f: "cont f"
and g: "cont g"
shows "cont (λx. f x ⊓ g x)"
proof -
have A:"⋀x. cont f ⟹ cont g ⟹ cont (λX. (f x)⊓ X)"
apply(rule contI2, rule monofunI)
apply(auto)
apply(subst Ndet_commute, subst cont_Ndet1)
by (auto simp:Ndet_commute)
have B:"⋀y. cont f ⟹ cont g ⟹ cont (λx. f x ⊓ y)"
apply(rule_tac c="(λ g. g ⊓ y)" in cont_compose)
apply(rule contI2,rule monofunI)
by (simp_all add: cont_Ndet1)
show ?thesis using f g
by (rule_tac f="(λ x. (λ g. f x ⊓ g))" in cont_apply, auto simp: A B)
qed
end