--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,42 @@
+(* Title: HOLCF/IOA/ABP/Impl.thy
+ Author: Olaf Müller
+*)
+
+header {* The environment *}
+
+theory Env
+imports IOA Action
+begin
+
+types
+ 'm env_state = bool -- {* give next bit to system *}
+
+definition
+ env_asig :: "'m action signature" where
+ "env_asig == ({Next},
+ UN m. {S_msg(m)},
+ {})"
+
+definition
+ env_trans :: "('m action, 'm env_state)transition set" where
+ "env_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => t=True |
+ S_msg(m) => s=True & t=False |
+ R_msg(m) => False |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False}"
+
+definition
+ env_ioa :: "('m action, 'm env_state)ioa" where
+ "env_ioa = (env_asig, {True}, env_trans,{},{})"
+
+axiomatization
+ "next" :: "'m env_state => bool"
+
+end