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