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