author  mueller 
Thu, 17 Jul 1997 12:43:32 +0200  
changeset 3521  bdc51b4c6050 
parent 3457  a8ab7c64817c 
child 3842  b55686a7b22c 
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); 
3071  10 

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

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

13 

14 

15 
(*  *) 

16 

17 
section "recursive equations of operators"; 

18 

19 

20 
(*  *) 

21 
(* filter_act *) 

22 
(*  *) 

23 

24 

25 
goal thy "filter_act`UU = UU"; 

26 
by (simp_tac (!simpset addsimps [filter_act_def]) 1); 

27 
qed"filter_act_UU"; 

28 

29 
goal thy "filter_act`nil = nil"; 

30 
by (simp_tac (!simpset addsimps [filter_act_def]) 1); 

31 
qed"filter_act_nil"; 

32 

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

34 
by (simp_tac (!simpset addsimps [filter_act_def]) 1); 

35 
qed"filter_act_cons"; 

36 

37 
Addsimps [filter_act_UU,filter_act_nil,filter_act_cons]; 

38 

39 

40 
(*  *) 

41 
(* mk_trace *) 

42 
(*  *) 

43 

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

45 
by (simp_tac (!simpset addsimps [mk_trace_def]) 1); 

46 
qed"mk_trace_UU"; 

47 

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

49 
by (simp_tac (!simpset addsimps [mk_trace_def]) 1); 

50 
qed"mk_trace_nil"; 

51 

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

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

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

55 
\ else mk_trace A`xs)"; 

56 

57 
by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1); 

58 
qed"mk_trace_cons"; 

59 

60 
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons]; 

61 

62 
(*  *) 

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

63 
(* is_exec_fragC *) 
3071  64 
(*  *) 
65 

66 

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

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

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

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

73 
by (rtac trans 1); 

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

76 
by (rtac beta_cfun 1); 

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

78 
qed"is_exec_fragC_unfold"; 
3071  79 

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

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

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

83 
qed"is_exec_fragC_UU"; 
3071  84 

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

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

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

88 
qed"is_exec_fragC_nil"; 
3071  89 

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

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

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

94 
by (stac is_exec_fragC_unfold 1); 
3071  95 
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1); 
96 
by (Simp_tac 1); 

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

97 
qed"is_exec_fragC_cons"; 
3071  98 

99 

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

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

102 

103 
(*  *) 

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

104 
(* is_exec_frag *) 
3071  105 
(*  *) 
106 

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

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

108 
by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1); 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

109 
qed"is_exec_frag_UU"; 
3071  110 

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

111 
goal thy "is_exec_frag A (s, nil)"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

112 
by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1); 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

113 
qed"is_exec_frag_nil"; 
3071  114 

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

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

117 
\ is_exec_frag A (t, ex))"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

118 
by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1); 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

119 
qed"is_exec_frag_cons"; 
3071  120 

121 

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

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

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

125 

126 
(*  *) 

127 

128 
section "has_trace, mk_trace"; 

129 

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

131 
take the detour of schedules *) 

132 

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

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

135 

136 
by (safe_tac set_cs); 

137 
(* 1 *) 

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

139 
by (stac beta_cfun 1); 

140 
by (cont_tacR 1); 

141 
by (Simp_tac 1); 

142 
by (Asm_simp_tac 1); 

143 
(* 2 *) 

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

145 
by (stac beta_cfun 1); 

146 
by (cont_tacR 1); 

147 
by (Simp_tac 1); 

148 
by (safe_tac set_cs); 

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

150 
by (REPEAT (Asm_simp_tac 1)); 

151 
qed"has_trace_def2"; 

152 

3275  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 

3521  165 
"!! A. is_trans_of A ==> \ 
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

166 
\ ! s. is_exec_frag A (s,xs) > Forall (%a.a:act A) (filter_act`xs)"; 
3275  167 

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

168 
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); 
3275  169 
(* main case *) 
170 
ren "ss a t" 1; 

171 
by (safe_tac set_cs); 

3521  172 
by (REPEAT (asm_full_simp_tac (!simpset addsimps [is_trans_of_def]) 1)); 
3275  173 
qed"execfrag_in_sig"; 
174 

175 
goal thy 

3521  176 
"!! A.[ is_trans_of A; x:executions A ] ==> \ 
3275  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); 

3457  181 
by (rtac (execfrag_in_sig RS spec RS mp) 1); 
182 
by (Auto_tac()); 

3275  183 
qed"exec_in_sig"; 
184 

185 
goalw thy [schedules_def,has_schedule_def] 

3521  186 
"!! A.[ is_trans_of A; x:schedules A ] ==> \ 
3275  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 !! *) 

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

198 
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

199 
by (pair_induct_tac "y" [is_exec_frag_def] 1); 
3275  200 
by (strip_tac 1); 
201 
by (Seq_case_simp_tac "xa" 1); 

202 
by (pair_tac "a" 1); 

3457  203 
by (Auto_tac()); 
3275  204 
qed"execfrag_prefixclosed"; 
205 

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

207 

3361  208 

209 
(* second prefix notion for Finite x *) 

210 

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

211 
goal thy "! y s.is_exec_frag A (s,x@@y) > is_exec_frag A (s,x)"; 
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset

212 
by (pair_induct_tac "x" [is_exec_frag_def] 1); 
3361  213 
by (strip_tac 1); 
214 
by (Seq_case_simp_tac "s" 1); 

215 
by (pair_tac "a" 1); 

3457  216 
by (Auto_tac()); 
3361  217 
qed_spec_mp"exec_prefix2closed"; 
218 