src/HOLCF/IOA/NTP/Impl.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/IOA/NTP/Impl.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,356 +0,0 @@
     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