author | wenzelm |
Wed, 30 Dec 2015 21:56:12 +0100 | |
changeset 62001 | 1f2788fb0b8b |
parent 62000 | 8cba509ace9c |
child 62002 | f1599e98c4d0 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/meta_theory/Traces.thy |
40945 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
3071 | 4 |
|
58880 | 5 |
section {* Executions and Traces of I/O automata in HOLCF *} |
3071 | 6 |
|
17233 | 7 |
theory Traces |
8 |
imports Sequence Automata |
|
9 |
begin |
|
3071 | 10 |
|
36452 | 11 |
default_sort type |
17233 | 12 |
|
41476 | 13 |
type_synonym |
3071 | 14 |
('a,'s)pairs = "('a * 's) Seq" |
41476 | 15 |
|
16 |
type_synonym |
|
3071 | 17 |
('a,'s)execution = "'s * ('a,'s)pairs" |
41476 | 18 |
|
19 |
type_synonym |
|
3071 | 20 |
'a trace = "'a Seq" |
3521 | 21 |
|
41476 | 22 |
type_synonym |
3521 | 23 |
('a,'s)execution_module = "('a,'s)execution set * 'a signature" |
41476 | 24 |
|
25 |
type_synonym |
|
3521 | 26 |
'a schedule_module = "'a trace set * 'a signature" |
41476 | 27 |
|
28 |
type_synonym |
|
3521 | 29 |
'a trace_module = "'a trace set * 'a signature" |
17233 | 30 |
|
3071 | 31 |
consts |
32 |
||
33 |
(* Executions *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
34 |
|
17233 | 35 |
is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr" |
36 |
is_exec_frag ::"[('a,'s)ioa, ('a,'s)execution] => bool" |
|
3071 | 37 |
has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool" |
38 |
executions :: "('a,'s)ioa => ('a,'s)execution set" |
|
39 |
||
40 |
(* Schedules and traces *) |
|
41 |
filter_act ::"('a,'s)pairs -> 'a trace" |
|
17233 | 42 |
has_schedule :: "[('a,'s)ioa, 'a trace] => bool" |
3071 | 43 |
has_trace :: "[('a,'s)ioa, 'a trace] => bool" |
17233 | 44 |
schedules :: "('a,'s)ioa => 'a trace set" |
3071 | 45 |
traces :: "('a,'s)ioa => 'a trace set" |
46 |
mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace" |
|
47 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
48 |
laststate ::"('a,'s)execution => 's" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
49 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
50 |
(* A predicate holds infinitely (finitely) often in a sequence *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
51 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
52 |
inf_often ::"('a => bool) => 'a Seq => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
53 |
fin_often ::"('a => bool) => 'a Seq => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
54 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
55 |
(* fairness of executions *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
56 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
57 |
wfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
58 |
sfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
59 |
is_wfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
60 |
is_sfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
61 |
fair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
62 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
63 |
(* fair behavior sets *) |
17233 | 64 |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
65 |
fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
66 |
fairtraces ::"('a,'s)ioa => 'a trace set" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
67 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
68 |
(* Notions of implementation *) |
22808 | 69 |
ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "=<|" 12) |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
70 |
fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" |
3071 | 71 |
|
3521 | 72 |
(* Execution, schedule and trace modules *) |
73 |
Execs :: "('a,'s)ioa => ('a,'s)execution_module" |
|
74 |
Scheds :: "('a,'s)ioa => 'a schedule_module" |
|
75 |
Traces :: "('a,'s)ioa => 'a trace_module" |
|
76 |
||
3071 | 77 |
|
78 |
defs |
|
79 |
||
80 |
||
81 |
(* ------------------- Executions ------------------------------ *) |
|
82 |
||
83 |
||
17233 | 84 |
is_exec_frag_def: |
10835 | 85 |
"is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" |
3071 | 86 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
87 |
|
17233 | 88 |
is_exec_fragC_def: |
89 |
"is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of |
|
3071 | 90 |
nil => TT |
17233 | 91 |
| x##xs => (flift1 |
92 |
(%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) |
|
10835 | 93 |
$x) |
17233 | 94 |
)))" |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
95 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
96 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
97 |
|
17233 | 98 |
executions_def: |
99 |
"executions ioa == {e. ((fst e) : starts_of(ioa)) & |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
100 |
is_exec_frag ioa e}" |
3071 | 101 |
|
102 |
||
103 |
(* ------------------- Schedules ------------------------------ *) |
|
104 |
||
105 |
||
17233 | 106 |
filter_act_def: |
3071 | 107 |
"filter_act == Map fst" |
108 |
||
17233 | 109 |
has_schedule_def: |
110 |
"has_schedule ioa sch == |
|
10835 | 111 |
(? ex:executions ioa. sch = filter_act$(snd ex))" |
3071 | 112 |
|
17233 | 113 |
schedules_def: |
3071 | 114 |
"schedules ioa == {sch. has_schedule ioa sch}" |
115 |
||
116 |
||
117 |
(* ------------------- Traces ------------------------------ *) |
|
118 |
||
17233 | 119 |
has_trace_def: |
120 |
"has_trace ioa tr == |
|
10835 | 121 |
(? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" |
17233 | 122 |
|
123 |
traces_def: |
|
3071 | 124 |
"traces ioa == {tr. has_trace ioa tr}" |
125 |
||
126 |
||
17233 | 127 |
mk_trace_def: |
128 |
"mk_trace ioa == LAM tr. |
|
10835 | 129 |
Filter (%a. a:ext(ioa))$(filter_act$tr)" |
3071 | 130 |
|
131 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
132 |
(* ------------------- Fair Traces ------------------------------ *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
133 |
|
17233 | 134 |
laststate_def: |
10835 | 135 |
"laststate ex == case Last$(snd ex) of |
12028 | 136 |
UU => fst ex |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
137 |
| Def at => snd at" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
138 |
|
17233 | 139 |
inf_often_def: |
10835 | 140 |
"inf_often P s == Infinite (Filter P$s)" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
141 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
142 |
(* filtering P yields a finite or partial sequence *) |
17233 | 143 |
fin_often_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
144 |
"fin_often P s == ~inf_often P s" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
145 |
|
17233 | 146 |
(* Note that partial execs cannot be wfair as the inf_often predicate in the |
147 |
else branch prohibits it. However they can be sfair in the case when all W |
|
148 |
are only finitely often enabled: Is this the right model? |
|
5976 | 149 |
See LiveIOA for solution conforming with the literature and superseding this one *) |
17233 | 150 |
wfair_ex_def: |
151 |
"wfair_ex A ex == ! W : wfair_of A. |
|
152 |
if Finite (snd ex) |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
153 |
then ~Enabled A W (laststate ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
154 |
else is_wfair A W ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
155 |
|
17233 | 156 |
is_wfair_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
157 |
"is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex) |
62000 | 158 |
| inf_often (%x. ~ Enabled A W (snd x)) (snd ex))" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
159 |
|
17233 | 160 |
sfair_ex_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
161 |
"sfair_ex A ex == ! W : sfair_of A. |
17233 | 162 |
if Finite (snd ex) |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
163 |
then ~Enabled A W (laststate ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
164 |
else is_sfair A W ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
165 |
|
17233 | 166 |
is_sfair_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
167 |
"is_sfair A W ex == (inf_often (%x. fst x:W) (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
168 |
| fin_often (%x. Enabled A W (snd x)) (snd ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
169 |
|
17233 | 170 |
fair_ex_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
171 |
"fair_ex A ex == wfair_ex A ex & sfair_ex A ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
172 |
|
17233 | 173 |
fairexecutions_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
174 |
"fairexecutions A == {ex. ex:executions A & fair_ex A ex}" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
175 |
|
17233 | 176 |
fairtraces_def: |
10835 | 177 |
"fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
178 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
179 |
|
3071 | 180 |
(* ------------------- Implementation ------------------------------ *) |
181 |
||
17233 | 182 |
ioa_implements_def: |
183 |
"ioa1 =<| ioa2 == |
|
184 |
(((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
|
3071 | 185 |
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & |
186 |
traces(ioa1) <= traces(ioa2))" |
|
187 |
||
17233 | 188 |
fair_implements_def: |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
189 |
"fair_implements C A == inp(C) = inp(A) & out(C)=out(A) & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
190 |
fairtraces(C) <= fairtraces(A)" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
191 |
|
3521 | 192 |
(* ------------------- Modules ------------------------------ *) |
193 |
||
17233 | 194 |
Execs_def: |
3521 | 195 |
"Execs A == (executions A, asig_of A)" |
196 |
||
17233 | 197 |
Scheds_def: |
3521 | 198 |
"Scheds A == (schedules A, asig_of A)" |
199 |
||
17233 | 200 |
Traces_def: |
3521 | 201 |
"Traces A == (traces A,asig_of A)" |
202 |
||
19741 | 203 |
|
37598 | 204 |
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex |
19741 | 205 |
declare Let_def [simp] |
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
45606
diff
changeset
|
206 |
setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *} |
19741 | 207 |
|
208 |
lemmas exec_rws = executions_def is_exec_frag_def |
|
209 |
||
210 |
||
211 |
||
212 |
subsection "recursive equations of operators" |
|
213 |
||
214 |
(* ---------------------------------------------------------------- *) |
|
215 |
(* filter_act *) |
|
216 |
(* ---------------------------------------------------------------- *) |
|
217 |
||
218 |
||
219 |
lemma filter_act_UU: "filter_act$UU = UU" |
|
220 |
apply (simp add: filter_act_def) |
|
221 |
done |
|
222 |
||
223 |
lemma filter_act_nil: "filter_act$nil = nil" |
|
224 |
apply (simp add: filter_act_def) |
|
225 |
done |
|
226 |
||
62001 | 227 |
lemma filter_act_cons: "filter_act$(x\<leadsto>xs) = (fst x) \<leadsto> filter_act$xs" |
19741 | 228 |
apply (simp add: filter_act_def) |
229 |
done |
|
230 |
||
231 |
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp] |
|
232 |
||
233 |
||
234 |
(* ---------------------------------------------------------------- *) |
|
235 |
(* mk_trace *) |
|
236 |
(* ---------------------------------------------------------------- *) |
|
237 |
||
238 |
lemma mk_trace_UU: "mk_trace A$UU=UU" |
|
239 |
apply (simp add: mk_trace_def) |
|
240 |
done |
|
241 |
||
242 |
lemma mk_trace_nil: "mk_trace A$nil=nil" |
|
243 |
apply (simp add: mk_trace_def) |
|
244 |
done |
|
245 |
||
62001 | 246 |
lemma mk_trace_cons: "mk_trace A$(at \<leadsto> xs) = |
19741 | 247 |
(if ((fst at):ext A) |
62001 | 248 |
then (fst at) \<leadsto> (mk_trace A$xs) |
19741 | 249 |
else mk_trace A$xs)" |
250 |
||
251 |
apply (simp add: mk_trace_def) |
|
252 |
done |
|
253 |
||
254 |
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp] |
|
255 |
||
256 |
(* ---------------------------------------------------------------- *) |
|
257 |
(* is_exec_fragC *) |
|
258 |
(* ---------------------------------------------------------------- *) |
|
259 |
||
260 |
||
261 |
lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of |
|
262 |
nil => TT |
|
263 |
| x##xs => (flift1 |
|
264 |
(%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) |
|
265 |
$x) |
|
266 |
))" |
|
267 |
apply (rule trans) |
|
268 |
apply (rule fix_eq2) |
|
269 |
apply (rule is_exec_fragC_def) |
|
270 |
apply (rule beta_cfun) |
|
271 |
apply (simp add: flift1_def) |
|
272 |
done |
|
273 |
||
274 |
lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU" |
|
275 |
apply (subst is_exec_fragC_unfold) |
|
276 |
apply simp |
|
277 |
done |
|
278 |
||
279 |
lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT" |
|
280 |
apply (subst is_exec_fragC_unfold) |
|
281 |
apply simp |
|
282 |
done |
|
283 |
||
62001 | 284 |
lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr\<leadsto>xs)) s = |
19741 | 285 |
(Def ((s,pr):trans_of A) |
286 |
andalso (is_exec_fragC A$xs)(snd pr))" |
|
287 |
apply (rule trans) |
|
288 |
apply (subst is_exec_fragC_unfold) |
|
289 |
apply (simp add: Consq_def flift1_def) |
|
290 |
apply simp |
|
291 |
done |
|
292 |
||
293 |
||
294 |
declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp] |
|
295 |
||
296 |
||
297 |
(* ---------------------------------------------------------------- *) |
|
298 |
(* is_exec_frag *) |
|
299 |
(* ---------------------------------------------------------------- *) |
|
300 |
||
301 |
lemma is_exec_frag_UU: "is_exec_frag A (s, UU)" |
|
302 |
apply (simp add: is_exec_frag_def) |
|
303 |
done |
|
304 |
||
305 |
lemma is_exec_frag_nil: "is_exec_frag A (s, nil)" |
|
306 |
apply (simp add: is_exec_frag_def) |
|
307 |
done |
|
308 |
||
62001 | 309 |
lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)\<leadsto>ex) = |
19741 | 310 |
(((s,a,t):trans_of A) & |
311 |
is_exec_frag A (t, ex))" |
|
312 |
apply (simp add: is_exec_frag_def) |
|
313 |
done |
|
314 |
||
315 |
||
316 |
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *) |
|
317 |
declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp] |
|
318 |
||
319 |
(* ---------------------------------------------------------------------------- *) |
|
320 |
section "laststate" |
|
321 |
(* ---------------------------------------------------------------------------- *) |
|
322 |
||
323 |
lemma laststate_UU: "laststate (s,UU) = s" |
|
324 |
apply (simp add: laststate_def) |
|
325 |
done |
|
326 |
||
327 |
lemma laststate_nil: "laststate (s,nil) = s" |
|
328 |
apply (simp add: laststate_def) |
|
329 |
done |
|
330 |
||
62001 | 331 |
lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at\<leadsto>ex) = laststate (snd at,ex)" |
19741 | 332 |
apply (simp (no_asm) add: laststate_def) |
333 |
apply (case_tac "ex=nil") |
|
334 |
apply (simp (no_asm_simp)) |
|
335 |
apply (simp (no_asm_simp)) |
|
336 |
apply (drule Finite_Last1 [THEN mp]) |
|
337 |
apply assumption |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
27208
diff
changeset
|
338 |
apply defined |
19741 | 339 |
done |
340 |
||
341 |
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp] |
|
342 |
||
343 |
lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
344 |
apply (tactic "Seq_Finite_induct_tac @{context} 1") |
19741 | 345 |
done |
346 |
||
347 |
||
348 |
subsection "has_trace, mk_trace" |
|
349 |
||
350 |
(* alternative definition of has_trace tailored for the refinement proof, as it does not |
|
351 |
take the detour of schedules *) |
|
352 |
||
353 |
lemma has_trace_def2: |
|
354 |
"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))" |
|
355 |
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def) |
|
26359 | 356 |
apply auto |
19741 | 357 |
done |
358 |
||
359 |
||
360 |
subsection "signatures and executions, schedules" |
|
361 |
||
362 |
(* All executions of A have only actions of A. This is only true because of the |
|
363 |
predicate state_trans (part of the predicate IOA): We have no dependent types. |
|
364 |
For executions of parallel automata this assumption is not needed, as in par_def |
|
365 |
this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *) |
|
366 |
||
367 |
lemma execfrag_in_sig: |
|
368 |
"!! A. is_trans_of A ==> |
|
369 |
! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
370 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
371 |
@{thm Forall_def}, @{thm sforall_def}] 1 *}) |
19741 | 372 |
(* main case *) |
26359 | 373 |
apply (auto simp add: is_trans_of_def) |
19741 | 374 |
done |
375 |
||
376 |
lemma exec_in_sig: |
|
377 |
"!! A.[| is_trans_of A; x:executions A |] ==> |
|
378 |
Forall (%a. a:act A) (filter_act$(snd x))" |
|
379 |
apply (simp add: executions_def) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
380 |
apply (tactic {* pair_tac @{context} "x" 1 *}) |
19741 | 381 |
apply (rule execfrag_in_sig [THEN spec, THEN mp]) |
382 |
apply auto |
|
383 |
done |
|
384 |
||
385 |
lemma scheds_in_sig: |
|
386 |
"!! A.[| is_trans_of A; x:schedules A |] ==> |
|
387 |
Forall (%a. a:act A) x" |
|
388 |
apply (unfold schedules_def has_schedule_def) |
|
389 |
apply (fast intro!: exec_in_sig) |
|
390 |
done |
|
391 |
||
392 |
||
393 |
subsection "executions are prefix closed" |
|
394 |
||
395 |
(* only admissible in y, not if done in x !! *) |
|
396 |
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
397 |
apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *}) |
19741 | 398 |
apply (intro strip) |
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
58880
diff
changeset
|
399 |
apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *}) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
400 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 401 |
apply auto |
402 |
done |
|
403 |
||
404 |
lemmas exec_prefixclosed = |
|
45606 | 405 |
conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]] |
19741 | 406 |
|
407 |
||
408 |
(* second prefix notion for Finite x *) |
|
409 |
||
410 |
lemma exec_prefix2closed [rule_format]: |
|
411 |
"! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)" |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
412 |
apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *}) |
19741 | 413 |
apply (intro strip) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
414 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
415 |
apply (tactic {* pair_tac @{context} "a" 1 *}) |
19741 | 416 |
apply auto |
417 |
done |
|
418 |
||
17233 | 419 |
end |