author  wenzelm 
Mon, 09 Oct 2006 02:20:11 +0200  
changeset 20918  b9068bd7255c 
parent 19738  1ac610922636 
child 25131  2c8caac48ade 
permissions  rwrr 
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

1 
(* Title: HOLCF/IOA/ABP/Correctness.thy 
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

2 
ID: $Id$ 
12218  3 
Author: Olaf Müller 
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

4 
*) 
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

5 

17244  6 
header {* The main correctness proof: System_fin implements System *} 
7 

8 
theory Correctness 

9 
imports IOA Env Impl Impl_finite 

10 
begin 

3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

11 

a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

12 
consts 
19689  13 
reduce :: "'a list => 'a list" 
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

14 
primrec 
17244  15 
reduce_Nil: "reduce [] = []" 
16 
reduce_Cons: "reduce(x#xs) = 

17 
(case xs of 

18 
[] => [x] 

19 
 y#ys => (if (x=y) 

20 
then reduce xs 

3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

21 
else (x#(reduce xs))))" 
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

22 

19689  23 
constdefs 
24 
abs where 

25 
"abs == 

26 
(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), 

27 
(reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))" 

17244  28 

19689  29 
system_ioa :: "('m action, bool * 'm impl_state)ioa" 
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

30 
"system_ioa == (env_ioa  impl_ioa)" 
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

31 

19689  32 
system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" 
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

33 
"system_fin_ioa == (env_ioa  impl_fin_ioa)" 
17244  34 

3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

35 

17244  36 
axioms 
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

37 

17244  38 
sys_IOA: "IOA system_ioa" 
39 
sys_fin_IOA: "IOA system_fin_ioa" 

40 

19738  41 

42 

43 
declare split_paired_All [simp del] Collect_empty_eq [simp del] 

44 

45 
lemmas [simp] = 

46 
srch_asig_def rsch_asig_def rsch_ioa_def srch_ioa_def ch_ioa_def 

47 
ch_asig_def srch_actions_def rsch_actions_def rename_def rename_set_def asig_of_def 

48 
actions_def exis_elim srch_trans_def rsch_trans_def ch_trans_def 

49 
trans_of_def asig_projections set_lemmas 

50 

51 
lemmas abschannel_fin [simp] = 

52 
srch_fin_asig_def rsch_fin_asig_def 

53 
rsch_fin_ioa_def srch_fin_ioa_def 

54 
ch_fin_ioa_def ch_fin_trans_def ch_fin_asig_def 

55 

56 
lemmas impl_ioas = sender_ioa_def receiver_ioa_def 

57 
and impl_trans = sender_trans_def receiver_trans_def 

58 
and impl_asigs = sender_asig_def receiver_asig_def 

59 

60 
declare let_weak_cong [cong] 

61 
declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp] 

62 

63 
lemmas env_ioas = env_ioa_def env_asig_def env_trans_def 

20918  64 
lemmas hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas 
19738  65 

66 

67 
subsection {* lemmas about reduce *} 

68 

69 
lemma l_iff_red_nil: "(reduce l = []) = (l = [])" 

70 
by (induct l) (auto split: list.split) 

71 

72 
lemma hd_is_reduce_hd: "s ~= [] > hd s = hd (reduce s)" 

73 
by (induct s) (auto split: list.split) 

74 

75 
text {* to be used in the following Lemma *} 

76 
lemma rev_red_not_nil [rule_format]: 

77 
"l ~= [] > reverse (reduce l) ~= []" 

78 
by (induct l) (auto split: list.split) 

79 

80 
text {* shows applicability of the induction hypothesis of the following Lemma 1 *} 

81 
lemma last_ind_on_first: 

82 
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" 

83 
apply simp 

84 
apply (tactic {* auto_tac (claset(), 

85 
HOL_ss addsplits [thm"list.split"] 

86 
addsimps (thms "reverse.simps" @ [thm "hd_append", thm "rev_red_not_nil"])) *}) 

87 
done 

88 

89 
text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *} 

90 
lemma reduce_hd: 

91 
"if x=hd(reverse(reduce(l))) & reduce(l)~=[] then 

92 
reduce(l@[x])=reduce(l) else 

93 
reduce(l@[x])=reduce(l)@[x]" 

94 
apply (simplesubst split_if) 

95 
apply (rule conjI) 

96 
txt {* @{text ">"} *} 

97 
apply (induct_tac "l") 

98 
apply (simp (no_asm)) 

99 
apply (case_tac "list=[]") 

100 
apply (simp add: reverse.simps) 

101 
apply (rule impI) 

102 
apply (simp (no_asm)) 

103 
apply (cut_tac l = "list" in cons_not_nil) 

104 
apply (simp del: reduce_Cons) 

105 
apply (erule exE)+ 

106 
apply hypsubst 

107 
apply (simp del: reduce_Cons add: last_ind_on_first l_iff_red_nil) 

108 
txt {* @{text "<"} *} 

109 
apply (simp (no_asm) add: and_de_morgan_and_absorbe l_iff_red_nil) 

110 
apply (induct_tac "l") 

111 
apply (simp (no_asm)) 

112 
apply (case_tac "list=[]") 

113 
apply (cut_tac [2] l = "list" in cons_not_nil) 

114 
apply simp 

115 
apply (auto simp del: reduce_Cons simp add: last_ind_on_first l_iff_red_nil split: split_if) 

116 
apply simp 

117 
done 

118 

119 

120 
text {* Main Lemma 2 for R_pkt in showing that reduce is refinement. *} 

121 
lemma reduce_tl: "s~=[] ==> 

122 
if hd(s)=hd(tl(s)) & tl(s)~=[] then 

123 
reduce(tl(s))=reduce(s) else 

124 
reduce(tl(s))=tl(reduce(s))" 

125 
apply (cut_tac l = "s" in cons_not_nil) 

126 
apply simp 

127 
apply (erule exE)+ 

128 
apply (auto split: list.split) 

129 
done 

130 

131 

132 
subsection {* Channel Abstraction *} 

133 

134 
declare split_if [split del] 

135 

136 
lemma channel_abstraction: "is_weak_ref_map reduce ch_ioa ch_fin_ioa" 

137 
apply (simp (no_asm) add: is_weak_ref_map_def) 

138 
txt {* mainpart *} 

139 
apply (rule allI)+ 

140 
apply (rule imp_conj_lemma) 

141 
apply (induct_tac "a") 

142 
txt {* 2 cases *} 

143 
apply (simp_all (no_asm) cong del: if_weak_cong add: externals_def) 

144 
txt {* fst case *} 

145 
apply (rule impI) 

146 
apply (rule disjI2) 

147 
apply (rule reduce_hd) 

148 
txt {* snd case *} 

149 
apply (rule impI) 

150 
apply (erule conjE)+ 

151 
apply (erule disjE) 

152 
apply (simp add: l_iff_red_nil) 

153 
apply (erule hd_is_reduce_hd [THEN mp]) 

154 
apply (simp add: l_iff_red_nil) 

155 
apply (rule conjI) 

156 
apply (erule hd_is_reduce_hd [THEN mp]) 

157 
apply (rule bool_if_impl_or [THEN mp]) 

158 
apply (erule reduce_tl) 

159 
done 

160 

161 
declare split_if [split] 

162 

163 
lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" 

164 
apply (tactic {* 

165 
simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def", 

166 
thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap", 

167 
thm "channel_abstraction"]) 1 *}) 

168 
done 

169 

170 
lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" 

171 
apply (tactic {* 

172 
simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def", 

173 
thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap", 

174 
thm "channel_abstraction"]) 1 *}) 

175 
done 

176 

177 

178 
text {* 3 thms that do not hold generally! The lucky restriction here is 

179 
the absence of internal actions. *} 

180 
lemma sender_unchanged: "is_weak_ref_map (%id. id) sender_ioa sender_ioa" 

181 
apply (simp (no_asm) add: is_weak_ref_map_def) 

182 
txt {* mainpart *} 

183 
apply (rule allI)+ 

184 
apply (induct_tac a) 

185 
txt {* 7 cases *} 

186 
apply (simp_all (no_asm) add: externals_def) 

187 
done 

188 

189 
text {* 2 copies of before *} 

190 
lemma receiver_unchanged: "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa" 

191 
apply (simp (no_asm) add: is_weak_ref_map_def) 

192 
txt {* mainpart *} 

193 
apply (rule allI)+ 

194 
apply (induct_tac a) 

195 
txt {* 7 cases *} 

196 
apply (simp_all (no_asm) add: externals_def) 

197 
done 

198 

199 
lemma env_unchanged: "is_weak_ref_map (%id. id) env_ioa env_ioa" 

200 
apply (simp (no_asm) add: is_weak_ref_map_def) 

201 
txt {* mainpart *} 

202 
apply (rule allI)+ 

203 
apply (induct_tac a) 

204 
txt {* 7 cases *} 

205 
apply (simp_all (no_asm) add: externals_def) 

206 
done 

207 

208 

209 
lemma compat_single_ch: "compatible srch_ioa rsch_ioa" 

210 
apply (simp add: compatible_def Int_def) 

211 
apply (rule set_ext) 

212 
apply (induct_tac x) 

213 
apply simp_all 

214 
done 

215 

216 
text {* totally the same as before *} 

217 
lemma compat_single_fin_ch: "compatible srch_fin_ioa rsch_fin_ioa" 

218 
apply (simp add: compatible_def Int_def) 

219 
apply (rule set_ext) 

220 
apply (induct_tac x) 

221 
apply simp_all 

222 
done 

223 

224 
lemmas del_simps = trans_of_def srch_asig_def rsch_asig_def 

225 
asig_of_def actions_def srch_trans_def rsch_trans_def srch_ioa_def 

226 
srch_fin_ioa_def rsch_fin_ioa_def rsch_ioa_def sender_trans_def 

227 
receiver_trans_def set_lemmas 

228 

229 
lemma compat_rec: "compatible receiver_ioa (srch_ioa  rsch_ioa)" 

230 
apply (simp del: del_simps 

231 
add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 

232 
apply simp 

233 
apply (rule set_ext) 

234 
apply (induct_tac x) 

235 
apply simp_all 

236 
done 

237 

238 
text {* 5 proofs totally the same as before *} 

239 
lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa  rsch_fin_ioa)" 

240 
apply (simp del: del_simps 

241 
add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 

242 
apply simp 

243 
apply (rule set_ext) 

244 
apply (induct_tac x) 

245 
apply simp_all 

246 
done 

247 

248 
lemma compat_sen: "compatible sender_ioa 

249 
(receiver_ioa  srch_ioa  rsch_ioa)" 

250 
apply (simp del: del_simps 

251 
add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 

252 
apply simp 

253 
apply (rule set_ext) 

254 
apply (induct_tac x) 

255 
apply simp_all 

256 
done 

257 

258 
lemma compat_sen_fin: "compatible sender_ioa 

259 
(receiver_ioa  srch_fin_ioa  rsch_fin_ioa)" 

260 
apply (simp del: del_simps 

261 
add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 

262 
apply simp 

263 
apply (rule set_ext) 

264 
apply (induct_tac x) 

265 
apply simp_all 

266 
done 

267 

268 
lemma compat_env: "compatible env_ioa 

269 
(sender_ioa  receiver_ioa  srch_ioa  rsch_ioa)" 

270 
apply (simp del: del_simps 

271 
add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 

272 
apply simp 

273 
apply (rule set_ext) 

274 
apply (induct_tac x) 

275 
apply simp_all 

276 
done 

277 

278 
lemma compat_env_fin: "compatible env_ioa 

279 
(sender_ioa  receiver_ioa  srch_fin_ioa  rsch_fin_ioa)" 

280 
apply (simp del: del_simps 

281 
add: compatible_def asig_of_par asig_comp_def actions_def Int_def) 

282 
apply simp 

283 
apply (rule set_ext) 

284 
apply (induct_tac x) 

285 
apply simp_all 

286 
done 

287 

288 

289 
text {* lemmata about externals of channels *} 

290 
lemma ext_single_ch: "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & 

291 
externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))" 

292 
by (simp add: externals_def) 

293 

294 

295 
subsection {* Soundness of Abstraction *} 

296 

297 
lemmas ext_simps = externals_of_par ext_single_ch 

298 
and compat_simps = compat_single_ch compat_single_fin_ch compat_rec 

299 
compat_rec_fin compat_sen compat_sen_fin compat_env compat_env_fin 

300 
and abstractions = env_unchanged sender_unchanged 

301 
receiver_unchanged sender_abstraction receiver_abstraction 

302 

303 

304 
(* FIX: this proof should be done with compositionality on trace level, not on 

305 
weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA 

306 

307 
Goal "is_weak_ref_map abs system_ioa system_fin_ioa" 

308 

309 
by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def, 

310 
rsch_fin_ioa_def] @ env_ioas @ impl_ioas) 

311 
addsimps [system_def, system_fin_def, abs_def, 

312 
impl_ioa_def, impl_fin_ioa_def, sys_IOA, 

313 
sys_fin_IOA]) 1); 

314 

315 
by (REPEAT (EVERY[rtac fxg_is_weak_ref_map_of_product_IOA 1, 

316 
simp_tac (ss addsimps abstractions) 1, 

317 
rtac conjI 1])); 

318 

319 
by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); 

320 

321 
qed "system_refinement"; 

322 
*) 

17244  323 

3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

324 
end 