author  wenzelm 
Tue, 18 Nov 2008 18:25:42 +0100  
changeset 28839  32d498cf7595 
parent 28265  7e14443f2dd6 
child 35174  e15040ae75d7 
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 

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

19 
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

20 

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

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

24 
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

25 

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

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

29 

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

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

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

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

36 

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

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

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

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

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

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

46 
rsending(rec(s)) & 

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

47 
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

48 
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

49 

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

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

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

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

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

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

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

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

19739  62 

63 
subsection {* Invariants *} 

64 

65 
declare Let_def [simp] le_SucI [simp] 

66 

67 
lemmas impl_ioas = 

68 
impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection] 

69 
rsch_ioa_thm [THEN eq_reflection] 

70 

71 
lemmas "transitions" = 

72 
sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def 

73 

74 

75 
lemmas [simp] = 

76 
ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig 

77 
in_receiver_asig in_srch_asig in_rsch_asig 

78 

79 
declare let_weak_cong [cong] 

80 

81 
lemma [simp]: 

82 
"fst(x) = sen(x)" 

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

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

85 
"snd(snd(snd(x))) = rsch(x)" 

86 
by (simp_all add: sen_def rec_def srch_def rsch_def) 

87 

88 
lemma [simp]: 

89 
"a:actions(sender_asig) 

90 
 a:actions(receiver_asig) 

91 
 a:actions(srch_asig) 

92 
 a:actions(rsch_asig)" 

93 
by (induct a) simp_all 

94 

95 
declare split_paired_All [simp del] 

96 

97 

98 
(* Three Simp_sets in different sizes 

99 
 

100 

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

102 
2) ss unfolds transition relations 

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

104 

105 
ML {* 

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

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

19739  111 
*} 
112 

113 

114 
subsubsection {* Invariant 1 *} 

115 

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

118 
apply (unfold impl_ioas) 

119 
apply (rule invariantI) 

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

121 

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

123 

124 
txt {* Split proof in two *} 

125 
apply (rule conjI) 

126 

127 
(* First half *) 

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

129 
apply (induct_tac a) 

130 

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

132 
apply (tactic "tac 1") 

133 
apply (tactic "tac_ren 1") 

134 

135 
txt {* 5 + 1 *} 

136 

137 
apply (tactic "tac 1") 

138 
apply (tactic "tac_ren 1") 

139 

140 
txt {* 4 + 1 *} 

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

142 

143 

144 
txt {* Now the other half *} 

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

146 
apply (induct_tac a) 

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

148 

149 
txt {* detour 1 *} 

150 
apply (tactic "tac 1") 

151 
apply (tactic "tac_ren 1") 

152 
apply (rule impI) 

153 
apply (erule conjE)+ 

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

155 
split add: split_if) 

156 
txt {* detour 2 *} 

157 
apply (tactic "tac 1") 

158 
apply (tactic "tac_ren 1") 

159 
apply (rule impI) 

160 
apply (erule conjE)+ 

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

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

165 
apply (rule impI) 

166 
apply hypsubst 

167 
apply (rule pred_suc [THEN iffD1]) 

168 
apply (drule less_le_trans) 

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

170 
apply assumption 

171 
apply assumption 

172 

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

174 
apply (rule refl) 

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

176 

177 
apply (rule impI) 

178 
apply (simp add: neg_flip) 

179 
apply hypsubst 

180 
apply (rule countm_spurious_delm) 

181 
apply (simp (no_asm)) 

182 

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

184 

185 
done 

186 

187 

188 

189 
subsubsection {* INVARIANT 2 *} 

190 

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

193 
apply (rule invariantI1) 

194 
txt {* Base case *} 

195 
apply (simp add: inv2_def receiver_projections sender_projections impl_ioas) 

196 

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

198 
apply (induct_tac "a") 

199 

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

201 

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

204 
txt {* 10  7 *} 

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

206 
txt {* 6 *} 

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

19739  209 

210 
txt {* 6  5 *} 

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

212 

213 
txt {* 4 *} 

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

19739  216 
apply (tactic "tac2 1") 
217 

218 
txt {* 3 *} 

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

19739  221 

222 
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

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

227 
txt {* 2 *} 

228 
apply (tactic "tac2 1") 

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

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

233 
apply simp 

234 

235 
txt {* 1 *} 

236 
apply (tactic "tac2 1") 

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

19739  239 
apply (intro strip) 
240 
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

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

244 
done 

245 

246 

247 
subsubsection {* INVARIANT 3 *} 

248 

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

251 
apply (rule invariantI) 

252 
txt {* Base case *} 

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

254 

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

256 
apply (induct_tac "a") 

257 

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

260 
txt {* 10  8 *} 

261 

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

263 

264 
apply (tactic "tac_ren 1") 

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

266 
apply hypsubst 

267 
apply (erule exE) 

268 
apply simp 

269 

270 
txt {* 7 *} 

271 
apply (tactic "tac3 1") 

272 
apply (tactic "tac_ren 1") 

273 
apply force 

274 

275 
txt {* 6  3 *} 

276 

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

278 

279 
txt {* 2 *} 

280 
apply (tactic "asm_full_simp_tac ss 1") 

281 
apply (simp (no_asm) add: inv3_def) 

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

283 
apply (rule imp_disjL [THEN iffD1]) 

284 
apply (rule impI) 

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

19739  287 
apply simp 
288 
apply (erule conjE)+ 

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

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

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

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

295 
apply (rule countm_props) 

296 
apply (simp (no_asm)) 

297 
apply (rule countm_props) 

298 
apply (simp (no_asm)) 

299 
apply assumption 

300 

301 
txt {* 1 *} 

302 
apply (tactic "tac3 1") 

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

304 
apply (rule imp_disjL [THEN iffD1]) 

305 
apply (rule impI) 

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

19739  308 
apply simp 
309 
done 

310 

311 

312 
subsubsection {* INVARIANT 4 *} 

313 

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

316 
apply (rule invariantI) 

317 
txt {* Base case *} 

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

319 

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

321 
apply (induct_tac "a") 

322 

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

325 
txt {* 10  2 *} 

326 

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

328 

329 
txt {* 2 b *} 

330 

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

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

19739  334 
apply simp 
335 

336 
txt {* 1 *} 

337 
apply (tactic "tac4 1") 

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

339 
apply (rule ccontr) 

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

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

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

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

346 
apply simp 

347 
done 

348 

349 

350 
text {* rebind them *} 

351 

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

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

355 
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

356 

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

357 
end 