Theory CSP_PTick_Renaming
chapter ‹Some Work on Renaming›
theory CSP_PTick_Renaming
imports "HOL-CSPM" Synchronization_Product_Generalized
begin
unbundle option_type_syntax
text ‹
This chapter contains several developments related to the \<^const>‹Renaming› operator.
Some are not directly related to this session and may be moved
to \<^session>‹HOL-CSP› or \<^session>‹HOL-CSPM› in the future,
while others specifically concern the operator \<^const>‹Sync⇩p⇩t⇩i⇩c⇩k_locale.Sync⇩p⇩t⇩i⇩c⇩k›.
›
section ‹Tick Swap Operator›
text ‹We want to define an operator for swapping the values inside termination.
Intuitively, we want \<^term>‹TickSwap (SKIP (r, s)) = SKIP (s, r)›.›
subsection ‹Preliminaries›
subsubsection ‹Swapping an Event›
text ‹We start by defining \<^term>‹tick_swap›, which is swapping the values inside termination
but only for an event. Then this will be generalized to a trace, a refusal and a failure.›
fun tick_swap :: ‹('a, 'r × 's) event⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 's × 'r) event⇩p⇩t⇩i⇩c⇩k›
where ‹tick_swap (ev a) = ev a›
| ‹tick_swap ✓((r, s)) = ✓((s, r))›
lemma tick_swap_tick : ‹tick_swap ✓(r_s) = (case r_s of (r, s) ⇒ ✓((s, r)))›
by (cases r_s) simp
lemma tick_swap_tick_swap [simp] : ‹tick_swap (tick_swap e) = e›
proof (cases e)
show ‹e = ev a ⟹ tick_swap (tick_swap e) = e› for a by simp
next
show ‹e = ✓(r_s) ⟹ tick_swap (tick_swap e) = e› for r_s
by (cases r_s) simp_all
qed
lemma tick_swap_comp_tick_swap [simp] : ‹tick_swap ∘ tick_swap = id›
by (rule ext) simp
lemma inj_tick_swap [simp] : ‹inj tick_swap›
by (metis injI tick_swap_tick_swap)
lemma surj_tick_swap [simp] : ‹surj tick_swap›
by (metis surjI tick_swap_tick_swap)
lemma bij_tick_swap [simp] : ‹bij tick_swap›
by (simp add: bij_betw_def)
lemma bij_betw_tick_swap :
‹bij_betw tick_swap (range ev ) (range ev )›
‹bij_betw tick_swap (range tick) (range tick)›
by (auto simp add: bij_betw_def inj_on_def set_eq_iff image_iff)
lemma ev_eq_tick_swap_iff [simp] : ‹ev a = tick_swap e ⟷ e = ev a›
and tick_swap_eq_ev_iff [simp] : ‹tick_swap e = ev a ⟷ e = ev a›
and tick_eq_tick_swap_iff [simp] : ‹✓((r, s)) = tick_swap e ⟷ e = ✓((s, r))›
and tick_swap_eq_tick_iff [simp] : ‹tick_swap e = ✓((r, s)) ⟷ e = ✓((s, r))›
by (cases e, auto)+
subsubsection ‹Swapping a Trace›
fun trace_tick_swap :: ‹('a, ('r × 's)) trace⇩p⇩t⇩i⇩c⇩k ⇒ ('a, ('s × 'r)) trace⇩p⇩t⇩i⇩c⇩k›
where ‹trace_tick_swap [] = []›
| ‹trace_tick_swap (ev a # t) = ev a # trace_tick_swap t›
| ‹trace_tick_swap (✓((r, s)) # t) = ✓((s, r)) # trace_tick_swap t›
lemma trace_tick_swap_tick_Cons :
‹trace_tick_swap (✓(r_s) # t) = (case r_s of (r, s) ⇒ ✓((s, r)) # trace_tick_swap t)›
by (cases r_s) simp
lemma trace_tick_swap_def : ‹trace_tick_swap = map tick_swap›
proof (rule ext)
show ‹trace_tick_swap t = map tick_swap t› for t :: ‹('a, ('r × 's)) trace⇩p⇩t⇩i⇩c⇩k›
by (induct t rule: trace_tick_swap.induct) simp_all
qed
lemma trace_tick_swap_append : ‹trace_tick_swap (t @ u) = trace_tick_swap t @ trace_tick_swap u›
by (simp add: trace_tick_swap_def)
lemma trace_tick_swap_singl [simp] : ‹trace_tick_swap [e] = [tick_swap e]›
by (cases e) auto
lemma trace_tick_swap_comp_trace_tick_swap [simp] : ‹trace_tick_swap ∘ trace_tick_swap = id›
by (simp add: trace_tick_swap_def)
lemma trace_tick_swap_trace_tick_swap [simp] : ‹trace_tick_swap (trace_tick_swap t) = t›
by (metis comp_def id_apply trace_tick_swap_comp_trace_tick_swap)
lemma inj_trace_tick_swap [simp] : ‹inj trace_tick_swap›
by (metis injI trace_tick_swap_trace_tick_swap)
lemma surj_trace_tick_swap [simp] : ‹surj trace_tick_swap›
by (metis surjI trace_tick_swap_trace_tick_swap)
lemma bij_trace_tick_swap [simp] : ‹bij trace_tick_swap›
by (simp add: bij_betw_def)
lemma strict_mono_trace_tick_swap : ‹strict_mono trace_tick_swap›
by (unfold trace_tick_swap_def)
(rule strict_mono_map, simp add: strict_monoI)
lemma image_trace_tick_swap_min_elems :
‹trace_tick_swap ` (min_elems T) = min_elems (trace_tick_swap ` T)›
proof (intro subset_antisym subsetI)
show ‹t ∈ trace_tick_swap ` min_elems T ⟹ t ∈ min_elems (trace_tick_swap ` T)› for t
by (auto simp add: min_elems_def less_list_def less_eq_list_def prefix_def)
(metis Prefix_Order.prefixI Prefix_Order.same_prefix_nil
trace_tick_swap_append trace_tick_swap_trace_tick_swap)
next
show ‹t ∈ min_elems (trace_tick_swap ` T) ⟹ t ∈ trace_tick_swap ` min_elems T› for t
by (auto simp add: min_elems_def less_list_def less_eq_list_def prefix_def image_iff)
(metis trace_tick_swap_append trace_tick_swap_trace_tick_swap)
qed
lemma Nil_eq_trace_tick_swap_iff [iff] : ‹[] = trace_tick_swap t ⟷ t = []›
and trace_tick_swap_eq_Nil_iff [iff] : ‹trace_tick_swap t = [] ⟷ t = []›
by (metis trace_tick_swap.simps(1) trace_tick_swap_trace_tick_swap)+
lemma ev_Cons_eq_trace_tick_swap_iff [iff] :
‹ev a # t = trace_tick_swap u ⟷ u = ev a # trace_tick_swap t›
and trace_tick_swap_eq_ev_Cons_iff [iff] :
‹trace_tick_swap u = ev a # t ⟷ u = ev a # trace_tick_swap t›
by (metis trace_tick_swap.simps(2) trace_tick_swap_trace_tick_swap)+
lemma tick_Cons_eq_trace_tick_swap_iff [iff] :
‹✓((r, s)) # t = trace_tick_swap u ⟷ u = ✓((s, r)) # trace_tick_swap t›
and trace_tick_swap_eq_tick_Cons_iff [iff] :
‹trace_tick_swap u = ✓((r, s)) # t ⟷ u = ✓((s, r)) # trace_tick_swap t›
by (metis trace_tick_swap.simps(3) trace_tick_swap_trace_tick_swap)+
lemma snoc_ev_eq_trace_tick_swap_iff [iff] :
‹t @ [ev a] = trace_tick_swap u ⟷ u = trace_tick_swap t @ [ev a]›
and trace_tick_swap_eq_snoc_ev_iff [iff] :
‹trace_tick_swap u = t @ [ev a] ⟷ u = trace_tick_swap t @ [ev a]›
by (metis trace_tick_swap_append trace_tick_swap.simps(1, 2) trace_tick_swap_trace_tick_swap)+
lemma snoc_tick_eq_trace_tick_swap_iff [iff] :
‹t @ [✓((r, s))] = trace_tick_swap u ⟷ u = trace_tick_swap t @ [✓((s, r))]›
and trace_tick_swap_eq_snoc_tick_iff [iff] :
‹trace_tick_swap u = t @ [✓((r, s))] ⟷ u = trace_tick_swap t @ [✓((s, r))]›
by (metis trace_tick_swap_append trace_tick_swap.simps(1, 3) trace_tick_swap_trace_tick_swap)+
lemma trace_tick_swap_eq_ev_ConsE :
‹trace_tick_swap u = ev a # t ⟹ (⋀u'. u = ev a # u' ⟹ t = trace_tick_swap u' ⟹ thesis) ⟹ thesis›
and trace_tick_swap_eq_tick_ConsE :
‹trace_tick_swap u = ✓((r, s)) # t ⟹ (⋀u'. u = ✓((s, r)) # u' ⟹ t = trace_tick_swap u' ⟹ thesis) ⟹ thesis›
and trace_tick_swap_eq_snoc_evE :
‹trace_tick_swap u = t @ [ev a] ⟹ (⋀u'. u = u' @ [ev a] ⟹ t = trace_tick_swap u' ⟹ thesis) ⟹ thesis›
and trace_tick_swap_eq_snoc_tickE :
‹trace_tick_swap u = t @ [✓((r, s))] ⟹ (⋀u'. u = u' @ [✓((s, r))] ⟹ t = trace_tick_swap u' ⟹ thesis) ⟹ thesis›
by (simp, metis trace_tick_swap_trace_tick_swap)+
lemma trace_tick_swap_tickFree :
‹tF t ⟹ trace_tick_swap t = map (ev ∘ of_ev) t› for t :: ‹('a, ('r × 's)) trace⇩p⇩t⇩i⇩c⇩k›
proof (induct t)
show ‹trace_tick_swap [] = map (ev ∘ of_ev) []› by simp
next
fix e and t :: ‹('a, ('r × 's)) trace⇩p⇩t⇩i⇩c⇩k›
assume ‹tF (e # t)› and ‹tF t ⟹ trace_tick_swap t = map (ev ∘ of_ev) t›
moreover from ‹tF (e # t)› obtain a where ‹e = ev a› ‹tF t›
by (meson is_ev_def tickFree_Cons_iff)
ultimately show ‹trace_tick_swap (e # t) = map (ev ∘ of_ev) (e # t)› by simp
qed
lemma trace_tick_swap_front_tickFree :
‹trace_tick_swap t = ( if tF t then map (ev ∘ of_ev) t
else map (ev ∘ of_ev) (butlast t) @ [case last t of ✓((r, s)) ⇒ ✓((s, r))])›
if ‹ftF t› for t :: ‹('a, ('r × 's)) trace⇩p⇩t⇩i⇩c⇩k›
proof -
show ?thesis
proof (split if_split, intro conjI impI)
show ‹tF t ⟹ trace_tick_swap t = map (ev ∘ of_ev) t›
by (simp add: trace_tick_swap_tickFree)
next
assume ‹¬ tF t›
with ‹ftF t› obtain t' r s where ‹t = t' @ [✓((r, s))]› ‹tF t'›
by (metis front_tickFree_append_iff nonTickFree_n_frontTickFree not_Cons_self2 surj_pair)
hence ‹trace_tick_swap t = trace_tick_swap t' @ [✓((s, r))]›
by (metis trace_tick_swap_append trace_tick_swap.simps(1, 3))
also from ‹tF t'› ‹t = t' @ [✓((r, s))]›
have ‹trace_tick_swap t' = map (ev ∘ of_ev) (butlast t)› by (simp add: trace_tick_swap_tickFree)
also from ‹t = t' @ [✓((r, s))]›
have ‹[✓((s, r))] = [case last t of ✓((r, s)) ⇒ ✓((s, r))]› by simp
finally show ‹trace_tick_swap t = map (ev ∘ of_ev) (butlast t) @
[case last t of ✓((r, s)) ⇒ ✓((s, r))]› .
qed
qed
lemma tickFree_trace_tick_swap_iff [simp] : ‹tF (trace_tick_swap t) ⟷ tF t›
by (metis tickFree_map_ev_comp trace_tick_swap_tickFree trace_tick_swap_trace_tick_swap)
lemma front_tickFree_trace_tick_swap_iff [simp] : ‹ftF (trace_tick_swap t) ⟷ ftF t›
by (metis (no_types, lifting) front_tickFree_iff_tickFree_butlast map_butlast
tickFree_trace_tick_swap_iff trace_tick_swap_def)
subsubsection ‹Swapping a Refusal›
definition refusal_tick_swap :: ‹('a, ('r × 's)) refusal⇩p⇩t⇩i⇩c⇩k ⇒ ('a, ('s × 'r)) refusal⇩p⇩t⇩i⇩c⇩k›
where ‹refusal_tick_swap X = tick_swap ` X›
lemma refusal_tick_swap_empty [simp] : ‹refusal_tick_swap {} = {}›
by (simp add: refusal_tick_swap_def)
lemma refusal_tick_swap_insert [simp] :
‹refusal_tick_swap (insert x X) = insert (tick_swap x) (refusal_tick_swap X)›
by (simp add: refusal_tick_swap_def)
lemma refusal_tick_swap_union :
‹refusal_tick_swap (X ∪ Y) = refusal_tick_swap X ∪ refusal_tick_swap Y›
by (simp add: refusal_tick_swap_def image_Un)
lemma refusal_tick_swap_diff :
‹refusal_tick_swap (X - Y) = refusal_tick_swap X - refusal_tick_swap Y›
by (simp add: refusal_tick_swap_def image_set_diff)
lemma refusal_tick_swap_inter :
‹refusal_tick_swap (X ∩ Y) = refusal_tick_swap X ∩ refusal_tick_swap Y›
by (simp add: refusal_tick_swap_def image_Int)
lemma refusal_tick_swap_singl : ‹refusal_tick_swap {e} = {tick_swap e}› by simp
lemma refusal_tick_swap_comp_refusal_tick_swap [simp] :
‹refusal_tick_swap ∘ refusal_tick_swap = id›
by (auto simp add: refusal_tick_swap_def image_iff)
lemma refusal_tick_swap_refusal_tick_swap [simp] :
‹refusal_tick_swap (refusal_tick_swap X) = X›
by (simp add: comp_eq_dest_lhs)
lemma inj_refusal_tick_swap [simp] : ‹inj refusal_tick_swap›
by (metis injI refusal_tick_swap_refusal_tick_swap)
lemma surj_refusal_tick_swap [simp] : ‹surj refusal_tick_swap›
by (metis surjI refusal_tick_swap_refusal_tick_swap)
lemma bij_refusal_tick_swap [simp] : ‹bij refusal_tick_swap›
by (simp add: bij_betw_def)
lemma strict_mono_refusal_tick_swap : ‹strict_mono refusal_tick_swap›
by (rule strict_monoI)
(metis refusal_tick_swap_refusal_tick_swap sup.strict_order_iff refusal_tick_swap_union)
lemma empty_eq_refusal_tick_swap_iff [iff] : ‹{} = refusal_tick_swap X ⟷ X = {}›
and refusal_tick_swap_eq_empty_iff [iff] : ‹refusal_tick_swap X = {} ⟷ X = {}›
by (simp_all add: refusal_tick_swap_def)
lemma insert_ev_eq_refusal_tick_swap_iff [iff] :
‹insert (ev a) X = refusal_tick_swap Y ⟷ Y = insert (ev a) (refusal_tick_swap X)›
and refusal_tick_swap_eq_insert_ev_iff [iff] :
‹refusal_tick_swap Y =insert (ev a) X ⟷ Y = insert (ev a) (refusal_tick_swap X)›
by (metis refusal_tick_swap_insert refusal_tick_swap_refusal_tick_swap tick_swap.simps(1))+
lemma insert_tick_eq_refusal_tick_swap_iff [iff] :
‹insert ✓((r, s)) X = refusal_tick_swap Y ⟷ Y = insert ✓((s, r)) (refusal_tick_swap X)›
and refusal_tick_swap_eq_insert_tick_iff [iff] :
‹refusal_tick_swap Y = insert ✓((r, s)) X ⟷ Y = insert ✓((s, r)) (refusal_tick_swap X)›
by (metis refusal_tick_swap_insert refusal_tick_swap_refusal_tick_swap tick_swap.simps(2))+
lemma refusal_tick_swap_eq_insert_evE :
‹refusal_tick_swap Y = insert (ev a) X ⟹ (⋀Y'. Y = insert (ev a) Y' ⟹ X = refusal_tick_swap Y' ⟹ thesis) ⟹ thesis›
and refusal_tick_swap_eq_insert_tickE :
‹refusal_tick_swap Y = insert ✓((r, s)) X ⟹ (⋀Y'. Y = insert ✓((s, r)) Y' ⟹ X = refusal_tick_swap Y' ⟹ thesis) ⟹ thesis›
by (simp, metis refusal_tick_swap_refusal_tick_swap)+
lemma refusal_tick_swap_tickFree :
‹X ⊆ range ev ⟹ refusal_tick_swap X = (ev ∘ of_ev) ` X›
by (force simp add: refusal_tick_swap_def)
lemma tickFree_refusal_tick_swap_iff :
‹refusal_tick_swap X ⊆ range ev ⟷ X ⊆ range ev›
by (simp add: refusal_tick_swap_def subset_iff image_def)
(metis tick_swap.simps(1) tick_swap_tick_swap)
text ‹The old version of interleaving of traces is not affected.›
lemma setinterleaves_imp_setinterleaves_trace_tick_swap :
‹t setinterleaves ((u, v), S) ⟹
trace_tick_swap t setinterleaves ((trace_tick_swap u, trace_tick_swap v), refusal_tick_swap S)›
proof (induct ‹(u, S, v)› arbitrary: t u v rule: setinterleaving.induct)
case 1 thus ?case by simp
next
case (2 y v)
from "2.prems" obtain t' where ‹y ∉ S› ‹t = y # t'› ‹t' setinterleaves (([], v), S)›
by (auto split: if_split_asm)
from "2.hyps"[OF ‹y ∉ S› ‹t' setinterleaves (([], v), S)›]
have ‹trace_tick_swap t' setinterleaves (([], trace_tick_swap v), refusal_tick_swap S)› by simp
with ‹y ∉ S› show ?case by (cases y) (auto simp add: ‹t = y # t'› refusal_tick_swap_def split: prod.split)
next
case (3 x u)
from "3.prems" obtain t' where ‹x ∉ S› ‹t = x # t'› ‹t' setinterleaves ((u, []), S)›
by (auto split: if_split_asm)
from "3.hyps"[OF ‹x ∉ S› ‹t' setinterleaves ((u, []), S)›]
have ‹trace_tick_swap t' setinterleaves ((trace_tick_swap u, []), refusal_tick_swap S)› by simp
with ‹x ∉ S› show ?case by (cases x) (auto simp add: ‹t = x # t'› refusal_tick_swap_def split: prod.split)
next
case (4 x u y v)
from "4.prems"
consider (both_in) t' where ‹x ∈ S› ‹y ∈ S› ‹x = y› ‹t = x # t'› ‹t' setinterleaves ((u, v), S)›
| (inR_mvL) t' where ‹x ∉ S› ‹y ∈ S› ‹t = x # t'› ‹t' setinterleaves ((u, y # v), S)›
| (inL_mvR) t' where ‹x ∈ S› ‹y ∉ S› ‹t = y # t'› ‹t' setinterleaves ((x # u, v), S)›
| (notin_mvL) t' where ‹x ∉ S› ‹y ∉ S› ‹t = x # t'› ‹t' setinterleaves ((u, y # v), S)›
| (notin_mvR) t' where ‹x ∉ S› ‹y ∉ S› ‹t = y # t'› ‹t' setinterleaves ((x # u, v), S)›
by (auto split: if_split_asm)
thus ?case
proof cases
case both_in
from "4.hyps"(1)[OF both_in(1-3, 5)] both_in(1-3)
show ?thesis by (cases y, auto simp add: both_in(4) refusal_tick_swap_def split: prod.split)
next
case inR_mvL
have ‹¬ y ∉ S› by (simp add: inR_mvL(2))
from "4.hyps"(5)[OF inR_mvL(1) ‹¬ y ∉ S› inR_mvL(4)] inR_mvL(1, 2)
show ?thesis by (cases x, auto simp add: inR_mvL(3) refusal_tick_swap_def SyncSingleHeadAdd image_iff split: prod.split)
next
case inL_mvR
have * : ‹a setinterleaves ((t, u), tick_swap ` S) ⟹ h ∉ tick_swap ` S ⟹
(h # a) setinterleaves ((t, h # u), tick_swap ` S)› for a t h u
by (cases t, auto split: if_split_asm)
from "4.hyps"(2)[OF inL_mvR(1, 2, 4)] inL_mvR(1, 2)
show ?thesis by (cases y, auto simp add: inL_mvR(3) refusal_tick_swap_def image_iff "*" split: prod.split)
next
case notin_mvL
from "4.hyps"(3)[OF notin_mvL(1, 2, 4)] notin_mvL(1, 2)
show ?thesis by (cases y, auto simp add: notin_mvL(3) refusal_tick_swap_def split: prod.split)
(simp_all add: inj_image_mem_iff trace_tick_swap_def)
next
case notin_mvR
from "4.hyps"(4)[OF notin_mvR(1, 2, 4)] notin_mvR(1, 2)
show ?thesis by (cases x, auto simp add: notin_mvR(3) refusal_tick_swap_def split: prod.split)
(simp_all add: inj_image_mem_iff trace_tick_swap_def)
qed
qed
lemma trace_tick_swap_setinterleaves_iff :
‹trace_tick_swap t setinterleaves ((u, v), S) ⟷
t setinterleaves ((trace_tick_swap u, trace_tick_swap v), refusal_tick_swap S)›
by (metis refusal_tick_swap_refusal_tick_swap trace_tick_swap_trace_tick_swap
setinterleaves_imp_setinterleaves_trace_tick_swap)
subsubsection ‹Swapping a Failure›
definition failure_tick_swap :: ‹('a, ('r × 's)) failure⇩p⇩t⇩i⇩c⇩k ⇒ ('a, ('s × 'r)) failure⇩p⇩t⇩i⇩c⇩k›
where ‹failure_tick_swap F ≡ case F of (t, X) ⇒ (trace_tick_swap t, refusal_tick_swap X)›
lemma failure_tick_swap_empty [simp] : ‹failure_tick_swap ([], {}) = ([], {})›
by (simp add: failure_tick_swap_def)
lemma failure_tick_swap_comp_failure_tick_swap [simp] :
‹failure_tick_swap ∘ failure_tick_swap = id›
by (auto simp add: failure_tick_swap_def)
lemma failure_tick_swap_failure_tick_swap [simp] :
‹failure_tick_swap (failure_tick_swap F) = F›
by (simp add: comp_eq_dest_lhs)
lemma inj_failure_tick_swap [simp] : ‹inj failure_tick_swap›
by (metis injI failure_tick_swap_failure_tick_swap)
lemma surj_failure_tick_swap [simp] : ‹surj failure_tick_swap›
by (metis surjI failure_tick_swap_failure_tick_swap)
lemma bij_failure_tick_swap [simp] : ‹bij failure_tick_swap›
by (simp add: bij_betw_def)
lemma empty_eq_failure_tick_swap_iff [iff] : ‹([], {}) = failure_tick_swap F ⟷ F = ([], {})›
and failure_tick_swap_eq_empty_iff [iff] : ‹failure_tick_swap F = ([], {}) ⟷ F = ([], {})›
by (auto simp add: failure_tick_swap_def split: prod.split)
subsection ‹The Operator›
subsubsection ‹Definition›
lift_definition TickSwap :: ‹('a, 'r × 's) process⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 's × 'r) process⇩p⇩t⇩i⇩c⇩k›
is ‹λP. ({(t, X). failure_tick_swap (t, X) ∈ ℱ P}, {t. trace_tick_swap t ∈ 𝒟 P})›
proof -
show ‹?thesis P› (is ‹is_process (?f, ?d)›) for P
proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv,
intro conjI impI allI)
show ‹([], {}) ∈ ?f› by (simp add: is_processT1)
next
show ‹(t, X) ∈ ?f ⟹ ftF t› for t X
by (simp add: failure_tick_swap_def)
(use is_processT2 front_tickFree_trace_tick_swap_iff in blast)
next
show ‹(t @ u, {}) ∈ ?f ⟹ (t, {}) ∈ ?f› for t u
by (simp add: failure_tick_swap_def) (metis trace_tick_swap_append is_processT3)
next
show ‹(t, Y) ∈ ?f ∧ X ⊆ Y ⟹ (t, X) ∈ ?f› for t X Y
by (simp add: failure_tick_swap_def)
(metis is_processT4 le_iff_sup refusal_tick_swap_union)
next
fix t X Y assume ‹(t, X) ∈ ?f ∧ (∀e. e ∈ Y ⟶ (t @ [e], {}) ∉ ?f)›
hence ‹(trace_tick_swap t, refusal_tick_swap X) ∈ ℱ P ∧
(∀e. e ∈ refusal_tick_swap Y ⟶ (trace_tick_swap t @ [e], {}) ∉ ℱ P)›
by (auto simp add: failure_tick_swap_def refusal_tick_swap_def trace_tick_swap_append)
thus ‹(t, X ∪ Y) ∈ ?f›
by (simp add: failure_tick_swap_def is_processT5 refusal_tick_swap_union)
next
show ‹(t @ [✓(s_r)], {}) ∈ ?f ⟹ (t, X - {✓(s_r)}) ∈ ?f› for t X s_r
by (cases s_r) (simp add: failure_tick_swap_def trace_tick_swap_append
is_processT6 refusal_tick_swap_diff)
next
show ‹t ∈ ?d ∧ tF t ∧ ftF u ⟹ t @ u ∈ ?d› for t u
by (simp add: trace_tick_swap_append is_processT7)
next
show ‹t ∈ ?d ⟹ (t, X) ∈ ?f› for t X
by (simp add: failure_tick_swap_def is_processT8)
next
show ‹t @ [✓(s_r)] ∈ ?d ⟹ t ∈ ?d› for t s_r
by (cases s_r) (auto simp add: trace_tick_swap_append intro: is_processT9)
qed
qed
subsubsection ‹Projections›
lemma F_TickSwap' : ‹ℱ (TickSwap P) = {(t, X). failure_tick_swap (t, X) ∈ ℱ P}›
by (simp add: Failures.rep_eq TickSwap.rep_eq FAILURES_def)
lemma D_TickSwap' : ‹𝒟 (TickSwap P) = {t. trace_tick_swap t ∈ 𝒟 P}›
by (simp add: Divergences.rep_eq TickSwap.rep_eq DIVERGENCES_def)
lemma T_TickSwap' : ‹𝒯 (TickSwap P) = {t. trace_tick_swap t ∈ 𝒯 P}›
by (simp add: set_eq_iff F_TickSwap' failure_tick_swap_def flip: T_F_spec)
lemmas TickSwap_projs' = F_TickSwap' D_TickSwap' T_TickSwap'
text ‹This is not very intuitive. The following lemmas are more intuitive.›
lemma F_TickSwap : ‹ℱ (TickSwap P) = failure_tick_swap ` ℱ P›
by (simp add: set_eq_iff F_TickSwap')
(metis (no_types, lifting) failure_tick_swap_failure_tick_swap imageE image_eqI)
lemma D_TickSwap : ‹𝒟 (TickSwap P) = trace_tick_swap ` 𝒟 P›
by (simp add: set_eq_iff D_TickSwap')
(metis (no_types, lifting) trace_tick_swap_trace_tick_swap imageE image_eqI)
lemma T_TickSwap : ‹𝒯 (TickSwap P) = trace_tick_swap ` 𝒯 P›
by (simp add: set_eq_iff T_TickSwap')
(metis (no_types, lifting) trace_tick_swap_trace_tick_swap imageE image_eqI)
lemmas TickSwap_projs = F_TickSwap D_TickSwap T_TickSwap
text ‹We finally give the following versions, sometimes more convenient to use.›
lemma F_TickSwap'' : ‹ℱ (TickSwap P) = {(trace_tick_swap t, refusal_tick_swap X)| t X. (t, X) ∈ ℱ P}›
by (auto simp add: F_TickSwap failure_tick_swap_def)
lemma D_TickSwap'' : ‹𝒟 (TickSwap P) = {trace_tick_swap t| t. t ∈ 𝒟 P}›
by (auto simp add: D_TickSwap)
lemma T_TickSwap'' : ‹𝒯 (TickSwap P) = {trace_tick_swap t| t. t ∈ 𝒯 P}›
by (auto simp add: T_TickSwap)
lemmas TickSwap_projs'' = F_TickSwap'' D_TickSwap'' T_TickSwap''
subsubsection ‹Properties›
lemma events_TickSwap [simp] : ‹events_of (TickSwap P) = events_of P›
by (auto simp add: events_of_def T_TickSwap trace_tick_swap_def)
lemma ticks_TickSwap [simp] : ‹ticks_of (TickSwap P) = {(s, r). (r, s) ∈ ticks_of P}›
by (auto simp add: ticks_of_def T_TickSwap' trace_tick_swap_append)
(metis trace_tick_swap_trace_tick_swap)
lemma strict_ticks_TickSwap [simp] :
‹strict_ticks_of (TickSwap P) = {(s, r). (r, s) ∈ strict_ticks_of P}›
by (auto simp add: strict_ticks_of_def TickSwap_projs' trace_tick_swap_append)
(metis trace_tick_swap_trace_tick_swap)
lemma trace_tick_swap_image_setinterleaving⇩P⇩a⇩i⇩r :
‹trace_tick_swap ` setinterleaving⇩p⇩t⇩i⇩c⇩k (λr s. ⌊(r, s)⌋, u, A, v) =
setinterleaving⇩p⇩t⇩i⇩c⇩k (λr s. ⌊(r, s)⌋, v, A, u)›
for u :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and v :: ‹('a, 's) trace⇩p⇩t⇩i⇩c⇩k›
by (rule sym, induct ‹(λr :: 'r. λs :: 's. ⌊(r, s)⌋, u, A, v)›
arbitrary: u v) (simp_all, safe, auto)
lemma trace_tick_swap_setinterleaves⇩P⇩a⇩i⇩r_iff [iff] :
‹trace_tick_swap t setinterleaves⇩✓⇘λr s. ⌊(r, s)⌋⇙ ((u, v), A) ⟷
t setinterleaves⇩✓⇘λr s. ⌊(r, s)⌋⇙ ((v, u), A)›
by (metis (mono_tags, lifting) image_eqI trace_tick_swap_image_setinterleaving⇩P⇩a⇩i⇩r
trace_tick_swap_trace_tick_swap)
text ‹The following theorem is a bridge with the existing operators:
\<^const>‹TickSwap› can be expressed via the \<^const>‹Renaming› operator.›
lemma tick_swap_is_map_event⇩p⇩t⇩i⇩c⇩k : ‹tick_swap = map_event⇩p⇩t⇩i⇩c⇩k id prod.swap›
proof (rule ext)
show ‹tick_swap e = map_event⇩p⇩t⇩i⇩c⇩k id prod.swap e› for e :: ‹('a, 'r × 's) event⇩p⇩t⇩i⇩c⇩k›
by (cases e) (auto split: event⇩p⇩t⇩i⇩c⇩k.splits prod.splits)
qed
lemma trace_tick_swap_is_map_map_event⇩p⇩t⇩i⇩c⇩k :
‹trace_tick_swap = map (map_event⇩p⇩t⇩i⇩c⇩k id prod.swap)›
by (simp add: tick_swap_is_map_event⇩p⇩t⇩i⇩c⇩k trace_tick_swap_def)
lemma refusal_tick_swap_is_image_map_event⇩p⇩t⇩i⇩c⇩k :
‹refusal_tick_swap = (`) (map_event⇩p⇩t⇩i⇩c⇩k id prod.swap)›
by (rule ext) (simp add: refusal_tick_swap_def tick_swap_is_map_event⇩p⇩t⇩i⇩c⇩k)
theorem TickSwap_is_Renaming :
‹TickSwap P = Renaming P id prod.swap› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
fix t assume ‹t ∈ 𝒟 ?lhs›
with D_imp_front_tickFree have ‹ftF t› by blast
define t1 where ‹t1 ≡ trace_tick_swap (if tF t then t else butlast t)›
define t2 where ‹t2 ≡ if tF t then [] else [last t]›
have ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k id prod.swap) t1 @ t2›
by (simp add: t1_def t2_def flip: trace_tick_swap_is_map_map_event⇩p⇩t⇩i⇩c⇩k)
(metis append_butlast_last_id tickFree_Nil)
moreover from ‹ftF t› front_tickFree_iff_tickFree_butlast t1_def have ‹tF t1› by auto
moreover have ‹ftF t2› by (simp add: t2_def)
moreover from t1_def D_TickSwap' ‹ftF t› ‹t ∈ 𝒟 ?lhs›
div_butlast_when_non_tickFree_iff have ‹t1 ∈ 𝒟 P› by blast
ultimately show ‹t ∈ 𝒟 ?rhs› unfolding D_Renaming by blast
next
fix t assume ‹t ∈ 𝒟 ?rhs›
then obtain t1 t2
where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k id prod.swap) t1 @ t2› ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 P›
unfolding D_Renaming by blast
thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_TickSwap' trace_tick_swap_append is_processT7
flip: trace_tick_swap_is_map_map_event⇩p⇩t⇩i⇩c⇩k)
next
fix t X assume ‹(t, X) ∈ ℱ ?lhs›
then obtain t' X' where ‹t = trace_tick_swap t'› ‹X = refusal_tick_swap X'› ‹(t', X') ∈ ℱ P›
unfolding F_TickSwap failure_tick_swap_def by auto
moreover have ‹map_event⇩p⇩t⇩i⇩c⇩k id prod.swap -` refusal_tick_swap X' = X'›
by (simp add: set_eq_iff) (metis inj_image_mem_iff inj_tick_swap
refusal_tick_swap_def tick_swap_is_map_event⇩p⇩t⇩i⇩c⇩k)
ultimately show ‹(t, X) ∈ ℱ ?rhs›
by (auto simp add: F_Renaming simp flip: trace_tick_swap_is_map_map_event⇩p⇩t⇩i⇩c⇩k)
next
fix t X assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
assume ‹(t, X) ∈ ℱ ?rhs›
then consider ‹t ∈ 𝒟 ?rhs›
| t' where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k id prod.swap) t'› ‹(t', map_event⇩p⇩t⇩i⇩c⇩k id prod.swap -` X) ∈ ℱ P›
unfolding Renaming_projs by blast
thus ‹(t, X) ∈ ℱ ?lhs›
proof cases
from same_div D_F show ‹t ∈ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ?lhs› by blast
next
fix t' assume * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k id prod.swap) t'›
‹(t', map_event⇩p⇩t⇩i⇩c⇩k id prod.swap -` X) ∈ ℱ P›
from "*"(1) have ‹(t, X) = failure_tick_swap (t', map_event⇩p⇩t⇩i⇩c⇩k id prod.swap -` X)›
by (simp add: failure_tick_swap_def refusal_tick_swap_def trace_tick_swap_def
flip: tick_swap_is_map_event⇩p⇩t⇩i⇩c⇩k)
with "*"(2) show ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_TickSwap)
qed
qed
lemma TickSwap_TickSwap [simp] : ‹TickSwap (TickSwap P) = P›
by (simp add: Process_eq_spec TickSwap_projs')
lemma TickSwap_comp_TickSwap [simp] : ‹TickSwap ∘ TickSwap = id›
by (rule ext) simp
lemma TickSwap_eq_iff_eq_TickSwap : ‹TickSwap P = Q ⟷ P = TickSwap Q› by auto
lemma inj_TickSwap [simp] : ‹inj TickSwap›
by (metis injI TickSwap_TickSwap)
lemma surj_TickSwap [simp] : ‹surj TickSwap›
by (metis surjI TickSwap_TickSwap)
lemma bij_TickSwap [simp] : ‹bij TickSwap›
by (simp add: bij_betw_def)
lemma strict_mono_TickSwap : ‹strict_mono TickSwap›
by (rule strict_monoI)
(metis D_TickSwap F_TickSwap failure_refine_def image_mono injD inj_TickSwap
nless_le failure_divergence_refine_def divergence_refine_def)
subsubsection ‹Monotonicity Properties›
lemma mono_TickSwap : ‹P ⊑ Q ⟹ TickSwap P ⊑ TickSwap Q›
by (simp add: TickSwap_is_Renaming mono_Renaming)
lemma mono_TickSwap_FD : ‹P ⊑⇩F⇩D Q ⟹ TickSwap P ⊑⇩F⇩D TickSwap Q›
and mono_TickSwap_DT : ‹P ⊑⇩D⇩T Q ⟹ TickSwap P ⊑⇩D⇩T TickSwap Q›
and mono_TickSwap_F : ‹P ⊑⇩F Q ⟹ TickSwap P ⊑⇩F TickSwap Q›
and mono_TickSwap_D : ‹P ⊑⇩D Q ⟹ TickSwap P ⊑⇩D TickSwap Q›
and mono_TickSwap_T : ‹P ⊑⇩T Q ⟹ TickSwap P ⊑⇩T TickSwap Q›
by (simp_all add: TickSwap_projs refine_defs image_mono)
lemmas monos_TickSwap = mono_TickSwap mono_TickSwap_FD mono_TickSwap_DT
mono_TickSwap_F mono_TickSwap_D mono_TickSwap_T
lemma le_approx_TickSwap_iff : ‹TickSwap P ⊑ TickSwap Q ⟷ P ⊑ Q›
and FD_TickSwap_iff : ‹TickSwap P ⊑⇩F⇩D TickSwap Q ⟷ P ⊑⇩F⇩D Q›
and DT_TickSwap_iff : ‹TickSwap P ⊑⇩D⇩T TickSwap Q ⟷ P ⊑⇩D⇩T Q›
and F_TickSwap_iff : ‹TickSwap P ⊑⇩F TickSwap Q ⟷ P ⊑⇩F Q›
and D_TickSwap_iff : ‹TickSwap P ⊑⇩D TickSwap Q ⟷ P ⊑⇩D Q›
and T_TickSwap_iff : ‹TickSwap P ⊑⇩T TickSwap Q ⟷ P ⊑⇩T Q›
by (rule iffI; drule monos_TickSwap, simp add: monos_TickSwap)+
lemmas le_TickSwap_iff = le_approx_TickSwap_iff FD_TickSwap_iff DT_TickSwap_iff
F_TickSwap_iff D_TickSwap_iff T_TickSwap_iff
subsubsection ‹Continuity›
text ‹Continuity is a direct corollary of the continuity of \<^const>‹Renaming›.›
lemma TickSwap_cont[simp] : ‹cont P ⟹ cont (λx. TickSwap (P x))›
by (simp add: TickSwap_is_Renaming)
subsubsection ‹Algebraic Laws›
paragraph ‹Constant Processes›
lemma TickSwap_STOP [simp] : ‹TickSwap STOP = STOP›
by (simp add: STOP_iff_T T_TickSwap T_STOP)
lemma TickSwap_is_STOP_iff [simp] : ‹TickSwap P = STOP ⟷ P = STOP›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_BOT [simp] : ‹TickSwap ⊥ = ⊥›
by (simp add: BOT_iff_Nil_D D_TickSwap D_BOT)
lemma TickSwap_is_BOT_iff [simp] : ‹TickSwap P = ⊥ ⟷ P = ⊥›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_SKIP [simp] : ‹TickSwap (SKIP (r, s)) = SKIP (s, r)›
by (simp add: TickSwap_is_Renaming)
lemma TickSwap_is_SKIP_iff [simp] : ‹TickSwap P = SKIP (r, s) ⟷ P = SKIP (s, r)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_SKIPS [simp] : ‹TickSwap (SKIPS R_S) = SKIPS {(s, r). (r, s) ∈ R_S}›
by (auto simp add: Process_eq_spec TickSwap_projs' SKIPS_projs)
(auto simp add: failure_tick_swap_def refusal_tick_swap_def)
lemma TickSwap_is_SKIPS_iff [simp] :
‹TickSwap P = SKIPS R_S ⟷ P = SKIPS {(s, r). (r, s) ∈ R_S}›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
paragraph ‹Binary (or less) Operators›
lemma TickSwap_Ndet [simp] : ‹TickSwap (P ⊓ Q) = TickSwap P ⊓ TickSwap Q›
by (simp add: Process_eq_spec TickSwap_projs Ndet_projs image_Un)
lemma TickSwap_is_Ndet_iff [simp] : ‹TickSwap P = Q ⊓ R ⟷ P = TickSwap Q ⊓ TickSwap R›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Det [simp] :
‹TickSwap (P □ Q) = TickSwap P □ TickSwap Q›
by (simp add: TickSwap_is_Renaming Renaming_Det)
lemma TickSwap_is_Det_iff [simp] : ‹TickSwap P = Q □ R ⟷ P = TickSwap Q □ TickSwap R›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Sliding [simp] : ‹TickSwap (P ⊳ Q) = TickSwap P ⊳ TickSwap Q›
by (simp add: Sliding_def)
lemma TickSwap_is_Sliding_iff [simp] : ‹TickSwap P = Q ⊳ R ⟷ P = TickSwap Q ⊳ TickSwap R›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Sync [simp] :
‹TickSwap (P ⟦S⟧ Q) = TickSwap P ⟦S⟧ TickSwap Q›
by (simp add: TickSwap_is_Renaming bij_Renaming_Sync)
lemma TickSwap_is_Sync_iff [simp] :
‹TickSwap P = Q ⟦S⟧ R ⟷ P = TickSwap Q ⟦S⟧ TickSwap R›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Seq [simp] :
‹TickSwap (P ❙; Q) = TickSwap P ❙; TickSwap Q›
by (simp add: Renaming_Seq TickSwap_is_Renaming)
lemma TickSwap_is_Seq_iff [simp] :
‹TickSwap P = Q ❙; R ⟷ P = TickSwap Q ❙; TickSwap R›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Renaming [simp] :
‹TickSwap (Renaming P f g) =
Renaming (TickSwap P) f (prod.swap ∘ g ∘ prod.swap)›
by (simp add: TickSwap_is_Renaming flip: Renaming_comp)
(metis comp_apply swap_swap)
lemma TickSwap_Renaming' :
‹TickSwap (Renaming P f g) = Renaming P f (prod.swap ∘ g)›
by (simp add: TickSwap_is_Renaming flip: Renaming_comp)
lemma TickSwap_is_Renaming_iff [simp] :
‹TickSwap P = Renaming Q f g ⟷ P = Renaming (TickSwap Q) f (prod.swap ∘ g ∘ prod.swap)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Hiding [simp] : ‹TickSwap (P \ S) = TickSwap P \ S›
by (simp add: TickSwap_is_Renaming bij_Renaming_Hiding)
lemma TickSwap_is_Hiding_iff [simp] : ‹TickSwap P = Q \ S ⟷ P = TickSwap Q \ S›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Interrupt [simp] :
‹TickSwap (P △ Q) = TickSwap P △ TickSwap Q›
by (simp add: TickSwap_is_Renaming Renaming_Interrupt)
lemma TickSwap_is_Interrupt_iff [simp] :
‹TickSwap P = Q △ R ⟷ P = TickSwap Q △ TickSwap R›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Throw [simp] :
‹TickSwap (P Θ a ∈ A. Q a) = TickSwap P Θ a ∈ A. TickSwap (Q a)›
by (simp add: TickSwap_is_Renaming inj_on_Renaming_Throw)
(rule mono_Throw_eq, metis id_apply inj_on_id inv_into_f_f)
lemma TickSwap_is_Throw_iff [simp] :
‹TickSwap P = Q Θ a ∈ A. R a ⟷ P = TickSwap Q Θ a ∈ A. TickSwap (R a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
paragraph ‹Architectural Operators›
lemma TickSwap_GlobalNdet [simp] :
‹TickSwap (⊓a ∈ A. P a) = ⊓a ∈ A. TickSwap (P a)›
by (simp add: TickSwap_is_Renaming Renaming_distrib_GlobalNdet)
lemma TickSwap_is_GlobalNdet_iff [simp] :
‹TickSwap P = ⊓a ∈ A. Q a ⟷ P = ⊓a ∈ A. TickSwap (Q a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_GlobalDet [simp] :
‹TickSwap (□a ∈ A. P a) = □a ∈ A. TickSwap (P a)›
by (simp add: TickSwap_is_Renaming Renaming_distrib_GlobalDet)
lemma TickSwap_is_GlobalDet_iff [simp] :
‹TickSwap P = □a ∈ A. Q a ⟷ P = □a ∈ A. TickSwap (Q a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_MultiSync [simp] :
‹TickSwap (❙⟦S❙⟧ m ∈# M. P m) = ❙⟦S❙⟧ m ∈# M. TickSwap (P m)›
by (induct M rule: induct_subset_mset_empty_single) simp_all
lemma TickSwap_is_TickSwap_MultiSync_iff [simp] :
‹TickSwap P = ❙⟦S❙⟧ m ∈# M. Q m ⟷ P = ❙⟦S❙⟧ m ∈# M. TickSwap (Q m)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_MultiSeq [simp] :
‹L ≠ [] ⟹ TickSwap (SEQ l ∈@ L. P l) = SEQ l ∈@ L. TickSwap (P l)›
by (induct L rule: rev_induct, simp_all)
(metis MultiSeq_Nil SKIP_Seq TickSwap_Seq)
lemma TickSwap_is_MultiSeq_iff [simp] :
‹L ≠ [] ⟹ TickSwap P = SEQ l ∈@ L. Q l ⟷ P = SEQ l ∈@ L. TickSwap (Q l)›
by (metis TickSwap_MultiSeq TickSwap_TickSwap)
paragraph ‹Communications›
lemma TickSwap_write0 [simp] : ‹TickSwap (e → P) = e → TickSwap P›
by (simp add: TickSwap_is_Renaming Renaming_write0)
lemma TickSwap_is_write0_iff [simp] : ‹TickSwap P = e → Q ⟷ P = e → TickSwap Q›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_write [simp] : ‹TickSwap (c❙!e → P) = c❙!e → TickSwap P›
by (simp add: TickSwap_is_Renaming Renaming_write)
lemma TickSwap_is_write_iff [simp] : ‹TickSwap P = c❙!e → Q ⟷ P = c❙!e → TickSwap Q›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Mprefix [simp] :
‹TickSwap (□a ∈ A → P a) = □a ∈ A → TickSwap (P a)›
by (simp add: Mprefix_GlobalDet)
lemma TickSwap_is_Mprefix_iff [simp] :
‹TickSwap P = (□a ∈ A → Q a) ⟷ P = □a ∈ A → TickSwap (Q a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_read [simp] : ‹TickSwap (c❙?a∈A → P a) = c❙?a∈A → TickSwap (P a)›
by (simp add: read_def comp_def)
lemma TickSwap_is_read_iff [simp] :
‹TickSwap P = c❙?a∈A → Q a ⟷ P = c❙?a∈A → TickSwap (Q a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_Mndetprefix [simp] :
‹TickSwap (⊓a ∈ A → P a) = ⊓a ∈ A → TickSwap (P a)›
by (simp add: Mndetprefix_GlobalNdet)
lemma TickSwap_is_Mndetprefix_iff [simp] :
‹TickSwap P = (⊓a ∈ A → Q a) ⟷ P = ⊓a ∈ A → TickSwap (Q a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
lemma TickSwap_ndet_write [simp] : ‹TickSwap (c❙!❙!a∈A → P a) = c❙!❙!a∈A → TickSwap (P a)›
by (simp add: ndet_write_def comp_def)
lemma TickSwap_is_ndet_write_iff [simp] :
‹TickSwap P = c❙!❙!a∈A → Q a ⟷ P = c❙!❙!a∈A → TickSwap (Q a)›
by (simp add: TickSwap_eq_iff_eq_TickSwap)
section ‹Splitting the Renaming Operator›
text ‹
We split the \<^const>‹Renaming› operator in two: the first one only renames
the ``regular'' events, the second one only the ticks.
›
subsection ‹Renaming only Events›
abbreviation RenamingEv :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a ⇒ 'b] ⇒ ('b, 'r) process⇩p⇩t⇩i⇩c⇩k›
where ‹RenamingEv P f ≡ Renaming P f id›
lemma RenamingEv_id_unfolded [iff] :
‹Renaming P f (λr. r) = RenamingEv P f› by (simp add: id_def)
lemmas strict_ticks_of_RenamingEv_subset = strict_ticks_of_Renaming_subset [where g = id, simplified]
and strict_ticks_of_inj_on_RenamingEv = strict_ticks_of_inj_on_Renaming [where g = id, simplified]
lemmas monos_RenamingEv = monos_Renaming[where g = id]
lemma RenamingEv_SKIP : ‹RenamingEv (SKIP r) f = SKIP r› by simp
lemma RenamingEv_cont :
‹cont P ⟹ finitary f ⟹ cont (λx. RenamingEv (P x) f)› by simp
lemma RenamingEv_Seq :
‹RenamingEv (P ❙; Q) f = RenamingEv P f ❙; RenamingEv Q f›
by (simp add: Renaming_Seq)
declare Renaming_id [simp]
lemmas RenamingEv_id = Renaming_id
and RenamingEv_STOP = Renaming_STOP [where g = id]
and RenamingEv_BOT = Renaming_BOT [where g = id]
and RenamingEv_is_STOP_iff = Renaming_is_STOP_iff [where g = id]
and RenamingEv_is_BOT_iff = Renaming_is_BOT_iff [where g = id]
lemmas RenamingEv_Det = Renaming_Det [where g = id]
and RenamingEv_Ndet = Renaming_Ndet [where g = id]
and RenamingEv_Sliding = Renaming_Sliding [where g = id]
and RenamingEv_Interrupt = Renaming_Interrupt [where g = id]
and RenamingEv_write0 = Renaming_write0 [where g = id]
and RenamingEv_write = Renaming_write [where g = id]
and RenamingEv_comp = Renaming_comp [of _ _ _ id id, simplified]
and RenamingEv_inv = Renaming_inv [where g = id, simplified]
and inv_RenamingEv = inv_Renaming [where g = id, simplified]
lemmas bij_RenamingEv_Sync = bij_Renaming_Sync [where g = id, simplified]
and bij_RenamingEv_Hiding = bij_Renaming_Hiding [where g = id, simplified]
and inj_on_RenamingEv_Throw = inj_on_Renaming_Throw [where g = id]
and RenamingEv_fix = Renaming_fix [where g = id, simplified]
lemmas RenamingEv_distrib_GlobalDet = Renaming_distrib_GlobalDet [where g = id]
and RenamingEv_distrib_GlobalNDet = Renaming_distrib_GlobalNdet [where g = id]
and RenamingEv_Mprefix = Renaming_Mprefix [where g = id]
and RenamingEv_Mndetprefix = Renaming_Mndetprefix [where g = id]
and RenamingEv_read = Renaming_read [where g = id]
and RenamingEv_ndet_write = Renaming_ndet_write [where g = id]
subsection ‹Renaming only Ticks›
abbreviation RenamingTick :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'r ⇒ 's] ⇒ ('a, 's) process⇩p⇩t⇩i⇩c⇩k›
where ‹RenamingTick P g ≡ Renaming P id g›
lemma RenamingTick_id_unfolded [iff] :
‹Renaming P (λa. a) g = RenamingTick P g› by (simp add: id_def)
lemmas strict_ticks_of_RenamingTick_subset = strict_ticks_of_Renaming_subset [where f = id]
and strict_ticks_of_inj_on_RenamingTick = strict_ticks_of_inj_on_Renaming [where f = id, simplified]
lemmas monos_RenamingTick = monos_Renaming[where f = id]
lemma RenamingTick_cont :
‹cont P ⟹ finitary g ⟹ cont (λx. RenamingTick (P x) g)› by simp
lemmas RenamingTick_id = Renaming_id
and RenamingTick_STOP = Renaming_STOP [where f = id]
and RenamingTick_SKIP = Renaming_SKIP [where f = id]
and RenamingTick_BOT = Renaming_BOT [where f = id]
and RenamingTick_is_STOP_iff = Renaming_is_STOP_iff [where f = id]
and RenamingTick_is_BOT_iff = Renaming_is_BOT_iff [where f = id]
lemmas RenamingTick_Seq = Renaming_Seq[where f = id]
and RenamingTick_Det = Renaming_Det [where f = id]
and RenamingTick_Ndet = Renaming_Ndet [where f = id]
and RenamingTick_Sliding = Renaming_Sliding [where f = id]
and RenamingTick_Interrupt = Renaming_Interrupt [where f = id]
and RenamingTick_write0 = Renaming_write0 [where f = id, simplified]
and RenamingTick_write = Renaming_write [where f = id, simplified]
and RenamingTick_comp = Renaming_comp [of _ id id , simplified]
and RenamingTick_inv = Renaming_inv [where f = id, simplified]
and inv_RenamingTick = inv_Renaming [where f = id, simplified]
lemmas bij_RenamingTick_Sync = bij_Renaming_Sync [where f = id, simplified]
and RenamingTick_fix = Renaming_fix [where f = id, simplified]
lemma RenamingTick_Throw :
‹RenamingTick (P Θ a∈A. Q a) g = RenamingTick P g Θ a∈A. RenamingTick (Q a) g›
proof (subst inj_on_Renaming_Throw)
show ‹inj_on id (events_of P ∪ A)› by simp
next
show ‹RenamingTick P g Θ b∈id ` A. RenamingTick (Q (inv_into A id b)) g =
RenamingTick P g Θ a∈A. RenamingTick (Q a) g›
by (simp, rule mono_Throw_eq)
(metis f_inv_into_f id_apply image_id)
qed
lemmas RenamingTick_distrib_GlobalDet = Renaming_distrib_GlobalDet [where f = id]
and RenamingTick_distrib_GlobalNDet = Renaming_distrib_GlobalNdet [where f = id]
and RenamingTick_Mprefix = Renaming_Mprefix_image_inj [where f = id, simplified]
and RenamingTick_Mndetprefix = Renaming_Mndetprefix_inj [where f = id, simplified]
and RenamingTick_read = Renaming_read [where f = id, simplified]
and RenamingTick_ndet_write = Renaming_ndet_write [where f = id, simplified]
lemma RenamingEv_RenamingTick_is_Renaming :
‹RenamingEv (RenamingTick P g) f = Renaming P f g›
and RenamingTick_RenamingEv_is_Renaming :
‹RenamingTick (RenamingEv P f) g = Renaming P f g›
by (metis Renaming_comp comp_id fun.map_id)+
subsection ‹Properties›
lemma isInfHidden_seqRun_imp_tickFree_seqRun :
‹isInfHidden_seqRun x P A t ⟹ tF (seqRun t x i)›
by (metis event⇩p⇩t⇩i⇩c⇩k.disc(1) image_iff isInfHidden_seqRun_imp_tickFree tickFree_seqRun_iff)
lemma tickFree_map_map_event⇩p⇩t⇩i⇩c⇩k_is :
‹tF t ⟹ map (map_event⇩p⇩t⇩i⇩c⇩k f g) t = map (ev ∘ f ∘ of_ev) t›
by (induct t) (auto simp add: is_ev_def)
lemma RenamingTick_Hiding :
‹RenamingTick (P \ A) g = RenamingTick P g \ A›
(is ‹?lhs = ?rhs›) for P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof -
let ?RT = ‹λP. RenamingTick P g›
let ?th_A = ‹λt. trace_hide t (ev ` A)›
let ?map = ‹map (map_event⇩p⇩t⇩i⇩c⇩k id g)›
have $ : ‹?th_A (?map t) = ?map (?th_A t)› for t
by (induct t) (simp_all add: image_iff map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff)
have $$ : ‹map_event⇩p⇩t⇩i⇩c⇩k id g -` X ∪ ev ` A =
map_event⇩p⇩t⇩i⇩c⇩k id g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k id g -` ev ` A› for X
by (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_ev_iff)
show ‹?lhs = ?rhs›
proof (rule Process_eq_optimizedI)
fix t assume ‹t ∈ 𝒟 ?lhs›
then obtain t1 t2 where * : ‹t = ?map t1 @ t2›
‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P \ A)› unfolding D_Renaming by blast
from "*"(4) obtain u v where ** : ‹ftF v› ‹tF u› ‹t1 = ?th_A u @ v›
‹u ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun_strong x P A u)›
by (blast elim: D_Hiding_seqRunE)
from "**"(4) show ‹t ∈ 𝒟 ?rhs›
proof (elim disjE exE)
assume ‹u ∈ 𝒟 P›
with "**"(2) have ‹?map u ∈ 𝒟 (?RT P)›
by (auto simp add: D_Renaming intro: front_tickFree_Nil)
thus ‹t ∈ 𝒟 ?rhs›
by (simp add: D_Hiding "*"(1) "**"(3) flip: "$")
(metis "*"(2, 3) "**"(2, 3) front_tickFree_append
map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
next
fix x assume *** : ‹isInfHidden_seqRun_strong x P A u›
have ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) (?RT P) A (?map u)›
proof (intro allI conjI)
fix i
have ‹seqRun (?map u) (ev ∘ of_ev ∘ x) i = ?map (seqRun u x i)›
by (simp add: seqRun_def image_iff ev_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)
(metis "***" event⇩p⇩t⇩i⇩c⇩k.sel(1) imageE)
also have ‹?map (seqRun u x i) ∈ 𝒯 (?RT P)›
unfolding T_Renaming using "***" Un_iff by blast
finally show ‹seqRun (?map u) (ev ∘ of_ev ∘ x) i ∈ 𝒯 (?RT P)› .
next
show ‹(ev ∘ of_ev ∘ x) i ∈ ev ` A› for i
by (metis "***" comp_apply event⇩p⇩t⇩i⇩c⇩k.sel(1) image_iff)
qed
thus ‹t ∈ 𝒟 ?rhs›
by (simp (no_asm) add: D_Hiding_seqRun "*"(1) "**"(3) flip: "$")
(metis "*"(2, 3) "**"(2, 3) front_tickFree_append
map_event⇩p⇩t⇩i⇩c⇩k_tickFree tickFree_append_iff)
qed
next
fix t assume ‹t ∈ 𝒟 ?rhs›
then obtain u v where * : ‹ftF v› ‹tF u› ‹t = ?th_A u @ v›
‹u ∈ 𝒟 (?RT P) ∨ (∃x. isInfHidden_seqRun_strong x (?RT P) A u)›
by (blast elim: D_Hiding_seqRunE)
from "*"(4) show ‹t ∈ 𝒟 ?lhs›
proof (elim disjE exE)
assume ‹u ∈ 𝒟 (?RT P)›
then obtain u1 u2 where ** : ‹u = ?map u1 @ u2›
‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P› unfolding D_Renaming by blast
from mem_D_imp_mem_D_Hiding "**"(4) have ‹?th_A u1 ∈ 𝒟 (P \ A)› .
thus ‹t ∈ 𝒟 ?lhs›
by (simp add: D_Renaming "*"(3) "**"(1) "$")
(metis "*"(1, 2) "**"(1, 2) Hiding_tickFree
front_tickFree_append tickFree_append_iff)
next
fix x assume ** : ‹isInfHidden_seqRun_strong x (?RT P) A u›
hence ‹∀i. ∃v. seqRun u x i = ?map v ∧ v ∈ 𝒯 P›
unfolding Renaming_projs by blast
then obtain f where *** : ‹seqRun u x i = ?map (f i)› ‹f i ∈ 𝒯 P› for i by metis
have ‹tF (f i)› for i
by (metis isInfHidden_seqRun_imp_tickFree_seqRun
"**" "***"(1) map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
hence ‹?map (f i) = map (ev ∘ of_ev) (f i)› for i
by (simp add: tickFree_map_map_event⇩p⇩t⇩i⇩c⇩k_is)
from "***"(1)[unfolded this]
have ‹map (ev ∘ of_ev) (seqRun u x i) =
(map (ev ∘ of_ev) (map (ev ∘ of_ev) (f i)) :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k)› for i by simp
also have ‹map (ev ∘ of_ev) (map (ev ∘ of_ev) (f i)) = f i› for i
using ‹⋀i. tF (f i)›[of i]
by (auto simp add: tickFree_iff_is_map_ev)
finally have ‹f i = map (ev ∘ of_ev) (seqRun u x i)› for i by (rule sym)
hence **** : ‹f i = seqRun (f 0) (ev ∘ of_ev ∘ x) i› for i
by (simp add: seqRun_def "***"(1))
have ‹isInfHidden_seqRun (ev ∘ of_ev ∘ x) P A (f 0)›
proof (intro allI conjI)
show ‹seqRun (f 0) (ev ∘ of_ev ∘ x) i ∈ 𝒯 P› for i by (metis "***"(2) "****")
next
show ‹(ev ∘ of_ev ∘ x) i ∈ ev ` A› for i
using "**"[THEN spec, of i] by auto
qed
with ‹⋀i. tF (f i)› have ‹?th_A (f 0) ∈ 𝒟 (P \ A)›
by (simp add: D_Hiding_seqRun)
(metis append.right_neutral comp_apply front_tickFree_Nil)
moreover have ‹?th_A u = ?map (?th_A (f 0))›
by (metis "$" "***"(1) seqRun_0)
ultimately show ‹t ∈ 𝒟 ?lhs›
by (simp add: D_Renaming "*"(3))
(use "*"(1) Hiding_tickFree ‹⋀i. tF (f i)› in blast)
qed
next
fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
then obtain t' where * : ‹t = ?map t'›
‹(t', map_event⇩p⇩t⇩i⇩c⇩k id g -` X) ∈ ℱ (P \ A)›
unfolding Renaming_projs by blast
from "*"(2) consider ‹t' ∈ 𝒟 (P \ A)›
| ("**") t'' where ‹t' = ?th_A t''›
‹(t'', map_event⇩p⇩t⇩i⇩c⇩k id g -` X ∪ ev ` A) ∈ ℱ P›
unfolding F_Hiding D_Hiding by blast
thus ‹(t, X) ∈ ℱ ?rhs›
proof cases
assume ‹t' ∈ 𝒟 (P \ A)›
hence ‹tF t' ∨ (∃t'' r. t' = t'' @ [✓(r)] ∧ tF t'')›
by (metis D_imp_front_tickFree front_tickFree_append_iff
nonTickFree_n_frontTickFree not_Cons_self2)
with ‹t' ∈ 𝒟 (P \ A)› ‹t ∉ 𝒟 ?lhs› have False
by (elim disjE exE conjE, simp_all add: D_Renaming "*"(1))
(use front_tickFree_Nil in blast, metis front_tickFree_single is_processT9)
thus ‹(t, X) ∈ ℱ ?rhs› ..
next
case "**"
from "**"(2) have ‹(?map t'', X ∪ ev ` A) ∈ ℱ (?RT P)›
by (auto simp add: F_Renaming "$$")
thus ‹(t, X) ∈ ℱ ?rhs› by (simp add: F_Hiding "*"(1) "**"(1)) (metis "$")
qed
next
fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
then obtain t' where * : ‹t = ?th_A t'› ‹(t', X ∪ ev ` A) ∈ ℱ (?RT P)›
unfolding F_Hiding D_Hiding by blast
from "*"(2) consider ‹t' ∈ 𝒟 (?RT P)›
| ("**") t'' where ‹t' = ?map t''›
‹(t'', map_event⇩p⇩t⇩i⇩c⇩k id g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k id g -` ev ` A) ∈ ℱ P›
by (auto simp add: Renaming_projs)
thus ‹(t, X) ∈ ℱ ?lhs›
proof cases
assume ‹t' ∈ 𝒟 (?RT P)›
hence ‹tF t' ∨ (∃t'' r. t' = t'' @ [✓(r)] ∧ tF t'')›
by (metis D_imp_front_tickFree front_tickFree_append_iff
nonTickFree_n_frontTickFree not_Cons_self2)
with ‹t' ∈ 𝒟 (?RT P)› ‹t ∉ 𝒟 ?rhs› have False
by (elim disjE exE, auto simp add: D_Hiding_seqRun "*"(1) image_iff
intro: front_tickFree_single is_processT9)
thus ‹(t, X) ∈ ℱ ?lhs› ..
next
case "**"
from "**"(2) have ‹(?th_A t'', map_event⇩p⇩t⇩i⇩c⇩k id g -` X) ∈ ℱ (P \ A)›
by (auto simp add: F_Hiding "$$")
thus ‹(t, X) ∈ ℱ ?lhs›
by (auto simp add: F_Renaming "*"(1) "**"(1) "$")
qed
qed
qed
corollary bij_Renaming_Hiding :
‹Renaming (P \ S) f g = Renaming P f g \ f ` S› (is ‹?lhs = ?rhs›) if ‹bij f›
proof -
have ‹?lhs = RenamingTick (RenamingEv (P \ S) f) g›
by (simp only: RenamingTick_RenamingEv_is_Renaming)
also have ‹… = RenamingTick (RenamingEv P f \ f ` S) g›
by (simp only: bij_RenamingEv_Hiding[OF ‹bij f›])
also have ‹… = RenamingTick (RenamingEv P f) g \ f ` S›
by (simp only: RenamingTick_Hiding)
also have ‹… = ?rhs›
by (simp only: RenamingTick_RenamingEv_is_Renaming)
finally show ‹?lhs = ?rhs› .
qed
lemma Renaming_is_restrictable_on_events_of_strict_ticks_of :
‹Renaming P f g = Renaming P f' g'›
if fun_hyps : ‹⋀a. a ∈ α(P) ⟹ f a = f' a›
‹⋀r. r ∈ ❙✓❙s(P) ⟹ g r = g' r›
for f f' :: ‹'a ⇒ 'b› and g g' :: ‹'r ⇒ 't›
proof -
have * : ‹Renaming P f g ⊑⇩F⇩D Renaming P f' g'›
if fun_hyps_bis : ‹⋀a. a ∈ α(P) ⟹ f a = f' a› ‹⋀r. r ∈ ❙✓❙s(P) ⟹ g r = g' r›
for f f' :: ‹'a ⇒ 'b› and g g' :: ‹'r ⇒ 't›
proof -
have $ : ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u = map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u›
if ‹u ∈ 𝒯 P› and ‹tF u› for u
proof -
from ‹u ∈ 𝒯 P› have ‹ev a ∈ set u ⟹ a ∈ α(P)› for a
by (meson events_of_memI)
with ‹tF u› show ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u = map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u›
by (induct u, simp_all)
(metis event⇩p⇩t⇩i⇩c⇩k.collapse(1) event⇩p⇩t⇩i⇩c⇩k.simps(9) fun_hyps_bis(1))
qed
have ‹(∀t. t ∈ 𝒟 (Renaming P f' g') ⟶ t ∈ 𝒟 (Renaming P f g)) ∧
(∀t X. (t, X) ∈ ℱ (Renaming P f' g') ⟶ t ∉ 𝒟 (Renaming P f' g') ⟶ (t, X) ∈ ℱ (Renaming P f g))›
proof (intro conjI allI impI)
fix t assume ‹t ∈ 𝒟 (Renaming P f' g')›
then obtain u1 u2 where * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u1 @ u2›
‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 P› unfolding D_Renaming by blast
have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1›
by (simp add: ‹tF u1› "$" "*"(4) D_T)
with "*" show ‹t ∈ 𝒟 (Renaming P f g)›
by (auto simp add: D_Renaming)
next
fix t X assume ‹(t, X) ∈ ℱ (Renaming P f' g')› ‹t ∉ 𝒟 (Renaming P f' g')›
then obtain u where * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u›
‹(u, map_event⇩p⇩t⇩i⇩c⇩k f' g' -` X) ∈ ℱ P›
unfolding Renaming_projs by blast
show ‹(t, X) ∈ ℱ (Renaming P f g)›
proof (cases ‹tF u›)
assume ‹tF u›
have ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f' g' -` X ∪ {ev a |a. a ∉ α(P)} ∪
{✓(r) |r. r ∉ ❙✓❙s(P)}) ∈ ℱ P› (is ‹(u, ?Y) ∈ ℱ P›)
by (intro is_processT5, simp_all add: "*"(2))
(meson T_F_spec events_of_memI in_set_conv_decomp,
metis (mono_tags, lifting) "*"(1) D_Renaming F_imp_front_tickFree T_F_spec
‹t ∉ 𝒟 (Renaming P f' g')› append_Nil2 append_T_imp_tickFree is_processT1
is_processT9 list.simps(3) mem_Collect_eq strict_ticks_of_memI)
moreover from fun_hyps_bis
have ‹e ∈ map_event⇩p⇩t⇩i⇩c⇩k f g -` X ⟹ e ∈ ?Y› for e
by (cases e) auto
ultimately have ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ P›
by (meson is_processT4 subset_eq)
moreover have ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u›
by (metis "$" "*" F_T ‹tF u›)
ultimately show ‹(t, X) ∈ ℱ (Renaming P f g)›
by (auto simp add: F_Renaming)
next
assume ‹¬ tF u›
then obtain u' r where ‹tF u'› ‹u = u' @ [✓(r)]›
by (metis "*"(2) F_imp_front_tickFree front_tickFree_append_iff
nonTickFree_n_frontTickFree not_Cons_self2)
from "*"(2) F_T ‹u = u' @ [✓(r)]› have ‹u' @ [✓(r)] ∈ 𝒯 P› by blast
have $$ : ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u'›
by (metis "$" "*"(2) F_T ‹tF u'› ‹u = u' @ [✓(r)]› is_processT3_TR_append)
have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' @ [✓(g' r)] ∈ 𝒯 (Renaming P f g)›
proof (cases ‹r ∈ ❙✓❙s(P)›)
assume ‹r ∈ ❙✓❙s(P)›
hence ‹g' r = g r› by (simp add: fun_hyps_bis(2))
with "$$" show ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' @ [✓(g' r)] ∈ 𝒯 (Renaming P f g)›
by (simp add: T_Renaming) (use ‹u' @ [✓(r)] ∈ 𝒯 P› in auto)
next
assume ‹r ∉ ❙✓❙s(P)›
hence ‹u' ∈ 𝒟 P›
by (metis ‹u' @ [✓(r)] ∈ 𝒯 P› is_processT9 strict_ticks_of_memI)
hence ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u' ∈ 𝒟 (Renaming P f g)›
using D_Renaming F_imp_front_tickFree ‹tF u'› is_processT1 by blast
with "$$" have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' ∈ 𝒟 (Renaming P f g)› by presburger
hence ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' @ [✓(g' r)] ∈ 𝒟 (Renaming P f g)›
by (simp add: ‹tF u'› is_processT7 map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
thus ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' @ [✓(g' r)] ∈ 𝒯 (Renaming P f g)›
by (simp add: D_T)
qed
hence ‹(map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' @ [✓(g' r)], X) ∈ ℱ (Renaming P f g)›
by (simp add: tick_T_F)
also have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f' g') u' @ [✓(g' r)] = t›
by (simp add: "*"(1) ‹u = u' @ [✓(r)]›)
finally show ‹(t, X) ∈ ℱ (Renaming P f g)› .
qed
qed
thus ‹Renaming P f g ⊑⇩F⇩D Renaming P f' g'›
by (auto simp add: refine_defs intro: is_processT8)
qed
show ‹Renaming P f g = Renaming P f' g'›
proof (rule FD_antisym)
show ‹Renaming P f g ⊑⇩F⇩D Renaming P f' g'› ‹Renaming P f' g' ⊑⇩F⇩D Renaming P f g›
by (simp_all add: "*" fun_hyps)
qed
qed
corollary Renaming_is_restrictable_on_events_of_ticks_of :
‹⟦⋀a. a ∈ α(P) ⟹ f a = f' a; ⋀r. r ∈ ✓s(P) ⟹ g r = g' r⟧
⟹ Renaming P f g = Renaming P f' g'›
by (rule Renaming_is_restrictable_on_events_of_strict_ticks_of)
(simp_all add: ticks_of_is_strict_ticks_of_or_UNIV)
corollary RenamingEv_is_restrictable_on_events_of :
‹(⋀a. a ∈ α(P) ⟹ f a = f' a) ⟹ RenamingEv P f = RenamingEv P f'›
by (fact Renaming_is_restrictable_on_events_of_ticks_of
[of P f f' id id, simplified])
corollary RenamingTick_is_restrictable_on_strict_ticks_of :
‹(⋀r. r ∈ ❙✓❙s(P) ⟹ g r = g' r) ⟹ RenamingTick P g = RenamingTick P g'›
by (fact Renaming_is_restrictable_on_events_of_strict_ticks_of
[of P id id g g', simplified])
corollary RenamingTick_is_restrictable_on_ticks_of :
‹(⋀r. r ∈ ✓s(P) ⟹ g r = g' r) ⟹ RenamingTick P g = RenamingTick P g'›
by (fact Renaming_is_restrictable_on_events_of_ticks_of
[of P id id g g', simplified])
section ‹Renaming and Generalized Synchronization Product›
lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) inj_on_RenamingTick_Sync⇩p⇩t⇩i⇩c⇩k :
‹RenamingTick (P ⟦S⟧⇩✓ Q) g =
Sync⇩p⇩t⇩i⇩c⇩k_locale.Sync⇩p⇩t⇩i⇩c⇩k (λr s. case r ⊗✓ s of ⌊r_s⌋ ⇒ ⌊g r_s⌋ | ◇ ⇒ ◇) P S Q›
(is ‹?lhs = ?rhs›)
if inj_on_g : ‹inj_on g range_tick_join›
proof -
let ?map_evt = ‹λg. map (map_event⇩p⇩t⇩i⇩c⇩k id g)›
let ?tick_join' = ‹λr s. case r ⊗✓ s of ⌊r_s⌋ ⇒ ⌊g r_s⌋ | ◇ ⇒ ◇›
interpret Sync⇩p⇩t⇩i⇩c⇩k' : Sync⇩p⇩t⇩i⇩c⇩k_locale ?tick_join'
by (intro interpretable_inj_on_range_tick_join inj_on_g)
have inj_on_inv_into_g :
‹inj_on (inv_into range_tick_join g) Sync⇩p⇩t⇩i⇩c⇩k'.range_tick_join›
by (rule inj_onI, simp split: option.split_asm)
(metis (mono_tags, lifting) f_inv_into_f image_eqI mem_Collect_eq)
from inv_into_f_f inj_on_g have expanded_tick_join :
‹(⊗✓) = (λr s. case ?tick_join' r s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊inv_into range_tick_join g r_s⌋)›
by (fastforce split: split: option.split)
show ‹?lhs = ?rhs›
proof (rule Process_eq_optimizedI)
fix t assume ‹t ∈ 𝒟 ?lhs›
then obtain u1 u2 where * : ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k id g) u1 @ u2›
‹tF u1› ‹ftF u2› ‹u1 ∈ 𝒟 (P ⟦S⟧⇩✓ Q)›
unfolding D_Renaming by blast
from "*"(4) obtain v1 w1 t_P t_Q
where ** : ‹u1 = v1 @ w1› ‹tF v1› ‹ftF w1›
‹v1 setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
from inj_on_map_map_event⇩p⇩t⇩i⇩c⇩k_setinterleaves⇩p⇩t⇩i⇩c⇩k[OF inj_on_g "**"(4)]
have ‹?map_evt g v1 setinterleaves⇩✓⇘?tick_join'⇙ ((t_P, t_Q), S)› .
moreover from "*"(1-3) "**"(1, 2)
have ‹t = ?map_evt g v1 @ (?map_evt g w1 @ u2) ∧
tF (?map_evt g v1) ∧ ftF (?map_evt g w1 @ u2)›
by (simp add: front_tickFree_append_iff map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
ultimately show ‹t ∈ 𝒟 ?rhs›
using "**"(5) by (simp (no_asm) add: Sync⇩p⇩t⇩i⇩c⇩k'.D_Sync⇩p⇩t⇩i⇩c⇩k) blast
next
fix t assume ‹t ∈ 𝒟 ?rhs›
then obtain u v t_P t_Q
where * : ‹t = u @ v› ‹tF u› ‹ftF v›
‹u setinterleaves⇩✓⇘?tick_join'⇙ ((t_P, t_Q), S)›
‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
unfolding Sync⇩p⇩t⇩i⇩c⇩k'.D_Sync⇩p⇩t⇩i⇩c⇩k by blast
from ‹tF u› have ‹e ∈ set u ⟹ map_event⇩p⇩t⇩i⇩c⇩k id (g ∘ inv_into range_tick_join g) e = e› for e
by (cases e) (simp_all add: tickFree_def disjoint_iff)
hence ‹t = ?map_evt g (?map_evt (inv_into range_tick_join g) u) @ v›
by (simp add: "*"(1) flip: map_event⇩p⇩t⇩i⇩c⇩k_comp)
(induct u, simp_all)
moreover have ‹tF (?map_evt (inv_into range_tick_join g) u)›
by (simp add: "*"(2) map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
moreover
{
have ‹?map_evt (inv_into range_tick_join g) u =
?map_evt (inv_into range_tick_join g) u @ []› by simp
moreover have ‹tF ((map (map_event⇩p⇩t⇩i⇩c⇩k id (inv_into range_tick_join g))) u)›
by (simp add: "*"(2) map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
moreover have ‹ftF []› by simp
moreover from Sync⇩p⇩t⇩i⇩c⇩k'.inj_on_map_map_event⇩p⇩t⇩i⇩c⇩k_setinterleaves⇩p⇩t⇩i⇩c⇩k
[OF inj_on_inv_into_g "*"(4), folded expanded_tick_join]
have ‹?map_evt (inv_into range_tick_join g) u
setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)› .
ultimately have ‹?map_evt (inv_into range_tick_join g) u ∈ 𝒟 (P ⟦S⟧⇩✓ Q)›
unfolding D_Sync⇩p⇩t⇩i⇩c⇩k using "*"(5) by blast
}
ultimately show ‹t ∈ 𝒟 ?lhs›
unfolding D_Renaming using "*"(3) by blast
next
fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
then obtain u
where * : ‹t = ?map_evt g u› ‹(u, map_event⇩p⇩t⇩i⇩c⇩k id g -` X) ∈ ℱ (P ⟦S⟧⇩✓ Q)›
unfolding Renaming_projs by blast
with ‹t ∉ 𝒟 ?lhs› obtain t_P t_Q X_P X_Q
where ** : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
‹map_event⇩p⇩t⇩i⇩c⇩k id g -` X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k (⊗✓) X_P S X_Q›
by (auto simp add: D_Renaming Sync⇩p⇩t⇩i⇩c⇩k_projs)
(metis append.right_neutral front_tickFree_Nil map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree)+
have ‹t setinterleaves⇩✓⇘?tick_join'⇙ ((t_P, t_Q), S)›
using "*"(1) "**"(3) inj_on_map_map_event⇩p⇩t⇩i⇩c⇩k_setinterleaves⇩p⇩t⇩i⇩c⇩k inj_on_g by blast
moreover from vimage_inj_on_subset_super_ref_Sync⇩p⇩t⇩i⇩c⇩k_iff[OF inj_on_g, THEN iffD1, OF "**"(4)]
have ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k ?tick_join' X_P S X_Q› .
ultimately show ‹(t, X) ∈ ℱ ?rhs›
unfolding Sync⇩p⇩t⇩i⇩c⇩k'.F_Sync⇩p⇩t⇩i⇩c⇩k using "**"(1, 2) by fast
next
fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
then obtain t_P t_Q X_P X_Q
where * : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
‹t setinterleaves⇩✓⇘?tick_join'⇙ ((t_P, t_Q), S)›
‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k ?tick_join' X_P S X_Q›
unfolding Sync⇩p⇩t⇩i⇩c⇩k'.Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
from Sync⇩p⇩t⇩i⇩c⇩k'.setinterleaves⇩p⇩t⇩i⇩c⇩k_imp_set_range_tick_join[OF "*"(3)]
have ‹{r_s. ✓(r_s) ∈ set t} ⊆ Sync⇩p⇩t⇩i⇩c⇩k'.range_tick_join› .
hence ‹e ∈ set t ⟹ map_event⇩p⇩t⇩i⇩c⇩k id (g ∘ inv_into range_tick_join g) e = e› for e
by (cases e, auto simp add: subset_iff split: option.split_asm)
(metis (mono_tags, lifting) inv_into_f_f mem_Collect_eq inj_on_g)
hence ‹t = ?map_evt g (?map_evt (inv_into range_tick_join g) t)›
by (simp add: "*"(1) flip: map_event⇩p⇩t⇩i⇩c⇩k_comp)
(induct t, simp_all)
moreover
{ from Sync⇩p⇩t⇩i⇩c⇩k'.inj_on_map_map_event⇩p⇩t⇩i⇩c⇩k_setinterleaves⇩p⇩t⇩i⇩c⇩k
[OF inj_on_inv_into_g "*"(3), folded expanded_tick_join]
have ‹?map_evt (inv_into range_tick_join g) t
setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)› .
moreover from vimage_inj_on_subset_super_ref_Sync⇩p⇩t⇩i⇩c⇩k_iff
[OF inj_on_g, THEN iffD2, OF "*"(4)]
have ‹map_event⇩p⇩t⇩i⇩c⇩k id g -` X ⊆
super_ref_Sync⇩p⇩t⇩i⇩c⇩k (⊗✓) X_P S X_Q› .
ultimately have ‹(?map_evt (inv_into range_tick_join g) t,
map_event⇩p⇩t⇩i⇩c⇩k id g -` X) ∈ ℱ (P ⟦S⟧⇩✓ Q)›
by (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k "*"(1, 2))
}
ultimately show ‹(t, X) ∈ ℱ ?lhs› unfolding F_Renaming by blast
qed
qed
lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) inj_RenamingTick_Sync⇩p⇩t⇩i⇩c⇩k_inj_RenamingTick :
‹RenamingTick P g ⟦S⟧⇩✓ RenamingTick Q h =
Sync⇩p⇩t⇩i⇩c⇩k_locale.Sync⇩p⇩t⇩i⇩c⇩k (λr s. g r ⊗✓ h s) P S Q› (is ‹?lhs = ?rhs›)
if ‹inj g› and ‹inj h›
for P :: ‹('a, 'r') process⇩p⇩t⇩i⇩c⇩k› and Q :: ‹('a, 's') process⇩p⇩t⇩i⇩c⇩k›
proof -
interpret tjoin_interpreted : Sync⇩p⇩t⇩i⇩c⇩k_locale ‹λr s. g r ⊗✓ h s›
by unfold_locales (meson injD inj_tick_join ‹inj g› ‹inj h›)
let ?map_evt = ‹λg. map (map_event⇩p⇩t⇩i⇩c⇩k id g)›
let ?map_ev = ‹λt. map ev (map of_ev t)›
let ?RT = RenamingTick
have * : ‹tF t ⟹ ?map_evt g t = ?map_ev t› for t :: ‹('a, 'r') trace⇩p⇩t⇩i⇩c⇩k›
by (induct t) (auto simp add: is_ev_def)
have ** : ‹tF t ⟹ ?map_evt h t = ?map_ev t› for t :: ‹('a, 's') trace⇩p⇩t⇩i⇩c⇩k›
by (induct t) (auto simp add: is_ev_def)
have *** : ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((?map_evt g u, ?map_evt h v), S)
⟷ t setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((u, v), S)› for t u v
by (induct ‹(λr s. g r ⊗✓ h s, u, S, v)› arbitrary: t u v) (auto split: option.split)
have **** : ‹?map_evt g t = ?map_evt g t' ⟷ t = t'› for t t' :: ‹('a, 'r') trace⇩p⇩t⇩i⇩c⇩k›
by (rule iffI, induct t arbitrary: t', auto)
(metis event⇩p⇩t⇩i⇩c⇩k.inj_map id_apply inj_def ‹inj g›)
have ***** : ‹?map_evt h t = ?map_evt h t' ⟷ t = t'› for t t' :: ‹('a, 's') trace⇩p⇩t⇩i⇩c⇩k›
by (rule iffI, induct t arbitrary: t', auto)
(metis event⇩p⇩t⇩i⇩c⇩k.inj_map id_apply inj_def ‹inj h›)
show ‹?lhs = ?rhs›
proof (rule Process_eq_optimizedI)
fix t assume ‹t ∈ 𝒟 ?lhs›
then obtain u v t_P' t_Q' where $ : ‹t = u @ v› ‹tF u› ‹ftF v›
‹u setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)›
‹t_P' ∈ 𝒟 (?RT P g) ∧ t_Q' ∈ 𝒯 (?RT Q h) ∧ t_Q' ∉ 𝒟 (?RT Q h) ∨
t_P' ∈ 𝒯 (?RT P g) ∧ t_P' ∉ 𝒟 (?RT P g) ∧ t_Q' ∈ 𝒟 (?RT Q h) ∨
t_P' ∈ 𝒟 (?RT P g) ∧ t_Q' ∈ 𝒟 (?RT Q h)›
unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
from "$"(5) show ‹t ∈ 𝒟 ?rhs›
proof (elim disjE conjE)
assume ‹t_P' ∈ 𝒟 (?RT P g)› ‹t_Q' ∈ 𝒯 (?RT Q h)› ‹t_Q' ∉ 𝒟 (?RT Q h)›
then obtain t_P⇩1 t_P⇩2 t_Q
where $$ : ‹t_P' = ?map_evt g t_P⇩1 @ t_P⇩2› ‹tF t_P⇩1› ‹ftF t_P⇩2› ‹t_P⇩1 ∈ 𝒟 P›
‹t_Q' = ?map_evt h t_Q› ‹t_Q ∈ 𝒯 Q› unfolding Renaming_projs by blast
from "$"(4)[unfolded "$$"(1), THEN setinterleaves⇩p⇩t⇩i⇩c⇩k_appendL]
obtain u⇩1 u⇩2 t_Q'⇩1 t_Q'⇩2 where $$$ : ‹u = u⇩1 @ u⇩2› ‹t_Q' = t_Q'⇩1 @ t_Q'⇩2›
‹u⇩1 setinterleaves⇩✓⇘(⊗✓)⇙ ((?map_evt g t_P⇩1, t_Q'⇩1), S)› by blast
obtain t_Q⇩1 t_Q⇩2 where ‹t_Q = t_Q⇩1 @ t_Q⇩2› ‹t_Q'⇩1 = ?map_evt h t_Q⇩1›
by (metis "$$"(5) "$$$"(2) map_eq_append_conv)
from "$$$"(3)[unfolded this(2), THEN "***"[THEN iffD1]]
have ‹u⇩1 setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((t_P⇩1, t_Q⇩1), S)› .
moreover from ‹t_Q = t_Q⇩1 @ t_Q⇩2› is_processT3_TR_append "$$"(6)
have ‹t_Q⇩1 ∈ 𝒯 Q› by blast
ultimately show ‹t ∈ 𝒟 ?rhs›
using "$"(1-3) "$$"(4) "$$$"(1) front_tickFree_append
by (auto simp add: tjoin_interpreted.D_Sync⇩p⇩t⇩i⇩c⇩k)
next
assume ‹t_Q' ∈ 𝒟 (?RT Q h)› ‹t_P' ∈ 𝒯 (?RT P g)› ‹t_P' ∉ 𝒟 (?RT P g)›
then obtain t_Q⇩1 t_Q⇩2 t_P
where $$ : ‹t_Q' = ?map_evt h t_Q⇩1 @ t_Q⇩2› ‹tF t_Q⇩1› ‹ftF t_Q⇩2› ‹t_Q⇩1 ∈ 𝒟 Q›
‹t_P' = ?map_evt g t_P› ‹t_P ∈ 𝒯 P› unfolding Renaming_projs by blast
from "$"(4)[unfolded "$$"(1), THEN setinterleaves⇩p⇩t⇩i⇩c⇩k_appendR]
obtain u⇩1 u⇩2 t_P'⇩1 t_P'⇩2 where $$$ : ‹u = u⇩1 @ u⇩2› ‹t_P' = t_P'⇩1 @ t_P'⇩2›
‹u⇩1 setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P'⇩1, ?map_evt h t_Q⇩1), S)› by blast
obtain t_P⇩1 t_P⇩2 where ‹t_P = t_P⇩1 @ t_P⇩2› ‹t_P'⇩1 = ?map_evt g t_P⇩1›
by (metis "$$"(5) "$$$"(2) map_eq_append_conv)
from "$$$"(3)[unfolded this(2), THEN "***"[THEN iffD1]]
have ‹u⇩1 setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((t_P⇩1, t_Q⇩1), S)› .
moreover from ‹t_P = t_P⇩1 @ t_P⇩2› is_processT3_TR_append "$$"(6)
have ‹t_P⇩1 ∈ 𝒯 P› by blast
ultimately show ‹t ∈ 𝒟 ?rhs›
using "$"(1-3) "$$"(4) "$$$"(1) front_tickFree_append
by (auto simp add: tjoin_interpreted.D_Sync⇩p⇩t⇩i⇩c⇩k)
next
assume ‹t_P' ∈ 𝒟 (?RT P g)› ‹t_Q' ∈ 𝒟 (?RT Q h)›
then obtain t_P⇩1 t_P⇩2 t_Q⇩1 t_Q⇩2
where $$ : ‹t_P' = ?map_evt g t_P⇩1 @ t_P⇩2› ‹tF t_P⇩1› ‹ftF t_P⇩2› ‹t_P⇩1 ∈ 𝒟 P›
‹t_Q' = ?map_evt h t_Q⇩1 @ t_Q⇩2› ‹tF t_Q⇩1› ‹ftF t_Q⇩2› ‹t_Q⇩1 ∈ 𝒟 Q›
unfolding D_Renaming by blast
from "$"(4)[unfolded "$$"(1, 5), THEN setinterleaves⇩p⇩t⇩i⇩c⇩k_appendL]
obtain u⇩1 u⇩2 t_Q⇩1_bis t_Q⇩2_bis
where $$$ : ‹u = u⇩1 @ u⇩2› ‹?map_evt h t_Q⇩1 @ t_Q⇩2 = t_Q⇩1_bis @ t_Q⇩2_bis›
‹u⇩1 setinterleaves⇩✓⇘(⊗✓)⇙ ((?map_evt g t_P⇩1, t_Q⇩1_bis), S)› by blast
from "$$$"(2) have ‹t_Q⇩1_bis = ?map_evt h (take (length t_Q⇩1_bis) t_Q⇩1) ∨
t_Q⇩1_bis = ?map_evt h t_Q⇩1 @ take (length t_Q⇩1_bis - length t_Q⇩1) t_Q⇩2›
by (cases ‹length t_Q⇩1_bis ≤ length t_Q⇩1›)
(simp_all add: append_eq_append_conv_if take_map split: if_split_asm)
thus ‹t ∈ 𝒟 ?rhs›
proof (elim disjE)
assume ‹t_Q⇩1_bis = ?map_evt h (take (length t_Q⇩1_bis) t_Q⇩1)›
hence ‹u⇩1 setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((t_P⇩1, take (length t_Q⇩1_bis) t_Q⇩1), S)›
by (metis "$$$"(3) "***")
moreover have ‹take (length t_Q⇩1_bis) t_Q⇩1 ∈ 𝒯 Q›
by (metis "$$"(8) D_T append_take_drop_id is_processT3_TR_append)
ultimately show ‹t ∈ 𝒟 ?rhs›
using "$"(1-3) "$$"(4) "$$$"(1) front_tickFree_append
by (auto simp add: tjoin_interpreted.D_Sync⇩p⇩t⇩i⇩c⇩k)
next
assume ‹t_Q⇩1_bis = ?map_evt h t_Q⇩1 @ take (length t_Q⇩1_bis - length t_Q⇩1) t_Q⇩2›
with "$$$"(3)
have ‹u⇩1 setinterleaves⇩✓⇘(⊗✓)⇙ ((?map_evt g t_P⇩1,
?map_evt h t_Q⇩1 @ take (length t_Q⇩1_bis - length t_Q⇩1) t_Q⇩2), S)› by simp
from setinterleaves⇩p⇩t⇩i⇩c⇩k_appendR[OF this] obtain u⇩1⇩1 u⇩1⇩2 t_P⇩1⇩1 t_P⇩1⇩2
where $$$$ : ‹u⇩1 = u⇩1⇩1 @ u⇩1⇩2› ‹?map_evt g t_P⇩1 = t_P⇩1⇩1 @ t_P⇩1⇩2›
‹u⇩1⇩1 setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P⇩1⇩1, ?map_evt h t_Q⇩1), S)› by blast
have ‹t_P⇩1⇩1 = ?map_evt g (take (length t_P⇩1⇩1) t_P⇩1)›
by (metis "$$$$"(2) append_eq_conv_conj take_map)
hence ‹u⇩1⇩1 setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙((take (length t_P⇩1⇩1) t_P⇩1, t_Q⇩1), S)›
by (metis "$$$$"(3) "***")
moreover have ‹take (length t_P⇩1⇩1) t_P⇩1 ∈ 𝒯 P›
by (metis "$$"(4) D_T append_take_drop_id is_processT3_TR_append)
ultimately show ‹t ∈ 𝒟 ?rhs›
by (simp add: tjoin_interpreted.D_Sync⇩p⇩t⇩i⇩c⇩k)
(metis (no_types, lifting) "$"(1,2,3) "$$"(8) "$$$"(1) "$$$$"(1)
append.assoc front_tickFree_append tickFree_append_iff)
qed
qed
next
fix t assume ‹t ∈ 𝒟 ?rhs›
then obtain u v t_P t_Q where $ : ‹t = u @ v› ‹tF u› ‹ftF v›
‹u setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((t_P, t_Q), S)›
‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
unfolding tjoin_interpreted.D_Sync⇩p⇩t⇩i⇩c⇩k by blast
from tickFree_setinterleaves⇩p⇩t⇩i⇩c⇩k_iff[THEN iffD1, OF "$"(4, 2)]
have ‹tF t_P› ‹tF t_Q› by simp_all
with "$"(5) have ‹?map_evt g t_P ∈ 𝒟 (?RT P g) ∧ ?map_evt h t_Q ∈ 𝒯 (?RT Q h) ∨
?map_evt g t_P ∈ 𝒯 (?RT P g) ∧ ?map_evt h t_Q ∈ 𝒟 (?RT Q h)›
by (simp add: Renaming_projs) (metis append.right_neutral front_tickFree_Nil)
moreover from "***"[THEN iffD2, OF "$"(4)]
have ‹u setinterleaves⇩✓⇘(⊗✓)⇙ ((?map_evt g t_P, ?map_evt h t_Q), S)› .
ultimately show ‹t ∈ 𝒟 ?lhs›
using "$"(1-3) by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
next
fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
then obtain t_P' X_P' t_Q' X_Q'
where $ : ‹(t_P', X_P') ∈ ℱ (?RT P g)› ‹(t_Q', X_Q') ∈ ℱ (?RT Q h)›
‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)› ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k (⊗✓) X_P' S X_Q'›
unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
from ‹t ∉ 𝒟 ?lhs› "$"(1, 2)[THEN F_T] "$"(3)
have ‹t_P' ∉ 𝒟 (?RT P g) ∧ t_Q' ∉ 𝒟 (?RT Q h)›
by (simp add: D_Sync⇩p⇩t⇩i⇩c⇩k') (metis append_self_conv front_tickFree_Nil)
with "$"(1, 2) obtain t_P t_Q
where $$ : ‹t_P' = ?map_evt g t_P› ‹(t_P, map_event⇩p⇩t⇩i⇩c⇩k id g -` X_P') ∈ ℱ P›
‹t_Q' = ?map_evt h t_Q› ‹(t_Q, map_event⇩p⇩t⇩i⇩c⇩k id h -` X_Q') ∈ ℱ Q›
unfolding Renaming_projs by blast
from "$"(3)[unfolded "$$"(1, 3), THEN "***"[THEN iffD1]]
have ‹t setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((t_P, t_Q), S)› .
moreover from "$"(4) inj_tick_join
have ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k (λr s. g r ⊗✓ h s)
(map_event⇩p⇩t⇩i⇩c⇩k id g -` X_P') S (map_event⇩p⇩t⇩i⇩c⇩k id h -` X_Q')›
by (simp add: super_ref_Sync⇩p⇩t⇩i⇩c⇩k_def, safe) blast
ultimately show ‹(t, X) ∈ ℱ ?rhs›
using "$$"(2, 4) by (auto simp add: tjoin_interpreted.F_Sync⇩p⇩t⇩i⇩c⇩k)
next
fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
then obtain t_P t_Q X_P X_Q
where $ : ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
‹t setinterleaves⇩✓⇘λr s. g r ⊗✓ h s⇙ ((t_P, t_Q), S)›
‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k (λr s. g r ⊗✓ h s) X_P S X_Q›
unfolding tjoin_interpreted.Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
from ‹t ∉ 𝒟 ?rhs› have ‹t_P ∉ 𝒟 P ∧ t_Q ∉ 𝒟 Q›
by (simp add: tjoin_interpreted.D_Sync⇩p⇩t⇩i⇩c⇩k')
(metis "$"(1-3) F_T append.right_neutral front_tickFree_Nil)
hence $$ : ‹t_P @ [✓(r)] ∈ 𝒯 P ⟹ r ∈ ❙✓❙s(P)›
‹t_Q @ [✓(s)] ∈ 𝒯 Q ⟹ s ∈ ❙✓❙s(Q)› for r s
by (meson is_processT9 strict_ticks_of_memI)+
have $$$ : ‹?map_evt g t_P @ [✓(g_r)] ∈ 𝒯 (?RT P g) ⟷ (∃r. g_r = g r ∧ t_P @ [✓(r)] ∈ 𝒯 P)› for g_r
proof (rule iffI)
from ‹t_P ∉ 𝒟 P ∧ t_Q ∉ 𝒟 Q› have ‹?map_evt g t_P ∉ 𝒟 (?RT P g)›
by (simp add: D_Renaming map_eq_append_conv "****")
(use is_processT7 map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree in blast)
hence ‹?map_evt g t_P @ [✓(g_r)] ∉ 𝒟 (?RT P g)› by (meson is_processT9)
moreover assume ‹?map_evt g t_P @ [✓(g_r)] ∈ 𝒯 (?RT P g)›
ultimately show ‹?map_evt g t_P @ [✓(g_r)] ∈ 𝒯 (?RT P g) ⟹ ∃r. g_r = g r ∧ t_P @ [✓(r)] ∈ 𝒯 P›
by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff "****")
next
show ‹∃r. g_r = g r ∧ t_P @ [✓(r)] ∈ 𝒯 P ⟹ ?map_evt g t_P @ [✓(g_r)] ∈ 𝒯 (?RT P g)›
by (auto simp add: T_Renaming)
qed
have $$$$ : ‹?map_evt h t_Q @ [✓(h_s)] ∈ 𝒯 (?RT Q h) ⟷ (∃s. h_s = h s ∧ t_Q @ [✓(s)] ∈ 𝒯 Q)› for h_s
proof (rule iffI)
from ‹t_P ∉ 𝒟 P ∧ t_Q ∉ 𝒟 Q› have ‹?map_evt h t_Q ∉ 𝒟 (?RT Q h)›
by (simp add: D_Renaming map_eq_append_conv "*****")
(use is_processT7 map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree in blast)
hence ‹?map_evt h t_Q @ [✓(h_s)] ∉ 𝒟 (?RT Q h)› by (meson is_processT9)
moreover assume ‹?map_evt h t_Q @ [✓(h_s)] ∈ 𝒯 (?RT Q h)›
ultimately show ‹?map_evt h t_Q @ [✓(h_s)] ∈ 𝒯 (?RT Q h) ⟹ ∃s. h_s = h s ∧ t_Q @ [✓(s)] ∈ 𝒯 Q›
by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff "*****")
next
show ‹∃s. h_s = h s ∧ t_Q @ [✓(s)] ∈ 𝒯 Q ⟹ ?map_evt h t_Q @ [✓(h_s)] ∈ 𝒯 (?RT Q h)›
by (auto simp add: T_Renaming)
qed
define X_P' where ‹X_P' ≡ map_event⇩p⇩t⇩i⇩c⇩k id g ` X_P ∪ {✓(g_r) |g_r. ?map_evt g t_P @ [✓(g_r)] ∉ 𝒯 (?RT P g)}›
define X_Q' where ‹X_Q' ≡ map_event⇩p⇩t⇩i⇩c⇩k id h ` X_Q ∪ {✓(h_s) |h_s. ?map_evt h t_Q @ [✓(h_s)] ∉ 𝒯 (?RT Q h)}›
have ‹map_event⇩p⇩t⇩i⇩c⇩k id g -` (map_event⇩p⇩t⇩i⇩c⇩k id g ` X_P) = X_P›
‹map_event⇩p⇩t⇩i⇩c⇩k id h -` (map_event⇩p⇩t⇩i⇩c⇩k id h ` X_Q) = X_Q›
by (simp_all add: set_eq_iff image_iff)
(metis event⇩p⇩t⇩i⇩c⇩k.inj_map injD inj_on_id ‹inj g›,
metis event⇩p⇩t⇩i⇩c⇩k.inj_map injD inj_on_id ‹inj h›)
with "$"(1, 2) have ‹(?map_evt g t_P, map_event⇩p⇩t⇩i⇩c⇩k id g ` X_P) ∈ ℱ (?RT P g)›
‹(?map_evt h t_Q, map_event⇩p⇩t⇩i⇩c⇩k id h ` X_Q) ∈ ℱ (?RT Q h)›
by (auto simp add: F_Renaming)
hence ‹(?map_evt g t_P, X_P') ∈ ℱ (?RT P g)›
‹(?map_evt h t_Q, X_Q') ∈ ℱ (?RT Q h)›
by (auto simp add: X_P'_def X_Q'_def intro: is_processT5 F_T)
moreover have ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((?map_evt g t_P, ?map_evt h t_Q), S)›
by (simp add: "$"(3) "***")
moreover have ‹e ∈ X ⟹ e ∈ super_ref_Sync⇩p⇩t⇩i⇩c⇩k (⊗✓) X_P' S X_Q'› for e
using "$"(4)[THEN set_mp, of e]
by (cases e,
simp_all add: X_P'_def X_Q'_def super_ref_Sync⇩p⇩t⇩i⇩c⇩k_def image_iff
ev_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff "$$$" "$$$$")
metis
ultimately show ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_Sync⇩p⇩t⇩i⇩c⇩k) blast
qed
qed
end