src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/ABP/Abschannel_finite.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/Abschannels.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* The transmission channel -- finite version *}
     6 
     7 theory Abschannel_finite
     8 imports Abschannel IOA Action Lemmas
     9 begin
    10 
    11 primrec reverse :: "'a list => 'a list"
    12 where
    13   reverse_Nil:  "reverse([]) = []"
    14 | reverse_Cons: "reverse(x#xs) =  reverse(xs)@[x]"
    15 
    16 definition
    17   ch_fin_asig :: "'a abs_action signature" where
    18   "ch_fin_asig = ch_asig"
    19 
    20 definition
    21   ch_fin_trans :: "('a abs_action, 'a list)transition set" where
    22   "ch_fin_trans =
    23    {tr. let s = fst(tr);
    24             t = snd(snd(tr))
    25         in
    26         case fst(snd(tr))
    27           of S(b) => ((t = s) |
    28                      (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |
    29              R(b) => s ~= [] &
    30                       b = hd(s) &
    31                       ((t = s) | (t = tl(s)))}"
    32 
    33 definition
    34   ch_fin_ioa :: "('a abs_action, 'a list)ioa" where
    35   "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})"
    36 
    37 definition
    38   srch_fin_ioa :: "('m action, 'm packet list)ioa" where
    39   "srch_fin_ioa = rename ch_fin_ioa  srch_actions"
    40 
    41 definition
    42   rsch_fin_ioa :: "('m action, bool list)ioa" where
    43   "rsch_fin_ioa = rename ch_fin_ioa  rsch_actions"
    44 
    45 definition
    46   srch_fin_asig :: "'m action signature" where
    47   "srch_fin_asig = asig_of(srch_fin_ioa)"
    48 
    49 definition
    50   rsch_fin_asig :: "'m action signature" where
    51   "rsch_fin_asig = asig_of(rsch_fin_ioa)"
    52 
    53 definition
    54   srch_fin_trans :: "('m action, 'm packet list)transition set" where
    55   "srch_fin_trans = trans_of(srch_fin_ioa)"
    56 
    57 definition
    58   rsch_fin_trans :: "('m action, bool list)transition set" where
    59   "rsch_fin_trans = trans_of(rsch_fin_ioa)"
    60 
    61 end