src/HOL/IOA/ABP/Abschannel_finite.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1476 608483c2122a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/IOA/example/Abschannels.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1994  TU Muenchen
     5 
     6 The transmission channel -- finite version
     7 *)
     8 
     9 Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
    10  
    11 consts
    12  
    13 ch_fin_asig  :: 'a act signature
    14 
    15 ch_fin_trans :: ('a act, 'a list)transition set
    16 
    17 ch_fin_ioa   :: ('a act, 'a list)ioa
    18 
    19 srch_fin_asig, 
    20 rsch_fin_asig  :: 'm action signature
    21 
    22 srch_fin_trans :: ('m action, 'm packet list)transition set
    23 rsch_fin_trans :: ('m action, bool list)transition set
    24 
    25 srch_fin_ioa   :: ('m action, 'm packet list)ioa
    26 rsch_fin_ioa   :: ('m action, bool list)ioa   
    27 
    28 reverse        :: 'a list => 'a list
    29 
    30 primrec
    31   reverse List.list  
    32   reverse_Nil  "reverse([]) = []"
    33   reverse_Cons "reverse(x#xs) =  reverse(xs)@[x]"
    34 
    35 defs
    36 
    37 srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)"
    38 rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)"
    39 
    40 srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)"  
    41 rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)"
    42 
    43 srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa  srch_actions"
    44 rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa  rsch_actions"
    45 
    46 
    47 ch_fin_asig_def "ch_fin_asig == ch_asig"
    48 
    49 ch_fin_trans_def "ch_fin_trans ==                                       
    50  {tr. let s = fst(tr);                                         
    51           t = snd(snd(tr))                                     
    52       in                                                       
    53       case fst(snd(tr))                                        
    54         of S(b) => ((t = s) |                                    
    55                    (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
    56            R(b) => s ~= [] &                                   
    57                     b = hd(s) &                                 
    58                     ((t = s) | (t = tl(s)))    }"
    59   
    60 ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
    61 
    62 end  
    63 
    64 
    65 
    66 
    67 
    68 
    69 
    70 
    71 
    72 
    73 
    74 
    75 
    76 
    77 
    78 
    79 
    80