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