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_finite.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 -- finite version\<close> |
17244 | 6 |
|
7 |
theory Abschannel_finite |
|
62009 | 8 |
imports Abschannel "../IOA" Action Lemmas |
17244 | 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 |