author  mueller 
Mon, 12 Jan 1998 17:48:23 +0100  
changeset 4559  8e604d885b54 
parent 4536  74f7c556fd90 
child 4815  b8a32ef742d9 
permissions  rwrr 
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 

3275  9 
Delsimps (ex_simps @ all_simps); 
4536  10 
Delsimps [split_paired_Ex]; 
3071  11 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

12 
val exec_rws = [executions_def,is_exec_frag_def]; 
3071  13 

14 

15 

16 
(*  *) 

17 

18 
section "recursive equations of operators"; 

19 

20 

21 
(*  *) 

22 
(* filter_act *) 

23 
(*  *) 

24 

25 

26 
goal thy "filter_act`UU = UU"; 

4098  27 
by (simp_tac (simpset() addsimps [filter_act_def]) 1); 
3071  28 
qed"filter_act_UU"; 
29 

30 
goal thy "filter_act`nil = nil"; 

4098  31 
by (simp_tac (simpset() addsimps [filter_act_def]) 1); 
3071  32 
qed"filter_act_nil"; 
33 

34 
goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs"; 

4098  35 
by (simp_tac (simpset() addsimps [filter_act_def]) 1); 
3071  36 
qed"filter_act_cons"; 
37 

38 
Addsimps [filter_act_UU,filter_act_nil,filter_act_cons]; 

39 

40 

41 
(*  *) 

42 
(* mk_trace *) 

43 
(*  *) 

44 

45 
goal thy "mk_trace A`UU=UU"; 

4098  46 
by (simp_tac (simpset() addsimps [mk_trace_def]) 1); 
3071  47 
qed"mk_trace_UU"; 
48 

49 
goal thy "mk_trace A`nil=nil"; 

4098  50 
by (simp_tac (simpset() addsimps [mk_trace_def]) 1); 
3071  51 
qed"mk_trace_nil"; 
52 

53 
goal thy "mk_trace A`(at >> xs) = \ 

54 
\ (if ((fst at):ext A) \ 

55 
\ then (fst at) >> (mk_trace A`xs) \ 

56 
\ else mk_trace A`xs)"; 

57 

4098  58 
by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1); 
3071  59 
qed"mk_trace_cons"; 
60 

61 
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons]; 

62 

63 
(*  *) 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

64 
(* is_exec_fragC *) 
3071  65 
(*  *) 
66 

67 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

68 
goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \ 
3071  69 
\ nil => TT \ 
70 
\  x##xs => (flift1 \ 

3842  71 
\ (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \ 
3071  72 
\ `x) \ 
73 
\ ))"; 

74 
by (rtac trans 1); 

3457  75 
by (rtac fix_eq2 1); 
76 
by (rtac is_exec_fragC_def 1); 

77 
by (rtac beta_cfun 1); 

4098  78 
by (simp_tac (simpset() addsimps [flift1_def]) 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

79 
qed"is_exec_fragC_unfold"; 
3071  80 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

81 
goal thy "(is_exec_fragC A`UU) s=UU"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

82 
by (stac is_exec_fragC_unfold 1); 
3071  83 
by (Simp_tac 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

84 
qed"is_exec_fragC_UU"; 
3071  85 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

86 
goal thy "(is_exec_fragC A`nil) s = TT"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

87 
by (stac is_exec_fragC_unfold 1); 
3071  88 
by (Simp_tac 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

89 
qed"is_exec_fragC_nil"; 
3071  90 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

91 
goal thy "(is_exec_fragC A`(pr>>xs)) s = \ 
3071  92 
\ (Def ((s,pr):trans_of A) \ 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

93 
\ andalso (is_exec_fragC A`xs)(snd pr))"; 
3457  94 
by (rtac trans 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

95 
by (stac is_exec_fragC_unfold 1); 
4098  96 
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1); 
3071  97 
by (Simp_tac 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

98 
qed"is_exec_fragC_cons"; 
3071  99 

100 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

101 
Addsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; 
3071  102 

103 

104 
(*  *) 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

105 
(* is_exec_frag *) 
3071  106 
(*  *) 
107 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

108 
goal thy "is_exec_frag A (s, UU)"; 
4098  109 
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

110 
qed"is_exec_frag_UU"; 
3071  111 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

112 
goal thy "is_exec_frag A (s, nil)"; 
4098  113 
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

114 
qed"is_exec_frag_nil"; 
3071  115 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

116 
goal thy "is_exec_frag A (s, (a,t)>>ex) = \ 
3071  117 
\ (((s,a,t):trans_of A) & \ 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

118 
\ is_exec_frag A (t, ex))"; 
4098  119 
by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1); 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

120 
qed"is_exec_frag_cons"; 
3071  121 

122 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

123 
(* 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

124 
Addsimps [is_exec_frag_UU,is_exec_frag_nil, is_exec_frag_cons]; 
3071  125 

4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

126 
(*  *) 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

127 
section "laststate"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

128 
(*  *) 
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 
goal thy "laststate (s,UU) = s"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

131 
by (simp_tac (simpset() addsimps [laststate_def]) 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

132 
qed"laststate_UU"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

133 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

134 
goal thy "laststate (s,nil) = s"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

135 
by (simp_tac (simpset() addsimps [laststate_def]) 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

136 
qed"laststate_nil"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

137 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

138 
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

139 
by (simp_tac (simpset() addsimps [laststate_def]) 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

140 
by (case_tac "ex=nil" 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

141 
by (Asm_simp_tac 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

142 
by (Asm_simp_tac 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

143 
by (dtac (Finite_Last1 RS mp) 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

144 
by (assume_tac 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

145 
by (def_tac 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

146 
qed"laststate_cons"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

147 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

148 
Addsimps [laststate_UU,laststate_nil,laststate_cons]; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

149 

8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

150 
goal thy "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

151 
by (Seq_Finite_induct_tac 1); 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

152 
qed"exists_laststate"; 
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
4536
diff
changeset

153 

3071  154 

155 
(*  *) 

156 

157 
section "has_trace, mk_trace"; 

158 

159 
(* alternative definition of has_trace tailored for the refinement proof, as it does not 

160 
take the detour of schedules *) 

161 

162 
goalw thy [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 

163 
"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))"; 

164 

165 
by (safe_tac set_cs); 

166 
(* 1 *) 

167 
by (res_inst_tac[("x","ex")] bexI 1); 

168 
by (stac beta_cfun 1); 

169 
by (cont_tacR 1); 

170 
by (Simp_tac 1); 

171 
by (Asm_simp_tac 1); 

172 
(* 2 *) 

173 
by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1); 

174 
by (stac beta_cfun 1); 

175 
by (cont_tacR 1); 

176 
by (Simp_tac 1); 

177 
by (safe_tac set_cs); 

178 
by (res_inst_tac[("x","ex")] bexI 1); 

179 
by (REPEAT (Asm_simp_tac 1)); 

180 
qed"has_trace_def2"; 

181 

3275  182 

183 
(*  *) 

184 

185 
section "signatures and executions, schedules"; 

186 

187 

188 
(* All executions of A have only actions of A. This is only true because of the 

189 
predicate state_trans (part of the predicate IOA): We have no dependent types. 

190 
For executions of parallel automata this assumption is not needed, as in par_def 

191 
this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *) 

192 

193 
goal thy 

3521  194 
"!! A. is_trans_of A ==> \ 
3842  195 
\ ! s. is_exec_frag A (s,xs) > Forall (%a. a:act A) (filter_act`xs)"; 
3275  196 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

197 
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); 
3275  198 
(* main case *) 
199 
ren "ss a t" 1; 

200 
by (safe_tac set_cs); 

4098  201 
by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1)); 
3275  202 
qed"execfrag_in_sig"; 
203 

204 
goal thy 

3521  205 
"!! A.[ is_trans_of A; x:executions A ] ==> \ 
3842  206 
\ Forall (%a. a:act A) (filter_act`(snd x))"; 
3275  207 

4098  208 
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); 
3275  209 
by (pair_tac "x" 1); 
3457  210 
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

211 
by Auto_tac; 
3275  212 
qed"exec_in_sig"; 
213 

214 
goalw thy [schedules_def,has_schedule_def] 

3521  215 
"!! A.[ is_trans_of A; x:schedules A ] ==> \ 
3842  216 
\ Forall (%a. a:act A) x"; 
3275  217 

4098  218 
by (fast_tac (claset() addSIs [exec_in_sig]) 1); 
3275  219 
qed"scheds_in_sig"; 
220 

4283  221 
(* 
222 

223 
is ok but needs ForallQFilterP which has to been proven first (is trivial also) 

224 

225 
goalw thy [traces_def,has_trace_def] 

226 
"!! A.[ x:traces A ] ==> \ 

227 
\ Forall (%a. a:act A) x"; 

228 
by (safe_tac set_cs ); 

4423  229 
by (rtac ForallQFilterP 1); 
4283  230 
by (fast_tac (!claset addSIs [ext_is_act]) 1); 
231 
qed"traces_in_sig"; 

232 
*) 

233 

3275  234 

235 
(*  *) 

236 

237 
section "executions are prefix closed"; 

238 

239 
(* only admissible in y, not if done in x !! *) 

3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

240 
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

241 
by (pair_induct_tac "y" [is_exec_frag_def] 1); 
3275  242 
by (strip_tac 1); 
243 
by (Seq_case_simp_tac "xa" 1); 

244 
by (pair_tac "a" 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

245 
by Auto_tac; 
3275  246 
qed"execfrag_prefixclosed"; 
247 

248 
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp)); 

249 

3361  250 

251 
(* second prefix notion for Finite x *) 

252 

3842  253 
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

254 
by (pair_induct_tac "x" [is_exec_frag_def] 1); 
3361  255 
by (strip_tac 1); 
256 
by (Seq_case_simp_tac "s" 1); 

257 
by (pair_tac "a" 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

258 
by Auto_tac; 
3361  259 
qed_spec_mp"exec_prefix2closed"; 
260 