(* Title: HOL/IOA/example/Abschannels.thy
ID: $Id$
Author: Olaf Mueller
Copyright 1994 TU Muenchen
The transmission channel -- finite version
*)
Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
consts
ch_fin_asig :: 'a act signature
ch_fin_trans :: ('a act, 'a list)transition set
ch_fin_ioa :: ('a act, 'a list)ioa
srch_fin_asig,
rsch_fin_asig :: 'm action signature
srch_fin_trans :: ('m action, 'm packet list)transition set
rsch_fin_trans :: ('m action, bool list)transition set
srch_fin_ioa :: ('m action, 'm packet list)ioa
rsch_fin_ioa :: ('m action, bool list)ioa
reverse :: 'a list => 'a list
primrec
reverse List.list
reverse_Nil "reverse([]) = []"
reverse_Cons "reverse(x#xs) = reverse(xs)@[x]"
defs
srch_fin_asig_def "srch_fin_asig == asig_of(srch_fin_ioa)"
rsch_fin_asig_def "rsch_fin_asig == asig_of(rsch_fin_ioa)"
srch_fin_trans_def "srch_fin_trans == trans_of(srch_fin_ioa)"
rsch_fin_trans_def "rsch_fin_trans == trans_of(rsch_fin_ioa)"
srch_fin_ioa_def "srch_fin_ioa == rename ch_fin_ioa srch_actions"
rsch_fin_ioa_def "rsch_fin_ioa == rename ch_fin_ioa rsch_actions"
ch_fin_asig_def "ch_fin_asig == ch_asig"
ch_fin_trans_def "ch_fin_trans ==
{tr. let s = fst(tr);
t = snd(snd(tr))
in
case fst(snd(tr))
of S(b) => ((t = s) |
(if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) |
R(b) => s ~= [] &
b = hd(s) &
((t = s) | (t = tl(s))) }"
ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
end