src/HOL/HOLCF/IOA/NTP/Impl.thy
changeset 40774 0437dbc127b3
parent 35215 a03462cbf86f
child 41476 0fa9629aa399
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,356 @@
     1.4 +(*  Title:      HOL/IOA/NTP/Impl.thy
     1.5 +    Author:     Tobias Nipkow & Konrad Slind
     1.6 +*)
     1.7 +
     1.8 +header {* The implementation *}
     1.9 +
    1.10 +theory Impl
    1.11 +imports Sender Receiver Abschannel
    1.12 +begin
    1.13 +
    1.14 +types 'm impl_state
    1.15 +  = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
    1.16 +  (*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
    1.17 +
    1.18 +
    1.19 +definition
    1.20 +  impl_ioa :: "('m action, 'm impl_state)ioa" where
    1.21 +  impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
    1.22 +
    1.23 +definition sen :: "'m impl_state => 'm sender_state" where "sen = fst"
    1.24 +definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd"
    1.25 +definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd"
    1.26 +definition rsch :: "'m impl_state => bool multiset" where "rsch = snd o snd o snd"
    1.27 +
    1.28 +definition
    1.29 +  hdr_sum :: "'m packet multiset => bool => nat" where
    1.30 +  "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
    1.31 +
    1.32 +(* Lemma 5.1 *)
    1.33 +definition
    1.34 +  "inv1(s) ==
    1.35 +     (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
    1.36 +   & (!b. count (ssent(sen s)) b
    1.37 +          = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
    1.38 +
    1.39 +(* Lemma 5.2 *)
    1.40 +definition
    1.41 +  "inv2(s) ==
    1.42 +  (rbit(rec(s)) = sbit(sen(s)) &
    1.43 +   ssending(sen(s)) &
    1.44 +   count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
    1.45 +   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))
    1.46 +   |
    1.47 +  (rbit(rec(s)) = (~sbit(sen(s))) &
    1.48 +   rsending(rec(s)) &
    1.49 +   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
    1.50 +   count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
    1.51 +
    1.52 +(* Lemma 5.3 *)
    1.53 +definition
    1.54 +  "inv3(s) ==
    1.55 +   rbit(rec(s)) = sbit(sen(s))
    1.56 +   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
    1.57 +        -->  count (rrcvd(rec s)) (sbit(sen(s)),m)
    1.58 +             + count (srch s) (sbit(sen(s)),m)
    1.59 +            <= count (rsent(rec s)) (~sbit(sen s)))"
    1.60 +
    1.61 +(* Lemma 5.4 *)
    1.62 +definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
    1.63 +
    1.64 +
    1.65 +subsection {* Invariants *}
    1.66 +
    1.67 +declare le_SucI [simp]
    1.68 +
    1.69 +lemmas impl_ioas =
    1.70 +  impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection]
    1.71 +  rsch_ioa_thm [THEN eq_reflection]
    1.72 +
    1.73 +lemmas "transitions" =
    1.74 +  sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def
    1.75 +
    1.76 +
    1.77 +lemmas [simp] =
    1.78 +  ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig
    1.79 +  in_receiver_asig in_srch_asig in_rsch_asig
    1.80 +
    1.81 +declare let_weak_cong [cong]
    1.82 +
    1.83 +lemma [simp]:
    1.84 +  "fst(x) = sen(x)"
    1.85 +  "fst(snd(x)) = rec(x)"
    1.86 +  "fst(snd(snd(x))) = srch(x)"
    1.87 +  "snd(snd(snd(x))) = rsch(x)"
    1.88 +  by (simp_all add: sen_def rec_def srch_def rsch_def)
    1.89 +
    1.90 +lemma [simp]:
    1.91 +  "a:actions(sender_asig)
    1.92 +  | a:actions(receiver_asig)
    1.93 +  | a:actions(srch_asig)
    1.94 +  | a:actions(rsch_asig)"
    1.95 +  by (induct a) simp_all
    1.96 +
    1.97 +declare split_paired_All [simp del]
    1.98 +
    1.99 +
   1.100 +(* Three Simp_sets in different sizes
   1.101 +----------------------------------------------
   1.102 +
   1.103 +1) simpset() does not unfold the transition relations
   1.104 +2) ss unfolds transition relations
   1.105 +3) renname_ss unfolds transitions and the abstract channel *)
   1.106 +
   1.107 +ML {*
   1.108 +val ss = @{simpset} addsimps @{thms "transitions"};
   1.109 +val rename_ss = ss addsimps @{thms unfold_renaming};
   1.110 +
   1.111 +val tac     = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
   1.112 +val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
   1.113 +*}
   1.114 +
   1.115 +
   1.116 +subsubsection {* Invariant 1 *}
   1.117 +
   1.118 +lemma raw_inv1: "invariant impl_ioa inv1"
   1.119 +
   1.120 +apply (unfold impl_ioas)
   1.121 +apply (rule invariantI)
   1.122 +apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def)
   1.123 +
   1.124 +apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def)
   1.125 +
   1.126 +txt {* Split proof in two *}
   1.127 +apply (rule conjI)
   1.128 +
   1.129 +(* First half *)
   1.130 +apply (simp add: Impl.inv1_def split del: split_if)
   1.131 +apply (induct_tac a)
   1.132 +
   1.133 +apply (tactic "EVERY1[tac, tac, tac, tac]")
   1.134 +apply (tactic "tac 1")
   1.135 +apply (tactic "tac_ren 1")
   1.136 +
   1.137 +txt {* 5 + 1 *}
   1.138 +
   1.139 +apply (tactic "tac 1")
   1.140 +apply (tactic "tac_ren 1")
   1.141 +
   1.142 +txt {* 4 + 1 *}
   1.143 +apply (tactic {* EVERY1[tac, tac, tac, tac] *})
   1.144 +
   1.145 +
   1.146 +txt {* Now the other half *}
   1.147 +apply (simp add: Impl.inv1_def split del: split_if)
   1.148 +apply (induct_tac a)
   1.149 +apply (tactic "EVERY1 [tac, tac]")
   1.150 +
   1.151 +txt {* detour 1 *}
   1.152 +apply (tactic "tac 1")
   1.153 +apply (tactic "tac_ren 1")
   1.154 +apply (rule impI)
   1.155 +apply (erule conjE)+
   1.156 +apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
   1.157 +  split add: split_if)
   1.158 +txt {* detour 2 *}
   1.159 +apply (tactic "tac 1")
   1.160 +apply (tactic "tac_ren 1")
   1.161 +apply (rule impI)
   1.162 +apply (erule conjE)+
   1.163 +apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
   1.164 +  Multiset.delm_nonempty_def split add: split_if)
   1.165 +apply (rule allI)
   1.166 +apply (rule conjI)
   1.167 +apply (rule impI)
   1.168 +apply hypsubst
   1.169 +apply (rule pred_suc [THEN iffD1])
   1.170 +apply (drule less_le_trans)
   1.171 +apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props])
   1.172 +apply assumption
   1.173 +apply assumption
   1.174 +
   1.175 +apply (rule countm_done_delm [THEN mp, symmetric])
   1.176 +apply (rule refl)
   1.177 +apply (simp (no_asm_simp) add: Multiset.count_def)
   1.178 +
   1.179 +apply (rule impI)
   1.180 +apply (simp add: neg_flip)
   1.181 +apply hypsubst
   1.182 +apply (rule countm_spurious_delm)
   1.183 +apply (simp (no_asm))
   1.184 +
   1.185 +apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]")
   1.186 +
   1.187 +done
   1.188 +
   1.189 +
   1.190 +
   1.191 +subsubsection {* INVARIANT 2 *}
   1.192 +
   1.193 +lemma raw_inv2: "invariant impl_ioa inv2"
   1.194 +
   1.195 +  apply (rule invariantI1)
   1.196 +  txt {* Base case *}
   1.197 +  apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
   1.198 +
   1.199 +  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   1.200 +  apply (induct_tac "a")
   1.201 +
   1.202 +  txt {* 10 cases. First 4 are simple, since state doesn't change *}
   1.203 +
   1.204 +  ML_prf {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
   1.205 +
   1.206 +  txt {* 10 - 7 *}
   1.207 +  apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
   1.208 +  txt {* 6 *}
   1.209 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   1.210 +                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   1.211 +
   1.212 +  txt {* 6 - 5 *}
   1.213 +  apply (tactic "EVERY1 [tac2,tac2]")
   1.214 +
   1.215 +  txt {* 4 *}
   1.216 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   1.217 +                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   1.218 +  apply (tactic "tac2 1")
   1.219 +
   1.220 +  txt {* 3 *}
   1.221 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   1.222 +    (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
   1.223 +
   1.224 +  apply (tactic "tac2 1")
   1.225 +  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
   1.226 +    (@{thm Impl.hdr_sum_def})] *})
   1.227 +  apply arith
   1.228 +
   1.229 +  txt {* 2 *}
   1.230 +  apply (tactic "tac2 1")
   1.231 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   1.232 +                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   1.233 +  apply (intro strip)
   1.234 +  apply (erule conjE)+
   1.235 +  apply simp
   1.236 +
   1.237 +  txt {* 1 *}
   1.238 +  apply (tactic "tac2 1")
   1.239 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   1.240 +                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   1.241 +  apply (intro strip)
   1.242 +  apply (erule conjE)+
   1.243 +  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   1.244 +  apply simp
   1.245 +
   1.246 +  done
   1.247 +
   1.248 +
   1.249 +subsubsection {* INVARIANT 3 *}
   1.250 +
   1.251 +lemma raw_inv3: "invariant impl_ioa inv3"
   1.252 +
   1.253 +  apply (rule invariantI)
   1.254 +  txt {* Base case *}
   1.255 +  apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
   1.256 +
   1.257 +  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   1.258 +  apply (induct_tac "a")
   1.259 +
   1.260 +  ML_prf {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
   1.261 +
   1.262 +  txt {* 10 - 8 *}
   1.263 +
   1.264 +  apply (tactic "EVERY1[tac3,tac3,tac3]")
   1.265 +
   1.266 +  apply (tactic "tac_ren 1")
   1.267 +  apply (intro strip, (erule conjE)+)
   1.268 +  apply hypsubst
   1.269 +  apply (erule exE)
   1.270 +  apply simp
   1.271 +
   1.272 +  txt {* 7 *}
   1.273 +  apply (tactic "tac3 1")
   1.274 +  apply (tactic "tac_ren 1")
   1.275 +  apply force
   1.276 +
   1.277 +  txt {* 6 - 3 *}
   1.278 +
   1.279 +  apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
   1.280 +
   1.281 +  txt {* 2 *}
   1.282 +  apply (tactic "asm_full_simp_tac ss 1")
   1.283 +  apply (simp (no_asm) add: inv3_def)
   1.284 +  apply (intro strip, (erule conjE)+)
   1.285 +  apply (rule imp_disjL [THEN iffD1])
   1.286 +  apply (rule impI)
   1.287 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   1.288 +    (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   1.289 +  apply simp
   1.290 +  apply (erule conjE)+
   1.291 +  apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
   1.292 +    k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
   1.293 +  apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
   1.294 +                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   1.295 +  apply (simp add: hdr_sum_def Multiset.count_def)
   1.296 +  apply (rule add_le_mono)
   1.297 +  apply (rule countm_props)
   1.298 +  apply (simp (no_asm))
   1.299 +  apply (rule countm_props)
   1.300 +  apply (simp (no_asm))
   1.301 +  apply assumption
   1.302 +
   1.303 +  txt {* 1 *}
   1.304 +  apply (tactic "tac3 1")
   1.305 +  apply (intro strip, (erule conjE)+)
   1.306 +  apply (rule imp_disjL [THEN iffD1])
   1.307 +  apply (rule impI)
   1.308 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   1.309 +    (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   1.310 +  apply simp
   1.311 +  done
   1.312 +
   1.313 +
   1.314 +subsubsection {* INVARIANT 4 *}
   1.315 +
   1.316 +lemma raw_inv4: "invariant impl_ioa inv4"
   1.317 +
   1.318 +  apply (rule invariantI)
   1.319 +  txt {* Base case *}
   1.320 +  apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
   1.321 +
   1.322 +  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   1.323 +  apply (induct_tac "a")
   1.324 +
   1.325 +  ML_prf {* val tac4 =  asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
   1.326 +
   1.327 +  txt {* 10 - 2 *}
   1.328 +
   1.329 +  apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
   1.330 +
   1.331 +  txt {* 2 b *}
   1.332 +
   1.333 +  apply (intro strip, (erule conjE)+)
   1.334 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   1.335 +                               (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   1.336 +  apply simp
   1.337 +
   1.338 +  txt {* 1 *}
   1.339 +  apply (tactic "tac4 1")
   1.340 +  apply (intro strip, (erule conjE)+)
   1.341 +  apply (rule ccontr)
   1.342 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   1.343 +                               (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   1.344 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
   1.345 +                               (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
   1.346 +  apply simp
   1.347 +  apply (erule_tac x = "m" in allE)
   1.348 +  apply simp
   1.349 +  done
   1.350 +
   1.351 +
   1.352 +text {* rebind them *}
   1.353 +
   1.354 +lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def]
   1.355 +  and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def]
   1.356 +  and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def]
   1.357 +  and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def]
   1.358 +
   1.359 +end