src/HOLCF/IOA/ABP/Abschannel_finite.thy

Old ABP files now running under the IOA meta theory based on HOLCF;

(*  Title:      HOLCF/IOA/ABP/Abschannels.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1995  TU Muenchen

The transmission channel -- finite version
*)

Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
 
consts
 
ch_fin_asig  :: 'a abs_action signature

ch_fin_trans :: ('a abs_action, 'a list)transition set

ch_fin_ioa   :: ('a abs_action, 'a list)ioa

srch_fin_asig, 
rsch_fin_asig  :: 'm action signature

srch_fin_trans :: ('m action, 'm packet list)transition set
rsch_fin_trans :: ('m action, bool list)transition set

srch_fin_ioa   :: ('m action, 'm packet list)ioa
rsch_fin_ioa   :: ('m action, bool list)ioa   

reverse        :: 'a list => 'a list

primrec
  reverse List.list  
  reverse_Nil  "reverse([]) = []"
  reverse_Cons "reverse(x#xs) =  reverse(xs)@[x]"

defs

srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)"
rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)"

srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)"  
rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)"

srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa  srch_actions"
rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa  rsch_actions"


ch_fin_asig_def "ch_fin_asig == ch_asig"

ch_fin_trans_def "ch_fin_trans ==                                       
 {tr. let s = fst(tr);                                         
          t = snd(snd(tr))                                     
      in                                                       
      case fst(snd(tr))                                        
        of S(b) => ((t = s) |                                    
                   (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
           R(b) => s ~= [] &                                   
                    b = hd(s) &                                 
                    ((t = s) | (t = tl(s)))    }"
  
ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"

end