Theory Multi_Sequential_Composition
section ‹Multiple Sequential Composition›
theory Multi_Sequential_Composition
imports "HOL-CSP.CSP"
begin
text ‹Because of the fact that \<^term>‹SKIP r› is not exactly a neutral element for
@{const [source] Seq} (cf @{thm SKIP_Seq Seq_SKIP}), we do the folding
on the reversed list.›
subsection ‹Definition›
fun MultiSeq_rev :: ‹['b list, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
where MultiSeq_rev_Nil : ‹MultiSeq_rev [] P = SKIP undefined›
| MultiSeq_rev_Cons : ‹MultiSeq_rev (l # L) P = MultiSeq_rev L P ❙; P l›
definition MultiSeq :: ‹['b list, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
where ‹MultiSeq L P ≡ MultiSeq_rev (rev L) P›
lemma MultiSeq_Nil [simp] : ‹MultiSeq [] P = SKIP undefined›
and MultiSeq_snoc [simp] : ‹MultiSeq (L @ [l]) P = MultiSeq L P ❙; P l›
by (simp_all add: MultiSeq_def)
lemma MultiSeq_elims :
‹MultiSeq L P = Q ⟹
(⋀P'. L = [] ⟹ P = P' ⟹ Q = SKIP undefined ⟹ thesis) ⟹
(⋀l L' P'. L = L' @ [l] ⟹ P = P' ⟹ Q = MultiSeq L' P' ❙; P' l ⟹ thesis) ⟹ thesis›
by (simp add: MultiSeq_def, erule MultiSeq_rev.elims, simp_all)
syntax "_MultiSeq" :: ‹[pttrn, 'b list, 'b ⇒ 'r ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'r] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
(‹(3SEQ _∈@_./ _)› [78,78,77] 77)
syntax_consts "_MultiSeq" ⇌ MultiSeq
translations "SEQ p ∈@ L. P" ⇌ "CONST MultiSeq L (λp. P)"
subsection ‹First Properties›
lemma ‹SEQ p ∈@ []. P p = SKIP undefined› by (fact MultiSeq_Nil)
lemma ‹SEQ i ∈@ (L @ [l]). P i = SEQ i ∈@ L. P i ❙; P l› by (fact MultiSeq_snoc)
lemma MultiSeq_singl [simp] : ‹SEQ l ∈@ [l]. P l = P l› by (simp add: MultiSeq_def)
subsection ‹Some Tests›
lemma ‹SEQ p ∈@ []. P p = SKIP undefined›
and ‹SEQ p ∈@ [a]. P p = P a›
and ‹SEQ p ∈@ [a, b]. P p = P a ❙; P b›
and ‹SEQ p ∈@ [a, b, c]. P p = P a ❙; P b ❙; P c›
by (simp_all add: MultiSeq_def)
lemma test_MultiSeq: ‹(SEQ p ∈@ [1::int .. 3]. P p) = P 1 ❙; P 2 ❙; P 3›
by (simp add: upto.simps MultiSeq_def)
subsection ‹Continuity›
lemma mono_MultiSeq :
‹(⋀x. x ∈ set L ⟹ P x ⊑ Q x) ⟹ SEQ l ∈@ L. P l ⊑ SEQ l ∈@ L. Q l›
by (induct L rule: rev_induct, simp_all add: fun_belowI mono_Seq)
lemma MultiSeq_cont[simp]:
‹(⋀x. x ∈ set L ⟹ cont (P x)) ⟹ cont (λy. SEQ z ∈@ L. P z y)›
by (induct L rule: rev_induct) simp_all
subsection ‹Factorization of \<^const>‹Seq› in front of \<^const>‹MultiSeq››
lemma MultiSeq_factorization_append:
‹L2 ≠ [] ⟹ SEQ p ∈@ L1. P p ❙; SEQ p ∈@ L2. P p = SEQ p ∈@ (L1 @ L2). P p›
by (induct L2 rule: rev_induct, simp_all)
(metis (no_types, lifting) MultiSeq_singl MultiSeq_snoc
Seq_assoc append_assoc append_self_conv2)
subsection ‹\<^term>‹⊥› Absorbtion›
lemma MultiSeq_BOT_absorb:
‹SEQ z ∈@ (L1 @ a # L2). P z = SEQ z ∈@ L1. P z ❙; ⊥› if ‹P a = ⊥›
proof (cases ‹L2 = []›)
from ‹P a = ⊥› show ‹L2 = [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; ⊥› by simp
next
show ‹L2 ≠ [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; ⊥›
by (simp add: ‹P a = ⊥› flip: Seq_assoc MultiSeq_factorization_append
[of L2 ‹L1 @ [a]›, simplified])
qed
subsection ‹First Properties›
lemma MultiSeq_SKIP_neutral:
‹SEQ z ∈@ (L1 @ a # L2). P z =
( if L2 = [] then SEQ z ∈@ L1. P z ❙; SKIP r
else SEQ z ∈@ (L1 @ L2). P z)› if ‹P a = SKIP r›
proof (split if_split, intro conjI impI)
show ‹L2 = [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; SKIP r›
by (simp add: ‹P a = SKIP r›)
next
assume ‹L2 ≠ []›
have ‹MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; P a ❙; MultiSeq L2 P›
by (metis (mono_tags, opaque_lifting) Cons_eq_appendI MultiSeq_factorization_append
MultiSeq_snoc ‹L2 ≠ []› append_eq_appendI self_append_conv2)
also have ‹… = MultiSeq L1 P ❙; MultiSeq L2 P›
by (simp add: ‹P a = SKIP r› flip: Seq_assoc)
also have ‹… = MultiSeq (L1 @ L2) P›
by (simp add: MultiSeq_factorization_append ‹L2 ≠ []›)
finally show ‹MultiSeq (L1 @ a # L2) P = MultiSeq (L1 @ L2) P› .
qed
lemma MultiSeq_STOP_absorb:
‹SEQ z ∈@ (L1 @ a # L2). P z = SEQ z ∈@ L1. P z ❙; STOP› if ‹P a = STOP›
proof (cases ‹L2 = []›)
show ‹L2 = [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; STOP›
by (simp add: ‹P a = STOP›)
next
show ‹L2 ≠ [] ⟹ MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ❙; STOP›
by (simp add: ‹P a = STOP› flip: Seq_assoc MultiSeq_factorization_append
[of L2 ‹L1 @ [a]›, simplified])
qed
lemma mono_MultiSeq_eq:
‹(⋀x. x ∈ set L ⟹ P x = Q x) ⟹ MultiSeq L P = MultiSeq L Q›
by (induct L rule: rev_induct) simp_all
subsection ‹Commutativity›
text ‹Of course, since the sequential composition \<^term>‹P ❙; Q› is not commutative,
the result here is negative: the order of the elements of list \<^term>‹L›
does matter in @{term [eta_contract = false] ‹SEQ z ∈@ L. P z›}.›
subsection ‹Behaviour with Injectivity›
lemma inj_on_mapping_over_MultiSeq:
‹inj_on f (set C) ⟹
SEQ x ∈@ C. P x = SEQ x ∈@ map f C. P (inv_into (set C) f x)›
proof (induct C rule: rev_induct)
show ‹inj_on f (set []) ⟹ MultiSeq [] P =
SEQ x∈@map f []. P (inv_into (set []) f x)› by simp
next
case (snoc a C)
hence f1: ‹inv_into (insert a (set C)) f (f a) = a› by force
show ?case
apply (simp add: f1, intro ext arg_cong[where f = ‹λx. x ❙; P a›])
apply (subst "snoc.hyps"(1), rule inj_on_subset[OF "snoc.prems"],
simp add: subset_insertI)
using snoc.prems by (auto intro!: mono_MultiSeq_eq)
qed
subsection ‹Definition of ‹first_elem››
primrec first_elem :: ‹['a ⇒ bool, 'a list] ⇒ nat›
where ‹first_elem P [] = 0›
| ‹first_elem P (x # L) = (if P x then 0 else Suc (first_elem P L))›
text ‹\<^const>‹first_elem› returns the first index \<^term>‹i› such that
\<^term>‹P (L ! i) = True› if it exists, \<^term>‹length L› otherwise.
This will be very useful later.›
value ‹first_elem (λx. 4 < x) [0::nat, 2, 5]›
lemma ‹first_elem (λx. 5 < x) [0::nat, 2, 5] = 3› by simp
lemma ‹P ` set L ⊆ {False} ⟹ first_elem P L = length L› by (induct L; simp)
end