author  wenzelm 
Sun, 28 May 2006 19:54:20 +0200  
changeset 19741  f65265d71426 
parent 19739  c58ef2aa5430 
child 24327  a207114007c6 
permissions  rwrr 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

1 
(* Title: HOL/IOA/NTP/Impl.thy 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

2 
ID: $Id$ 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

3 
Author: Tobias Nipkow & Konrad Slind 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

5 

17244  6 
header {* The implementation *} 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

7 

17244  8 
theory Impl 
9 
imports Sender Receiver Abschannel 

10 
begin 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

11 

19739  12 
types 'm impl_state 
13 
= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" 

14 
(* sender_state * receiver_state * srch_state * rsch_state *) 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

15 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

16 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

17 
consts 
17244  18 
impl_ioa :: "('m action, 'm impl_state)ioa" 
19 
sen :: "'m impl_state => 'm sender_state" 

20 
rec :: "'m impl_state => 'm receiver_state" 

21 
srch :: "'m impl_state => 'm packet multiset" 

22 
rsch :: "'m impl_state => bool multiset" 

23 
inv1 :: "'m impl_state => bool" 

24 
inv2 :: "'m impl_state => bool" 

25 
inv3 :: "'m impl_state => bool" 

26 
inv4 :: "'m impl_state => bool" 

27 
hdr_sum :: "'m packet multiset => bool => nat" 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

28 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

29 
defs 
17244  30 
impl_def: 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

31 
"impl_ioa == (sender_ioa  receiver_ioa  srch_ioa  rsch_ioa)" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

32 

17244  33 
sen_def: "sen == fst" 
34 
rec_def: "rec == fst o snd" 

35 
srch_def: "srch == fst o snd o snd" 

36 
rsch_def: "rsch == snd o snd o snd" 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

37 

17244  38 
hdr_sum_def: 
3852  39 
"hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

40 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

41 
(* Lemma 5.1 *) 
17244  42 
inv1_def: 
43 
"inv1(s) == 

44 
(!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) 

45 
& (!b. count (ssent(sen s)) b 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

46 
= hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

47 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

48 
(* Lemma 5.2 *) 
17244  49 
inv2_def: "inv2(s) == 
50 
(rbit(rec(s)) = sbit(sen(s)) & 

51 
ssending(sen(s)) & 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

52 
count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) & 
17244  53 
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) 
54 
 

55 
(rbit(rec(s)) = (~sbit(sen(s))) & 

56 
rsending(rec(s)) & 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

57 
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) & 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

58 
count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

59 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

60 
(* Lemma 5.3 *) 
17244  61 
inv3_def: "inv3(s) == 
62 
rbit(rec(s)) = sbit(sen(s)) 

63 
> (!m. sq(sen(s))=[]  m ~= hd(sq(sen(s))) 

64 
> count (rrcvd(rec s)) (sbit(sen(s)),m) 

65 
+ count (srch s) (sbit(sen(s)),m) 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

66 
<= count (rsent(rec s)) (~sbit(sen s)))" 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

67 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

68 
(* Lemma 5.4 *) 
17244  69 
inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) > sq(sen(s)) ~= []" 
70 

19739  71 

72 
subsection {* Invariants *} 

73 

74 
declare Let_def [simp] le_SucI [simp] 

75 

76 
lemmas impl_ioas = 

77 
impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection] 

78 
rsch_ioa_thm [THEN eq_reflection] 

79 

80 
lemmas "transitions" = 

81 
sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def 

82 

83 

84 
lemmas [simp] = 

85 
ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig 

86 
in_receiver_asig in_srch_asig in_rsch_asig 

87 

88 
declare let_weak_cong [cong] 

89 

90 
lemma [simp]: 

91 
"fst(x) = sen(x)" 

92 
"fst(snd(x)) = rec(x)" 

93 
"fst(snd(snd(x))) = srch(x)" 

94 
"snd(snd(snd(x))) = rsch(x)" 

95 
by (simp_all add: sen_def rec_def srch_def rsch_def) 

96 

97 
lemma [simp]: 

98 
"a:actions(sender_asig) 

99 
 a:actions(receiver_asig) 

100 
 a:actions(srch_asig) 

101 
 a:actions(rsch_asig)" 

102 
by (induct a) simp_all 

103 

104 
declare split_paired_All [simp del] 

105 

106 

107 
(* Three Simp_sets in different sizes 

108 
 

109 

110 
1) simpset() does not unfold the transition relations 

111 
2) ss unfolds transition relations 

112 
3) renname_ss unfolds transitions and the abstract channel *) 

113 

114 
ML {* 

115 
val ss = simpset() addsimps thms "transitions"; 

116 
val rename_ss = ss addsimps thms "unfold_renaming"; 

117 

118 
val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]) 

119 
val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]) 

120 
*} 

121 

122 

123 
subsubsection {* Invariant 1 *} 

124 

125 
lemma inv1: "invariant impl_ioa inv1" 

126 

127 
apply (unfold impl_ioas) 

128 
apply (rule invariantI) 

129 
apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def) 

130 

131 
apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def) 

132 

133 
txt {* Split proof in two *} 

134 
apply (rule conjI) 

135 

136 
(* First half *) 

137 
apply (simp add: Impl.inv1_def split del: split_if) 

138 
apply (induct_tac a) 

139 

140 
apply (tactic "EVERY1[tac, tac, tac, tac]") 

141 
apply (tactic "tac 1") 

142 
apply (tactic "tac_ren 1") 

143 

144 
txt {* 5 + 1 *} 

145 

146 
apply (tactic "tac 1") 

147 
apply (tactic "tac_ren 1") 

148 

149 
txt {* 4 + 1 *} 

150 
apply (tactic {* EVERY1[tac, tac, tac, tac] *}) 

151 

152 

153 
txt {* Now the other half *} 

154 
apply (simp add: Impl.inv1_def split del: split_if) 

155 
apply (induct_tac a) 

156 
apply (tactic "EVERY1 [tac, tac]") 

157 

158 
txt {* detour 1 *} 

159 
apply (tactic "tac 1") 

160 
apply (tactic "tac_ren 1") 

161 
apply (rule impI) 

162 
apply (erule conjE)+ 

163 
apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def 

164 
split add: split_if) 

165 
txt {* detour 2 *} 

166 
apply (tactic "tac 1") 

167 
apply (tactic "tac_ren 1") 

168 
apply (rule impI) 

169 
apply (erule conjE)+ 

170 
apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def 

171 
Multiset.delm_nonempty_def split add: split_if) 

172 
apply (rule allI) 

173 
apply (rule conjI) 

174 
apply (rule impI) 

175 
apply hypsubst 

176 
apply (rule pred_suc [THEN iffD1]) 

177 
apply (drule less_le_trans) 

178 
apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props]) 

179 
apply assumption 

180 
apply assumption 

181 

182 
apply (rule countm_done_delm [THEN mp, symmetric]) 

183 
apply (rule refl) 

184 
apply (simp (no_asm_simp) add: Multiset.count_def) 

185 

186 
apply (rule impI) 

187 
apply (simp add: neg_flip) 

188 
apply hypsubst 

189 
apply (rule countm_spurious_delm) 

190 
apply (simp (no_asm)) 

191 

192 
apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]") 

193 

194 
done 

195 

196 

197 

198 
subsubsection {* INVARIANT 2 *} 

199 

200 
lemma inv2: "invariant impl_ioa inv2" 

201 

202 
apply (rule invariantI1) 

203 
txt {* Base case *} 

204 
apply (simp add: inv2_def receiver_projections sender_projections impl_ioas) 

205 

206 
apply (simp (no_asm_simp) add: impl_ioas split del: split_if) 

207 
apply (induct_tac "a") 

208 

209 
txt {* 10 cases. First 4 are simple, since state doesn't change *} 

210 

211 
ML {* val tac2 = asm_full_simp_tac (ss addsimps [thm "inv2_def"]) *} 

212 

213 
txt {* 10  7 *} 

214 
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]") 

215 
txt {* 6 *} 

216 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] 

19741  217 
(thm "inv1" RS thm "invariantE") RS conjunct1] 1 *}) 
19739  218 

219 
txt {* 6  5 *} 

220 
apply (tactic "EVERY1 [tac2,tac2]") 

221 

222 
txt {* 4 *} 

223 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] 

19741  224 
(thm "inv1" RS thm "invariantE") RS conjunct1] 1 *}) 
19739  225 
apply (tactic "tac2 1") 
226 

227 
txt {* 3 *} 

228 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] 

19741  229 
(thm "inv1" RS thm "invariantE")] 1 *}) 
19739  230 

231 
apply (tactic "tac2 1") 

232 
apply (tactic {* fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *}) 

233 
apply arith 

234 

235 
txt {* 2 *} 

236 
apply (tactic "tac2 1") 

237 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] 

19741  238 
(thm "inv1" RS thm "invariantE") RS conjunct1] 1 *}) 
19739  239 
apply (intro strip) 
240 
apply (erule conjE)+ 

241 
apply simp 

242 

243 
txt {* 1 *} 

244 
apply (tactic "tac2 1") 

245 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"] 

19741  246 
(thm "inv1" RS thm "invariantE") RS conjunct2] 1 *}) 
19739  247 
apply (intro strip) 
248 
apply (erule conjE)+ 

249 
apply (tactic {* fold_tac [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *}) 

250 
apply simp 

251 

252 
done 

253 

254 

255 
subsubsection {* INVARIANT 3 *} 

256 

257 
lemma inv3: "invariant impl_ioa inv3" 

258 

259 
apply (rule invariantI) 

260 
txt {* Base case *} 

261 
apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas) 

262 

263 
apply (simp (no_asm_simp) add: impl_ioas split del: split_if) 

264 
apply (induct_tac "a") 

265 

266 
ML {* val tac3 = asm_full_simp_tac (ss addsimps [thm "inv3_def"]) *} 

267 

268 
txt {* 10  8 *} 

269 

270 
apply (tactic "EVERY1[tac3,tac3,tac3]") 

271 

272 
apply (tactic "tac_ren 1") 

273 
apply (intro strip, (erule conjE)+) 

274 
apply hypsubst 

275 
apply (erule exE) 

276 
apply simp 

277 

278 
txt {* 7 *} 

279 
apply (tactic "tac3 1") 

280 
apply (tactic "tac_ren 1") 

281 
apply force 

282 

283 
txt {* 6  3 *} 

284 

285 
apply (tactic "EVERY1[tac3,tac3,tac3,tac3]") 

286 

287 
txt {* 2 *} 

288 
apply (tactic "asm_full_simp_tac ss 1") 

289 
apply (simp (no_asm) add: inv3_def) 

290 
apply (intro strip, (erule conjE)+) 

291 
apply (rule imp_disjL [THEN iffD1]) 

292 
apply (rule impI) 

293 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] 

19741  294 
(thm "inv2" RS thm "invariantE")] 1 *}) 
19739  295 
apply simp 
296 
apply (erule conjE)+ 

297 
apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and 

298 
k = "count (rsent (rec s)) (sbit (sen s))" in le_trans) 

299 
apply (tactic {* forward_tac [rewrite_rule [thm "inv1_def"] 

19741  300 
(thm "inv1" RS thm "invariantE") RS conjunct2] 1 *}) 
19739  301 
apply (simp add: hdr_sum_def Multiset.count_def) 
302 
apply (rule add_le_mono) 

303 
apply (rule countm_props) 

304 
apply (simp (no_asm)) 

305 
apply (rule countm_props) 

306 
apply (simp (no_asm)) 

307 
apply assumption 

308 

309 
txt {* 1 *} 

310 
apply (tactic "tac3 1") 

311 
apply (intro strip, (erule conjE)+) 

312 
apply (rule imp_disjL [THEN iffD1]) 

313 
apply (rule impI) 

314 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] 

19741  315 
(thm "inv2" RS thm "invariantE")] 1 *}) 
19739  316 
apply simp 
317 
done 

318 

319 

320 
subsubsection {* INVARIANT 4 *} 

321 

322 
lemma inv4: "invariant impl_ioa inv4" 

323 

324 
apply (rule invariantI) 

325 
txt {* Base case *} 

326 
apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas) 

327 

328 
apply (simp (no_asm_simp) add: impl_ioas split del: split_if) 

329 
apply (induct_tac "a") 

330 

331 
ML {* val tac4 = asm_full_simp_tac (ss addsimps [thm "inv4_def"]) *} 

332 

333 
txt {* 10  2 *} 

334 

335 
apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]") 

336 

337 
txt {* 2 b *} 

338 

339 
apply (intro strip, (erule conjE)+) 

340 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] 

19741  341 
(thm "inv2" RS thm "invariantE")] 1 *}) 
19739  342 
apply simp 
343 

344 
txt {* 1 *} 

345 
apply (tactic "tac4 1") 

346 
apply (intro strip, (erule conjE)+) 

347 
apply (rule ccontr) 

348 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"] 

19741  349 
(thm "inv2" RS thm "invariantE")] 1 *}) 
19739  350 
apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv3_def"] 
19741  351 
(thm "inv3" RS thm "invariantE")] 1 *}) 
19739  352 
apply simp 
353 
apply (erule_tac x = "m" in allE) 

354 
apply simp 

355 
done 

356 

357 

358 
text {* rebind them *} 

359 

360 
ML_setup {* 

361 
bind_thm ("inv1", rewrite_rule [thm "Impl.inv1_def"] (thm "inv1" RS thm "invariantE")); 

362 
bind_thm ("inv2", rewrite_rule [thm "Impl.inv2_def"] (thm "inv2" RS thm "invariantE")); 

363 
bind_thm ("inv3", rewrite_rule [thm "Impl.inv3_def"] (thm "inv3" RS thm "invariantE")); 

364 
bind_thm ("inv4", rewrite_rule [thm "Impl.inv4_def"] (thm "inv4" RS thm "invariantE")); 

365 
*} 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

366 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

367 
end 