diff -r 722bf1319be5 -r fd1be45b64bf IOA/meta_theory/IOA.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/IOA.thy	Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,180 @@
+(* The I/O automata of Lynch and Tuttle. *)
+
+IOA = Asig +
+
+types
+   'a seq            =   "nat => 'a"
+   'a oseq           =   "nat => 'a option"
+   ('a,'b)execution  =   "'a oseq * 'b seq"
+   ('a,'s)transition =   "('s * 'a * 's)"
+   ('a,'s)ioa        =   "'a signature * 's set * ('a,'s)transition set"
+
+consts
+
+  (* IO automata *)
+  state_trans::"['action signature, ('action,'state)transition set] => bool"
+  asig_of    ::"('action,'state)ioa => 'action signature"
+  starts_of  ::"('action,'state)ioa => 'state set"
+  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
+  IOA	     ::"('action,'state)ioa => bool"
+
+  (* Executions, schedules, and behaviours *)
+
+  is_execution_fragment,
+  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
+  executions    :: "('action,'state)ioa => ('action,'state)execution set"
+  mk_behaviour  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
+  reachable     :: "[('action,'state)ioa, 'state] => bool"
+  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
+  has_behaviour :: "[('action,'state)ioa, 'action oseq] => bool"
+  behaviours    :: "('action,'state)ioa => 'action oseq set"
+
+  (* Composition of action signatures and automata *)
+  compatible_asigs ::"('a => 'action signature) => bool"
+  asig_composition ::"('a => 'action signature) => 'action signature"
+  compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
+  ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
+
+  (* binary composition of action signatures and automata *)
+  compat_asigs ::"['action signature, 'action signature] => bool"
+  asig_comp    ::"['action signature, 'action signature] => 'action signature"
+  compat_ioas  ::"[('action,'state)ioa, ('action,'state)ioa] => bool"
+  "||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr 10)
+
+  (* Filtering and hiding *)
+  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
+
+  restrict_asig :: "['a signature, 'a set] => 'a signature"
+  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+
+  (* Notions of correctness *)
+  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
+
+
+rules
+
+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))"
+
+
+ioa_projections_def
+   "asig_of = fst  &  starts_of = (fst o snd)  &  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)))"
+
+
+(* An execution fragment is modelled with a pair of sequences:
+ * the first is the action options, the second the state sequence.
+ * 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))"
+
+
+executions_def
+  "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
+ * by the following 2 rules
+ *
+ *      x:starts_of(ioa)
+ *      ----------------
+ *      reachable(ioa,x)  
+ *
+ *      reachable(ioa,s) & ? <s,a,s'>:trans_of(ioa)
+ *      -------------------------------------------
+ *               reachable(ioa,s')
+ *
+ * A direkt definition follows.
+ *******************************)
+reachable_def
+  "reachable(ioa,s) == (? ex:executions(ioa). ? n. snd(ex,n) = s)"
+
+
+invariant_def "invariant(A,P) == (!s. reachable(A,s) --> P(s))"
+
+
+(* 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))"
+
+
+mk_behaviour_def
+  "mk_behaviour(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))"
+
+
+(* 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)))"
+
+
+(* All the behaviours of an ioa *)
+behaviours_def
+  "behaviours(ioa) == {b. has_behaviour(ioa,b)}"
+
+
+compat_asigs_def
+  "compat_asigs (a1,a2) ==                                              \
+ \ (((outputs(a1) Int outputs(a2)) = {}) &                              \
+ \  ((internals(a1) Int actions(a2)) = {}) &                            \
+ \  ((internals(a2) Int actions(a1)) = {}))"
+
+
+compat_ioas_def
+  "compat_ioas(ioa1,ioa2) == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
+
+
+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))>)"
+
+
+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))}>"
+
+
+restrict_asig_def
+  "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)>"
+
+
+ioa_implements_def
+  "ioa_implements(ioa1,ioa2) ==        \
+\     (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \
+\      behaviours(ioa1) <= behaviours(ioa2))"
+
+end