# Theory Buffer

Up to index of Isabelle/HOL/TLA

theory Buffer
imports State
(*  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 Bufferimports Statebegintext {*  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 => 'a list statefun => 'a statefun => temporal"where "BInit ic q oc ≡ TEMP $q = #[] ∧$ic = $oc" -- {* initial condition of buffer *}definition Enq :: "'a statefun => 'a list statefun => 'a statefun => temporal"where "Enq ic q oc ≡ TEMP ic$ ≠ $ic ∧ q$ = $q @ [ ic$ ]                        ∧ oc$=$oc"     -- {* enqueue a new value *}definition Deq :: "'a statefun => 'a list statefun => 'a statefun => temporal"where "Deq ic q oc ≡ TEMP # 0 < length<$q> ∧ oc$ = hd<$q> ∧ q$ = tl<$q> ∧ ic$ = $ic" -- {* dequeue value at front *}definition Nxt :: "'a statefun => 'a list statefun => 'a statefun => temporal"where "Nxt ic q oc ≡ TEMP (Enq ic q oc ∨ Deq ic q oc)"-- {* internal specification with buffer visible *}definition ISpec :: "'a statefun => 'a list statefun => 'a statefun => temporal"where "ISpec ic q oc ≡ TEMP BInit ic q oc ∧ \<box>[Nxt ic q oc]_(ic,q,oc) ∧ WF(Deq ic q oc)_(ic,q,oc)"-- {* external specification: buffer hidden *}definition Spec :: "'a statefun => 'a statefun => 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 => bool"where "noreps xs ≡ ∀i < length xs - 1. xs!i ≠ xs!(Suc i)"definition BInv :: "'a statefun => 'a list statefun => 'a statefun => temporal"where "BInv ic q oc ≡ TEMP List.last<$oc # $q> =$ic ∧ noreps<$oc #$q>"lemmas buffer_defs = BInit_def Enq_def Deq_def Nxt_def                      ISpec_def Spec_def BInv_deflemma 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 ≠ []" with 1 show "False"      by (auto simp: neq_Nil_conv)  qedqed (auto)lemma tl_self_iff_empty'[simp]: "(xs = tl xs) = (xs = [])"proof  assume 1: "xs = tl xs"  show "xs = []"  proof (rule ccontr)    assume "xs ≠ []" with 1 show "False"      by (auto simp: neq_Nil_conv)  qedqed (auto)lemma Deq_visible:  assumes v: "\<turnstile> Unchanged v --> 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)qedlemma Deq_enabledE: "\<turnstile> Enabled <Deq ic q oc>_(ic,q,oc) --> $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 ∧ (xs = [] ∨ x ≠ 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) qednext assume 1: "noreps (hd xs # xs)" and 2: "xs ≠ []" 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 ≠ 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 qedqedlemma noreps_append [simp]: "noreps (xs @ ys) = (noreps xs ∧ noreps ys ∧ (xs = [] ∨ ys = [] ∨ List.last xs ≠ 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) qednext 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) qednext assume 1: "noreps (xs @ ys)" and 2: "xs ≠ []" and 3: "ys ≠ []" 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 ≠ hd ys" show "noreps (xs @ ys)" proof (cases "xs = [] ∨ 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: "¬(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: "¬(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) ≠ ys!(Suc (i - length xs))" by (auto simp: noreps_def) moreover note eq ultimately show False by simp qed qed qed qedqedlemma ISpec_BInv_lemma: "\<turnstile> BInit ic q oc ∧ \<box>[Nxt ic q oc]_(ic,q,oc) --> \<box>(BInv ic q oc)"proof (rule invmono) show "\<turnstile> BInit ic q oc --> BInv ic q oc" by (auto simp: BInit_def BInv_def)next have enq: "|~ Enq ic q oc --> BInv ic q oc --> o(BInv ic q oc)" by (auto simp: Enq_def BInv_def tla_defs) have deq: "|~ Deq ic q oc --> BInv ic q oc --> o(BInv ic q oc)" by (auto simp: Deq_def BInv_def tla_defs neq_Nil_conv) have unch: "|~ Unchanged (ic,q,oc) --> BInv ic q oc --> o(BInv ic q oc)" by (auto simp: BInv_def tla_defs) show "|~ BInv ic q oc ∧ [Nxt ic q oc]_(ic, q, oc) --> o(BInv ic q oc)" by (auto simp: Nxt_def actrans_def elim: enq[unlift_rule] deq[unlift_rule] unch[unlift_rule])qedtheorem ISpec_BInv: "\<turnstile> ISpec ic q oc --> \<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 ≡ 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 ≡ TEMP ISpec inp q1 mid ∧ ISpec mid q2 out ∧ \<box>[¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars" text {* The proof rules of TLA are geared towards specifications of the form @{text "Init ∧ \<box>[Next]_vars ∧ L"}, and we prove that @{text DBSpec} corresponds to a specification in this form, which we now define. *} definition FullInit where "FullInit ≡ TEMP (BInit inp q1 mid ∧ BInit mid q2 out)" definition FullNxt where "FullNxt ≡ TEMP (Enq inp q1 mid ∧ Unchanged (q2,out) ∨ Deq inp q1 mid ∧ Enq mid q2 out ∨ Deq mid q2 out ∧ Unchanged (inp,q1))" definition FullSpec where "FullSpec ≡ TEMP FullInit ∧ \<box>[FullNxt]_vars ∧ WF(Deq inp q1 mid)_vars ∧ 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 ≡ LIFT (q2 @ q1)" lemmas db_defs = buffer_defs DBSpec_def FullInit_def FullNxt_def FullSpec_def qc_def vars_def 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 ∧ \<box>[Nxt inp q1 mid]_(inp,q1,mid) ∧ \<box>[Nxt mid q2 out]_(mid,q2,out) ∧ \<box>[¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars --> \<box>[FullNxt]_vars" (is "\<turnstile> \<box>?inv ∧ ?nxts --> \<box>[FullNxt]_vars") proof - have "\<turnstile> \<box>[Nxt inp q1 mid]_(inp,q1,mid) ∧ \<box>[Nxt mid q2 out]_(mid,q2,out) --> \<box>[ [Nxt inp q1 mid]_(inp,q1,mid) ∧ [Nxt mid q2 out]_(mid,q2,out)]_((inp,q1,mid),(mid,q2,out))" (is "\<turnstile> ?tmp --> \<box>[?b1b2]_?vs") by (auto simp: M12[int_rewrite]) moreover have "\<turnstile> \<box>[?b1b2]_?vs --> \<box>[?b1b2]_vars" by (rule R1, auto simp: vars_def tla_defs) ultimately have 1: "\<turnstile> \<box>[Nxt inp q1 mid]_(inp,q1,mid) ∧ \<box>[Nxt mid q2 out]_(mid,q2,out) --> \<box>[ [Nxt inp q1 mid]_(inp,q1,mid) ∧ [Nxt mid q2 out]_(mid,q2,out) ]_vars" by force have 2: "\<turnstile> \<box>[?b1b2]_vars ∧ \<box>[¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars --> \<box>[?b1b2 ∧ ¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars" (is "\<turnstile> ?tmp2 --> \<box>[?mid]_vars") by (simp add: M8[int_rewrite]) have "\<turnstile> ?inv --> #True" by auto moreover have "|~ ?inv ∧ o?inv ∧ [?mid]_vars --> [FullNxt]_vars" proof - have "|~ ?inv ∧ ?mid --> [FullNxt]_vars" proof - have A: "|~ Nxt inp q1 mid --> [Nxt mid q2 out]_(mid,q2,out) --> ¬(Enq inp q1 mid ∧ Deq mid q2 out) --> ?inv --> FullNxt" proof - have enq: "|~ Enq inp q1 mid ∧ [Nxt mid q2 out]_(mid,q2,out) ∧ ¬(Deq mid q2 out) --> Unchanged (q2,out)" by (auto simp: db_defs tla_defs) have deq1: "|~ Deq inp q1 mid --> ?inv --> mid$ ≠ $mid" by (auto simp: Deq_def BInv_def) have deq2: "|~ Deq mid q2 out --> mid$ = $mid" by (auto simp: Deq_def) have deq: "|~ Deq inp q1 mid ∧ [Nxt mid q2 out]_(mid,q2,out) ∧ ?inv --> 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 --> Unchanged (inp,q1,mid) --> FullNxt" by (auto simp: db_defs tla_defs) have C: "\<turnstile> Unchanged (inp,q1,mid) --> Unchanged (mid,q2,out) --> 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 ∧ \<box>[?mid]_vars --> \<box>#True ∧ \<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 --> FullSpec" proof - have 1: "\<turnstile> DBSpec --> FullInit" by (auto simp: DBSpec_def FullInit_def ISpec_def) have 2: "\<turnstile> DBSpec --> \<box>[FullNxt]_vars" proof - have "\<turnstile> DBSpec --> \<box>(BInv inp q1 mid)" by (auto simp: DBSpec_def intro: ISpec_BInv[unlift_rule]) moreover have "\<turnstile> DBSpec ∧ \<box>(BInv inp q1 mid) --> \<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 --> WF(Deq inp q1 mid)_vars" proof - have 31: "\<turnstile> Unchanged vars --> Unchanged q1" by (auto simp: vars_def tla_defs) have 32: "\<turnstile> Unchanged (inp,q1,mid) --> Unchanged q1" by (auto simp: tla_defs) have deq: "|~ ⟨Deq inp q1 mid⟩_vars = ⟨Deq inp q1 mid⟩_(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 --> WF(Deq mid q2 out)_vars" proof - have 41: "\<turnstile> Unchanged vars --> Unchanged q2" by (auto simp: vars_def tla_defs) have 42: "\<turnstile> Unchanged (mid,q2,out) --> Unchanged q2" by (auto simp: tla_defs) have deq: "|~ ⟨Deq mid q2 out⟩_vars = ⟨Deq mid q2 out⟩_(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 --> BInit inp qc out" by (auto simp: db_defs tla_defs) lemma Full_step_simulation: "|~ [FullNxt]_vars --> [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 ⟨Deq inp q1 mid⟩_vars = ($q1 ≠ #[])"  proof -    have 1: "|~ ⟨Deq inp q1 mid⟩_vars = Deq inp q1 mid"      by (rule Deq_visible, auto simp: vars_def tla_defs)    have "\<turnstile> Enabled (Deq inp q1 mid) = ($q1 ≠ #[])" by (force simp: Deq_def tla_defs vars_def intro: base_enabled[OF DB_base] elim!: enabledE) thus ?thesis by (simp add: 1[int_rewrite]) qed lemma Deq2_enabled: "\<turnstile> Enabled ⟨Deq mid q2 out⟩_vars = ($q2 ≠ #[])"  proof -    have 1: "|~ ⟨Deq mid q2 out⟩_vars = Deq mid q2 out"      by (rule Deq_visible, auto simp: vars_def tla_defs)    have "\<turnstile> Enabled (Deq mid q2 out) = ($q2 ≠ #[])" by (force simp: Deq_def tla_defs vars_def 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 ∧ WF(Deq mid q2 out)_vars ∧ \<box>WF(Deq inp q1 mid)_vars --> WF(Deq inp qc out)_(inp,qc,out)" proof (rule WF2) -- {* the helpful action is the @{text Deq} action of the second queue *} show "|~ ⟨FullNxt ∧ Deq mid q2 out⟩_vars --> ⟨Deq inp qc out⟩_(inp,qc,out)" by (auto simp: db_defs tla_defs) next -- {* the helpful condition is the second queue being non-empty *} show "|~ ($q2 ≠ #[]) ∧ o($q2 ≠ #[]) ∧ ⟨FullNxt ∧ Deq mid q2 out⟩_vars --> Deq mid q2 out" by (auto simp: tla_defs) next show "\<turnstile>$q2 ≠ #[] ∧ Enabled ⟨Deq inp qc out⟩_(inp, qc, out)             --> Enabled ⟨Deq mid q2 out⟩_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 ∧ ¬(Deq mid q2 out)]_vars            --> \<box>($q2 ≠ #[] --> \<box>($q2 ≠ #[]))"    proof (rule STL4)      have "|~ $q2 ≠ #[] ∧ [FullNxt ∧ ¬(Deq mid q2 out)]_vars --> o($q2 ≠ #[])"        by (auto simp: db_defs tla_defs)      from this[THEN INV1]      show "\<turnstile> \<box>[FullNxt ∧ ¬ Deq mid q2 out]_vars              --> ($q2 ≠ #[] --> \<box>($q2 ≠ #[]))"        by auto    qed    hence 1: "\<turnstile> \<box>[FullNxt ∧ ¬(Deq mid q2 out)]_vars                --> \<diamond>($q2 ≠ #[]) --> \<diamond>\<box>($q2 ≠ #[])"      by (force intro: E31[unlift_rule])    have 2: "\<turnstile> \<box>[FullNxt ∧ ¬(Deq mid q2 out)]_vars               ∧ WF(Deq inp q1 mid)_vars               --> (Enabled ⟨Deq inp qc out⟩_(inp, qc, out) \<leadsto> $q2 ≠ #[])" proof - have qc: "\<turnstile> ($qc ≠ #[]) = ($q1 ≠ #[] ∨$q2 ≠ #[])"        by (auto simp: qc_def tla_defs)      have "\<turnstile> \<box>[FullNxt ∧ ¬(Deq mid q2 out)]_vars ∧ WF(Deq inp q1 mid)_vars              --> ($q1 ≠ #[] \<leadsto>$q2 ≠ #[])"      proof (rule WF1)        show "|~ $q1 ≠ #[] ∧ [FullNxt ∧ ¬ Deq mid q2 out]_vars --> o($q1 ≠ #[]) ∨ o($q2 ≠ #[])" by (auto simp: db_defs tla_defs) next show "|~$q1 ≠ #[]                  ∧ ⟨(FullNxt ∧ ¬ Deq mid q2 out) ∧ Deq inp q1 mid⟩_vars -->                 o($q2 ≠ #[])" by (auto simp: db_defs tla_defs) next show "\<turnstile>$q1 ≠ #[] --> Enabled ⟨Deq inp q1 mid⟩_vars"          by (simp add: Deq1_enabled[int_rewrite])      next        show "|~ $q1 ≠ #[] ∧ Unchanged vars --> o($q1 ≠ #[])"          by (auto simp: vars_def tla_defs)      qed      hence "\<turnstile> \<box>[FullNxt ∧ ¬(Deq mid q2 out)]_vars                   ∧ WF(Deq inp q1 mid)_vars                  --> ($qc ≠ #[] \<leadsto>$q2 ≠ #[])"        by (auto simp: qc[int_rewrite] LT17[int_rewrite] LT1[int_rewrite])      moreover      have "\<turnstile> Enabled ⟨Deq inp qc out⟩_(inp, qc, out) \<leadsto> $qc ≠ #[]" by (rule Deq_enabledE[THEN LT3]) ultimately show ?thesis by (force elim: LT13[unlift_rule]) qed with LT6 have "\<turnstile> \<box>[FullNxt ∧ ¬(Deq mid q2 out)]_vars ∧ WF(Deq inp q1 mid)_vars ∧ \<diamond>Enabled ⟨Deq inp qc out⟩_(inp, qc, out) --> \<diamond>($q2 ≠ #[])"      by force    with 1 E16    show "\<turnstile> \<box>[FullNxt ∧ ¬(Deq mid q2 out)]_vars            ∧ WF(Deq mid q2 out)_vars            ∧ \<box>WF(Deq inp q1 mid)_vars            ∧ \<diamond>\<box> Enabled ⟨Deq inp qc out⟩_(inp, qc, out)            --> \<diamond>\<box>(\$q2 ≠ #[])"      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 --> 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 --> 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 --> Spec inp out"    by (rule lift_imp_trans[OF DBSpec_impl_FullSpec FullSpec_impl_Spec])end -- {* locale DBuffer *}end