# Theory Spec

Up to index of Isabelle/HOLCF/IOA/NTP

theory Spec
imports IOA Action
begin

    (*  Title:      HOL/IOA/NTP/Spec.thy
        ID:         $Id: Spec.thy,v 1.6 2005/09/03 14:50:25 wenzelm Exp $
        Author:     Tobias Nipkow & Konrad Slind
    *)

    header {* The specification of reliable transmission *}

    theory Spec
    imports IOA Action
    begin

    consts

    spec_sig   :: "'m action signature"
    spec_trans :: "('m action, 'm list)transition set"
    spec_ioa   :: "('m action, 'm list)ioa"

    defs

    sig_def: "spec_sig == (UN m.{S_msg(m)},
                         UN m.{R_msg(m)},
                         {})"

    trans_def: "spec_trans ==
     {tr. let s = fst(tr);
              t = snd(snd(tr))
          in
          case fst(snd(tr))
          of
          S_msg(m) => t = s@[m]  |
          R_msg(m) => s = (m#t)  |
          S_pkt(pkt) => False |
          R_pkt(pkt) => False |
          S_ack(b) => False |
          R_ack(b) => False |
          C_m_s => False |
          C_m_r => False |
          C_r_s => False |
          C_r_r(m) => False}"

    ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})"

    ML {* use_legacy_bindings (the_context ()) *}

    end