src/HOL/HOLCF/IOA/NTP/Sender.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61032 b57df8eecad6
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/NTP/Sender.thy
mueller@3073
     2
    Author:     Tobias Nipkow & Konrad Slind
mueller@3073
     3
*)
mueller@3073
     4
wenzelm@58880
     5
section {* The implementation: sender *}
wenzelm@17244
     6
wenzelm@17244
     7
theory Sender
wenzelm@17244
     8
imports IOA Action
wenzelm@17244
     9
begin
mueller@3073
    10
huffman@41476
    11
type_synonym
mueller@3073
    12
'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
mueller@3073
    13
(*                messages   #sent           #received      header  mode *)
mueller@3073
    14
wenzelm@27361
    15
definition sq :: "'m sender_state => 'm list" where "sq = fst"
wenzelm@27361
    16
definition ssent :: "'m sender_state => bool multiset" where "ssent = fst o snd"
wenzelm@27361
    17
definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst o snd o snd"
wenzelm@27361
    18
definition sbit :: "'m sender_state => bool" where "sbit = fst o snd o snd o snd"
wenzelm@27361
    19
definition ssending :: "'m sender_state => bool" where "ssending = snd o snd o snd o snd"
mueller@3073
    20
wenzelm@27361
    21
definition
wenzelm@27361
    22
  sender_asig :: "'m action signature" where
wenzelm@27361
    23
  "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
wenzelm@27361
    24
                   UN pkt. {S_pkt(pkt)},
wenzelm@27361
    25
                   {C_m_s,C_r_s})"
mueller@3073
    26
wenzelm@27361
    27
definition
wenzelm@27361
    28
  sender_trans :: "('m action, 'm sender_state)transition set" where
wenzelm@27361
    29
  "sender_trans =
wenzelm@17244
    30
 {tr. let s = fst(tr);
wenzelm@17244
    31
          t = snd(snd(tr))
wenzelm@17244
    32
      in case fst(snd(tr))
wenzelm@17244
    33
      of
wenzelm@17244
    34
      S_msg(m) => sq(t)=sq(s)@[m]   &
wenzelm@17244
    35
                  ssent(t)=ssent(s) &
wenzelm@17244
    36
                  srcvd(t)=srcvd(s) &
wenzelm@17244
    37
                  sbit(t)=sbit(s)   &
wenzelm@17244
    38
                  ssending(t)=ssending(s) |
wenzelm@17244
    39
      R_msg(m) => False |
wenzelm@17244
    40
      S_pkt(pkt) => hdr(pkt) = sbit(s)      &
wenzelm@17244
    41
                       (? Q. sq(s) = (msg(pkt)#Q))  &
wenzelm@17244
    42
                       sq(t) = sq(s)           &
wenzelm@17244
    43
                       ssent(t) = addm (ssent s) (sbit s) &
wenzelm@17244
    44
                       srcvd(t) = srcvd(s) &
wenzelm@17244
    45
                       sbit(t) = sbit(s)   &
wenzelm@17244
    46
                       ssending(s)         &
wenzelm@17244
    47
                       ssending(t) |
wenzelm@17244
    48
    R_pkt(pkt) => False |
wenzelm@17244
    49
    S_ack(b)   => False |
wenzelm@17244
    50
      R_ack(b) => sq(t)=sq(s)                  &
wenzelm@17244
    51
                     ssent(t)=ssent(s)            &
wenzelm@17244
    52
                     srcvd(t) = addm (srcvd s) b  &
wenzelm@17244
    53
                     sbit(t)=sbit(s)              &
wenzelm@17244
    54
                     ssending(t)=ssending(s) |
wenzelm@17244
    55
      C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) &
wenzelm@17244
    56
               sq(t)=sq(s)       &
wenzelm@17244
    57
               ssent(t)=ssent(s) &
wenzelm@17244
    58
               srcvd(t)=srcvd(s) &
wenzelm@17244
    59
               sbit(t)=sbit(s)   &
wenzelm@17244
    60
               ssending(s)       &
wenzelm@17244
    61
               ~ssending(t) |
wenzelm@17244
    62
      C_m_r => False |
wenzelm@17244
    63
      C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) &
wenzelm@17244
    64
               sq(t)=tl(sq(s))      &
wenzelm@17244
    65
               ssent(t)=ssent(s)    &
wenzelm@17244
    66
               srcvd(t)=srcvd(s)    &
wenzelm@17244
    67
               sbit(t) = (~sbit(s)) &
wenzelm@17244
    68
               ~ssending(s)         &
wenzelm@17244
    69
               ssending(t) |
mueller@3073
    70
      C_r_r(m) => False}"
mueller@3073
    71
wenzelm@27361
    72
definition
wenzelm@27361
    73
  sender_ioa :: "('m action, 'm sender_state)ioa" where
wenzelm@27361
    74
  "sender_ioa =
wenzelm@27361
    75
   (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"
mueller@3073
    76
wenzelm@19739
    77
lemma in_sender_asig: 
wenzelm@19739
    78
  "S_msg(m) : actions(sender_asig)"
wenzelm@19739
    79
  "R_msg(m) ~: actions(sender_asig)"
wenzelm@19739
    80
  "S_pkt(pkt) : actions(sender_asig)"
wenzelm@19739
    81
  "R_pkt(pkt) ~: actions(sender_asig)"
wenzelm@19739
    82
  "S_ack(b) ~: actions(sender_asig)"
wenzelm@19739
    83
  "R_ack(b) : actions(sender_asig)"
wenzelm@19739
    84
  "C_m_s : actions(sender_asig)"
wenzelm@19739
    85
  "C_m_r ~: actions(sender_asig)"
wenzelm@19739
    86
  "C_r_s : actions(sender_asig)"
wenzelm@19739
    87
  "C_r_r(m) ~: actions(sender_asig)"
wenzelm@19739
    88
  by (simp_all add: sender_asig_def actions_def asig_projections)
wenzelm@19739
    89
wenzelm@19739
    90
lemmas sender_projections = sq_def ssent_def srcvd_def sbit_def ssending_def
wenzelm@17244
    91
mueller@3073
    92
end