1(*  Title:      HOL/HOLCF/IOA/ABP/Abschannel.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The transmission channel\<close>
6
7theory Abschannel
8imports IOA.IOA Action Lemmas
9begin
10
11datatype '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
18definition
19  ch_asig :: "'a abs_action signature" where
20  "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
21
22definition
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
34definition
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
43definition
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
55definition
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
67definition
68  srch_ioa :: "('m action, 'm packet list)ioa" where
69  "srch_ioa = rename ch_ioa srch_actions"
70definition
71  rsch_ioa :: "('m action, bool list)ioa" where
72  "rsch_ioa = rename ch_ioa rsch_actions"
73
74definition
75  srch_asig :: "'m action signature" where
76  "srch_asig = asig_of(srch_ioa)"
77
78definition
79  rsch_asig :: "'m action signature" where
80  "rsch_asig = asig_of(rsch_ioa)"
81
82definition
83  srch_trans :: "('m action, 'm packet list)transition set" where
84  "srch_trans = trans_of(srch_ioa)"
85definition
86  rsch_trans :: "('m action, bool list)transition set" where
87  "rsch_trans = trans_of(rsch_ioa)"
88
89end
90