author | huffman |
Sat, 08 Jan 2011 09:30:52 -0800 | |
changeset 41476 | 0fa9629aa399 |
parent 40945 | b8703f63bfb2 |
child 42151 | 4da4fc77664b |
permissions | -rw-r--r-- |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOLCF/IOA/ABP/Abschannels.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 |
|
17244 | 5 |
header {* The transmission channel -- finite version *} |
6 |
||
7 |
theory Abschannel_finite |
|
8 |
imports Abschannel IOA Action Lemmas |
|
9 |
begin |
|
10 |
||
27361 | 11 |
primrec reverse :: "'a list => 'a list" |
12 |
where |
|
17244 | 13 |
reverse_Nil: "reverse([]) = []" |
27361 | 14 |
| reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
16 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
17 |
ch_fin_asig :: "'a abs_action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
18 |
"ch_fin_asig = ch_asig" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
20 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
21 |
ch_fin_trans :: "('a abs_action, 'a list)transition set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
22 |
"ch_fin_trans = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
23 |
{tr. let s = fst(tr); |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
24 |
t = snd(snd(tr)) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
25 |
in |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
26 |
case fst(snd(tr)) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
27 |
of S(b) => ((t = s) | |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
28 |
(if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
29 |
R(b) => s ~= [] & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
30 |
b = hd(s) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
31 |
((t = s) | (t = tl(s)))}" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
33 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
34 |
ch_fin_ioa :: "('a abs_action, 'a list)ioa" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
35 |
"ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
37 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
38 |
srch_fin_ioa :: "('m action, 'm packet list)ioa" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
39 |
"srch_fin_ioa = rename ch_fin_ioa srch_actions" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
40 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
41 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
42 |
rsch_fin_ioa :: "('m action, bool list)ioa" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
43 |
"rsch_fin_ioa = rename ch_fin_ioa rsch_actions" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
44 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
45 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
46 |
srch_fin_asig :: "'m action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
47 |
"srch_fin_asig = asig_of(srch_fin_ioa)" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
48 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
49 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
50 |
rsch_fin_asig :: "'m action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
51 |
"rsch_fin_asig = asig_of(rsch_fin_ioa)" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
52 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
53 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
54 |
srch_fin_trans :: "('m action, 'm packet list)transition set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
55 |
"srch_fin_trans = trans_of(srch_fin_ioa)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
56 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
57 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
58 |
rsch_fin_trans :: "('m action, bool list)transition set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19738
diff
changeset
|
59 |
"rsch_fin_trans = trans_of(rsch_fin_ioa)" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
60 |
|
17244 | 61 |
end |