author | oheimb |
Tue, 21 Apr 1998 17:21:42 +0200 | |
changeset 4815 | b8a32ef742d9 |
parent 4559 | 8e604d885b54 |
child 5068 | fb28eaa07e01 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Traces.ML |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Theorems about Executions and Traces of I/O automata in HOLCF. |
|
7 |
*) |
|
8 |
||
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4559
diff
changeset
|
9 |
(* global changes to simpset() and claset(), see also TLS.ML *) |
3275 | 10 |
Delsimps (ex_simps @ all_simps); |
4536 | 11 |
Delsimps [split_paired_Ex]; |
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4559
diff
changeset
|
12 |
Addsimps [Let_def]; |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4559
diff
changeset
|
13 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
3071 | 14 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
15 |
val exec_rws = [executions_def,is_exec_frag_def]; |
3071 | 16 |
|
17 |
||
18 |
||
19 |
(* ----------------------------------------------------------------------------------- *) |
|
20 |
||
21 |
section "recursive equations of operators"; |
|
22 |
||
23 |
||
24 |
(* ---------------------------------------------------------------- *) |
|
25 |
(* filter_act *) |
|
26 |
(* ---------------------------------------------------------------- *) |
|
27 |
||
28 |
||
29 |
goal thy "filter_act`UU = UU"; |
|
4098 | 30 |
by (simp_tac (simpset() addsimps [filter_act_def]) 1); |
3071 | 31 |
qed"filter_act_UU"; |
32 |
||
33 |
goal thy "filter_act`nil = nil"; |
|
4098 | 34 |
by (simp_tac (simpset() addsimps [filter_act_def]) 1); |
3071 | 35 |
qed"filter_act_nil"; |
36 |
||
37 |
goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs"; |
|
4098 | 38 |
by (simp_tac (simpset() addsimps [filter_act_def]) 1); |
3071 | 39 |
qed"filter_act_cons"; |
40 |
||
41 |
Addsimps [filter_act_UU,filter_act_nil,filter_act_cons]; |
|
42 |
||
43 |
||
44 |
(* ---------------------------------------------------------------- *) |
|
45 |
(* mk_trace *) |
|
46 |
(* ---------------------------------------------------------------- *) |
|
47 |
||
48 |
goal thy "mk_trace A`UU=UU"; |
|
4098 | 49 |
by (simp_tac (simpset() addsimps [mk_trace_def]) 1); |
3071 | 50 |
qed"mk_trace_UU"; |
51 |
||
52 |
goal thy "mk_trace A`nil=nil"; |
|
4098 | 53 |
by (simp_tac (simpset() addsimps [mk_trace_def]) 1); |
3071 | 54 |
qed"mk_trace_nil"; |
55 |
||
56 |
goal thy "mk_trace A`(at >> xs) = \ |
|
57 |
\ (if ((fst at):ext A) \ |
|
58 |
\ then (fst at) >> (mk_trace A`xs) \ |
|
59 |
\ else mk_trace A`xs)"; |
|
60 |
||
4098 | 61 |
by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1); |
3071 | 62 |
qed"mk_trace_cons"; |
63 |
||
64 |
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons]; |
|
65 |
||
66 |
(* ---------------------------------------------------------------- *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
67 |
(* is_exec_fragC *) |
3071 | 68 |
(* ---------------------------------------------------------------- *) |
69 |
||
70 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
71 |
goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \ |
3071 | 72 |
\ nil => TT \ |
73 |
\ | x##xs => (flift1 \ |
|
3842 | 74 |
\ (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \ |
3071 | 75 |
\ `x) \ |
76 |
\ ))"; |
|
77 |
by (rtac trans 1); |
|
3457 | 78 |
by (rtac fix_eq2 1); |
79 |
by (rtac is_exec_fragC_def 1); |
|
80 |
by (rtac beta_cfun 1); |
|
4098 | 81 |
by (simp_tac (simpset() addsimps [flift1_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
82 |
qed"is_exec_fragC_unfold"; |
3071 | 83 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
84 |
goal thy "(is_exec_fragC A`UU) s=UU"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
85 |
by (stac is_exec_fragC_unfold 1); |
3071 | 86 |
by (Simp_tac 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
87 |
qed"is_exec_fragC_UU"; |
3071 | 88 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
89 |
goal thy "(is_exec_fragC A`nil) s = TT"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
90 |
by (stac is_exec_fragC_unfold 1); |
3071 | 91 |
by (Simp_tac 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
92 |
qed"is_exec_fragC_nil"; |
3071 | 93 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
94 |
goal thy "(is_exec_fragC A`(pr>>xs)) s = \ |
3071 | 95 |
\ (Def ((s,pr):trans_of A) \ |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
96 |
\ andalso (is_exec_fragC A`xs)(snd pr))"; |
3457 | 97 |
by (rtac trans 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
98 |
by (stac is_exec_fragC_unfold 1); |
4098 | 99 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1); |
3071 | 100 |
by (Simp_tac 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
101 |
qed"is_exec_fragC_cons"; |
3071 | 102 |
|
103 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
104 |
Addsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; |
3071 | 105 |
|
106 |
||
107 |
(* ---------------------------------------------------------------- *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
108 |
(* is_exec_frag *) |
3071 | 109 |
(* ---------------------------------------------------------------- *) |
110 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
111 |
goal thy "is_exec_frag A (s, UU)"; |
4098 | 112 |
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
113 |
qed"is_exec_frag_UU"; |
3071 | 114 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
115 |
goal thy "is_exec_frag A (s, nil)"; |
4098 | 116 |
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
117 |
qed"is_exec_frag_nil"; |
3071 | 118 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
119 |
goal thy "is_exec_frag A (s, (a,t)>>ex) = \ |
3071 | 120 |
\ (((s,a,t):trans_of A) & \ |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
121 |
\ is_exec_frag A (t, ex))"; |
4098 | 122 |
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
123 |
qed"is_exec_frag_cons"; |
3071 | 124 |
|
125 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
126 |
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
127 |
Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons]; |
3071 | 128 |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
129 |
(* ---------------------------------------------------------------------------- *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
130 |
section "laststate"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
131 |
(* ---------------------------------------------------------------------------- *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
132 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
133 |
goal thy "laststate (s,UU) = s"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
134 |
by (simp_tac (simpset() addsimps [laststate_def]) 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
135 |
qed"laststate_UU"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
136 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
137 |
goal thy "laststate (s,nil) = s"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
138 |
by (simp_tac (simpset() addsimps [laststate_def]) 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
139 |
qed"laststate_nil"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
140 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
141 |
goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
142 |
by (simp_tac (simpset() addsimps [laststate_def]) 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
143 |
by (case_tac "ex=nil" 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
144 |
by (Asm_simp_tac 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
145 |
by (Asm_simp_tac 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
146 |
by (dtac (Finite_Last1 RS mp) 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
147 |
by (assume_tac 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
148 |
by (def_tac 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
149 |
qed"laststate_cons"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
150 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
151 |
Addsimps [laststate_UU,laststate_nil,laststate_cons]; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
152 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
153 |
goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
154 |
by (Seq_Finite_induct_tac 1); |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
155 |
qed"exists_laststate"; |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset
|
156 |
|
3071 | 157 |
|
158 |
(* -------------------------------------------------------------------------------- *) |
|
159 |
||
160 |
section "has_trace, mk_trace"; |
|
161 |
||
162 |
(* alternative definition of has_trace tailored for the refinement proof, as it does not |
|
163 |
take the detour of schedules *) |
|
164 |
||
165 |
goalw thy [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] |
|
166 |
"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))"; |
|
167 |
||
168 |
by (safe_tac set_cs); |
|
169 |
(* 1 *) |
|
170 |
by (res_inst_tac[("x","ex")] bexI 1); |
|
171 |
by (stac beta_cfun 1); |
|
172 |
by (cont_tacR 1); |
|
173 |
by (Simp_tac 1); |
|
174 |
by (Asm_simp_tac 1); |
|
175 |
(* 2 *) |
|
176 |
by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1); |
|
177 |
by (stac beta_cfun 1); |
|
178 |
by (cont_tacR 1); |
|
179 |
by (Simp_tac 1); |
|
180 |
by (safe_tac set_cs); |
|
181 |
by (res_inst_tac[("x","ex")] bexI 1); |
|
182 |
by (REPEAT (Asm_simp_tac 1)); |
|
183 |
qed"has_trace_def2"; |
|
184 |
||
3275 | 185 |
|
186 |
(* -------------------------------------------------------------------------------- *) |
|
187 |
||
188 |
section "signatures and executions, schedules"; |
|
189 |
||
190 |
||
191 |
(* All executions of A have only actions of A. This is only true because of the |
|
192 |
predicate state_trans (part of the predicate IOA): We have no dependent types. |
|
193 |
For executions of parallel automata this assumption is not needed, as in par_def |
|
194 |
this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *) |
|
195 |
||
196 |
goal thy |
|
3521 | 197 |
"!! A. is_trans_of A ==> \ |
3842 | 198 |
\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)"; |
3275 | 199 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
200 |
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); |
3275 | 201 |
(* main case *) |
202 |
ren "ss a t" 1; |
|
203 |
by (safe_tac set_cs); |
|
4098 | 204 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1)); |
3275 | 205 |
qed"execfrag_in_sig"; |
206 |
||
207 |
goal thy |
|
3521 | 208 |
"!! A.[| is_trans_of A; x:executions A |] ==> \ |
3842 | 209 |
\ Forall (%a. a:act A) (filter_act`(snd x))"; |
3275 | 210 |
|
4098 | 211 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
3275 | 212 |
by (pair_tac "x" 1); |
3457 | 213 |
by (rtac (execfrag_in_sig RS spec RS mp) 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
214 |
by Auto_tac; |
3275 | 215 |
qed"exec_in_sig"; |
216 |
||
217 |
goalw thy [schedules_def,has_schedule_def] |
|
3521 | 218 |
"!! A.[| is_trans_of A; x:schedules A |] ==> \ |
3842 | 219 |
\ Forall (%a. a:act A) x"; |
3275 | 220 |
|
4098 | 221 |
by (fast_tac (claset() addSIs [exec_in_sig]) 1); |
3275 | 222 |
qed"scheds_in_sig"; |
223 |
||
4283 | 224 |
(* |
225 |
||
226 |
is ok but needs ForallQFilterP which has to been proven first (is trivial also) |
|
227 |
||
228 |
goalw thy [traces_def,has_trace_def] |
|
229 |
"!! A.[| x:traces A |] ==> \ |
|
230 |
\ Forall (%a. a:act A) x"; |
|
231 |
by (safe_tac set_cs ); |
|
4423 | 232 |
by (rtac ForallQFilterP 1); |
4283 | 233 |
by (fast_tac (!claset addSIs [ext_is_act]) 1); |
234 |
qed"traces_in_sig"; |
|
235 |
*) |
|
236 |
||
3275 | 237 |
|
238 |
(* -------------------------------------------------------------------------------- *) |
|
239 |
||
240 |
section "executions are prefix closed"; |
|
241 |
||
242 |
(* only admissible in y, not if done in x !! *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
243 |
goal thy "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
244 |
by (pair_induct_tac "y" [is_exec_frag_def] 1); |
3275 | 245 |
by (strip_tac 1); |
246 |
by (Seq_case_simp_tac "xa" 1); |
|
247 |
by (pair_tac "a" 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
248 |
by Auto_tac; |
3275 | 249 |
qed"execfrag_prefixclosed"; |
250 |
||
251 |
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp)); |
|
252 |
||
3361 | 253 |
|
254 |
(* second prefix notion for Finite x *) |
|
255 |
||
3842 | 256 |
goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"; |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
257 |
by (pair_induct_tac "x" [is_exec_frag_def] 1); |
3361 | 258 |
by (strip_tac 1); |
259 |
by (Seq_case_simp_tac "s" 1); |
|
260 |
by (pair_tac "a" 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
261 |
by Auto_tac; |
3361 | 262 |
qed_spec_mp"exec_prefix2closed"; |
263 |