equal
deleted
inserted
replaced
1 (* The I/O automata of Lynch and Tuttle. *) |
1 (* Title: HOL/IOA/meta_theory/IOA.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The I/O automata of Lynch and Tuttle. |
|
7 *) |
2 |
8 |
3 IOA = Asig + |
9 IOA = Asig + |
4 |
10 |
5 types |
11 types |
6 'a seq = "nat => 'a" |
12 'a seq = "nat => 'a" |
49 |
55 |
50 (* Notions of correctness *) |
56 (* Notions of correctness *) |
51 ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" |
57 ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" |
52 |
58 |
53 |
59 |
54 rules |
60 defs |
55 |
61 |
56 state_trans_def |
62 state_trans_def |
57 "state_trans(asig,R) == \ |
63 "state_trans(asig,R) == \ |
58 \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \ |
64 \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \ |
59 \ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))" |
65 \ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))" |
60 |
66 |
61 |
67 |
62 ioa_projections_def |
68 asig_of_def "asig_of == fst" |
63 "asig_of = fst & starts_of = (fst o snd) & trans_of = (snd o snd)" |
69 starts_of_def "starts_of == (fst o snd)" |
64 |
70 trans_of_def "trans_of == (snd o snd)" |
65 |
71 |
66 ioa_def |
72 ioa_def |
67 "IOA(ioa) == (is_asig(asig_of(ioa)) & \ |
73 "IOA(ioa) == (is_asig(asig_of(ioa)) & \ |
68 \ (~ starts_of(ioa) = {}) & \ |
74 \ (~ starts_of(ioa) = {}) & \ |
69 \ state_trans(asig_of(ioa),trans_of(ioa)))" |
75 \ state_trans(asig_of(ioa),trans_of(ioa)))" |