author | wenzelm |
Sat, 29 Mar 2008 19:14:05 +0100 | |
changeset 26483 | b8f62618ad0a |
parent 26305 | 651371f29e00 |
child 27355 | a9d738d20174 |
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 |
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 {* |
|
26305 | 115 |
val ss = @{simpset} addsimps @{thms transitions}; |
116 |
val rename_ss = ss addsimps @{thms unfold_renaming}; |
|
19739 | 117 |
|
26305 | 118 |
val tac = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}]) |
119 |
val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}]) |
|
19739 | 120 |
*} |
121 |
||
122 |
||
123 |
subsubsection {* Invariant 1 *} |
|
124 |
||
26305 | 125 |
lemma raw_inv1: "invariant impl_ioa inv1" |
19739 | 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 |
|
25161 | 171 |
Multiset.delm_nonempty_def split add: split_if) |
19739 | 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 |
||
26305 | 200 |
lemma raw_inv2: "invariant impl_ioa inv2" |
19739 | 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 |
||
26483 | 211 |
ML_command {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *} |
19739 | 212 |
|
213 |
txt {* 10 - 7 *} |
|
214 |
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]") |
|
215 |
txt {* 6 *} |
|
26305 | 216 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] |
217 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *}) |
|
19739 | 218 |
|
219 |
txt {* 6 - 5 *} |
|
220 |
apply (tactic "EVERY1 [tac2,tac2]") |
|
221 |
||
222 |
txt {* 4 *} |
|
26305 | 223 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] |
224 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *}) |
|
19739 | 225 |
apply (tactic "tac2 1") |
226 |
||
227 |
txt {* 3 *} |
|
26305 | 228 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] |
229 |
(@{thm raw_inv1} RS @{thm invariantE})] 1 *}) |
|
19739 | 230 |
|
231 |
apply (tactic "tac2 1") |
|
26305 | 232 |
apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) |
19739 | 233 |
apply arith |
234 |
||
235 |
txt {* 2 *} |
|
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 conjunct1] 1 *}) |
|
19739 | 239 |
apply (intro strip) |
240 |
apply (erule conjE)+ |
|
241 |
apply simp |
|
242 |
||
243 |
txt {* 1 *} |
|
244 |
apply (tactic "tac2 1") |
|
26305 | 245 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}] |
246 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *}) |
|
19739 | 247 |
apply (intro strip) |
248 |
apply (erule conjE)+ |
|
26305 | 249 |
apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *}) |
19739 | 250 |
apply simp |
251 |
||
252 |
done |
|
253 |
||
254 |
||
255 |
subsubsection {* INVARIANT 3 *} |
|
256 |
||
26305 | 257 |
lemma raw_inv3: "invariant impl_ioa inv3" |
19739 | 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 |
||
26483 | 266 |
ML_command {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *} |
19739 | 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) |
|
26305 | 293 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] |
294 |
(@{thm raw_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) |
|
26305 | 299 |
apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}] |
300 |
(@{thm raw_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) |
|
26305 | 314 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] |
315 |
(@{thm raw_inv2} RS @{thm invariantE})] 1 *}) |
|
19739 | 316 |
apply simp |
317 |
done |
|
318 |
||
319 |
||
320 |
subsubsection {* INVARIANT 4 *} |
|
321 |
||
26305 | 322 |
lemma raw_inv4: "invariant impl_ioa inv4" |
19739 | 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 |
||
26483 | 331 |
ML_command {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *} |
19739 | 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)+) |
|
26305 | 340 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] |
341 |
(@{thm raw_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) |
|
26305 | 348 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}] |
349 |
(@{thm raw_inv2} RS @{thm invariantE})] 1 *}) |
|
350 |
apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}] |
|
351 |
(@{thm raw_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 |
||
26305 | 360 |
lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def] |
361 |
and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def] |
|
362 |
and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def] |
|
363 |
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
|
364 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
365 |
end |