author | wenzelm |
Thu, 31 Dec 2015 12:55:39 +0100 | |
changeset 62009 | ecb5212d5885 |
parent 62008 | cbedaddc9351 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/ABP/Abschannel.thy |
40945 | 2 |
Author: Olaf Müller |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
*) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
62002 | 5 |
section \<open>The transmission channel\<close> |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
|
17244 | 7 |
theory Abschannel |
62009 | 8 |
imports "../IOA" Action Lemmas |
17244 | 9 |
begin |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
|
58310 | 11 |
datatype 'a abs_action = S 'a | R 'a |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
(********************************************************** |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
G e n e r i c C h a n n e l |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
*********************************************************) |
17244 | 17 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
18 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
19 |
ch_asig :: "'a abs_action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
20 |
"ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
22 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
23 |
ch_trans :: "('a abs_action, 'a list)transition set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
24 |
"ch_trans = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
25 |
{tr. let s = fst(tr); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
26 |
t = snd(snd(tr)) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
27 |
in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
28 |
case fst(snd(tr)) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
29 |
of S(b) => ((t = s) | (t = s @ [b])) | |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
30 |
R(b) => s ~= [] & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
31 |
b = hd(s) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
32 |
((t = s) | (t = tl(s)))}" |
17244 | 33 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
34 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
35 |
ch_ioa :: "('a abs_action, 'a list)ioa" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
36 |
"ch_ioa = (ch_asig, {[]}, ch_trans,{},{})" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
37 |
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
(********************************************************** |
17244 | 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 |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
*********************************************************) |
17244 | 42 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
43 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
44 |
rsch_actions :: "'m action => bool abs_action option" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
45 |
"rsch_actions (akt) = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
46 |
(case akt of |
17244 | 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)) | |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
53 |
R_ack(b) => Some(R(b)))" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
54 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
55 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
56 |
srch_actions :: "'m action =>(bool * 'm) abs_action option" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
57 |
"srch_actions akt = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
58 |
(case akt of |
17244 | 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 | |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
65 |
R_ack(b) => None)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
66 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
67 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
68 |
srch_ioa :: "('m action, 'm packet list)ioa" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
69 |
"srch_ioa = rename ch_ioa srch_actions" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
70 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
71 |
rsch_ioa :: "('m action, bool list)ioa" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
72 |
"rsch_ioa = rename ch_ioa rsch_actions" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
73 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
74 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
75 |
srch_asig :: "'m action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
76 |
"srch_asig = asig_of(srch_ioa)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
77 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
78 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
79 |
rsch_asig :: "'m action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
80 |
"rsch_asig = asig_of(rsch_ioa)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
81 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
82 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
83 |
srch_trans :: "('m action, 'm packet list)transition set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
84 |
"srch_trans = trans_of(srch_ioa)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
85 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
86 |
rsch_trans :: "('m action, bool list)transition set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
87 |
"rsch_trans = trans_of(rsch_ioa)" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
88 |
|
17244 | 89 |
end |