--- a/IOA/meta_theory/IOA.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/meta_theory/IOA.thy Wed Jun 21 15:12:40 1995 +0200
@@ -60,9 +60,9 @@
defs
state_trans_def
- "state_trans(asig,R) == \
- \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
- \ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
+ "state_trans(asig,R) ==
+ (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
+ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
asig_of_def "asig_of == fst"
@@ -70,9 +70,9 @@
trans_of_def "trans_of == (snd o snd)"
ioa_def
- "IOA(ioa) == (is_asig(asig_of(ioa)) & \
- \ (~ starts_of(ioa) = {}) & \
- \ state_trans(asig_of(ioa),trans_of(ioa)))"
+ "IOA(ioa) == (is_asig(asig_of(ioa)) &
+ (~ starts_of(ioa) = {}) &
+ state_trans(asig_of(ioa),trans_of(ioa)))"
(* An execution fragment is modelled with a pair of sequences:
@@ -80,15 +80,15 @@
* Finite executions have None actions from some point on.
*******)
is_execution_fragment_def
- "is_execution_fragment(A,ex) == \
- \ let act = fst(ex); state = snd(ex) \
- \ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & \
- \ (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
+ "is_execution_fragment(A,ex) ==
+ let act = fst(ex); state = snd(ex)
+ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
+ (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
executions_def
- "executions(ioa) == {e. snd(e,0):starts_of(ioa) & \
-\ is_execution_fragment(ioa,e)}"
+ "executions(ioa) == {e. snd(e,0):starts_of(ioa) &
+ is_execution_fragment(ioa,e)}"
(* Is a state reachable. Using an inductive definition, this could be defined
@@ -113,10 +113,10 @@
(* Restrict the trace to those members of the set s *)
filter_oseq_def
- "filter_oseq(p,s) == \
-\ (%i.case s(i) \
-\ of None => None \
-\ | Some(x) => if(p(x),Some(x),None))"
+ "filter_oseq(p,s) ==
+ (%i.case s(i)
+ of None => None
+ | Some(x) => if(p(x),Some(x),None))"
mk_behaviour_def
@@ -125,8 +125,8 @@
(* Does an ioa have an execution with the given behaviour *)
has_behaviour_def
- "has_behaviour(ioa,b) == \
-\ (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
+ "has_behaviour(ioa,b) ==
+ (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
(* All the behaviours of an ioa *)
@@ -135,10 +135,10 @@
compat_asigs_def
- "compat_asigs (a1,a2) == \
- \ (((outputs(a1) Int outputs(a2)) = {}) & \
- \ ((internals(a1) Int actions(a2)) = {}) & \
- \ ((internals(a2) Int actions(a1)) = {}))"
+ "compat_asigs (a1,a2) ==
+ (((outputs(a1) Int outputs(a2)) = {}) &
+ ((internals(a1) Int actions(a2)) = {}) &
+ ((internals(a2) Int actions(a1)) = {}))"
compat_ioas_def
@@ -146,41 +146,41 @@
asig_comp_def
- "asig_comp (a1,a2) == \
- \ (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \
- \ (outputs(a1) Un outputs(a2)), \
- \ (internals(a1) Un internals(a2))>)"
+ "asig_comp (a1,a2) ==
+ (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
+ (outputs(a1) Un outputs(a2)),
+ (internals(a1) Un internals(a2))>)"
par_def
- "(ioa1 || ioa2) == \
- \ <asig_comp(asig_of(ioa1),asig_of(ioa2)), \
- \ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, \
- \ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
- \ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
- \ if(a:actions(asig_of(ioa1)), \
- \ <fst(s),a,fst(t)>:trans_of(ioa1), \
- \ fst(t) = fst(s)) \
- \ & \
- \ if(a:actions(asig_of(ioa2)), \
- \ <snd(s),a,snd(t)>:trans_of(ioa2), \
- \ snd(t) = snd(s))}>"
+ "(ioa1 || ioa2) ==
+ <asig_comp(asig_of(ioa1),asig_of(ioa2)),
+ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
+ if(a:actions(asig_of(ioa1)),
+ <fst(s),a,fst(t)>:trans_of(ioa1),
+ fst(t) = fst(s))
+ &
+ if(a:actions(asig_of(ioa2)),
+ <snd(s),a,snd(t)>:trans_of(ioa2),
+ snd(t) = snd(s))}>"
restrict_asig_def
- "restrict_asig(asig,actns) == \
-\ <inputs(asig) Int actns, outputs(asig) Int actns, \
-\ internals(asig) Un (externals(asig) - actns)>"
+ "restrict_asig(asig,actns) ==
+ <inputs(asig) Int actns, outputs(asig) Int actns,
+ internals(asig) Un (externals(asig) - actns)>"
restrict_def
- "restrict(ioa,actns) == \
-\ <restrict_asig(asig_of(ioa),actns), starts_of(ioa), trans_of(ioa)>"
+ "restrict(ioa,actns) ==
+ <restrict_asig(asig_of(ioa),actns), starts_of(ioa), trans_of(ioa)>"
ioa_implements_def
- "ioa_implements(ioa1,ioa2) == \
-\ (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \
-\ behaviours(ioa1) <= behaviours(ioa2))"
+ "ioa_implements(ioa1,ioa2) ==
+ (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) &
+ behaviours(ioa1) <= behaviours(ioa2))"
end