# Theory Buffer

Up to index of Isabelle/HOL/TLA/Buffer

theory Buffer
imports TLA
uses [Buffer.ML]
begin

    (*
        File:        Buffer.thy
        ID:          $Id: Buffer.thy,v 1.3 2005/09/07 18:22:40 wenzelm Exp $
        Author:      Stephan Merz
        Copyright:   1997 University of Munich

       Theory Name: Buffer
       Logic Image: TLA
    *)

    header {* A simple FIFO buffer (synchronous communication, interleaving) *}

    theory Buffer
    imports TLA
    begin

    consts
      (* actions *)
      BInit     :: "'a stfun => 'a list stfun => 'a stfun => stpred"
      Enq       :: "'a stfun => 'a list stfun => 'a stfun => action"
      Deq       :: "'a stfun => 'a list stfun => 'a stfun => action"
      Next      :: "'a stfun => 'a list stfun => 'a stfun => action"

      (* temporal formulas *)
      IBuffer   :: "'a stfun => 'a list stfun => 'a stfun => temporal"
      Buffer    :: "'a stfun => 'a stfun => temporal"

    defs
      BInit_def:   "BInit ic q oc    == PRED q = #[]"
      Enq_def:     "Enq ic q oc      == ACT (ic$ ~= $ic)
                                         & (q$ = $q @ [ ic$ ])
                                         & (oc$ = $oc)"
      Deq_def:     "Deq ic q oc      == ACT ($q ~= #[])
                                         & (oc$ = hd< $q >)
                                         & (q$ = tl< $q >)
                                         & (ic$ = $ic)"
      Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
      IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
                                          & [][Next ic q oc]_(ic,q,oc)
                                          & WF(Deq ic q oc)_(ic,q,oc)"
      Buffer_def:  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem tl_not_self:

      xs ≠ [] ==> tl xs ≠ xs

theorem Deq_visible:

      |- <Deq ic q oc>_(ic, q, oc) = Deq ic q oc

theorem Deq_enabled:

      basevars (ic, q, oc) ==> |- Enabled (<Deq ic q oc>_(ic, q, oc)) = (q ≠ #[])

theorem Deq_enabledE:

      |- Enabled (<Deq ic q oc>_(ic, q, oc)) --> q ≠ #[]