src/HOL/IOA/ABP/Abschannel.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 
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Abschannel = IOA + Action + Lemmas + List +
mueller@1138
    10
mueller@1138
    11
nipkow@1050
    12
datatype ('a)act =   S('a) | R('a)
nipkow@1050
    13
mueller@1138
    14
nipkow@1050
    15
consts
nipkow@1050
    16
 
clasohm@1376
    17
ch_asig  :: 'a act signature
clasohm@1376
    18
ch_trans :: ('a act, 'a list)transition set
clasohm@1376
    19
ch_ioa   :: ('a act, 'a list)ioa
nipkow@1050
    20
clasohm@1376
    21
rsch_actions  :: 'm action => bool act option
nipkow@1050
    22
srch_actions  :: "'m action =>(bool * 'm) act option"
nipkow@1050
    23
nipkow@1050
    24
srch_asig, 
clasohm@1376
    25
rsch_asig  :: 'm action signature
nipkow@1050
    26
clasohm@1376
    27
srch_trans :: ('m action, 'm packet list)transition set
clasohm@1376
    28
rsch_trans :: ('m action, bool list)transition set
nipkow@1050
    29
clasohm@1376
    30
srch_ioa   :: ('m action, 'm packet list)ioa
clasohm@1376
    31
rsch_ioa   :: ('m action, bool list)ioa   
nipkow@1050
    32
nipkow@1050
    33
nipkow@1050
    34
defs
nipkow@1050
    35
nipkow@1050
    36
srch_asig_def "srch_asig == asig_of(srch_ioa)"
nipkow@1050
    37
rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
nipkow@1050
    38
nipkow@1050
    39
srch_trans_def "srch_trans == trans_of(srch_ioa)"  
nipkow@1050
    40
rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
nipkow@1050
    41
nipkow@1050
    42
srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
nipkow@1050
    43
rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
nipkow@1050
    44
mueller@1138
    45
  
mueller@1138
    46
(**********************************************************
mueller@1138
    47
       G e n e r i c   C h a n n e l
mueller@1138
    48
 *********************************************************)
mueller@1138
    49
  
nipkow@1050
    50
ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
nipkow@1050
    51
clasohm@1151
    52
ch_trans_def "ch_trans ==                                       
clasohm@1151
    53
 {tr. let s = fst(tr);                                         
clasohm@1151
    54
          t = snd(snd(tr))                                     
clasohm@1151
    55
      in                                                       
clasohm@1151
    56
      case fst(snd(tr))                                        
clasohm@1151
    57
        of S(b) => ((t = s) | (t = s @ [b]))  |                
clasohm@1151
    58
           R(b) => s ~= [] &                                   
clasohm@1476
    59
                    b = hd(s) &                                 
clasohm@1476
    60
                    ((t = s) | (t = tl(s)))    }"
nipkow@1050
    61
  
nipkow@1050
    62
ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
nipkow@1050
    63
mueller@1138
    64
(**********************************************************
mueller@1138
    65
  C o n c r e t e  C h a n n e l s  b y   R e n a m i n g 
mueller@1138
    66
 *********************************************************)
mueller@1138
    67
  
clasohm@1151
    68
rsch_actions_def "rsch_actions (akt) ==                      
clasohm@1476
    69
            case akt of   
clasohm@1151
    70
           Next    =>  None |          
clasohm@1151
    71
           S_msg(m) => None |         
clasohm@1476
    72
            R_msg(m) => None |         
clasohm@1151
    73
           S_pkt(packet) => None |    
clasohm@1476
    74
            R_pkt(packet) => None |    
clasohm@1476
    75
            S_ack(b) => Some(S(b)) |   
clasohm@1476
    76
            R_ack(b) => Some(R(b))"
nipkow@1050
    77
clasohm@1151
    78
srch_actions_def "srch_actions (akt) ==                      
clasohm@1476
    79
            case akt of   
clasohm@1476
    80
            Next    =>  None |          
clasohm@1151
    81
           S_msg(m) => None |         
clasohm@1476
    82
            R_msg(m) => None |         
clasohm@1151
    83
           S_pkt(p) => Some(S(p)) |   
clasohm@1476
    84
            R_pkt(p) => Some(R(p)) |   
clasohm@1476
    85
            S_ack(b) => None |         
clasohm@1476
    86
            R_ack(b) => None"
nipkow@1050
    87
nipkow@1050
    88
nipkow@1050
    89
end  
nipkow@1050
    90
nipkow@1050
    91
nipkow@1050
    92
nipkow@1050
    93
nipkow@1050
    94
nipkow@1050
    95
nipkow@1050
    96
nipkow@1050
    97
nipkow@1050
    98
nipkow@1050
    99
nipkow@1050
   100
nipkow@1050
   101
nipkow@1050
   102
nipkow@1050
   103
nipkow@1050
   104
nipkow@1050
   105
nipkow@1050
   106
nipkow@1050
   107