src/HOLCF/IOA/NTP/Spec.thy

converted to Isar theory format;

(*  Title:      HOL/IOA/NTP/Spec.thy
    ID:         $Id$
    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