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