Theory CSP_Laws
chapter‹ The "Laws" of CSP ›
theory CSP_Laws
imports Bot Skip Stop Det Ndet Mprefix Mndetprefix Seq Hiding Sync Renaming
"HOL-Eisbach.Eisbach"
begin
method exI for y::'a = (rule_tac exI[where x = y])
section‹ General Laws›
lemma SKIP_Neq_STOP: "SKIP ≠ STOP"
by (auto simp: Process_eq_spec F_SKIP F_STOP D_SKIP D_STOP Un_def)
lemma BOT_less1[simp]: "⊥ ≤ (X::'a process)"
by (simp add: le_approx_implies_le_ref)
lemma BOT_less2[simp]: "BOT ≤ (X::'a process)"
by simp
section‹ Deterministic Choice Operator Laws ›
lemma mono_Det_FD_onside[simp]: " P ≤ P' ⟹ (P □ S) ≤ (P' □ S)"
unfolding le_ref_def F_Det D_Det using F_subset_imp_T_subset by blast
lemma mono_Det_FD[simp]: " ⟦P ≤ P'; S ≤ S'⟧ ⟹ (P □ S) ≤ (P' □ S')"
by (metis Det_commute dual_order.trans mono_Det_FD_onside)
lemma mono_Det_ref: " ⟦P ⊑ P'; S ⊑ S'⟧ ⟹ (P □ S) ⊑ (P' □ S')"
using below_trans mono_Det mono_Det_sym by blast
lemma Det_BOT : "(P □ ⊥) = ⊥"
by (auto simp add:Process_eq_spec D_Det F_Det is_processT2 D_imp_front_tickFree F_UU D_UU)
lemma Det_STOP: "(P □ STOP) = P"
by (auto simp add: Process_eq_spec D_Det F_Det D_STOP F_STOP T_STOP
Un_def Sigma_def is_processT8 is_processT6_S2)
lemma Det_id: "(P □ P) = P"
by (auto simp: Process_eq_spec D_Det F_Det Un_def Sigma_def is_processT8 is_processT6_S2)
lemma Det_assoc: "((M □ P) □ Q) = (M □ (P □ Q))"
by (auto simp add: Process_eq_spec D_Det F_Det Un_def Sigma_def T_Det)
section‹ NonDeterministic Choice Operator Laws ›
lemma mono_Ndet_FD[simp]: " ⟦P ≤ P'; S ≤ S'⟧ ⟹ (P ⊓ S) ≤ (P' ⊓ S')"
by (auto simp: le_ref_def F_Ndet D_Ndet)
lemma mono_Ndet_FD_left[simp]: "P ≤ Q ⟹ (P ⊓ S) ≤ Q"
by (metis D_Ndet F_Ndet dual_order.trans le_ref_def le_sup_iff order_refl)
lemma mono_Ndet_FD_right[simp]: "P ≤ Q ⟹ (S ⊓ P) ≤ Q"
by (metis D_Ndet F_Ndet dual_order.trans le_ref_def le_sup_iff order_refl)
lemma mono_Ndet_ref: " ⟦P ⊑ P'; S ⊑ S'⟧ ⟹ (P ⊓ S) ⊑ (P' ⊓ S')"
using below_trans mono_Ndet mono_Ndet_sym by blast
lemma Ndet_BOT: "(P ⊓ ⊥) = ⊥"
by (auto simp: Process_eq_spec D_Ndet F_Ndet is_processT2 D_imp_front_tickFree F_UU D_UU)
lemma Ndet_id: "(P ⊓ P) = P"
by (simp_all add: F_Ndet D_Ndet Process_eq_spec)
lemma Ndet_assoc: "((M ⊓ P) ⊓ Q) = (M ⊓ (P ⊓ Q))"
by (simp_all add: F_Ndet D_Ndet Process_eq_spec Un_assoc)
subsection‹ Multi-Operators laws ›
lemma Det_distrib: "(M □ (P ⊓ Q)) = ((M □ P) ⊓ (M □ Q))"
by (auto simp add: Process_eq_spec F_Det D_Det F_Ndet D_Ndet Un_def T_Ndet)
lemma Ndet_distrib: "(M ⊓ (P □ Q)) = ((M ⊓ P) □ (M ⊓ Q))"
by (auto simp add: Process_eq_spec F_Det D_Det F_Ndet
D_Ndet Un_def T_Ndet is_processT8 is_processT6_S2)
lemma Ndet_FD_Det: "(P ⊓ Q) ≤ (P □ Q)"
apply(auto simp add:le_ref_def D_Ndet D_Det F_Ndet F_Det T_Ndet T_Det Ra_def min_elems_def)
using is_processT6_S2 NF_ND by blast+
section‹ Sequence Operator Laws ›
subsection‹Preliminaries›
definition F_minus_D_Seq where
"F_minus_D_Seq P Q ≡ {(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
{(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q}"
lemma F_minus_D_Seq_opt: "(a,b) ∈ ℱ(P ❙; Q) = (a ∈ 𝒟(P ❙; Q) ∨ (a,b) ∈ F_minus_D_Seq P Q)"
using NF_ND by (auto simp add: F_Seq D_Seq F_minus_D_Seq_def) blast+
lemma Process_eq_spec_optimized_Seq :
"((P ❙; Q) = (U ❙; S)) = (𝒟 (P ❙; Q) = 𝒟 (U ❙; S) ∧
F_minus_D_Seq P Q ⊆ ℱ (U ❙; S) ∧
F_minus_D_Seq U S ⊆ ℱ (P ❙; Q))"
unfolding Process_eq_spec_optimized[of "(P ❙; Q)" "(U ❙; S)"]
by (auto simp:F_minus_D_Seq_opt)
subsection‹Laws›
lemma mono_Seq_FD[simp]: " ⟦P ≤ P'; S ≤ S'⟧ ⟹ (P ❙; S) ≤ (P' ❙; S')"
apply (auto simp: le_ref_def F_Seq D_Seq)
by (metis F_subset_imp_T_subset subsetCE)+
lemma mono_Seq_ref: " ⟦P ⊑ P'; S ⊑ S'⟧ ⟹ (P ❙; S) ⊑ (P' ❙; S')"
using below_trans mono_Seq mono_Seq_sym by blast
lemma BOT_Seq: "(⊥ ❙; P) = ⊥"
by (simp add: BOT_iff_D D_Seq D_UU)
lemma Seq_SKIP: "(P ❙; SKIP) = P"
apply (auto simp add: Process_eq_spec F_Seq F_SKIP D_Seq D_SKIP T_F_spec is_processT6_S1)
apply (use is_processT4 in blast)
apply (meson append_single_T_imp_tickFree is_processT5_S7 non_tickFree_tick tickFree_append)
apply (meson is_processT8)
apply (use T_F_spec insert_absorb is_processT5_S2 in fastforce)
by (metis F_T is_processT nonTickFree_n_frontTickFree)
lemma SKIP_Seq: "(SKIP ❙; P) = P"
by (auto simp add: Process_eq_spec D_Seq T_SKIP F_Seq F_SKIP D_SKIP is_processT8_Pair)
lemma STOP_Seq: "(STOP ❙; P) = STOP"
by (simp add: STOP_iff_T T_Seq T_STOP F_STOP D_STOP Collect_conv_if)
subsection‹ Multi-Operators laws ›
lemma Seq_Ndet_distrR: "((P ⊓ Q) ❙; S) = ((P ❙; S) ⊓ (Q ❙; S))"
by (auto simp add: Process_eq_spec D_Seq D_Ndet T_Ndet Un_def F_Seq T_Seq F_Ndet)
lemma Seq_Ndet_distrL: "(P ❙; (Q ⊓ S)) = ((P ❙; Q) ⊓ (P ❙; S))"
by (auto simp add: Process_eq_spec D_Seq D_Ndet T_Ndet Un_def F_Seq F_Ndet)
lemma Seq_assoc_D: "𝒟 (P ❙; (Q ❙; S)) = 𝒟 ((P ❙; Q) ❙; S)"
proof(safe, goal_cases)
show ‹s ∈ 𝒟 (P ❙; (Q ❙; S)) ⟹ s ∈ 𝒟 (P ❙; Q ❙; S)› for s
by (simp add: D_Seq T_Seq) (metis append.assoc)
next
fix s
assume ‹s ∈ 𝒟 (P ❙; Q ❙; S)›
thus ‹s ∈ 𝒟 (P ❙; (Q ❙; S))›
proof(auto simp add:D_Seq T_Seq, goal_cases)
case (1 t1 t2 t1a t2a)
from "1"(1)[rule_format, OF "1"(5)] show ?case
apply (cases ‹tickFree t2a›)
apply (metis "1"(4) "1"(5) append_single_T_imp_tickFree non_tickFree_tick tickFree_append)
by (metis "1"(3) "1"(4) "1"(6) T_nonTickFree_imp_decomp append.assoc butlast_snoc)
next
case (2 t1 t2)
then show ?case
by (meson D_imp_front_tickFree front_tickFree_implies_tickFree is_processT7 is_processT9_S_swap)
qed
qed
lemma Seq_assoc: "(P ❙; (Q ❙; S)) = ((P ❙; Q) ❙; S)"
proof (auto simp: Process_eq_spec_optimized_Seq Seq_assoc_D, goal_cases)
case (1 a b)
then show ?case
proof(auto simp add:F_minus_D_Seq_def Seq_assoc_D F_minus_D_Seq_opt append_single_T_imp_tickFree
del:conjI,
goal_cases 11 12)
case (11 t1 t2)
then show ?case by (metis (mono_tags, lifting) D_Seq Seq_assoc_D UnCI mem_Collect_eq)
next
case (12 t1 t1a t2a)
hence "(t1 @ t1a) @ [tick] ∈ 𝒯 (P ❙; Q)" by (auto simp:T_Seq)
then show ?case
using 12(2)[rule_format, of "t1@t1a" t2a] 12(4,5,6) by simp
qed
next
case (2 a b)
then show ?case
proof(auto simp add:F_minus_D_Seq_def Seq_assoc_D F_minus_D_Seq_opt
append_single_T_imp_tickFree T_Seq del:conjI,
goal_cases 21 22 23)
case 21
then show ?case
using D_Seq by force
next
case (22 t1 t2 t1a t2a)
then obtain t2b where "t2a = t2b@[tick]"
by (metis T_nonTickFree_imp_decomp append_single_T_imp_tickFree non_tickFree_tick tickFree_append)
with 22 show ?case using append.assoc butlast_snoc by auto
next
case (23 t1 t2)
hence "t1 ∈ 𝒟 (P ❙; (Q ❙; S))"
by (simp add: D_Seq) (meson is_processT9_S_swap)
with 23 Seq_assoc_D show ?case by (metis front_tickFree_implies_tickFree process_charn)
qed
qed
section‹ The Multi-Prefix Operator Laws ›
lemma mono_Mprefix_FD[simp]: "∀x ∈ A. P x ≤ P' x ⟹ Mprefix A P ≤ Mprefix A P'"
by (auto simp: le_ref_def F_Mprefix D_Mprefix) blast+
lemmas mono_Mprefix_ref = mono_Mprefix0
lemma Mprefix_STOP: "(Mprefix {} P) = STOP"
by (auto simp:Process_eq_spec F_Mprefix D_Mprefix D_STOP F_STOP)
subsection‹ Multi-Operators laws ›
lemma Mprefix_Un_distrib: "(Mprefix (A ∪ B) P) = ((Mprefix A P) □ (Mprefix B P))"
apply (unfold Process_eq_spec, rule conjI)
apply (auto, (elim disjE conjE | simp_all add: F_Det F_Mprefix Un_def image_def)+, auto)
by (auto simp add: D_Det D_Mprefix Un_def)
lemma Mprefix_Seq: "((Mprefix A P) ❙; Q) = (Mprefix A (λx. (P x) ❙; Q))"
proof (unfold Process_eq_spec, rule conjI, rule subset_antisym, goal_cases)
case 1
then show ?case
apply(unfold split_def F_Seq D_Seq F_Mprefix T_Mprefix D_Mprefix)
apply(rule subsetI, simp_all, elim disjE conjE exE)
apply(rule disjI1, simp, meson tickFree_tl)
apply (rule disjI2, rule conjI, simp) apply auto[1]
apply (auto simp add:hd_append)[1]
using tickFree_tl by fastforce
next
case 2
then show ?case
apply(unfold split_def F_Seq D_Seq F_Mprefix T_Mprefix D_Mprefix)
apply(rule subsetI, simp_all, elim disjE conjE exE)
apply(rule disjI1, simp, blast)
apply(rule disjI1, metis event.simps(3) list.exhaust_sel tickFree_Cons)
proof(goal_cases)
case (1 x a t1 t2)
then show ?case
apply(rule_tac disjI2, rule_tac disjI1, rule_tac x="(ev a)#t1" in exI)
using hd_Cons_tl image_iff by fastforce
next
case (2 x a)
then show ?case
by (metis prod.collapse)
qed
next
case 3
then show ?case
apply (auto simp add: D_Mprefix D_Seq T_Mprefix)
apply (metis event.distinct(1) hd_append image_iff list.sel(1))
apply (metis event.distinct(1) hd_append list.sel(1) tl_append2)
by (metis Cons_eq_appendI hd_Cons_tl list.sel(1) list.sel(3))
qed
subsection‹ Derivative Operators laws ›
lemma Mprefix_singl: "(Mprefix {a} P) = (a → (P a))"
by (simp add:write0_def Mprefix_def, rule arg_cong[of _ _ "λx. Abs_process x"]) fastforce
lemma mono_read_FD: "(⋀x. P x ≤ Q x) ⟹ (c❙?x → (P x)) ≤ (c❙?x → (Q x))"
by (simp add: read_def)
lemma mono_write_FD: "(P ≤ Q) ⟹ (c❙!x → P) ≤ (c❙!x → Q)"
by (simp add: write_def)
lemma mono_write0_FD: "P ≤ Q ⟹ (a → P) ≤ (a → Q)"
by (simp add: write0_def)
lemma mono_read_ref: "(⋀x. P x ⊑ Q x) ⟹ (c❙?x → (P x)) ⊑ (c❙?x → (Q x))"
by (simp add: mono_Mprefix0 read_def)
lemma mono_write_ref: "(P ⊑ Q) ⟹ (c❙!x → P) ⊑ (c❙!x → Q)"
by (simp add: mono_Mprefix0 write_def)
lemma mono_write0_ref: "P ⊑ Q ⟹ (a → P) ⊑ (a → Q)"
by (simp add: mono_Mprefix0 write0_def)
lemma write0_Ndet: "(a → (P ⊓ Q)) = ((a → P) ⊓ (a → Q))"
by (auto simp: Process_eq_spec write0_def D_Ndet F_Ndet F_Mprefix D_Mprefix Un_def)
lemma write0_Det_Ndet: "((a → P) □ (a → Q)) = ((a → P) ⊓ (a → Q))"
by (auto simp: Process_eq_spec write0_def D_Ndet F_Ndet F_Det D_Det) (simp add: F_Mprefix)+
lemma Mprefix_Det: ‹(□e∈A → P e) □ (□e∈A → Q e) = □e∈A → (P e ⊓ Q e)›
by (auto simp: Process_eq_spec F_Det D_Det) (auto simp: D_Ndet F_Ndet F_Mprefix D_Mprefix)
section‹ The Hiding Operator Laws ›
subsection‹ Preliminaries ›
lemma elemDIselemHD: ‹t ∈ 𝒟 P ⟹ trace_hide t (ev ` A) ∈ 𝒟 (P \ A)›
proof (cases "tickFree t")
case True
assume "t ∈ 𝒟 P"
with True show ?thesis by (simp add:D_Hiding, rule_tac x=t in exI, rule_tac x="[]" in exI, simp)
next
case False
assume a:"t ∈ 𝒟 P"
with False obtain t' where "t = t'@[tick]" using D_imp_front_tickFree nonTickFree_n_frontTickFree by blast
with a show ?thesis apply (auto simp add:D_Hiding, rule_tac x=t' in exI, rule_tac x="[tick]" in exI)
by (meson front_tickFree_implies_tickFree front_tickFree_single is_processT)
qed
lemma length_strict_mono: "strict_mono (f::nat ⇒ 'a list) ⟹ length (f i) ≥ i + length (f 0)"
apply(induct i, simp)
by (metis dual_order.trans lessI less_length_mono not_less not_less_eq_eq plus_nat.simps(2) strict_mono_def)
lemma mono_trace_hide: "a ≤ b ⟹ trace_hide a (ev ` A) ≤ trace_hide b (ev ` A)"
by (metis filter_append le_list_def)
lemma mono_constant:
assumes "mono (f::nat ⇒ 'a event list)" and "∀i. f i ≤ a"
shows "∃i. ∀j≥i. f j = f i"
proof -
from assms(2) have "∀i. length (f i) ≤ length a"
by (simp add: le_length_mono)
hence aa:"finite {length (f i)|i. True}"
using finite_nat_set_iff_bounded_le by auto
define lm where l2:"lm = Max {length (f i)|i. True}"
with aa obtain im where "length (f im) = lm" using Max_in by fastforce
with l2 assms(1) show ?thesis
apply(rule_tac x=im in exI, intro impI allI)
by (metis (mono_tags, lifting) Max_ge aa antisym le_length_mono le_neq_trans less_length_mono
mem_Collect_eq mono_def order_less_irrefl)
qed
lemma elemTIselemHT: ‹t ∈ 𝒯 P ⟹ trace_hide t (ev ` A) ∈ 𝒯 (P \ A)›
proof (cases "tickFree t")
case True
assume a:"t ∈ 𝒯 P"
with True show ?thesis
proof (cases "(∃ta. trace_hide t (ev ` A) = trace_hide ta (ev ` A) ∧ (ta, ev ` A) ∈ ℱ P)")
case True
thus ?thesis by (simp add:T_Hiding)
next
case False
with a False inf_hidden[of A t P] obtain f where "isInfHiddenRun f P A ∧ t ∈ range f" by auto
with True show ?thesis
by (simp add:T_Hiding, rule_tac disjI2, rule_tac x=t in exI, rule_tac x="[]" in exI, auto)
qed
next
case False
assume a:"t ∈ 𝒯 P"
with False obtain t' where tt:"t = t'@[tick]" using T_nonTickFree_imp_decomp by auto
with a show ?thesis
proof (cases "(∃ta. trace_hide t (ev ` A) = trace_hide ta (ev ` A) ∧ (ta, ev ` A) ∈ ℱ P)")
case True
thus ?thesis by (simp add:T_Hiding)
next
case False
assume "t ∈ 𝒯 P"
with False inf_hidden[of A t P] obtain f where "isInfHiddenRun f P A ∧ t ∈ range f" by auto
then show ?thesis
apply (simp add:T_Hiding, rule_tac disjI2, rule_tac x=t' in exI, rule_tac x="[tick]" in exI, auto)
apply (metis append_T_imp_tickFree list.distinct(1) tt)
using tt apply force
by (metis False append_T_imp_tickFree is_processT5_S7 non_tickFree_tick not_Cons_self2 tickFree_append tt)
qed
qed
lemma Hiding_Un_D1: ‹𝒟 (P \ (A ∪ B)) ⊆ 𝒟 ((P \ A) \ B)›
proof (simp add:conj_commute D_Hiding, intro conjI subset_antisym subsetI, simp_all, goal_cases)
case (1 x)
then obtain t u where B1:"x = trace_hide t (ev ` (A ∪ B)) @ u"
and B2:"tickFree t" and B3:"front_tickFree u"
and B4:"(t ∈ 𝒟 P ∨ (∃(f:: nat ⇒ 'a event list). isInfHiddenRun f P (A ∪ B)
∧ t ∈ range f))" by auto
thus ?case
apply(erule_tac disjE)
apply(rule_tac x="trace_hide t (ev ` A)" in exI, rule_tac x=u in exI)
apply(simp add:Hiding_tickFree tickFree_def)
apply(rule disjI1, rule_tac x=t in exI, rule_tac x="[]" in exI, simp)
proof(goal_cases)
case 1
then obtain f n where fc:"isInfHiddenRun f P (A ∪ B) ∧ t = f n" by auto
define ff where "ff = (λi. take (i + length (f 0)) (f i))"
with fc have ffc:"isInfHiddenRun ff P (A ∪ B) ∧ t ∈ range ff"
proof (auto, goal_cases)
case 1
{ fix x
from length_strict_mono[of f "Suc x ", OF 1(2)]
have a:"take (x + length (f 0)) (f (Suc x)) < take ((Suc x) + length (f 0)) (f (Suc x))"
by (simp add: take_Suc_conv_app_nth)
from 1(2)[THEN strict_monoD, of x "Suc x", simplified]
obtain t where "f (Suc x) = (f x @ t)" by (metis le_list_def less_imp_le)
with length_strict_mono[of f x, OF 1(2)]
have "take (x + length (f 0)) (f x) = take (x + length (f 0)) (f (Suc x))" by simp
with a have "take (x + length (f 0)) (f x) < take (Suc x + length (f 0)) (f (Suc x))" by simp
}
thus ?case by (meson lift_Suc_mono_less strict_mono_def)
next
case (2 i)
have "take (i + length (f 0)) (f i) ≤ f i"
using append_take_drop_id le_list_def by blast
also have "∀x y. x ≤ y ∧ y ∈ 𝒯 P ⟶ x ∈ 𝒯 P" using is_processT3_ST_pref by blast
ultimately show ?case using "2"(3) by blast
next
case (3 i)
hence "(f i) ≥ (f 0)" using strict_mono_less_eq by blast
hence "take (i + length (f 0)) (f i) ≥ (f 0)"
by (metis add.commute append_eq_conv_conj le_list_def take_add)
hence a:" [x←take (i + length (f 0)) (f i) . x ∉ ev ` A ∧ x ∉ ev ` B]
≥ [x←f 0 . x ∉ ev ` A ∧ x ∉ ev ` B]"
by (metis (no_types, lifting) filter_append le_list_def)
have "take (i + length (f 0)) (f i) ≤ f i"
using append_take_drop_id le_list_def by blast
hence " [x←take (i + length (f 0)) (f i) . x ∉ ev ` A ∧ x ∉ ev ` B]
≤ [x←f i . x ∉ ev ` A ∧ x ∉ ev ` B]"
by (metis (no_types, lifting) filter_append le_list_def)
with a 3(4) show ?case by (metis (no_types, lifting) dual_order.antisym)
next
case 4
have "f (length (f n) - length (f 0)) ≥ f n"
by (simp add: "4"(2) add_le_imp_le_diff length_strict_mono strict_mono_less_eq)
hence "f n = (λi. take (i + length (f 0)) (f i)) (length (f n) - length (f 0))"
by (metis "4"(2) add.commute append_eq_conv_conj diff_is_0_eq'
le_add_diff_inverse le_list_def le_zero_eq nat_le_linear strict_mono_less_eq)
then show ?case by blast
qed
thus ?case proof(cases "∃m. (∀i>m. last (ff i) ∈ (ev ` A))")
case True
then obtain m where mc:"∀i>m. last (ff i) ∈ (ev ` A)" by blast
hence mc2:"tickFree (ff m)"
by (metis (no_types, lifting) B2 event.distinct(1) ffc
image_iff mem_Collect_eq set_filter tickFree_def)
with mc mc2 1 ffc show ?thesis
apply(rule_tac x="trace_hide (ff m) (ev ` A)" in exI, rule_tac x=u in exI, simp, intro conjI)
apply (metis (no_types, lifting) mem_Collect_eq set_filter tickFree_def)
apply (metis (no_types, lifting) rangeE)
apply(rule disjI1, rule_tac x="ff m" in exI, rule_tac x="[]" in exI, intro conjI, simp_all)
apply(rule disjI2, rule_tac x="λi. ff(i + m)" in exI, intro conjI)
apply (metis (no_types, lifting) add.commute add.right_neutral rangeI)
apply (simp add: strict_mono_def)
apply blast
proof(rule allI, goal_cases)
case (1 i)
from ffc ff_def True have "∃t. (ff (i + m)) = (ff m) @ t ∧ set t ⊆ (ev ` A)"
proof(induct i)
case 0
then show ?case by fastforce
next
case (Suc i)
then obtain tt where tc:"(ff (i + m)) = (ff m) @ tt ∧ set tt ⊆ (ev ` A)" by blast
from ffc ff_def length_strict_mono[of ff] have lc:"length (ff (Suc i + m))
= Suc (length (ff (i + m)))"
by (metis (no_types, lifting) add_Suc fc length_strict_mono length_take min.absorb2)
from True obtain l where lc2:"l = last (ff (Suc i + m)) ∧ l ∈ (ev ` A)"
by (meson less_add_same_cancel2 mc zero_less_Suc)
from ffc obtain r where rc:"ff (Suc i + m) = ff (i + m)@r"
by (metis add.commute add_Suc_right le_list_def lessI less_imp_le strict_mono_less_eq)
with lc have "length r = 1" by (metis Suc_eq_plus1 add_left_cancel length_append)
with rc lc2 have "r = [l]"
by (metis (no_types, lifting) Nil_is_append_conv Suc_eq_plus1 append_butlast_last_id
append_eq_append_conv append_eq_append_conv2 length_Cons length_append)
with Suc lc2 tc rc show ?case by (rule_tac x="tt@[l]" in exI, auto)
qed
then show ?case using filter_empty_conv by fastforce
qed
next
case False
{ fix i
assume as:"(i::nat) > 0"
with ffc obtain tt where ttc:"ff i = ff 0 @ tt ∧ set tt ⊆ ev ` (A ∪ B)"
unfolding isInfHiddenRun_1 by blast
with ffc as have "tt ≠ []" using strict_mono_eq by fastforce
with ttc have "last (ff i) ∈ ev ` (A ∪ B)" by auto
}
hence as2:"∀i. ∃j>i. last(ff j) ∈ ((ev ` B) - (ev ` A))"
by (metis DiffI False UnE gr_implies_not_zero gr_zeroI image_Un)
define ffb where "ffb = rec_nat t (λi t. (let j = SOME j. ff j > t ∧
last(ff j) ∈ ((ev ` B) - (ev ` A)) in ff j))"
with as2 have ffbff:"⋀n. ffb n ∈ range ff"
by (metis (no_types, lifting) ffc old.nat.exhaust old.nat.simps(6) old.nat.simps(7) rangeI)
from 1 ffb_def show ?thesis
apply(rule_tac x="trace_hide t (ev ` A)" in exI, rule_tac x=u in exI, simp, intro conjI)
apply (meson filter_is_subset set_rev_mp tickFree_def)
proof(rule disjI2, rule_tac x="λi. trace_hide (ffb i) (ev ` A)" in exI, intro conjI, goal_cases)
case 1
then show ?case by (metis (no_types, lifting) old.nat.simps(6) rangeI)
next
case 2
{ fix n
have a0:"(ffb (Suc n)) = ff (SOME j. ff j > ffb n ∧ last(ff j) ∈ ((ev ` B) - (ev ` A)))"
by (simp add: ffb_def)
from ffbff obtain i where a1:"ffb n = ff i" by blast
with as2 have "∃j. ff j > ffb n ∧ last(ff j) ∈ ((ev ` B) - (ev ` A))"
by (metis ffc strict_mono_def)
with a0 a1 have a:"(ffb (Suc n)) > (ffb n) ∧ last (ffb (Suc n)) ∉ (ev ` A)"
by (metis (no_types, lifting) Diff_iff tfl_some)
then obtain r where "ffb (Suc n) = (ffb n)@r ∧ last r ∉ (ev ` A)"
by (metis append_self_conv last_append le_list_def less_list_def)
hence "trace_hide (ffb (Suc n)) (ev ` A) > trace_hide (ffb n) (ev ` A)"
by (metis (no_types, lifting) a append_self_conv filter_append filter_empty_conv
last_in_set le_list_def less_list_def)
}
then show ?case by (metis (mono_tags, lifting) lift_Suc_mono_less_iff strict_monoI)
next
case 3
then show ?case by (metis (mono_tags) elemTIselemHT ffbff ffc rangeE)
next
case 4
from ffbff ffc show ?case by (metis rangeE trace_hide_union)
qed
qed
qed
qed
lemma Hiding_Un_D2: ‹finite A ⟹ 𝒟 ((P \ A) \ B) ⊆ 𝒟 (P \ (A ∪ B))›
proof (simp add:conj_commute D_Hiding, intro conjI subset_antisym subsetI, simp_all, goal_cases)
case (1 x)
then obtain t u where B1:"x = trace_hide t (ev ` B) @ u"
and B2:"tickFree t"
and B3:"front_tickFree u"
and B4:‹(t ∈ 𝒟 (P \ A) ∨
(∃(f:: nat ⇒ 'a event list). isInfHiddenRun f (P \ A) B ∧ t ∈ range f))›
by (simp add:D_Hiding) blast
thus ?case
proof(erule_tac disjE, auto simp add:D_Hiding, goal_cases)
case (1 ta ua)
then show ?case
by (rule_tac x=ta in exI, rule_tac x = "trace_hide ua (ev ` B) @ u" in exI,
auto simp add: front_tickFree_append tickFree_def)
next
case (2 ua f xa)
then show ?case
apply(rule_tac x="f xa" in exI, rule_tac x="trace_hide ua (ev ` B) @ u" in exI,
intro conjI disjI2)
apply(auto simp add: front_tickFree_append tickFree_def)
by (rule_tac x="f" in exI) (metis (no_types) filter_filter rangeI)
next
case (3 f xx)
note "3a" = 3
then show ?case
proof(cases ‹∃i. f i ∈ 𝒟 (P \ A)›)
case True
with 3 show ?thesis
proof(auto simp add:D_Hiding, goal_cases)
case (1 i ta ua)
then show ?case
apply (rule_tac x=ta in exI, rule_tac x="trace_hide ua (ev ` B) @ u" in exI, intro conjI)
apply (metis (full_types) front_tickFree_append Hiding_tickFree tickFree_append)
apply(subgoal_tac "trace_hide (f xx) (ev ` B) = trace_hide (f i) (ev ` B)", auto)
apply (metis (full_types) filter_append filter_filter)
by (metis (full_types) filter_append filter_filter)
next
case (2 i ua fa xa)
hence "trace_hide (f xx) (ev ` B) = trace_hide (f i) (ev ` B)" by metis
with 2 show ?case
apply (rule_tac x="fa xa" in exI, rule_tac x="trace_hide ua (ev ` B) @ u" in exI, intro conjI)
apply (metis (full_types) front_tickFree_append Hiding_tickFree tickFree_append)
apply (simp_all)
apply(rule_tac disjI2, rule_tac x=fa in exI, auto)
by (metis (no_types) filter_filter)
qed
next
case False
with 3 have Falsebis:‹∀i. (f i ∈ 𝒯 (P \ A) ∧ f i ∉ 𝒟 (P \ A))› by blast
with T_Hiding[of P A] D_Hiding[of P A]
have "∀i. (f i ∈ {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ ℱ P})"
by (metis (no_types, lifting) UnE)
hence ff0:"∀i. (∃t. f i = trace_hide t (ev ` A) ∧ t ∈ 𝒯 P)" using F_T by fastforce
define ff where ff1:"ff = (λi. SOME t. f i = trace_hide t (ev ` A) ∧ t ∈ 𝒯 P)"
hence "inj ff" unfolding inj_def by (metis (mono_tags, lifting) "3"(4) ff0 strict_mono_eq tfl_some)
hence ff2:"infinite (range ff)" using finite_imageD by blast
{ fix tt i
assume "tt ∈ range ff"
then obtain k where "ff k = tt" using finite_nat_set_iff_bounded_le by blast
hence kk0:"f k = trace_hide tt (ev ` A) ∧ tt ∈ 𝒯 P" using ff1
by (metis (mono_tags, lifting) ff0 someI_ex)
hence "set (take i tt) ⊆ set (f i) ∪ (ev ` A)"
proof(cases "k ≤ i")
case True
hence "set (f k) ⊆ set (f i)"
by (metis "3"(4) le_list_def set_append strict_mono_less_eq sup.cobounded1)
moreover from kk0 have "set (take i tt) ⊆ set (f k) ∪ (ev ` A)" using in_set_takeD by fastforce
ultimately show ?thesis by blast
next
case False
have a:"length (f i) ≥ i" by (meson "3"(4) dual_order.trans le_add1 length_strict_mono)
have b:"f i ≤ f k" using "3"(4) False nat_le_linear strict_mono_less_eq by blast
with a have c:"take i (f k) ≤ (f i)"
by (metis append_eq_conv_conj le_add_diff_inverse le_list_def take_add)
from kk0[THEN conjunct1] have c1:"f k = (trace_hide (take i tt) (ev ` A)) @
(trace_hide (drop i tt) (ev ` A))"
by (metis append_take_drop_id filter_append)
have "length (trace_hide (take i tt) (ev ` A)) ≤ i"
by (metis length_filter_le length_take min.absorb2 nat_le_linear order.trans take_all)
with c1 have "take i (f k) ≥ (trace_hide (take i tt) (ev ` A))" by (simp add: le_list_def)
with c obtain t where d:"f i = (trace_hide (take i tt) (ev ` A))@t"
by (metis append.assoc le_list_def)
then show ?thesis using in_set_takeD by fastforce
qed
} note ee=this
{ fix i
have "finite {(take i t)|t. t ∈ range ff}"
proof(induct i, simp)
case (Suc i)
have ff:"{take (Suc i) t|t. t ∈ range ff} ⊆ {(take i t)|t. t ∈ range ff} ∪
(⋃e∈(set (f (Suc i)) ∪ (ev ` A)). {(take i t)@[e]|t. t ∈ range ff})" (is "?AA ⊆ ?BB")
proof
fix t
assume "t ∈ ?AA"
then obtain t' where hh:"t' ∈ range ff ∧ t = take (Suc i) t'"
using finite_nat_set_iff_bounded_le by blast
with ee[of t'] show "t ∈ ?BB"
proof(cases "length t' > i")
case True
hence ii:"take (Suc i) t' = take i t' @ [t'!i]" by (simp add: take_Suc_conv_app_nth)
with ee[of t' "Suc i"] have "t'!i ∈ set (f (Suc i)) ∪ (ev ` A)" by (simp add: hh)
with ii hh show ?thesis by blast
next
case False
hence "take (Suc i) t' = take i t'" by fastforce
with hh show ?thesis by auto
qed
qed
{ fix e
have "{x @ [e] |x. ∃t. x = take i t ∧ t ∈ range ff} = {take i t' @ [e] |t'. t' ∈ range ff}"
by auto
hence "finite({(take i t') @ [e] |t'. t'∈range ff})"
using finite_image_set[of _ "λt. t@[e]", OF Suc] by auto
} note gg=this
have "finite(set (f (Suc i)) ∪ (ev ` A))" using 1(1) by simp
with ff gg Suc show ?case by (metis (no_types, lifting) finite_UN finite_Un finite_subset)
qed
} note ff=this
hence "∀i. {take i t |t. t ∈ range ff} = {t. ∃t'. t = take i (ff t')}" by auto
with KoenigLemma[of "range ff"] ff ff2
obtain f' where gg:"strict_mono (f':: nat ⇒ 'a event list) ∧
range f' ⊆ {t. ∃t'∈range ff. t ≤ t'}" by auto
{ fix i
from gg obtain n where aa:"f' i ≤ ff n" by blast
have "∃t. f n = f 0 @ t" by (metis "3a"(4) le0 le_list_def strict_mono_less_eq)
with mono_trace_hide[OF aa, of A] ff0 ff1 have "∃t. trace_hide (f' i) (ev ` A) ≤ f 0 @ t"
by (metis (mono_tags, lifting) someI_ex)
} note zz=this
{
define ff' where "ff' = (λi. trace_hide (f' i) (ev ` A))"
with gg have "mono ff'"
by (rule_tac monoI, simp add: mono_trace_hide strict_mono_less_eq)
assume aa:"∀i. trace_hide (f' i) (ev ` A) ≤ f 0"
with aa mono_constant have "∃i. ∀j≥i. ff' j = ff' i" using ‹mono ff'› ff'_def by blast
then obtain m where bb:"∀j≥m. ff' j = ff' m" by blast
have ‹ff' m ∈ 𝒟 (P \ A)›
proof(simp add:D_Hiding, rule_tac x="f' m" in exI, rule_tac x="[]" in exI,
intro conjI, simp, goal_cases)
case 1
from gg have "f' m < f' (Suc m)" by (meson lessI strict_monoD)
moreover from gg obtain k where "f' (Suc m) ≤ ff k" by blast
moreover have "ff k ∈ 𝒯 P" by (metis (mono_tags, lifting) ff0 ff1 someI_ex)
ultimately show ?case
by (metis NF_NT append_Nil2 front_tickFree_mono is_processT le_list_def less_list_def)
next
case 2
then show ?case unfolding ff'_def by simp
next
case 3
then show ?case
proof(rule disjI2, rule_tac x="λi. f' (m + i)" in exI, simp_all, intro conjI allI, goal_cases)
case 1
show ?case using gg[THEN conjunct1]
by (rule_tac strict_monoI, simp add: strict_monoD)
next
case (2 i)
from gg obtain k where "f' (m + i) ≤ ff k" by blast
moreover from ff0 ff1 have "ff k ∈ 𝒯 P" by (metis (mono_tags, lifting) someI_ex)
ultimately have "f' (m + i) ∈ 𝒯 P" using is_processT3_ST_pref by blast
then show ?case by (simp add: add.commute)
next
case (3 i)
then show ?case using bb[THEN spec, of "m+i", simplified] unfolding ff'_def by assumption
next
case 4
then show ?case by (metis Nat.add_0_right rangeI)
qed
qed
with gg False have "False"
by (metis (no_types, lifting) Falsebis aa append_Nil2 ff'_def front_tickFree_mono
is_processT is_processT2_TR le_list_def)
}
with zz obtain m where hh:"trace_hide (f' m) (ev ` A) ≥ f 0"
unfolding le_list_def by (metis append_eq_append_conv2)
from ff0 ff1 gg show ?thesis
proof(auto simp add:T_Hiding, rule_tac x="f' m" in exI, rule_tac x=u in exI,
intro conjI, simp_all add:3(3), goal_cases)
case 1
hence "f' m < f' (Suc m)" by (meson lessI strict_monoD)
moreover from gg obtain k where "f' (Suc m) ≤ ff k" by blast
moreover have "ff k ∈ 𝒯 P" by (metis (mono_tags, lifting) ff0 ff1 someI_ex)
ultimately show ?case
by (metis NF_NT append_Nil2 front_tickFree_mono is_processT le_list_def less_list_def)
next
case 2
from gg obtain k where "f' m ≤ ff k" by blast
with ff0 ff1 mono_trace_hide[of "f' m"] have "trace_hide (f' m) (ev ` A) ≤ f k"
by (metis (mono_tags, lifting) someI_ex)
with mono_trace_hide[OF this, of B] mono_trace_hide[OF hh, of B] 3(6)[THEN spec, of k] 3(6)
show ?case by (metis (full_types) dual_order.antisym filter_filter)
next
case 3 show ?case
proof(rule disjI2, rule_tac x="λi. f' (m + i)" in exI, simp_all, intro conjI allI, goal_cases)
case 1
then show ?case by (metis Nat.add_0_right rangeI)
next
case 2 with 3(4) show ?case
by (rule_tac strict_monoI, simp add: strict_monoD)
next
case (3 i)
from gg obtain k where "f' (m + i) ≤ ff k" by blast
moreover from ff0 ff1 have "ff k ∈ 𝒯 P" by (metis (mono_tags, lifting) someI_ex)
ultimately have "f' (m + i) ∈ 𝒯 P" using is_processT3_ST_pref by blast
then show ?case by (simp add: add.commute)
next
case (4 i)
from gg obtain k where "f' (m + i) ≤ ff k" by blast
with ff0 ff1 mono_trace_hide[of "f' (m + i)"] have ll:"trace_hide (f' (m + i)) (ev ` A) ≤ f k"
by (metis (mono_tags, lifting) someI_ex)
{ fix a b c assume "(a::'a event list) ≤ b" and "b ≤ c" and "c ≤ a" hence "b = c" by auto}
note jj=this
from jj[OF mono_trace_hide[OF hh, of B],
OF mono_trace_hide[THEN mono_trace_hide, of "f' m" "f' (m + i)" B A,
OF gg[THEN conjunct1, THEN strict_mono_mono,
THEN monoD, of "m" "m+i", simplified]]]
mono_trace_hide[OF ll, of B]
show ?case unfolding "3a"(6) [THEN spec, of k] by simp
qed
qed
qed
qed
qed
lemma Hiding_Un_D: ‹finite A ⟹ 𝒟 ((P \ A) \ B) = 𝒟 (P \ (A ∪ B))›
using Hiding_Un_D1 Hiding_Un_D2 by blast
subsection‹ Laws ›
lemma mono_Hiding_FD[simp]: ‹P ≤ Q ⟹ P \ A ≤ Q \ A›
apply (auto simp: le_ref_def F_Hiding D_Hiding)
using F_subset_imp_T_subset by blast+
lemmas mono_Hiding_ref = mono_Hiding
lemma Hiding_Un: ‹finite A ⟹ P \ (A ∪ B) = (P \ A) \ B›
proof (simp add:Process_eq_spec, intro conjI, unfold F_Hiding, goal_cases)
case 1
thus ?case (is "{(s, X). ?A s X} ∪ {(s, X). ?B s} =
{(s, X). (∃t. (?C1 s t ∧ (t, X ∪ ev ` B) ∈ ?C2 ∪ ?C3))} ∪ {(s, X). ?D s}")
proof(unfold F_Hiding set_eq_subset Un_subset_iff, intro conjI, goal_cases)
case 1
then show ?case
by (auto, metis (no_types) filter_filter image_Un sup_commute sup_left_commute)
next
case 2
then show ?case
by (rule_tac Un_mono[of "{}", simplified], insert Hiding_Un_D[of A P B], simp add: D_Hiding)
next
case 3
have "{(s, X). (∃t. (?C1 s t ∧ (t, X ∪ ev ` B) ∈ ?C2))} ⊆ {(s, X). ?A s X}"
by (auto, metis (no_types) filter_filter image_Un sup_commute sup_left_commute)
moreover have "{(s, X). (∃t. (?C1 s t ∧ (t, X ∪ ev ` B) ∈ ?C3))} ⊆ {(s, X). ?B s}"
proof(auto,goal_cases)
case (1 ta u)
then show ?case using Hiding_fronttickFree by blast
next
case (2 u f x)
then show ?case
apply(rule_tac x="f x" in exI, rule_tac x="trace_hide u (ev ` B)" in exI, auto)
using Hiding_fronttickFree apply blast
apply(erule_tac x=f in allE) by (metis (no_types) filter_filter rangeI)
qed
moreover have "{(s, X). (∃t. (?C1 s t ∧ (t, X ∪ ev ` B) ∈ ?C2 ∪ ?C3))} =
{(s, X). (∃t. (?C1 s t ∧ (t, X ∪ ev ` B) ∈ ?C2 ))} ∪
{(s, X). (∃t. (?C1 s t ∧ (t, X ∪ ev ` B) ∈ ?C3))}" by blast
ultimately show ?case by (metis (no_types, lifting) Un_mono)
next
case 4
then show ?case
by (rule_tac Un_mono[of "{}", simplified], insert Hiding_Un_D[of A P B], simp add:D_Hiding)
qed
next
case 2
then show ?case by (simp add: Hiding_Un_D)
qed
lemma Hiding_set_BOT: ‹(⊥ \ A) = ⊥›
apply(auto simp add:Process_eq_spec D_Hiding F_Hiding F_UU D_UU)
using Hiding_fronttickFree apply blast
using front_tickFree_append Hiding_tickFree apply blast
using front_tickFree_append Hiding_tickFree apply blast
apply (metis (full_types) append_Nil filter.simps(1) tickFree_Nil tickFree_implies_front_tickFree)
using front_tickFree_append Hiding_tickFree apply blast
using front_tickFree_append Hiding_tickFree apply blast
using tickFree_Nil by fastforce
lemma Hiding_set_STOP: ‹(STOP \ A) = STOP›
apply(auto simp add:Process_eq_spec D_Hiding F_Hiding F_STOP D_STOP T_STOP)
by (metis (full_types) lessI less_irrefl strict_mono_eq) +
lemma Hiding_set_SKIP: ‹(SKIP \ A) = SKIP›
apply(auto simp add:Process_eq_spec D_Hiding F_Hiding F_SKIP D_SKIP T_SKIP split:if_splits)
apply (metis filter.simps(1) non_tickFree_tick)
apply (metis (full_types) Hiding_tickFree n_not_Suc_n non_tickFree_tick strict_mono_eq)
apply (metis (full_types) Hiding_tickFree n_not_Suc_n non_tickFree_tick strict_mono_eq)
apply (metis event.distinct(1) filter.simps(1) imageE)
apply (metis event.distinct(1) filter.simps(1) filter.simps(2) imageE)
by (metis (full_types) Hiding_tickFree n_not_Suc_n non_tickFree_tick strict_mono_eq)
lemma Hiding_set_empty: ‹(P \ {}) = P›
apply(auto simp add:Process_eq_spec D_Hiding F_Hiding is_processT7 is_processT8_S strict_mono_eq)
by (metis append_Nil2 front_tickFree_implies_tickFree front_tickFree_single is_processT
nonTickFree_n_frontTickFree)
subsection‹ Multi-Operators laws ›
lemma Hiding_Ndet: ‹(P ⊓ Q) \ A = ((P \ A) ⊓ (Q \ A))›
proof(auto simp add:Process_eq_spec D_Hiding F_Hiding,
simp_all add: F_Ndet T_Ndet D_Ndet D_Hiding F_Hiding, goal_cases)
case (1 b t)
then show ?case by blast
next
case (2 b t u)
then show ?case by blast
next
case (3 b u f x)
from 3(4) have A:"infinite ({i. f i ∈ 𝒯 P}) ∨ infinite ({i. f i ∈ 𝒯 Q})"
using finite_nat_set_iff_bounded by auto
hence "(∀i. f i ∈ 𝒯 P) ∨ (∀i. f i ∈ 𝒯 Q)"
by (metis (no_types, lifting) 3(3) finite_nat_set_iff_bounded
is_processT3_ST_pref mem_Collect_eq not_less strict_mono_less_eq)
with A show ?case by (metis (no_types, lifting) 3(1,2,3,5) rangeI)
next
case (4 a b)
then show ?case by blast
next
case (5 t u)
then show ?case by blast
next
case (6 u f x)
from 6(4) have A:"infinite ({i. f i ∈ 𝒯 P}) ∨ infinite ({i. f i ∈ 𝒯 Q})"
using finite_nat_set_iff_bounded by auto
hence "(∀i. f i ∈ 𝒯 P) ∨ (∀i. f i ∈ 𝒯 Q)"
by (metis (no_types, lifting) 6(3) finite_nat_set_iff_bounded
is_processT3_ST_pref mem_Collect_eq not_less strict_mono_less_eq)
with A show ?case by (metis (no_types, lifting) 6(1,2,3,5) rangeI)
next
case (7 x)
then show ?case by blast
qed
lemma Hiding_Mprefix_distr:
‹(B ∩ A) = {} ⟹ ((Mprefix A P) \ B) = (Mprefix A (λx. ((P x) \ B)))›
proof (auto simp add: Process_eq_spec,
simp_all add: F_Mprefix T_Mprefix D_Mprefix D_Hiding F_Hiding,
goal_cases)
case (1 x b) then show ?case
proof(elim exE disjE conjE, goal_cases)
case (1 t)
then show ?case by (simp add: inf_sup_distrib2)
next
case (2 t a)
then show ?case
by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
imageE list.sel(1) list.sel(3) list.collapse neq_Nil_conv)
next
case (3 t u a)
hence "hd t ∉ ev ` B" by force
with 3 have"x = hd t # trace_hide (tl t) (ev ` B) @ u"
by (metis append_Cons filter.simps(2) list.exhaust_sel)
with 3 show ?case by (metis list.distinct(1) list.sel(1) list.sel(3) tickFree_tl)
next
case (4 t u f)
then obtain k where kk:"t = f k" by blast
from 4 obtain a where "f 1 ≠ [] ∧ ev a = hd (f 1)" and aa:"a ∈ A"
by (metis less_numeral_extra(1) nil_le not_less strict_mono_less_eq)
with 4(1) 4(6)[THEN spec, of 0] 4(7)[THEN spec, of 1] have "f 0 ≠ [] ∧ hd (f 0) = ev a"
apply auto
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject
filter.simps(2) hd_Cons_tl imageE list.distinct(1))
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.distinct(1))
by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.sel(1))
with 4(1, 7) aa have nf: "∀i. f i ≠ [] ∧ hd (f i) = ev a"
by (metis (mono_tags, opaque_lifting) "4"(5) append_Cons le_list_def le_simps(2) list.distinct(1)
list.exhaust_sel list.sel(1) neq0_conv old.nat.distinct(1) strict_mono_less_eq)
with 4(5) have sm:"strict_mono (tl ∘ f)" by (simp add: less_tail strict_mono_def)
with 4 aa kk nf show ?case
apply(rule_tac disjI2, intro conjI)
apply (metis (no_types, lifting) Nil_is_append_conv disjoint_iff_not_equal event.inject
filter.simps(2) hd_Cons_tl imageE list.distinct(1))
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl hd_append2 image_iff list.distinct(1) list.sel(1))
apply(rule_tac x=a in exI, intro conjI disjI2)
apply (metis disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl hd_append2 image_iff list.distinct(1) list.sel(1))
apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply (metis tickFree_tl)
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.distinct(1) list.sel(3) tl_append2)
apply(subst disj_commute, rule_tac disjCI)
apply(rule_tac x="tl ∘ f" in exI, intro conjI)
apply auto
apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
done
qed
next
case (2 x b)
then show ?case proof(elim exE disjE conjE, goal_cases)
case 1 then show ?case
apply(rule_tac disjI1, rule_tac x="[]" in exI)
by (simp add: disjoint_iff_not_equal inf_sup_distrib2)
next
case (2 a t) then show ?case
apply(rule_tac disjI1, rule_tac x="(ev a)#t" in exI)
using list.collapse by fastforce
next
case (3 a t u)
then show ?case
apply(rule_tac disjI2, rule_tac x="(ev a)#t" in exI, rule_tac x=u in exI)
using list.collapse by fastforce
next
case (4 a t u f)
then show ?case
apply(rule_tac disjI2)
apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp)
apply auto[1]
using hd_Cons_tl apply fastforce
apply(rule_tac disjI2, rule_tac x="λi. (ev a) # (f i)" in exI)
by (auto simp add: less_cons strict_mono_def)
qed
next
case (3 x) then show ?case
proof(elim exE disjE conjE, goal_cases)
case (1 t u a)
hence aa: "hd (trace_hide t (ev ` B)) = ev a ∧ trace_hide t (ev ` B) ≠ []"
by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) hd_Cons_tl
imageE list.distinct(1) list.sel(1))
with 1 have "hd x = ev a ∧ x ≠ []" by simp
with 1 show ?case
apply(intro conjI, simp_all, rule_tac x=a in exI, simp)
apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
using tickFree_tl apply blast
using aa by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.sel(3) tl_append2)
next
case (2 t u f)
then obtain k where kk:"t = f k" by blast
from 2 obtain a where "f 1 ≠ [] ∧ ev a = hd (f 1)" and aa:"a ∈ A"
by (metis less_numeral_extra(1) nil_le not_less strict_mono_less_eq)
with 2(1) 2(6)[THEN spec, of 0] 2(7)[THEN spec, of 1] have "f 0 ≠ [] ∧ hd (f 0) = ev a"
apply auto
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject
filter.simps(2) hd_Cons_tl imageE list.distinct(1))
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.distinct(1))
by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.sel(1))
with 2(1, 7) aa have nf: "∀i. f i ≠ [] ∧ hd (f i) = ev a"
by (metis (mono_tags, opaque_lifting) 2(5) append_Cons le_list_def le_simps(2) list.distinct(1)
list.exhaust_sel list.sel(1) neq0_conv old.nat.distinct(1) strict_mono_less_eq)
with 2(5) have sm:"strict_mono (tl ∘ f)" by (simp add: less_tail strict_mono_def)
from 2(1,4) nf aa kk have x1:"x ≠ []"
by (metis Nil_is_append_conv disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.distinct(1))
with 2(1,4) nf aa kk have x2: "hd (trace_hide t (ev ` B)) = ev a ∧ trace_hide t (ev ` B) ≠ []"
by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) hd_Cons_tl
imageE list.distinct(1) list.sel(1))
with 2(1,4) nf aa kk x1 have x3:"hd x = ev a" by simp
with 2 aa kk nf sm x1 show ?case
apply(intro conjI, simp_all)
apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply (metis tickFree_tl)
apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
hd_Cons_tl imageE list.distinct(1) list.sel(3) tl_append2)
apply(subst disj_commute, rule_tac disjCI)
apply(rule_tac x="tl ∘ f" in exI, intro conjI)
apply auto
apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
by (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
qed
next
case (4 x) then show ?case
proof(elim exE disjE conjE, goal_cases)
case (1 a t u)
then show ?case
apply(rule_tac x="(ev a)#t" in exI, rule_tac x=u in exI)
using list.collapse by fastforce
next
case (2 a t u f)
then show ?case
apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply auto[1]
using hd_Cons_tl apply fastforce
apply(rule_tac disjI2, rule_tac x="λi. (ev a) # (f i)" in exI)
by (auto simp add: less_cons strict_mono_def)
qed
qed
lemma no_Hiding_read: ‹(∀y. c y ∉ B) ⟹ ((c❙?x → (P x)) \ B) = (c❙?x → ((P x) \ B))›
by (simp add: read_def o_def, subst Hiding_Mprefix_distr, auto)
lemma no_Hiding_write0: ‹a ∉ B ⟹ ((a → P) \ B) = (a → (P \ B))›
by (simp add: Hiding_Mprefix_distr write0_def)
lemma Hiding_write0: ‹a ∈ B ⟹ ((a → P) \ B) = (P \ B)›
proof (auto simp add: write0_def Process_eq_spec,
simp_all add: F_Mprefix T_Mprefix D_Mprefix D_Hiding F_Hiding,
goal_cases)
case (1 x b)
then show ?case
apply(elim exE disjE conjE)
apply (metis filter.simps(2) hd_Cons_tl image_eqI)
apply (metis (no_types, lifting) filter.simps(2) image_eqI list.sel(1)
list.sel(3) neq_Nil_conv tickFree_tl)
proof(goal_cases)
case (1 t u f)
have fS: "strict_mono (f ∘ Suc)" by (metis "1"(5) Suc_mono comp_def strict_mono_def)
from 1 have aa:"∀i. f (Suc i) ≠ []"
by (metis (full_types) less_Suc_eq_le less_irrefl nil_le strict_mono_less_eq)
with fS have sm:"strict_mono (tl ∘ f ∘ Suc)" by (simp add: less_tail strict_mono_def)
with 1 aa show ?case
apply(subst disj_commute, rule_tac disjCI, simp)
apply(rule_tac x="tl (f 1)" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply (metis Hiding_tickFree imageE tickFree_tl)
apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl image_eqI rangeE)
apply(subst disj_commute, rule_tac disjCI)
apply(rule_tac x="tl ∘ f ∘ Suc" in exI, intro conjI)
apply auto
apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
done
qed
next
case (2 aa b)
then show ?case
apply(elim exE disjE conjE)
apply (metis (no_types, lifting) filter.simps(2) image_eqI list.distinct(1)
list.sel(1) list.sel(3))
proof(goal_cases)
case (1 t u)
then show ?case by (rule_tac disjI2, rule_tac x="(ev a)#t" in exI, auto)
next
case (2 t u f)
then show ?case
apply(rule_tac disjI2)
apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply(rule_tac disjI2)
apply(rule_tac x="λi. (ev a) # (f i)" in exI, intro conjI)
by (auto simp add: less_cons strict_mono_def)
qed
next
case (3 x)
then show ?case
apply(elim exE disjE conjE)
apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
using tickFree_tl apply blast
apply (metis filter.simps(2) hd_Cons_tl image_eqI)
proof(goal_cases)
case (1 t u f)
have fS: "strict_mono (f ∘ Suc)" by (metis "1"(5) Suc_mono comp_def strict_mono_def)
from 1 have aa:"∀i. f (Suc i) ≠ []"
by (metis (full_types) less_Suc_eq_le less_irrefl nil_le strict_mono_less_eq)
with fS have sm:"strict_mono (tl ∘ f ∘ Suc)" by (simp add: less_tail strict_mono_def)
with 1 aa show ?case
apply(rule_tac x="tl (f 1)" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply (metis Hiding_tickFree imageE tickFree_tl)
apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl image_eqI rangeE)
apply(subst disj_commute, rule_tac disjCI)
apply(rule_tac x="tl ∘ f ∘ Suc" in exI, intro conjI)
apply auto
apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
done
qed
next
case (4 x)
then show ?case
apply(elim exE disjE conjE)
proof(goal_cases)
case (1 t u)
then show ?case by (rule_tac x="(ev a)#t" in exI, auto)
next
case (2 t u f)
then show ?case
apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
apply(rule_tac disjI2)
apply(rule_tac x="λi. (ev a) # (f i)" in exI, intro conjI)
by (auto simp add: less_cons strict_mono_def)
qed
qed
lemma no_Hiding_write: ‹(∀y. c y ∉ B) ⟹ ((c❙!a → P) \ B) = (c❙!a → (P \ B))›
by(simp add: write_def, subst Hiding_Mprefix_distr, auto)
lemma Hiding_write: ‹(c a) ∈ B ⟹ ((c❙!a → P) \ B) = (P \ B)›
by (simp add: write_def Hiding_write0 Mprefix_singl)
section‹ The Sync Operator Laws ›
subsection‹ Preliminaries ›
lemma SyncTlEmpty:"a setinterleaves (([], u), A) ⟹ tl a setinterleaves (([], tl u), A)"
by (case_tac u, simp, case_tac a, simp_all split:if_splits)
lemma SyncHd_Tl:
"a setinterleaves ((t, u), A) ∧ hd t ∈ A ∧ hd u ∉ A
⟹ hd a = hd u ∧ tl a setinterleaves ((t, tl u), A)"
by (case_tac u) (case_tac t, auto split:if_splits)+
lemma SyncHdAddEmpty:
"(tl a) setinterleaves (([], u), A) ∧ hd a ∉ A ∧ a ≠ []
⟹ a setinterleaves (([], hd a # u), A)"
using hd_Cons_tl by fastforce
lemma SyncHdAdd:
"(tl a) setinterleaves ((t, u), A) ∧ hd a ∉ A ∧ hd t ∈ A ∧ a ≠ []
⟹ a setinterleaves ((t, hd a # u), A)"
by (case_tac a, simp, case_tac t, auto)
lemmas SyncHdAdd1 = SyncHdAdd[of "a#r", simplified] for a r
lemma SyncSameHdTl:
"a setinterleaves ((t, u), A) ∧ hd t ∈ A ∧ hd u ∈ A
⟹ hd t = hd u ∧ hd a = hd t ∧ (tl a) setinterleaves ((tl t, tl u), A)"
by (case_tac u) (case_tac t, auto split:if_splits)+
lemma SyncSingleHeadAdd:
"a setinterleaves ((t, u), A) ∧ h ∉ A
⟹ (h#a) setinterleaves ((h#t, u), A)"
by (case_tac u, auto split:if_splits)
lemma TickLeftSync:
"tick ∈ A ∧ front_tickFree t ∧ s setinterleaves (([tick], t), A) ⟹ s = t ∧ last t = tick"
proof(induct t arbitrary: s)
case Nil
then show ?case by (simp add: Nil.prems)
next
case (Cons a t)
then show ?case
apply (auto split:if_splits)
using emptyLeftProperty apply blast
apply (metis last_ConsR last_snoc nonTickFree_n_frontTickFree tickFree_Cons)
by (metis append_Cons append_Nil front_tickFree_mono)+
qed
lemma EmptyLeftSync:"s setinterleaves (([], t), A) ⟹ s = t ∧ set t ∩ A = {}"
by (meson Int_emptyI emptyLeftNonSync emptyLeftProperty)
lemma tick_T_F:"t@[tick] ∈ 𝒯 P ⟹ (t@[tick], X) ∈ ℱ P"
using append_T_imp_tickFree is_processT5_S7 by force
lemma event_set: "(e::'a event) ∈ insert tick (range ev)"
by (metis event.exhaust insert_iff rangeI)
lemma Mprefix_Sync_distr1_D:
" A ⊆ S
⟹ B ⊆ S
⟹ 𝒟 (Mprefix A P ⟦S⟧ Mprefix B Q) = 𝒟 (□ x ∈ A ∩ B → (P x ⟦S⟧ Q x))"
apply(auto,simp_all add:D_Sync F_Sync F_Mprefix T_Mprefix D_Mprefix)
apply(elim exE disjE conjE)
apply (metis (no_types, lifting) Sync.sym empty_iff image_iff insertI2
list.exhaust_sel setinterleaving.simps(2) subsetCE)
proof(goal_cases)
case (1 x t u r v a aa)
from 1(1,2,6,8,11,13) have aa1: "hd t∈insert tick (ev ` S)∧hd u∈insert tick (ev ` S)"
by blast
from 1(5,6,7,8,11,13) aa1 have aa2: " hd x ∈ ev ` (A ∩ B)"
by (metis (no_types, lifting) IntI empty_setinterleaving event.inject
hd_append2 image_iff SyncSameHdTl)
then show ?case
using 1(3,4,5,6,7,9,10,13,14) by (metis (no_types, lifting) Nil_is_append_conv aa1
empty_setinterleaving event.inject hd_append2
SyncSameHdTl tickFree_tl tl_append2)
next
case (2 x t u r v a)
then show ?case
by (metis (no_types, lifting) Sync.si_empty3 equals0D imageE image_eqI insertI2 list.exhaust_sel subsetCE)
next
case (3 x t u r v a aa)
from 3(1,2,6,8,11,13) have aa1: "hd t∈insert tick (ev ` S)∧hd u∈insert tick (ev ` S)"
by blast
from 3(5,6,7,8,11,13) aa1 have aa2: " hd x ∈ ev ` (A ∩ B)"
by (metis (no_types, lifting) IntI empty_setinterleaving event.inject hd_append2 image_iff SyncSameHdTl)
then show ?case
using 3(3,4,5,6,7,9,10,13,14)
by (metis (no_types, lifting) Nil_is_append_conv aa1 empty_setinterleaving event.inject
hd_append2 SyncSameHdTl tickFree_tl tl_append2)
next
case (4 x t u r v a)
then show ?case
by (metis (no_types, lifting) Sync.si_empty3 equals0D imageE image_eqI insertI2 list.exhaust_sel subsetCE)
next
case (5 x t u r v a aa)
from 5(1,2,6,8,11,13) have aa1: "hd t∈insert tick (ev ` S)∧hd u∈insert tick (ev ` S)"
by blast
from 5(5,6,7,8,11,13) aa1 have aa2: " hd x ∈ ev ` (A ∩ B)"
by (metis (no_types, lifting) IntI empty_setinterleaving event.inject hd_append2 image_iff SyncSameHdTl)
then show ?case
using 5(3,4,5,6,7,9,10,13,14) by (metis aa1 append_Nil2 empty_setinterleaving event.inject SyncSameHdTl)
next
case (6 x t u r v a)
then show ?case
by (metis (no_types, lifting) Sync.si_empty3 equals0D imageE image_eqI insertI2 list.exhaust_sel subsetCE)
next
case (7 x t u r v a aa)
from 7(1,2,6,8,11,13) have aa1: "hd t∈insert tick (ev ` S)∧hd u∈insert tick (ev ` S)"
by blast
from 7(5,6,7,8,11,13) aa1 have aa2: " hd x ∈ ev ` (A ∩ B)"
by (metis (no_types, lifting) IntI empty_setinterleaving event.inject hd_append2 image_iff SyncSameHdTl)
then show ?case
using 7(3,4,5,6,7,9,10,13,14) by (metis aa1 append_Nil2 empty_setinterleaving event.inject SyncSameHdTl)
next
case (8 x)
then show ?case
apply(elim exE disjE conjE)
proof(goal_cases)
case (1 a t u r v)
obtain r1 t1 u1 where aa0: "r1=hd x#r∧t1=hd x#t∧u1=hd x#u"
by auto
from 1(3,4,5,7,8,9) have aa1: "tickFree r1∧x = r1 @ v"
by (metis Cons_eq_appendI aa0 event.distinct(1) list.exhaust_sel tickFree_Cons)
from 1(2,4,9) have aa2: "r1 setinterleaves ((t1, u1), insert tick (ev ` S))∧t1 ≠ []"
using aa0 subsetCE by auto
from 1(4,5,10,11) aa0
have aa3: "(tl t1) ∈ 𝒟 (P a) ∧ (tl u1) ∈ 𝒯 (Q a) ∧ ev a = hd t1 ∧ ev a = hd u1