author | wenzelm |
Fri, 08 Feb 2019 14:42:28 +0100 | |
changeset 69794 | a19fdf64726c |
parent 67613 | ce654b0e6d69 |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
4530 | 1 |
(* Title: HOL/IOA/IOA.thy |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow & Konrad Slind |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
3 |
Copyright 1994 TU Muenchen |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
4 |
*) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
5 |
|
63167 | 6 |
section \<open>The I/O automata of Lynch and Tuttle\<close> |
17288 | 7 |
|
8 |
theory IOA |
|
9 |
imports Asig |
|
10 |
begin |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
|
42174 | 12 |
type_synonym 'a seq = "nat => 'a" |
13 |
type_synonym 'a oseq = "nat => 'a option" |
|
14 |
type_synonym ('a, 'b) execution = "'a oseq * 'b seq" |
|
15 |
type_synonym ('a, 's) transition = "('s * 'a * 's)" |
|
16 |
type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
17 |
|
62145 | 18 |
(* IO automata *) |
19 |
||
20 |
definition state_trans :: "['action signature, ('action,'state)transition set] => bool" |
|
67613 | 21 |
where "state_trans asig R \<equiv> |
22 |
(\<forall>triple. triple \<in> R \<longrightarrow> fst(snd(triple)) \<in> actions(asig)) \<and> |
|
23 |
(\<forall>a. (a \<in> inputs(asig)) \<longrightarrow> (\<forall>s1. \<exists>s2. (s1,a,s2) \<in> R))" |
|
62145 | 24 |
|
25 |
definition asig_of :: "('action,'state)ioa => 'action signature" |
|
26 |
where "asig_of == fst" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
27 |
|
62145 | 28 |
definition starts_of :: "('action,'state)ioa => 'state set" |
29 |
where "starts_of == (fst o snd)" |
|
30 |
||
31 |
definition trans_of :: "('action,'state)ioa => ('action,'state)transition set" |
|
32 |
where "trans_of == (snd o snd)" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
33 |
|
62145 | 34 |
definition IOA :: "('action,'state)ioa => bool" |
35 |
where "IOA(ioa) == (is_asig(asig_of(ioa)) & |
|
36 |
(~ starts_of(ioa) = {}) & |
|
37 |
state_trans (asig_of ioa) (trans_of ioa))" |
|
38 |
||
39 |
||
40 |
(* Executions, schedules, and traces *) |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
41 |
|
62145 | 42 |
(* An execution fragment is modelled with a pair of sequences: |
43 |
the first is the action options, the second the state sequence. |
|
44 |
Finite executions have None actions from some point on. *) |
|
45 |
definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool" |
|
67613 | 46 |
where "is_execution_fragment A ex \<equiv> |
62145 | 47 |
let act = fst(ex); state = snd(ex) |
67613 | 48 |
in \<forall>n a. (act(n)=None \<longrightarrow> state(Suc(n)) = state(n)) \<and> |
49 |
(act(n)=Some(a) \<longrightarrow> (state(n),a,state(Suc(n))) \<in> trans_of(A))" |
|
62145 | 50 |
|
51 |
definition executions :: "('action,'state)ioa => ('action,'state)execution set" |
|
67613 | 52 |
where "executions(ioa) \<equiv> {e. snd e 0 \<in> starts_of(ioa) \<and> is_execution_fragment ioa e}" |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
53 |
|
62145 | 54 |
|
55 |
definition reachable :: "[('action,'state)ioa, 'state] => bool" |
|
67613 | 56 |
where "reachable ioa s \<equiv> (\<exists>ex\<in>executions(ioa). \<exists>n. (snd ex n) = s)" |
62145 | 57 |
|
58 |
definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool" |
|
67613 | 59 |
where "invariant A P \<equiv> (\<forall>s. reachable A s \<longrightarrow> P(s))" |
62145 | 60 |
|
61 |
||
62 |
(* Composition of action signatures and automata *) |
|
63 |
||
64 |
consts |
|
67613 | 65 |
compatible_asigs ::"('a \<Rightarrow> 'action signature) \<Rightarrow> bool" |
66 |
asig_composition ::"('a \<Rightarrow> 'action signature) \<Rightarrow> 'action signature" |
|
67 |
compatible_ioas ::"('a \<Rightarrow> ('action,'state)ioa) \<Rightarrow> bool" |
|
68 |
ioa_composition ::"('a \<Rightarrow> ('action, 'state)ioa) \<Rightarrow> ('action,'a \<Rightarrow> 'state)ioa" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
69 |
|
62145 | 70 |
|
71 |
(* binary composition of action signatures and automata *) |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
72 |
|
62145 | 73 |
definition compat_asigs ::"['action signature, 'action signature] => bool" |
74 |
where "compat_asigs a1 a2 == |
|
67613 | 75 |
(((outputs(a1) Int outputs(a2)) = {}) \<and> |
76 |
((internals(a1) Int actions(a2)) = {}) \<and> |
|
62145 | 77 |
((internals(a2) Int actions(a1)) = {}))" |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
78 |
|
67613 | 79 |
definition compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] \<Rightarrow> bool" |
80 |
where "compat_ioas ioa1 ioa2 \<equiv> compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
81 |
|
67613 | 82 |
definition asig_comp :: "['action signature, 'action signature] \<Rightarrow> 'action signature" |
83 |
where "asig_comp a1 a2 \<equiv> |
|
84 |
(((inputs(a1) \<union> inputs(a2)) - (outputs(a1) \<union> outputs(a2)), |
|
85 |
(outputs(a1) \<union> outputs(a2)), |
|
86 |
(internals(a1) \<union> internals(a2))))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
87 |
|
67613 | 88 |
definition par :: "[('a,'s)ioa, ('a,'t)ioa] \<Rightarrow> ('a,'s*'t)ioa" (infixr "||" 10) |
89 |
where "(ioa1 || ioa2) \<equiv> |
|
62145 | 90 |
(asig_comp (asig_of ioa1) (asig_of ioa2), |
67613 | 91 |
{pr. fst(pr) \<in> starts_of(ioa1) \<and> snd(pr) \<in> starts_of(ioa2)}, |
62145 | 92 |
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
67613 | 93 |
in (a \<in> actions(asig_of(ioa1)) | a \<in> actions(asig_of(ioa2))) & |
94 |
(if a \<in> actions(asig_of(ioa1)) then |
|
95 |
(fst(s),a,fst(t)) \<in> trans_of(ioa1) |
|
62145 | 96 |
else fst(t) = fst(s)) |
97 |
& |
|
67613 | 98 |
(if a \<in> actions(asig_of(ioa2)) then |
99 |
(snd(s),a,snd(t)) \<in> trans_of(ioa2) |
|
62145 | 100 |
else snd(t) = snd(s))})" |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
101 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
102 |
|
62145 | 103 |
(* Filtering and hiding *) |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
104 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
105 |
(* Restrict the trace to those members of the set s *) |
62145 | 106 |
definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq" |
67613 | 107 |
where "filter_oseq p s \<equiv> |
108 |
(\<lambda>i. case s(i) |
|
109 |
of None \<Rightarrow> None |
|
110 |
| Some(x) \<Rightarrow> if p x then Some x else None)" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
111 |
|
67613 | 112 |
definition mk_trace :: "[('action,'state)ioa, 'action oseq] \<Rightarrow> 'action oseq" |
113 |
where "mk_trace(ioa) \<equiv> filter_oseq(\<lambda>a. a \<in> externals(asig_of(ioa)))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
114 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
115 |
(* Does an ioa have an execution with the given trace *) |
67613 | 116 |
definition has_trace :: "[('action,'state)ioa, 'action oseq] \<Rightarrow> bool" |
117 |
where "has_trace ioa b \<equiv> (\<exists>ex\<in>executions(ioa). b = mk_trace ioa (fst ex))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
118 |
|
62145 | 119 |
definition NF :: "'a oseq => 'a oseq" |
67613 | 120 |
where "NF(tr) \<equiv> SOME nf. \<exists>f. mono(f) \<and> (\<forall>i. nf(i)=tr(f(i))) \<and> |
121 |
(\<forall>j. j \<notin> range(f) \<longrightarrow> nf(j)= None) & |
|
122 |
(\<forall>i. nf(i)=None --> (nf (Suc i)) = None)" |
|
17288 | 123 |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
124 |
(* All the traces of an ioa *) |
62145 | 125 |
definition traces :: "('action,'state)ioa => 'action oseq set" |
67613 | 126 |
where "traces(ioa) \<equiv> {trace. \<exists>tr. trace=NF(tr) \<and> has_trace ioa tr}" |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
127 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
128 |
|
62145 | 129 |
definition restrict_asig :: "['a signature, 'a set] => 'a signature" |
67613 | 130 |
where "restrict_asig asig actns \<equiv> |
131 |
(inputs(asig) \<inter> actns, outputs(asig) \<inter> actns, |
|
132 |
internals(asig) \<union> (externals(asig) - actns))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
133 |
|
62145 | 134 |
definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" |
67613 | 135 |
where "restrict ioa actns \<equiv> |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
136 |
(restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
137 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
138 |
|
62145 | 139 |
|
140 |
(* Notions of correctness *) |
|
141 |
||
142 |
definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" |
|
67613 | 143 |
where "ioa_implements ioa1 ioa2 \<equiv> |
144 |
((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) \<and> |
|
145 |
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) \<and> |
|
146 |
traces(ioa1) \<subseteq> traces(ioa2))" |
|
17288 | 147 |
|
62145 | 148 |
|
149 |
(* Instantiation of abstract IOA by concrete actions *) |
|
150 |
||
67613 | 151 |
definition rename :: "('a, 'b)ioa \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> ('c,'b)ioa" |
152 |
where "rename ioa ren \<equiv> |
|
153 |
(({b. \<exists>x. Some(x)= ren(b) \<and> x \<in> inputs(asig_of(ioa))}, |
|
154 |
{b. \<exists>x. Some(x)= ren(b) \<and> x \<in> outputs(asig_of(ioa))}, |
|
155 |
{b. \<exists>x. Some(x)= ren(b) \<and> x \<in> internals(asig_of(ioa))}), |
|
62145 | 156 |
starts_of(ioa) , |
157 |
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
|
158 |
in |
|
67613 | 159 |
\<exists>x. Some(x) = ren(a) \<and> (s,x,t) \<in> trans_of(ioa)})" |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
160 |
|
19801 | 161 |
|
162 |
declare Let_def [simp] |
|
163 |
||
164 |
lemmas ioa_projections = asig_of_def starts_of_def trans_of_def |
|
165 |
and exec_rws = executions_def is_execution_fragment_def |
|
166 |
||
167 |
lemma ioa_triple_proj: |
|
168 |
"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z" |
|
169 |
apply (simp add: ioa_projections) |
|
170 |
done |
|
171 |
||
172 |
lemma trans_in_actions: |
|
67613 | 173 |
"[| IOA(A); (s1,a,s2) \<in> trans_of(A) |] ==> a \<in> actions(asig_of(A))" |
62145 | 174 |
apply (unfold IOA_def state_trans_def actions_def is_asig_def) |
19801 | 175 |
apply (erule conjE)+ |
176 |
apply (erule allE, erule impE, assumption) |
|
177 |
apply simp |
|
178 |
done |
|
179 |
||
180 |
||
181 |
lemma filter_oseq_idemp: "filter_oseq p (filter_oseq p s) = filter_oseq p s" |
|
182 |
apply (simp add: filter_oseq_def) |
|
183 |
apply (rule ext) |
|
184 |
apply (case_tac "s i") |
|
185 |
apply simp_all |
|
186 |
done |
|
187 |
||
188 |
lemma mk_trace_thm: |
|
189 |
"(mk_trace A s n = None) = |
|
67613 | 190 |
(s(n)=None | (\<exists>a. s(n)=Some(a) \<and> a \<notin> externals(asig_of(A)))) |
19801 | 191 |
& |
192 |
(mk_trace A s n = Some(a)) = |
|
67613 | 193 |
(s(n)=Some(a) \<and> a \<in> externals(asig_of(A)))" |
19801 | 194 |
apply (unfold mk_trace_def filter_oseq_def) |
195 |
apply (case_tac "s n") |
|
196 |
apply auto |
|
197 |
done |
|
198 |
||
67613 | 199 |
lemma reachable_0: "s \<in> starts_of(A) \<Longrightarrow> reachable A s" |
19801 | 200 |
apply (unfold reachable_def) |
201 |
apply (rule_tac x = "(%i. None, %i. s)" in bexI) |
|
202 |
apply simp |
|
203 |
apply (simp add: exec_rws) |
|
204 |
done |
|
205 |
||
206 |
lemma reachable_n: |
|
67613 | 207 |
"\<And>A. [| reachable A s; (s,a,t) \<in> trans_of(A) |] ==> reachable A t" |
19801 | 208 |
apply (unfold reachable_def exec_rws) |
209 |
apply (simp del: bex_simps) |
|
210 |
apply (simp (no_asm_simp) only: split_tupled_all) |
|
211 |
apply safe |
|
212 |
apply (rename_tac ex1 ex2 n) |
|
213 |
apply (rule_tac x = "(%i. if i<n then ex1 i else (if i=n then Some a else None) , %i. if i<Suc n then ex2 i else t)" in bexI) |
|
214 |
apply (rule_tac x = "Suc n" in exI) |
|
215 |
apply (simp (no_asm)) |
|
216 |
apply simp |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
19801
diff
changeset
|
217 |
apply (metis ioa_triple_proj less_antisym) |
19801 | 218 |
done |
219 |
||
220 |
||
221 |
lemma invariantI: |
|
67613 | 222 |
assumes p1: "\<And>s. s \<in> starts_of(A) \<Longrightarrow> P(s)" |
223 |
and p2: "\<And>s t a. [|reachable A s; P(s)|] ==> (s,a,t) \<in> trans_of(A) \<longrightarrow> P(t)" |
|
19801 | 224 |
shows "invariant A P" |
225 |
apply (unfold invariant_def reachable_def Let_def exec_rws) |
|
226 |
apply safe |
|
227 |
apply (rename_tac ex1 ex2 n) |
|
228 |
apply (rule_tac Q = "reachable A (ex2 n) " in conjunct1) |
|
229 |
apply simp |
|
230 |
apply (induct_tac n) |
|
231 |
apply (fast intro: p1 reachable_0) |
|
232 |
apply (erule_tac x = na in allE) |
|
233 |
apply (case_tac "ex1 na", simp_all) |
|
234 |
apply safe |
|
235 |
apply (erule p2 [THEN mp]) |
|
236 |
apply (fast dest: reachable_n)+ |
|
237 |
done |
|
238 |
||
239 |
lemma invariantI1: |
|
67613 | 240 |
"[| \<And>s. s \<in> starts_of(A) \<Longrightarrow> P(s); |
241 |
\<And>s t a. reachable A s \<Longrightarrow> P(s) \<longrightarrow> (s,a,t) \<in> trans_of(A) \<longrightarrow> P(t) |
|
19801 | 242 |
|] ==> invariant A P" |
243 |
apply (blast intro!: invariantI) |
|
244 |
done |
|
245 |
||
246 |
lemma invariantE: |
|
247 |
"[| invariant A P; reachable A s |] ==> P(s)" |
|
248 |
apply (unfold invariant_def) |
|
249 |
apply blast |
|
250 |
done |
|
251 |
||
252 |
lemma actions_asig_comp: |
|
67613 | 253 |
"actions(asig_comp a b) = actions(a) \<union> actions(b)" |
19801 | 254 |
apply (auto simp add: actions_def asig_comp_def asig_projections) |
255 |
done |
|
256 |
||
257 |
lemma starts_of_par: |
|
67613 | 258 |
"starts_of(A || B) = {p. fst(p) \<in> starts_of(A) \<and> snd(p) \<in> starts_of(B)}" |
19801 | 259 |
apply (simp add: par_def ioa_projections) |
260 |
done |
|
261 |
||
262 |
(* Every state in an execution is reachable *) |
|
263 |
lemma states_of_exec_reachable: |
|
67613 | 264 |
"ex \<in> executions(A) \<Longrightarrow> \<forall>n. reachable A (snd ex n)" |
19801 | 265 |
apply (unfold reachable_def) |
266 |
apply fast |
|
267 |
done |
|
268 |
||
269 |
||
270 |
lemma trans_of_par4: |
|
67613 | 271 |
"(s,a,t) \<in> trans_of(A || B || C || D) = |
272 |
((a \<in> actions(asig_of(A)) | a \<in> actions(asig_of(B)) | a \<in> actions(asig_of(C)) | |
|
273 |
a \<in> actions(asig_of(D))) \<and> |
|
274 |
(if a \<in> actions(asig_of(A)) then (fst(s),a,fst(t)) \<in> trans_of(A) |
|
275 |
else fst t=fst s) \<and> |
|
276 |
(if a \<in> actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))) \<in> trans_of(B) |
|
277 |
else fst(snd(t))=fst(snd(s))) \<and> |
|
278 |
(if a \<in> actions(asig_of(C)) then |
|
279 |
(fst(snd(snd(s))),a,fst(snd(snd(t)))) \<in> trans_of(C) |
|
280 |
else fst(snd(snd(t)))=fst(snd(snd(s)))) \<and> |
|
281 |
(if a \<in> actions(asig_of(D)) then |
|
282 |
(snd(snd(snd(s))),a,snd(snd(snd(t)))) \<in> trans_of(D) |
|
19801 | 283 |
else snd(snd(snd(t)))=snd(snd(snd(s)))))" |
284 |
(*SLOW*) |
|
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42174
diff
changeset
|
285 |
apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections) |
19801 | 286 |
done |
287 |
||
288 |
lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) & |
|
289 |
trans_of(restrict ioa acts) = trans_of(ioa) & |
|
290 |
reachable (restrict ioa acts) s = reachable ioa s" |
|
291 |
apply (simp add: is_execution_fragment_def executions_def |
|
292 |
reachable_def restrict_def ioa_projections) |
|
293 |
done |
|
294 |
||
295 |
lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)" |
|
296 |
apply (simp add: par_def ioa_projections) |
|
297 |
done |
|
298 |
||
299 |
||
300 |
lemma externals_of_par: "externals(asig_of(A1||A2)) = |
|
67613 | 301 |
(externals(asig_of(A1)) \<union> externals(asig_of(A2)))" |
19801 | 302 |
apply (simp add: externals_def asig_of_par asig_comp_def |
26806 | 303 |
asig_inputs_def asig_outputs_def Un_def set_diff_eq) |
19801 | 304 |
apply blast |
305 |
done |
|
306 |
||
307 |
lemma ext1_is_not_int2: |
|
67613 | 308 |
"[| compat_ioas A1 A2; a \<in> externals(asig_of(A1))|] ==> a \<notin> internals(asig_of(A2))" |
19801 | 309 |
apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def) |
310 |
apply auto |
|
311 |
done |
|
312 |
||
313 |
lemma ext2_is_not_int1: |
|
67613 | 314 |
"[| compat_ioas A2 A1 ; a \<in> externals(asig_of(A1))|] ==> a \<notin> internals(asig_of(A2))" |
19801 | 315 |
apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def) |
316 |
apply auto |
|
317 |
done |
|
318 |
||
319 |
lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] |
|
320 |
and ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] |
|
17288 | 321 |
|
322 |
end |