src/HOL/HOLCF/IOA/ABP/Abschannel.thy
changeset 40774 0437dbc127b3
parent 35174 e15040ae75d7
child 40945 b8703f63bfb2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,89 @@
     1.4 +(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
     1.5 +    Author:     Olaf Müller
     1.6 +*)
     1.7 +
     1.8 +header {* The transmission channel *}
     1.9 +
    1.10 +theory Abschannel
    1.11 +imports IOA Action Lemmas
    1.12 +begin
    1.13 +
    1.14 +datatype 'a abs_action = S 'a | R 'a
    1.15 +
    1.16 +
    1.17 +(**********************************************************
    1.18 +       G e n e r i c   C h a n n e l
    1.19 + *********************************************************)
    1.20 +
    1.21 +definition
    1.22 +  ch_asig :: "'a abs_action signature" where
    1.23 +  "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
    1.24 +
    1.25 +definition
    1.26 +  ch_trans :: "('a abs_action, 'a list)transition set" where
    1.27 +  "ch_trans =
    1.28 +   {tr. let s = fst(tr);
    1.29 +            t = snd(snd(tr))
    1.30 +        in
    1.31 +        case fst(snd(tr))
    1.32 +          of S(b) => ((t = s) | (t = s @ [b]))  |
    1.33 +             R(b) => s ~= [] &
    1.34 +                      b = hd(s) &
    1.35 +                      ((t = s) | (t = tl(s)))}"
    1.36 +
    1.37 +definition
    1.38 +  ch_ioa :: "('a abs_action, 'a list)ioa" where
    1.39 +  "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})"
    1.40 +
    1.41 +
    1.42 +(**********************************************************
    1.43 +  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
    1.44 + *********************************************************)
    1.45 +
    1.46 +definition
    1.47 +  rsch_actions :: "'m action => bool abs_action option" where
    1.48 +  "rsch_actions (akt) =
    1.49 +          (case akt of
    1.50 +           Next    =>  None |
    1.51 +           S_msg(m) => None |
    1.52 +            R_msg(m) => None |
    1.53 +           S_pkt(packet) => None |
    1.54 +            R_pkt(packet) => None |
    1.55 +            S_ack(b) => Some(S(b)) |
    1.56 +            R_ack(b) => Some(R(b)))"
    1.57 +
    1.58 +definition
    1.59 +  srch_actions :: "'m action =>(bool * 'm) abs_action option" where
    1.60 +  "srch_actions akt =
    1.61 +          (case akt of
    1.62 +            Next    =>  None |
    1.63 +           S_msg(m) => None |
    1.64 +            R_msg(m) => None |
    1.65 +           S_pkt(p) => Some(S(p)) |
    1.66 +            R_pkt(p) => Some(R(p)) |
    1.67 +            S_ack(b) => None |
    1.68 +            R_ack(b) => None)"
    1.69 +
    1.70 +definition
    1.71 +  srch_ioa :: "('m action, 'm packet list)ioa" where
    1.72 +  "srch_ioa = rename ch_ioa srch_actions"
    1.73 +definition
    1.74 +  rsch_ioa :: "('m action, bool list)ioa" where
    1.75 +  "rsch_ioa = rename ch_ioa rsch_actions"
    1.76 +
    1.77 +definition
    1.78 +  srch_asig :: "'m action signature" where
    1.79 +  "srch_asig = asig_of(srch_ioa)"
    1.80 +
    1.81 +definition
    1.82 +  rsch_asig :: "'m action signature" where
    1.83 +  "rsch_asig = asig_of(rsch_ioa)"
    1.84 +
    1.85 +definition
    1.86 +  srch_trans :: "('m action, 'm packet list)transition set" where
    1.87 +  "srch_trans = trans_of(srch_ioa)"
    1.88 +definition
    1.89 +  rsch_trans :: "('m action, bool list)transition set" where
    1.90 +  "rsch_trans = trans_of(rsch_ioa)"
    1.91 +
    1.92 +end