1 (* Title: HOLCF/IOA/meta_theory/Traces.ML |
1 (* Title: HOLCF/IOA/meta_theory/Traces.ML |
2 ID: |
2 ID: $Id$ |
3 Author: Olaf M"uller |
3 Author: Olaf M"uller |
4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
5 |
5 |
6 Theorems about Executions and Traces of I/O automata in HOLCF. |
6 Theorems about Executions and Traces of I/O automata in HOLCF. |
7 *) |
7 *) |
8 |
8 |
9 |
9 Delsimps (ex_simps @ all_simps); |
10 |
10 |
11 val exec_rws = [executions_def,is_execution_fragment_def]; |
11 val exec_rws = [executions_def,is_execution_fragment_def]; |
12 |
12 |
13 |
13 |
14 |
14 |
148 by (safe_tac set_cs); |
148 by (safe_tac set_cs); |
149 by (res_inst_tac[("x","ex")] bexI 1); |
149 by (res_inst_tac[("x","ex")] bexI 1); |
150 by (REPEAT (Asm_simp_tac 1)); |
150 by (REPEAT (Asm_simp_tac 1)); |
151 qed"has_trace_def2"; |
151 qed"has_trace_def2"; |
152 |
152 |
|
153 |
|
154 (* -------------------------------------------------------------------------------- *) |
|
155 |
|
156 section "signatures and executions, schedules"; |
|
157 |
|
158 |
|
159 (* All executions of A have only actions of A. This is only true because of the |
|
160 predicate state_trans (part of the predicate IOA): We have no dependent types. |
|
161 For executions of parallel automata this assumption is not needed, as in par_def |
|
162 this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *) |
|
163 |
|
164 goal thy |
|
165 "!! A. IOA A ==> \ |
|
166 \ ! s. is_execution_fragment A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)"; |
|
167 |
|
168 by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1); |
|
169 (* main case *) |
|
170 ren "ss a t" 1; |
|
171 by (safe_tac set_cs); |
|
172 by (REPEAT (asm_full_simp_tac (!simpset addsimps [ioa_def,state_trans_def]) 1)); |
|
173 qed"execfrag_in_sig"; |
|
174 |
|
175 goal thy |
|
176 "!! A.[| IOA A; x:executions A |] ==> \ |
|
177 \ Forall (%a.a:act A) (filter_act`(snd x))"; |
|
178 |
|
179 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1); |
|
180 by (pair_tac "x" 1); |
|
181 br (execfrag_in_sig RS spec RS mp) 1; |
|
182 auto(); |
|
183 qed"exec_in_sig"; |
|
184 |
|
185 goalw thy [schedules_def,has_schedule_def] |
|
186 "!! A.[| IOA A; x:schedules A |] ==> \ |
|
187 \ Forall (%a.a:act A) x"; |
|
188 |
|
189 by (fast_tac (!claset addSIs [exec_in_sig]) 1); |
|
190 qed"scheds_in_sig"; |
|
191 |
|
192 |
|
193 (* -------------------------------------------------------------------------------- *) |
|
194 |
|
195 section "executions are prefix closed"; |
|
196 |
|
197 (* only admissible in y, not if done in x !! *) |
|
198 goal thy "!x s. is_execution_fragment A (s,x) & y<<x --> is_execution_fragment A (s,y)"; |
|
199 by (pair_induct_tac "y" [is_execution_fragment_def] 1); |
|
200 by (strip_tac 1); |
|
201 by (Seq_case_simp_tac "xa" 1); |
|
202 by (pair_tac "a" 1); |
|
203 auto(); |
|
204 qed"execfrag_prefixclosed"; |
|
205 |
|
206 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp)); |
|
207 |