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‹Consequences›
lemma emptyLeftProperty:"∀s. s setinterleaves (([], t), A)⟶s=t"
by (induct t) auto
lemma emptyLeftSelf: " (∀t1. t1∈ set t⟶t1∉A)⟶t setinterleaves (([], t), A) "
by (induct t) auto
lemma emptyLeftNonSync: "s setinterleaves (([], t), A) ⟹ ∀a. a ∈ set t ⟶ a ∉ A"
proof (induct t arbitrary: s)
case Nil
show ?case by simp
next
case (Cons a t)
thus ?case by (cases s; simp split: if_split_asm)
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)"
find_theorems ‹(@)› name: cases
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
subsection‹The Sync Operator Definition›
lift_definition Sync :: "['a process,'a set,'a process] => 'a process" (‹(3(_ ⟦_⟧/ _))› [64,0,65] 64)
is "λP A Q. ({(s,R).∃ t u X Y. (t,X)