Theory Mprefix
section‹ The Multi-Prefix Operator Definition ›
theory Mprefix
imports Process
begin
subsection‹ The Definition and some Consequences ›
lift_definition Mprefix :: "['a set,'a => 'a process] => 'a process"
is "λA P. ({(tr,ref). tr = [] ∧ ref Int (ev ` A) = {}} ∪
{(tr,ref). tr ≠ [] ∧ hd tr ∈ (ev ` A) ∧
(∃ a. ev a = (hd tr)∧(tl tr,ref)∈ℱ(P a))},
{d. d ≠ [] ∧ hd d ∈ (ev ` A) ∧ (∃ a. ev a = hd d ∧ tl d ∈ 𝒟 (P a))})"
proof -
show ‹is_process ({(tr, ref). tr = [] ∧ ref ∩ ev ` (A :: 'a set) = {}} ∪
{(tr, ref). tr ≠ [] ∧ hd tr ∈ ev ` A ∧
(∃a. ev a = hd tr ∧ (tl tr, ref) ∈ ℱ (P a))},
{d. d ≠ [] ∧ hd d ∈ ev ` A ∧ (∃a. ev a = hd d ∧ tl d ∈ 𝒟 (P a))}) ›
(is ‹is_process(?f, ?d)›) for A P
proof (simp only: is_process_def FAILURES_def DIVERGENCES_def
Product_Type.fst_conv Product_Type.snd_conv,
intro conjI allI impI)
show "([],{}) ∈ ?f" by(simp)
next
fix s:: "'a event list" fix X::"'a event set"
assume H : "(s, X) ∈ ?f"
show "front_tickFree s"
apply(insert H, auto simp: front_tickFree_def tickFree_def
dest!:list_nonMt_append)
apply(rename_tac aa ta x, case_tac "ta", auto simp: front_tickFree_charn
dest! : is_processT2[rule_format])
apply(simp add: tickFree_def)
done
next
fix s t :: "'a event list"
assume "(s @ t, {}) ∈ ?f"
then show "(s, {}) ∈ ?f"
by(auto elim: is_processT3[rule_format])
next
fix s:: "'a event list" fix X Y::"'a event set"
assume "(s, Y) ∈ ?f ∧ X ⊆ Y"
then show "(s, X) ∈ ?f"
by(auto intro: is_processT4[rule_format])
next
fix s:: "'a event list" fix X Y::"'a event set"
assume "(s, X) ∈ ?f ∧ (∀ c. c∈Y ⟶ (s @ [c], {}) ∉ ?f)"
then show "(s, X ∪ Y) ∈ ?f "
by(auto intro!: is_processT1 is_processT5[rule_format])
next
fix s:: "'a event list" fix X::"'a event set"
assume "(s @ [tick], {}) ∈ ?f"
then show "(s, X - {tick}) ∈ ?f"
by(cases s, auto dest!: is_processT6[rule_format])
next
fix s t:: "'a event list" fix X::"'a event set"
assume "s ∈ ?d ∧ tickFree s ∧ front_tickFree t"
then show "s @ t ∈ ?d"
by(auto intro!: is_processT7_S, cases s, simp_all)
next
fix s:: "'a event list" fix X::"'a event set"
assume "s ∈ ?d"
then show "(s, X) ∈ ?f"
by(auto simp: is_processT8_S)
next
fix s:: "'a event list"
assume "s @ [tick] ∈ ?d"
then show "s ∈ ?d"
apply(auto)
apply(cases s, simp_all)
apply(cases s, auto intro: is_processT9[rule_format])
done
qed
qed
syntax
"_Mprefix" :: "[pttrn,'a set,'a process] ⇒ 'a process" ("(3□(_/∈_)/ → (_))"[0,0,64]64)
term "Ball A (λx. P)"
translations
"□x∈A → P" ⇌ "CONST Mprefix A (λx. P)"
text‹Syntax Check:›
term ‹□x∈A → □y∈A → □z∈A → P z x y = Q›
lemma is_process_REP_Mprefix' :
"is_process ({(tr,ref). tr=[] ∧ ref ∩ (ev ` A) = {}} ∪
{(tr,ref). tr ≠ [] ∧ hd tr ∈ (ev ` A) ∧
(∃ a. ev a = (hd tr) ∧ (tl tr,ref) ∈ ℱ(P a))},
{d. d ≠ [] ∧ hd d ∈ (ev ` A) ∧
(∃ a. ev a = hd d ∧ tl d ∈ 𝒟(P a))})"
(is "is_process(?f, ?d)")
proof (simp only:is_process_def FAILURES_def DIVERGENCES_def
Product_Type.fst_conv Product_Type.snd_conv,
intro conjI allI impI,goal_cases)
case 1
show "([],{}) ∈ ?f" by(simp)
next
case (2 s X)
assume H : "(s, X) ∈ ?f"
have "front_tickFree s"
apply(insert H, auto simp: front_tickFree_def tickFree_def
dest!:list_nonMt_append)
apply(rename_tac aa ta x, case_tac "ta", auto simp: front_tickFree_charn
dest! : is_processT2[rule_format])
apply(simp add: tickFree_def)
done
then show "front_tickFree s" by(auto)
next
case (3 s t)
assume H : "(s @ t, {}) ∈ ?f"
show "(s, {}) ∈ ?f" using H by(auto elim: is_processT3[rule_format])
next
case (4 s X Y)
assume H1: "(s, Y) ∈ ?f ∧ X ⊆ Y"
then show "(s, X) ∈ ?f" by(auto intro: is_processT4[rule_format])
next
case (5 s X Y)
assume "(s, X) ∈ ?f ∧ (∀ c. c∈Y ⟶ (s @ [c], {}) ∉ ?f)"
then show "(s, X ∪ Y) ∈ ?f" by(auto intro!: is_processT1 is_processT5[rule_format])
next
case (6 s X)
assume "(s @ [tick], {}) ∈ ?f"
then show "(s, X - {tick}) ∈ ?f" by(cases s, auto dest!: is_processT6[rule_format])
next
case (7 s t)
assume H1 : "s ∈ ?d ∧ tickFree s ∧ front_tickFree t"
have 7: "s @ t ∈ ?d"
using H1 by(auto intro!: is_processT7_S, cases s, simp_all)
then show "s @ t ∈ ?d" using H1 by(auto)
next
case (8 s X)
assume H : "s ∈ ?d"
then show "(s, X) ∈ ?f" using H by(auto simp: is_processT8_S)
next
case (9 s)
assume H: "s @ [tick] ∈ ?d"
then have 9: "s ∈ ?d"
apply(auto)
apply(cases s, simp_all)
apply(cases s, auto intro: is_processT9[rule_format])
done
then show "s ∈ ?d" by(auto)
qed
lemma Rep_Abs_Mprefix'' :
assumes H1 : "f = {(tr, ref). tr = [] ∧ ref ∩ ev ` A = {}} ∪
{(tr, ref). tr ≠ [] ∧ hd tr ∈ ev ` A
∧ (∃a. ev a = hd tr ∧ (tl tr, ref) ∈ ℱ (P a))}"
and H2 : "d = {d. d ≠ [] ∧ hd d ∈ (ev ` A) ∧
(∃ a. ev a = hd d ∧ tl d ∈ 𝒟(P a))}"
shows "Rep_process (Abs_process (f,d)) = (f,d)"
using Abs_process_inverse H1 H2 is_process_REP_Mprefix' by blast
subsection ‹ Projections in Prefix ›
lemma F_Mprefix :
"ℱ (□ x ∈ A → P x) = {(tr,ref). tr=[] ∧ ref ∩ (ev ` A) = {}} ∪
{(tr,ref). tr ≠ [] ∧ hd tr ∈ (ev ` A) ∧
(∃ a. ev a = (hd tr) ∧ (tl tr,ref) ∈ ℱ(P a))}"
by (subst Failures.rep_eq, simp add: Mprefix.rep_eq FAILURES_def)
lemma D_Mprefix:
"𝒟 (□ x ∈ A → P x) = {d. d ≠ [] ∧ hd d ∈ (ev ` A) ∧
(∃ a. ev a = hd d ∧ tl d ∈ 𝒟(P a))}"
by (subst Divergences.rep_eq, simp add: Mprefix.rep_eq DIVERGENCES_def)
lemma T_Mprefix:
"𝒯 (□ x ∈ A → P x)={s. s=[] ∨ (∃ a. a∈A ∧ s≠[] ∧ hd s = ev a ∧ tl s ∈ 𝒯(P a))}"
by (subst Traces.rep_eq, auto simp add: TRACES_def Failures.rep_eq[symmetric] F_Mprefix)
(use F_T T_F in ‹blast+›)
subsection ‹ Basic Properties ›
lemma tick_T_Mprefix [simp]: "[tick] ∉ 𝒯 (□ x ∈ A → P x)"
by(simp add:T_Mprefix)
lemma Nil_Nin_D_Mprefix [simp]: "[] ∉ 𝒟 (□ x ∈ A → P x)"
by(simp add: D_Mprefix)
subsection‹ Proof of Continuity Rule ›
subsubsection‹ Backpatch Isabelle 2009-1›
definition
contlub :: "('a::cpo ⇒ 'b::cpo) ⇒ bool"
where
"contlub f = (∀Y. chain Y ⟶ f (⨆ i. Y i) = (⨆ i. f (Y i)))"
lemma contlubE:
"⟦contlub f; chain Y⟧ ⟹ f (⨆ i. Y i) = (⨆ i. f (Y i))"
by (simp add: contlub_def)
lemma monocontlub2cont: "⟦monofun f; contlub f⟧ ⟹ cont f"
apply (rule contI)
apply (rule thelubE)
apply (erule (1) ch2ch_monofun)
apply (erule (1) contlubE [symmetric])
done
lemma contlubI:
"(⋀Y. chain Y ⟹ f (⨆ i. Y i) = (⨆ i. f (Y i))) ⟹ contlub f"
by (simp add: contlub_def)
lemma cont2contlub: "cont f ⟹ contlub f"
apply (rule contlubI)
apply (rule Porder.po_class.lub_eqI [symmetric])
apply (erule (1) contE)
done
subsubsection‹ Core of Proof ›
lemma mono_Mprefix1:
"∀a∈A. P a ⊑ Q a ⟹ 𝒟 (Mprefix A Q) ⊆ 𝒟 (Mprefix A P)"
apply(auto simp: D_Mprefix) using le_approx1 by blast
lemma mono_Mprefix2:
"∀x∈A. P x ⊑ Q x ⟹
∀s. s ∉ 𝒟 (Mprefix A P) ⟶ Ra (Mprefix A P) s = Ra (Mprefix A Q) s"
apply (auto simp: Ra_def D_Mprefix F_Mprefix) using proc_ord2a by blast+
lemma mono_Mprefix3 :
assumes H:"∀x∈A. P x ⊑ Q x"
shows " min_elems (𝒟 (Mprefix A P)) ⊆ 𝒯 (Mprefix A Q)"
proof(auto simp: min_elems_def D_Mprefix T_Mprefix image_def, goal_cases)
case (1 x a)
with H[rule_format, of a, OF 1(2)] show ?case
apply(auto dest!: le_approx3 simp: min_elems_def)
apply(subgoal_tac "∀t. t ∈ 𝒟 (P a) ⟶ ¬ t < tl x", auto)
apply(rename_tac t, erule_tac x="(ev a)#t" in allE, auto)
using less_cons hd_Cons_tl by metis
qed
lemma mono_Mprefix0:
"∀x∈A. P x ⊑ Q x ⟹ Mprefix A P ⊑ Mprefix A Q"
apply(simp add: le_approx_def mono_Mprefix1 mono_Mprefix3)
apply(rule mono_Mprefix2)
apply(auto simp: le_approx_def)
done
lemma mono_Mprefix[simp]: "monofun(Mprefix A)"
by(auto simp: Fun_Cpo.below_fun_def monofun_def mono_Mprefix0)
lemma proc_ord2_set:
"P ⊑ Q ⟹ {(s, X). s ∉ 𝒟 P ∧ (s, X) ∈ ℱ P} = {(s, X). s ∉ 𝒟 P ∧ (s, X) ∈ ℱ Q}"
by(auto simp: le_approx2)
lemma proc_ord_proc_eq_spec: "P ⊑ Q ⟹ 𝒟 P ⊆ 𝒟 Q ⟹ P = Q"
by (metis (mono_tags, lifting) below_antisym below_refl le_approx_def subset_antisym)
lemma Mprefix_chainpreserving: "chain Y ⟹ chain (λi. Mprefix A (Y i))"
apply(rule chainI, rename_tac i)
apply(frule_tac i="i" in chainE)
by(simp add: mono_Mprefix0 fun_belowD)
lemma limproc_is_thelub_fun:
assumes "chain S"
shows "(Lub S c) = lim_proc (range (λx. (S x c)))"
proof -
have "⋀xa. chain (λx. S x xa)"
using `chain S` by(auto intro!: chainI simp: chain_def fun_belowD )
then show ?thesis by (metis contlub_lambda limproc_is_thelub)
qed
lemma contlub_Mprefix : "contlub(%P. Mprefix A P)"
proof(rule contlubI, rule proc_ord_proc_eq_spec)
fix Y :: "nat ⇒ 'a ⇒ 'a process"
assume C : "chain Y"
have C': "⋀xa. chain (λx. Y x xa)"
apply(insert C,rule chainI)
by(auto simp: chain_def fun_belowD)
show "Mprefix A (⨆ i. Y i) ⊑ (⨆ i. Mprefix A (Y i))"
by(auto simp: Process.le_approx_def F_Mprefix D_Mprefix T_Mprefix C C'
Mprefix_chainpreserving limproc_is_thelub limproc_is_thelub_fun
D_T D_LUB D_LUB_2 F_LUB T_LUB_2 Ra_def min_elems_def)
next
fix Y :: "nat ⇒ 'a ⇒ 'a process"
assume C : "chain Y"
show "𝒟 (Mprefix A (⨆ i. Y i)) ⊆ 𝒟 (⨆ i. Mprefix A (Y i))"
apply(auto simp: Process.le_approx_def F_Mprefix D_Mprefix T_Mprefix
C Mprefix_chainpreserving limproc_is_thelub D_LUB_2)
by (meson C fun_below_iff in_mono is_ub_thelub le_approx1)
qed
lemma Mprefix_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)
apply(rule monocontlub2cont)
apply(auto intro: mono_Mprefix contlub_Mprefix Fun_Cpo.cont2cont_lambda)
done
subsection‹ High-level Syntax for Read and Write ›
text‹ The following syntax introduces the usual channel notation for CSP.
Slightly deviating from conventional wisdom, we view a channel not as a tag in
a pair, rather than as a function of type @{typ "'a⇒'b"}. This paves the way
for \emph{typed} channels over a common universe of events. ›
definition read :: "['a ⇒ 'b,'a set, 'a ⇒ 'b process] ⇒ 'b process"
where "read c A P ≡ Mprefix(c ` A) (P o (inv_into A c))"
definition "write" :: "['a ⇒ 'b, 'a, 'b process] ⇒ 'b process"
where "write c a P ≡ Mprefix {c a} (λ x. P)"
definition write0 :: "['a, 'a process] ⇒ 'a process"
where "write0 a P ≡ Mprefix {a} (λ x. P)"
syntax
"_read" :: "[id, pttrn, 'a process] => 'a process"
("(3(_❙?_) /→ _)" [0,0,78] 78)
"_readX" :: "[id, pttrn, bool,'a process] => 'a process"
("(3(_❙?_)❙|_ /→ _)" [0,0,78] 78)
"_readS" :: "[id, pttrn, 'b set,'a process] => 'a process"
("(3(_❙?_)∈_ /→ _)" [0,0,78] 78)
"_write" :: "[id, 'b, 'a process] => 'a process"
("(3(_❙!_) /→ _)" [0,0,78] 78)
"_writeS" :: "['a, 'a process] => 'a process"
("(3_ /→ _)" [0,78]78)
subsection‹CSP$_M$-Style Syntax for Communication Primitives›
translations
"_read c p P" ⇌ "CONST read c CONST UNIV (λp. P)"
"_write c p P" ⇌ "CONST write c p P"
"_readX c p b P" => "CONST read c {p. b} (λp. P)"
"_writeS a P" ⇌ "CONST write0 a P"
"_readS c p A P" => "CONST read c A (λp. P)"
text‹Syntax Check:›
term‹ d❙?y → c❙!x → P = Q›
lemma read_cont[simp]: "cont P ⟹ cont (λy. read c A (P y))"
unfolding read_def o_def
by (rule Mprefix_cont) (rule cont2cont_fun)
lemma read_cont'[simp]: "(⋀x. cont (f x)) ⟹ cont (λy. c❙?x → f x y)" by simp
lemma write_cont[simp]: "cont (P::('b::cpo ⇒ 'a process)) ⟹ cont(λx. (c❙!a → P x))"
by(simp add:write_def)
corollary write0_cont_lub : "contlub(Mprefix {a})"
using contlub_Mprefix by blast
lemma write0_contlub : "contlub(write0 a)"
unfolding write0_def contlub_def
proof (auto)
fix Y :: "nat ⇒ 'a process"
assume "chain Y"
have * : "chain (λi. (λ_. Y i)::'b ⇒ 'a process)"
by (meson ‹chain Y› fun_below_iff po_class.chain_def)
have **: "(λx. Lub Y) = Lub (λi. (λ_. Y i))"
by(rule ext,metis * ch2ch_fun limproc_is_thelub limproc_is_thelub_fun lub_eq)
show "Mprefix {a} (λx. Lub Y) = (⨆i. Mprefix {a} (λx. Y i))"
apply(subst **, subst contlubE[OF contlub_Mprefix])
by (simp_all add: *)
qed
lemma write0_cont[simp]: "cont (P::('b::cpo ⇒ 'a process)) ⟹ cont(λx. (a → P x))"
by(simp add:write0_def)
end