# Theory Sender

Up to index of Isabelle/HOLCF/IOA/NTP

theory Sender
imports IOA Action
uses [Sender.ML]
begin

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

    header {* The implementation: sender *}

    theory Sender
    imports IOA Action
    begin

    types
    'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
    (*                messages   #sent           #received      header  mode *)

    consts

    sender_asig   :: "'m action signature"
    sender_trans  :: "('m action, 'm sender_state)transition set"
    sender_ioa    :: "('m action, 'm sender_state)ioa"
    sq            :: "'m sender_state => 'm list"
    ssent         :: "'m sender_state => bool multiset"
    srcvd         :: "'m sender_state => bool multiset"
    sbit          :: "'m sender_state => bool"
    ssending      :: "'m sender_state => bool"

    defs

    sq_def:       "sq == fst"
    ssent_def:    "ssent == fst o snd"
    srcvd_def:    "srcvd == fst o snd o snd"
    sbit_def:     "sbit == fst o snd o snd o snd"
    ssending_def: "ssending == snd o snd o snd o snd"

    sender_asig_def:
      "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
                      UN pkt. {S_pkt(pkt)},
                      {C_m_s,C_r_s})"

    sender_trans_def: "sender_trans ==
     {tr. let s = fst(tr);
              t = snd(snd(tr))
          in case fst(snd(tr))
          of
          S_msg(m) => sq(t)=sq(s)@[m]   &
                      ssent(t)=ssent(s) &
                      srcvd(t)=srcvd(s) &
                      sbit(t)=sbit(s)   &
                      ssending(t)=ssending(s) |
          R_msg(m) => False |
          S_pkt(pkt) => hdr(pkt) = sbit(s)      &
                           (? Q. sq(s) = (msg(pkt)#Q))  &
                           sq(t) = sq(s)           &
                           ssent(t) = addm (ssent s) (sbit s) &
                           srcvd(t) = srcvd(s) &
                           sbit(t) = sbit(s)   &
                           ssending(s)         &
                           ssending(t) |
        R_pkt(pkt) => False |
        S_ack(b)   => False |
          R_ack(b) => sq(t)=sq(s)                  &
                         ssent(t)=ssent(s)            &
                         srcvd(t) = addm (srcvd s) b  &
                         sbit(t)=sbit(s)              &
                         ssending(t)=ssending(s) |
          C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) &
                   sq(t)=sq(s)       &
                   ssent(t)=ssent(s) &
                   srcvd(t)=srcvd(s) &
                   sbit(t)=sbit(s)   &
                   ssending(s)       &
                   ~ssending(t) |
          C_m_r => False |
          C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) &
                   sq(t)=tl(sq(s))      &
                   ssent(t)=ssent(s)    &
                   srcvd(t)=srcvd(s)    &
                   sbit(t) = (~sbit(s)) &
                   ~ssending(s)         &
                   ssending(t) |
          C_r_r(m) => False}"

    sender_ioa_def: "sender_ioa ==
     (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem in_sender_asig:

      S_msg m ∈ actions sender_asig ∧
      R_msg m ∉ actions sender_asig ∧
      S_pkt pkt ∈ actions sender_asig ∧
      R_pkt pkt ∉ actions sender_asig ∧
      S_ack b ∉ actions sender_asig ∧
      R_ack b ∈ actions sender_asig ∧
      C_m_s ∈ actions sender_asig ∧
      C_m_r ∉ actions sender_asig ∧
      C_r_s ∈ actions sender_asig ∧ C_r_r m ∉ actions sender_asig