--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Sep 02 15:54:47 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Sep 02 17:23:59 2005 +0200
@@ -1,18 +1,19 @@
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy
ID: $Id$
Author: Olaf Müller
+*)
-Live I/O automata -- specified by temproal formulas.
-*)
-
-LiveIOA = TLS +
+header {* Live I/O automata -- specified by temproal formulas *}
-default type
+theory LiveIOA
+imports TLS
+begin
+
+defaultsort type
types
+ ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
- ('a,'s)live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
-
consts
validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool"
@@ -25,36 +26,37 @@
live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
-
+
defs
-validLIOA_def
+validLIOA_def:
"validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
-WF_def
+WF_def:
"WF A acts == <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
-SF_def
+SF_def:
"SF A acts == [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
-
+
-liveexecutions_def
+liveexecutions_def:
"liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
-livetraces_def
+livetraces_def:
"livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
-live_implements_def
- "live_implements CL AM == (inp (fst CL) = inp (fst AM)) &
+live_implements_def:
+ "live_implements CL AM == (inp (fst CL) = inp (fst AM)) &
(out (fst CL) = out (fst AM)) &
livetraces CL <= livetraces AM"
-is_live_ref_map_def
- "is_live_ref_map f CL AM ==
- is_ref_map f (fst CL ) (fst AM) &
- (! exec : executions (fst CL). (exec |== (snd CL)) -->
+is_live_ref_map_def:
+ "is_live_ref_map f CL AM ==
+ is_ref_map f (fst CL ) (fst AM) &
+ (! exec : executions (fst CL). (exec |== (snd CL)) -->
((corresp_ex (fst AM) f exec) |== (snd AM)))"
+ML {* use_legacy_bindings (the_context ()) *}
-end
\ No newline at end of file
+end