Theory CSP_Laws
section ‹ Powerful Laws of CSP ›
theory CSP_Laws
imports Basic_CSP_Laws Step_CSP_Laws_Extended
begin
subsection‹ Laws for Mndetprefix and Sync›
lemma Mndetprefix_Sync_Det_distr_FD :
‹(⊓ a ∈ A → (P a ⟦ C ⟧ (⊓ b ∈ B → Q b))) □
(⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧ Q b))
⊑⇩F⇩D (⊓ a ∈ A → P a) ⟦ C ⟧ (⊓ b ∈ B → Q b)›
(is ‹?lhs1 □ ?lhs2 ⊑⇩F⇩D ?rhs›)
if ‹A ≠ {}› ‹B ≠ {}› ‹A ∩ C = {}› ‹B ∩ C = {}›
proof -
have ‹?lhs1 = ⊓ b∈B. ⊓ a∈A. (a → (P a ⟦C⟧ (b → Q b)))› (is ‹_ = ?lhs1'›)
by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right
write0_def GlobalNdet_Mprefix_distr[OF ‹B ≠ {}›, symmetric])
(subst GlobalNdet_sets_commute, simp)
moreover have ‹?lhs2 = ⊓ b∈B. ⊓ a∈A. (b → (a → P a ⟦C⟧ Q b))› (is ‹_ = ?lhs2'›)
by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right
write0_def GlobalNdet_Mprefix_distr[OF ‹A ≠ {}›, symmetric])
ultimately have ‹?lhs1 □ ?lhs2 = ?lhs1' □ ?lhs2'› by simp
moreover have ‹?lhs1' □ ?lhs2' ⊑⇩F⇩D ⊓ b∈B. ⊓ a∈A. (a → (P a ⟦C⟧ (b → Q b)))
□ (b → ((a → P a) ⟦C⟧ Q b))›
by (auto simp add: ‹A ≠ {}› ‹B ≠ {}› refine_defs GlobalNdet_projs Det_projs write0_def)
moreover have ‹… = ⊓ b∈B. ⊓ a∈A. ((a → P a) ⟦C⟧ (b → Q b))›
by (rule mono_GlobalNdet_eq, rule mono_GlobalNdet_eq,
simp add: write0_def, subst Mprefix_Sync_Mprefix_indep)
(use ‹A ∩ C = {}› ‹B ∩ C = {}› in auto)
moreover have ‹… = ?rhs›
by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right)
ultimately show ‹?lhs1 □ ?lhs2 ⊑⇩F⇩D ?rhs› by argo
qed
lemmas Mndetprefix_Sync_Det_distr_F = Mndetprefix_Sync_Det_distr_FD[THEN leFD_imp_leF]
and Mndetprefix_Sync_Det_distr_D = Mndetprefix_Sync_Det_distr_FD[THEN leFD_imp_leD]
lemmas Mndetprefix_Sync_Det_distr_T = Mndetprefix_Sync_Det_distr_F[THEN leF_imp_leT]
lemma Mndetprefix_Sync_Det_distr_DT :
‹⟦A ≠ {}; B ≠ {}; A ∩ C = {}; B ∩ C = {}⟧ ⟹
(⊓ a ∈ A → (P a ⟦ C ⟧ (⊓ b ∈ B → Q b))) □
(⊓ b ∈ B → ((⊓ a ∈ A → P a) ⟦ C ⟧ Q b))
⊑⇩D⇩T (⊓ a ∈ A → P a) ⟦ C ⟧ (⊓ b ∈ B → Q b)›
by (simp add: Mndetprefix_Sync_Det_distr_D Mndetprefix_Sync_Det_distr_T leD_leT_imp_leDT)
subsection ‹Hiding Operator Laws›
theorem Hiding_Hiding_less_eq_process_Hiding_Un : ‹P \ A \ B ⊑⇩F⇩D P \ (A ∪ B)›
proof (rule failure_divergence_refine_optimizedI)
fix s assume ‹s ∈ 𝒟 (P \ (A ∪ B))›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` (A ∪ B)) @ u›
‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P (A ∪ B) ∧ t ∈ range f)›
unfolding D_Hiding by blast
have ** : ‹trace_hide t (ev ` (A ∪ B)) = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
using trace_hide_ev_union by blast
from "*"(4) show ‹s ∈ 𝒟 (P \ A \ B)›
proof (elim disjE exE)
assume ‹t ∈ 𝒟 P›
with mem_D_imp_mem_D_Hiding have ‹trace_hide t (ev ` A) ∈ 𝒟 (P \ A)› by blast
thus ‹s ∈ 𝒟 (P \ A \ B)›
by (subst D_Hiding) (use"*"(1, 2, 3) "**" Hiding_tickFree in blast)
next
fix f assume ** : ‹isInfHiddenRun f P (A ∪ B) ∧ t ∈ range f›
hence ‹strict_mono f› by simp
define ff where ‹ff i ≡ take (i + length (f 0)) (f i)› for i
have *** : ‹isInfHiddenRun ff P (A ∪ B) ∧ t ∈ range ff›
proof (intro conjI allI)
show ‹strict_mono ff›
proof (unfold strict_mono_Suc_iff, rule allI, unfold ff_def)
fix i nat
from length_strict_mono[of f ‹Suc i›, OF ‹strict_mono f›]
have $ : ‹take (i + length (f 0)) (f (Suc i)) < take ((Suc i) + length (f 0)) (f (Suc i))›
by (simp add: take_Suc_conv_app_nth)
from ‹strict_mono f›[THEN strict_monoD, of i ‹Suc i›, simplified]
obtain t where ‹f (Suc i) = f i @ t› by (meson strict_prefixE')
with length_strict_mono[of f i, OF ‹strict_mono f›]
have ‹take (i + length (f 0)) (f i) = take (i + length (f 0)) (f (Suc i))› by simp
with "$" show ‹take (i + length (f 0)) (f i) < take (Suc i + length (f 0)) (f (Suc i))› by simp
qed
next
show ‹ff i ∈ 𝒯 P› for i
by (unfold ff_def) (metis "**" prefixI append_take_drop_id is_processT3_TR)
next
show ‹trace_hide (ff i) (ev ` (A ∪ B)) = trace_hide (ff 0) (ev ` (A ∪ B))› for i
proof (rule order_antisym)
have ‹f 0 ≤ f i› by (simp add: "**" strict_mono_less_eq)
hence ‹f 0 ≤ take (i + length (f 0)) (f i)›
by (metis prefixE Prefix_Order.prefixI le_add2 take_all_iff take_append)
from mono_trace_hide[OF this]
show ‹trace_hide (ff 0) (ev ` (A ∪ B)) ≤ trace_hide (ff i) (ev ` (A ∪ B))›
by (unfold ff_def) (metis le_add2 take_all_iff)
next
have ‹take (i + length (f 0)) (f i) ≤ f i›
by (metis prefixI append_take_drop_id)
from mono_trace_hide[OF this]
show ‹trace_hide (ff i) (ev ` (A ∪ B)) ≤ trace_hide (ff 0) (ev ` (A ∪ B))›
by (unfold ff_def) (metis "**" le_add2 take_all_iff)
qed
next
from "**" obtain i where ‹t = f i› by blast
moreover have ‹f 0 ≤ f i› by (simp add: "**" strict_mono_less_eq)
ultimately have ‹t = ff (max i (length t - length (f 0)))›
by (simp add: ff_def max_def le_length_mono)
(metis "**" prefixE append_eq_conv_conj strict_mono_less_eq)
thus ‹t ∈ range ff› by blast
qed
show ‹s ∈ 𝒟 (P \ A \ B)›
proof (cases ‹∃m. ∀i>m. last (ff i) ∈ ev ` A›)
assume ‹∃m. ∀i>m. last (ff i) ∈ ev ` A›
then obtain m where $ : ‹m < i ⟹ last (ff i) ∈ ev ` A› for i by blast
hence ‹tF (ff m)›
by (metis "***" strict_prefixE' append_T_imp_tickFree list.distinct(1) strict_mono_Suc_iff)
have $$ : ‹∃t. ff (i + m) = ff m @ t ∧ set t ⊆ ev ` A› for i
proof (induct i)
show ‹∃t. ff (0 + m) = ff m @ t ∧ set t ⊆ ev ` A› by simp
next
fix i assume ‹∃t. ff (i + m) = ff m @ t ∧ set t ⊆ ev ` A›
then obtain t where ‹ff (i + m) = ff m @ t› ‹set t ⊆ ev ` A› by blast
obtain r where ‹ff (Suc i + m) = ff (i + m) @ r›
by (metis "***" strict_prefixE' add_Suc strict_mono_Suc_iff)
moreover have ‹length (ff (Suc i + m)) = Suc (length (ff (i + m)))›
by (simp add: ff_def) (metis "**" add_Suc length_strict_mono min_absorb2)
ultimately have ‹length r = 1› by (metis Suc_eq_plus1 add_left_cancel length_append)
with ‹ff (Suc i + m) = ff (i + m) @ r›
have ‹ff (Suc i + m) = ff (i + m) @ [last (ff (Suc i + m))]› by (cases r) simp_all
with ‹ff (i + m) = ff m @ t›
have ‹ff (Suc i + m) = ff m @ t @ [last (ff (Suc i + m))]› by simp
moreover have ‹last (ff (Suc i + m)) ∈ ev ` A› by (simp add: "$")
ultimately show ‹∃t. ff (Suc i + m) = ff m @ t ∧ set t ⊆ ev ` A›
by (intro exI[of _ ‹t @ [last (ff (Suc i + m))]›]) (simp add: ‹set t ⊆ ev ` A›)
qed
then obtain fff where $$$$ : ‹ff (i + m) = ff m @ fff i› ‹set (fff i) ⊆ ev ` A› for i by metis
show ‹s ∈ 𝒟 (P \ A \ B)›
apply (simp add: D_Hiding)
apply (rule exI[of _ ‹trace_hide (ff m) (ev ` A)›], rule exI[of _ u], intro conjI)
subgoal by (fact ‹ftF u›)
subgoal using Hiding_tickFree ‹tF (ff m)› by blast
subgoal by (metis (no_types) "*"(3) "***" rangeE trace_hide_ev_union)
apply (rule disjI1)
apply (rule exI[of _ ‹ff m›], rule exI[of _ ‹[]›], simp add: ‹tF (ff m)›)
apply (rule disjI2)
apply (rule exI[of _ ‹λi. ff (i + m)›], intro conjI)
subgoal by (metis (mono_tags, lifting) "***" add_Suc strict_mono_Suc_iff)
subgoal using "***" by blast
subgoal using "$$$$" by (simp add: subset_iff)
by (metis (mono_tags) add_0 rangeI)
next
assume ‹∄m. ∀i>m. last (ff i) ∈ ev ` A›
{ fix i :: nat assume ‹0 < i›
from "***" obtain t where ‹ff i = ff 0 @ t› ‹set t ⊆ ev ` (A ∪ B)›
unfolding isInfHiddenRun_1 by blast
with ‹0 < i› have ‹last (ff i) ∈ ev ` (A ∪ B)›
by (cases t) (auto simp add: "***" strict_mono_eq)
}
with ‹∄m. ∀i>m. last (ff i) ∈ ev ` A› have $ : ‹∀i. ∃j>i. last(ff j) ∈ ev ` B - ev ` A›
by (metis Un_Diff_cancel2 Un_iff gr0I image_Un not_less0)
define fff where ‹fff = rec_nat t (λi t. ff (SOME j. t < ff j ∧ last (ff j) ∈ ev ` B - ev ` A))›
hence ‹fff i ∈ range ff› for i
unfolding fff_def
by (metis (mono_tags, lifting) "***" gr0_conv_Suc nat.rec(2)
old.nat.simps(6) rangeI zero_less_iff_neq_zero)
have $$$ : ‹strict_mono (λi. trace_hide (fff i) (ev ` A))›
proof (unfold strict_mono_Suc_iff, rule allI)
fix i
have "£" : ‹fff (Suc i) = ff (SOME j. fff i < ff j ∧ last (ff j) ∈ ev ` B - ev ` A)›
by (simp add: fff_def)
from ‹⋀i. fff i ∈ range ff› obtain j where ‹fff i = ff j› by blast
hence ‹∃j. fff i < ff j ∧ last (ff j) ∈ ev ` B - ev ` A› by (metis "$" "***" monotoneD)
hence "££" : ‹fff i < fff (Suc i) ∧ last (fff (Suc i)) ∉ ev ` A›
by (metis (no_types, lifting) Diff_iff "£" someI_ex)
then obtain r where ‹fff (Suc i) = fff i @ r› ‹last r ∉ ev ` A›
by (metis append_self_conv last_append less_eq_list_def prefix_def less_list_def)
thus ‹trace_hide (fff i) (ev ` A) < trace_hide (fff (Suc i)) (ev ` A)›
by (metis (mono_tags, lifting) prefixI "££" empty_filter_conv
filter_append last_in_set nless_le self_append_conv)
qed
show ‹s ∈ 𝒟 (P \ A \ B)›
apply (simp add: D_Hiding)
apply (rule exI[of _ ‹trace_hide t (ev ` A)›], rule exI[of _ u], intro conjI)
subgoal by (fact ‹ftF u›)
subgoal using Hiding_tickFree ‹tF t› by blast
subgoal by (simp add: "*"(3))
apply (rule disjI2)
apply (rule exI[of _ ‹λi. trace_hide (fff i) (ev ` A)›], intro conjI)
subgoal by (fact "$$$")
subgoal by (metis "***" ‹⋀i. fff i ∈ range ff› mem_T_imp_mem_T_Hiding rangeE)
subgoal by (metis (no_types) "***" ‹⋀i. fff i ∈ range ff› rangeE trace_hide_ev_union)
by (metis (mono_tags, lifting) fff_def old.nat.simps(6) rangeI)
qed
qed
next
assume subset_div : ‹𝒟 (P \ (A ∪ B)) ⊆ 𝒟 (P \ A \ B)›
fix s X assume ‹(s, X) ∈ ℱ (P \ (A ∪ B))›
then consider ‹s ∈ 𝒟 (P \ (A ∪ B))›
| t where ‹s = trace_hide t (ev ` (A ∪ B))› ‹(t, X ∪ ev ` (A ∪ B)) ∈ ℱ P›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ ℱ (P \ A \ B)›
proof cases
from subset_div D_F show ‹s ∈ 𝒟 (P \ (A ∪ B)) ⟹ (s, X) ∈ ℱ (P \ A \ B)› by blast
next
fix t assume ‹s = trace_hide t (ev ` (A ∪ B))› ‹(t, X ∪ ev ` (A ∪ B)) ∈ ℱ P›
hence * : ‹s = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
‹(t, X ∪ ev ` B ∪ ev ` A) ∈ ℱ P›
by (simp_all add: image_Un sup_commute sup_left_commute)
show ‹(s, X) ∈ ℱ (P \ A \ B)›
by (simp add: F_Hiding) (use "*" in blast)
qed
qed
theorem Hiding_Un : ‹P \ (A ∪ B) = P \ A \ B›
if ‹finite A› for P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (rule order_antisym)
show ‹P \ (A ∪ B) ≤ P \ A \ B›
proof (rule failure_divergence_refine_optimizedI)
fix s assume ‹s ∈ 𝒟 (P \ A \ B)›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` B) @ u›
‹t ∈ 𝒟 (P \ A) ∨ (∃x. isInfHidden_seqRun_strong x (P \ A) B t)›
by (elim D_Hiding_seqRunE)
from "*"(4) show ‹s ∈ 𝒟 (P \ (A ∪ B))›
proof (elim disjE exE)
assume ‹t ∈ 𝒟 (P \ A)›
then obtain t' u'
where ** : ‹ftF u'› ‹tF t'› ‹t = trace_hide t' (ev ` A) @ u'›
‹t' ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun_strong x P A t')›
by (elim D_Hiding_seqRunE)
from "*"(1, 2) "**"(3) have *** : ‹ftF (trace_hide u' (ev ` B) @ u)›
using Hiding_tickFree front_tickFree_append tickFree_append_iff by blast
show ‹s ∈ 𝒟 (P \ (A ∪ B))›
apply (unfold D_Hiding_seqRun, clarify)
apply (rule exI[of _ t'], rule exI[of _ ‹trace_hide u' (ev ` B) @ u›])
apply (intro conjI)
subgoal by (fact "***")
subgoal by (fact "**"(2))
subgoal by (simp add: "*"(3) "**"(3))
by (metis "**"(4) Un_iff image_Un)
next
fix x assume ** : ‹isInfHidden_seqRun_strong x (P \ A) B t›
have trH_x : ‹trace_hide (seqRun t x i) (ev ` B) = trace_hide t (ev ` B)› for i
using "**" trace_hide_seqRun_eq_iff by blast
from "**" have ‹∀i. seqRun t x i ∈ {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ ℱ P}›
unfolding T_Hiding D_Hiding by blast
with F_T have ‹∀i. ∃w. seqRun t x i = trace_hide w (ev ` A) ∧ w ∈ 𝒯 P› by blast
then obtain f where *** : ‹seqRun t x i = trace_hide (f i) (ev ` A)› ‹f i ∈ 𝒯 P› for i by metis
have ‹inj f› by (rule injI) (metis "***"(1) seqRun_eq_iff)
with finite_imageD have ‹infinite (range f)› by blast
have $ : ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› if ‹t' ∈ range f› for i t'
proof -
from ‹t' ∈ range f› obtain j where ‹t' = f j› ..
hence "£" : ‹seqRun t x j = trace_hide t' (ev ` A)› ‹t' ∈ 𝒯 P› by (simp_all add: "***")
consider ‹i ≤ j› | ‹j ≤ i› by linarith
thus ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A›
proof cases
assume ‹j ≤ i›
hence ‹seqRun t x j ≤ seqRun t x i› by simp
hence ‹set (seqRun t x j) ⊆ set (seqRun t x i)›
by (metis prefixE Un_iff set_append subsetI)
moreover have ‹set (take i t') ⊆ set (seqRun t x j) ∪ ev ` A›
by (rule subsetI, drule in_set_takeD) (simp add: "£"(1))
ultimately show ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› by blast
next
assume ‹i ≤ j›
hence ‹seqRun t x i ≤ seqRun t x j› by simp
hence ‹take i (seqRun t x j) ≤ seqRun t x i› by simp
have ‹seqRun t x j = trace_hide (take i t') (ev ` A) @ trace_hide (drop i t') (ev ` A)›
by (metis "£"(1) append_take_drop_id filter_append)
moreover have ‹length (trace_hide (take i t') (ev ` A)) ≤ i›
by (metis length_filter_le length_take min.bounded_iff)
ultimately have ‹trace_hide (take i t') (ev ` A) ≤ take i (seqRun t x j)› by simp
with ‹take i (seqRun t x j) ≤ seqRun t x i› obtain t''
where ‹seqRun t x i = trace_hide (take i t') (ev ` A) @ t''›
by (meson prefixE dual_order.trans)
thus ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› by (simp add: subsetI)
qed
qed
have ‹finite {take i w |w. w ∈ range f}› for i
proof (induct i)
show ‹finite {take 0 w |w. w ∈ range f}› by simp
next
fix i assume hyp : ‹finite {take i w |w. w ∈ range f}›
show ‹finite {take (Suc i) w |w. w ∈ range f}›
proof (rule finite_subset)
show ‹ {take (Suc i) w |w. w ∈ range f}
⊆ {take i w |w. w ∈ range f}
∪ (⋃e∈set (seqRun t x (Suc i)) ∪ ev ` A. {take i w @ [e] |w. w ∈ range f})›
(is ‹?lhs ⊆ {take i w |w. w ∈ range f} ∪ (⋃e∈?S1. ?S2 e)›)
proof (intro subsetI)
fix t' assume ‹t' ∈ ?lhs›
then obtain w where "£" : ‹t' = take (Suc i) w› ‹w ∈ range f› by blast
show ‹t' ∈ {take i w |w. w ∈ range f} ∪ (⋃e∈?S1. ?S2 e)›
proof (cases ‹i < length t'›)
assume ‹i < length t'›
with "£"(1) take_Suc_conv_app_nth
have ‹take (Suc i) t' = take i w @ [t' ! i]› by auto
moreover from "£" "$" ‹i < length t'› nth_mem have ‹t' ! i ∈ ?S1› by blast
ultimately have ‹t' ∈ (⋃e∈?S1. ?S2 e)›
by (intro UN_I[of ‹t' ! i›], simp_all)
(metis "£" less_not_refl min.absorb2 not_le_imp_less take_take)
thus ‹t' ∈ {take i w |w. w ∈ range f} ∪ (⋃e∈?S1. ?S2 e)› by simp
next
assume ‹¬ i < length t'›
hence ‹take (Suc i) t' = take i t'› by simp
with "£" show ‹t' ∈ {take i w |w. w ∈ range f} ∪ (⋃e∈?S1. ?S2 e)› by auto
qed
qed
next
show ‹finite ({take i w |w. w ∈ range f} ∪
(⋃e∈set (seqRun t x (Suc i)) ∪ ev ` A.
{take i w @ [e] |w. w ∈ range f}))›
proof (rule finite_UnI)
show ‹finite {take i w |w. w ∈ range f}› by (fact hyp)
next
show ‹finite (⋃e∈set (seqRun t x (Suc i)) ∪ ev ` A. {take i w @ [e] |w. w ∈ range f})›
proof (rule finite_UN_I)
show ‹finite (set (seqRun t x (Suc i)) ∪ ev ` A)›
by (simp add: ‹finite A›)
next
fix e assume ‹e ∈ set (seqRun t x (Suc i)) ∪ ev ` A›
have ‹ {take i w @ [e] |w. w ∈ range f}
= (λt'. t' @ [e]) ` {take i w |w. w ∈ range f}› by auto
also have ‹finite …› by (rule finite_imageI) (fact hyp)
finally show ‹finite {take i w @ [e] |w. w ∈ range f}› .
qed
qed
qed
qed
also have ‹{take i w |w. w ∈ range f} = {w. ∃t'∈range f. w = take i t'}› for i by auto
finally have ‹∀i. finite {w. ∃t'∈range f. w = take i t'}› ..
from KoenigLemma[OF ‹infinite (range f)› this]
obtain ff :: ‹nat ⇒ ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
where $$ : ‹strict_mono ff› ‹range ff ⊆ {t. ∃t'∈range f. t ≤ t'}› by blast
from "$$"(2) have $$$ : ‹∃t'. ff (Suc j) ≤ t' ∧ t' ∈ range f› for j by blast
hence ‹ftF (ff (Suc j))› for j
by (metis "***"(2) imageE is_processT2_TR is_processT3_TR)
hence ‹tF (ff j)› for j
using strict_monoD[OF "$$"(1), of j ‹Suc j›, simplified]
by (metis strict_prefixE' front_tickFree_append_iff list.distinct(1))
from "$$"(2) "***"(2) have ‹ff (j + i) ∈ 𝒯 P› for i j
by (simp add: subset_iff) (meson is_processT3_TR rangeI)
have $$$$ : ‹∃w. trace_hide (ff i) (ev ` A) ≤ t @ w› for i
proof -
from "$$"(2) obtain j where ‹ff i ≤ f j› by auto
moreover from "**" isInfHiddenRun_1 have ‹∃w. seqRun t x j = t @ w›
by (simp add: seqRun_def)
ultimately show ‹∃w. trace_hide (ff i) (ev ` A) ≤ t @ w›
by (metis "***"(1) mono_trace_hide)
qed
have ‹∃i. t ≤ trace_hide (ff i) (ev ` A)›
proof (rule ccontr)
define fff where ‹fff i ≡ trace_hide (ff i) (ev ` A)› for i
assume assm : ‹∄i. t ≤ fff i›
moreover from "$$$$" have ‹∀i. ∃w. fff i ≤ t @ w› unfolding fff_def ..
ultimately have assm_bis : ‹∀i. fff i ≤ t›
by (metis prefixI le_same_imp_eq_or_less order.order_iff_strict)
have ‹mono fff›
by (rule monoI, simp add: fff_def)
(metis "$$"(1) prefixE prefixI filter_append strict_mono_less_eq)
from mono_constant[OF this assm_bis]
obtain j where ‹j ≤ i ⟹ fff i = fff j› for i by blast
have ‹fff j ∈ 𝒟 (P \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹ff j›], rule exI[of _ ‹[]›])
apply (simp add: fff_def ‹tF (ff j)›)
apply (rule disjI2)
apply (rule exI[of _ ‹λi. ff (j + i)›])
apply (intro conjI)
subgoal by (simp add: "$$"(1) strict_monoI strict_mono_less)
subgoal by (simp add: ‹⋀i. ff (j + i) ∈ 𝒯 P›)
subgoal by (metis ‹⋀i. j ≤ i ⟹ fff i = fff j› fff_def le_add1)
subgoal by (metis Nat.add_0_right rangeI) .
thus False
by (metis (no_types) "**" prefixE T_imp_front_tickFree append.right_neutral assm_bis
front_tickFree_append_iff is_processT3_TR is_processT7 t_le_seqRun)
qed
then obtain j where ‹t ≤ trace_hide (ff j) (ev ` A)› ..
have "£" : ‹s = trace_hide (ff j) (ev ` (A ∪ B)) @ u›
proof (unfold "*"(3), rule arg_cong[where f = ‹λx. x @ _›])
from "$$"(1) "$$$" obtain l where ‹ff j ≤ f l›
by (metis dual_order.trans order_less_imp_le rangeE strict_mono_Suc_iff)
from mono_trace_hide[OF this] have ‹trace_hide (ff j) (ev ` A) ≤ seqRun t x l›
unfolding "***"(1) by presburger
with mono_trace_hide[OF this] mono_trace_hide[OF ‹t ≤ trace_hide (ff j) (ev ` A)›]
show ‹trace_hide t (ev ` B) = trace_hide (ff j) (ev ` (A ∪ B))›
by (metis trH_x dual_order.eq_iff trace_hide_ev_union)
qed
have "££" : ‹trace_hide (ff (j + i)) (ev ` (A ∪ B)) = trace_hide (ff (j + 0)) (ev ` (A ∪ B))› for i
proof -
from "$$"(1) "$$$" obtain l where ‹ff (j + i) ≤ f l›
by (metis dual_order.trans order_less_imp_le rangeE strict_mono_Suc_iff)
from mono_trace_hide[OF this] have ‹trace_hide (ff (j + i)) (ev ` A) ≤ seqRun t x l›
unfolding "***"(1) by presburger
from mono_trace_hide[OF this, of B]
mono_trace_hide[THEN mono_trace_hide, of _ _ B A,
OF ‹strict_mono ff›[THEN strict_mono_mono, THEN monoD, of j ‹j + i›, simplified]]
mono_trace_hide[OF ‹t ≤ trace_hide (ff j) (ev ` A)›, of B]
show ‹trace_hide (ff (j + i)) (ev ` (A ∪ B)) =
trace_hide (ff (j + 0)) (ev ` (A ∪ B))› by (simp add: trH_x)
qed
show ‹s ∈ 𝒟 (P \ (A ∪ B))›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹ff j›], rule exI[of _ u])
apply (intro conjI)
subgoal by (fact ‹ftF u›)
subgoal by (fact ‹tF (ff j)›)
subgoal by (fact "£")
apply (rule disjI2)
apply (rule exI[of _ ‹λi. ff (j + i)›])
apply (intro conjI)
subgoal by (simp add: "$$"(1) strict_monoI strict_mono_less)
subgoal by (simp add: ‹⋀i. ff (j + i) ∈ 𝒯 P›)
subgoal by (use "££" in blast)
by (metis Nat.add_0_right rangeI)
qed
next
assume subset_div : ‹𝒟 (P \ A \ B) ⊆ 𝒟 (P \ (A ∪ B))›
fix s X assume ‹(s, X) ∈ ℱ (P \ A \ B)›
from this[simplified F_Hiding[of ‹P \ A› B]] D_Hiding[of ‹P \ A› B]
consider ‹s ∈ 𝒟 (P \ A \ B)›
| t where ‹s = trace_hide t (ev ` B)› ‹(t, X ∪ ev ` B) ∈ ℱ (P \ A)› by blast
thus ‹(s, X) ∈ ℱ (P \ (A ∪ B))›
proof cases
from subset_div D_F show ‹s ∈ 𝒟 (P \ A \ B) ⟹ (s, X) ∈ ℱ (P \ (A ∪ B))› by blast
next
fix t assume * : ‹s = trace_hide t (ev ` B)› ‹(t, X ∪ ev ` B) ∈ ℱ (P \ A)›
from "*"(2) consider ‹t ∈ 𝒟 (P \ A)›
| u where ‹t = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` B ∪ ev ` A) ∈ ℱ P›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ ℱ (P \ (A ∪ B))›
proof cases
assume ‹t ∈ 𝒟 (P \ A)›
with "*"(1) mem_D_imp_mem_D_Hiding have ‹s ∈ 𝒟 (P \ A \ B)› by fast
with subset_div D_F show ‹(s, X) ∈ ℱ (P \ (A ∪ B))› by blast
next
fix u assume ** : ‹t = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` B ∪ ev ` A) ∈ ℱ P›
from "*"(1) "**"(1) have ‹s = trace_hide u (ev ` (A ∪ B))› by simp
moreover from "**"(2) have ‹(u, X ∪ ev ` (A ∪ B)) ∈ ℱ P›
by (simp add: image_Un sup_commute sup_left_commute)
ultimately show ‹(s, X) ∈ ℱ (P \ (A ∪ B))› unfolding F_Hiding by blast
qed
qed
qed
next
show ‹P \ A \ B ≤ P \ (A ∪ B)› by (fact Hiding_Hiding_less_eq_process_Hiding_Un)
qed
subsection‹ Sync Operator Laws ›
subsubsection‹ Preliminaries ›
lemma tickFree_isInfHiddenRun : ‹tF s›
if ‹isInfHiddenRun f P A› and ‹s ∈ range f›
proof -
from ‹s ∈ range f› obtain i where ‹s = f i› ..
moreover have ‹f i < f (Suc i)› by (meson ‹isInfHiddenRun f P A› strict_mono_Suc_iff)
ultimately obtain t where ‹t ≠ []› ‹f (Suc i) = s @ t› by (meson strict_prefixE' list.discI)
moreover from ‹isInfHiddenRun f P A› is_processT2_TR
have ‹ftF (f (Suc i))› by blast
ultimately show ‹tF s› by (simp add: front_tickFree_append_iff)
qed
lemma Hiding_interleave:
‹r setinterleaves ((t, u), C) ⟹
(trace_hide r A) setinterleaves ((trace_hide t A, trace_hide u A), C)›
proof (induct ‹(t, C, u)› arbitrary: r t u rule: setinterleaving.induct)
case 1 thus ?case by simp
next
case (2 x t) thus ?case by auto
next
case (3 y u) thus ?case by auto
next
case (4 x t y u)
thus ?case
by (simp split: if_splits)
(safe, simp_all, (use SyncSingleHeadAdd setinterleaving_sym in blast)+)
qed
lemma non_Sync_interleaving:
‹(set t ∪ set u) ∩ C = {} ⟹ setinterleaving (t, C, u) ≠ {}›
by (induct ‹(t, C, u)› arbitrary: t u rule: setinterleaving.induct) simp_all
lemma interleave_Hiding:
‹s setinterleaves ((trace_hide t A, trace_hide u A), C)
⟹ ∃r. s = trace_hide r A ∧ r setinterleaves ((t, u), C)› if ‹A ∩ C = {}›
proof (induct ‹(t, C, u)› arbitrary: t u s rule: setinterleaving.induct)
case 1
thus ?case by simp
next
case (2 y u)
from "2.prems" ‹A ∩ C = {}› show ?case
by (simp add: disjoint_iff split: if_split_asm)
(metis "2.hyps" "2.prems" emptyLeftProperty filter.simps(1))+
next
case (3 x t)
from "3.prems" ‹A ∩ C = {}› show ?case
by (simp add: disjoint_iff split: if_split_asm)
(metis "3.hyps" "3.prems" emptyRightProperty filter.simps(1))+
next
case (4 x t y u)
from "4.prems" ‹A ∩ C = {}› show ?case
apply (cases ‹x = y›, simp_all add: disjoint_iff split: if_split_asm)
subgoal using "4.hyps"(1) by force
subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(4) filter.simps(2))
subgoal by (metis (no_types, lifting) "4.hyps"(3) filter.simps(2))
subgoal using "4.hyps"(2) by force
subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(4) filter.simps(2))
subgoal using "4.hyps"(5) by force
subgoal by (metis (no_types, lifting) "4.hyps"(2) "4.hyps"(4) filter.simps(2))
subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(5) filter.simps(2))
subgoal by (metis (no_types, lifting) "4.hyps"(4) filter.simps(2))
done
qed
lemma le_trace_hide : ‹u ≤ trace_hide t S ⟹ ∃u'. u = trace_hide u' S ∧ u' ≤ t›
proof (induct t arbitrary: u)
show ‹u ≤ trace_hide [] S ⟹ ∃u'. u = trace_hide u' S ∧ u' ≤ []› for u by simp
next
fix a t u assume prem: ‹u ≤ trace_hide (a # t) S›
assume hyp : ‹u ≤ trace_hide t S ⟹ ∃u'. u = trace_hide u' S ∧ u' ≤ t› for u
from prem consider ‹u = []› | ‹a ∈ S› ‹u ≤ trace_hide t S›
| v where ‹a ∉ S› ‹u = a # v› ‹v ≤ trace_hide t S›
by (cases u) (simp_all split: if_split_asm)
thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t›
proof cases
show ‹u = [] ⟹ ∃u'. u = trace_hide u' S ∧ u' ≤ a # t›
by (metis filter.simps(1) nil_le)
next
assume ‹a ∈ S› ‹u ≤ trace_hide t S›
from hyp[OF ‹u ≤ trace_hide t S›] obtain u' where ‹u = trace_hide u' S ∧ u' ≤ t› ..
with ‹a ∈ S› have ‹u = trace_hide (a # u') S ∧ a # u' ≤ a # t› by simp
thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t› ..
next
fix v assume ‹a ∉ S› ‹u = a # v› ‹v ≤ trace_hide t S›
from hyp[OF ‹v ≤ trace_hide t S›] obtain v' where ‹v = trace_hide v' S ∧ v' ≤ t› ..
with ‹a ∉ S› ‹u = a # v› have ‹u = trace_hide (a # v') S ∧ a # v' ≤ a # t› by simp
thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t› ..
qed
qed
lemma append_interleave :
‹s1 setinterleaves ((t1, u1), S) ⟹ s2 setinterleaves ((t2, u2), S) ⟹
(s1 @ s2) setinterleaves ((t1 @ t2, u1 @ u2), S)›
proof (induct ‹(t1, S, u1)› arbitrary: s1 t1 u1 rule: setinterleaving.induct)
case 1 thus ?case by simp
next
case (2 y u1)
thus ?case by (auto split: if_split_asm)
(use SyncSingleHeadAdd setinterleaving_sym in blast)
next
case (3 x t1)
thus ?case by (auto split: if_split_asm) (blast intro: SyncSingleHeadAdd)
next
case (4 x t2 y u2)
thus ?case by auto
qed
subsubsection ‹The Theorem: Sync and Hiding›
theorem Hiding_Sync : ‹(P ⟦S⟧ Q) \ A = (P \ A) ⟦S⟧ (Q \ A)›
if ‹finite A› and ‹A ∩ S = {}› for P Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (subst Process_eq_spec_optimized, safe)
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
fix s assume ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = ?trH_A t @ u›
‹t ∈ 𝒟 (P ⟦S⟧ Q) ∨ (∃x. isInfHidden_seqRun_strong x (P ⟦S⟧ Q) A t)›
by (elim D_Hiding_seqRunE)
from "*"(4) show ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
proof (elim disjE exE)
assume ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
then obtain t' u' r' v'
where ** : ‹ftF v'› ‹tF r' ∨ v' = []›
‹t = r' @ v'› ‹r' setinterleaves ((t', u'), ?tick_S)›
‹t' ∈ 𝒟 P ∧ u' ∈ 𝒯 Q ∨ t' ∈ 𝒟 Q ∧ u' ∈ 𝒯 P›
unfolding D_Sync by blast
{ fix t' u' and P Q
assume *** : ‹r' setinterleaves ((t', u'), ?tick_S)›
‹t' ∈ 𝒟 P› ‹u' ∈ 𝒯 Q›
have ‹?trH_A r' setinterleaves ((?trH_A t', ?trH_A u'), ?tick_S)›
using "***"(1) Hiding_interleave by blast
moreover from "***"(2) mem_D_imp_mem_D_Hiding have ‹?trH_A t' ∈ 𝒟 (P \ A)› by blast
moreover from "***"(3) mem_T_imp_mem_T_Hiding have ‹?trH_A u' ∈ 𝒯 (Q \ A)› by blast
ultimately have ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
apply (simp add: "*"(3) D_Sync)
apply (rule exI[of _ ‹?trH_A t'›], rule exI[of _ ‹?trH_A u'›],
rule exI[of _ ‹?trH_A r'›], rule exI[of _ ‹?trH_A v' @ u›])
apply (simp add: "*"(3) "**"(3) Hiding_tickFree)
using "*"(1, 2) "**"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff by blast
} note $ = this
from "**"(5) show ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
proof (elim disjE conjE)
show ‹t' ∈ 𝒟 P ⟹ u' ∈ 𝒯 Q ⟹ s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
by (metis "$" "**"(4))
show ‹t' ∈ 𝒟 Q ⟹ u' ∈ 𝒯 P ⟹ s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
by (metis "$" "**"(4) Sync_commute)
qed
next
fix x assume ** : ‹isInfHidden_seqRun_strong x (P ⟦S⟧ Q) A t›
from "**" have *** : ‹∃t' u'. t' ∈ 𝒯 P ∧ u' ∈ 𝒯 Q ∧
seqRun t x i setinterleaves ((t', u'), ?tick_S)› for i
unfolding T_Sync D_Sync by blast
define ftu where ‹ftu i ≡ SOME (t', u'). t' ∈ 𝒯 P ∧ u' ∈ 𝒯 Q ∧
seqRun t x i setinterleaves ((t', u'), ?tick_S)› for i
define ft fu where ‹ft ≡ λi. fst (ftu i)› and ‹fu ≡ λi. snd (ftu i)›
have **** : ‹ft i ∈ 𝒯 P› ‹fu i ∈ 𝒯 Q›
‹seqRun t x i setinterleaves ((ft i, fu i), ?tick_S)› for i
by (use "***"[of i] in ‹simp add: ft_def fu_def,
cases ‹ftu i›, simp add: ftu_def,
metis (mono_tags, lifting) case_prod_conv someI_ex›)+
from "**" have ‹set (seqRun t x i) ⊆ set t ∪ ev ` A› for i
by (auto simp add: seqRun_def)
have ‹set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A› for i
by (rule subset_trans[OF interleave_set[OF "****"(3)]])
(fact ‹set (seqRun t x i) ⊆ set t ∪ ev ` A›)
have ‹inj ftu›
proof (rule injI)
fix i j assume ‹ftu i = ftu j›
obtain t' u' where ‹(t', u') = ftu i› by (metis surj_pair)
with ‹ftu i = ftu j› have ‹seqRun t x i setinterleaves ((t', u'), ?tick_S)›
‹seqRun t x j setinterleaves ((t', u'), ?tick_S)›
by (metis "****"(3) fst_conv ft_def fu_def snd_conv)+
from interleave_eq_size[OF this] have ‹length (seqRun t x i) = length (seqRun t x j)› .
thus ‹i = j› by simp
qed
hence ‹infinite (range ftu)› using finite_imageD by blast
moreover have ‹range ftu ⊆ range ft × range fu›
by (clarify, metis fst_conv ft_def fu_def rangeI snd_conv)
ultimately have ‹infinite (range ft) ∨ infinite (range fu)›
by (meson finite_SigmaI infinite_super)
{ fix ft fu P Q
assume assms : ‹infinite (range ft)›
‹⋀i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
‹⋀i. ft i ∈ 𝒯 P› ‹⋀i. fu i ∈ 𝒯 Q›
‹⋀i. seqRun t x i setinterleaves ((ft i, fu i), ?tick_S)›
have ‹finite {t. ∃t'∈range ft. t = take i t'}› for i
proof (rule finite_subset)
show ‹ {w. ∃t'∈range ft. w = take i t'}
⊆ {w. set w ⊆ set t ∪ ev ` A ∧ length w ≤ i}›
by auto (meson Un_iff assms(2) in_set_takeD subsetD)
next
show ‹finite {w. set w ⊆ set t ∪ ev ` A ∧ length w ≤ i}›
by (rule finite_lists_length_le) (simp add: ‹finite A›)
qed
with assms(1) obtain ft' :: ‹nat ⇒ _›
where $ : ‹strict_mono ft'› ‹range ft' ⊆ {w. ∃t'∈range ft. w ≤ t'}›
using KoenigLemma by blast
from "$"(2) assms(3) is_processT3_TR have ‹range ft' ⊆ 𝒯 P› by blast
define ft'' where ‹ft'' i ≡ ft' (i + length t)› for i
from ‹range ft' ⊆ 𝒯 P› have ‹range ft'' ⊆ 𝒯 P› and ‹strict_mono ft''›
by (auto simp add: ft''_def "$"(1) strict_monoD strict_monoI)
have $$ : ‹?trH_A (ft'' i) = ?trH_A (ft'' 0)› for i
proof -
have ‹length t ≤ length (ft'' 0)›
by (metis "$"(1) add_0 add_leD1 ft''_def length_strict_mono)
obtain t' where ‹ft'' i = ft'' 0 @ t'›
by (meson prefixE ‹strict_mono ft''› strict_mono_less_eq zero_order(1))
moreover from "$"(2) obtain j where ‹ft'' i ≤ ft j› by (auto simp add: ft''_def)
ultimately obtain t'' where ‹ft j = ft'' 0 @ t' @ t''› by (metis prefixE append.assoc)
have ‹set (t' @ t'') ⊆ set (drop (length t) (seqRun t x j))›
proof (rule subset_trans)
show ‹set (t' @ t'') ⊆ set (drop (length (ft'' 0)) (seqRun t x j))›
by (rule interleave_order, fold ‹ft j = ft'' 0 @ t' @ t''›, fact assms(5))
next
show ‹set (drop (length (ft'' 0)) (seqRun t x j)) ⊆ set (drop (length t) (seqRun t x j))›
by (simp add: ‹length t ≤ length (ft'' 0)› set_drop_subset_set_drop)
qed
also from "**" have ‹set (drop (length t) (seqRun t x j)) ⊆ ev ` A›
by (auto simp add: seqRun_def)
finally show ‹?trH_A (ft'' i) = ?trH_A (ft'' 0)›
by (simp add: ‹ft'' i = ft'' 0 @ t'› subset_iff)
qed
from "$"(2) obtain i where ‹ft'' 0 ≤ ft i› by (auto simp add: ft''_def)
with prefixE obtain v where ‹ft i = ft'' 0 @ v› by blast
have ‹ftF u› by (fact "*"(1))
moreover have ‹tF (?trH_A (seqRun t x i)) ∨ u = []›
by (metis "*"(2) "**" Hiding_tickFree trace_hide_seqRun_eq_iff)
moreover have ‹s = ?trH_A (seqRun t x i) @ u›
by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
moreover have ‹?trH_A (seqRun t x i) setinterleaves ((?trH_A (ft i), ?trH_A (fu i)), ?tick_S)›
using assms(5) Hiding_interleave by blast
moreover have ‹?trH_A (ft i) ∈ 𝒟 (P \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹ft'' 0›])
apply (rule exI[of _ ‹?trH_A v›])
apply (intro conjI)
subgoal by (metis assms(3) Hiding_front_tickFree ‹ft i = ft'' 0 @ v›
front_tickFree_Nil front_tickFree_nonempty_append_imp is_processT2_TR)
subgoal by (metis strict_prefixE' T_imp_front_tickFree ‹range ft'' ⊆ 𝒯 P› ‹strict_mono ft''›
front_tickFree_append_iff list.distinct(1) range_subsetD strict_mono_Suc_iff)
subgoal by (simp add: ‹ft i = ft'' 0 @ v›)
subgoal using "$$" ‹range ft'' ⊆ 𝒯 P› ‹strict_mono ft''› by blast .
moreover have ‹?trH_A (fu i) ∈ 𝒯 (Q \ A)›
proof (cases ‹∃t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ ℱ Q›)
assume ‹∃t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ ℱ Q›
then obtain t' where ‹?trH_A (fu i) = ?trH_A t'› ‹(t', ev ` A) ∈ ℱ Q› by metis
thus ‹?trH_A (fu i) ∈ 𝒯 (Q \ A)› unfolding T_Hiding by blast
next
assume ‹∄t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ ℱ Q›
with assms(4) inf_hidden obtain fu' j
where $$$ : ‹isInfHiddenRun fu' Q A› ‹fu i = fu' j› by blast
show ‹?trH_A (fu i) ∈ 𝒯 (Q \ A)›
apply (unfold T_Hiding, simp)
apply (rule disjI2)
apply (rule exI[of _ ‹fu' j›], rule exI[of _ ‹[]›])
apply (intro conjI)
subgoal by simp
subgoal by (metis "$$$"(1) strict_prefixE' T_imp_front_tickFree neq_Nil_conv
front_tickFree_nonempty_append_imp strict_mono_Suc_iff)
subgoal by (simp add: "$$$"(2))
subgoal using "$$$"(1) by blast .
qed
ultimately have ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))› unfolding D_Sync by blast
} note $ = this
from ‹infinite (range ft) ∨ infinite (range fu)›
show ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
proof (elim disjE)
from "$" "****" ‹⋀i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
show ‹infinite (range ft) ⟹ s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))› by blast
next
from "$" "****" ‹⋀i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
show ‹infinite (range fu) ⟹ s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
by (metis Sync_commute setinterleaving_sym sup_commute)
qed
qed
next
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
assume same_div : ‹𝒟 (P ⟦S⟧ Q \ A) = 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
fix s X assume ‹(s, X) ∈ ℱ (P ⟦S⟧ Q \ A)›
then consider ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
| t where ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ ℱ (P ⟦S⟧ Q)›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
proof cases
from same_div D_F show ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A) ⟹ (s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))› by blast
next
fix t assume * : ‹s = ?trH_A t› ‹(t, X ∪ ev ` A) ∈ ℱ (P ⟦S⟧ Q)›
then consider ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
| (F) t_P X_P t_Q X_Q
where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
‹t setinterleaves ((t_P, t_Q), ?tick_S)›
‹X ∪ ev ` A = (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q›
by (auto simp add: F_Sync D_Sync)
thus ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
proof cases
assume ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
with "*"(1) mem_D_imp_mem_D_Hiding have ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)› by blast
with same_div D_F show ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))› by blast
next
case F
from inf_hidden[OF _ F(1)[THEN F_T], of A] inf_hidden[OF _ F(2)[THEN F_T], of A]
consider (D_P) f_P where ‹isInfHiddenRun f_P P A› ‹t_P ∈ range f_P›
| (D_Q) f_Q where ‹isInfHiddenRun f_Q Q A› ‹t_Q ∈ range f_Q›
| (F_both) t_P' t_Q'
where ‹?trH_A t_P' = ?trH_A t_P› ‹(t_P', ev ` A) ∈ ℱ P›
‹?trH_A t_Q' = ?trH_A t_Q› ‹(t_Q', ev ` A) ∈ ℱ Q›
by blast
thus ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
proof cases
case D_P
have $ : ‹?trH_A t_P ∈ 𝒟 (P \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹t_P›], rule exI[of _ ‹[]›])
using tickFree_isInfHiddenRun D_P front_tickFree_Nil by blast
from F(2) F_T mem_T_imp_mem_T_Hiding
have $$ : ‹?trH_A t_Q ∈ 𝒯 (Q \ A)› by blast
show ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
apply (simp add: F_Sync)
apply (rule disjI2)
apply (rule exI[of _ ‹?trH_A t_P›])
apply (rule exI[of _ ‹?trH_A t_Q›])
apply (rule exI[of _ ‹?trH_A t›], rule exI[of _ ‹[]›])
by (simp add: "*"(1) F(3) Hiding_interleave "$" "$$")
next
case D_Q
from F(1) F_T mem_T_imp_mem_T_Hiding
have $ : ‹?trH_A t_P∈ 𝒯 (P \ A)› by blast
have $$ : ‹?trH_A t_Q ∈ 𝒟 (Q \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹t_Q›], rule exI[of _ ‹[]›])
using tickFree_isInfHiddenRun D_Q front_tickFree_Nil by blast
show ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
apply (simp add: F_Sync)
apply (rule disjI2)
apply (rule exI[of _ ‹?trH_A t_Q›])
apply (rule exI[of _ ‹?trH_A t_P›])
apply (rule exI[of _ ‹?trH_A t›], rule exI[of _ ‹[]›])
by (simp add: "*"(1) F(3) Hiding_interleave setinterleaving_sym "$" "$$")
next
case F_both
from F(4) ‹A ∩ S = {}› have ‹ev ` A ⊆ X_P› and ‹ev ` A ⊆ X_Q› by auto
have ‹(?trH_A t_P, X_P) ∈ ℱ (P \ A)›
by (simp add: F_Hiding) (metis F(1) F_both(1) ‹ev ` A ⊆ X_P› sup.orderE)
moreover have ‹(?trH_A t_Q, X_Q) ∈ ℱ (Q \ A)›
by (simp add: F_Hiding) (metis F(2) F_both(3) ‹ev ` A ⊆ X_Q› sup.orderE)
moreover from F(3) Hiding_interleave
have ‹s setinterleaves ((?trH_A t_P, ?trH_A t_Q), ?tick_S)›
unfolding "*"(1) by blast
ultimately have ‹(s, (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
unfolding F_Sync by blast
moreover from F(4) have ‹X ⊆ (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q› by blast
ultimately show ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))› by (fact is_processT4)
qed
qed
qed
next
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
fix s assume ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
then obtain t_P t_Q r v
where * : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v› ‹r setinterleaves ((t_P, t_Q), ?tick_S)›
‹t_P ∈ 𝒟 (P \ A) ∧ t_Q ∈ 𝒯 (Q \ A) ∨ t_P ∈ 𝒟 (Q \ A) ∧ t_Q ∈ 𝒯 (P \ A)›
unfolding D_Sync by blast
from ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))› have ‹ftF s›
by (simp add: D_imp_front_tickFree)
{ fix t_P t_Q and P Q
assume ** : ‹r setinterleaves ((t_P, t_Q), ?tick_S)›
‹t_P ∈ 𝒟 (P \ A)› ‹t_Q ∈ 𝒯 (Q \ A)›
from **(2) obtain t u
where *** : ‹ftF u› ‹tF t› ‹t_P = ?trH_A t @ u›
‹t ∈ 𝒟 P ∨ (∃x. isInfHidden_seqRun_strong x P A t)›
by (elim D_Hiding_seqRunE)
from interleave_append_left[OF "**"(1)[unfolded "***"(3)]]
obtain t_Q1 t_Q2 r1 r2
where **** : ‹t_Q = t_Q1 @ t_Q2› ‹r = r1 @ r2›
‹r1 setinterleaves ((?trH_A t, t_Q1), ?tick_S)›
‹r2 setinterleaves ((u, t_Q2), ?tick_S)› by blast
from "**"(3) consider t_Q' where ‹t_Q = ?trH_A t_Q'› ‹(t_Q', ev ` A) ∈ ℱ Q›
| (D_Q) t' u' where ‹ftF u'› ‹tF t'› ‹t_Q = ?trH_A t' @ u'›
‹t' ∈ 𝒟 Q ∨ (∃y. isInfHidden_seqRun_strong y Q A t')›
by (elim T_Hiding_seqRunE)
hence ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof cases
fix t_Q' assume ‹t_Q = ?trH_A t_Q'› ‹(t_Q', ev ` A) ∈ ℱ Q›
from trace_hide_append[OF this(1)[unfolded "****"(1)]]
obtain t_Q1' t_Q2' where $ : ‹t_Q' = t_Q1' @ t_Q2'› ‹t_Q1 = ?trH_A t_Q1'›
‹t_Q2 = ?trH_A t_Q2'› by blast
from ‹A ∩ S = {}› have ‹ev ` A ∩ ?tick_S = {}› by blast
from interleave_Hiding[OF this "****"(3)[unfolded "$"(2)]]
obtain r1' where $$ : ‹r1 = ?trH_A r1'›
‹r1' setinterleaves ((t, t_Q1'), ?tick_S)› by blast
show ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof (rule D_Hiding_seqRunI)
show ‹ftF (r2 @ v)›
by (metis "*"(1, 3) "****"(2) ‹ftF s›
front_tickFree_append_iff tickFree_append_iff)
next
show ‹tF r1'›
by (metis "$"(1) "$$"(2) "***"(2) F_imp_front_tickFree SyncWithTick_imp_NTF
‹(t_Q', ev ` A) ∈ ℱ Q› front_tickFree_dw_closed nonTickFree_n_frontTickFree
non_tickFree_tick tickFree_append_iff ftf_Sync tickFree_imp_front_tickFree)
next
from "$$"(1) "*"(3) "****"(2) append.assoc
show ‹s = ?trH_A r1' @ r2 @ v› by blast
next
from "***"(4) show ‹r1' ∈ 𝒟 (P ⟦S⟧ Q) ∨
(∃x. ∀i. seqRun r1' x i ∈ 𝒯 (P ⟦S⟧ Q) ∧ x i ∈ ev ` A)›
proof (elim disjE exE)
assume ‹t ∈ 𝒟 P›
moreover have ‹t_Q1' ∈ 𝒯 Q›
by (metis "$"(1) F_T prefixI ‹(t_Q', ev ` A) ∈ ℱ Q› is_processT3_TR)
ultimately have ‹r1' ∈ 𝒟 (P ⟦S⟧ Q)›
unfolding D_Sync using "$$"(2) front_tickFree_Nil by blast
thus ‹r1' ∈ 𝒟 (P ⟦S⟧ Q) ∨ (∃x. isInfHidden_seqRun x (P ⟦S⟧ Q) A r1')› ..
next
fix x assume "£" : ‹isInfHidden_seqRun_strong x P A t›
from "£" ‹A ∩ S = {}› have ‹set (map x [0..<i]) ∩ ?tick_S = {}› for i
by (simp add: disjoint_iff image_iff)
(metis event⇩p⇩t⇩i⇩c⇩k.distinct(1) event⇩p⇩t⇩i⇩c⇩k.inject(1))
from "$$"(2)[THEN interleave_append_tail_left, OF this, folded seqRun_def]
have "££" : ‹seqRun r1' x i setinterleaves ((seqRun t x i, t_Q1'), ?tick_S)› for i .
have ‹isInfHidden_seqRun x (P ⟦S⟧ Q) A r1'›
proof (intro allI conjI)
have ‹t_Q1' ∈ 𝒯 Q›
by (metis "$"(1) F_T prefixI ‹(t_Q', ev ` A) ∈ ℱ Q› is_processT3_TR)
with "£" "££" show ‹seqRun r1' x i ∈ 𝒯 (P ⟦S⟧ Q)› for i
unfolding T_Sync by blast
next
show ‹x i ∈ ev ` A› for i by (simp add: "£")
qed
thus ‹r1' ∈ 𝒟 (P ⟦S⟧ Q) ∨ (∃x. isInfHidden_seqRun x (P ⟦S⟧ Q) A r1')› by blast
qed
qed
next
case D_Q
have ‹t ∈ 𝒯 P› using "***"(4) D_T by (metis seqRun_0)
consider ‹?trH_A t' ≤ t_Q1› | ‹t_Q1 ≤ ?trH_A t'›
by (metis "****"(1) D_Q(3) prefixI dual_order.eq_iff le_same_imp_eq_or_less nless_le)
thus ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof cases
assume ‹?trH_A t' ≤ t_Q1›
from interleave_le_right[OF "****"(3) this]
obtain r1_bis t_hidden_bis
where ‹r1_bis ≤ r1› ‹t_hidden_bis ≤ ?trH_A t›
‹r1_bis setinterleaves ((t_hidden_bis, ?trH_A t'), ?tick_S)› by blast
moreover from le_trace_hide[OF ‹t_hidden_bis ≤ ?trH_A t›]
obtain t_bis where ‹t_hidden_bis = ?trH_A t_bis ∧ t_bis ≤ t› ..
ultimately have $ : ‹r1_bis ≤ r1› ‹t_bis ≤ t›
‹r1_bis setinterleaves ((?trH_A t_bis, ?trH_A t'), ?tick_S)› by blast+
from interleave_Hiding[OF _ "$"(3)] ‹A ∩ S = {}›
obtain r1_bis_unhidden
where $$ : ‹r1_bis = ?trH_A r1_bis_unhidden›
‹r1_bis_unhidden setinterleaves ((t_bis, t'), ?tick_S)› by blast
from "$"(2) ‹t ∈ 𝒯 P› is_processT3_TR have ‹t_bis ∈ 𝒯 P› by blast
from D_Q(4) have ‹r1_bis ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof (elim disjE exE)
assume ‹t' ∈ 𝒟 Q›
with "$$"(2) ‹t_bis ∈ 𝒯 P› have ‹r1_bis_unhidden ∈ 𝒟 (P ⟦S⟧ Q)›
by (simp add: D_Sync)
(use front_tickFree_Nil setinterleaving_sym in blast)
with "$$"(1) mem_D_imp_mem_D_Hiding show ‹r1_bis ∈ 𝒟 (P ⟦S⟧ Q \ A)› by blast
next
fix y assume £ : ‹isInfHidden_seqRun_strong y Q A t'›
from "£" ‹A ∩ S = {}› have ‹set (map y [0..<i]) ∩ ?tick_S = {}› for i
by (simp add: disjoint_iff image_iff)
(metis event⇩p⇩t⇩i⇩c⇩k.distinct(1) event⇩p⇩t⇩i⇩c⇩k.inject(1))
from "$$"(2)[THEN interleave_append_tail_right, OF this, folded seqRun_def]
have $$$ : ‹seqRun r1_bis_unhidden y i setinterleaves ((t_bis, seqRun t' y i), ?tick_S)› for i .
have $$$$ : ‹isInfHidden_seqRun y (P ⟦S⟧ Q) A r1_bis_unhidden›
proof (intro allI conjI)
from "$$$" "£" ‹t_bis ∈ 𝒯 P›
show ‹seqRun r1_bis_unhidden y i ∈ 𝒯 (P ⟦S⟧ Q)› for i
unfolding T_Sync by blast
next
show ‹y i ∈ ev ` A› for i by (simp add: "£")
qed
show ‹r1_bis ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof (rule D_Hiding_seqRunI)
show ‹ftF []› by simp
next
show ‹tF r1_bis_unhidden›
by (metis "$$"(2) D_Q(2) SyncWithTick_imp_NTF T_imp_front_tickFree ‹t_bis ∈ 𝒯 P›
ftf_Sync nonTickFree_n_frontTickFree non_tickFree_tick
tickFree_append_iff tickFree_imp_front_tickFree)
next
show ‹r1_bis = ?trH_A r1_bis_unhidden @ []› by (simp add: $$(1))
next
from "$$$$" show ‹r1_bis_unhidden ∈ 𝒟 (P ⟦S⟧ Q) ∨
(∃x. isInfHidden_seqRun x (P ⟦S⟧ Q) A r1_bis_unhidden)› by blast
qed
qed
with "$"(1) show ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
unfolding less_eq_list_def prefix_def
by (metis (no_types, opaque_lifting) "*"(3) "****"(2) ‹ftF s›
append_Nil2 front_tickFree_append_iff front_tickFree_dw_closed is_processT7)
next
assume ‹t_Q1 ≤ ?trH_A t'›
from le_trace_hide[OF this] obtain t_Q1_unhidden
where $ : ‹t_Q1 = ?trH_A t_Q1_unhidden› ‹t_Q1_unhidden ≤ t'› by blast
from ‹A ∩ S = {}› have ‹ev ` A ∩ ?tick_S = {}› by blast
from "****"(3)[unfolded "$"(1)]
have ‹r1 setinterleaves ((?trH_A t, ?trH_A t_Q1_unhidden), ?tick_S)› .
from interleave_Hiding[OF ‹ev ` A ∩ ?tick_S = {}› this]
obtain r1_unhidden
where $$ : ‹r1 = ?trH_A r1_unhidden›
‹r1_unhidden setinterleaves ((t, t_Q1_unhidden), ?tick_S)› by blast
from ‹t_Q1_unhidden ≤ t'› have ‹t_Q1_unhidden ∈ 𝒯 Q›
by (metis D_Q(4) D_T is_processT3_TR t_le_seqRun)
from "***"(4) have ‹r1 ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof (elim disjE exE)
assume ‹t ∈ 𝒟 P›
have ‹r1_unhidden ∈ 𝒟 (P ⟦S⟧ Q)›
proof (unfold D_Sync, clarify, intro exI conjI)
show ‹ftF []› ‹tF r1_unhidden ∨ [] = []›
‹r1_unhidden = r1_unhidden @ []› by simp_all
next
show ‹r1_unhidden setinterleaves ((t, t_Q1_unhidden), ?tick_S)› by (fact "$$"(2))
next
show ‹t ∈ 𝒟 P ∧ t_Q1_unhidden ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ t_Q1_unhidden ∈ 𝒯 P›
by (simp add: ‹t ∈ 𝒟 P› ‹t_Q1_unhidden ∈ 𝒯 Q›)
qed
thus ‹r1 ∈ 𝒟 (P ⟦S⟧ Q \ A)› unfolding "$$"(1) by (fact mem_D_imp_mem_D_Hiding)
next
fix x assume £ : ‹isInfHidden_seqRun_strong x P A t›
from "£" ‹A ∩ S = {}› have ‹set (map x [0..<i]) ∩ ?tick_S = {}› for i
by (simp add: disjoint_iff image_iff)
(metis event⇩p⇩t⇩i⇩c⇩k.distinct(1) event⇩p⇩t⇩i⇩c⇩k.inject(1))
from "$$"(2)[THEN interleave_append_tail_left, OF this, folded seqRun_def]
have "££" : ‹seqRun r1_unhidden x i setinterleaves ((seqRun t x i, t_Q1_unhidden), ?tick_S)› for i .
have "£££" : ‹isInfHidden_seqRun x (P ⟦S⟧ Q) A r1_unhidden›
proof (intro allI conjI)
from "£" "££" ‹t_Q1_unhidden ∈ 𝒯 Q›
show ‹seqRun r1_unhidden x i ∈ 𝒯 (P ⟦S⟧ Q)› for i unfolding T_Sync by blast
next
from "£" show ‹x i ∈ ev ` A› for i by blast
qed
show ‹r1 ∈ 𝒟 (P ⟦S⟧ Q \ A)›
proof (unfold D_Hiding_seqRun, clarify, intro exI conjI)
show ‹ftF []› by simp
next
from isInfHidden_seqRun_imp_tickFree[OF "£££"] show ‹tF r1_unhidden› .
next
show ‹r1 = ?trH_A r1_unhidden @ []› by (simp add: "$$"(1))
next
from "£££" show ‹r1_unhidden ∈ 𝒟 (P ⟦S⟧ Q) ∨
(∃x. isInfHidden_seqRun x (P ⟦S⟧ Q) A r1_unhidden)› by blast
qed
qed
thus ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
by (metis "*"(3) "****"(2) ‹ftF s› append.right_neutral
front_tickFree_append_iff front_tickFree_dw_closed is_processT7)
qed
qed
} note $ = this
from "*"(5) show ‹s ∈ 𝒟 (P ⟦S⟧ Q \ A)›
by (elim disjE conjE) (metis "$" "*"(4), metis "$" "*"(4) Sync_commute)
next
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
assume same_div : ‹𝒟 (P ⟦S⟧ Q \ A) = 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
fix s X assume ‹(s, X) ∈ ℱ ((P \ A) ⟦S⟧ (Q \ A))›
then consider ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
| (F) s_P X_P s_Q X_Q
where ‹(s_P, X_P) ∈ ℱ (P \ A)› ‹(s_Q, X_Q) ∈ ℱ (Q \ A)›
‹s setinterleaves ((s_P, s_Q), ?tick_S)›
‹X = (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q›
unfolding F_Sync D_Sync by blast
thus ‹(s, X) ∈ ℱ (P ⟦S⟧ Q \ A)›
proof cases
from same_div D_F show ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A)) ⟹ (s, X) ∈ ℱ (P ⟦S⟧ Q \ A)› by blast
next
case F
from F(1, 2) consider ‹s_P ∈ 𝒟 (P \ A)› | ‹s_Q ∈ 𝒟 (Q \ A)›
| (F_both) s_P' s_Q'
where ‹s_P = ?trH_A s_P'› ‹(s_P', X_P ∪ ev ` A) ∈ ℱ P›
‹s_Q = ?trH_A s_Q'› ‹(s_Q', X_Q ∪ ev ` A) ∈ ℱ Q›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ ℱ (P ⟦S⟧ Q \ A)›
proof cases
assume ‹s_P ∈ 𝒟 (P \ A)›
moreover from F(2) F_T have ‹s_Q ∈ 𝒯 (Q \ A)› by blast
ultimately have ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
using F(3) front_tickFree_Nil unfolding D_Sync by blast
with same_div D_F show ‹(s, X) ∈ ℱ (P ⟦S⟧ Q \ A)› by blast
next
from F(1) F_T have ‹s_P ∈ 𝒯 (P \ A)› by blast
moreover assume ‹s_Q ∈ 𝒟 (Q \ A)›
moreover have ‹s setinterleaves ((s_Q, s_P), range tick ∪ ev ` S)›
by (simp add: F(3) setinterleaving_sym)
ultimately have ‹s ∈ 𝒟 ((P \ A) ⟦S⟧ (Q \ A))›
using front_tickFree_Nil unfolding D_Sync by blast
with same_div D_F show ‹(s, X) ∈ ℱ (P ⟦S⟧ Q \ A)› by blast
next
case F_both
from ‹A ∩ S = {}› have ‹ev ` A ∩ (range tick ∪ ev ` S) = {}› by blast
from interleave_Hiding[OF this F(3)[unfolded F_both(1, 3)]]
obtain s' where * : ‹s = ?trH_A s'›
‹s' setinterleaves ((s_P', s_Q'), range tick ∪ ev ` S)› by blast
have ‹X ∪ ev ` A = (X_P ∪ ev ` A ∪ (X_Q ∪ ev ` A)) ∩ (range tick ∪ ev ` S)
∪ (X_P ∪ ev ` A) ∩ (X_Q ∪ ev ` A)›
by (simp add: F(4) Un_Int_distrib2 Un_assoc sup_left_commute)
thus ‹(s, X) ∈ ℱ (P ⟦S⟧ Q \ A)›
by (simp add: "*"(1) F_Hiding F_Sync) (use "*"(2) F_both(2, 4) in blast)
qed
qed
qed
subsection ‹Renaming Operator Laws›
lemma Renaming_Ndet: ‹Renaming (P ⊓ Q) f g = Renaming P f g ⊓ Renaming Q f g›
by (subst Process_eq_spec) (auto simp add: F_Renaming D_Renaming F_Ndet D_Ndet)
lemma Renaming_Det: ‹Renaming (P □ Q) f g = Renaming P f g □ Renaming Q f g›
proof (subst Process_eq_spec, safe)
show ‹(s, X) ∈ ℱ (Renaming (P □ Q) f g) ⟹
(s, X) ∈ ℱ (Renaming P f g □ Renaming Q f g)› for s X
by (cases s) (auto simp add: F_Renaming F_Det D_Renaming D_Det T_Renaming)+
next
fix s X assume ‹(s, X) ∈ ℱ (Renaming P f g □ Renaming Q f g)›
then consider ‹s = []› ‹(s, X) ∈ ℱ (Renaming P f g)› ‹(s, X) ∈ ℱ (Renaming Q f g)›
| e s' where ‹s = e # s'› ‹(s, X) ∈ ℱ (Renaming P f g) ∨ (s, X) ∈ ℱ (Renaming Q f g)›
| ‹s = []› ‹s ∈ 𝒟 (Renaming P f g) ∨ s ∈ 𝒟 (Renaming Q f g)›
| r where ‹s = []› ‹✓(r) ∉ X› ‹([✓(r)] ∈ 𝒯 (Renaming P f g) ∨ [✓(r)] ∈ 𝒯 (Renaming Q f g))›
by (cases s) (auto simp add: F_Det)
thus ‹(s, X) ∈ ℱ (Renaming (P □ Q) f g)›
proof cases
show ‹⟦s = []; (s, X) ∈ ℱ (Renaming P f g); (s, X) ∈ ℱ (Renaming Q f g)⟧
⟹ (s, X) ∈ ℱ (Renaming (P □ Q) f g)›
by (auto simp add: F_Renaming F_Det)
next
show ‹s = e # s' ⟹ (s, X) ∈ ℱ (Renaming P f g) ∨ (s, X) ∈ ℱ (Renaming Q f g)
⟹ (s, X) ∈ ℱ (Renaming (P □ Q) f g)› for s' e
by (simp add: F_Renaming F_Det D_Det, safe)
(metis list.distinct(1) list.simps(9), presburger)+
next
show ‹s = [] ⟹ s ∈ 𝒟 (Renaming P f g) ∨ s ∈ 𝒟 (Renaming Q f g)
⟹ (s, X) ∈ ℱ (Renaming (P □ Q) f g)›
by (simp add: D_Renaming F_Renaming D_Det)
next
show ‹⟦s = []; ✓(r) ∉ X; [✓(r)] ∈ 𝒯 (Renaming P f g) ∨ [✓(r)] ∈ 𝒯 (Renaming Q f g)⟧
⟹ (s, X) ∈ ℱ (Renaming (P □ Q) f g)› for r
by (auto simp add: T_Renaming F_Renaming D_Det F_Det
dest: map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff[THEN iffD1, OF sym, of r])
(metis append_eq_Cons_conv list.map_disc_iff map_event⇩p⇩t⇩i⇩c⇩k_tickFree
non_tickFree_tick tickFree_Nil tickFree_append_iff)+
qed
next
show ‹s ∈ 𝒟 (Renaming (P □ Q) f g) ⟹ s ∈ 𝒟 (Renaming P f g □ Renaming Q f g)›
and ‹s ∈ 𝒟 (Renaming P f g □ Renaming Q f g) ⟹ s ∈ 𝒟 (Renaming (P □ Q) f g)› for s
by (auto simp add: D_Renaming D_Det)
qed
lemma Sliding_STOP_Det [simp] : ‹(P ⊳ STOP) □ Q = P ⊳ Q›
by (simp add: Det_commute Det_distrib_Ndet_left Sliding_def)
lemma Sliding_Det: ‹(P ⊳ P') □ Q = P ⊳ P' □ Q›
by (metis Det_assoc Sliding_STOP_Det)
lemma Renaming_Sliding:
‹Renaming (P ⊳ Q) f g = Renaming P f g ⊳ Renaming Q f g›
by (simp add: Renaming_Det Renaming_Ndet Sliding_def)
lemma Renaming_Mprefix_image:
‹Renaming (□ a ∈ A → P (f a)) f g =
□ b ∈ f ` A → Renaming (P b) f g› (is ‹?lhs = ?rhs›)
by (subst Renaming_Mprefix, rule mono_Mprefix_eq)
(simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Renaming D_Renaming, safe, auto)
lemma Renaming_Mprefix_image_inj_on:
‹Renaming (Mprefix A P) f g = □ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
if inj_on_f: ‹inj_on f A›
apply (subst Renaming_Mprefix_image[symmetric])
apply (intro arg_cong[where f = ‹λQ. Renaming Q f g›] mono_Mprefix_eq)
by (metis that the_inv_into_def the_inv_into_f_f)
corollary Renaming_Mprefix_image_inj:
‹Renaming (Mprefix A P) f g = □ b ∈ f ` A → Renaming (P (THE a. f a = b)) f g› if inj_f: ‹inj f›
apply (subst Renaming_Mprefix_image_inj_on, metis inj_eq inj_onI that)
apply (rule mono_Mprefix_eq[rule_format])
by (metis imageE inj_eq[OF inj_f])
lemma Renaming_Mndetprefix_image: ‹Renaming (⊓ a ∈ A → P (f a)) f g = ⊓ b ∈ f ` A → Renaming (P b) f g›
by (auto simp add: Mndetprefix_GlobalNdet Renaming_distrib_GlobalNdet write0_def Renaming_Mprefix
intro!: mono_Mprefix_eq mono_GlobalNdet_eq2 intro: sym)
corollary Renaming_Mndetprefix_inj_on:
‹Renaming (Mndetprefix A P) f g = ⊓ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
if inj_on_f: ‹inj_on f A›
apply (subst Renaming_Mndetprefix_image[symmetric])
apply (intro arg_cong[where f = ‹λQ. Renaming Q f g›] mono_Mndetprefix_eq)
by (metis that the_inv_into_def the_inv_into_f_f)
corollary Renaming_Mndetprefix_inj:
‹Renaming (Mndetprefix A P) f g = ⊓ b ∈ f ` A → Renaming (P (THE a. f a = b)) f g›
if inj_f: ‹inj f›
apply (subst Renaming_Mndetprefix_inj_on, metis inj_eq inj_onI that)
apply (rule mono_Mndetprefix_eq[rule_format])
by (metis imageE inj_eq[OF inj_f])
lemma Hiding_distrib_FD_GlobalNdet :
‹(⊓a ∈ A. P a) \ S ⊑⇩F⇩D ⊓a ∈ A. (P a \ S)› (is ‹?lhs ⊑⇩F⇩D ?rhs›)
proof (cases ‹A = {}›)
show ‹A = {} ⟹ ?lhs ⊑⇩F⇩D ?rhs› by simp
next
show ‹?lhs ⊑⇩F⇩D ?rhs› if ‹A ≠ {}›
proof (rule failure_divergence_refine_optimizedI)
show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
by (simp add: GlobalNdet_projs D_Hiding_seqRun) blast
next
assume subset_div : ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
fix s X assume ‹(s, X) ∈ ℱ ?rhs›
then obtain a where ‹a ∈ A› ‹(s, X) ∈ ℱ (P a \ S)›
by (auto simp add: F_GlobalNdet ‹A ≠ {}›)
from ‹(s, X) ∈ ℱ (P a \ S)› consider ‹s ∈ 𝒟 (P a \ S)›
| t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (P a)›
unfolding D_Hiding F_Hiding by blast
thus ‹(s, X) ∈ ℱ ?lhs›
proof cases
assume ‹s ∈ 𝒟 (P a \ S)›
with ‹a ∈ A› have ‹s ∈ 𝒟 ?rhs› by (auto simp add: D_GlobalNdet)
with subset_div D_F show ‹(s, X) ∈ ℱ ?lhs› by blast
next
from ‹a ∈ A› show ‹s = trace_hide t (ev ` S) ⟹ (t, X ∪ ev ` S) ∈ ℱ (P a)
⟹ (s, X) ∈ ℱ ?lhs› for t
by (simp add: F_Hiding_seqRun F_GlobalNdet) blast
qed
qed
qed
lemma Renaming_Seq :
‹Renaming (P ❙; Q) f g = Renaming P f g ❙; Renaming Q f g› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
fix t assume ‹t ∈ 𝒟 ?lhs›
then obtain u v where ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ v› ‹tF u› ‹ftF v› ‹u ∈ 𝒟 (P ❙; Q)›
unfolding D_Renaming by blast
from ‹u ∈ 𝒟 (P ❙; Q)› consider ‹u ∈ 𝒟 P›
| u1 u2 r where ‹u = u1 @ u2› ‹u1 @ [✓(r)] ∈ 𝒯 P› ‹u2 ∈ 𝒟 Q›
unfolding D_Seq by blast
thus ‹t ∈ 𝒟 ?rhs›
proof cases
from ‹ftF v› ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ v› ‹tF u›
show ‹u ∈ 𝒟 P ⟹ t ∈ 𝒟 ?rhs› by (auto simp add: D_Seq D_Renaming)
next
fix u1 u2 r assume ‹u = u1 @ u2› ‹u1 @ [✓(r)] ∈ 𝒯 P› ‹u2 ∈ 𝒟 Q›
from ‹u1 @ [✓(r)] ∈ 𝒯 P› have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
by (auto simp add: T_Renaming)
moreover from ‹u2 ∈ 𝒟 Q› ‹tF u› ‹u = u1 @ u2›
have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 ∈ 𝒟 (Renaming Q f g)›
by (simp add: D_Renaming) (use front_tickFree_Nil in blast)
ultimately have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u ∈ 𝒟 ?rhs› by (auto simp add: ‹u = u1 @ u2› D_Seq)
thus ‹t ∈ 𝒟 ?rhs› by (simp add: ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u @ v› ‹ftF v›
‹tF u› is_processT7 map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
qed
next
fix t assume ‹t ∈ 𝒟 ?rhs›
thm this[simplified D_Seq, simplified]
then consider ‹t ∈ 𝒟 (Renaming P f g)›
| t1 t2 s where ‹t = t1 @ t2› ‹t1 @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
‹t1 @ [✓(s)] ∉ 𝒟 (Renaming P f g)› ‹t2 ∈ 𝒟 (Renaming Q f g)›
by (simp add: D_Seq) (metis D_imp_front_tickFree append_T_imp_tickFree
is_processT7 is_processT9 list.distinct(1))
thus ‹t ∈ 𝒟 ?lhs›
proof cases
show ‹t ∈ 𝒟 (Renaming P f g) ⟹ t ∈ 𝒟 ?lhs›
by (auto simp add: D_Renaming D_Seq)
next
fix t1 t2 s assume ‹t = t1 @ t2› ‹t1 @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
‹t1 @ [✓(s)] ∉ 𝒟 (Renaming P f g)› ‹t2 ∈ 𝒟 (Renaming Q f g)›
from this(2, 3) obtain u1' where ‹t1 @ [✓(s)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1'› ‹u1' ∈ 𝒯 P›
by (auto simp add: Renaming_projs)
then obtain u1 r where ‹s = g r› ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 @ [✓(r)] ∈ 𝒯 P›
by (cases u1' rule: rev_cases) (auto simp add: tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)
from ‹t2 ∈ 𝒟 (Renaming Q f g)› obtain u2 u3
where ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ u3› ‹tF u2› ‹ftF u3› ‹u2 ∈ 𝒟 Q›
unfolding D_Renaming by blast
from ‹u1 @ [✓(r)] ∈ 𝒯 P› ‹u2 ∈ 𝒟 Q› have ‹u1 @ u2 ∈ 𝒟 (P ❙; Q)›
by (auto simp add: D_Seq)
with ‹ftF u3› ‹tF u2› ‹u1 @ [✓(r)] ∈ 𝒯 P› show ‹t ∈ 𝒟 ?lhs›
by (simp add: ‹t = t1 @ t2› ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1›
‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2 @ u3› D_Renaming)
(metis append_T_imp_tickFree append_eq_appendI map_append not_Cons_self tickFree_append_iff)
qed
next
fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
from ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs› 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 ❙; Q)›
unfolding Renaming_projs by blast
from ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P ❙; Q)› ‹t ∉ 𝒟 ?lhs›
consider ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ range tick) ∈ ℱ P› ‹tF u›
| u1 r u2 where ‹u = u1 @ u2› ‹u1 @ [✓(r)] ∈ 𝒯 P› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q›
by (auto simp add: ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› Seq_projs D_Renaming)
(metis D_imp_front_tickFree butlast_snoc front_tickFree_iff_tickFree_butlast front_tickFree_single
is_processT8 is_processT9 map_append map_event⇩p⇩t⇩i⇩c⇩k_front_tickFree nonTickFree_n_frontTickFree)
thus ‹(t, X) ∈ ℱ ?rhs›
proof cases
assume ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ range tick) ∈ ℱ P› ‹tF u›
have ‹map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` range tick ⊆ map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ range tick›
by (auto simp add: map_event⇩p⇩t⇩i⇩c⇩k_eq_tick_iff)
with ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ range tick) ∈ ℱ P›
have ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` range tick) ∈ ℱ P›
by (meson is_processT4)
with ‹tF u› show ‹(t, X) ∈ ℱ ?rhs›
by (auto simp add: F_Seq ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› F_Renaming map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
next
fix u1 u2 r assume ‹u = u1 @ u2› ‹u1 @ [✓(r)] ∈ 𝒯 P› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q›
from ‹u1 @ [✓(r)] ∈ 𝒯 P› have ‹map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1 @ [✓(g r)] ∈ 𝒯 (Renaming P f g)›
by (auto simp add: T_Renaming)
moreover from ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q›
have ‹(map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2, X) ∈ ℱ (Renaming Q f g)› by (auto simp add: F_Renaming)
ultimately show ‹(t, X) ∈ ℱ ?rhs›
by (auto simp add: ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› ‹u = u1 @ u2› F_Seq)
qed
next
fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs› ‹t ∉ 𝒟 ?lhs›
then consider ‹(t, X ∪ range tick) ∈ ℱ (Renaming P f g)› ‹tF t›
| t1 t2 s where ‹t = t1 @ t2› ‹t1 @ [✓(s)] ∈ 𝒯 (Renaming P f g)› ‹(t2, X) ∈ ℱ (Renaming Q f g)›
unfolding Seq_projs by blast
thus ‹(t, X) ∈ ℱ ?lhs›
proof cases
assume ‹(t, X ∪ range tick) ∈ ℱ (Renaming P f g)› ‹tF t›
with ‹t ∉ 𝒟 ?rhs› 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 ∪ map_event⇩p⇩t⇩i⇩c⇩k f g -` range tick) ∈ ℱ P›
by (auto simp add: D_Seq Renaming_projs)
from this(2) have ‹(u, map_event⇩p⇩t⇩i⇩c⇩k f g -` X ∪ range tick) ∈ ℱ P›
by (rule is_processT4) auto
with ‹tF t› show ‹(t, X) ∈ ℱ ?lhs›
by (auto simp add: F_Renaming F_Seq ‹t = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u› map_event⇩p⇩t⇩i⇩c⇩k_tickFree)
next
fix t1 t2 s assume ‹t = t1 @ t2› ‹t1 @ [✓(s)] ∈ 𝒯 (Renaming P f g)› ‹(t2, X) ∈ ℱ (Renaming Q f g)›
from ‹t ∉ 𝒟 ?rhs› have ‹t1 @ [✓(s)] ∉ 𝒟 (Renaming P f g)›
by (simp add: ‹t = t1 @ t2› D_Seq)
(metis D_imp_front_tickFree F_imp_front_tickFree ‹(t2, X) ∈ ℱ (Renaming Q f g)›
front_tickFree_append_iff is_processT7 is_processT9 not_Cons_self)
with ‹t1 @ [✓(s)] ∈ 𝒯 (Renaming P f g)› obtain u1'
where ‹t1 @ [✓(s)] = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1'› ‹u1' ∈ 𝒯 P›
unfolding Renaming_projs by blast
then obtain u1 r where ‹s = g r› ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1› ‹u1 @ [✓(r)] ∈ 𝒯 P›
by (cases u1' rule: rev_cases) (auto simp add: tick_eq_map_event⇩p⇩t⇩i⇩c⇩k_iff)
from ‹t ∉ 𝒟 ?rhs› ‹t1 @ [✓(s)] ∈ 𝒯 (Renaming P f g)› have ‹t2 ∉ 𝒟 (Renaming Q f g)›
by (auto simp add: ‹t = t1 @ t2› D_Seq)
with ‹(t2, X) ∈ ℱ (Renaming Q f g)› obtain u2
where ‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2› ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q›
unfolding Renaming_projs by blast
from ‹(u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ Q› ‹u1 @ [✓(r)] ∈ 𝒯 P›
have ‹(u1 @ u2, map_event⇩p⇩t⇩i⇩c⇩k f g -` X) ∈ ℱ (P ❙; Q)› by (auto simp add: F_Seq)
thus ‹(t, X) ∈ ℱ ?lhs›
by (auto simp add: ‹t = t1 @ t2› ‹t1 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u1›
‹t2 = map (map_event⇩p⇩t⇩i⇩c⇩k f g) u2› F_Renaming)
qed
qed
lemma Renaming_fix :
‹Renaming (μ X. φ X) f g = (μ X. ((λP. Renaming P f g) ∘ φ ∘ (λP. Renaming P (inv f) (inv g))) X)›
(is ‹Renaming (μ X. φ X) f g = (μ X. ?φ' X)›) if ‹cont φ›
and ‹bij f› and ‹bij g› for φ :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof -
have * : ‹φ = (λP. Renaming P (inv f) (inv g)) ∘ ?φ' ∘ (λP. Renaming P f g)›
by (rule ext) (simp add: Renaming_inv bij_is_inj ‹bij f› ‹bij g›)
have mono_φ : ‹P ⊑ Q ⟹ φ P ⊑ φ Q› for P Q
by (simp add: cont2monofunE ‹cont φ›)
have mono_φ' : ‹P ⊑ Q ⟹ ?φ' P ⊑ ?φ' Q› for P Q
by (simp add: mono_Renaming mono_φ)
have finitary_props : ‹finitary f› ‹finitary g› ‹finitary (inv f)› ‹finitary (inv g)›
by (simp_all add: bij_is_inj bij_is_surj surj_imp_inj_inv ‹bij f› ‹bij g›)
have ‹cont (λX. Renaming (φ X) f g)› by (simp add: finitary_props(1, 2) ‹cont φ›)
moreover have ‹cont (λX. Renaming X (inv f) (inv g))› by (simp add: finitary_props(3, 4))
ultimately have ‹cont ?φ'› unfolding comp_def by (rule cont_compose)
from ‹cont φ› ‹cont ?φ'› cont_process_rec
have ** : ‹(μ X. φ X) = φ (μ X. φ X)› ‹(μ X. ?φ' X) = ?φ' (μ X. ?φ' X)› by blast+
show ‹Renaming (μ X. φ X) f g = (μ X. ?φ' X)›
proof (rule below_antisym)
show ‹Renaming (μ X. φ X) f g ⊑ (μ X. ?φ' X)›
proof (induct rule: fix_ind[where F = ‹Λ X. φ X›])
show ‹adm (λa. Renaming a f g ⊑ (μ X. ?φ' X))›
by (simp add: ‹finitary f› ‹finitary g› monofunI)
next
show ‹Renaming ⊥ f g ⊑ (μ X. ?φ' X)› by simp
next
fix X assume ‹Renaming X f g ⊑ (μ X. ?φ' X)›
hence ‹?φ' (Renaming X f g) ⊑ ?φ' (μ X. ?φ' X)› by (fact mono_φ')
hence ‹Renaming (?φ' (Renaming X f g)) (inv f) (inv g) ⊑
Renaming (?φ' (μ X. ?φ' X)) (inv f) (inv g)› by (fact mono_Renaming)
also from "*" have ‹Renaming (?φ' (Renaming X f g)) (inv f) (inv g) = φ X›
unfolding comp_def by metis
also from "**"(2) have ‹?φ' (μ X. ?φ' X) = (μ X. ?φ' X)› by argo
finally have ‹Renaming (φ X) f g ⊑ Renaming (Renaming (μ X. ?φ' X) (inv f) (inv g)) f g›
by (fact mono_Renaming)
also have ‹… = (μ X. ?φ' X)› by (simp add: inv_Renaming ‹bij f› ‹bij g›)
finally show ‹Renaming ((Λ X. φ X)⋅X) f g ⊑ (μ X. ?φ' X)›
by (subst beta_cfun[OF ‹cont φ›]) (simp add: comp_def)
qed
next
show ‹(μ X. ?φ' X) ⊑ Renaming (μ X. φ X) f g›
proof (induct rule: fix_ind[where F = ‹Λ X. ?φ' X›])
show ‹adm (λa. a ⊑ Renaming (μ x. φ x) f g)› by (simp add: monofunI)
next
show ‹⊥ ⊑ Renaming (μ x. φ x) f g› by simp
next
fix X assume hyp : ‹X ⊑ Renaming (μ X. φ X) f g›
hence ‹Renaming X (inv f) (inv g) ⊑ Renaming (Renaming (μ X. φ X) f g) (inv f) (inv g)›
by (fact mono_Renaming)
also have ‹… = (μ X. φ X)› by (simp add: Renaming_inv bij_is_inj ‹bij f› ‹bij g›)
finally have ‹φ (Renaming X (inv f) (inv g)) ⊑ φ (μ X. φ X)› by (fact mono_φ)
hence ‹Renaming (φ (Renaming X (inv f) (inv g))) f g ⊑
Renaming (φ (μ x. φ x)) f g› by (fact mono_Renaming)
also from "**"(1) have ‹φ (μ x. φ x) = (μ X. φ X)› by presburger
finally show ‹(Λ X. ?φ' X)⋅X ⊑ Renaming (μ X. φ X) f g›
by (subst beta_cfun[OF ‹cont ?φ'›]) (simp add: comp_def)
qed
qed
qed
end