author  huffman 
Wed, 17 Feb 2010 10:00:22 0800  
changeset 35174  e15040ae75d7 
parent 28839  32d498cf7595 
child 35215  a03462cbf86f 
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 
Author: Tobias Nipkow & Konrad Slind 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

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

4 

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

6 

17244  7 
theory Impl 
8 
imports Sender Receiver Abschannel 

9 
begin 

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

10 

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

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

14 

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

15 

27361  16 
definition 
17 
impl_ioa :: "('m action, 'm impl_state)ioa" where 

18 
impl_def: "impl_ioa == (sender_ioa  receiver_ioa  srch_ioa  rsch_ioa)" 

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

19 

27361  20 
definition sen :: "'m impl_state => 'm sender_state" where "sen = fst" 
21 
definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd" 

22 
definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd" 

23 
definition rsch :: "'m impl_state => bool multiset" where "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

24 

27361  25 
definition 
26 
hdr_sum :: "'m packet multiset => bool => nat" where 

27 
"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

28 

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

29 
(* Lemma 5.1 *) 
27361  30 
definition 
17244  31 
"inv1(s) == 
32 
(!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) 

33 
& (!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

34 
= 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

35 

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

36 
(* Lemma 5.2 *) 
27361  37 
definition 
38 
"inv2(s) == 

17244  39 
(rbit(rec(s)) = sbit(sen(s)) & 
40 
ssending(sen(s)) & 

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

41 
count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) & 
17244  42 
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) 
43 
 

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

45 
rsending(rec(s)) & 

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

46 
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

47 
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

48 

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

49 
(* Lemma 5.3 *) 
27361  50 
definition 
51 
"inv3(s) == 

17244  52 
rbit(rec(s)) = sbit(sen(s)) 
53 
> (!m. sq(sen(s))=[]  m ~= hd(sq(sen(s))) 

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

55 
+ 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

56 
<= 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

57 

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

58 
(* Lemma 5.4 *) 
27361  59 
definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) > sq(sen(s)) ~= []" 
17244  60 

19739  61 

62 
subsection {* Invariants *} 

63 

64 
declare Let_def [simp] le_SucI [simp] 

65 

66 
lemmas impl_ioas = 

67 
impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection] 

68 
rsch_ioa_thm [THEN eq_reflection] 

69 

70 
lemmas "transitions" = 

71 
sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def 

72 

73 

74 
lemmas [simp] = 

75 
ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig 

76 
in_receiver_asig in_srch_asig in_rsch_asig 

77 

78 
declare let_weak_cong [cong] 

79 

80 
lemma [simp]: 

81 
"fst(x) = sen(x)" 

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

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

84 
"snd(snd(snd(x))) = rsch(x)" 

85 
by (simp_all add: sen_def rec_def srch_def rsch_def) 

86 

87 
lemma [simp]: 

88 
"a:actions(sender_asig) 

89 
 a:actions(receiver_asig) 

90 
 a:actions(srch_asig) 

91 
 a:actions(rsch_asig)" 

92 
by (induct a) simp_all 

93 

94 
declare split_paired_All [simp del] 

95 

96 

97 
(* Three Simp_sets in different sizes 

98 
 

99 

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

101 
2) ss unfolds transition relations 

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

103 

104 
ML {* 

27355  105 
val ss = @{simpset} addsimps @{thms "transitions"}; 
26305  106 
val rename_ss = ss addsimps @{thms unfold_renaming}; 
19739  107 

26305  108 
val tac = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}]) 
109 
val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}]) 

19739  110 
*} 
111 

112 

113 
subsubsection {* Invariant 1 *} 

114 

26305  115 
lemma raw_inv1: "invariant impl_ioa inv1" 
19739  116 

117 
apply (unfold impl_ioas) 

118 
apply (rule invariantI) 

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

120 

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

122 

123 
txt {* Split proof in two *} 

124 
apply (rule conjI) 

125 

126 
(* First half *) 

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

128 
apply (induct_tac a) 

129 

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

131 
apply (tactic "tac 1") 

132 
apply (tactic "tac_ren 1") 

133 

134 
txt {* 5 + 1 *} 

135 

136 
apply (tactic "tac 1") 

137 
apply (tactic "tac_ren 1") 

138 

139 
txt {* 4 + 1 *} 

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

141 

142 

143 
txt {* Now the other half *} 

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

145 
apply (induct_tac a) 

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

147 

148 
txt {* detour 1 *} 

149 
apply (tactic "tac 1") 

150 
apply (tactic "tac_ren 1") 

151 
apply (rule impI) 

152 
apply (erule conjE)+ 

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

154 
split add: split_if) 

155 
txt {* detour 2 *} 

156 
apply (tactic "tac 1") 

157 
apply (tactic "tac_ren 1") 

158 
apply (rule impI) 

159 
apply (erule conjE)+ 

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

25161  161 
Multiset.delm_nonempty_def split add: split_if) 
19739  162 
apply (rule allI) 
163 
apply (rule conjI) 

164 
apply (rule impI) 

165 
apply hypsubst 

166 
apply (rule pred_suc [THEN iffD1]) 

167 
apply (drule less_le_trans) 

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

169 
apply assumption 

170 
apply assumption 

171 

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

173 
apply (rule refl) 

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

175 

176 
apply (rule impI) 

177 
apply (simp add: neg_flip) 

178 
apply hypsubst 

179 
apply (rule countm_spurious_delm) 

180 
apply (simp (no_asm)) 

181 

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

183 

184 
done 

185 

186 

187 

188 
subsubsection {* INVARIANT 2 *} 

189 

26305  190 
lemma raw_inv2: "invariant impl_ioa inv2" 
19739  191 

192 
apply (rule invariantI1) 

193 
txt {* Base case *} 

194 
apply (simp add: inv2_def receiver_projections sender_projections impl_ioas) 

195 

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

197 
apply (induct_tac "a") 

198 

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

200 

28265  201 
ML_prf {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *} 
19739  202 

203 
txt {* 10  7 *} 

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

205 
txt {* 6 *} 

26305  206 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] 
207 
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *}) 

19739  208 

209 
txt {* 6  5 *} 

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

211 

212 
txt {* 4 *} 

26305  213 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] 
214 
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *}) 

19739  215 
apply (tactic "tac2 1") 
216 

217 
txt {* 3 *} 

26305  218 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] 
219 
(@{thm raw_inv1} RS @{thm invariantE})] 1 *}) 

19739  220 

221 
apply (tactic "tac2 1") 

28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not wellformed tactics due to change of main conclusion;
wenzelm
parents:
28265
diff
changeset

222 
apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] 
27361  223 
(@{thm Impl.hdr_sum_def})] *}) 
19739  224 
apply arith 
225 

226 
txt {* 2 *} 

227 
apply (tactic "tac2 1") 

26305  228 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] 
229 
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *}) 

19739  230 
apply (intro strip) 
231 
apply (erule conjE)+ 

232 
apply simp 

233 

234 
txt {* 1 *} 

235 
apply (tactic "tac2 1") 

26305  236 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] 
237 
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *}) 

19739  238 
apply (intro strip) 
239 
apply (erule conjE)+ 

28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not wellformed tactics due to change of main conclusion;
wenzelm
parents:
28265
diff
changeset

240 
apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) 
19739  241 
apply simp 
242 

243 
done 

244 

245 

246 
subsubsection {* INVARIANT 3 *} 

247 

26305  248 
lemma raw_inv3: "invariant impl_ioa inv3" 
19739  249 

250 
apply (rule invariantI) 

251 
txt {* Base case *} 

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

253 

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

255 
apply (induct_tac "a") 

256 

28265  257 
ML_prf {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *} 
19739  258 

259 
txt {* 10  8 *} 

260 

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

262 

263 
apply (tactic "tac_ren 1") 

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

265 
apply hypsubst 

266 
apply (erule exE) 

267 
apply simp 

268 

269 
txt {* 7 *} 

270 
apply (tactic "tac3 1") 

271 
apply (tactic "tac_ren 1") 

272 
apply force 

273 

274 
txt {* 6  3 *} 

275 

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

277 

278 
txt {* 2 *} 

279 
apply (tactic "asm_full_simp_tac ss 1") 

280 
apply (simp (no_asm) add: inv3_def) 

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

282 
apply (rule imp_disjL [THEN iffD1]) 

283 
apply (rule impI) 

26305  284 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] 
285 
(@{thm raw_inv2} RS @{thm invariantE})] 1 *}) 

19739  286 
apply simp 
287 
apply (erule conjE)+ 

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

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

26305  290 
apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}] 
291 
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *}) 

19739  292 
apply (simp add: hdr_sum_def Multiset.count_def) 
293 
apply (rule add_le_mono) 

294 
apply (rule countm_props) 

295 
apply (simp (no_asm)) 

296 
apply (rule countm_props) 

297 
apply (simp (no_asm)) 

298 
apply assumption 

299 

300 
txt {* 1 *} 

301 
apply (tactic "tac3 1") 

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

303 
apply (rule imp_disjL [THEN iffD1]) 

304 
apply (rule impI) 

26305  305 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] 
306 
(@{thm raw_inv2} RS @{thm invariantE})] 1 *}) 

19739  307 
apply simp 
308 
done 

309 

310 

311 
subsubsection {* INVARIANT 4 *} 

312 

26305  313 
lemma raw_inv4: "invariant impl_ioa inv4" 
19739  314 

315 
apply (rule invariantI) 

316 
txt {* Base case *} 

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

318 

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

320 
apply (induct_tac "a") 

321 

28265  322 
ML_prf {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *} 
19739  323 

324 
txt {* 10  2 *} 

325 

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

327 

328 
txt {* 2 b *} 

329 

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

26305  331 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] 
332 
(@{thm raw_inv2} RS @{thm invariantE})] 1 *}) 

19739  333 
apply simp 
334 

335 
txt {* 1 *} 

336 
apply (tactic "tac4 1") 

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

338 
apply (rule ccontr) 

26305  339 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] 
340 
(@{thm raw_inv2} RS @{thm invariantE})] 1 *}) 

341 
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}] 

342 
(@{thm raw_inv3} RS @{thm invariantE})] 1 *}) 

19739  343 
apply simp 
344 
apply (erule_tac x = "m" in allE) 

345 
apply simp 

346 
done 

347 

348 

349 
text {* rebind them *} 

350 

26305  351 
lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def] 
352 
and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def] 

353 
and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def] 

354 
and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def] 

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

355 

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

356 
end 