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