--- a
+++ b/thys/TLA/Buffer.thy
@@ -0,0 +1,660 @@
+(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
+    Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
+                 Stephan Merz <Stephan.Merz at loria.fr>
+    Year:        2011
+    Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
+*)
+
+header {* Refining a Buffer Specification *}
+
+theory Buffer
+imports State
+begin
+
+text {*
+  We specify a simple FIFO buffer and prove that two FIFO buffers
+  in a row implement a FIFO buffer.
+*}
+
+subsection "Buffer specification"
+
+text {*
+  The following definitions all take three parameters: a state function
+  representing the input channel of the FIFO buffer, another representing
+  the internal queue, and a third one representing the output channel.
+  These parameters will be instantiated later in the definition of the
+  double FIFO.
+*}
+
+definition BInit :: "'a statefun \<Rightarrow> 'a list statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal"
+where "BInit ic q oc \<equiv> TEMP $q = #[] + \<and>$ic = $oc" -- {* initial condition of buffer *} + +definition Enq :: "'a statefun \<Rightarrow> 'a list statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal" +where "Enq ic q oc \<equiv> TEMP ic$ \<noteq> $ic + \<and> q$ = $q @ [ ic$ ]
+                        \<and> oc$=$oc"     -- {* enqueue a new value *}
+
+definition Deq :: "'a statefun \<Rightarrow> 'a list statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal"
+where "Deq ic q oc \<equiv> TEMP # 0 < length<$q> + \<and> oc$ = hd<$q> + \<and> q$ = tl<$q> + \<and> ic$ = $ic" -- {* dequeue value at front *} + +definition Nxt :: "'a statefun \<Rightarrow> 'a list statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal" +where "Nxt ic q oc \<equiv> TEMP (Enq ic q oc \<or> Deq ic q oc)" + +-- {* internal specification with buffer visible *} +definition ISpec :: "'a statefun \<Rightarrow> 'a list statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal" +where "ISpec ic q oc \<equiv> TEMP BInit ic q oc + \<and> \<box>[Nxt ic q oc]_(ic,q,oc) + \<and> WF(Deq ic q oc)_(ic,q,oc)" + +-- {* external specification: buffer hidden *} +definition Spec :: "'a statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal" +where "Spec ic oc == TEMP (EEX q. ISpec ic q oc)" + +subsection "Properties of the buffer" + +text {* + The buffer never enqueues the same element twice. We therefore + have the following invariant: + \begin{itemize} + \item any two subsequent elements in the queue are different, and + the last element in the queue is different from the value of the + output channel, + \item if the queue is non-empty then the last element in the queue + is the value that appears on the input channel, + \item if the queue is empty then the values on the output and input + channels are equal. + \end{itemize} + + The following auxiliary predicate @{text noreps} is true if no + two subsequent elements in a list are identical. +*} + +definition noreps :: "'a list \<Rightarrow> bool" +where "noreps xs \<equiv> \<forall>i < length xs - 1. xs!i \<noteq> xs!(Suc i)" + +definition BInv :: "'a statefun \<Rightarrow> 'a list statefun \<Rightarrow> 'a statefun \<Rightarrow> temporal" +where "BInv ic q oc \<equiv> TEMP List.last<$oc # $q> =$ic \<and> noreps<$oc #$q>"
+
+lemmas buffer_defs = BInit_def Enq_def Deq_def Nxt_def
+                     ISpec_def Spec_def BInv_def
+
+lemma ISpec_stutinv: "STUTINV (ISpec ic q oc)"
+  unfolding buffer_defs by (simp add: bothstutinvs livestutinv)
+
+lemma Spec_stutinv: "STUTINV Spec ic oc"
+  unfolding buffer_defs by (simp add: bothstutinvs livestutinv eexSTUT)
+
+text {* A lemma about lists that is useful in the following *}
+lemma tl_self_iff_empty[simp]: "(tl xs = xs) = (xs = [])"
+proof
+  assume 1: "tl xs = xs"
+  show "xs = []"
+  proof (rule ccontr)
+    assume "xs \<noteq> []" with 1 show "False"
+      by (auto simp: neq_Nil_conv)
+  qed
+qed (auto)
+
+lemma tl_self_iff_empty'[simp]: "(xs = tl xs) = (xs = [])"
+proof
+  assume 1: "xs = tl xs"
+  show "xs = []"
+  proof (rule ccontr)
+    assume "xs \<noteq> []" with 1 show "False"
+      by (auto simp: neq_Nil_conv)
+  qed
+qed (auto)
+
+lemma Deq_visible:
+  assumes v: "\<turnstile> Unchanged v \<longrightarrow> Unchanged q"
+  shows "|~ <Deq ic q oc>_v = Deq ic q oc"
+proof (auto simp: tla_defs)
+  fix w
+  assume deq: "w \<Turnstile> Deq ic q oc" and unch: "v (w (Suc 0)) = v (w 0)"
+  from unch v[unlifted] have "q (w (Suc 0)) = q (w 0)"
+    by (auto simp: tla_defs)
+  with deq show "False" by (auto simp: Deq_def tla_defs)
+qed
+
+lemma Deq_enabledE: "\<turnstile> Enabled <Deq ic q oc>_(ic,q,oc) \<longrightarrow> $q ~= #[]" + by (auto elim!: enabledE simp: Deq_def tla_defs) + +text {* + We now prove that @{text BInv} is an invariant of the Buffer + specification. + + We need several lemmas about @{text noreps} that are used in the + invariant proof. +*} + +lemma noreps_empty [simp]: "noreps []" + by (auto simp: noreps_def) + +lemma noreps_singleton: "noreps [x]" -- {* special case of following lemma *} + by (auto simp: noreps_def) + +lemma noreps_cons [simp]: + "noreps (x # xs) = (noreps xs \<and> (xs = [] \<or> x \<noteq> hd xs))" +proof (auto simp: noreps_singleton) + assume cons: "noreps (x # xs)" + show "noreps xs" + proof (auto simp: noreps_def) + fix i + assume i: "i < length xs - Suc 0" and eq: "xs!i = xs!(Suc i)" + from i have "Suc i < length (x#xs) - 1" by auto + moreover + from eq have "(x#xs)!(Suc i) = (x#xs)!(Suc (Suc i))" by auto + moreover + note cons + ultimately show False by (auto simp: noreps_def) + qed +next + assume 1: "noreps (hd xs # xs)" and 2: "xs \<noteq> []" + from 2 obtain x xxs where "xs = x # xxs" by (cases xs, auto) + with 1 show False by (auto simp: noreps_def) +next + assume 1: "noreps xs" and 2: "x \<noteq> hd xs" + show "noreps (x # xs)" + proof (auto simp: noreps_def) + fix i + assume i: "i < length xs" and eq: "(x # xs)!i = xs!i" + from i obtain y ys where xs: "xs = y # ys" by (cases xs, auto) + show False + proof (cases i) + assume "i = 0" + with eq 2 xs show False by auto + next + fix k + assume k: "i = Suc k" + with i eq xs 1 show False by (auto simp: noreps_def) + qed + qed +qed + +lemma noreps_append [simp]: + "noreps (xs @ ys) = + (noreps xs \<and> noreps ys \<and> (xs = [] \<or> ys = [] \<or> List.last xs \<noteq> hd ys))" +proof auto + assume 1: "noreps (xs @ ys)" + show "noreps xs" + proof (auto simp: noreps_def) + fix i + assume i: "i < length xs - Suc 0" and eq: "xs!i = xs!(Suc i)" + from i have "i < length (xs @ ys) - Suc 0" by auto + moreover + from i eq have "(xs @ ys)!i = (xs@ys)!(Suc i)" by (auto simp: nth_append) + moreover note 1 + ultimately show "False" by (auto simp: noreps_def) + qed +next + assume 1: "noreps (xs @ ys)" + show "noreps ys" + proof (auto simp: noreps_def) + fix i + assume i: "i < length ys - Suc 0" and eq: "ys!i = ys!(Suc i)" + from i have "i + length xs < length (xs @ ys) - Suc 0" by auto + moreover + from i eq have "(xs @ ys)!(i+length xs) = (xs@ys)!(Suc (i + length xs))" + by (auto simp: nth_append) + moreover note 1 + ultimately show "False" by (auto simp: noreps_def) + qed +next + assume 1: "noreps (xs @ ys)" and 2: "xs \<noteq> []" and 3: "ys \<noteq> []" + and 4: "List.last xs = hd ys" + from 2 obtain x xxs where xs: "xs = x # xxs" by (cases xs, auto) + from 3 obtain y yys where ys: "ys = y # yys" by (cases ys, auto) + from xs ys have 5: "length xxs < length (xs @ ys) - 1" by auto + from 4 xs ys have "(xs @ ys) ! (length xxs) = (xs @ ys) ! (Suc (length xxs))" + by (auto simp: nth_append last_conv_nth) + with 5 1 show "False" by (auto simp: noreps_def) +next + assume 1: "noreps xs" and 2: "noreps ys" and 3: "List.last xs \<noteq> hd ys" + show "noreps (xs @ ys)" + proof (cases "xs = [] \<or> ys = []") + case True + with 1 2 show ?thesis by auto + next + case False + then obtain x xxs where xs: "xs = x # xxs" by (cases xs, auto) + from False obtain y yys where ys: "ys = y # yys" by (cases ys, auto) + show ?thesis + proof (auto simp: noreps_def) + fix i + assume i: "i < length xs + length ys - Suc 0" + and eq: "(xs @ ys)!i = (xs @ ys)!(Suc i)" + show "False" + proof (cases "i < length xxs") + case True + hence "i < length (x # xxs)" by simp + hence xsi: "((x # xxs) @ ys)!i = (x # xxs)!i" + unfolding nth_append by simp + from True have "(xxs @ ys)!i = xxs!i" by (auto simp: nth_append) + with True xsi eq 1 xs show "False" by (auto simp: noreps_def) + next + assume i2: "\<not>(i < length xxs)" + show False + proof (cases "i = length xxs") + case True + with xs have xsi: "(xs @ ys)!i = List.last xs" + by (auto simp: nth_append last_conv_nth) + from True xs ys have "(xs @ ys)!(Suc i) = y" + by (auto simp: nth_append) + with 3 ys eq xsi show False by simp + next + case False + with i2 xs have xsi: "\<not>(i < length xs)" by auto + hence "(xs @ ys)!i = ys!(i - length xs)" + by (simp add: nth_append) + moreover + from xsi have "Suc i - length xs = Suc (i - length xs)" by auto + with xsi have "(xs @ ys)!(Suc i) = ys!(Suc (i - length xs))" + by (simp add: nth_append) + moreover + from i xsi have "i - length xs < length ys - 1" by auto + with 2 have "ys!(i - length xs) \<noteq> ys!(Suc (i - length xs))" + by (auto simp: noreps_def) + moreover + note eq + ultimately show False by simp + qed + qed + qed + qed +qed + +lemma ISpec_BInv_lemma: + "\<turnstile> BInit ic q oc \<and> \<box>[Nxt ic q oc]_(ic,q,oc) \<longrightarrow> \<box>(BInv ic q oc)" +proof (rule invmono) + show "\<turnstile> BInit ic q oc \<longrightarrow> BInv ic q oc" + by (auto simp: BInit_def BInv_def) +next + have enq: "|~ Enq ic q oc \<longrightarrow> BInv ic q oc \<longrightarrow> \<circ>(BInv ic q oc)" + by (auto simp: Enq_def BInv_def tla_defs) + have deq: "|~ Deq ic q oc \<longrightarrow> BInv ic q oc \<longrightarrow> \<circ>(BInv ic q oc)" + by (auto simp: Deq_def BInv_def tla_defs neq_Nil_conv) + have unch: "|~ Unchanged (ic,q,oc) \<longrightarrow> BInv ic q oc \<longrightarrow> \<circ>(BInv ic q oc)" + by (auto simp: BInv_def tla_defs) + show "|~ BInv ic q oc \<and> [Nxt ic q oc]_(ic, q, oc) \<longrightarrow> \<circ>(BInv ic q oc)" + by (auto simp: Nxt_def actrans_def + elim: enq[unlift_rule] deq[unlift_rule] unch[unlift_rule]) +qed + +theorem ISpec_BInv: "\<turnstile> ISpec ic q oc \<longrightarrow> \<box>(BInv ic q oc)" + by (auto simp: ISpec_def intro: ISpec_BInv_lemma[unlift_rule]) + + +subsection "Two FIFO buffers in a row implement a buffer" + +locale DBuffer = + fixes inp :: "'a statefun" -- {* input channel for double FIFO *} + and mid :: "'a statefun" -- {* channel linking the two buffers *} + and out :: "'a statefun" -- {* output channel for double FIFO *} + and q1 :: "'a list statefun" -- {* inner queue of first FIFO *} + and q2 :: "'a list statefun" -- {* inner queue of second FIFO *} + and vars + defines + vars: "vars \<equiv> LIFT (inp,mid,out,q1,q2)" + assumes DB_base: "basevars vars" +begin + + text {* + We need to specify the behavior of two FIFO buffers in a row. + Intuitively, that specification is just the conjunction of + two buffer specifications, where the first buffer has input + channel @{text inp} and output channel @{text mid} whereas + the second one receives from @{text mid} and outputs on @{text out}. + However, this conjunction allows a simultaneous enqueue action + of the first buffer and dequeue of the second one. It would not + implement the previous buffer specification, which excludes such + simultaneous enqueueing and dequeueing (it is written in + interleaving style''). We could relax the specification of + the FIFO buffer above, which is esthetically pleasant, but + non-interleaving specifications are usually hard to get right + and to understand. We therefore impose an interleaving constraint + on the specification of the double buffer, which requires that + enqueueing and dequeueing do not happen simultaneously. + *} + + definition DBSpec + where "DBSpec \<equiv> TEMP ISpec inp q1 mid + \<and> ISpec mid q2 out + \<and> \<box>[\<not>(Enq inp q1 mid \<and> Deq mid q2 out)]_vars" + + text {* + The proof rules of TLA are geared towards specifications of the + form @{text "Init \<and> \<box>[Next]_vars \<and> L"}, and we prove that + @{text DBSpec} corresponds to a specification in this form, + which we now define. + *} + + definition FullInit + where "FullInit \<equiv> TEMP (BInit inp q1 mid \<and> BInit mid q2 out)" + + definition FullNxt + where "FullNxt \<equiv> TEMP (Enq inp q1 mid \<and> Unchanged (q2,out) + \<or> Deq inp q1 mid \<and> Enq mid q2 out + \<or> Deq mid q2 out \<and> Unchanged (inp,q1))" + + definition FullSpec + where "FullSpec \<equiv> TEMP FullInit + \<and> \<box>[FullNxt]_vars + \<and> WF(Deq inp q1 mid)_vars + \<and> WF(Deq mid q2 out)_vars" + + text {* + The concatenation of the two queues will serve as the refinement mapping. + *} + definition qc :: "'a list statefun" + where "qc \<equiv> LIFT (q2 @ q1)" + + + lemmas db_defs = buffer_defs DBSpec_def FullInit_def FullNxt_def FullSpec_def + qc_def vars + + lemma DBSpec_stutinv: "STUTINV DBSpec" + unfolding db_defs by (simp add: bothstutinvs livestutinv) + + lemma FullSpec_stutinv: "STUTINV FullSpec" + unfolding db_defs by (simp add: bothstutinvs livestutinv) + + text {* + We prove that @{text DBSpec} implies @{text FullSpec}. (The converse + implication also holds but is not needed for our implementation proof.) + *} + + text {* + The following lemma is somewhat more bureaucratic than we'd like + it to be. It shows that the conjunction of the next-state relations, + together with the invariant for the first queue, implies the full + next-state relation of the combined queues. + *} + lemma DBNxt_then_FullNxt: + "\<turnstile> \<box>BInv inp q1 mid + \<and> \<box>[Nxt inp q1 mid]_(inp,q1,mid) + \<and> \<box>[Nxt mid q2 out]_(mid,q2,out) + \<and> \<box>[\<not>(Enq inp q1 mid \<and> Deq mid q2 out)]_vars + \<longrightarrow> \<box>[FullNxt]_vars" + (is "\<turnstile> \<box>?inv \<and> ?nxts \<longrightarrow> \<box>[FullNxt]_vars") + proof - + have "\<turnstile> \<box>[Nxt inp q1 mid]_(inp,q1,mid) + \<and> \<box>[Nxt mid q2 out]_(mid,q2,out) + \<longrightarrow> \<box>[ [Nxt inp q1 mid]_(inp,q1,mid) + \<and> [Nxt mid q2 out]_(mid,q2,out)]_((inp,q1,mid),(mid,q2,out))" + (is "\<turnstile> ?tmp \<longrightarrow> \<box>[?b1b2]_?vs") + by (auto simp: M12[int_rewrite]) + moreover + have "\<turnstile> \<box>[?b1b2]_?vs \<longrightarrow> \<box>[?b1b2]_vars" + by (rule R1, auto simp: vars_def tla_defs) + ultimately + have 1: "\<turnstile> \<box>[Nxt inp q1 mid]_(inp,q1,mid) + \<and> \<box>[Nxt mid q2 out]_(mid,q2,out) + \<longrightarrow> \<box>[ [Nxt inp q1 mid]_(inp,q1,mid) + \<and> [Nxt mid q2 out]_(mid,q2,out) ]_vars" + by force + have 2: "\<turnstile> \<box>[?b1b2]_vars \<and> \<box>[\<not>(Enq inp q1 mid \<and> Deq mid q2 out)]_vars + \<longrightarrow> \<box>[?b1b2 \<and> \<not>(Enq inp q1 mid \<and> Deq mid q2 out)]_vars" + (is "\<turnstile> ?tmp2 \<longrightarrow> \<box>[?mid]_vars") + by (simp add: M8[int_rewrite]) + have "\<turnstile> ?inv \<longrightarrow> #True" by auto + moreover + have "|~ ?inv \<and> \<circ>?inv \<and> [?mid]_vars \<longrightarrow> [FullNxt]_vars" + proof - + have "|~ ?inv \<and> ?mid \<longrightarrow> [FullNxt]_vars" + proof - + have A: "|~ Nxt inp q1 mid + \<longrightarrow> [Nxt mid q2 out]_(mid,q2,out) + \<longrightarrow> \<not>(Enq inp q1 mid \<and> Deq mid q2 out) + \<longrightarrow> ?inv + \<longrightarrow> FullNxt" + proof - + have enq: "|~ Enq inp q1 mid + \<and> [Nxt mid q2 out]_(mid,q2,out) + \<and> \<not>(Deq mid q2 out) + \<longrightarrow> Unchanged (q2,out)" + by (auto simp: db_defs tla_defs) + have deq1: "|~ Deq inp q1 mid \<longrightarrow> ?inv \<longrightarrow> mid$ \<noteq> $mid" + by (auto simp: Deq_def BInv_def) + have deq2: "|~ Deq mid q2 out \<longrightarrow> mid$ = $mid" + by (auto simp: Deq_def) + have deq: "|~ Deq inp q1 mid + \<and> [Nxt mid q2 out]_(mid,q2,out) + \<and> ?inv + \<longrightarrow> Enq mid q2 out" + by (force simp: Nxt_def tla_defs + dest: deq1[unlift_rule] deq2[unlift_rule]) + with enq show ?thesis by (force simp: Nxt_def FullNxt_def) + qed + have B: "|~ Nxt mid q2 out + \<longrightarrow> Unchanged (inp,q1,mid) + \<longrightarrow> FullNxt" + by (auto simp: db_defs tla_defs) + have C: "\<turnstile> Unchanged (inp,q1,mid) + \<longrightarrow> Unchanged (mid,q2,out) + \<longrightarrow> Unchanged vars" + by (auto simp: vars_def tla_defs) + show ?thesis + by (force simp: actrans_def + dest: A[unlift_rule] B[unlift_rule] C[unlift_rule]) + qed + thus ?thesis by (auto simp: tla_defs) + qed + ultimately + have "\<turnstile> \<box>?inv \<and> \<box>[?mid]_vars \<longrightarrow> \<box>#True \<and> \<box>[FullNxt]_vars" + by (rule TLA2) + with 1 2 show ?thesis by force + qed + + text {* + It is now easy to show that @{text DBSpec} refines @{text FullSpec}. + *} + theorem DBSpec_impl_FullSpec: "\<turnstile> DBSpec \<longrightarrow> FullSpec" + proof - + have 1: "\<turnstile> DBSpec \<longrightarrow> FullInit" + by (auto simp: DBSpec_def FullInit_def ISpec_def) + have 2: "\<turnstile> DBSpec \<longrightarrow> \<box>[FullNxt]_vars" + proof - + have "\<turnstile> DBSpec \<longrightarrow> \<box>(BInv inp q1 mid)" + by (auto simp: DBSpec_def intro: ISpec_BInv[unlift_rule]) + moreover have "\<turnstile> DBSpec \<and> \<box>(BInv inp q1 mid) \<longrightarrow> \<box>[FullNxt]_vars" + by (auto simp: DBSpec_def ISpec_def + intro: DBNxt_then_FullNxt[unlift_rule]) + ultimately show ?thesis by force + qed + have 3: "\<turnstile> DBSpec \<longrightarrow> WF(Deq inp q1 mid)_vars" + proof - + have 31: "\<turnstile> Unchanged vars \<longrightarrow> Unchanged q1" + by (auto simp: vars_def tla_defs) + have 32: "\<turnstile> Unchanged (inp,q1,mid) \<longrightarrow> Unchanged q1" + by (auto simp: tla_defs) + have deq: "|~ \<langle>Deq inp q1 mid\<rangle>_vars = \<langle>Deq inp q1 mid\<rangle>_(inp,q1,mid)" + by (simp add: Deq_visible[OF 31, int_rewrite] + Deq_visible[OF 32, int_rewrite]) + show ?thesis + by (auto simp: DBSpec_def ISpec_def WeakF_def + deq[int_rewrite] deq[THEN AA26,int_rewrite]) + qed + have 4: "\<turnstile> DBSpec \<longrightarrow> WF(Deq mid q2 out)_vars" + proof - + have 41: "\<turnstile> Unchanged vars \<longrightarrow> Unchanged q2" + by (auto simp: vars_def tla_defs) + have 42: "\<turnstile> Unchanged (mid,q2,out) \<longrightarrow> Unchanged q2" + by (auto simp: tla_defs) + have deq: "|~ \<langle>Deq mid q2 out\<rangle>_vars = \<langle>Deq mid q2 out\<rangle>_(mid,q2,out)" + by (simp add: Deq_visible[OF 41, int_rewrite] + Deq_visible[OF 42, int_rewrite]) + show ?thesis + by (auto simp: DBSpec_def ISpec_def WeakF_def + deq[int_rewrite] deq[THEN AA26,int_rewrite]) + qed + show ?thesis + by (auto simp: FullSpec_def + elim: 1[unlift_rule] 2[unlift_rule] 3[unlift_rule] + 4[unlift_rule]) + qed + + text {* + We now prove that two FIFO buffers in a row (as specified by formula + @{text FullSpec}) implement a FIFO buffer whose internal queue is the + concatenation of the two buffers. We start by proving step simulation. + *} + + lemma FullInit: "\<turnstile> FullInit \<longrightarrow> BInit inp qc out" + by (auto simp: db_defs tla_defs) + + lemma Full_step_simulation: + "|~ [FullNxt]_vars \<longrightarrow> [Nxt inp qc out]_(inp,qc,out)" + by (auto simp: db_defs tla_defs) + + text {* + The liveness condition requires that the combined buffer + eventually performs a @{text Deq} action on the output channel + if it contains some element. The idea is to use the + fairness hypothesis for the first buffer to prove that in that + case, eventually the queue of the second buffer will be + non-empty, and that it must therefore eventually dequeue + some element. + + The first step is to establish the enabledness conditions + for the two @{text Deq} actions of the implementation. + *} + + lemma Deq1_enabled: "\<turnstile> Enabled \<langle>Deq inp q1 mid\<rangle>_vars = ($q1 \<noteq> #[])"
+  proof -
+    have 1: "|~ \<langle>Deq inp q1 mid\<rangle>_vars = Deq inp q1 mid"
+      by (rule Deq_visible, auto simp: vars tla_defs)
+    have "\<turnstile> Enabled (Deq inp q1 mid) = ($q1 \<noteq> #[])" + by (force simp: Deq_def tla_defs vars + intro: base_enabled[OF DB_base] elim!: enabledE) + thus ?thesis by (simp add: 1[int_rewrite]) + qed + + lemma Deq2_enabled: "\<turnstile> Enabled \<langle>Deq mid q2 out\<rangle>_vars = ($q2 \<noteq> #[])"
+  proof -
+    have 1: "|~ \<langle>Deq mid q2 out\<rangle>_vars = Deq mid q2 out"
+      by (rule Deq_visible, auto simp: vars tla_defs)
+    have "\<turnstile> Enabled (Deq mid q2 out) = ($q2 \<noteq> #[])" + by (force simp: Deq_def tla_defs vars + intro: base_enabled[OF DB_base] elim!: enabledE) + thus ?thesis by (simp add: 1[int_rewrite]) + qed + + text {* + We now use rule @{text WF2} to prove that the combined buffer + (behaving according to specification @{text FullSpec}) + implements the fairness condition of the single buffer under + the refinement mapping. + *} + lemma Full_fairness: + "\<turnstile> \<box>[FullNxt]_vars \<and> WF(Deq mid q2 out)_vars \<and> \<box>WF(Deq inp q1 mid)_vars + \<longrightarrow> WF(Deq inp qc out)_(inp,qc,out)" + proof (rule WF2) + -- {* the helpful action is the @{text Deq} action of the second queue *} + show "|~ \<langle>FullNxt \<and> Deq mid q2 out\<rangle>_vars \<longrightarrow> \<langle>Deq inp qc out\<rangle>_(inp,qc,out)" + by (auto simp: db_defs tla_defs) + next + -- {* the helpful condition is the second queue being non-empty *} + show "|~ ($q2 \<noteq> #[]) \<and> \<circ>($q2 \<noteq> #[]) \<and> \<langle>FullNxt \<and> Deq mid q2 out\<rangle>_vars + \<longrightarrow> Deq mid q2 out" + by (auto simp: tla_defs) + next + show "\<turnstile>$q2 \<noteq> #[] \<and> Enabled \<langle>Deq inp qc out\<rangle>_(inp, qc, out)
+             \<longrightarrow> Enabled \<langle>Deq mid q2 out\<rangle>_vars"
+      unfolding Deq2_enabled[int_rewrite] by auto
+  next
+    txt {*
+      The difficult part of the proof is to show that the helpful
+      condition will eventually always be true provided that the
+      combined dequeue action is eventually always enabled and that
+      the helpful action is never executed. We prove that (1) the
+      helpful condition persists and (2) that it must eventually
+      become true.
+    *}
+    have "\<turnstile> \<box>\<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars
+            \<longrightarrow> \<box>($q2 \<noteq> #[] \<longrightarrow> \<box>($q2 \<noteq> #[]))"
+    proof (rule STL4)
+      have "|~ $q2 \<noteq> #[] \<and> [FullNxt \<and> \<not>(Deq mid q2 out)]_vars + \<longrightarrow> \<circ>($q2 \<noteq> #[])"
+        by (auto simp: db_defs tla_defs)
+      from this[THEN INV1]
+      show "\<turnstile> \<box>[FullNxt \<and> \<not> Deq mid q2 out]_vars
+              \<longrightarrow> ($q2 \<noteq> #[] \<longrightarrow> \<box>($q2 \<noteq> #[]))"
+        by auto
+    qed
+    hence 1: "\<turnstile> \<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars
+                \<longrightarrow> \<diamond>($q2 \<noteq> #[]) \<longrightarrow> \<diamond>\<box>($q2 \<noteq> #[])"
+      by (force intro: E31[unlift_rule])
+    have 2: "\<turnstile> \<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars
+               \<and> WF(Deq inp q1 mid)_vars
+               \<longrightarrow> (Enabled \<langle>Deq inp qc out\<rangle>_(inp, qc, out) \<leadsto> $q2 \<noteq> #[])" + proof - + have qc: "\<turnstile> ($qc \<noteq> #[]) = ($q1 \<noteq> #[] \<or>$q2 \<noteq> #[])"
+        by (auto simp: qc_def tla_defs)
+      have "\<turnstile> \<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars \<and> WF(Deq inp q1 mid)_vars
+              \<longrightarrow> ($q1 \<noteq> #[] \<leadsto>$q2 \<noteq> #[])"
+      proof (rule WF1)
+        show "|~ $q1 \<noteq> #[] \<and> [FullNxt \<and> \<not> Deq mid q2 out]_vars + \<longrightarrow> \<circ>($q1 \<noteq> #[]) \<or> \<circ>($q2 \<noteq> #[])" + by (auto simp: db_defs tla_defs) + next + show "|~$q1 \<noteq> #[]
+                 \<and> \<langle>(FullNxt \<and> \<not> Deq mid q2 out) \<and> Deq inp q1 mid\<rangle>_vars \<longrightarrow>
+                 \<circ>($q2 \<noteq> #[])" + by (auto simp: db_defs tla_defs) + next + show "\<turnstile>$q1 \<noteq> #[] \<longrightarrow> Enabled \<langle>Deq inp q1 mid\<rangle>_vars"
+      next
+        show "|~ $q1 \<noteq> #[] \<and> Unchanged vars \<longrightarrow> \<circ>($q1 \<noteq> #[])"
+          by (auto simp: vars tla_defs)
+      qed
+      hence "\<turnstile> \<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars
+                  \<and> WF(Deq inp q1 mid)_vars
+                  \<longrightarrow> ($qc \<noteq> #[] \<leadsto>$q2 \<noteq> #[])"
+        by (auto simp: qc[int_rewrite] LT17[int_rewrite] LT1[int_rewrite])
+      moreover
+      have "\<turnstile> Enabled \<langle>Deq inp qc out\<rangle>_(inp, qc, out) \<leadsto> $qc \<noteq> #[]" + by (rule Deq_enabledE[THEN LT3]) + ultimately show ?thesis by (force elim: LT13[unlift_rule]) + qed + with LT6 + have "\<turnstile> \<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars + \<and> WF(Deq inp q1 mid)_vars + \<and> \<diamond>Enabled \<langle>Deq inp qc out\<rangle>_(inp, qc, out) + \<longrightarrow> \<diamond>($q2 \<noteq> #[])"
+      by force
+    with 1 E16
+    show "\<turnstile> \<box>[FullNxt \<and> \<not>(Deq mid q2 out)]_vars
+            \<and> WF(Deq mid q2 out)_vars
+            \<and> \<box>WF(Deq inp q1 mid)_vars
+            \<and> \<diamond>\<box> Enabled \<langle>Deq inp qc out\<rangle>_(inp, qc, out)
+            \<longrightarrow> \<diamond>\<box>(\$q2 \<noteq> #[])"
+      by force
+  qed
+
+  text {*
+    Putting everything together, we obtain that @{text FullSpec} refines
+    the Buffer specification under the refinement mapping.
+  *}
+  theorem FullSpec_impl_ISpec: "\<turnstile> FullSpec \<longrightarrow> ISpec inp qc out"
+    unfolding FullSpec_def ISpec_def
+    using FullInit Full_step_simulation[THEN M11] Full_fairness
+    by force
+
+  theorem FullSpec_impl_Spec: "\<turnstile> FullSpec \<longrightarrow> Spec inp out"
+    unfolding Spec_def using FullSpec_impl_ISpec
+    by (force intro: eexI[unlift_rule])
+
+  text {*
+    By transitivity, two buffers in a row also implement a single buffer.
+  *}
+  theorem DBSpec_impl_Spec: "\<turnstile> DBSpec \<longrightarrow> Spec inp out"
+    by (rule lift_imp_trans[OF DBSpec_impl_FullSpec FullSpec_impl_Spec])
+
+end -- {* locale DBuffer *}
+
+end