Theory Buffer

(*  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>
*)

section ‹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 ⇒ '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
                          ∧ □[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 (∃∃ 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 ‹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_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 ≠ []" 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 ≠ []" with 1 show "False"
      by (auto simp: neq_Nil_conv)
  qed
qed (auto)

lemma Deq_visible:
  assumes v: "⊢ Unchanged v ⟶ Unchanged q"
  shows "|~ <Deq ic q oc>_v = Deq ic q oc"
proof (auto simp: tla_defs)
  fix w
  assume deq: "w ⊨ 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: "⊢ Enabled <Deq ic q oc>_(ic,q,oc) ⟶ $q ~= #[]"
  by (auto elim!: enabledE simp: Deq_def tla_defs)

text ‹
  We now prove that ‹BInv› is an invariant of the Buffer
  specification.

  We need several lemmas about ‹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)
  qed
next
  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
  qed
qed

lemma 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)
  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 ≠ []" 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
  qed
qed

lemma ISpec_BInv_lemma:
  "⊢ BInit ic q oc ∧ □[Nxt ic q oc]_(ic,q,oc) ⟶ □(BInv ic q oc)"
proof (rule invmono)
  show "⊢ 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 ⟶ ○(BInv ic q oc)"
    by (auto simp: Enq_def BInv_def tla_defs)
  have deq: "|~ Deq ic q oc ⟶ BInv ic q oc ⟶ ○(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 ⟶ ○(BInv ic q oc)"
    by (auto simp: BInv_def tla_defs)
  show "|~ BInv ic q oc ∧ [Nxt ic q oc]_(ic, q, oc) ⟶ ○(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: "⊢ ISpec ic q oc ⟶ □(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 ‹inp› and output channel ‹mid› whereas
    the second one receives from ‹mid› and outputs on ‹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
                     ∧ □[¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars"

  text ‹
    The proof rules of TLA are geared towards specifications of the
    form ‹Init ∧ □[Next]_vars ∧ L›, and we prove that
    ‹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
                       ∧ □[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 ‹DBSpec› implies ‹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:
    "⊢ □BInv inp q1 mid
        ∧ □[Nxt inp q1 mid]_(inp,q1,mid) 
        ∧ □[Nxt mid q2 out]_(mid,q2,out)
        ∧ □[¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars
        ⟶ □[FullNxt]_vars"
    (is "⊢ □?inv ∧ ?nxts ⟶ □[FullNxt]_vars")
  proof -
    have "⊢ □[Nxt inp q1 mid]_(inp,q1,mid)
          ∧ □[Nxt mid q2 out]_(mid,q2,out)
          ⟶ □[  [Nxt inp q1 mid]_(inp,q1,mid) 
               ∧ [Nxt mid q2 out]_(mid,q2,out)]_((inp,q1,mid),(mid,q2,out))"
      (is "⊢ ?tmp ⟶ □[?b1b2]_?vs")
      by (auto simp: M12[int_rewrite])
    moreover
    have "⊢ □[?b1b2]_?vs ⟶ □[?b1b2]_vars"
      by (rule R1, auto simp: vars_def tla_defs)
    ultimately
    have 1: "⊢ □[Nxt inp q1 mid]_(inp,q1,mid)
             ∧ □[Nxt mid q2 out]_(mid,q2,out)
             ⟶ □[  [Nxt inp q1 mid]_(inp,q1,mid) 
                   ∧ [Nxt mid q2 out]_(mid,q2,out) ]_vars"
      by force
    have 2: "⊢ □[?b1b2]_vars ∧ □[¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars
               ⟶ □[?b1b2 ∧ ¬(Enq inp q1 mid ∧ Deq mid q2 out)]_vars"
      (is "⊢ ?tmp2 ⟶ □[?mid]_vars")
      by (simp add: M8[int_rewrite])
    have "⊢ ?inv ⟶ #True" by auto
    moreover
    have "|~ ?inv ∧ ○?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: "⊢ 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 "⊢ □?inv ∧ □[?mid]_vars ⟶ □#True ∧ □[FullNxt]_vars"
      by (rule TLA2)
    with 1 2 show ?thesis by force
  qed

  text ‹
    It is now easy to show that ‹DBSpec› refines ‹FullSpec›.
›
  theorem DBSpec_impl_FullSpec: "⊢ DBSpec ⟶ FullSpec"
  proof -
    have 1: "⊢ DBSpec ⟶ FullInit"
      by (auto simp: DBSpec_def FullInit_def ISpec_def)
    have 2: "⊢ DBSpec ⟶ □[FullNxt]_vars"
    proof -
      have "⊢ DBSpec ⟶ □(BInv inp q1 mid)"
        by (auto simp: DBSpec_def intro: ISpec_BInv[unlift_rule])
      moreover have "⊢ DBSpec ∧ □(BInv inp q1 mid) ⟶ □[FullNxt]_vars"
        by (auto simp: DBSpec_def ISpec_def
                 intro: DBNxt_then_FullNxt[unlift_rule])
      ultimately show ?thesis by force
    qed
    have 3: "⊢ DBSpec ⟶ WF(Deq inp q1 mid)_vars"
    proof -
      have 31: "⊢ Unchanged vars ⟶ Unchanged q1"
        by (auto simp: vars_def tla_defs)
      have 32: "⊢ 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: "⊢ DBSpec ⟶ WF(Deq mid q2 out)_vars"
    proof -
      have 41: "⊢ Unchanged vars ⟶ Unchanged q2"
        by (auto simp: vars_def tla_defs)
      have 42: "⊢ 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
    ‹FullSpec›) implement a FIFO buffer whose internal queue is the
    concatenation of the two buffers. We start by proving step simulation.
›  

  lemma FullInit: "⊢ 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 ‹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 ‹Deq› actions of the implementation.
›

  lemma Deq1_enabled: "⊢ 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 "⊢ 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: "⊢ 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 "⊢ 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 ‹WF2› to prove that the combined buffer
    (behaving according to specification ‹FullSpec›)
    implements the fairness condition of the single buffer under
    the refinement mapping.
›
  lemma Full_fairness:
    "⊢ □[FullNxt]_vars ∧ WF(Deq mid q2 out)_vars ∧ □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 ≠ #[]) ∧ ○($q2 ≠ #[]) ∧ ⟨FullNxt ∧ Deq mid q2 out⟩_vars 
             ⟶ Deq mid q2 out"
      by (auto simp: tla_defs)
  next
    show "⊢ $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 "⊢ □□[FullNxt ∧ ¬(Deq mid q2 out)]_vars
            ⟶ □($q2 ≠ #[] ⟶ □($q2 ≠ #[]))"
    proof (rule STL4)
      have "|~ $q2 ≠ #[] ∧ [FullNxt ∧ ¬(Deq mid q2 out)]_vars
               ⟶ ○($q2 ≠ #[])"
        by (auto simp: db_defs tla_defs)
      from this[THEN INV1]
      show "⊢ □[FullNxt ∧ ¬ Deq mid q2 out]_vars
              ⟶ ($q2 ≠ #[] ⟶ □($q2 ≠ #[]))"
        by auto
    qed
    hence 1: "⊢ □[FullNxt ∧ ¬(Deq mid q2 out)]_vars
                ⟶ ◇($q2 ≠ #[]) ⟶ ◇□($q2 ≠ #[])"
      by (force intro: E31[unlift_rule])
    have 2: "⊢ □[FullNxt ∧ ¬(Deq mid q2 out)]_vars
               ∧ WF(Deq inp q1 mid)_vars
               ⟶ (Enabled ⟨Deq inp qc out⟩_(inp, qc, out) ↝ $q2 ≠ #[])"
    proof -
      have qc: "⊢ ($qc ≠ #[]) = ($q1 ≠ #[] ∨ $q2 ≠ #[])"
        by (auto simp: qc_def tla_defs)
      have "⊢ □[FullNxt ∧ ¬(Deq mid q2 out)]_vars ∧ WF(Deq inp q1 mid)_vars
              ⟶ ($q1 ≠ #[] ↝ $q2 ≠ #[])"
      proof (rule WF1)
        show "|~ $q1 ≠ #[] ∧ [FullNxt ∧ ¬ Deq mid q2 out]_vars
                 ⟶ ○($q1 ≠ #[]) ∨ ○($q2 ≠ #[])"
          by (auto simp: db_defs tla_defs)
      next
        show "|~ $q1 ≠ #[] 
                 ∧ ⟨(FullNxt ∧ ¬ Deq mid q2 out) ∧ Deq inp q1 mid⟩_vars ⟶
                 ○($q2 ≠ #[])"
          by (auto simp: db_defs tla_defs)
      next
        show "⊢ $q1 ≠ #[] ⟶ Enabled ⟨Deq inp q1 mid⟩_vars"
          by (simp add: Deq1_enabled[int_rewrite])
      next
        show "|~ $q1 ≠ #[] ∧ Unchanged vars ⟶ ○($q1 ≠ #[])"
          by (auto simp: vars_def tla_defs)
      qed
      hence "⊢ □[FullNxt ∧ ¬(Deq mid q2 out)]_vars 
                  ∧ WF(Deq inp q1 mid)_vars
                  ⟶ ($qc ≠ #[] ↝ $q2 ≠ #[])"
        by (auto simp: qc[int_rewrite] LT17[int_rewrite] LT1[int_rewrite])
      moreover
      have "⊢ Enabled ⟨Deq inp qc out⟩_(inp, qc, out) ↝ $qc ≠ #[]"
        by (rule Deq_enabledE[THEN LT3])
      ultimately show ?thesis by (force elim: LT13[unlift_rule])
    qed
    with LT6 
    have "⊢ □[FullNxt ∧ ¬(Deq mid q2 out)]_vars
             ∧ WF(Deq inp q1 mid)_vars
             ∧ ◇Enabled ⟨Deq inp qc out⟩_(inp, qc, out)
             ⟶ ◇($q2 ≠ #[])"
      by force
    with 1 E16
    show "⊢ □[FullNxt ∧ ¬(Deq mid q2 out)]_vars
            ∧ WF(Deq mid q2 out)_vars
            ∧ □WF(Deq inp q1 mid)_vars
            ∧ ◇□ Enabled ⟨Deq inp qc out⟩_(inp, qc, out)
            ⟶ ◇□($q2 ≠ #[])"
      by force
  qed

  text ‹
    Putting everything together, we obtain that ‹FullSpec› refines
    the Buffer specification under the refinement mapping.
›
  theorem FullSpec_impl_ISpec: "⊢ 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: "⊢ 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: "⊢ DBSpec ⟶ Spec inp out"
    by (rule lift_imp_trans[OF DBSpec_impl_FullSpec FullSpec_impl_Spec])

end ― ‹locale DBuffer›

end