src/HOL/HOLCF/IOA/ABP/Abschannel.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/ABP/Abschannel.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOLCF/IOA/ABP/Abschannel.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* The transmission channel *}
     6 
     7 theory Abschannel
     8 imports IOA Action Lemmas
     9 begin
    10 
    11 datatype 'a abs_action = S 'a | R 'a
    12 
    13 
    14 (**********************************************************
    15        G e n e r i c   C h a n n e l
    16  *********************************************************)
    17 
    18 definition
    19   ch_asig :: "'a abs_action signature" where
    20   "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
    21 
    22 definition
    23   ch_trans :: "('a abs_action, 'a list)transition set" where
    24   "ch_trans =
    25    {tr. let s = fst(tr);
    26             t = snd(snd(tr))
    27         in
    28         case fst(snd(tr))
    29           of S(b) => ((t = s) | (t = s @ [b]))  |
    30              R(b) => s ~= [] &
    31                       b = hd(s) &
    32                       ((t = s) | (t = tl(s)))}"
    33 
    34 definition
    35   ch_ioa :: "('a abs_action, 'a list)ioa" where
    36   "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})"
    37 
    38 
    39 (**********************************************************
    40   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
    41  *********************************************************)
    42 
    43 definition
    44   rsch_actions :: "'m action => bool abs_action option" where
    45   "rsch_actions (akt) =
    46           (case akt of
    47            Next    =>  None |
    48            S_msg(m) => None |
    49             R_msg(m) => None |
    50            S_pkt(packet) => None |
    51             R_pkt(packet) => None |
    52             S_ack(b) => Some(S(b)) |
    53             R_ack(b) => Some(R(b)))"
    54 
    55 definition
    56   srch_actions :: "'m action =>(bool * 'm) abs_action option" where
    57   "srch_actions akt =
    58           (case akt of
    59             Next    =>  None |
    60            S_msg(m) => None |
    61             R_msg(m) => None |
    62            S_pkt(p) => Some(S(p)) |
    63             R_pkt(p) => Some(R(p)) |
    64             S_ack(b) => None |
    65             R_ack(b) => None)"
    66 
    67 definition
    68   srch_ioa :: "('m action, 'm packet list)ioa" where
    69   "srch_ioa = rename ch_ioa srch_actions"
    70 definition
    71   rsch_ioa :: "('m action, bool list)ioa" where
    72   "rsch_ioa = rename ch_ioa rsch_actions"
    73 
    74 definition
    75   srch_asig :: "'m action signature" where
    76   "srch_asig = asig_of(srch_ioa)"
    77 
    78 definition
    79   rsch_asig :: "'m action signature" where
    80   "rsch_asig = asig_of(rsch_ioa)"
    81 
    82 definition
    83   srch_trans :: "('m action, 'm packet list)transition set" where
    84   "srch_trans = trans_of(srch_ioa)"
    85 definition
    86   rsch_trans :: "('m action, bool list)transition set" where
    87   "rsch_trans = trans_of(rsch_ioa)"
    88 
    89 end