Theory Sync
section‹ The Synchronizing Operator ›
theory Sync
imports Process "HOL-Library.Infinite_Set"
begin
subsection‹Basic Concepts›
fun setinterleaving:: "'a trace × ('a event) set × 'a trace ⇒ ('a trace)set"
where
si_empty1: "setinterleaving([], X, []) = {[]}"
| si_empty2: "setinterleaving([], X, (y # t)) =
(if (y ∈ X)
then {}
else {z.∃ u. z = (y # u) ∧ u ∈ setinterleaving ([], X, t)})"
| si_empty3: "setinterleaving((x # s), X, []) =
(if (x ∈ X)
then {}
else {z.∃ u. z = (x # u) ∧ u ∈ setinterleaving (s, X, [])})"
| si_neq : "setinterleaving((x # s), X, (y # t)) =
(if (x ∈ X)
then if (y ∈ X)
then if (x = y)
then {z.∃ u. z = (x#u) ∧ u ∈ setinterleaving(s, X, t)}
else {}
else {z.∃ u. z = (y#u) ∧ u ∈ setinterleaving ((x#s), X, t)}
else if (y ∉ X)
then {z.∃ u. z = (x # u) ∧ u ∈ setinterleaving (s, X, (y # t))}
∪ {z.∃ u. z = (y # u) ∧ u ∈ setinterleaving((x # s), X, t)}
else {z.∃ u. z = (x # u) ∧ u ∈ setinterleaving (s, X, (y # t))})"
fun setinterleavingList::"'a trace × ('a event) set × 'a trace ⇒ ('a trace)list"
where
si_empty1l: "setinterleavingList([], X, []) = [[]]"
| si_empty2l: "setinterleavingList([], X, (y # t)) =
(if (y ∈ X)
then []
else map (λz. y#z) (setinterleavingList ([], X, t)))"
| si_empty3l: "setinterleavingList((x # s), X, []) =
(if (x ∈ X)
then []
else map (λz. x#z) (setinterleavingList (s, X, [])))"
| si_neql : "setinterleavingList((x # s), X, (y # t)) =
(if (x ∈ X)
then if (y ∈ X)
then if (x = y)
then map (λz. x#z) (setinterleavingList(s, X, t))
else []
else map (λz. y#z) (setinterleavingList ((x#s), X, t))
else if (y ∉ X)
then map (λz. x#z) (setinterleavingList (s, X, (y # t)))
@ map (λz. y#z) (setinterleavingList ((x#s), X, t))
else map (λz. x#z) (setinterleavingList (s, X, (y # t))))"
lemma finiteSetinterleavingList: "finite (set (setinterleavingList(s, X, t)))"
by auto
lemma sym : "setinterleaving(s, X, t)= setinterleaving(t, X, s)"
by (rule setinterleaving.induct[of "λ(s,X,t). setinterleaving (s, X, t)
= setinterleaving (t, X, s)" "(s, X, t)", simplified], auto)
abbreviation "setinterleaves_syntax" ("_ setinterleaves '(()'(_, _')(), _')" [60,0,0,0]70)
where "u setinterleaves ((s, t), X) == (u ∈ setinterleaving(s, X, t))"
subsection‹Definition›
definition Sync :: "['a process,'a set,'a process] => 'a process" ("(3(_ ⟦_⟧/ _))" [64,0,65] 64)
where "P ⟦ A ⟧ Q ≡ Abs_process({(s,R).∃ t u X Y. (t,X) ∈ ℱ P ∧ (u,Y) ∈ ℱ Q ∧
(s setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y} ∪
{(s,R).∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧
s = r@v ∧
(r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)},
{s. ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧
s = r@v ∧
(r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)})"
subsection‹Consequences›
lemma emptyLeftProperty:"∀s. s setinterleaves (([], t), A)⟶s=t"
apply(induct_tac t)
apply simp
by auto
lemma emptyLeftSelf: " (∀t1. t1∈ set t⟶t1∉A)⟶t setinterleaves (([], t), A) "
apply(induct_tac t)
apply simp
by auto
lemma emptyLeftNonSync: "∀s. s setinterleaves (([], t), A)⟶(∀t1. t1∈ set t⟶t1∉A)"
apply(induct_tac t)
apply simp
proof-
fix a list
assume a: "∀s. s setinterleaves (([], list), A) ⟶ (∀t1. t1 ∈ set list ⟶ t1 ∉ A)"
thus "∀s. s setinterleaves (([], a # list), A) ⟶ (∀t1. t1 ∈ set (a # list) ⟶ t1 ∉ A)"
proof-
have th: "s setinterleaves (([], a # list), A)⟶a∉A" by auto
obtain s1 where th1: "s setinterleaves (([], a # list), A)⟶s1 setinterleaves (([], list), A)"
using mem_Collect_eq th by fastforce
from a th1 have th2: "∀s. s setinterleaves (([], a # list), A)⟶(∀t. t∈ set list⟶t ∉ A)"
by auto
with a show ?thesis
by (metis (no_types, lifting) empty_iff set_ConsD setinterleaving.simps(2))
qed
qed
lemma ftf_Sync1: "a ∉ set(u) ∧ a ∉ set(t) ∧ s setinterleaves ((t, u), A) ⟶ a ∉ set(s)"
proof (induction "length t + length u" arbitrary:s t u rule:nat_less_induct)
case 1
show ?case
apply(cases t) using sym emptyLeftProperty apply blast
apply(cases u) using sym emptyLeftProperty apply blast
apply(simp split:if_splits, intro conjI impI, elim conjE disjE exE)
apply (metis "1.hyps" add_less_le_mono length_Cons lessI order_refl set_ConsD)
apply (metis "1.hyps" add_Suc_right length_Cons lessI set_ConsD)
apply (metis "1.hyps" add_less_mono length_Cons lessI set_ConsD)
apply (metis "1.hyps" add_Suc_right length_Cons lessI set_ConsD)
apply (metis (no_types, opaque_lifting) "1.hyps" add.commute add_Suc_right insert_iff
length_Cons lessI list.simps(15))
by (metis "1.hyps" add_less_le_mono length_Cons lessI order_refl set_ConsD)
qed
lemma addNonSyncEmpty: "sa setinterleaves (([], u), A) ∧ y1 ∉ A ⟶
(sa @ [y1]) setinterleaves (([y1], u), A) ∧ (sa @ [y1]) setinterleaves (([], u @ [y1]), A)"
proof (induction "length u" arbitrary:sa u rule:nat_less_induct)
case 1
then show ?case
apply(cases u)
apply simp
proof-
fix a list
assume a: "∀m<length u. ∀x. m = length x ⟶(∀xa. xa setinterleaves (([], x), A) ∧ y1 ∉ A ⟶
(xa @ [y1]) setinterleaves (([y1], x), A) ∧ (xa @ [y1]) setinterleaves (([], x @ [y1]), A))"
and b: "u = a # list"
from b have th: "sa setinterleaves (([], u), A)⟹(tl sa) setinterleaves (([], list), A)"
by (metis emptyLeftNonSync emptyLeftProperty emptyLeftSelf list.distinct(1) list.sel(3)
list.set_sel(2))
from a b th have th1: "sa setinterleaves (([], u), A) ∧ y1 ∉ A⟶ ((tl sa) @ [y1])
setinterleaves (([y1], list), A)∧((tl sa)@[y1]) setinterleaves (([], list@[y1]), A)" by auto
thus "sa setinterleaves (([], u), A) ∧ y1 ∉ A ⟶
(sa @ [y1]) setinterleaves (([y1], u), A) ∧ (sa @ [y1]) setinterleaves (([], u @ [y1]), A)"
using b th by auto
qed
qed
lemma addNonSync: "sa setinterleaves ((t,u),A)∧ y1 ∉ A⟶
(sa@[y1]) setinterleaves ((t@[y1],u),A)∧(sa@[y1]) setinterleaves ((t,u@[y1]),A)"
proof (induction "length t + length u" arbitrary:sa t u rule:nat_less_induct)
case 1
then show ?case
apply(cases t)
apply (simp add: addNonSyncEmpty)
apply (cases u)
apply (metis Sync.sym addNonSyncEmpty append_self_conv2)
proof-
fix a list aa lista
assume a: "∀m<length t + length u. ∀x xa. m = length x + length xa ⟶
(∀xb. xb setinterleaves ((x, xa), A) ∧ y1 ∉ A ⟶(xb @ [y1]) setinterleaves ((x @ [y1], xa), A)
∧ (xb @ [y1]) setinterleaves ((x, xa @ [y1]), A))"
and b: " t = a # list"
and c: "u = aa # lista"
thus " sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u), A) ∧ (sa @ [y1]) setinterleaves ((t, u @ [y1]), A)"
proof-
from b c have th0pre: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
(tl sa) setinterleaves ((list,lista), A)" by auto
from th0pre a b c have th0pre1: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∉ A⟹
((tl sa) @ [y1]) setinterleaves ((list@ [y1], lista), A)∧
((tl sa) @ [y1]) setinterleaves ((list, lista@ [y1]), A)"
by (metis add_less_mono length_Cons lessI)
from th0pre th0pre1 b c have th0: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u), A)∧(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)"
by auto
from b c have th1pre: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
(tl sa) setinterleaves ((list,aa#lista), A)" by auto
from th1pre a b c have th1pre1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∉ A⟹
((tl sa) @ [y1]) setinterleaves ((list@ [y1], aa#lista), A)∧
((tl sa) @ [y1]) setinterleaves ((list, aa#lista@ [y1]), A)"
by (metis add_Suc append_Cons length_Cons lessI)
from th1pre th1pre1 b c have th1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u), A)∧(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)"
by auto
from b c have th2pre: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ⟹
(tl sa) setinterleaves ((a#list,lista), A)" by auto
from th2pre a b c have th2pre1: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∉ A⟹
((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista), A)∧
((tl sa) @ [y1]) setinterleaves ((a#list, lista@ [y1]), A)"
by (metis add_Suc_right append_Cons length_Cons lessI)
from th2pre th2pre1 b c have th2: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∉ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u), A)∧(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)"
by auto
from b c have th3pre: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)⟹
(tl sa) setinterleaves ((a#list,lista), A)∨(tl sa)setinterleaves ((list,aa#lista), A)" by auto
from th3pre a b c have th3pre1: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
(tl sa) setinterleaves ((a#list,lista), A)∧ y1 ∉ A ⟹
((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista ), A)∧((tl sa) @ [y1]) setinterleaves
((a#list, lista@ [y1] ), A)"
by (metis add_Suc_right append_Cons length_Cons lessI)
from th3pre a b c have th3pre2: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
(tl sa) setinterleaves ((list,aa#lista), A)∧ y1 ∉ A ⟹((tl sa) @ [y1]) setinterleaves
((list@ [y1], aa#lista ), A)∧((tl sa) @ [y1]) setinterleaves ((list, aa#lista @ [y1]), A)"
by (metis add_Suc append_Cons length_Cons lessI)
from th3pre th3pre1 th3pre2 a b c have th3: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A) ∧
y1 ∉ A ⟶(sa @ [y1]) setinterleaves ((t @ [y1], u), A) ∧
(sa @ [y1]) setinterleaves ((t, u @ [y1]), A)" by auto
show ?thesis
using b c th0 th1 th2 th3 by auto
qed
qed
qed
lemma addSyncEmpty: "sa setinterleaves (([], u), A) ∧ y1 ∈ A ⟶
(sa @ [y1]) setinterleaves (([y1], u @ [y1]), A)"
proof (induction "length u" arbitrary:sa u rule:nat_less_induct)
case 1
then show ?case
apply(cases u)
apply simp
proof-
fix a list
assume a: "∀m<length u. ∀x. m = length x ⟶(∀xa. xa setinterleaves (([], x), A) ∧ y1 ∈ A
⟶ (xa @ [y1]) setinterleaves (([y1], x @ [y1]), A))"
and b: "u = a # list"
from b have th: "sa setinterleaves (([], u), A)⟹(tl sa) setinterleaves (([], list), A)"
by (metis emptyLeftNonSync emptyLeftProperty emptyLeftSelf list.distinct(1) list.sel(3)
list.set_sel(2))
from a th have th1: "sa setinterleaves (([], u), A) ∧ y1 ∈ A⟹
((tl sa) @ [y1]) setinterleaves (([y1], list @ [y1]), A)" using b by auto
thus "sa setinterleaves (([], u), A) ∧ y1 ∈ A ⟶
(sa @ [y1]) setinterleaves (([y1], u @ [y1]), A)" using b th by auto
qed
qed
lemma addSync: "sa setinterleaves ((t,u),A)∧ y1 ∈ A⟶(sa@[y1]) setinterleaves ((t@[y1],u@[y1]),A)"
proof (induction "length t + length u" arbitrary:sa t u rule:nat_less_induct)
case 1
then show ?case
apply(cases t)
apply (simp add: addSyncEmpty)
apply(cases u)
apply (metis Sync.sym addSyncEmpty append.left_neutral)
proof-
fix a list aa lista
assume a: "∀m<length t + length u. ∀x xa. m = length x + length xa ⟶
(∀xb. xb setinterleaves ((x, xa), A) ∧ y1 ∈ A ⟶ (xb @ [y1]) setinterleaves
((x @ [y1], xa @ [y1]), A))"
and b: "t = a # list "
and c: " u = aa # lista"
thus "sa setinterleaves((t, u),A)∧y1 ∈A⟶(sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)"
proof-
from b c have th0pre: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
(tl sa) setinterleaves ((list,lista), A)" by auto
from th0pre a b c have th0pre1: "a=aa∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∈ A⟹
((tl sa) @ [y1]) setinterleaves ((list@ [y1], lista @ [y1]), A)"
by (metis add_less_mono length_Cons lessI)
from th0pre th0pre1 b c have th0: "a=aa∧a∈A⟹sa setinterleaves ((t, u), A) ∧ y1 ∈ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto
from b c have th1pre: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ⟹
(tl sa) setinterleaves ((list,aa#lista), A)" by auto
from th1pre a b c have th1pre1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∈ A⟹
((tl sa) @ [y1]) setinterleaves ((list@ [y1], aa#lista @ [y1]), A)"
by (metis add_Suc append_Cons length_Cons lessI)
from th1pre th1pre1 b c have th1: "a∉A∧aa∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∈ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto
from b c have th2pre: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ⟹
(tl sa) setinterleaves ((a#list,lista), A)" by auto
from th2pre a b c have th2pre1: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A)∧ y1 ∈ A⟹
((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista @ [y1]), A)"
by (metis add_Suc_right append_Cons length_Cons lessI)
from th2pre th2pre1 b c have th2: "aa∉A∧a∈ A⟹sa setinterleaves ((t, u), A) ∧ y1 ∈ A ⟶
(sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto
from b c have th3pre: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)⟹
(tl sa) setinterleaves((a#list,lista), A)∨(tl sa)setinterleaves ((list,aa#lista), A)" by auto
from th3pre a b c have th3pre1: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
(tl sa) setinterleaves ((a#list,lista), A)∧ y1 ∈ A ⟹
((tl sa) @ [y1]) setinterleaves ((a#list@ [y1], lista @ [y1]), A)"
by (metis add_Suc_right append_Cons length_Cons lessI)
from th3pre a b c have th3pre2: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A)∧
(tl sa) setinterleaves ((list,aa#lista), A)∧ y1 ∈ A ⟹
((tl sa) @ [y1]) setinterleaves ((list@ [y1], aa#lista @ [y1]), A)"
by (metis add_Suc append_Cons length_Cons lessI)
from th3pre th3pre1 th3pre2 a b c have th3: "aa∉A∧a∉ A⟹sa setinterleaves ((t, u), A) ∧
y1 ∈ A ⟶ (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)" by auto
show ?thesis
using b c th0 th1 th2 th3 by auto
qed
qed
qed
lemma doubleReverse: "s1 setinterleaves ((t, u), A)⟶(rev s1) setinterleaves ((rev t, rev u), A)"
proof (induction "length t + length u" arbitrary:s1 t u rule:nat_less_induct)
case 1
then show ?case
apply(cases t)
using emptyLeftNonSync
apply (metis emptyLeftProperty emptyLeftSelf rev.simps(1) set_rev)
apply(cases u)
using sym
apply (metis (no_types, lifting) emptyLeftNonSync emptyLeftProperty emptyLeftSelf
rev.simps(1) set_rev)
proof-
fix a list aa lista
assume a: "∀m<length t + length u. ∀x xa. m = length x + length xa ⟶
(∀xb. xb setinterleaves ((x, xa), A) ⟶rev xb setinterleaves ((rev x, rev xa), A))"
and b: "t = a # list"
and c: "u = aa # lista"
thus "s1 setinterleaves ((t, u), A) ⟶rev s1 setinterleaves ((rev t, rev u), A)"
proof-
from b c have th0pre: "a=aa∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
(tl s1) setinterleaves ((list,lista), A)" by auto
from th0pre a b c have th0pre1: "a=aa∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
((rev (tl s1)) setinterleaves ((rev list, rev lista), A))"
by (metis add_less_mono length_Cons lessI)
from th0pre th0pre1 b c have th0: "a=aa∧aa∈ A⟹s1 setinterleaves ((t, u), A) ⟶
rev s1 setinterleaves ((rev t, rev u), A)" using addSync by fastforce
from b c have th1pre: "a∉A∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
(tl s1) setinterleaves ((list,aa#lista), A)" by auto
from th1pre a b c have th1pre1: "a∉A∧aa∈ A⟹s1 setinterleaves ((t, u), A)⟹
((rev (tl s1)) setinterleaves ((rev list, rev (aa#lista)), A))"
by (metis add_less_mono1 length_Cons lessI)
from th1pre th1pre1 b c have th1: "a∉A∧aa∈ A⟹s1 setinterleaves ((t, u), A) ⟶
rev s1 setinterleaves ((rev t, rev u), A)" using addNonSync by fastforce
from b c have th2pre: "aa∉A∧a∈ A⟹s1 setinterleaves ((t, u), A)⟹
(tl s1) setinterleaves ((a#list,lista), A)" by auto
from th2pre a b c have th2pre1: "aa∉A∧a∈ A⟹s1 setinterleaves ((t, u), A)⟹
((rev (tl s1)) setinterleaves ((rev (a#list), rev lista), A))"
by (metis add_Suc_right length_Cons lessI)
from th2pre th2pre1 b c have th2: "aa∉A∧a∈ A⟹s1 setinterleaves ((t, u), A) ⟶
rev s1 setinterleaves ((rev t, rev u), A)"
using addNonSync by fastforce
from b c have th3pre: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)⟹
(tl s1) setinterleaves ((a#list,lista),A)∨(tl s1) setinterleaves((list,aa#lista), A)" by auto
from th3pre a b c have th3pre1: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
(tl s1) setinterleaves ((a#list,lista), A) ⟹
((rev (tl s1)) setinterleaves ((rev (a#list), rev (lista)), A))"
by (metis add_Suc_right length_Cons lessI)
from th3pre a b c have th3pre2: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
(tl s1) setinterleaves ((list,aa#lista), A) ⟹
((rev (tl s1)) setinterleaves ((rev (list), rev (aa#lista)), A))"
by (metis add_less_mono1 length_Cons lessI)
from th3pre1 have th3pre31: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
((rev (tl s1)) setinterleaves ((rev (a#list), rev (lista)), A))⟶
((rev (tl s1))@[aa]) setinterleaves ((rev (a#list), (rev (lista))@[aa]), A)"
by (simp add: addNonSync)
from th3pre2 have th3pre32: "aa∉A∧a∉ A⟹s1 setinterleaves ((t, u), A)∧
((rev (tl s1)) setinterleaves ((rev (list), rev (aa#lista)), A))⟶
((rev (tl s1))@[a]) setinterleaves (((rev (list)@[a]), (rev (aa#lista))), A)"
by (simp add: addNonSync)
from th3pre th3pre1 th3pre2 th3pre31 th3pre32 a b c have th3: "aa∉A∧a∉ A⟹
s1 setinterleaves ((t, u), A) ⟶rev s1 setinterleaves ((rev t, rev u), A)" by force
show?thesis
using b c th0 th1 th2 th3 by auto
qed
qed
qed
lemma ftf_Sync21: "(a∈set(u)∧a∉set(t)∨a∈set(t)∧a∉set(u))∧a∈A⟶setinterleaving(u, A ,t)= {}"
proof (induction "length t + length u" arbitrary: t u rule:nat_less_induct)
case 1
then show ?case
apply(cases t)
using Sync.sym emptyLeftNonSync apply fastforce
apply(cases u)
apply auto[1]
apply(simp split:if_splits, intro conjI impI, elim conjE disjE exE)
apply blast
apply auto[1]
apply blast
apply auto[1]
apply auto[1]
using less_SucI apply blast
apply auto[1]
apply auto[1]
using list.simps(15) apply auto[1]
by auto
qed
lemma ftf_Sync32: "u=u1@[tick]∧t=t1@[tick]∧s setinterleaves ((t, u), insert tick (ev ` A))⟹
∃s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))∧ (s=s1@[tick])"
proof-
assume h: "u=u1@[tick]∧t=t1@[tick]∧s setinterleaves ((t, u), insert tick (ev ` A))"
thus "∃s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))∧ (s=s1@[tick])"
proof-
from h have a:"rev u=tick#rev u1" by auto
from h have b:"rev t=tick#rev t1" by auto
from h have ab: "(rev s) setinterleaves ((tick#rev t1, tick#rev u1), insert tick (ev ` A))"
using doubleReverse by fastforce
from h obtain ss where c: "ss setinterleaves ((rev t1, rev u1), insert tick (ev ` A))∧
ss=tl(rev s)" using ab by auto
from c have d: "(rev ss) setinterleaves (( t1, u1), insert tick (ev ` A))"
using doubleReverse by fastforce
from d have e: "rev s=tick#ss"
using ab append_Cons_eq_iff c by auto
show ?thesis
using d e by blast
qed
qed
lemma SyncWithTick_imp_NTF:
"(s @ [tick]) setinterleaves ((t, u),insert tick (ev ` A))
⟹ t∈ 𝒯 P ⟹ u ∈ 𝒯 Q
⟹ ∃t1 u1. t=t1@[tick] ∧ u=u1@[tick]∧ s setinterleaves ((t1, u1), insert tick (ev ` A))"
proof-
assume h: "(s @ [tick]) setinterleaves ((t, u), insert tick (ev ` A))"
and h1: "t∈ 𝒯 P"
and h2: "u∈ 𝒯 Q"
thus "∃t1 u1. t=t1@[tick] ∧ u=u1@[tick]∧ s setinterleaves ((t1, u1), insert tick (ev ` A))"
proof-
from h have a: "(tick#rev s) setinterleaves ((rev t, rev u), insert tick (ev ` A))"
using doubleReverse by fastforce
from h obtain tt uu where b: "t=tt@[tick]∧u=uu@[tick]"
by (metis T_nonTickFree_imp_decomp empty_iff ftf_Sync1 ftf_Sync21 h1 h2 insertI1
non_tickFree_tick tickFree_append tickFree_def)
from h b have d: "s setinterleaves ((tt, uu), insert tick (ev ` A))"
using ftf_Sync32 by blast
show ?thesis
using b d by blast
qed
qed
lemma synPrefix1:
" ta = []
⟹ ∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶
t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"
proof-
assume a: "ta = []"
obtain u1 where th: "u1=s" by blast
from a have th2: "(s @ t) setinterleaves ((ta, u), A) ⟶ (s @ t)= u"
by (simp add: a emptyLeftProperty)
from a have th3: "(s @ t) setinterleaves ((ta, u), A) ⟶ (∀t1. t1∈set u⟶t1∉A)"
by (simp add: emptyLeftNonSync)
from a th have th1: "(s @ t) setinterleaves ((ta, u), A) ⟶ [] ≤ ta ∧ u1 ≤ u "
using le_list_def th2 by blast
from a th have thh1: "(s @ t) setinterleaves ((ta, u), A)∧ (∀t1. t1∈set u1⟶t1∉A) ⟶
s setinterleaves (([], u1), A)" by (simp add: emptyLeftSelf)
thus "∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ t1 ≤ ta ∧ u1 ≤ u ∧
s setinterleaves ((t1, u1), A)" using th th1 th2 th3 thh1 by fastforce
qed
lemma synPrefix: "∃t1 u1. (s @ t) setinterleaves ((ta, u), A)⟶
t1≤ta∧u1≤u∧s setinterleaves ((t1, u1), A)"
proof (induction "length ta + length u" arbitrary: s t ta u rule:nat_less_induct)
case 1
then show ?case
apply(cases ta)
using synPrefix1 apply fastforce
apply(cases u)
using sym synPrefix1 apply metis
proof-
fix a list aa lista s t
assume a: " ∀m<length ta + length u. ∀x xa. m = length x + length xa ⟶
(∀xb xc. ∃t1 u1. (xb @ xc) setinterleaves ((x, xa), A) ⟶
t1 ≤ x ∧ u1 ≤ xa ∧ xb setinterleaves ((t1, u1), A))"
and b: "ta = a # list"
and c: "u = aa # lista "
thus " ∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶ t1 ≤ ta ∧ u1 ≤ u ∧
s setinterleaves ((t1, u1), A)"
proof-
from a have th0: "∀xb xc. ∃t1 u1. (xb @ xc) setinterleaves ((list, lista), A) ⟶
t1 ≤ list ∧ u1 ≤ lista ∧ xb setinterleaves ((t1, u1), A)"
by (metis add_less_le_mono b c impossible_Cons le_cases not_le_imp_less)
from b c obtain yb where thp: "a=aa∧a∈ A∧(s@t) setinterleaves ((ta, u), A)∧length s >1 ⟹
yb=tl s" by blast
with b c have thp4: "a=aa∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s >1 ⟹s=a#yb"
by (auto, metis Cons_eq_append_conv list.sel(3) list.size(3) not_less0)
have thp5: "a=aa∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s >1 ⟹
(yb @ t) setinterleaves ((list, lista), A)" using b c thp4 by auto
from th0 obtain yt yu where thp1: "a = aa ∧ a ∈ A ⟹ (s @ t) setinterleaves ((ta, u), A) ∧
1 < length s⟹yb setinterleaves ((yt, yu), A)∧yt≤list∧yu≤lista" using thp5 by blast
from thp thp1 have thp2: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A)∧ length s >1⟶
s setinterleaves ((a#yt, aa#yu), A)" using thp4 by auto
from b c have thp3: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A) ∧ length s=1⟶
s setinterleaves (([a], [aa]), A)"
using append_eq_append_conv2[of s t "[aa]"] by (auto, metis append_Nil2
append_eq_append_conv length_Cons list.size(3))
have thp6: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A) ∧ length s=0⟶
s setinterleaves (([], []), A)" by auto
from thp1 have thp7: "a=aa∧a∈ A⟹ (s @ t) setinterleaves ((ta, u), A)∧ length s >1⟹
(a # yt)≤ta ∧(aa # yu)≤u" by (metis b c le_less less_cons)
have th: "a=aa∧a∈ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶
t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"
proof -
assume dd:"a=aa ∧ a∈ A"
consider (aa) "length s = 0" | (bb) "length s = 1" | (cc) "length s > 1"
by linarith
then show ?thesis
proof cases
case aa
with thp6 show ?thesis
by (rule_tac x="[]" in exI, rule_tac x="[]" in exI, simp)
next
case bb
with dd thp3 b c show ?thesis
by (rule_tac x="[a]" in exI, rule_tac x="[a]" in exI, auto simp add: le_list_def)
next
case cc
with dd thp2 thp7 b c show ?thesis
by (rule_tac x="a#yt" in exI, rule_tac x="a#yu" in exI, auto simp add: le_list_def)
qed
qed
from b c have th1pre: "a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A) ⟶
tl (s @ t) setinterleaves ((list, u), A)∧hd (s@t)=a" by auto
from a b c obtain yt1 yu1 where th1pre1: "a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
length s>0⟶yt1≤list∧ yu1 ≤ u∧ tl s setinterleaves ((yt1, yu1), A)"
by (metis (no_types, lifting) length_Cons length_greater_0_conv lessI plus_nat.simps(2)
th1pre tl_append2)
from b have th1pre2: "yt1≤list⟶a#yt1≤ta"
by (simp add: le_less less_cons)
from b c have th1pre3: "a∉A∧aa∈ A∧tl s setinterleaves ((yt1, yu1), A)⟶
(a#(tl s)) setinterleaves ((a#yt1, yu1), A)"
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from b c th1pre1 th1pre2 have th1pre4: "a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
length s>0 ⟶a#yt1≤ta∧ yu1 ≤u∧ s setinterleaves ((a#yt1, yu1), A)"
using th1pre th1pre3 by fastforce
have th1pre5:"a∉A∧aa∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s=0 ⟶[]≤ta∧ [] ≤u∧
s setinterleaves (([], []), A)" by auto
have th1: "a∉A∧aa∈ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶
t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)" using th1pre4 th1pre5 by blast
from b c have th2pre: "aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A) ⟶
tl (s @ t) setinterleaves ((ta, lista), A)∧hd (s@t)=aa" by auto
from a b c obtain yt2 yu2 where th2pre1: "aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
length s>0⟶yt2≤ta∧ yu2 ≤ lista∧ (tl s) setinterleaves ((yt2, yu2), A)"
by (metis (no_types, lifting) add_Suc_right length_Cons length_greater_0_conv lessI
th2pre tl_append2)
from c have th2pre2: "yu2≤lista⟶aa#yu2≤u"
by (simp add: le_less less_cons)
from b c have th2pre3: "aa∉A∧a∈ A∧tl s setinterleaves ((yt2, yu2), A)⟶
(aa#(tl s)) setinterleaves ((yt2, aa#yu2), A)"
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from b c th2pre1 th2pre2 have th2pre4: "aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧
length s>0 ⟶yt2≤ta∧ aa#yu2 ≤u∧ s setinterleaves ((yt2, aa#yu2), A)"
using th2pre th2pre3 by fastforce
have th2pre5:"aa∉A∧a∈ A∧(s @ t) setinterleaves ((ta, u), A)∧length s=0 ⟶
[]≤ta∧ [] ≤u∧ s setinterleaves (([], []), A)" by auto
have th2: "aa∉A∧a∈ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶
t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)" using th2pre4 th2pre5 by blast
from b c have th3pre: "aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)⟶tl (s @ t)
setinterleaves ((ta, lista), A)∧hd (s@t)=aa∨tl (s @ t)setinterleaves((list, u), A)∧hd(s@t)=a"
by auto
from a b c th3pre obtain yt31 yu31 where th3pre1: "aa∉A∧a∉ A∧
(s @ t) setinterleaves ((ta, u), A)∧tl (s @ t) setinterleaves ((ta, lista), A)∧
hd (s@t)=aa∧length s>0⟶yt31≤ta∧ yu31 ≤ lista∧ (tl s) setinterleaves ((yt31, yu31), A)"
by(metis(no_types,lifting)add_Suc_right length_Cons length_greater_0_conv lessI tl_append2)
from a b c th3pre obtain yt32 yu32 where th3pre2: "aa∉A∧a∉A∧(s@t)setinterleaves ((ta, u),A)∧
tl (s @ t) setinterleaves ((list, u), A)∧hd (s@t)=a∧length s>0⟶yt32≤list∧ yu32 ≤u∧
(tl s) setinterleaves ((yt32, yu32), A)"
by (metis add_less_mono1 impossible_Cons le_neq_implies_less length_greater_0_conv
nat_le_linear tl_append2)
from b c have th3pre3: "aa∉A∧a∉ A∧tl s setinterleaves ((yt31, yu31), A)⟶
(aa#(tl s)) setinterleaves ((yt31, aa#yu31), A)"
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from b c th3pre1 th3pre2 have th3pre4: "aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)∧
length s>0∧tl (s @ t) setinterleaves ((ta, lista), A)∧hd (s@t)=aa ⟶yt31≤ta∧ aa#yu31 ≤u∧
s setinterleaves ((yt31, aa#yu31), A)"
by (metis hd_append2 le_less length_greater_0_conv less_cons list.exhaust_sel th3pre3)
from b c have th3pre5: "aa∉A∧a∉ A∧tl s setinterleaves ((yt32, yu32), A)⟶
(a#(tl s)) setinterleaves ((a#yt32, yu32), A)"
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from b c th3pre1 th3pre2 have th3pre6: "aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)∧
length s>0∧tl (s @ t) setinterleaves ((list, u), A)∧hd (s@t)=a ⟶a#yt32≤ta∧ yu32 ≤u∧
s setinterleaves ((a#yt32, yu32), A)"
using th3pre th3pre5 by (metis hd_append2 le_less length_greater_0_conv less_cons
list.exhaust_sel)
have th3pre7:"aa∉A∧a∉ A∧(s @ t) setinterleaves ((ta, u), A)∧length s=0 ⟶
[]≤ta∧ [] ≤u∧ s setinterleaves (([], []), A)" by auto
have th3: "aa∉A∧a∉ A⟹∃t1 u1. (s @ t) setinterleaves ((ta, u), A) ⟶
t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)"
using th3pre th3pre4 th3pre6 th3pre7 by blast
with a b c th th1 th2 show ?thesis
by fastforce
qed
qed
qed
lemma SyncWithTick_imp_NTF1:
"(s @ [tick]) setinterleaves ((t, u), insert tick (ev ` A))
⟹ t∈ 𝒯 P ⟹ u∈ 𝒯 Q
⟹ ∃ t u Xa Y. (t, Xa) ∈ ℱ P ∧ ( (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
X - {tick} = (Xa ∪ Y) ∩ insert tick (ev ` A) ∪ Xa ∩ Y)"
apply (drule SyncWithTick_imp_NTF)
apply simp
apply simp
proof -
assume A: "t ∈ 𝒯 P"
and B: "u ∈ 𝒯 Q"
and C: "∃t1 u1. t = t1 @ [tick]∧u = u1@[tick]∧s setinterleaves ((t1, u1), insert tick (ev ` A))"
from C obtain t1 u1
where D: "t = t1 @ [tick] ∧ u = u1 @ [tick] ∧
s setinterleaves ((t1, u1), insert tick (ev ` A))" by blast
from A B D have E: "(t1, X-{tick}) ∈ ℱ P ∧ (u1, X-{tick}) ∈ ℱ Q"
by (simp add: T_F process_charn)
thus " ∃t u Xa Y. (t, Xa) ∈ ℱ P ∧ (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
X - {tick} = (Xa ∪ Y) ∩ insert tick (ev ` A) ∪ Xa ∩ Y"
using A B C D E by blast
qed
lemma ftf_Sync:
"front_tickFree u
⟹ front_tickFree t
⟹ s setinterleaves ((t, u),insert tick (ev ` A))
⟹ front_tickFree s"
proof-
assume A: "front_tickFree u"
assume B: "front_tickFree t"
assume C: "s setinterleaves ((t, u), insert tick (ev ` A))"
thus "front_tickFree s"
proof-
from A obtain u1 where A1: "∀ u2. u1≤u∧tickFree u1∧ (u2≤u∧tickFree u2⟶u2≤u1)"
by (metis append.right_neutral append_eq_first_pref_spec front_tickFree_charn le_list_def
tickFree_Nil)
from A A1 have AA1: "u1=u∨u=u1@[tick]"
by (metis(no_types, lifting) antisym append_Nil2 append_eq_first_pref_spec append_is_Nil_conv
front_tickFree_charn le_list_def less_list_def less_self nonTickFree_n_frontTickFree)
from B obtain t1 where B1: "∀ t2. t1≤t∧tickFree t1∧ (t2≤t∧tickFree t2⟶t2≤t1)"
by (metis append.right_neutral append_eq_first_pref_spec front_tickFree_charn le_list_def
tickFree_Nil)
from B B1 have BB1: "t1=t∨t=t1@[tick]"
by (metis(no_types, lifting) antisym append_Nil2 append_eq_first_pref_spec append_is_Nil_conv
front_tickFree_charn le_list_def less_list_def less_self nonTickFree_n_frontTickFree)
from A1 B1 have C1: "∀s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))⟶tickFree s1"
by (meson ftf_Sync1 tickFree_def)
from AA1 BB1 have CC1: "u1=u∧t1=t⟶tickFree s"
by (simp add: C C1)
from AA1 BB1 have CC2: "u1=u∧t=t1@[tick]⟶tickFree s" using ftf_Sync21
by (metis A1 C equals0D insertI1 non_tickFree_tick tickFree_append tickFree_def)
from AA1 BB1 have CC3: "u=u1@[tick]∧t1=t⟶tickFree s" using ftf_Sync21
by (metis B1 C insertI1 insert_not_empty mk_disjoint_insert non_tickFree_tick tickFree_append
tickFree_def)
from AA1 BB1 have CC4: "u=u1@[tick]∧t=t1@[tick]⟹
∃s1. s1 setinterleaves ((t1, u1), insert tick (ev ` A))∧(s=s1@[tick])"
using C ftf_Sync32 by blast
from C1 CC4 have CC5: "front_tickFree s"
using AA1 BB1 CC1 CC2 CC3 tickFree_implies_front_tickFree
tickFree_implies_front_tickFree_single by auto
with A1 B1 C1 AA1 BB1 show ?thesis
using CC1 CC2 CC3 tickFree_implies_front_tickFree by auto
qed
qed
lemma is_processT5_SYNC2: "
⋀ sa Y t u Xa Ya. (t,Xa) ∈ ℱ P ∧ (u,Ya) ∈ ℱ Q ∧ (sa setinterleaves ((t,u),insert tick (ev ` A)))
⟹∀c. c ∈ Y ⟶
(∀ t1 u1. (sa@[c]) setinterleaves ((t1,u1),insert tick (ev ` A))⟶
(((t1,{}) ∈ ℱ P⟶(u1, {}) ∉ ℱ Q)∧((t1,{}) ∈ ℱ Q⟶(u1, {}) ∉ ℱ P)))
⟹ ∃t2 u2 Xb. (t2, Xb) ∈ ℱ P ∧
(∃Yb. (u2, Yb) ∈ ℱ Q ∧
sa setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
( Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y =
(Xb ∪ Yb) ∩ insert tick (ev ` A) ∪ Xb ∩ Yb)"
proof -
fix sa Y t u Xa Ya
assume A: "(t,Xa) ∈ ℱ P ∧ (u,Ya) ∈ ℱ Q ∧(sa setinterleaves ((t,u),insert tick (ev ` A)))"
and B: " ∀c. c ∈ Y ⟶
(∀ t1 u1. (sa@[c]) setinterleaves ((t1,u1),insert tick (ev ` A)) ⟶
(((t1,{}) ∈ ℱ P ⟶
(u1, {}) ∉ ℱ Q) ∧ ((t1,{}) ∈ ℱ Q⟶(u1, {}) ∉ ℱ P)))"
thus "∃t2 u2 Xb. (t2, Xb) ∈ ℱ P ∧
(∃Yb. (u2, Yb) ∈ ℱ Q ∧ sa setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
(Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y =
(Xb ∪ Yb) ∩ insert tick (ev ` A) ∪ Xb ∩ Yb)"
proof-
from A B obtain Y1 Y2
where A1: "(Y1=(Y∩insert tick (ev ` A)))∧(Y2=(Y - insert tick (ev ` A)))"
by blast
from A1 have AA1: "Y1 ∪ Y2 = Y"
by blast
from A1 have newAA: "∀y∈Y1. y∈ insert tick (ev ` A)"
by blast
from A1 have newAAA: "∀y∈Y2. y∉ insert tick (ev ` A)"
by blast
from B A1 have AA2: "∀z∈Y1.(t@[z], {}) ∉ ℱ P ∨ (u@[z], {}) ∉ ℱ Q"
proof(cases "∃z ∈ Y1. (t@[z], {})∈ℱ P ∧ (u@[z], {}) ∈ ℱ Q")
case True
from True obtain z1 where TrA: "z1∈Y1∧(t@[z1], {})∈ℱ P ∧ (u@[z1], {}) ∈ ℱ Q"
by blast
from TrA A have TrB:
"⟦sa setinterleaves ((t,u),insert tick(ev ` A));
z1∈insert tick (ev ` A)⟧
⟹(sa@[z1]) setinterleaves ((t@[z1],(u@[z1])),insert tick (ev ` A))"
proof-
have a: "(rev sa) setinterleaves ((rev t,rev u),insert tick (ev ` A))"
using local.A doubleReverse by blast
have b: "(z1#rev sa) setinterleaves ((z1#rev t,z1# rev u),insert tick (ev ` A))"
using TrA a newAA by auto
show ?thesis
using b doubleReverse by fastforce
qed
then show ?thesis
using A1 B TrA local.A by blast
next
case False
then show ?thesis
by blast
qed
from A B A1 obtain Z1 Z2 where A2: "(Z1=Y1∩{z.(t@[z], {})∉ℱ P})∧(Z2=Y1-{z.(t@[z], {})∉ℱ P})"
by blast
from A2 have BA: "Y1=Z1∪Z2"
by blast
from A2 have BAA: "∀z∈Z1. (t@[z], {}) ∉ ℱ P"
by blast
from A2 have BAAA: "∀z∈Z2. (u@[z], {})∉ ℱ Q"
using AA2 by blast
from A2 BA BAA have A3: "(t, Z1)∈ ℱ P"
by (meson F_T NF_NT is_processT5_S7 local.A)
from A A1 have A43: "∀y∈Y2. (t@[y], {})∉ ℱ P ∧ (u@[y], {})∉ ℱ Q"
proof(cases "∃y∈Y2. ((t@[y], {})∈ ℱ P)∨((u@[y], {})∈ ℱ Q)")
case True
from True obtain y1 where innAA: "y1∈Y2∧(((t@[y1], {})∈ ℱ P)∨((u@[y1], {})∈ ℱ Q))" by blast
from innAA have innAAA: "y1∉ insert tick (ev ` A)"
using newAAA by auto
from innAA have innAA1:
"⟦sa setinterleaves ((t,u),insert tick (ev ` A));
y1 ∉ insert tick (ev ` A)⟧
⟹ ((t@[y1], {})∈ ℱ P
⟶(sa@[y1]) setinterleaves ((t@[y1],u),insert tick (ev ` A))) ∧
((u@[y1], {})∈ ℱ Q⟶(sa@[y1]) setinterleaves((t,u@[y1]),insert tick (ev`A)))"
by (simp add: addNonSync)
with A B innAA1 innAA show ?thesis
by (metis A1 DiffD1 innAAA is_processT4_empty)
next
case False
then show ?thesis by blast
qed
from A1 A2 obtain Xbb where B1: "Xbb=(Xa∪Z1∪Y2)"
by blast
from A B1 A3 A43 have A5: "(t, Xbb)∈ ℱ P"
by (meson BAA is_processT5_S1)
from A1 A2 obtain Ybb where B2: "Ybb=(Ya∪Z2∪Y2)"
by blast
from A B have A52: "(u, Ybb)∈ ℱ Q"
by (metis A43 B2 BAAA is_processT5_S1)
from A1 A2 have A61: "(Xbb ∪ Ybb)∩insert tick (ev ` A)=((Xa∪Ya∪Y1∪Y2) ∩ insert tick (ev ` A))"
using B1 B2 by blast
from A1 have A62: "(Y1) ∩ insert tick (ev ` A)=Y1"
using inf.orderE by auto
from A1 have A63: "(Y2) ∩ insert tick (ev ` A)={}"
by (simp add: AA1 Int_commute)
from A61 A62 A63 have A64:"((Xa∪Ya∪Y1∪Y2)∩insert tick(ev `A))=((Xa∪Ya)∩insert tick(ev `A)∪Y1)"
by (simp add: Int_Un_distrib2)
from AA1 BA B1 B2 have A65: "(Xbb∩Ybb)⊆((Xa∩Ya)∪Y) "
by auto
from AA1 BA B1 B2 have A66:"(Xbb∩Ybb)⊇((Xa∩Ya)∪Y2)"
by auto
from A1 A2 have A66: "((Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y) = ((Xbb ∪ Ybb) ∩
insert tick (ev ` A) ∪ Xbb ∩ Ybb)"
proof -
have f1: "(Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y = Y ∪ Xa ∩ Ya ∪ ((Xa ∪ Ya) ∩
insert tick (ev ` A) ∪ Xbb ∩ Ybb)"using A65 by auto
have "Xa ∩ Ya ∪ Y2 ∪ Xbb ∩ Ybb = Xbb ∩ Ybb"
by (meson A66 le_iff_sup)
then have "(Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya ∪ Y = Xbb ∩ Ybb ∪ ((Xa ∪ Ya) ∩
insert tick (ev ` A) ∪ Y1)" using f1 A1 by auto
then show ?thesis
using A61 A64 by force
qed
with A5 A52 A66 show ?thesis
using local.A by blast
qed
qed
lemma pt3:
"ta ∈ 𝒯 P
⟹ u ∈ 𝒯 Q ⟹ (s @ t) setinterleaves ((ta, u), insert tick (ev ` A))
⟹ ∃t u X. (t, X) ∈ ℱ P ∧
(∃Y. (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
proof-
assume a1: "ta ∈ 𝒯 P"
assume a2: "u ∈ 𝒯 Q"
assume a3: "(s @ t) setinterleaves ((ta, u), insert tick (ev ` A))"
have aa: "ta ∈ 𝒯 P ⟹u ∈ 𝒯 Q ⟹ (s @ t) setinterleaves ((ta, u), insert tick (ev ` A))⟹
∃t u. t ∈ 𝒯 P ∧(u ∈ 𝒯 Q ∧s setinterleaves ((t, u), insert tick (ev ` A)))"
using is_processT3_ST_pref synPrefix by blast
thus "∃t u X. (t, X) ∈ ℱ P ∧(∃Y. (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
using NF_NT a1 a2 a3 by blast
qed
lemma Sync_maintains_is_process:
"is_process ({(s,R).∃ t u X Y. (t,X) ∈ ℱ P ∧ (u,Y) ∈ ℱ Q ∧
(s setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y} ∪
{(s,R).∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧
s = r@v ∧
(r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)},
{s. ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧
s = r@v ∧
(r setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)})"
(is "is_process(?f, ?d)")
proof(simp only: fst_conv snd_conv Failures_def is_process_def FAILURES_def DIVERGENCES_def,
fold FAILURES_def DIVERGENCES_def,fold Failures_def,intro conjI)
show "([], {}) ∈ ?f"
apply auto
by (metis Int_commute Int_empty_right Sync.si_empty1 Un_empty empty_iff insert_iff is_processT1)
next
show " ∀s X. (s, X) ∈ ?f ⟶ front_tickFree s"
apply (auto simp:is_processT2 append_T_imp_tickFree front_tickFree_append D_imp_front_tickFree)
using ftf_Sync is_processT2 apply blast
using D_imp_front_tickFree ftf_Sync is_processT2_TR apply blast
using D_imp_front_tickFree ftf_Sync is_processT2_TR by blast
next
show "∀s t. (s @ t, {}) ∈ ?f ⟶ (s, {}) ∈ ?f"
apply auto
apply(drule F_T)
apply(drule F_T)
proof(goal_cases)
case (1 s t ta u X Y)
then show ?case
using pt3 by fastforce
next
case (2 s t ta u r v)
have aa: "front_tickFree v
⟹ s@t = r @ v ⟹ r setinterleaves ((ta, u), insert tick (ev ` A))
⟹ ∀t u r. r setinterleaves ((t,u),insert tick(ev `A)) ⟶
(∀v. s=r@v⟶front_tickFree v ⟶
¬tickFree r ∧ v≠[]∨(t ∈ 𝒟 P ⟶
u ∉ 𝒯 Q) ∧ (t ∈ 𝒟 Q ⟶ u ∉ 𝒯 P))
⟹ tickFree r ⟹ ta ∈ 𝒟 P ⟹ u ∈ 𝒯 Q ⟹ s<r"
apply(simp add: append_eq_append_conv2)
by (metis append_Nil2 front_tickFree_Nil front_tickFree_dw_closed le_list_def less_list_def)
from 2(1,2,3,4,5,6,7) Sync.sym aa have a1: "s<r" by blast
have aaa: "r setinterleaves ((ta, u), insert tick (ev ` A))
⟹ tickFree r ⟹ ta ∈ 𝒟 P
⟹ u ∈ 𝒯 Q ⟹ s<r
⟹ ∃t u X. (t, X) ∈ ℱ P ∧ (∃Y. (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
apply(drule D_T)
apply(simp add: le_list_def less_list_def)
using Sync.sym pt3 by blast
have aab: "∃t u X. (t, X) ∈ ℱ P ∧(∃Y. (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
using 2(1,2,3,4,5,6,7) aa aaa Sync.sym by auto
then show ?case by auto
next
case (3 s t ta u r v)
have aa: "front_tickFree v ⟹s @ t = r @ v
⟹ r setinterleaves ((ta, u), insert tick (ev ` A))
⟹ ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. s = r @ v ⟶front_tickFree v ⟶¬ tickFree r ∧ v ≠ [] ∨
(t ∈ 𝒟 P ⟶ u ∉ 𝒯 Q) ∧ (t ∈ 𝒟 Q ⟶ u ∉ 𝒯 P))
⟹ tickFree r
⟹ ta ∈ 𝒟 Q ⟹ u ∈ 𝒯 P ⟹ s<r"
apply(simp add: append_eq_append_conv2)
by (metis append_Nil2 front_tickFree_Nil front_tickFree_dw_closed le_list_def less_list_def)
have aaa: "r setinterleaves ((ta, u), insert tick (ev ` A))
⟹ tickFree r ⟹ ta ∈ 𝒟 Q ⟹ u ∈ 𝒯 P ⟹s<r
⟹ ∃t u X. (t, X) ∈ ℱ P ∧
(∃Y. (u, Y) ∈ ℱ Q ∧s setinterleaves ((t, u), insert tick (ev ` A)) ∧
tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
apply(drule D_T)
apply(simp add: le_list_def less_list_def)
using Sync.sym pt3 by blast
from 3(1,2,3,4,5,6,7) Sync.sym aa have a1: "s<r"
by blast
have aab: "∃t u X. (t, X) ∈ ℱ P ∧ (∃Y. (u, Y) ∈ ℱ Q ∧
s setinterleaves ((t, u), insert tick (ev ` A)) ∧
tick ∉ X ∧ tick ∉ Y ∧ (X ∪ Y) ∩ ev ` A = {} ∧ X ∩ Y = {})"
using 3(1,2,3,4,5,6,7) aa aaa Sync.sym by auto
then show ?case
by auto
next
case (4 s t ta u)
from 4(3) have a1: "ta ∈ 𝒯 P"
by (simp add: D_T)
then show ?case
using "4"(1) "4"(4) pt3 by blast
next
case (5 s t ta u)
from 5(3) have a1: "ta ∈ 𝒯 Q"
by (simp add: D_T)
then show ?case
using "5"(1) "5"(4) Sync.sym pt3 by blast
qed
next
show "∀s X Y. (s, Y) ∈ ?f ∧ X ⊆ Y ⟶ (s, X) ∈ ?f"
apply auto
proof(goal_cases)
case (1 s X t u Xa Ya)
have aa: "X ⊆ ((Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya )⟹∃x1 y1. x1⊆Xa ∧ y1⊆Ya ∧
X=((x1 ∪ y1) ∩ insert tick (ev ` A) ∪ x1 ∩ y1)"
apply(simp add: Set.subset_iff_psubset_eq)
apply(erule disjE)
defer
apply blast
proof-
assume A: "X ⊂ (Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya"
from A obtain X1 where B: "X1=((Xa ∪ Ya) ∩ insert tick (ev ` A) ∪ Xa ∩ Ya)-X"
by blast
from A obtain x where C: "x=Xa-X1"
by blast
from A obtain y where D: "y=Ya-X1"
by blast
from A B C D have E: "X = (x ∪ y) ∩ insert tick (ev ` A) ∪ x ∩ y"
by blast
thus " ∃x1. (x1 ⊂ Xa ∨ x1 = Xa) ∧ (∃y1. (y1 ⊂ Ya ∨ y1 = Ya) ∧ X = (x1 ∪ y1) ∩
insert tick (ev ` A) ∪ x1 ∩ y1)"
using A B C D E by (metis Un_Diff_Int inf.strict_order_iff inf_sup_absorb)
qed
then show ?case using 1(1,2,3,4,5)
by (meson process_charn)
qed
next
let ?f1 = "{(s,R). ∃ t u X Y. (t,X) ∈ ℱ P ∧ (u,Y) ∈ ℱ Q ∧
(s setinterleaves ((t,u),(ev`A) ∪ {tick})) ∧
R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y}"
have is_processT5_SYNC3:
"⋀sa X Y.(sa, X) ∈?f1 ⟹(∀c. c∈Y⟶(sa@[c],{})∉?f)⟹(sa, X∪Y) ∈ ?f1"
apply(clarsimp)
apply(rule is_processT5_SYNC2[simplified])
apply(auto simp:is_processT5) apply blast
by (metis Sync.sym Un_empty_right inf_sup_absorb inf_sup_aci(5) insert_absorb insert_not_empty)
show "∀s X Y. (s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟶ (s, X ∪ Y) ∈ ?f"
apply(intro allI impI, elim conjE UnE)
apply(rule rev_subsetD)
apply(rule is_processT5_SYNC3)
by(auto)
next
show "∀s X. (s @ [tick], {}) ∈ ?f ⟶ (s, X - {tick}) ∈ ?f"
apply auto
apply(drule F_T)
apply(drule F_T)
using SyncWithTick_imp_NTF1 apply fastforce
apply(metis append_assoc append_same_eq front_tickFree_dw_closed nonTickFree_n_frontTickFree
non_tickFree_tick tickFree_append)
apply(metis butlast_append butlast_snoc front_tickFree_charn non_tickFree_tick tickFree_append
tickFree_implies_front_tickFree)
apply (metis NT_ND append_Nil2 front_tickFree_Nil is_processT3_ST is_processT9_S_swap
SyncWithTick_imp_NTF)
by (metis NT_ND append_Nil2 front_tickFree_Nil is_processT3_ST is_processT9_S_swap
SyncWithTick_imp_NTF)
next
show "∀s t. s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ ?d"
apply auto
using front_tickFree_append apply blast
using front_tickFree_append apply blast
apply blast
by blast
next
show "∀s X. s ∈ ?d ⟶ (s, X) ∈ ?f"
by blast
next
show "∀s. s @ [tick] ∈ ?d ⟶ s ∈ ?d"
apply auto
apply (metis butlast_append butlast_snoc front_tickFree_charn non_tickFree_tick
tickFree_append tickFree_implies_front_tickFree)
apply (metis butlast_append butlast_snoc front_tickFree_charn non_tickFree_tick
tickFree_append tickFree_implies_front_tickFree)
apply (metis D_T append.right_neutral front_tickFree_Nil is_processT3_ST is_processT9
SyncWithTick_imp_NTF)
by (metis D_T append.right_neutral front_tickFree_Nil is_processT3_ST is_processT9
SyncWithTick_imp_NTF)
qed
lemmas Rep_Abs_Sync[simp] = Abs_process_inverse[simplified, OF Sync_maintains_is_process]
subsection‹Projections›
lemma
F_Sync : "ℱ (P ⟦ A ⟧ Q) =
{(s,R).∃ t u X Y. (t,X) ∈ ℱ P ∧
(u,Y) ∈ ℱ Q ∧
s setinterleaves ((t,u),(ev`A) ∪ {tick}) ∧
R = (X ∪ Y) ∩ ((ev`A) ∪ {tick}) ∪ X ∩ Y} ∪
{(s,R).∃ t u r v. front_tickFree v ∧
(tickFree r ∨ v=[]) ∧
s = r@v ∧
r setinterleaves ((t,u),(ev`A)∪{tick}) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}"
unfolding Sync_def
apply(subst Failures_def)
apply(simp only: Rep_Abs_Sync)
by(auto simp: FAILURES_def)
lemma
D_Sync : "𝒟 (P ⟦ A ⟧ Q) =
{s. ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧
s = r@v ∧ r setinterleaves ((t,u),(ev`A) ∪ {tick}) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}"
unfolding Sync_def
apply(subst D_def)
apply(simp only: Rep_Abs_Sync)
by(simp add: DIVERGENCES_def)
lemma
T_Sync : "𝒯 (P ⟦ A ⟧ Q) =
{s. ∃ t u. t ∈ 𝒯 P ∧ u ∈ 𝒯 Q ∧
s setinterleaves ((t,u),(ev`A) ∪ {tick})}∪
{s. ∃ t u r v. front_tickFree v ∧ (tickFree r ∨ v=[]) ∧
s = r@v ∧ r setinterleaves ((t,u),(ev`A) ∪ {tick}) ∧
(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}"
unfolding Sync_def
apply(subst Traces_def, simp only: Rep_Abs_Sync, simp add:TRACES_def FAILURES_def)
apply auto
apply (meson F_T)
using T_F by blast
subsection‹Syntax for Interleave and Parallel Operator ›
abbreviation Inter_syntax ("(_|||_)" [72,73] 72)
where "P ||| Q ≡ (P ⟦ {} ⟧ Q)"
abbreviation Par_syntax ("(_||_)" [74,75] 74)
where "P || Q ≡ (P ⟦ UNIV ⟧ Q)"
subsection‹ Continuity Rule ›
lemma mono_Sync_D1:
"P ⊑ Q ⟹ 𝒟 (Q ⟦ A ⟧ S) ⊆ 𝒟 (P ⟦ A ⟧ S)"
apply(auto simp: D_Sync)
using le_approx1 apply blast
using le_approx_lemma_T apply blast
apply (metis append_Nil2 le_approx1 subsetCE tickFree_Nil tickFree_implies_front_tickFree)
by (metis append_Nil2 le_approx_lemma_T subsetCE tickFree_Nil tickFree_implies_front_tickFree)
lemma mono_Sync_D2:
"P ⊑ Q⟹(∀ s. s ∉ 𝒟 (P ⟦ A ⟧ S) ⟶ Ra (P ⟦ A ⟧ S) s = Ra (Q ⟦ A ⟧ S) s)"
apply auto
apply(simp add: Ra_def D_Sync F_Sync)
apply (metis (no_types, lifting) F_T append_Nil2 front_tickFree_Nil le_approx2)
apply(simp add: Ra_def D_Sync F_Sync)
apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q]
le_approx1[of P Q] le_approx2T[of P Q], auto)
apply blast
apply blast
apply blast
using front_tickFree_Nil apply blast
using front_tickFree_Nil by blast
lemma interPrefixEmpty: "s setinterleaves ((t,[]),A)∧t1<t⟹∃s1<s. s1 setinterleaves ((t1, []), A)"
by (metis (no_types, lifting) Sync.sym emptyLeftProperty le_list_def nil_le2
order.strict_implies_order synPrefix1)
lemma interPrefix:"∃u1 s1. s setinterleaves((t,u),A)∧t1<t⟶u1≤u∧s1<s∧s1 setinterleaves((t1,u1),A)"
proof (induction "length t + length u" arbitrary:s t u t1 rule:nat_less_induct)
case 1
then show ?case
apply(cases t)
apply auto[1]
apply(cases u)
apply (meson interPrefixEmpty nil_le2)
proof-
fix a list aa lista
assume a: " ∀m<length t + length u. ∀x xa. m = length x + length xa ⟶ (∀xb xc. ∃u1 s1.
xb setinterleaves((x, xa),A)∧xc < x ⟶ u1 ≤ xa ∧ s1 < xb ∧ s1 setinterleaves ((xc, u1), A))"
and b: "t = a # list"
and c: "u = aa # lista"
thus "∃u1 s1. s setinterleaves((t, u),A)∧t1<t⟶u1 ≤u∧s1<s∧s1 setinterleaves ((t1, u1), A)"
proof-
from b c have th0pre: "a=aa∧aa∈ A⟹s setinterleaves ((t, u), A) ⟹
(tl s) setinterleaves ((list,lista), A)" by auto
from a obtain yu ys
where th0pre1: "a=aa∧aa∈ A ∧ s setinterleaves ((t, u), A)∧ t1 < a # list ∧ length t1>0
⟹ yu ≤ lista ∧ ys<tl s ∧ ys setinterleaves ((tl t1, yu), A)"
apply (simp add: le_list_def less_list_def append_eq_Cons_conv)
by (metis add_less_mono b c length_Cons lessI list.sel(3) th0pre)
from th0pre th0pre1 b c
have th0pre2: "a=aa ∧ aa∈A
⟹ s setinterleaves ((a # list, u), A) ∧ t1<a#list∧length t1>0
⟹ (a#ys)setinterleaves((a#tl t1, a#yu), A)∧a#ys<s∧a#yu≤u∧t1=a#tl t1"
apply (simp add: le_list_def less_list_def Cons_eq_append_conv)
by (metis append_Cons list.exhaust_sel list.inject list.sel(3))
have th0pre3: "a=aa∧aa∈A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0⟹
[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)"
apply (simp add: le_list_def less_list_def) using c by auto
from th0pre2 th0pre3 c have th0 : "a=aa∧aa∈A⟹s setinterleaves ((a # list, u), A)∧
t1 < a # list⟹∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)" by fastforce
from b c have th1pre: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A) ⟹
(tl s) setinterleaves ((list,aa#lista), A)" by auto
from a obtain yu1 ys1 where th1pre1: "a∉A∧aa∈ A∧s setinterleaves ((a # list, u), A)∧
t1 < a # list∧length t1>0⟹yu1≤u∧ys1<tl s∧ys1 setinterleaves ((tl t1, yu1), A)"
apply (simp add: le_list_def less_list_def append_eq_Cons_conv)
by (metis add_Suc b c length_Cons lessI list.sel(3) th1pre)
from th1pre1 have th1pre2: "a∉A∧aa∈ A ∧ ys1 setinterleaves ((tl t1, yu1), A)⟹
(a#ys1) setinterleaves ((a#tl t1, yu1), A)" apply simp
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from th1pre th1pre1 b c have th1pre3: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A)∧
t1<a#list∧length t1>0⟹(a#ys1) setinterleaves ((a#tl t1, yu1), A)∧a#ys1<s∧yu1≤u∧t1=a#tl t1"
apply (simp add: le_list_def less_list_def )
by (metis append_Cons list.exhaust_sel list.inject list.sel(3) th1pre2)
have th1preEmpty: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0
⟹[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)" apply (simp add: le_list_def less_list_def)
using c by auto
from c have th1: "a∉A∧aa∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list⟹
∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)" using th1pre3 th1preEmpty by fastforce
from b c have th2pre: "aa∉A∧a∈ A⟹s setinterleaves ((a # list, u), A) ⟹
(tl s) setinterleaves ((a#list,lista), A)" by auto
from a th2pre obtain yu2 ys2 where th2pre1: "aa∉A∧a∈ A∧s setinterleaves ((a # list, u), A)∧
t1 < a # list∧length t1>0⟹yu2≤lista∧ys2<tl s∧ys2 setinterleaves ((t1, yu2), A)"
apply (simp add: le_list_def less_list_def)
by (metis add_Suc_right b c length_Cons lessI)
from th2pre1 have th2pre2: "aa∉A∧a∈ A ∧ ys2 setinterleaves ((t1, yu2), A)⟹
(aa#ys2) setinterleaves ((t1, aa#yu2), A)" apply simp
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from th2pre th2pre1 b c have th2pre3: "aa∉A∧a∈ A ⟹s setinterleaves ((a # list, u), A)∧
t1 < a # list∧length t1>0⟹(aa#ys2) setinterleaves ((t1, aa#yu2), A)∧aa#ys2<s∧aa#yu2≤u"
apply (simp add: le_list_def less_list_def ) using th2pre2 by auto
have th2preEmpty: "aa∉A∧a∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0
⟹[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)" apply (simp add: le_list_def less_list_def)
using c by auto
from th2pre3 b c have th2: "aa∉A∧a∈ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list⟹
∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)"
using th2preEmpty by blast
from b c have th3pre: "aa∉A∧a∉ A⟹s setinterleaves ((a # list, u), A) ⟹
(tl s) setinterleaves ((a#list,lista), A)∧hd s=aa∨(tl s) setinterleaves ((list,u), A)∧hd s=a"
by auto
from a c b th3pre obtain yu3 ys3 where th3pre1: "(aa∉A∧a∉ A∧s setinterleaves
((a # list, u), A)∧ t1 < a # list∧length t1>0∧(tl s) setinterleaves ((a#list,lista), A)⟶
yu3≤lista∧ys3<tl s∧ys3 setinterleaves((t1,yu3),A))" apply(simp add:le_list_def less_list_def)
by (metis (no_types, lifting) add_Suc length_Cons lessI)
have adsmallPrefix: "t1<a # list∧length t1>0⟹tl t1<list"
using less_tail by fastforce
from a b c th3pre adsmallPrefix obtain yu30 ys30 where th3pre12: "(aa∉A∧a∉ A⟹
(tl s) setinterleaves ((list,u), A)∧hd s=a∧tl t1< list⟶yu30≤u∧ys30<tl s∧
ys30 setinterleaves ((tl t1, yu30), A))" apply (simp add: le_list_def less_list_def)
by (metis (no_types, lifting) add_Suc_right length_Cons lessI)
have th3pre1more1: "yu3≤lista ⟹aa#yu3≤u " using c
by (metis le_less less_cons)
have th3pre1more2: "aa∉A∧a∉ A∧s setinterleaves ((a # list, aa#lista), A) ∧
(tl s) setinterleaves ((a#list,lista), A)∧hd s=aa∧ys3<tl s ⟹aa#ys3<s " using c
by (metis less_cons list.exhaust_sel list.sel(2) nil_less)
have th3pre1more21: "aa ∉ A ∧a ∉ A ∧ ys3<tl s∧ys3 setinterleaves ((t1, yu3), A) ∧
hd s = aa ⟶(aa # ys3) setinterleaves ((t1, aa # yu3), A)"
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from th3pre1more1 th3pre1more2 th3pre1more21 th3pre1 have th3pre1more3: "(aa∉A∧a∉ A∧
s setinterleaves ((a # list, u), A)∧ t1 < a # list∧length t1>0∧(tl s) setinterleaves
((a#list,lista), A)∧hd s=aa⟶aa#yu3≤u∧aa#ys3<s∧(aa#ys3) setinterleaves ((t1, aa#yu3), A))"
using c by blast
have th3pre1more32: "aa∉A∧a∉ A∧s setinterleaves ((a # list, aa#lista), A) ∧
(tl s) setinterleaves ((list,aa#lista), A)∧hd s=a∧ys30<tl s ⟹a#ys30<s " using c
by (metis less_cons list.exhaust_sel list.sel(2) nil_less)
have th3pre1more213: "aa ∉ A ∧a ∉ A ∧ ys30<tl s∧ys30 setinterleaves ((tl t1, yu30), A) ∧
hd s = a ∧t1<a#list⟶(a # ys30) setinterleaves ((a#tl t1, yu30), A)"
by (metis (mono_tags, lifting) addNonSync doubleReverse rev.simps(2) rev_rev_ident)
from th3pre1more32 th3pre12 th3pre1more213 have th3pre1more33: "(aa∉A∧a∉ A∧s setinterleaves
((a # list, u), A)∧ t1 < a # list∧length t1>0∧(tl s) setinterleaves ((list,aa#lista), A)∧
hd s=a⟶yu30≤u∧a#ys30<s∧(a#ys30) setinterleaves ((t1, yu30), A))"
by (metis adsmallPrefix c hd_append2 le_list_def length_greater_0_conv list.exhaust_sel
list.sel(1) order.strict_implies_order)
from th3pre1more3 th3pre1more33 b c th3pre have th3NoEmpty: "aa∉A∧a∉ A⟹s setinterleaves
((a # list, u), A)∧t1 < a # list∧length t1>0⟹∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)"
apply (simp add: le_list_def less_list_def)
by (metis append.simps(2))
have th3preEmpty: "aa∉A∧a∉ A⟹s setinterleaves ((a # list, u), A)∧t1 < a # list∧length t1=0
⟹[]<s∧[]≤u∧ [] setinterleaves ((t1, []), A)"
apply (simp add: le_list_def less_list_def) using c by auto
from th3NoEmpty th3preEmpty have th3: "aa∉A∧a∉ A⟹s setinterleaves ((a # list, u), A)∧t1 <
a # list⟹∃u1≤u. ∃s1<s. s1 setinterleaves ((t1, u1), A)"
by blast
show?thesis
using b c th0 th1 th2 th3 by auto
qed
qed
qed
lemma mono_Sync2a:
"r∈min_elems(𝒟 (P ⟦A⟧ S))
⟹ ∃t u. r setinterleaves ((t, u),insert tick (ev ` A)) ∧
(t ∈ min_elems(𝒟 P) ∧ u ∈ 𝒯 S ∨ t ∈ min_elems(𝒟 S) ∧
u ∈ 𝒯 P ∧ u ∈ (𝒯 P - (𝒟 P-min_elems(𝒟 P))))"
proof-
fix r
assume A: "r ∈ min_elems(𝒟 (P ⟦A⟧ S))"
thus "∃t u. r setinterleaves ((t, u), insert tick (ev ` A))∧(t ∈ min_elems(𝒟 P) ∧
u ∈ 𝒯 S ∨ t ∈ min_elems(𝒟 S) ∧ u ∈ 𝒯 P ∧ u ∈ (𝒯 P - (𝒟 P-min_elems(𝒟 P))))"
proof(cases "∀t u r1. r1≤r∧ r1 setinterleaves((t, u),insert tick (ev ` A))
⟶ (t ∉ min_elems(𝒟 P)) ∧ (t ∉ min_elems(𝒟 S))")
case True
from A have AA: "r ∈ 𝒟 (P ⟦A⟧ S)"
using elem_min_elems by blast
from AA obtain t1 u1 where A1:
"∃r1≤r. r1 setinterleaves ((t1, u1), insert tick (ev ` A)) ∧
(t1 ∈ 𝒟 P ∨ t1 ∈ 𝒟 S)" apply(simp add: D_Sync)
using le_list_def by blast
from True A1 have A2: "(t1 ∉ min_elems(𝒟 P)) ∧ (t1 ∉ min_elems(𝒟 S))"
by blast
from A1 A2 min_elems5 obtain tm1 tm2
where tmA: "(t1∈𝒟 P ⟶
(tm1≤t1∧tm1∈ min_elems(𝒟 P))) ∧ (t1∈𝒟 S⟶(tm2≤t1∧tm2∈ min_elems(𝒟 S)))"
by metis
from A2 tmA have AB1: "(t1∈𝒟 P⟶tm1<t1)∧(t1∈𝒟 S⟶tm2<t1)"
by (metis A1 order.not_eq_order_implies_strict)
from A1 AB1 obtain um1 rm1 um2 rm2 where AB2: " (t1∈𝒟 P⟶um1≤u1 ∧ rm1 setinterleaves
((tm1, um1),insert tick (ev ` A)))∧(t1∈𝒟 S⟶um2≤u1 ∧ rm2 setinterleaves
((tm2, um2), insert tick (ev ` A)))" by (meson interPrefix)
from A1 A2 True tmA AB1 have A3: "(t1∈𝒟 P⟶rm1<r∧rm1∈𝒟(P⟦A⟧S))∧(t1∈𝒟 S⟶rm2<r∧rm2∈ 𝒟(P⟦A⟧S))"
by (meson dual_order.strict_implies_order interPrefix order_trans)
from A3 AA have ATrue: "r ∉ min_elems(𝒟 (P ⟦A⟧ S))" using min_elems_def
using A1 by blast
with A ATrue show ?thesis
by blast
next
case False
from A have dsync: "r∈𝒟 (P ⟦A⟧ S)"
by (simp add: local.A elem_min_elems)
from dsync obtain r1 t2 u2
where C: "r1≤r∧ r1 setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
((t2 ∈ 𝒟 P ∧ u2 ∈ 𝒯 S) ∨ (t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 P))"
apply(simp add: D_Sync)
using le_list_def by blast
from C have r1D: "r1 ∈ 𝒟 (P ⟦A⟧ S)" apply(simp add: D_Sync)
using front_tickFree_Nil by blast
from A C r1D have eq: "r1=r" apply(simp add: min_elems_def)
using le_neq_trans by blast
from A False have minAa: "(t2 ∈ 𝒟 P∧u2∈𝒯 S)⟶(t2 ∈ min_elems(𝒟 P))"
proof(cases "t2 ∈ 𝒟 P ∧u2 ∈ 𝒯 S∧ t2 ∉ min_elems(𝒟 P)")
case True
from True obtain t3 where inA: "t3<t2∧t3∈min_elems(𝒟 P)"
by (metis le_imp_less_or_eq min_elems5)
from inA obtain r3 u3 where inA1: "u3≤u2∧r3 setinterleaves((t3,u3),insert tick(ev ` A))∧r3<r"
using C eq interPrefix by blast
from inA1 have inA3: "u3 ∈ 𝒯 S"
using True is_processT3_ST_pref by blast
from inA1 have inA2: "r3 ∈ 𝒟(P ⟦A⟧ S)" apply (simp add: D_Sync)
using elem_min_elems front_tickFree_Nil inA inA3 by blast
with A eq inA1 show ?thesis
by(simp add: min_elems_def)
next
case False
then show ?thesis
by blast
qed
from A False have minAb1: "(t2 ∈ 𝒟 S∧u2∈ 𝒯 P)⟶(t2 ∈ min_elems(𝒟 S))"
proof(cases "t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 P∧ t2 ∉ min_elems(𝒟 S)")
case True
from True obtain t3 r3 u3 where inA: "t3<t2∧t3∈min_elems(𝒟 S)"
and inA1: "u3≤u2∧r3 setinterleaves ((t3, u3), insert tick (ev ` A))∧r3<r"
by (metis C eq interPrefix le_less min_elems5)
from inA1 have inA3: "u3 ∈ 𝒯 P"
using True is_processT3_ST_pref by blast
from inA1 have inA2: "r3 ∈ 𝒟 (P ⟦A⟧ S)" apply (simp add: D_Sync)
using elem_min_elems front_tickFree_Nil inA inA3 by blast
with A eq inA1 show ?thesis
by(simp add: min_elems_def)
next
case False
then show ?thesis
by blast
qed
from A False have minAb2: "(t2 ∈ 𝒟 S∧u2∈ 𝒯 P)⟶(u2 ∈ (𝒯 P-(𝒟 P-min_elems(𝒟 P))))"
proof(cases "t2 ∈ 𝒟 S ∧u2 ∈ 𝒯 P∧ u2 ∈(𝒟 P-min_elems(𝒟 P))")
case True
from True have inAAA: "u2∈𝒟 P∧u2∉min_elems(𝒟 P)"
by blast
from inAAA obtain u3 where inA: "u3<u2∧u3∈min_elems(𝒟 P)"
by (metis le_neq_trans min_elems5)
from inA obtain t3 r3 where inA1: "t3≤t2∧r3 setinterleaves((t3,u3),insert tick(ev ` A))∧r3<r"
using C Sync.sym eq interPrefix by blast
from inA1 have inA3: "u3 ∈ 𝒟 P∧t3 ∈ 𝒯 S"
using D_T True elem_min_elems inA is_processT3_ST_pref by blast
from inA1 have inA2: "r3 ∈ 𝒟 (P ⟦A⟧ S)" apply (simp add: D_Sync)
using Sync.sym front_tickFree_Nil inA3 by blast
with A inA1 inA2 show ?thesis
by(simp add: min_elems_def)
next
case False
then show ?thesis
by blast
qed
with A C show ?thesis
using eq minAa minAb1 by blast
qed
qed
lemma mono_Sync_D3:
assumes ordered: "P ⊑ Q"
shows "min_elems (𝒟 (P ⟦A⟧ S)) ⊆ 𝒯(Q ⟦A⟧ S)"
proof-
have mono_sync2b:"P ⊑ Q ⟹ ∀r. r ∈ min_elems(𝒟 (P⟦A⟧S))⟶r ∈ 𝒯(Q⟦A⟧S)"
apply(frule impI)
apply(auto simp: mono_Sync2a)
proof -
fix r
assume A: "P ⊑ Q"
and B: "r ∈ min_elems(𝒟(P⟦A⟧S))"
from B obtain t u
where E: "r setinterleaves ((t, u), insert tick (ev ` A)) ∧ (t ∈ min_elems(𝒟 P) ∧
u ∈ 𝒯 S ∨ t ∈ min_elems(𝒟 S) ∧ u ∈ (𝒯 P-(𝒟 P - min_elems(𝒟 P))))"
using mono_Sync2a by blast
from E have F:"(t ∈ 𝒯 Q ∧ u ∈ 𝒯 S) ∨ (t ∈ 𝒯 S ∧ u ∈ 𝒯 Q)"
using le_approx2T le_approx3 ordered by blast
thus "r ∈ 𝒯 (Q ⟦A⟧ S)"
by (metis (no_types, lifting) E Sync.sym T_Sync UnCI Un_commute insert_is_Un mem_Collect_eq)
qed
show ?thesis
apply(insert ordered)
apply(frule mono_sync2b)
by blast
qed
lemma mono_D_Sync: "𝒟 (S ⟦ A ⟧ Q) = 𝒟 (Q ⟦ A ⟧ S)"
by(auto simp: D_Sync)
lemma mono_T_Sync: "𝒯 (S ⟦ A ⟧ Q) = 𝒯 (Q ⟦ A ⟧ S)"
apply(auto simp: T_Sync)
using Sync.sym by fastforce+
lemma mono_F_Sync: "ℱ (S ⟦ A ⟧ Q) = ℱ (Q ⟦ A ⟧ S) "
apply auto
apply (simp add: F_Sync)
using Sync.sym apply blast
apply (simp add: F_Sync)
using Sync.sym by blast
lemma mono_Ra_Sync: "Ra (S ⟦ A ⟧ Q) s = Ra (Q ⟦ A ⟧ S) s"
apply auto
apply (auto simp: Ra_def)
by (auto simp: mono_F_Sync)
lemma mono_Sync[simp] : "P ⊑ Q ⟹ (P ⟦ A ⟧ S) ⊑ (Q ⟦ A ⟧ S)"
by(auto simp: le_approx_def mono_Sync_D1 mono_Sync_D2 mono_Sync_D3)
lemma mono_Sync_sym [simp]: "P ⊑ Q ⟹ (S ⟦ A ⟧ P) ⊑ (S ⟦ A ⟧ Q)"
by (metis Process_eq_spec mono_D_Sync mono_F_Sync mono_Sync)
lemma chain_Sync1: "chain Y ⟹ chain (λi. Y i ⟦ A ⟧ S)"
by(simp add: chain_def)
lemma chain_Sync2: "chain Y ⟹ chain (λi. S ⟦ A ⟧ Y i)"
by(simp add: chain_def)
lemma empty_setinterleaving : "[] setinterleaves ((t, u), A) ⟹ t = []"
by (cases t, cases u, auto, cases u, simp_all split:if_splits)
lemma inters_fin_fund: "finite{(t, u). s setinterleaves ((t, u), A)}"
proof (induction "length s" arbitrary:s rule:nat_less_induct)
case 1
have A:"{(t, u). s setinterleaves((t, u), A)} ⊆ {([],[])} ∪
{(t, u). s setinterleaves ((t, u), A) ∧
(∃ a list. t = a#list ∧ a ∉ A) ∧ u = []} ∪
{(t, u). s setinterleaves ((t, u), A) ∧
(∃ a list. u = a#list ∧ a ∉ A) ∧ t = []} ∪
{(t, u). s setinterleaves ((t, u), A) ∧
(∃ a list aa lista. u = a#list ∧ t = aa#lista)}"
(is "?A ⊆ {([],[])} ∪ ?B ∪ ?C ∪ ?D")
apply (rule subsetI, safe)
apply(simp_all add: neq_Nil_conv)
apply (metis Sync.si_empty2 Sync.sym empty_iff list.exhaust_sel)
using list.exhaust_sel apply blast
apply (metis Sync.sym emptyLeftNonSync list.exhaust_sel list.set_intros(1))
using list.exhaust_sel apply blast
apply (metis emptyLeftNonSync list.exhaust_sel list.set_intros(1))
by (metis Sync.si_empty2 Sync.sym empty_iff list.exhaust_sel)
have a1:"?B ⊆ { ((hd s#list), [])| list. (tl s) setinterleaves ((list, []), A) ∧ (hd s) ∉ A}"
(is "?B ⊆ ?B1") by auto
define f where a2:"f = (λa (t, (u::'a event list)). ((a::'a event)#t, ([]::'a event list)))"
have a3:"?B1 ⊆ {(hd s # list, []) |list. tl s setinterleaves ((list, []), A)} " (is "?B1 ⊆ ?B2")
by blast
from a1 a3 have a13:"?B ⊆ ?B2"
by simp
have AA: "finite ?B"
proof (cases s)
case Nil
then show ?thesis
using not_finite_existsD by fastforce
next
case (Cons a list)
hence aa:"finite{(t,u).(tl s) setinterleaves((t, u), A)}"using 1[THEN spec, of "length (tl s)"]
by (simp)
have "{(hd s#list, [])|list. tl s setinterleaves((list,[]),A)}⊆(λ(t, u).f(hd s)(t, u)) `{(t, u).
tl s setinterleaves ((t, u), A)}" using a2 by auto
hence "finite ?B2" using finite_imageI [of "{(t, u). (tl s) setinterleaves ((t, u), A)}"
"λ(t, u). f (hd s) (t, u)", OF aa] using rev_finite_subset by auto
then show ?thesis using a13
by (meson rev_finite_subset)
qed
have a1:"?C ⊆ { ([],(hd s#list))| list. (tl s) setinterleaves (([],list), A) ∧ (hd s) ∉ A}"
(is "?C ⊆ ?C1") by auto
define f where a2:"f = (λa ((t::'a event list), u). (([]::'a event list), (a::'a event)#u))"
have a3:"?C1 ⊆ {([],hd s # list) |list. tl s setinterleaves (([],list), A)} " (is "?C1 ⊆ ?C2")
by blast
from a1 a3 have a13:"?C ⊆ ?C2"
by simp
have AAA:"finite ?C"
proof (cases s)
case Nil
then show ?thesis
using not_finite_existsD by fastforce
next
case (Cons a list)
hence aa:"finite {(t,u).(tl s)setinterleaves((t, u), A)}"using 1[THEN spec, of "length (tl s)"]
by (simp)
have "{([], hd s # list) |list. tl s setinterleaves (([], list), A)} ⊆ (λ(t, u).
f (hd s) (t, u)) ` {(t, u). tl s setinterleaves ((t, u), A)}" using a2 by auto
hence "finite ?C2" using finite_imageI [of "{(t, u). (tl s) setinterleaves ((t, u), A)}"
"λ(t, u). f (hd s) (t, u)", OF aa] using rev_finite_subset by auto
then show ?thesis using a13
by (meson rev_finite_subset)
qed
have dd0:"?D ⊆ {(a#l, aa#la)|a aa l la. s setinterleaves ((a#l, aa#la), A)}" (is "?D ⊆ ?D1")
apply (rule subsetI, auto, simp split:if_splits)
by (blast, blast, metis, blast)
have AAAA:"finite ?D"
proof (cases s)
case Nil
hence "?D ⊆ {([],[])}"
using empty_setinterleaving by auto
then show ?thesis
using infinite_super by auto
next
case (Cons a list)
hence dd1:"?D1 ⊆ {(a#l, u)| l u. list setinterleaves ((l, u), A)}
∪ {(t, a#la)| t la. list setinterleaves ((t, la), A)}
∪ {(a#l, a#la)|l la. list setinterleaves ((l, la), A)}"(is "?D1 ⊆ ?D2 ∪ ?D3 ∪ ?D4")
by (rule_tac subsetI, auto split:if_splits)
with Cons have aa:"finite {(t,u). list setinterleaves ((t, u), A)}"
using 1[THEN spec, of "length list"] by (simp)
define f where a2:"f = (λ (t, (u::'a event list)). ((a::'a event)# t, u))"
with Cons have "?D2 ⊆ (f ` {(t, u). list setinterleaves ((t, u), A)})"
using a2 by auto
hence dd2:"finite ?D2"
using finite_imageI [of "{(t, u). list setinterleaves ((t, u), A)}" f, OF aa]
by (meson rev_finite_subset)
define f where a2:"f = (λ ((t::'a event list),u). (t,(a::'a event)#u))"
with Cons have "?D3 ⊆ (f ` {(t, u). list setinterleaves ((t, u), A)})"
using a2 by auto
hence dd3:"finite ?D3"
using finite_imageI [of "{(t, u). list setinterleaves ((t, u), A)}" f, OF aa]
by (meson rev_finite_subset)
define f where a2:"f = (λ (t,u). ((a::'a event)#t,(a::'a event)#u))"
with Cons have "?D4 ⊆ (f ` {(t, u). list setinterleaves ((t, u), A)})"
using a2 by auto
hence dd4:"finite ?D4"
using finite_imageI [of "{(t, u). list setinterleaves ((t, u), A)}" f, OF aa]
by (meson rev_finite_subset)
with dd0 dd1 dd2 dd3 dd4 show ?thesis
by (simp add: finite_subset)
qed
from A AA AAA AAAA show ?case
by (simp add: finite_subset)
qed
lemma inters_fin: "finite{(t, u, r). r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(∃v. x = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = []))}"
(is "finite ?A")
proof -
have a:"?A⊆(⋃r ∈ {r. r ≤ x}. {a. ∃t u. a=(t,u,r)∧r setinterleaves((t,u),insert tick(ev ` A))})"
(is "?A ⊆ (⋃r ∈ {r. r ≤ x}. ?P r)")
using le_list_def by fastforce
have b:"∀(r::'a event list). finite (?P r)"
proof(rule allI)
fix r::"'a event list"
define f where "f= (λ((t::'a event list), (u::'a event list)). (t,u,r))"
hence "?P r ⊆ (f ` {(t, u). r setinterleaves ((t, u), insert tick (ev ` A) )})"
by auto
then show "finite (?P r)"
using inters_fin_fund[of r "insert tick (ev ` A)"] finite_imageI[of "{(t, u). r setinterleaves
((t, u), insert tick (ev ` A))}" f] by (meson rev_finite_subset)
qed
have "{t. ∃t2. x = t @ t2} = {r. ∃ra. r @ ra = x}"
by blast
hence "finite {r. r ≤ x}" using prefixes_fin[of x, simplified Let_def, THEN conjunct1]
by (auto simp add:le_list_def)
with a b show ?thesis
by (meson finite_UN_I infinite_super)
qed
lemma limproc_Sync_D:
"chain Y⟹ 𝒟 (lim_proc(range Y)⟦A⟧ S) = 𝒟(lim_proc(range(λi. Y i ⟦A⟧ S)))"
apply(auto simp:Process_eq_spec F_Sync D_Sync T_Sync F_LUB D_LUB T_LUB chain_Sync1)
apply blast
apply blast
using front_tickFree_Nil apply blast
using front_tickFree_Nil apply blast
proof -
fix x
assume A: "chain Y"
and B: " ∀xa. ∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧
x = r @ v ∧ r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(t ∈ 𝒟 (Y xa) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 (Y xa))"
thus "∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ x = r @ v ∧
r setinterleaves ((t, u), insert tick (ev ` A)) ∧
((∀x. t ∈ 𝒟 (Y x)) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ (∀x. u ∈ 𝒯 (Y x)))"
proof(cases "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(r≤x ⟶ ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x))))")
case True
from A obtain tryunion where Ctryy:
"tryunion={(t, u, r). r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(∃v.(x = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])))}"
by simp
from Ctryy inters_fin have tolfin: "finite tryunion"
by auto
obtain tryunion1
where Ctryy1: "tryunion1 = {n. ∃(t,u, r) ∈ tryunion.
(t ∈ 𝒟 (Y n) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 (Y n))}" by simp
from B Ctryy1 Ctryy have Ctryy3: "∀n. n∈tryunion1"
by blast
from Ctryy3 have Ctryy2: "infinite tryunion1"
using finite_nat_set_iff_bounded by auto
from Ctryy2 Ctryy1 tolfin obtain r2 t2 u2
where Ee: "(t2,u2, r2) ∈ tryunion ∧
infinite {n. (t2 ∈ 𝒟 (Y n) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n))}"
by auto
from True Ee Ctryy obtain x1 x2
where Ee1: "((t2 ∉ 𝒟 (Y x1)) ∨ u2 ∉ 𝒯 S) ∧ (t2 ∈ 𝒟 S ⟶ (u2 ∉ 𝒯 (Y x2)))"
apply (simp add: le_list_def) by blast
from Ee Ee1 Ctryy obtain x3
where Ee2: "(x1≤x3) ∧ (x2≤x3) ∧ (t2 ∈ 𝒟 (Y x3) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y x3))"
apply(simp add: infinite_nat_iff_unbounded_le)
proof -
assume a1: "r2 setinterleaves ((t2, u2), insert tick (ev ` A)) ∧
(∃v. x = r2 @ v ∧ front_tickFree v ∧ (tickFree r2 ∨ v = [])) ∧
((∀m. ∃n≥m. t2 ∈ 𝒟 (Y n) ∧ u2 ∈ 𝒯 S) ∨
(∀m. ∃n≥m. t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n)))"
assume a2: "⋀x3. x1 ≤ x3 ∧ x2 ≤ x3∧(t2 ∈ 𝒟 (Y x3) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y x3))
⟹ thesis"
obtain nn :: "nat ⇒ nat"
where f3: "∀x0. (∃v1≥x0. t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y v1)) =
(x0 ≤ nn x0 ∧ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y (nn x0)))" by moura
obtain nna :: "nat ⇒ nat"
where "∀x0. (∃v1≥x0. t2 ∈ 𝒟 (Y v1) ∧ u2 ∈ 𝒯 S) =
(x0 ≤ nna x0 ∧ t2 ∈ 𝒟 (Y (nna x0)) ∧ u2 ∈ 𝒯 S)" by moura
then have f4: "(∀n. n ≤ nna n ∧ t2 ∈ 𝒟 (Y (nna n)) ∧ u2 ∈ 𝒯 S) ∨
(∀n. n ≤ nn n ∧ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y (nn n)))" using f3 a1 by presburger
have "(∃n. ¬ n ≤ nn n ∨ t2 ∉ 𝒟 S ∨ u2 ∉ 𝒯 (Y (nn n))) ∨
(∃n≥x1. x2 ≤ n ∧ (t2 ∈ 𝒟 (Y n) ∧
u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n)))" by (metis le_cases order.trans)
moreover
{ assume "∃n. ¬ n ≤ nn n ∨ t2 ∉ 𝒟 S ∨ u2 ∉ 𝒯 (Y (nn n))"
then have "∀n. n ≤ nna n ∧ t2 ∈ 𝒟 (Y (nna n)) ∧ u2 ∈ 𝒯 S"
using f4 by blast
then have "∃n≥x1. x2 ≤ n ∧ (t2 ∈ 𝒟 (Y n) ∧ u2 ∈ 𝒯 S ∨ t2 ∈ 𝒟 S ∧ u2 ∈ 𝒯 (Y n))"
by (metis (no_types) le_cases order.trans)
}
ultimately show ?thesis
using a2 by blast
qed
from A have Abb1: "∀n1 n2. n1≤n2 ⟶ Y n1 ⊑ Y n2"
by (simp add: po_class.chain_mono)
from A Abb1 have Abb2: "∀n1 n2. n1>n2 ∧ t ∉ 𝒟 (Y n2) ⟶ t ∉ 𝒟 (Y n1)"
using le_approx1 less_imp_le_nat by blast
from A Abb1 have Abb3: "∀n1 n2. n1>n2 ∧ t ∉ 𝒯 (Y n2) ⟶ t ∉ 𝒯 (Y n1)"
by (meson NT_ND le_approx2T less_imp_le_nat)
from Abb2 Ee2 have Ab1: "t2 ∉ 𝒟 (Y x1)⟶t2 ∉ 𝒟 (Y x3)"
by (meson Abb1 le_approx1 less_imp_le_nat subsetCE)
from Abb3 have Ab2: "u2 ∉ 𝒯 (Y x2)⟶u2 ∉ 𝒯 (Y x3)"
by (meson Abb1 Ee2 NT_ND le_approx2T less_imp_le_nat)
from True Ee Ee1 Ee2 Ab1 Ab2 show ?thesis
by blast
next
case False
from A B False obtain t u r
where Bb1: "r setinterleaves ((t, u), insert tick (ev ` A)) ∧ r ≤ x ∧
((∀x. t ∈ 𝒟 (Y x)) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ (∀x. u ∈ 𝒯 (Y x)))"
by auto
from B have Bb21: "front_tickFree x"
by (metis D_imp_front_tickFree append_Nil2 front_tickFree_append ftf_Sync is_processT2_TR)
from B Bb1 have Bb2: "∃v. front_tickFree v ∧ (tickFree r ∨ v = [])∧ x = r @ v"
by (metis Bb21 front_tickFree_Nil front_tickFree_mono le_list_def)
then show ?thesis
using Bb1 by blast
qed
qed
lemma limproc_Sync_F_annex1:
" chain Y
⟹ ∀n. (a, b) ∈ ℱ (Y n ⟦A⟧ S)
⟹ ∃x. a ∉ 𝒟 (Y x ⟦A⟧ S)
⟹ ∃t u X. (∀x. (t, X) ∈ ℱ (Y x)) ∧
(∃Y. (u, Y) ∈ ℱ S ∧ a setinterleaves((t, u),insert tick (ev ` A)) ∧
b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)"
proof -
fix a b
assume A: "chain Y"
assume B: "∀n. (a, b) ∈ ℱ (Y n ⟦A⟧ S)"
assume C: "∃x. a ∉ 𝒟 (Y x ⟦A⟧ S)"
thus "∃t u X. (∀x. (t, X) ∈ ℱ (Y x)) ∧
(∃Y. (u, Y) ∈ ℱ S ∧
a setinterleaves ((t, u), insert tick (ev ` A)) ∧
b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)"
proof-
from B C obtain x1 where D: "a ∉ 𝒟 (Y x1 ⟦A⟧ S)"
by blast
from B D obtain t1 u1 X1 Y1 where E:
"a setinterleaves ((t1, u1), insert tick (ev ` A)) ∧
(t1, X1) ∈ ℱ (Y x1) ∧ (u1, Y1) ∈ ℱ S ∧
b = (X1 ∪ Y1) ∩ insert tick (ev ` A) ∪ X1 ∩ Y1"
apply(auto simp: D_Sync F_Sync)
by fastforce
from B D E have F: "t1 ∉ 𝒟 (Y x1) ∧ t1 ∈ 𝒯(Y x1)" apply(auto simp: D_Sync)
using F_T front_tickFree_Nil apply blast
by (simp add: F_T)
from F have ee: "∀i. (t1, X1) ∈ ℱ (Y i)∧(u1, Y1)∈ ℱ S∧ a setinterleaves
((t1, u1), insert tick (ev ` A))∧ b = (X1 ∪ Y1) ∩ insert tick (ev ` A) ∪ X1 ∩ Y1"
using E chain_lemma is_processT8_S le_approx2 local.A by metis
with A B C D E F ee show?thesis
by blast
qed
qed
lemma limproc_Sync_F_annex2:
"chain Y
⟹ ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶ front_tickFree v ⟶
¬ tickFree r ∧ v ≠ [] ∨ ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x))))
⟹ ∃x. a ∉ 𝒟(Y x ⟦ A ⟧ S)"
apply(auto simp: D_Sync)
proof-
fix a
assume A: "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶ front_tickFree v ⟶
¬ tickFree r ∧ v ≠ [] ∨
((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x))))"
assume B: "chain Y"
thus "∃x. ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶ front_tickFree v ⟶
¬ tickFree r∧v≠[] ∨ (t ∈ 𝒟 (Y x) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y x)))"
proof-
from B have D: "((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x)))
⟹ (∃x. ((t ∈ 𝒟 (Y x) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y x))))"
by (meson D_T chain_lemma le_approx1 le_approx2T subsetCE)
from A obtain tryunion
where Ctryy: "tryunion={(t, u, r). r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = []))}"
by simp
from Ctryy have tolfin: "finite tryunion"
using inters_fin by auto
from B have Abb1: "∀n1 n2. n1≤n2 ⟶ Y n1 ⊑ Y n2"
by (simp add: po_class.chain_mono)
from A Abb1 have Abb2: "∀n1 n2 t. n1>n2∧t ∉ 𝒟 (Y n2)⟶t ∉ 𝒟 (Y n1)"
using le_approx1 less_imp_le_nat by blast
from A Abb1 have Abb3: "∀n1 n2 t. n1>n2∧t ∉ 𝒯 (Y n2)⟶t ∉ 𝒯 (Y n1)"
by (meson NT_ND le_approx2T less_imp_le_nat)
from Abb2 Abb3
have oneIndexPre: "∀t u. ((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶
(∃x. u ∉ 𝒯 (Y x))) ⟶
(∃x. (t ∉ 𝒟 (Y x) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y x)))"
by (meson B D_T ND_F_dir2' chain_lemma le_approx1 subsetCE)
from A B oneIndexPre Abb2 Abb3
have oneIndex: "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶front_tickFree v ⟶ ¬ tickFree r∧v≠[] ∨
( ∃x.( (( t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ (u ∉ 𝒯 (Y x))))))" by blast
define proUnion1
where finiUnion: "proUnion1 = {n. ∃(t,u, r)∈tryunion. (((t ∈ 𝒟 (Y n) ⟶ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y n)))∧
(∀m. ( (t ∈ 𝒟 (Y m)⟶u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S⟶u ∉ 𝒯 (Y m)))⟶n≤m))}"
from B
have finiSet1: "⋀r t u. (t,u, r) ∈ tryunion
⟹ finite {n1.(((t ∈ 𝒟 (Y n1)⟶u ∉ 𝒯 S) ∧
(t∈𝒟 S⟶u∉𝒯(Y n1)))∧(∀m1. ((t ∈ 𝒟 (Y m1) ⟶
u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y m1)))⟶n1≤m1))}"
by (metis (no_types, lifting) infinite_nat_iff_unbounded mem_Collect_eq not_less)
from B tolfin finiUnion oneIndex finiSet1 have finiSet: "finite proUnion1"
by auto
from finiSet obtain proMax where ann: "proMax=Max(proUnion1)"
by blast
from ann Abb2 have ann1: "∀num∈proUnion1. ∀t. t ∉ 𝒟 (Y num)⟶t ∉ 𝒟 (Y proMax)"
by (meson Abb1 Max_ge finiSet le_approx1 subsetCE)
from ann Abb3 have ann2: "∀num∈proUnion1. ∀t. t ∉ 𝒯 (Y num)⟶t ∉ 𝒯 (Y proMax)"
by (meson Abb1 D_T Max_ge finiSet le_approx2T)
from finiUnion
have ann3: "∀num∈proUnion1. ∃r t u. r setinterleaves((t, u),insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶front_tickFree v ⟶
¬ tickFree r ∧ v ≠ [] ∨(( ((t∉𝒟(Y num))∨u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ (u ∉ 𝒯 (Y num))))))" by auto
obtain proUnion2
where ann0: "proUnion2 ={(t, u, r).∃n. (t, u, r) ∈ tryunion ∧
((t ∈ 𝒟 (Y n)⟶u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y n)))}" by auto
from ann0 Ctryy finiUnion
have ann1: "⋀t u r. (t, u, r)∈ proUnion2
⟹∃num. num∈proUnion1 ∧ ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))"
proof-
fix t u r
assume a: "(t, u, r)∈ proUnion2"
define P where PP:"P = (λnum. ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num))))"
thus "∃num. num∈proUnion1∧ P num"
proof-
from finiUnion obtain minIndexRB where ann1preB: "minIndexRB={n. (P n)}"
by auto
from B ann1preB obtain minmin where ab: "(minmin::nat) = Inf (minIndexRB)"
by auto
from ann0 ann1preB PP have ann1preNoEmpty1: "minIndexRB ≠ {}"
using a by blast
from ab ann1preNoEmpty1 have ann1pre0:"minmin ∈ minIndexRB"
using Inf_nat_def wellorder_Least_lemma(1) by force
have "minmin∈ {n. ∃t u r. (t,u,r)∈tryunion ∧ ((t ∈ 𝒟 (Y n) ⟶ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y n))) ∧ (∀m. (t ∈ 𝒟 (Y m) ⟶
u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y m)) ⟶ n ≤ m)}"
apply(rule CollectI,rule_tac x=t in exI,rule_tac x=u in exI,rule_tac x=r in exI,intro conjI)
using a ann0 apply blast
using PP ann1pre0 ann1preB apply blast
using PP ann1pre0 ann1preB apply blast
by (simp add: Inf_nat_def PP ab ann1preB wellorder_Least_lemma(2))
then show ?thesis
using ann1pre0 ann1preB finiUnion by blast
qed
qed
from ann1
have ann12: "∀t u r. ∃num.(t, u, r) ∈ proUnion2 ⟶ num∈proUnion1 ∧
((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))" by auto
from ann0 Ctryy
have ann2: "∀t u r. (t, u, r) ∈ proUnion2 ⟶
(r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])) ∧
(∃nu1. (t ∈ 𝒟 (Y nu1) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nu1))))" by simp
have ann15: "∀t u r. (r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])) ∧
(∃nu1. (t ∈ 𝒟 (Y nu1) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nu1)))) ⟶
(t, u, r) ∈ proUnion2"
using Ctryy ann0 by blast
from ann12 ann15
have ann01: "∀t u r. ((r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(∃v. a = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = [])) ∧
(∃nu1. (t ∈ 𝒟 (Y nu1)⟶u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nu1))))⟶
(∃num∈proUnion1. ((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))))" by blast
from ann01
have annhelp: "∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶ front_tickFree v ⟶(tickFree r ∨ v = [])⟶
(∃num∈proUnion1.((t ∈ 𝒟 (Y num) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y num)))))"
by (metis oneIndex)
from Abb1 Abb2
have annHelp2: "∀nn t u.
nn ∈ proUnion1 ∧ (t ∈ 𝒟 (Y nn) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y nn)) ⟶
(t ∈ 𝒟 (Y proMax) ⟶ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y proMax))"
by (metis Abb3 Max_ge ann finiSet le_neq_trans)
from annHelp2 annhelp
have annHelp1: "∀t u r.
r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶
front_tickFree v ⟶
tickFree r ∨ v = [] ⟶ (t ∈ 𝒟 (Y proMax) ⟶ u ∉ 𝒯 S) ∧
(t ∈ 𝒟 S ⟶ u ∉ 𝒯 (Y proMax)))" by blast
with A B show ?thesis
by blast
qed
qed
lemma limproc_Sync_F:
"chain Y ⟹ ℱ(lim_proc (range Y)⟦ A ⟧S) = ℱ(lim_proc (range (λi. Y i ⟦ A ⟧ S)))"
apply(auto simp add: Process_eq_spec D_Sync F_Sync F_LUB D_LUB T_LUB chain_Sync1)
apply blast
apply blast
apply blast
using front_tickFree_Nil apply blast
using front_tickFree_Nil apply blast
proof-
fix a b
assume A1: " ∀x. (∃t u X. (t, X) ∈ ℱ (Y x) ∧
(∃Y. (u, Y) ∈ ℱ S ∧
a setinterleaves ((t, u), insert tick (ev ` A)) ∧
b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)) ∨
(∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ a = r @ v ∧
r setinterleaves ((t, u), insert tick (ev ` A)) ∧
(t ∈ 𝒟 (Y x) ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 (Y x)))"
and B: " ∀t u r. r setinterleaves ((t, u), insert tick (ev ` A)) ⟶
(∀v. a = r @ v ⟶ front_tickFree v ⟶
¬ tickFree r ∧ v ≠ [] ∨
((∃x. t ∉ 𝒟 (Y x)) ∨ u ∉ 𝒯 S) ∧ (t ∈ 𝒟 S ⟶ (∃x. u ∉ 𝒯 (Y x))))"
and C: "chain Y"
thus "∃t u X. (∀x. (t, X) ∈ ℱ (Y x)) ∧(∃Y. (u, Y) ∈ ℱ S ∧ a setinterleaves
((t, u), insert tick (ev ` A)) ∧ b = (X ∪ Y) ∩ insert tick (ev ` A) ∪ X ∩ Y)"
proof (cases "∃m. a ∉ 𝒟(Y m ⟦ A ⟧ S)")
case True
then obtain m where "a ∉ 𝒟(Y m ⟦ A ⟧ S)"
by blast
with A1 have D: "∀n. (a, b)∈ ℱ (Y n ⟦ A ⟧ S)"
by (auto simp: F_Sync)
with A1 B C show ?thesis
apply(erule_tac x=m in allE)
apply(frule limproc_Sync_F_annex2)
apply simp
by(simp add: limproc_Sync_F_annex1)
next
case False
with False have E: "∀n. a ∈ 𝒟 (Y n ⟦ A ⟧ S)"
by blast
with C E B show ?thesis
apply auto
apply(drule limproc_Sync_F_annex2)
apply blast
by fast
qed
qed
lemma cont_left_Sync : "chain Y ⟹ ((⨆ i. Y i) ⟦ A ⟧ S) = (⨆ i. (Y i ⟦ A ⟧ S))"
by(simp add: Process_eq_spec chain_Sync1 limproc_Sync_D limproc_Sync_F limproc_is_thelub)
lemma cont_right_Sync : "chain Y ⟹ (S ⟦ A ⟧ (⨆ i. Y i)) = (⨆ i. (S ⟦ A ⟧ Y i))"
by (metis (no_types, lifting) Process_eq_spec cont_left_Sync lub_eq mono_D_Sync mono_F_Sync)
lemma Sync_cont[simp]:
assumes f:"cont f"
and g:"cont g"
shows "cont (λx. (f x) ⟦A⟧ (g x))"
proof -
have A : "⋀x. cont g ⟹ cont (λy. y ⟦A⟧ (g x))"
apply (rule contI2, rule monofunI)
apply(auto)
by (simp add: cont_left_Sync)
have B : "⋀y. cont g ⟹ cont (λx. y ⟦A⟧ g x)"
apply(rule_tac c="(λ x. y ⟦A⟧ x)" in cont_compose)
apply(rule contI2, rule monofunI)
apply (simp)
apply (simp add: cont_right_Sync)
by simp
show ?thesis using f g
apply(rule_tac f="(λx. (λ f. f ⟦A⟧ g x))" in cont_apply)
by(auto intro:contI2 simp:A B)
qed
end