8 imports Asig |
8 imports Asig |
9 begin |
9 begin |
10 |
10 |
11 default_sort type |
11 default_sort type |
12 |
12 |
13 type_synonym |
13 type_synonym ('a, 's) transition = "'s * 'a * 's" |
14 ('a, 's) transition = "'s * 'a * 's" |
14 type_synonym ('a, 's) ioa = |
15 |
15 "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)" |
16 type_synonym |
16 |
17 ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)" |
17 |
18 |
18 (* --------------------------------- IOA ---------------------------------*) |
19 consts |
19 |
20 |
20 (* IO automata *) |
21 (* IO automata *) |
21 |
22 |
22 definition asig_of :: "('a, 's)ioa \<Rightarrow> 'a signature" |
23 asig_of ::"('a,'s)ioa => 'a signature" |
23 where "asig_of = fst" |
24 starts_of ::"('a,'s)ioa => 's set" |
24 |
25 trans_of ::"('a,'s)ioa => ('a,'s)transition set" |
25 definition starts_of :: "('a, 's) ioa \<Rightarrow> 's set" |
26 wfair_of ::"('a,'s)ioa => ('a set) set" |
26 where "starts_of = (fst \<circ> snd)" |
27 sfair_of ::"('a,'s)ioa => ('a set) set" |
27 |
28 |
28 definition trans_of :: "('a, 's) ioa \<Rightarrow> ('a, 's) transition set" |
29 is_asig_of ::"('a,'s)ioa => bool" |
29 where "trans_of = (fst \<circ> snd \<circ> snd)" |
30 is_starts_of ::"('a,'s)ioa => bool" |
30 |
31 is_trans_of ::"('a,'s)ioa => bool" |
31 abbreviation trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81, 81, 81, 81] 100) |
32 input_enabled ::"('a,'s)ioa => bool" |
32 where "s \<midarrow>a\<midarrow>A\<rightarrow> t \<equiv> (s, a, t) \<in> trans_of A" |
33 IOA ::"('a,'s)ioa => bool" |
33 |
34 |
34 definition wfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set" |
35 (* constraints for fair IOA *) |
35 where "wfair_of = (fst \<circ> snd \<circ> snd \<circ> snd)" |
36 |
36 |
37 fairIOA ::"('a,'s)ioa => bool" |
37 definition sfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set" |
38 input_resistant::"('a,'s)ioa => bool" |
38 where "sfair_of = (snd \<circ> snd \<circ> snd \<circ> snd)" |
39 |
39 |
40 (* enabledness of actions and action sets *) |
40 definition is_asig_of :: "('a, 's) ioa \<Rightarrow> bool" |
41 |
41 where "is_asig_of A = is_asig (asig_of A)" |
42 enabled ::"('a,'s)ioa => 'a => 's => bool" |
42 |
43 Enabled ::"('a,'s)ioa => 'a set => 's => bool" |
43 definition is_starts_of :: "('a, 's) ioa \<Rightarrow> bool" |
44 |
44 where "is_starts_of A \<longleftrightarrow> starts_of A \<noteq> {}" |
45 (* action set keeps enabled until probably disabled by itself *) |
45 |
46 |
46 definition is_trans_of :: "('a, 's) ioa \<Rightarrow> bool" |
47 en_persistent :: "('a,'s)ioa => 'a set => bool" |
47 where "is_trans_of A \<longleftrightarrow> |
48 |
48 (\<forall>triple. triple \<in> trans_of A \<longrightarrow> fst (snd triple) \<in> actions (asig_of A))" |
49 (* post_conditions for actions and action sets *) |
49 |
50 |
50 definition input_enabled :: "('a, 's) ioa \<Rightarrow> bool" |
51 was_enabled ::"('a,'s)ioa => 'a => 's => bool" |
51 where "input_enabled A \<longleftrightarrow> |
52 set_was_enabled ::"('a,'s)ioa => 'a set => 's => bool" |
52 (\<forall>a. a \<in> inputs (asig_of A) \<longrightarrow> (\<forall>s1. \<exists>s2. (s1, a, s2) \<in> trans_of A))" |
53 |
53 |
54 (* invariants *) |
54 definition IOA :: "('a, 's) ioa \<Rightarrow> bool" |
55 invariant :: "[('a,'s)ioa, 's=>bool] => bool" |
55 where "IOA A \<longleftrightarrow> |
56 |
56 is_asig_of A \<and> |
57 (* binary composition of action signatures and automata *) |
57 is_starts_of A \<and> |
58 asig_comp ::"['a signature, 'a signature] => 'a signature" |
58 is_trans_of A \<and> |
59 compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool" |
59 input_enabled A" |
60 par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\<parallel>" 10) |
|
61 |
|
62 (* hiding and restricting *) |
|
63 hide_asig :: "['a signature, 'a set] => 'a signature" |
|
64 hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" |
|
65 restrict_asig :: "['a signature, 'a set] => 'a signature" |
|
66 restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" |
|
67 |
|
68 (* renaming *) |
|
69 rename_set :: "'a set => ('c => 'a option) => 'c set" |
|
70 rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" |
|
71 |
|
72 |
|
73 inductive |
|
74 reachable :: "('a, 's) ioa => 's => bool" |
|
75 for C :: "('a, 's) ioa" |
|
76 where |
|
77 reachable_0: "s : starts_of C ==> reachable C s" |
|
78 | reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t" |
|
79 |
|
80 abbreviation |
|
81 trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81,81,81,81] 100) where |
|
82 "s \<midarrow>a\<midarrow>A\<rightarrow> t == (s,a,t):trans_of A" |
|
83 |
60 |
84 abbreviation "act A == actions (asig_of A)" |
61 abbreviation "act A == actions (asig_of A)" |
85 abbreviation "ext A == externals (asig_of A)" |
62 abbreviation "ext A == externals (asig_of A)" |
86 abbreviation int where "int A == internals (asig_of A)" |
63 abbreviation int where "int A == internals (asig_of A)" |
87 abbreviation "inp A == inputs (asig_of A)" |
64 abbreviation "inp A == inputs (asig_of A)" |
88 abbreviation "out A == outputs (asig_of A)" |
65 abbreviation "out A == outputs (asig_of A)" |
89 abbreviation "local A == locals (asig_of A)" |
66 abbreviation "local A == locals (asig_of A)" |
90 |
67 |
91 defs |
68 (* invariants *) |
92 |
69 inductive reachable :: "('a, 's) ioa \<Rightarrow> 's \<Rightarrow> bool" |
93 (* --------------------------------- IOA ---------------------------------*) |
70 for C :: "('a, 's) ioa" |
94 |
71 where |
95 asig_of_def: "asig_of == fst" |
72 reachable_0: "s \<in> starts_of C \<Longrightarrow> reachable C s" |
96 starts_of_def: "starts_of == (fst o snd)" |
73 | reachable_n: "\<lbrakk>reachable C s; (s, a, t) \<in> trans_of C\<rbrakk> \<Longrightarrow> reachable C t" |
97 trans_of_def: "trans_of == (fst o snd o snd)" |
74 |
98 wfair_of_def: "wfair_of == (fst o snd o snd o snd)" |
75 definition invariant :: "[('a, 's) ioa, 's \<Rightarrow> bool] \<Rightarrow> bool" |
99 sfair_of_def: "sfair_of == (snd o snd o snd o snd)" |
76 where "invariant A P \<longleftrightarrow> (\<forall>s. reachable A s \<longrightarrow> P s)" |
100 |
|
101 is_asig_of_def: |
|
102 "is_asig_of A == is_asig (asig_of A)" |
|
103 |
|
104 is_starts_of_def: |
|
105 "is_starts_of A == (~ starts_of A = {})" |
|
106 |
|
107 is_trans_of_def: |
|
108 "is_trans_of A == |
|
109 (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))" |
|
110 |
|
111 input_enabled_def: |
|
112 "input_enabled A == |
|
113 (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))" |
|
114 |
|
115 |
|
116 ioa_def: |
|
117 "IOA A == (is_asig_of A & |
|
118 is_starts_of A & |
|
119 is_trans_of A & |
|
120 input_enabled A)" |
|
121 |
|
122 |
|
123 invariant_def: "invariant A P == (!s. reachable A s --> P(s))" |
|
124 |
77 |
125 |
78 |
126 (* ------------------------- parallel composition --------------------------*) |
79 (* ------------------------- parallel composition --------------------------*) |
127 |
80 |
128 |
81 (* binary composition of action signatures and automata *) |
129 compatible_def: |
82 |
130 "compatible A B == |
83 definition compatible :: "[('a, 's) ioa, ('a, 't) ioa] \<Rightarrow> bool" |
131 (((out A Int out B) = {}) & |
84 where |
132 ((int A Int act B) = {}) & |
85 "compatible A B \<longleftrightarrow> |
133 ((int B Int act A) = {}))" |
86 (((out A \<inter> out B) = {}) \<and> |
134 |
87 ((int A \<inter> act B) = {}) \<and> |
135 asig_comp_def: |
88 ((int B \<inter> act A) = {}))" |
136 "asig_comp a1 a2 == |
89 |
137 (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), |
90 definition asig_comp :: "['a signature, 'a signature] \<Rightarrow> 'a signature" |
138 (outputs(a1) Un outputs(a2)), |
91 where |
139 (internals(a1) Un internals(a2))))" |
92 "asig_comp a1 a2 = |
140 |
93 (((inputs(a1) \<union> inputs(a2)) - (outputs(a1) \<union> outputs(a2)), |
141 par_def: |
94 (outputs(a1) \<union> outputs(a2)), |
142 "(A \<parallel> B) == |
95 (internals(a1) \<union> internals(a2))))" |
|
96 |
|
97 definition par :: "[('a, 's) ioa, ('a, 't) ioa] \<Rightarrow> ('a, 's * 't) ioa" (infixr "\<parallel>" 10) |
|
98 where |
|
99 "(A \<parallel> B) = |
143 (asig_comp (asig_of A) (asig_of B), |
100 (asig_comp (asig_of A) (asig_of B), |
144 {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)}, |
101 {pr. fst(pr) \<in> starts_of(A) \<and> snd(pr) \<in> starts_of(B)}, |
145 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
102 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
146 in (a:act A | a:act B) & |
103 in (a \<in> act A | a:act B) \<and> |
147 (if a:act A then |
104 (if a \<in> act A then |
148 (fst(s),a,fst(t)):trans_of(A) |
105 (fst(s), a, fst(t)) \<in> trans_of(A) |
149 else fst(t) = fst(s)) |
106 else fst(t) = fst(s)) |
150 & |
107 & |
151 (if a:act B then |
108 (if a \<in> act B then |
152 (snd(s),a,snd(t)):trans_of(B) |
109 (snd(s), a, snd(t)) \<in> trans_of(B) |
153 else snd(t) = snd(s))}, |
110 else snd(t) = snd(s))}, |
154 wfair_of A Un wfair_of B, |
111 wfair_of A \<union> wfair_of B, |
155 sfair_of A Un sfair_of B)" |
112 sfair_of A \<union> sfair_of B)" |
156 |
113 |
157 |
114 |
158 (* ------------------------ hiding -------------------------------------------- *) |
115 (* ------------------------ hiding -------------------------------------------- *) |
159 |
116 |
160 restrict_asig_def: |
117 (* hiding and restricting *) |
161 "restrict_asig asig actns == |
118 |
|
119 definition restrict_asig :: "['a signature, 'a set] \<Rightarrow> 'a signature" |
|
120 where |
|
121 "restrict_asig asig actns = |
162 (inputs(asig) Int actns, |
122 (inputs(asig) Int actns, |
163 outputs(asig) Int actns, |
123 outputs(asig) Int actns, |
164 internals(asig) Un (externals(asig) - actns))" |
124 internals(asig) Un (externals(asig) - actns))" |
165 |
125 |
166 (* Notice that for wfair_of and sfair_of nothing has to be changed, as |
126 (* Notice that for wfair_of and sfair_of nothing has to be changed, as |
167 changes from the outputs to the internals does not touch the locals as |
127 changes from the outputs to the internals does not touch the locals as |
168 a whole, which is of importance for fairness only *) |
128 a whole, which is of importance for fairness only *) |
169 |
129 definition restrict :: "[('a, 's) ioa, 'a set] \<Rightarrow> ('a, 's) ioa" |
170 restrict_def: |
130 where |
171 "restrict A actns == |
131 "restrict A actns = |
172 (restrict_asig (asig_of A) actns, |
132 (restrict_asig (asig_of A) actns, |
173 starts_of A, |
133 starts_of A, |
174 trans_of A, |
134 trans_of A, |
175 wfair_of A, |
135 wfair_of A, |
176 sfair_of A)" |
136 sfair_of A)" |
177 |
137 |
178 hide_asig_def: |
138 definition hide_asig :: "['a signature, 'a set] \<Rightarrow> 'a signature" |
179 "hide_asig asig actns == |
139 where |
|
140 "hide_asig asig actns = |
180 (inputs(asig) - actns, |
141 (inputs(asig) - actns, |
181 outputs(asig) - actns, |
142 outputs(asig) - actns, |
182 internals(asig) Un actns)" |
143 internals(asig) \<union> actns)" |
183 |
144 |
184 hide_def: |
145 definition hide :: "[('a, 's) ioa, 'a set] \<Rightarrow> ('a, 's) ioa" |
185 "hide A actns == |
146 where |
|
147 "hide A actns = |
186 (hide_asig (asig_of A) actns, |
148 (hide_asig (asig_of A) actns, |
187 starts_of A, |
149 starts_of A, |
188 trans_of A, |
150 trans_of A, |
189 wfair_of A, |
151 wfair_of A, |
190 sfair_of A)" |
152 sfair_of A)" |
191 |
153 |
192 (* ------------------------- renaming ------------------------------------------- *) |
154 (* ------------------------- renaming ------------------------------------------- *) |
193 |
155 |
194 rename_set_def: |
156 definition rename_set :: "'a set \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> 'c set" |
195 "rename_set A ren == {b. ? x. Some x = ren b & x : A}" |
157 where "rename_set A ren = {b. \<exists>x. Some x = ren b \<and> x \<in> A}" |
196 |
158 |
197 rename_def: |
159 definition rename :: "('a, 'b) ioa \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> ('c, 'b) ioa" |
198 "rename ioa ren == |
160 where |
199 ((rename_set (inp ioa) ren, |
161 "rename ioa ren = |
200 rename_set (out ioa) ren, |
162 ((rename_set (inp ioa) ren, |
201 rename_set (int ioa) ren), |
163 rename_set (out ioa) ren, |
202 starts_of ioa, |
164 rename_set (int ioa) ren), |
203 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
165 starts_of ioa, |
204 in |
166 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
205 ? x. Some(x) = ren(a) & (s,x,t):trans_of ioa}, |
167 in |
206 {rename_set s ren | s. s: wfair_of ioa}, |
168 \<exists>x. Some(x) = ren(a) \<and> (s,x,t):trans_of ioa}, |
207 {rename_set s ren | s. s: sfair_of ioa})" |
169 {rename_set s ren | s. s \<in> wfair_of ioa}, |
|
170 {rename_set s ren | s. s \<in> sfair_of ioa})" |
|
171 |
208 |
172 |
209 (* ------------------------- fairness ----------------------------- *) |
173 (* ------------------------- fairness ----------------------------- *) |
210 |
174 |
211 fairIOA_def: |
175 (* enabledness of actions and action sets *) |
212 "fairIOA A == (! S : wfair_of A. S<= local A) & |
176 |
213 (! S : sfair_of A. S<= local A)" |
177 definition enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" |
214 |
178 where "enabled A a s \<longleftrightarrow> (\<exists>t. s \<midarrow>a\<midarrow>A\<rightarrow> t)" |
215 input_resistant_def: |
179 |
216 "input_resistant A == ! W : sfair_of A. ! s a t. |
180 definition Enabled :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> 's \<Rightarrow> bool" |
217 reachable A s & reachable A t & a:inp A & |
181 where "Enabled A W s \<longleftrightarrow> (\<exists>w \<in> W. enabled A w s)" |
218 Enabled A W s & s \<midarrow>a\<midarrow>A\<rightarrow> t |
182 |
219 --> Enabled A W t" |
183 |
220 |
184 (* action set keeps enabled until probably disabled by itself *) |
221 enabled_def: |
185 |
222 "enabled A a s == ? t. s \<midarrow>a\<midarrow>A\<rightarrow> t" |
186 definition en_persistent :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> bool" |
223 |
187 where |
224 Enabled_def: |
188 "en_persistent A W \<longleftrightarrow> |
225 "Enabled A W s == ? w:W. enabled A w s" |
189 (\<forall>s a t. Enabled A W s \<and> a \<notin> W \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)" |
226 |
190 |
227 en_persistent_def: |
191 |
228 "en_persistent A W == ! s a t. Enabled A W s & |
192 (* post_conditions for actions and action sets *) |
229 a ~:W & |
193 |
230 s \<midarrow>a\<midarrow>A\<rightarrow> t |
194 definition was_enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" |
231 --> Enabled A W t" |
195 where "was_enabled A a t \<longleftrightarrow> (\<exists>s. s \<midarrow>a\<midarrow>A\<rightarrow> t)" |
232 was_enabled_def: |
196 |
233 "was_enabled A a t == ? s. s \<midarrow>a\<midarrow>A\<rightarrow> t" |
197 definition set_was_enabled :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> 's \<Rightarrow> bool" |
234 |
198 where "set_was_enabled A W t \<longleftrightarrow> (\<exists>w \<in> W. was_enabled A w t)" |
235 set_was_enabled_def: |
199 |
236 "set_was_enabled A W t == ? w:W. was_enabled A w t" |
200 |
|
201 (* constraints for fair IOA *) |
|
202 |
|
203 definition fairIOA :: "('a, 's) ioa \<Rightarrow> bool" |
|
204 where "fairIOA A \<longleftrightarrow> (\<forall>S \<in> wfair_of A. S \<subseteq> local A) \<and> (\<forall>S \<in> sfair_of A. S \<subseteq> local A)" |
|
205 |
|
206 definition input_resistant :: "('a, 's) ioa \<Rightarrow> bool" |
|
207 where |
|
208 "input_resistant A \<longleftrightarrow> |
|
209 (\<forall>W \<in> sfair_of A. \<forall>s a t. |
|
210 reachable A s \<and> reachable A t \<and> a \<in> inp A \<and> |
|
211 Enabled A W s \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)" |
237 |
212 |
238 |
213 |
239 declare split_paired_Ex [simp del] |
214 declare split_paired_Ex [simp del] |
240 |
215 |
241 lemmas ioa_projections = asig_of_def starts_of_def trans_of_def wfair_of_def sfair_of_def |
216 lemmas ioa_projections = asig_of_def starts_of_def trans_of_def wfair_of_def sfair_of_def |
242 |
217 |
243 |
218 |
244 subsection "asig_of, starts_of, trans_of" |
219 subsection "asig_of, starts_of, trans_of" |
245 |
220 |
246 lemma ioa_triple_proj: |
221 lemma ioa_triple_proj: |
247 "((asig_of (x,y,z,w,s)) = x) & |
222 "((asig_of (x,y,z,w,s)) = x) & |
248 ((starts_of (x,y,z,w,s)) = y) & |
223 ((starts_of (x,y,z,w,s)) = y) & |
249 ((trans_of (x,y,z,w,s)) = z) & |
224 ((trans_of (x,y,z,w,s)) = z) & |
250 ((wfair_of (x,y,z,w,s)) = w) & |
225 ((wfair_of (x,y,z,w,s)) = w) & |
251 ((sfair_of (x,y,z,w,s)) = s)" |
226 ((sfair_of (x,y,z,w,s)) = s)" |
252 apply (simp add: ioa_projections) |
227 apply (simp add: ioa_projections) |
253 done |
228 done |
254 |
229 |
255 lemma trans_in_actions: |
230 lemma trans_in_actions: |
256 "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A" |
231 "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A" |
257 apply (unfold is_trans_of_def actions_def is_asig_def) |
232 apply (unfold is_trans_of_def actions_def is_asig_def) |
258 apply (erule allE, erule impE, assumption) |
233 apply (erule allE, erule impE, assumption) |
259 apply simp |
234 apply simp |
260 done |
235 done |
261 |
236 |
262 lemma starts_of_par: |
237 lemma starts_of_par: "starts_of(A \<parallel> B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}" |
263 "starts_of(A \<parallel> B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}" |
238 by (simp add: par_def ioa_projections) |
264 apply (simp add: par_def ioa_projections) |
239 |
265 done |
240 lemma trans_of_par: |
266 |
241 "trans_of(A \<parallel> B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
267 lemma trans_of_par: |
242 in (a:act A | a:act B) & |
268 "trans_of(A \<parallel> B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
243 (if a:act A then |
269 in (a:act A | a:act B) & |
244 (fst(s),a,fst(t)):trans_of(A) |
270 (if a:act A then |
245 else fst(t) = fst(s)) |
271 (fst(s),a,fst(t)):trans_of(A) |
246 & |
272 else fst(t) = fst(s)) |
247 (if a:act B then |
273 & |
248 (snd(s),a,snd(t)):trans_of(B) |
274 (if a:act B then |
|
275 (snd(s),a,snd(t)):trans_of(B) |
|
276 else snd(t) = snd(s))}" |
249 else snd(t) = snd(s))}" |
277 |
250 by (simp add: par_def ioa_projections) |
278 apply (simp add: par_def ioa_projections) |
|
279 done |
|
280 |
251 |
281 |
252 |
282 subsection "actions and par" |
253 subsection "actions and par" |
283 |
254 |
284 lemma actions_asig_comp: |
255 lemma actions_asig_comp: "actions(asig_comp a b) = actions(a) Un actions(b)" |
285 "actions(asig_comp a b) = actions(a) Un actions(b)" |
256 by (auto simp add: actions_def asig_comp_def asig_projections) |
286 apply (simp (no_asm) add: actions_def asig_comp_def asig_projections) |
|
287 apply blast |
|
288 done |
|
289 |
257 |
290 lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)" |
258 lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)" |
291 apply (simp add: par_def ioa_projections) |
259 by (simp add: par_def ioa_projections) |
292 done |
260 |
293 |
261 |
294 |
262 lemma externals_of_par: "ext (A1\<parallel>A2) = (ext A1) Un (ext A2)" |
295 lemma externals_of_par: "ext (A1\<parallel>A2) = |
263 apply (simp add: externals_def asig_of_par asig_comp_def |
296 (ext A1) Un (ext A2)" |
264 asig_inputs_def asig_outputs_def Un_def set_diff_eq) |
297 apply (simp add: externals_def asig_of_par asig_comp_def |
265 apply blast |
298 asig_inputs_def asig_outputs_def Un_def set_diff_eq) |
266 done |
299 apply blast |
267 |
300 done |
268 lemma actions_of_par: "act (A1\<parallel>A2) = (act A1) Un (act A2)" |
301 |
269 apply (simp add: actions_def asig_of_par asig_comp_def |
302 lemma actions_of_par: "act (A1\<parallel>A2) = |
270 asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) |
303 (act A1) Un (act A2)" |
271 apply blast |
304 apply (simp add: actions_def asig_of_par asig_comp_def |
272 done |
305 asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) |
273 |
306 apply blast |
274 lemma inputs_of_par: "inp (A1\<parallel>A2) = ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))" |
307 done |
275 by (simp add: actions_def asig_of_par asig_comp_def |
308 |
276 asig_inputs_def asig_outputs_def Un_def set_diff_eq) |
309 lemma inputs_of_par: "inp (A1\<parallel>A2) = |
277 |
310 ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))" |
278 lemma outputs_of_par: "out (A1\<parallel>A2) = (out A1) Un (out A2)" |
311 apply (simp add: actions_def asig_of_par asig_comp_def |
279 by (simp add: actions_def asig_of_par asig_comp_def |
312 asig_inputs_def asig_outputs_def Un_def set_diff_eq) |
280 asig_outputs_def Un_def set_diff_eq) |
313 done |
281 |
314 |
282 lemma internals_of_par: "int (A1\<parallel>A2) = (int A1) Un (int A2)" |
315 lemma outputs_of_par: "out (A1\<parallel>A2) = |
283 by (simp add: actions_def asig_of_par asig_comp_def |
316 (out A1) Un (out A2)" |
284 asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) |
317 apply (simp add: actions_def asig_of_par asig_comp_def |
|
318 asig_outputs_def Un_def set_diff_eq) |
|
319 done |
|
320 |
|
321 lemma internals_of_par: "int (A1\<parallel>A2) = |
|
322 (int A1) Un (int A2)" |
|
323 apply (simp add: actions_def asig_of_par asig_comp_def |
|
324 asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) |
|
325 done |
|
326 |
285 |
327 |
286 |
328 subsection "actions and compatibility" |
287 subsection "actions and compatibility" |
329 |
288 |
330 lemma compat_commute: "compatible A B = compatible B A" |
289 lemma compat_commute: "compatible A B = compatible B A" |
331 apply (simp add: compatible_def Int_commute) |
290 by (auto simp add: compatible_def Int_commute) |
332 apply auto |
291 |
333 done |
292 lemma ext1_is_not_int2: "[| compatible A1 A2; a:ext A1|] ==> a~:int A2" |
334 |
293 apply (unfold externals_def actions_def compatible_def) |
335 lemma ext1_is_not_int2: |
294 apply simp |
336 "[| compatible A1 A2; a:ext A1|] ==> a~:int A2" |
295 apply blast |
337 apply (unfold externals_def actions_def compatible_def) |
296 done |
338 apply simp |
|
339 apply blast |
|
340 done |
|
341 |
297 |
342 (* just commuting the previous one: better commute compatible *) |
298 (* just commuting the previous one: better commute compatible *) |
343 lemma ext2_is_not_int1: |
299 lemma ext2_is_not_int1: "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2" |
344 "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2" |
300 apply (unfold externals_def actions_def compatible_def) |
345 apply (unfold externals_def actions_def compatible_def) |
301 apply simp |
346 apply simp |
302 apply blast |
347 apply blast |
303 done |
348 done |
|
349 |
304 |
350 lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] |
305 lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] |
351 lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] |
306 lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] |
352 |
307 |
353 lemma intA_is_not_extB: |
308 lemma intA_is_not_extB: "[| compatible A B; x:int A |] ==> x~:ext B" |
354 "[| compatible A B; x:int A |] ==> x~:ext B" |
309 apply (unfold externals_def actions_def compatible_def) |
355 apply (unfold externals_def actions_def compatible_def) |
310 apply simp |
356 apply simp |
311 apply blast |
357 apply blast |
312 done |
358 done |
313 |
359 |
314 lemma intA_is_not_actB: "[| compatible A B; a:int A |] ==> a ~: act B" |
360 lemma intA_is_not_actB: |
315 apply (unfold externals_def actions_def compatible_def is_asig_def asig_of_def) |
361 "[| compatible A B; a:int A |] ==> a ~: act B" |
316 apply simp |
362 apply (unfold externals_def actions_def compatible_def is_asig_def asig_of_def) |
317 apply blast |
363 apply simp |
318 done |
364 apply blast |
|
365 done |
|
366 |
319 |
367 (* the only one that needs disjointness of outputs and of internals and _all_ acts *) |
320 (* the only one that needs disjointness of outputs and of internals and _all_ acts *) |
368 lemma outAactB_is_inpB: |
321 lemma outAactB_is_inpB: "[| compatible A B; a:out A ;a:act B|] ==> a : inp B" |
369 "[| compatible A B; a:out A ;a:act B|] ==> a : inp B" |
322 apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def |
370 apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def |
323 compatible_def is_asig_def asig_of_def) |
371 compatible_def is_asig_def asig_of_def) |
324 apply simp |
372 apply simp |
325 apply blast |
373 apply blast |
326 done |
374 done |
|
375 |
327 |
376 (* needed for propagation of input_enabledness from A,B to A\<parallel>B *) |
328 (* needed for propagation of input_enabledness from A,B to A\<parallel>B *) |
377 lemma inpAAactB_is_inpBoroutB: |
329 lemma inpAAactB_is_inpBoroutB: |
378 "[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B" |
330 "[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B" |
379 apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def |
331 apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def |
380 compatible_def is_asig_def asig_of_def) |
332 compatible_def is_asig_def asig_of_def) |
381 apply simp |
333 apply simp |
382 apply blast |
334 apply blast |
383 done |
335 done |
384 |
336 |
385 |
337 |
386 subsection "input_enabledness and par" |
338 subsection "input_enabledness and par" |
387 |
339 |
388 (* ugly case distinctions. Heart of proof: |
340 (* ugly case distinctions. Heart of proof: |
389 1. inpAAactB_is_inpBoroutB ie. internals are really hidden. |
341 1. inpAAactB_is_inpBoroutB ie. internals are really hidden. |
390 2. inputs_of_par: outputs are no longer inputs of par. This is important here *) |
342 2. inputs_of_par: outputs are no longer inputs of par. This is important here *) |
391 lemma input_enabled_par: |
343 lemma input_enabled_par: |
392 "[| compatible A B; input_enabled A; input_enabled B|] |
344 "[| compatible A B; input_enabled A; input_enabled B|] |
393 ==> input_enabled (A\<parallel>B)" |
345 ==> input_enabled (A\<parallel>B)" |
394 apply (unfold input_enabled_def) |
346 apply (unfold input_enabled_def) |
395 apply (simp add: Let_def inputs_of_par trans_of_par) |
347 apply (simp add: Let_def inputs_of_par trans_of_par) |
396 apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})") |
348 apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})") |
397 apply (simp add: inp_is_act) |
349 apply (simp add: inp_is_act) |
398 prefer 2 |
350 prefer 2 |
399 apply (simp add: inp_is_act) |
351 apply (simp add: inp_is_act) |
400 (* a: inp A *) |
352 (* a: inp A *) |
401 apply (case_tac "a:act B") |
353 apply (case_tac "a:act B") |
402 (* a:act B *) |
354 (* a:act B *) |
403 apply (erule_tac x = "a" in allE) |
355 apply (erule_tac x = "a" in allE) |
404 apply simp |
356 apply simp |
405 apply (drule inpAAactB_is_inpBoroutB) |
357 apply (drule inpAAactB_is_inpBoroutB) |
406 apply assumption |
358 apply assumption |
407 apply assumption |
359 apply assumption |
408 apply (erule_tac x = "a" in allE) |
360 apply (erule_tac x = "a" in allE) |
409 apply simp |
361 apply simp |
410 apply (erule_tac x = "aa" in allE) |
362 apply (erule_tac x = "aa" in allE) |
411 apply (erule_tac x = "b" in allE) |
363 apply (erule_tac x = "b" in allE) |
412 apply (erule exE) |
364 apply (erule exE) |
413 apply (erule exE) |
365 apply (erule exE) |
414 apply (rule_tac x = " (s2,s2a) " in exI) |
366 apply (rule_tac x = " (s2,s2a) " in exI) |
415 apply (simp add: inp_is_act) |
367 apply (simp add: inp_is_act) |
416 (* a~: act B*) |
368 (* a~: act B*) |
417 apply (simp add: inp_is_act) |
369 apply (simp add: inp_is_act) |
418 apply (erule_tac x = "a" in allE) |
370 apply (erule_tac x = "a" in allE) |
419 apply simp |
371 apply simp |
420 apply (erule_tac x = "aa" in allE) |
372 apply (erule_tac x = "aa" in allE) |
421 apply (erule exE) |
373 apply (erule exE) |
422 apply (rule_tac x = " (s2,b) " in exI) |
374 apply (rule_tac x = " (s2,b) " in exI) |
423 apply simp |
375 apply simp |
424 |
376 |
425 (* a:inp B *) |
377 (* a:inp B *) |
426 apply (case_tac "a:act A") |
378 apply (case_tac "a:act A") |
427 (* a:act A *) |
379 (* a:act A *) |
428 apply (erule_tac x = "a" in allE) |
380 apply (erule_tac x = "a" in allE) |
429 apply (erule_tac x = "a" in allE) |
381 apply (erule_tac x = "a" in allE) |
430 apply (simp add: inp_is_act) |
382 apply (simp add: inp_is_act) |
431 apply (frule_tac A1 = "A" in compat_commute [THEN iffD1]) |
383 apply (frule_tac A1 = "A" in compat_commute [THEN iffD1]) |
432 apply (drule inpAAactB_is_inpBoroutB) |
384 apply (drule inpAAactB_is_inpBoroutB) |
433 back |
385 back |
434 apply assumption |
386 apply assumption |
435 apply assumption |
387 apply assumption |
436 apply simp |
388 apply simp |
437 apply (erule_tac x = "aa" in allE) |
389 apply (erule_tac x = "aa" in allE) |
438 apply (erule_tac x = "b" in allE) |
390 apply (erule_tac x = "b" in allE) |
439 apply (erule exE) |
391 apply (erule exE) |
440 apply (erule exE) |
392 apply (erule exE) |
441 apply (rule_tac x = " (s2,s2a) " in exI) |
393 apply (rule_tac x = " (s2,s2a) " in exI) |
442 apply (simp add: inp_is_act) |
394 apply (simp add: inp_is_act) |
443 (* a~: act B*) |
395 (* a~: act B*) |
444 apply (simp add: inp_is_act) |
396 apply (simp add: inp_is_act) |
445 apply (erule_tac x = "a" in allE) |
397 apply (erule_tac x = "a" in allE) |
446 apply (erule_tac x = "a" in allE) |
398 apply (erule_tac x = "a" in allE) |
447 apply simp |
399 apply simp |
448 apply (erule_tac x = "b" in allE) |
400 apply (erule_tac x = "b" in allE) |
449 apply (erule exE) |
401 apply (erule exE) |
450 apply (rule_tac x = " (aa,s2) " in exI) |
402 apply (rule_tac x = " (aa,s2) " in exI) |
451 apply simp |
403 apply simp |
452 done |
404 done |
453 |
405 |
454 |
406 |
455 subsection "invariants" |
407 subsection "invariants" |
456 |
408 |
457 lemma invariantI: |
409 lemma invariantI: |
458 "[| !!s. s:starts_of(A) ==> P(s); |
410 "[| !!s. s:starts_of(A) ==> P(s); |
459 !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] |
411 !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] |
460 ==> invariant A P" |
412 ==> invariant A P" |
461 apply (unfold invariant_def) |
413 apply (unfold invariant_def) |
462 apply (rule allI) |
414 apply (rule allI) |
463 apply (rule impI) |
415 apply (rule impI) |
464 apply (rule_tac x = "s" in reachable.induct) |
416 apply (rule_tac x = "s" in reachable.induct) |
465 apply assumption |
417 apply assumption |
466 apply blast |
418 apply blast |
467 apply blast |
419 apply blast |
468 done |
420 done |
469 |
421 |
470 lemma invariantI1: |
422 lemma invariantI1: |
471 "[| !!s. s : starts_of(A) ==> P(s); |
423 "[| !!s. s : starts_of(A) ==> P(s); |
472 !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) |
424 !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) |
473 |] ==> invariant A P" |
425 |] ==> invariant A P" |
474 apply (blast intro: invariantI) |
426 apply (blast intro: invariantI) |
475 done |
427 done |
476 |
428 |
477 lemma invariantE: "[| invariant A P; reachable A s |] ==> P(s)" |
429 lemma invariantE: "[| invariant A P; reachable A s |] ==> P(s)" |
484 |
436 |
485 |
437 |
486 lemmas reachable_0 = reachable.reachable_0 |
438 lemmas reachable_0 = reachable.reachable_0 |
487 and reachable_n = reachable.reachable_n |
439 and reachable_n = reachable.reachable_n |
488 |
440 |
489 lemma cancel_restrict_a: "starts_of(restrict ioa acts) = starts_of(ioa) & |
441 lemma cancel_restrict_a: "starts_of(restrict ioa acts) = starts_of(ioa) & |
490 trans_of(restrict ioa acts) = trans_of(ioa)" |
442 trans_of(restrict ioa acts) = trans_of(ioa)" |
491 apply (simp add: restrict_def ioa_projections) |
443 by (simp add: restrict_def ioa_projections) |
492 done |
|
493 |
444 |
494 lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s" |
445 lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s" |
495 apply (rule iffI) |
446 apply (rule iffI) |
496 apply (erule reachable.induct) |
447 apply (erule reachable.induct) |
497 apply (simp add: cancel_restrict_a reachable_0) |
448 apply (simp add: cancel_restrict_a reachable_0) |
498 apply (erule reachable_n) |
449 apply (erule reachable_n) |
499 apply (simp add: cancel_restrict_a) |
450 apply (simp add: cancel_restrict_a) |
500 (* <-- *) |
451 (* <-- *) |
501 apply (erule reachable.induct) |
452 apply (erule reachable.induct) |
502 apply (rule reachable_0) |
453 apply (rule reachable_0) |
503 apply (simp add: cancel_restrict_a) |
454 apply (simp add: cancel_restrict_a) |
504 apply (erule reachable_n) |
455 apply (erule reachable_n) |
505 apply (simp add: cancel_restrict_a) |
456 apply (simp add: cancel_restrict_a) |
506 done |
457 done |
507 |
458 |
508 lemma acts_restrict: "act (restrict A acts) = act A" |
459 lemma acts_restrict: "act (restrict A acts) = act A" |
509 apply (simp (no_asm) add: actions_def asig_internals_def |
460 apply (simp (no_asm) add: actions_def asig_internals_def |
510 asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def) |
461 asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def) |
511 apply auto |
462 apply auto |
512 done |
463 done |
513 |
464 |
514 lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) & |
465 lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) & |
515 trans_of(restrict ioa acts) = trans_of(ioa) & |
466 trans_of(restrict ioa acts) = trans_of(ioa) & |
516 reachable (restrict ioa acts) s = reachable ioa s & |
467 reachable (restrict ioa acts) s = reachable ioa s & |
517 act (restrict A acts) = act A" |
468 act (restrict A acts) = act A" |
518 apply (simp (no_asm) add: cancel_restrict_a cancel_restrict_b acts_restrict) |
469 by (simp add: cancel_restrict_a cancel_restrict_b acts_restrict) |
519 done |
|
520 |
470 |
521 |
471 |
522 subsection "rename" |
472 subsection "rename" |
523 |
473 |
524 lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t ==> (? x. Some(x) = f(a) & s \<midarrow>x\<midarrow>C\<rightarrow> t)" |
474 lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t ==> (? x. Some(x) = f(a) & s \<midarrow>x\<midarrow>C\<rightarrow> t)" |
525 apply (simp add: Let_def rename_def trans_of_def) |
475 by (simp add: Let_def rename_def trans_of_def) |
526 done |
|
527 |
476 |
528 |
477 |
529 lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s" |
478 lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s" |
530 apply (erule reachable.induct) |
479 apply (erule reachable.induct) |
531 apply (rule reachable_0) |
480 apply (rule reachable_0) |
532 apply (simp add: rename_def ioa_projections) |
481 apply (simp add: rename_def ioa_projections) |
533 apply (drule trans_rename) |
482 apply (drule trans_rename) |
534 apply (erule exE) |
483 apply (erule exE) |
535 apply (erule conjE) |
484 apply (erule conjE) |
536 apply (erule reachable_n) |
485 apply (erule reachable_n) |
537 apply assumption |
486 apply assumption |
538 done |
487 done |
539 |
488 |
540 |
489 |
541 subsection "trans_of(A\<parallel>B)" |
490 subsection "trans_of(A\<parallel>B)" |
542 |
491 |
543 |
492 lemma trans_A_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act A|] |
544 lemma trans_A_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act A|] |
|
545 ==> (fst s,a,fst t):trans_of A" |
493 ==> (fst s,a,fst t):trans_of A" |
546 apply (simp add: Let_def par_def trans_of_def) |
494 by (simp add: Let_def par_def trans_of_def) |
547 done |
495 |
548 |
496 lemma trans_B_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act B|] |
549 lemma trans_B_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act B|] |
|
550 ==> (snd s,a,snd t):trans_of B" |
497 ==> (snd s,a,snd t):trans_of B" |
551 apply (simp add: Let_def par_def trans_of_def) |
498 by (simp add: Let_def par_def trans_of_def) |
552 done |
499 |
553 |
500 lemma trans_A_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act A|] |
554 lemma trans_A_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act A|] |
|
555 ==> fst s = fst t" |
501 ==> fst s = fst t" |
556 apply (simp add: Let_def par_def trans_of_def) |
502 by (simp add: Let_def par_def trans_of_def) |
557 done |
503 |
558 |
504 lemma trans_B_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act B|] |
559 lemma trans_B_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act B|] |
|
560 ==> snd s = snd t" |
505 ==> snd s = snd t" |
561 apply (simp add: Let_def par_def trans_of_def) |
506 by (simp add: Let_def par_def trans_of_def) |
562 done |
507 |
563 |
508 lemma trans_AB_proj: "(s,a,t):trans_of (A\<parallel>B) |
564 lemma trans_AB_proj: "(s,a,t):trans_of (A\<parallel>B) |
|
565 ==> a :act A | a :act B" |
509 ==> a :act A | a :act B" |
566 apply (simp add: Let_def par_def trans_of_def) |
510 by (simp add: Let_def par_def trans_of_def) |
567 done |
511 |
568 |
512 lemma trans_AB: "[|a:act A;a:act B; |
569 lemma trans_AB: "[|a:act A;a:act B; |
513 (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|] |
570 (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|] |
|
571 ==> (s,a,t):trans_of (A\<parallel>B)" |
514 ==> (s,a,t):trans_of (A\<parallel>B)" |
572 apply (simp add: Let_def par_def trans_of_def) |
515 by (simp add: Let_def par_def trans_of_def) |
573 done |
516 |
574 |
517 lemma trans_A_notB: "[|a:act A;a~:act B; |
575 lemma trans_A_notB: "[|a:act A;a~:act B; |
518 (fst s,a,fst t):trans_of A;snd s=snd t|] |
576 (fst s,a,fst t):trans_of A;snd s=snd t|] |
|
577 ==> (s,a,t):trans_of (A\<parallel>B)" |
519 ==> (s,a,t):trans_of (A\<parallel>B)" |
578 apply (simp add: Let_def par_def trans_of_def) |
520 by (simp add: Let_def par_def trans_of_def) |
579 done |
521 |
580 |
522 lemma trans_notA_B: "[|a~:act A;a:act B; |
581 lemma trans_notA_B: "[|a~:act A;a:act B; |
523 (snd s,a,snd t):trans_of B;fst s=fst t|] |
582 (snd s,a,snd t):trans_of B;fst s=fst t|] |
|
583 ==> (s,a,t):trans_of (A\<parallel>B)" |
524 ==> (s,a,t):trans_of (A\<parallel>B)" |
584 apply (simp add: Let_def par_def trans_of_def) |
525 by (simp add: Let_def par_def trans_of_def) |
585 done |
|
586 |
526 |
587 lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B |
527 lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B |
588 and trans_of_defs2 = trans_A_proj trans_B_proj trans_A_proj2 trans_B_proj2 trans_AB_proj |
528 and trans_of_defs2 = trans_A_proj trans_B_proj trans_A_proj2 trans_B_proj2 trans_AB_proj |
589 |
529 |
590 |
530 |
591 lemma trans_of_par4: |
531 lemma trans_of_par4: |
592 "((s,a,t) : trans_of(A \<parallel> B \<parallel> C \<parallel> D)) = |
532 "((s,a,t) : trans_of(A \<parallel> B \<parallel> C \<parallel> D)) = |
593 ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | |
533 ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | |
594 a:actions(asig_of(D))) & |
534 a:actions(asig_of(D))) & |
595 (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) |
535 (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) |
596 else fst t=fst s) & |
536 else fst t=fst s) & |
597 (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) |
537 (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) |
598 else fst(snd(t))=fst(snd(s))) & |
538 else fst(snd(t))=fst(snd(s))) & |
599 (if a:actions(asig_of(C)) then |
539 (if a:actions(asig_of(C)) then |
600 (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) |
540 (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) |
601 else fst(snd(snd(t)))=fst(snd(snd(s)))) & |
541 else fst(snd(snd(t)))=fst(snd(snd(s)))) & |
602 (if a:actions(asig_of(D)) then |
542 (if a:actions(asig_of(D)) then |
603 (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) |
543 (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) |
604 else snd(snd(snd(t)))=snd(snd(snd(s)))))" |
544 else snd(snd(snd(t)))=snd(snd(snd(s)))))" |
605 apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections) |
545 by (simp add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections) |
606 done |
|
607 |
546 |
608 |
547 |
609 subsection "proof obligation generator for IOA requirements" |
548 subsection "proof obligation generator for IOA requirements" |
610 |
549 |
611 (* without assumptions on A and B because is_trans_of is also incorporated in \<parallel>def *) |
550 (* without assumptions on A and B because is_trans_of is also incorporated in \<parallel>def *) |
612 lemma is_trans_of_par: "is_trans_of (A\<parallel>B)" |
551 lemma is_trans_of_par: "is_trans_of (A\<parallel>B)" |
613 apply (unfold is_trans_of_def) |
552 by (simp add: is_trans_of_def Let_def actions_of_par trans_of_par) |
614 apply (simp add: Let_def actions_of_par trans_of_par) |
553 |
615 done |
554 lemma is_trans_of_restrict: "is_trans_of A ==> is_trans_of (restrict A acts)" |
616 |
555 by (simp add: is_trans_of_def cancel_restrict acts_restrict) |
617 lemma is_trans_of_restrict: |
556 |
618 "is_trans_of A ==> is_trans_of (restrict A acts)" |
557 lemma is_trans_of_rename: "is_trans_of A ==> is_trans_of (rename A f)" |
619 apply (unfold is_trans_of_def) |
558 apply (unfold is_trans_of_def restrict_def restrict_asig_def) |
620 apply (simp add: cancel_restrict acts_restrict) |
559 apply (simp add: Let_def actions_def trans_of_def asig_internals_def |
621 done |
560 asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def) |
622 |
561 apply blast |
623 lemma is_trans_of_rename: |
562 done |
624 "is_trans_of A ==> is_trans_of (rename A f)" |
563 |
625 apply (unfold is_trans_of_def restrict_def restrict_asig_def) |
564 lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|] |
626 apply (simp add: Let_def actions_def trans_of_def asig_internals_def |
|
627 asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def) |
|
628 apply blast |
|
629 done |
|
630 |
|
631 lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|] |
|
632 ==> is_asig_of (A\<parallel>B)" |
565 ==> is_asig_of (A\<parallel>B)" |
633 apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def |
566 apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def |
634 asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def) |
567 asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def) |
635 apply (simp add: asig_of_def) |
568 apply (simp add: asig_of_def) |
636 apply auto |
569 apply auto |
637 done |
570 done |
638 |
571 |
639 lemma is_asig_of_restrict: |
572 lemma is_asig_of_restrict: "is_asig_of A ==> is_asig_of (restrict A f)" |
640 "is_asig_of A ==> is_asig_of (restrict A f)" |
573 apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def |
641 apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def |
574 asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def) |
642 asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def) |
575 apply simp |
643 apply simp |
576 apply auto |
644 apply auto |
577 done |
645 done |
|
646 |
578 |
647 lemma is_asig_of_rename: "is_asig_of A ==> is_asig_of (rename A f)" |
579 lemma is_asig_of_rename: "is_asig_of A ==> is_asig_of (rename A f)" |
648 apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def |
580 apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def |
649 asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def) |
581 asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def) |
650 apply auto |
582 apply auto |
651 apply (drule_tac [!] s = "Some _" in sym) |
583 apply (drule_tac [!] s = "Some _" in sym) |
652 apply auto |
584 apply auto |
653 done |
585 done |
654 |
586 |
655 lemmas [simp] = is_asig_of_par is_asig_of_restrict |
587 lemmas [simp] = is_asig_of_par is_asig_of_restrict |
656 is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename |
588 is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename |
657 |
589 |
658 |
590 |
659 lemma compatible_par: |
591 lemma compatible_par: "[|compatible A B; compatible A C |]==> compatible A (B\<parallel>C)" |
660 "[|compatible A B; compatible A C |]==> compatible A (B\<parallel>C)" |
592 apply (unfold compatible_def) |
661 apply (unfold compatible_def) |
593 apply (simp add: internals_of_par outputs_of_par actions_of_par) |
662 apply (simp add: internals_of_par outputs_of_par actions_of_par) |
594 apply auto |
663 apply auto |
595 done |
664 done |
|
665 |
596 |
666 (* better derive by previous one and compat_commute *) |
597 (* better derive by previous one and compat_commute *) |
667 lemma compatible_par2: |
598 lemma compatible_par2: "[|compatible A C; compatible B C |]==> compatible (A\<parallel>B) C" |
668 "[|compatible A C; compatible B C |]==> compatible (A\<parallel>B) C" |
599 apply (unfold compatible_def) |
669 apply (unfold compatible_def) |
600 apply (simp add: internals_of_par outputs_of_par actions_of_par) |
670 apply (simp add: internals_of_par outputs_of_par actions_of_par) |
601 apply auto |
671 apply auto |
602 done |
672 done |
603 |
673 |
604 lemma compatible_restrict: |
674 lemma compatible_restrict: |
605 "[| compatible A B; (ext B - S) Int ext A = {}|] |
675 "[| compatible A B; (ext B - S) Int ext A = {}|] |
606 ==> compatible A (restrict B S)" |
676 ==> compatible A (restrict B S)" |
607 apply (unfold compatible_def) |
677 apply (unfold compatible_def) |
608 apply (simp add: ioa_triple_proj asig_triple_proj externals_def |
678 apply (simp add: ioa_triple_proj asig_triple_proj externals_def |
609 restrict_def restrict_asig_def actions_def) |
679 restrict_def restrict_asig_def actions_def) |
610 apply auto |
680 apply auto |
611 done |
681 done |
|
682 |
|
683 |
612 |
684 declare split_paired_Ex [simp] |
613 declare split_paired_Ex [simp] |
685 |
614 |
686 end |
615 end |