--- a/src/HOLCF/IOA/ABP/Env.thy Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/ABP/Env.thy Sat Sep 03 16:50:22 2005 +0200
@@ -1,46 +1,43 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
ID: $Id$
Author: Olaf Müller
-
-The environment.
*)
-Env = IOA + Action +
+header {* The environment *}
+
+theory Env
+imports IOA Action
+begin
types
+ 'm env_state = bool -- {* give next bit to system *}
-'m env_state = "bool"
-(* give next bit to system *)
+constdefs
+env_asig :: "'m action signature"
+"env_asig == ({Next},
+ UN m. {S_msg(m)},
+ {})"
+
+env_trans :: "('m action, 'm env_state)transition set"
+"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}"
+
+env_ioa :: "('m action, 'm env_state)ioa"
+"env_ioa == (env_asig, {True}, env_trans,{},{})"
consts
-
-env_asig :: "'m action signature"
-env_trans :: ('m action, 'm env_state)transition set
-env_ioa :: ('m action, 'm env_state)ioa
-next :: 'm env_state => bool
-
-defs
-
-env_asig_def
- "env_asig == ({Next},
- UN m. {S_msg(m)},
- {})"
+ "next" :: "'m env_state => bool"
-env_trans_def "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}"
-
-env_ioa_def "env_ioa ==
- (env_asig, {True}, env_trans,{},{})"
+ML {* use_legacy_bindings (the_context ()) *}
end
-