1(* Title: HOL/HOLCF/IOA/NTP/Impl.thy 2 Author: Tobias Nipkow & Konrad Slind 3*) 4 5section \<open>The implementation\<close> 6 7theory Impl 8imports Sender Receiver Abschannel 9begin 10 11type_synonym 'm impl_state 12 = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" 13 (* sender_state * receiver_state * srch_state * rsch_state *) 14 15 16definition 17 impl_ioa :: "('m action, 'm impl_state)ioa" where 18 impl_def: "impl_ioa == (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)" 19 20definition sen :: "'m impl_state => 'm sender_state" where "sen = fst" 21definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst \<circ> snd" 22definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst \<circ> snd \<circ> snd" 23definition rsch :: "'m impl_state => bool multiset" where "rsch = snd \<circ> snd \<circ> snd" 24 25definition 26 hdr_sum :: "'m packet multiset => bool => nat" where 27 "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" 28 29(* Lemma 5.1 *) 30definition 31 "inv1(s) \<equiv> 32 (\<forall>b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) 33 \<and> (\<forall>b. count (ssent(sen s)) b 34 = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)" 35 36(* Lemma 5.2 *) 37definition 38 "inv2(s) == 39 (rbit(rec(s)) = sbit(sen(s)) & 40 ssending(sen(s)) & 41 count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) & 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)) & 46 count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) & 47 count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))" 48 49(* Lemma 5.3 *) 50definition 51 "inv3(s) \<equiv> 52 rbit(rec(s)) = sbit(sen(s)) 53 \<longrightarrow> (\<forall>m. sq(sen(s))=[] | m \<noteq> hd(sq(sen(s))) 54 \<longrightarrow> count (rrcvd(rec s)) (sbit(sen(s)),m) 55 + count (srch s) (sbit(sen(s)),m) 56 \<le> count (rsent(rec s)) (~sbit(sen s)))" 57 58(* Lemma 5.4 *) 59definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" 60 61 62subsection \<open>Invariants\<close> 63 64declare le_SucI [simp] 65 66lemmas 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 70lemmas "transitions" = 71 sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def 72 73 74lemmas [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 78declare let_weak_cong [cong] 79 80lemma [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 87lemma [simp]: 88 "a\<in>actions(sender_asig) 89 \<or> a\<in>actions(receiver_asig) 90 \<or> a\<in>actions(srch_asig) 91 \<or> a\<in>actions(rsch_asig)" 92 by (induct a) simp_all 93 94declare split_paired_All [simp del] 95 96 97(* Three Simp_sets in different sizes 98---------------------------------------------- 99 1001) simpset() does not unfold the transition relations 1012) ss unfolds transition relations 1023) renname_ss unfolds transitions and the abstract channel *) 103 104ML \<open> 105val ss = simpset_of (@{context} addsimps @{thms "transitions"}); 106val rename_ss = simpset_of (put_simpset ss @{context} addsimps @{thms unfold_renaming}); 107 108fun tac ctxt = 109 asm_simp_tac (put_simpset ss ctxt 110 |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm if_split}) 111fun tac_ren ctxt = 112 asm_simp_tac (put_simpset rename_ss ctxt 113 |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm if_split}) 114\<close> 115 116 117subsubsection \<open>Invariant 1\<close> 118 119lemma raw_inv1: "invariant impl_ioa inv1" 120 121apply (unfold impl_ioas) 122apply (rule invariantI) 123apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def) 124 125apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def) 126 127txt \<open>Split proof in two\<close> 128apply (rule conjI) 129 130(* First half *) 131apply (simp add: Impl.inv1_def split del: if_split) 132apply (induct_tac a) 133 134apply (tactic "EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]") 135apply (tactic "tac @{context} 1") 136apply (tactic "tac_ren @{context} 1") 137 138txt \<open>5 + 1\<close> 139 140apply (tactic "tac @{context} 1") 141apply (tactic "tac_ren @{context} 1") 142 143txt \<open>4 + 1\<close> 144apply (tactic \<open>EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]\<close>) 145 146 147txt \<open>Now the other half\<close> 148apply (simp add: Impl.inv1_def split del: if_split) 149apply (induct_tac a) 150apply (tactic "EVERY1 [tac @{context}, tac @{context}]") 151 152txt \<open>detour 1\<close> 153apply (tactic "tac @{context} 1") 154apply (tactic "tac_ren @{context} 1") 155apply (rule impI) 156apply (erule conjE)+ 157apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def 158 split: if_split) 159txt \<open>detour 2\<close> 160apply (tactic "tac @{context} 1") 161apply (tactic "tac_ren @{context} 1") 162apply (rule impI) 163apply (erule conjE)+ 164apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def 165 Multiset.delm_nonempty_def split: if_split) 166apply (rule allI) 167apply (rule conjI) 168apply (rule impI) 169apply hypsubst 170apply (rule pred_suc [THEN iffD1]) 171apply (drule less_le_trans) 172apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props]) 173apply assumption 174apply assumption 175 176apply (rule countm_done_delm [THEN mp, symmetric]) 177apply (rule refl) 178apply (simp (no_asm_simp) add: Multiset.count_def) 179 180apply (rule impI) 181apply (simp add: neg_flip) 182apply hypsubst 183apply (rule countm_spurious_delm) 184apply (simp (no_asm)) 185 186apply (tactic "EVERY1 [tac @{context}, tac @{context}, tac @{context}, 187 tac @{context}, tac @{context}, tac @{context}]") 188 189done 190 191 192 193subsubsection \<open>INVARIANT 2\<close> 194 195lemma raw_inv2: "invariant impl_ioa inv2" 196 197 apply (rule invariantI1) 198 txt \<open>Base case\<close> 199 apply (simp add: inv2_def receiver_projections sender_projections impl_ioas) 200 201 apply (simp (no_asm_simp) add: impl_ioas split del: if_split) 202 apply (induct_tac "a") 203 204 txt \<open>10 cases. First 4 are simple, since state doesn't change\<close> 205 206 ML_prf \<open>val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}])\<close> 207 208 txt \<open>10 - 7\<close> 209 apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]") 210 txt \<open>6\<close> 211 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] 212 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>) 213 214 txt \<open>6 - 5\<close> 215 apply (tactic "EVERY1 [tac2,tac2]") 216 217 txt \<open>4\<close> 218 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] 219 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>) 220 apply (tactic "tac2 1") 221 222 txt \<open>3\<close> 223 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] 224 (@{thm raw_inv1} RS @{thm invariantE})] 1\<close>) 225 226 apply (tactic "tac2 1") 227 apply (tactic \<open>fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}] 228 (@{thm Impl.hdr_sum_def})]\<close>) 229 apply arith 230 231 txt \<open>2\<close> 232 apply (tactic "tac2 1") 233 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] 234 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>) 235 apply (intro strip) 236 apply (erule conjE)+ 237 apply simp 238 239 txt \<open>1\<close> 240 apply (tactic "tac2 1") 241 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] 242 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>) 243 apply (intro strip) 244 apply (erule conjE)+ 245 apply (tactic \<open>fold_goals_tac @{context} 246 [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})]\<close>) 247 apply simp 248 249 done 250 251 252subsubsection \<open>INVARIANT 3\<close> 253 254lemma raw_inv3: "invariant impl_ioa inv3" 255 256 apply (rule invariantI) 257 txt \<open>Base case\<close> 258 apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas) 259 260 apply (simp (no_asm_simp) add: impl_ioas split del: if_split) 261 apply (induct_tac "a") 262 263 ML_prf \<open>val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}])\<close> 264 265 txt \<open>10 - 8\<close> 266 267 apply (tactic "EVERY1[tac3,tac3,tac3]") 268 269 apply (tactic "tac_ren @{context} 1") 270 apply (intro strip, (erule conjE)+) 271 apply hypsubst 272 apply (erule exE) 273 apply simp 274 275 txt \<open>7\<close> 276 apply (tactic "tac3 1") 277 apply (tactic "tac_ren @{context} 1") 278 apply force 279 280 txt \<open>6 - 3\<close> 281 282 apply (tactic "EVERY1[tac3,tac3,tac3,tac3]") 283 284 txt \<open>2\<close> 285 apply (tactic "asm_full_simp_tac (put_simpset ss @{context}) 1") 286 apply (simp (no_asm) add: inv3_def) 287 apply (intro strip, (erule conjE)+) 288 apply (rule imp_disjL [THEN iffD1]) 289 apply (rule impI) 290 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] 291 (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) 292 apply simp 293 apply (erule conjE)+ 294 apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and 295 k = "count (rsent (rec s)) (sbit (sen s))" in le_trans) 296 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm inv1_def}] 297 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>) 298 apply (simp add: hdr_sum_def Multiset.count_def) 299 apply (rule add_le_mono) 300 apply (rule countm_props) 301 apply (simp (no_asm)) 302 apply (rule countm_props) 303 apply (simp (no_asm)) 304 apply assumption 305 306 txt \<open>1\<close> 307 apply (tactic "tac3 1") 308 apply (intro strip, (erule conjE)+) 309 apply (rule imp_disjL [THEN iffD1]) 310 apply (rule impI) 311 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] 312 (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) 313 apply simp 314 done 315 316 317subsubsection \<open>INVARIANT 4\<close> 318 319lemma raw_inv4: "invariant impl_ioa inv4" 320 321 apply (rule invariantI) 322 txt \<open>Base case\<close> 323 apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas) 324 325 apply (simp (no_asm_simp) add: impl_ioas split del: if_split) 326 apply (induct_tac "a") 327 328 ML_prf \<open>val tac4 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}])\<close> 329 330 txt \<open>10 - 2\<close> 331 332 apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]") 333 334 txt \<open>2 b\<close> 335 336 apply (intro strip, (erule conjE)+) 337 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] 338 (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) 339 apply simp 340 341 txt \<open>1\<close> 342 apply (tactic "tac4 1") 343 apply (intro strip, (erule conjE)+) 344 apply (rule ccontr) 345 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] 346 (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) 347 apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv3_def}] 348 (@{thm raw_inv3} RS @{thm invariantE})] 1\<close>) 349 apply simp 350 apply (rename_tac m, erule_tac x = "m" in allE) 351 apply simp 352 done 353 354 355text \<open>rebind them\<close> 356 357lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def] 358 and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def] 359 and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def] 360 and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def] 361 362end 363