src/HOL/HOLCF/IOA/NTP/Spec.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;
     1 (*  Title:      HOL/HOLCF/IOA/NTP/Spec.thy
     2     Author:     Tobias Nipkow & Konrad Slind
     3 *)
     4 
     5 section {* The specification of reliable transmission *}
     6 
     7 theory Spec
     8 imports IOA Action
     9 begin
    10 
    11 definition
    12   spec_sig :: "'m action signature" where
    13   sig_def: "spec_sig = (UN m.{S_msg(m)}, 
    14                         UN m.{R_msg(m)}, 
    15                         {})"
    16 
    17 definition
    18   spec_trans :: "('m action, 'm list)transition set" where
    19   trans_def: "spec_trans =
    20    {tr. let s = fst(tr);                            
    21             t = snd(snd(tr))                        
    22         in                                          
    23         case fst(snd(tr))                           
    24         of                                          
    25         S_msg(m) => t = s@[m]  |                    
    26         R_msg(m) => s = (m#t)  |                    
    27         S_pkt(pkt) => False |                    
    28         R_pkt(pkt) => False |                    
    29         S_ack(b) => False |                      
    30         R_ack(b) => False |                      
    31         C_m_s => False |                            
    32         C_m_r => False |                            
    33         C_r_s => False |                            
    34         C_r_r(m) => False}"
    35 
    36 definition
    37   spec_ioa :: "('m action, 'm list)ioa" where
    38   ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})"
    39 
    40 end