Theory Process_norm
chapter‹ Normalisation of Deterministic CSP Processes ›
theory Process_norm
imports "HOL-CSP.Assertions" "HOL-CSP.CSP_Induct"
begin
section‹Deterministic normal-forms with explicit state›
abbreviation "P_dnorm τ υ ≡ (μ X. (λ s. □ e ∈ (τ s) → X (υ s e)))"
notation P_dnorm (‹P⇩n⇩o⇩r⇩m⟦_,_⟧› 60)
lemma dnorm_cont[simp]:
fixes τ::"'σ::type ⇒ 'event::type set" and υ::"'σ ⇒ 'event ⇒ 'σ"
shows "cont (λX. (λs. □ e ∈ (τ s) → X (υ s e)))" (is "cont ?f")
proof -
have "cont (λX. ?f X s)" for s by (simp add:cont_fun)
then show ?thesis by simp
qed
section‹Interleaving product lemma›
lemma dnorm_inter:
fixes τ⇩1 ::"'σ⇩1::type ⇒ 'event::type set" and τ⇩2::"'σ⇩2::type ⇒ 'event set"
and υ⇩1 ::"'σ⇩1 ⇒ 'event ⇒ 'σ⇩1" and υ⇩2::"'σ⇩2 ⇒ 'event ⇒ 'σ⇩2"
defines P: "P ≡ P⇩n⇩o⇩r⇩m⟦τ⇩1,υ⇩1⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
defines Q: "Q ≡ P⇩n⇩o⇩r⇩m⟦τ⇩2,υ⇩2⟧" (is "Q ≡ fix⋅(Λ X. ?Q X)")
assumes indep: ‹∀s⇩1 s⇩2. τ⇩1 s⇩1 ∩ τ⇩2 s⇩2 = {}›
defines Tr: "τ ≡ (λ(s⇩1,s⇩2). τ⇩1 s⇩1 ∪ τ⇩2 s⇩2)"
defines Up: "υ ≡ (λ(s⇩1,s⇩2) e. if e ∈ τ⇩1 s⇩1 then (υ⇩1 s⇩1 e,s⇩2)
else if e ∈ τ⇩2 s⇩2 then (s⇩1, υ⇩2 s⇩2 e) else (s⇩1,s⇩2))"
defines S: "S ≡ P⇩n⇩o⇩r⇩m⟦τ,υ⟧" (is "S ≡ fix⋅(Λ X. ?S X)")
shows "(P s⇩1 ||| Q s⇩2) = S (s⇩1,s⇩2)"
proof -
have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp
have Q_rec: "Q = ?Q Q" using fix_eq[of "(Λ X. ?Q X)"] Q by simp
have S_rec: "S = ?S S" using fix_eq[of "(Λ X. ?S X)"] S by simp
have dir1: "∀ s⇩1 s⇩2. (P s⇩1 ||| Q s⇩2) ⊑⇩F⇩D S (s⇩1, s⇩2)"
proof(subst P, subst Q,
induct rule:parallel_fix_ind_inc[of "λx y. ∀ s⇩1 s⇩2. (x s⇩1 ||| y s⇩2) ⊑⇩F⇩D S (s⇩1,s⇩2)"])
case admissibility
then show ?case
by (intro adm_all le_FD_adm) (simp_all add: cont2cont_fun monofunI)
next
case (base_fst y)
then show ?case by (metis app_strict BOT_leFD Sync_BOT Sync_commute)
next
case (base_snd x)
then show ?case by (simp add: Sync_BOT)
next
case (step x)
then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
proof(intro allI)
fix s⇩1 s⇩2
show "?C s⇩1 s⇩2"
apply simp
apply (subst Mprefix_Sync_distr_indep[where S = "{}", simplified])
apply (subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
apply (intro mono_Det_FD mono_Mprefix_FD)
using step(3)[simplified] indep apply simp
using step(2)[simplified] indep by fastforce
qed
qed
have dir2: "∀ s⇩1 s⇩2. S (s⇩1, s⇩2) ⊑⇩F⇩D (P s⇩1 ||| Q s⇩2)"
proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s⇩1 s⇩2. x (s⇩1,s⇩2) ⊑⇩F⇩D (P s⇩1 ||| Q s⇩2)" 1])
case admissibility
show ?case by (intro adm_all le_FD_adm) (simp_all add: cont_fun monofunI)
next
case base_k_steps
then show ?case by simp
next
case step
then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
proof(intro allI)
fix s⇩1 s⇩2
have P_rec_sym:"Mprefix (τ⇩1 s⇩1) (λe. P (υ⇩1 s⇩1 e)) = P s⇩1" using P_rec by metis
have Q_rec_sym:"Mprefix (τ⇩2 s⇩2) (λe. Q (υ⇩2 s⇩2 e)) = Q s⇩2" using Q_rec by metis
show "?C s⇩1 s⇩2"
apply (simp add: Tr Up Mprefix_Un_distrib)
apply (subst P_rec, subst Q_rec, subst Mprefix_Sync_distr_indep[where S="{}", simplified])
apply (intro mono_Det_FD mono_Mprefix_FD)
apply (subst Q_rec_sym, simp add:step[simplified])
apply (subst P_rec_sym) using step[simplified] indep by fastforce
qed
qed
from dir1 dir2 show ?thesis using FD_antisym by blast
qed
section ‹Synchronous product lemma›
lemma dnorm_par:
fixes τ⇩1 ::"'σ⇩1::type ⇒ 'event::type set" and τ⇩2::"'σ⇩2::type ⇒ 'event set"
and υ⇩1 ::"'σ⇩1 ⇒ 'event ⇒ 'σ⇩1" and υ⇩2::"'σ⇩2 ⇒ 'event ⇒ 'σ⇩2"
defines P: "P ≡ P⇩n⇩o⇩r⇩m⟦τ⇩1,υ⇩1⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
defines Q: "Q ≡ P⇩n⇩o⇩r⇩m⟦τ⇩2,υ⇩2⟧" (is "Q ≡ fix⋅(Λ X. ?Q X)")
defines Tr: "τ ≡ (λ(s⇩1,s⇩2). τ⇩1 s⇩1 ∩ τ⇩2 s⇩2)"
defines Up: "υ ≡ (λ(s⇩1,s⇩2) e. (υ⇩1 s⇩1 e, υ⇩2 s⇩2 e))"
defines S: "S ≡ P⇩n⇩o⇩r⇩m⟦τ,υ⟧" (is "S ≡ fix⋅(Λ X. ?S X)")
shows "(P s⇩1 || Q s⇩2) = S (s⇩1,s⇩2)"
proof -
have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp
have Q_rec: "Q = ?Q Q" using fix_eq[of "(Λ X. ?Q X)"] Q by simp
have S_rec: "S = ?S S" using fix_eq[of "(Λ X. ?S X)"] S by simp
have dir1: "∀ s⇩1 s⇩2. (P s⇩1 || Q s⇩2) ⊑⇩F⇩D S (s⇩1, s⇩2)"
proof(subst P, subst Q,
induct rule:parallel_fix_ind[of "λx y. ∀ s⇩1 s⇩2. (x s⇩1 || y s⇩2) ⊑⇩F⇩D S (s⇩1,s⇩2)"])
case adm:1
then show ?case
by (intro adm_all le_FD_adm) (simp_all add: cont2cont_fun monofunI)
next
case base:2
then show ?case by (simp add: Sync_BOT)
next
case step:(3 x y)
then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
proof(intro allI)
fix s⇩1 s⇩2
show "?C s⇩1 s⇩2"
apply(simp)
apply(subst Mprefix_Sync_distr_subset[where S="UNIV", simplified])
apply(subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
by (simp add: step)
qed
qed
have dir2: "∀ s⇩1 s⇩2. S (s⇩1, s⇩2) ⊑⇩F⇩D (P s⇩1 || Q s⇩2)"
proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s⇩1 s⇩2. x (s⇩1,s⇩2) ⊑⇩F⇩D (P s⇩1 || Q s⇩2)" 1])
case admissibility
show ?case by (intro adm_all le_FD_adm) (simp_all add: cont_fun monofunI)
next
case base_k_steps
then show ?case by simp
next
case step
then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
proof(intro allI)
fix s⇩1 s⇩2
have P_rec_sym:"Mprefix (τ⇩1 s⇩1) (λe. P (υ⇩1 s⇩1 e)) = P s⇩1" using P_rec by metis
have Q_rec_sym:"Mprefix (τ⇩2 s⇩2) (λe. Q (υ⇩2 s⇩2 e)) = Q s⇩2" using Q_rec by metis
show "?C s⇩1 s⇩2"
apply(simp add: Tr Up)
apply(subst P_rec, subst Q_rec, subst Mprefix_Sync_distr_subset[where S="UNIV", simplified])
apply(rule mono_Mprefix_FD)
using step by auto
qed
qed
from dir1 dir2 show ?thesis using FD_antisym by blast
qed
section‹Consequences›
inductive_set ℜ for τ ::"'σ::type ⇒ 'event::type set"
and υ ::"'σ ⇒ 'event ⇒ 'σ"
and σ⇩0 ::'σ
where rbase: "σ⇩0 ∈ ℜ τ υ σ⇩0"
| rstep: "s ∈ ℜ τ υ σ⇩0 ⟹ e ∈ τ s ⟹ υ s e ∈ ℜ τ υ σ⇩0"
lemma deadlock_free_dnorm_ :
fixes τ ::"'σ::type ⇒ 'event::type set"
and υ ::"'σ ⇒ 'event ⇒ 'σ"
and σ⇩0 ::'σ
assumes non_reachable_sink: "∀s ∈ ℜ τ υ σ⇩0. τ s ≠ {}"
defines P: "P ≡ P⇩n⇩o⇩r⇩m⟦τ,υ⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
shows "s ∈ ℜ τ υ σ⇩0 ⟹ deadlock_free_v2 (P s)"
proof(unfold deadlock_free_v2_FD DF⇩S⇩K⇩I⇩P_def, induct arbitrary:s rule:fix_ind)
show "adm (λa. ∀x. x ∈ ℜ τ υ σ⇩0 ⟶ a ⊑⇩F⇩D P x)" by (simp add: monofun_def)
next
fix s :: "'σ"
show "s ∈ ℜ τ υ σ⇩0 ⟹ ⊥ ⊑⇩F⇩D P s" by simp
next
fix s :: "'σ" and x :: "'event process"
have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp
assume 1 : "⋀s. s ∈ ℜ τ υ σ⇩0 ⟹ x ⊑⇩F⇩D P s"
and 2 : "s ∈ ℜ τ υ σ⇩0 "
from 1 2 show "(Λ x. (⊓xa∈UNIV → x) ⊓ SKIP)⋅x ⊑⇩F⇩D P s"
apply (subst P_rec, rule_tac trans_FD[rotated, OF Mprefix_refines_Mndetprefix_FD])
apply simp
apply (rule mono_Ndet_FD_left)
apply (rule trans_FD[OF mono_Mndetprefix_FD_set[of ‹τ s› ‹UNIV›]
mono_Mndetprefix_FD[rule_format, OF 1]])
using non_reachable_sink[rule_format, OF 2] apply assumption
by blast (meson ℜ.rstep)
qed
lemmas deadlock_free_dnorm = deadlock_free_dnorm_[rotated, OF rbase, rule_format]
end