Theory MultiSync
chapter ‹The MultiSync Operator›
theory MultiSync
imports "HOL-Library.Multiset" PreliminaryWork Patch
begin
section ‹Definition›
text ‹As in the \<^const>‹Ndet› case, we have no neutral element so we will also have to go through lists
first. But the binary operator \<^const>‹Sync› is not idempotent either, so the generalization will be done
on \<^typ>‹'α multiset› and not on \<^typ>‹'α set›.›
text ‹Note that a \<^typ>‹'α multiset› is by construction finite (cf. theorem
@{thm Multiset.finite_set_mset[no_vars]}).›
fun MultiSync_list :: ‹['b set, 'a list, 'a ⇒ 'b process] ⇒ 'b process›
where ‹MultiSync_list S [] P = STOP›
| ‹MultiSync_list S (l # L) P = fold (λx r. r ⟦S⟧ P x) L (P l)›
syntax "_MultiSync_list" :: ‹[pttrn, 'b set, 'a list, 'b process] ⇒ 'b process›
(‹(3❙⟦_❙⟧⇩l_∈_./ _)› 63)
syntax_consts "_MultiSync_list" ⇌ MultiSync_list
translations "❙⟦S❙⟧⇩l p ∈ L. P " ⇌ "CONST MultiSync_list S L (λp. P)"
interpretation MultiSync: comp_fun_commute where f = ‹λx r. r ⟦E⟧ P x›
unfolding comp_fun_commute_def comp_fun_idem_axioms_def comp_def
by (metis Sync_assoc Sync_commute)
lemma MultiSync_list_mset:
‹mset L = mset L' ⟹ MultiSync_list S L P = MultiSync_list S L' P›
apply (cases L; simp)
proof -
fix a l
assume * : ‹add_mset a (mset l) = mset L'› and ** : ‹L = a # l›
then obtain a' l' where *** : ‹ L' = a' # l'›
by (metis list.exhaust mset.simps(2) mset_zero_iff)
note **** = *[simplified ***, simplified]
have a0: ‹a ≠ a' ⟹ MultiSync_list S L P =
fold (λx r. r ⟦S⟧ P x) (a' # (remove1 a' l)) (P a)›
apply (subst fold_multiset_equiv[where ys = ‹l›])
apply (metis MultiSync.comp_fun_commute_axioms comp_fun_commute_def)
apply (simp_all add: * ** ***)
by (metis **** insert_DiffM insert_noteq_member)
have a1: ‹a ≠ a' ⟹ MultiSync_list S L' P =
fold (λx r. r ⟦S⟧ P x) (a # (remove1 a l')) (P a')›
apply (subst fold_multiset_equiv[where ys = ‹l'›])
apply (metis MultiSync.comp_fun_commute_axioms comp_fun_commute_def)
apply (simp_all add: * ** ***)
by (metis **** insert_DiffM insert_noteq_member)
from **** ** *** a0 a1
show ‹fold (λx r. r ⟦S⟧ P x) l (P a) = MultiSync_list S L' P›
apply (cases ‹a = a'›, simp)
apply (subst fold_multiset_equiv[where ys = l'])
apply (metis MultiSync.comp_fun_commute_axioms comp_fun_commute_def)
apply (simp_all)
apply (subst fold_multiset_equiv[where ys = ‹remove1 a l'›],
simp_all add: Sync_commute)
apply (metis MultiSync.comp_fun_commute_axioms
comp_fun_commute.comp_fun_commute)
by (metis add_mset_commute add_mset_diff_bothsides)
qed
definition MultiSync :: ‹['b set, 'a multiset, 'a ⇒ 'b process] ⇒ 'b process›
where ‹MultiSync S M P = MultiSync_list S (SOME L. mset L = M) P›
syntax "_MultiSync" :: ‹[pttrn,'b set,'a multiset,'b process] ⇒ 'b process›
(‹(3❙⟦_❙⟧ _∈#_. / _)› 63)
syntax_consts "_MultiSync" ⇌ MultiSync
translations "❙⟦S❙⟧ p ∈# M. P " ⇌ "CONST MultiSync S M (λp. P)"
text ‹Special case of \<^term>‹MultiSync E P› when \<^term>‹E = {}›.›
abbreviation MultiInter :: ‹['a multiset, 'a ⇒ 'b process] ⇒ 'b process›
where ‹MultiInter M P ≡ MultiSync {} M P›
syntax "_MultiInter" :: ‹[pttrn, 'a multiset, 'b process] ⇒ 'b process›
(‹(3❙|❙|❙| _∈#_. / _)› 77)
syntax_consts "_MultiInter" ⇌ MultiInter
translations "❙|❙|❙| p ∈# M. P" ⇌ "CONST MultiInter M (λp. P)"
text ‹Special case of \<^term>‹MultiSync E P› when \<^term>‹E = UNIV›.›
abbreviation MultiPar :: ‹['a multiset, 'a ⇒ 'b process] ⇒ 'b process›
where ‹MultiPar M P ≡ MultiSync UNIV M P›
syntax "_MultiPar" :: ‹[pttrn, 'a multiset, 'b process] ⇒ 'b process›
(‹(3❙|❙| _∈#_. / _)› 77)
syntax_consts "_MultiPar" ⇌ MultiPar
translations "❙|❙| p ∈# M. P" ⇌ "CONST MultiPar M (λp. P)"
section ‹First Properties›
lemma MultiSync_rec0[simp]: ‹(❙⟦S❙⟧ p ∈# {#}. P p) = STOP›
unfolding MultiSync_def by simp
lemma MultiSync_rec1[simp]: ‹(❙⟦S❙⟧ p ∈# {#a#}. P p) = P a›
unfolding MultiSync_def apply(rule someI2_ex) by simp_all
lemma MultiSync_add[simp]:
‹M ≠ {#} ⟹ (❙⟦S❙⟧ p ∈# add_mset m M. P p) = P m ⟦S⟧ (❙⟦S❙⟧ p ∈# M. P p)›
unfolding MultiSync_def
apply (rule someI2_ex, simp add: ex_mset)+
proof -
fix L L'
assume ‹M ≠ {#}› ‹mset L = M› ‹mset L' = add_mset m M›
thus ‹MultiSync_list S L' P = P m ⟦S⟧ MultiSync_list S L P›
apply (subst MultiSync_list_mset[where L = ‹L'› and L' = ‹L @ [m]›], simp)
by (cases L; simp add: Sync_commute)
qed
lemma mono_MultiSync_eq:
‹∀x ∈# M. P x = Q x ⟹ MultiSync S M P = MultiSync S M Q›
by (induct M rule: induct_subset_mset_empty_single; simp)
lemmas MultiInter_rec0 = MultiSync_rec0[where S = ‹{}›]
and MultiPar_rec0 = MultiSync_rec0[where S = ‹UNIV›]
and MultiInter_rec1 = MultiSync_rec1[where S = ‹{}›]
and MultiPar_rec1 = MultiSync_rec1[where S = ‹UNIV›]
and MultiInter_add = MultiSync_add[where S = ‹{}›]
and MultiPar_add = MultiSync_add[where S = ‹UNIV›]
and mono_MultiInter_eq = mono_MultiSync_eq[where S = ‹{}›]
and mono_MultiPar_eq = mono_MultiSync_eq[where S = ‹UNIV›]
section ‹Some Tests›
lemma ‹(❙⟦S❙⟧⇩l p ∈ []. P p) = STOP›
and ‹(❙⟦S❙⟧⇩l p ∈ [a]. P p) = P a›
and ‹(❙⟦S❙⟧⇩l p ∈ [a, b]. P p) = P a ⟦S⟧ P b›
and ‹(❙⟦S❙⟧⇩l p ∈ [a, b, c]. P p) = P a ⟦S⟧ P b ⟦S⟧ P c›
by simp+
lemma test_MultiSync:
‹(❙⟦S❙⟧ p ∈# mset []. P p) = STOP›
‹(❙⟦S❙⟧ p ∈# mset [a]. P p) = P a›
‹(❙⟦S❙⟧ p ∈# mset [a, b]. P p) = P a ⟦S⟧ P b›
‹(❙⟦S❙⟧ p ∈# mset [a, b, c]. P p) = P a ⟦S⟧ P b ⟦S⟧ P c›
by (simp_all add: Sync_assoc)
lemma MultiSync_set1: ‹MultiSync S (mset_set {k::nat..<k}) P = STOP›
by fastforce
lemma MultiSync_set2: ‹MultiSync S (mset_set {k..<Suc k}) P = P k›
by fastforce
lemma MultiSync_set3:
‹l < k ⟹ MultiSync S (mset_set {l ..< Suc k}) P =
P l ⟦S⟧ (MultiSync S (mset_set {Suc l ..< Suc k}) P)›
by (simp add: Icc_eq_insert_lb_nat atLeastLessThanSuc_atLeastAtMost)
lemma test_MultiSync':
‹(❙⟦S❙⟧ p ∈# mset_set {1::int .. 3}. P p) = P 1 ⟦S⟧ P 2 ⟦S⟧ P 3›
proof -
have ‹{1::int .. 3} = insert 1 (insert 2 (insert 3 {}))› by fastforce
thus ‹(❙⟦S❙⟧ p ∈# mset_set {1::int .. 3}. P p) = P 1 ⟦S⟧ P 2 ⟦S⟧ P 3› by (simp add: Sync_assoc)
qed
lemma test_MultiSync'':
‹(❙⟦S❙⟧ p ∈# mset_set {0::nat .. a}. P p) =
❙⟦S❙⟧ p ∈# mset_set ({a} ∪ {1 .. a} ∪ {0}) . P p›
by (metis Un_insert_right atMost_atLeast0 boolean_algebra_cancel.sup0
image_Suc_lessThan insert_absorb2 insert_is_Un lessThan_Suc
lessThan_Suc_atMost lessThan_Suc_eq_insert_0)
lemmas test_MultiInter = test_MultiSync[where S = ‹{}›]
and test_MultiPar = test_MultiSync[where S = ‹UNIV›]
and MultiInter_set1 = MultiSync_set1[where S = ‹{}›]
and MultiPar_set1 = MultiSync_set1[where S = ‹UNIV›]
and MultiInter_set2 = MultiSync_set2[where S = ‹{}›]
and MultiPar_set2 = MultiSync_set2[where S = ‹UNIV›]
and MultiInter_set3 = MultiSync_set3[where S = ‹{}›]
and MultiPar_set3 = MultiSync_set3[where S = ‹UNIV›]
and test_MultiInter' = test_MultiSync'[where S = ‹{}›]
and test_MultiPar' = test_MultiSync'[where S = ‹UNIV›]
and test_MultiInter'' = test_MultiSync''[where S = ‹{}›]
and test_MultiPar'' = test_MultiSync''[where S = ‹UNIV›]
section ‹Continuity›
lemma MultiSync_cont[simp]:
‹∀x ∈# M. cont (P x) ⟹ cont (λy. ❙⟦S❙⟧ z ∈# M. P z y)›
by (cases ‹M = {#}›, simp, erule mset_induct_nonempty, simp+)
lemmas MultiInter_cont[simp] = MultiSync_cont[where S = ‹{}›]
and MultiPar_cont[simp] = MultiSync_cont[where S = ‹UNIV›]
section ‹Factorization of \<^const>‹Sync› in front of \<^const>‹MultiSync››
lemma MultiSync_factorization_union:
‹⟦M ≠ {#}; N ≠ {#}⟧ ⟹
(❙⟦S❙⟧ z ∈# M. P z) ⟦S⟧ (❙⟦S❙⟧ z ∈# N. P z) = ❙⟦S❙⟧ z∈# M + N. P z›
by (erule mset_induct_nonempty, simp_all add: Sync_assoc)
lemmas MultiInter_factorization_union =
MultiSync_factorization_union[where S = ‹{}›]
and MultiPar_factorization_union =
MultiSync_factorization_union[where S = ‹UNIV›]
section ‹\<^term>‹⊥› Absorbance›
lemma MultiSync_BOT_absorb:
‹m ∈# M ⟹ P m = ⊥ ⟹ (❙⟦S❙⟧ z ∈# M. P z) = ⊥›
by (metis MultiSync_add MultiSync_rec1 mset_add Sync_BOT Sync_commute)
lemmas MultiInter_BOT_absorb = MultiSync_BOT_absorb[where S = ‹{}› ]
and MultiPar_BOT_absorb = MultiSync_BOT_absorb[where S = ‹UNIV›]
lemma MultiSync_is_BOT_iff:
‹(❙⟦S❙⟧ m ∈# M. P m) = ⊥ ⟷ (∃m ∈# M. P m = ⊥)›
apply (cases ‹M = {#}›, simp add: BOT_iff_D D_STOP)
by (rotate_tac, induct M rule: mset_induct_nonempty)
(auto simp add: Sync_is_BOT_iff)
lemmas MultiInter_is_BOT_iff = MultiSync_is_BOT_iff[where S = ‹{}› ]
and MultiPar_is_BOT_iff = MultiSync_is_BOT_iff[where S = ‹UNIV›]
section ‹Other Properties›
lemma MultiSync_SKIP_id: ‹M ≠ {#} ⟹ (❙⟦S❙⟧ z ∈# M. SKIP) = SKIP›
by (rule mset_induct_nonempty, simp_all add: Sync_SKIP_SKIP)
lemmas MultiInter_SKIP_id = MultiSync_SKIP_id[where S = ‹{}›]
and MultiPar_SKIP_id = MultiSync_SKIP_id[where S = ‹UNIV›]
lemma MultiPar_prefix_two_distincts_STOP:
assumes ‹m ∈# M› and ‹m' ∈# M› and ‹fst m ≠ fst m'›
shows ‹(❙|❙| a ∈# M. (fst a → P (snd a))) = STOP›
proof -
obtain M' where f2: ‹M = add_mset m (add_mset m' M')›
by (metis diff_union_swap insert_DiffM assms)
show ‹(❙|❙| x ∈# M. (fst x → P (snd x))) = STOP›
apply (cases ‹M' = {#}›,
simp_all add: f2 prefix_Par1[rotated, rotated, OF assms(3)])
apply (induct M' rule: mset_induct_nonempty, simp)
apply (metis (no_types, opaque_lifting) Sync_BOT Par_STOP prefix_Par2
prefix_Par1 assms(3))
by (metis (no_types, lifting) MultiPar_add add_mset_commute empty_not_add_mset
Par_BOT Par_STOP prefix_Par_SKIP Par_commute)
qed
lemma MultiPar_prefix_two_distincts_STOP':
‹⟦(m, n) ∈# M; (m', n') ∈# M; m ≠ m'⟧ ⟹
(❙|❙| (m, n) ∈# M. (m → P n)) = STOP›
apply (subst cond_case_prod_eta[where g = ‹λ x. (fst x → P (snd x))›])
by (simp_all add: MultiPar_prefix_two_distincts_STOP)
section ‹Behaviour of \<^const>‹MultiSync› with \<^const>‹Sync››
lemma Sync_STOP_STOP: ‹STOP ⟦S⟧ STOP = STOP›
by (fact Mprefix_Sync_distr_subset[of ‹{}› S ‹{}›, simplified,
simplified Mprefix_STOP])
lemma MultiSync_Sync:
‹(❙⟦S❙⟧ z ∈# M. P z) ⟦S⟧ (❙⟦S❙⟧ z ∈# M. P' z) = ❙⟦S❙⟧ z ∈# M. P z ⟦S⟧ P' z›
apply (cases ‹M = {#}›, simp add: Sync_STOP_STOP)
apply (induct M rule: mset_induct_nonempty)
by simp_all (metis (no_types, lifting) Sync_assoc Sync_commute)
lemmas MultiInter_Inter = MultiSync_Sync[where S = ‹{}›]
and MultiPar_Par = MultiSync_Sync[where S = ‹UNIV›]
section ‹Commutativity›
lemma MultiSync_sets_commute:
‹(❙⟦S❙⟧ a ∈# M. ❙⟦S❙⟧ b ∈# N. P a b) = ❙⟦S❙⟧ b ∈# N. ❙⟦S❙⟧ a ∈# M. P a b›
apply (cases ‹N = {#}›, induct M, simp_all,
metis MultiSync_add MultiSync_rec1 Sync_STOP_STOP)
apply (induct N rule: mset_induct_nonempty, fastforce)
by simp (metis MultiSync_Sync)
lemmas MultiInter_sets_commute = MultiSync_sets_commute[where S = ‹{}›]
and MultiPar_sets_commute = MultiSync_sets_commute[where S = ‹UNIV›]
section ‹Behaviour with Injectivity›
lemma inj_on_mapping_over_MultiSync:
‹inj_on f (set_mset M) ⟹
(❙⟦S❙⟧ x ∈# M. P x) = ❙⟦S❙⟧ x ∈# image_mset f M. P (inv_into (set_mset M) f x)›
proof (induct M rule: induct_subset_mset_empty_single)
case (3 N a)
hence f1: ‹inv_into (insert a (set_mset N)) f (f a) = a› by force
show ?case
apply (simp add: "3.hyps"(2) "3.hyps"(3) f1,
rule arg_cong[where f = ‹λx. P a ⟦S⟧ x›])
apply (subst "3.hyps"(4), rule inj_on_subset[OF "3.prems"],
simp add: subset_insertI)
apply (rule mono_MultiSync_eq)
using "3.prems" by fastforce
qed auto
lemmas inj_on_mapping_over_MultiInter =
inj_on_mapping_over_MultiSync[where S = ‹{}›]
and inj_on_mapping_over_MultiPar =
inj_on_mapping_over_MultiSync[where S = ‹UNIV›]
end