author | huffman |
Wed, 17 Feb 2010 10:00:22 -0800 | |
changeset 35174 | e15040ae75d7 |
parent 28839 | 32d498cf7595 |
child 35215 | a03462cbf86f |
permissions | -rw-r--r-- |
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 well-formed 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 well-formed 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 |