--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,61 @@
+(* Title: HOLCF/IOA/ABP/Abschannels.thy
+ Author: Olaf Müller
+*)
+
+header {* The transmission channel -- finite version *}
+
+theory Abschannel_finite
+imports Abschannel IOA Action Lemmas
+begin
+
+primrec reverse :: "'a list => 'a list"
+where
+ reverse_Nil: "reverse([]) = []"
+| reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]"
+
+definition
+ ch_fin_asig :: "'a abs_action signature" where
+ "ch_fin_asig = ch_asig"
+
+definition
+ ch_fin_trans :: "('a abs_action, 'a list)transition set" where
+ "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)))}"
+
+definition
+ ch_fin_ioa :: "('a abs_action, 'a list)ioa" where
+ "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})"
+
+definition
+ srch_fin_ioa :: "('m action, 'm packet list)ioa" where
+ "srch_fin_ioa = rename ch_fin_ioa srch_actions"
+
+definition
+ rsch_fin_ioa :: "('m action, bool list)ioa" where
+ "rsch_fin_ioa = rename ch_fin_ioa rsch_actions"
+
+definition
+ srch_fin_asig :: "'m action signature" where
+ "srch_fin_asig = asig_of(srch_fin_ioa)"
+
+definition
+ rsch_fin_asig :: "'m action signature" where
+ "rsch_fin_asig = asig_of(rsch_fin_ioa)"
+
+definition
+ srch_fin_trans :: "('m action, 'm packet list)transition set" where
+ "srch_fin_trans = trans_of(srch_fin_ioa)"
+
+definition
+ rsch_fin_trans :: "('m action, bool list)transition set" where
+ "rsch_fin_trans = trans_of(rsch_fin_ioa)"
+
+end