src/HOL/HOLCF/IOA/NTP/Impl.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35215 src/HOLCF/IOA/NTP/Impl.thy@a03462cbf86f
child 41476 0fa9629aa399
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOL/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 types '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} addsimps @{thms "transitions"};
   106 val rename_ss = ss addsimps @{thms unfold_renaming};
   107 
   108 val tac     = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
   109 val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
   110 *}
   111 
   112 
   113 subsubsection {* Invariant 1 *}
   114 
   115 lemma raw_inv1: "invariant impl_ioa inv1"
   116 
   117 apply (unfold impl_ioas)
   118 apply (rule invariantI)
   119 apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def)
   120 
   121 apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def)
   122 
   123 txt {* Split proof in two *}
   124 apply (rule conjI)
   125 
   126 (* First half *)
   127 apply (simp add: Impl.inv1_def split del: split_if)
   128 apply (induct_tac a)
   129 
   130 apply (tactic "EVERY1[tac, tac, tac, tac]")
   131 apply (tactic "tac 1")
   132 apply (tactic "tac_ren 1")
   133 
   134 txt {* 5 + 1 *}
   135 
   136 apply (tactic "tac 1")
   137 apply (tactic "tac_ren 1")
   138 
   139 txt {* 4 + 1 *}
   140 apply (tactic {* EVERY1[tac, tac, tac, tac] *})
   141 
   142 
   143 txt {* Now the other half *}
   144 apply (simp add: Impl.inv1_def split del: split_if)
   145 apply (induct_tac a)
   146 apply (tactic "EVERY1 [tac, tac]")
   147 
   148 txt {* detour 1 *}
   149 apply (tactic "tac 1")
   150 apply (tactic "tac_ren 1")
   151 apply (rule impI)
   152 apply (erule conjE)+
   153 apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
   154   split add: split_if)
   155 txt {* detour 2 *}
   156 apply (tactic "tac 1")
   157 apply (tactic "tac_ren 1")
   158 apply (rule impI)
   159 apply (erule conjE)+
   160 apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
   161   Multiset.delm_nonempty_def split add: split_if)
   162 apply (rule allI)
   163 apply (rule conjI)
   164 apply (rule impI)
   165 apply hypsubst
   166 apply (rule pred_suc [THEN iffD1])
   167 apply (drule less_le_trans)
   168 apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props])
   169 apply assumption
   170 apply assumption
   171 
   172 apply (rule countm_done_delm [THEN mp, symmetric])
   173 apply (rule refl)
   174 apply (simp (no_asm_simp) add: Multiset.count_def)
   175 
   176 apply (rule impI)
   177 apply (simp add: neg_flip)
   178 apply hypsubst
   179 apply (rule countm_spurious_delm)
   180 apply (simp (no_asm))
   181 
   182 apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]")
   183 
   184 done
   185 
   186 
   187 
   188 subsubsection {* INVARIANT 2 *}
   189 
   190 lemma raw_inv2: "invariant impl_ioa inv2"
   191 
   192   apply (rule invariantI1)
   193   txt {* Base case *}
   194   apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
   195 
   196   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   197   apply (induct_tac "a")
   198 
   199   txt {* 10 cases. First 4 are simple, since state doesn't change *}
   200 
   201   ML_prf {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
   202 
   203   txt {* 10 - 7 *}
   204   apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
   205   txt {* 6 *}
   206   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   207                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   208 
   209   txt {* 6 - 5 *}
   210   apply (tactic "EVERY1 [tac2,tac2]")
   211 
   212   txt {* 4 *}
   213   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   214                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   215   apply (tactic "tac2 1")
   216 
   217   txt {* 3 *}
   218   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   219     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
   220 
   221   apply (tactic "tac2 1")
   222   apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
   223     (@{thm Impl.hdr_sum_def})] *})
   224   apply arith
   225 
   226   txt {* 2 *}
   227   apply (tactic "tac2 1")
   228   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   229                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   230   apply (intro strip)
   231   apply (erule conjE)+
   232   apply simp
   233 
   234   txt {* 1 *}
   235   apply (tactic "tac2 1")
   236   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   237                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   238   apply (intro strip)
   239   apply (erule conjE)+
   240   apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   241   apply simp
   242 
   243   done
   244 
   245 
   246 subsubsection {* INVARIANT 3 *}
   247 
   248 lemma raw_inv3: "invariant impl_ioa inv3"
   249 
   250   apply (rule invariantI)
   251   txt {* Base case *}
   252   apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
   253 
   254   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   255   apply (induct_tac "a")
   256 
   257   ML_prf {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
   258 
   259   txt {* 10 - 8 *}
   260 
   261   apply (tactic "EVERY1[tac3,tac3,tac3]")
   262 
   263   apply (tactic "tac_ren 1")
   264   apply (intro strip, (erule conjE)+)
   265   apply hypsubst
   266   apply (erule exE)
   267   apply simp
   268 
   269   txt {* 7 *}
   270   apply (tactic "tac3 1")
   271   apply (tactic "tac_ren 1")
   272   apply force
   273 
   274   txt {* 6 - 3 *}
   275 
   276   apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
   277 
   278   txt {* 2 *}
   279   apply (tactic "asm_full_simp_tac ss 1")
   280   apply (simp (no_asm) add: inv3_def)
   281   apply (intro strip, (erule conjE)+)
   282   apply (rule imp_disjL [THEN iffD1])
   283   apply (rule impI)
   284   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   285     (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   286   apply simp
   287   apply (erule conjE)+
   288   apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
   289     k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
   290   apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
   291                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   292   apply (simp add: hdr_sum_def Multiset.count_def)
   293   apply (rule add_le_mono)
   294   apply (rule countm_props)
   295   apply (simp (no_asm))
   296   apply (rule countm_props)
   297   apply (simp (no_asm))
   298   apply assumption
   299 
   300   txt {* 1 *}
   301   apply (tactic "tac3 1")
   302   apply (intro strip, (erule conjE)+)
   303   apply (rule imp_disjL [THEN iffD1])
   304   apply (rule impI)
   305   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   306     (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   307   apply simp
   308   done
   309 
   310 
   311 subsubsection {* INVARIANT 4 *}
   312 
   313 lemma raw_inv4: "invariant impl_ioa inv4"
   314 
   315   apply (rule invariantI)
   316   txt {* Base case *}
   317   apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
   318 
   319   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   320   apply (induct_tac "a")
   321 
   322   ML_prf {* val tac4 =  asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
   323 
   324   txt {* 10 - 2 *}
   325 
   326   apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
   327 
   328   txt {* 2 b *}
   329 
   330   apply (intro strip, (erule conjE)+)
   331   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   332                                (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   333   apply simp
   334 
   335   txt {* 1 *}
   336   apply (tactic "tac4 1")
   337   apply (intro strip, (erule conjE)+)
   338   apply (rule ccontr)
   339   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   340                                (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   341   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
   342                                (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
   343   apply simp
   344   apply (erule_tac x = "m" in allE)
   345   apply simp
   346   done
   347 
   348 
   349 text {* rebind them *}
   350 
   351 lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def]
   352   and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def]
   353   and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def]
   354   and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def]
   355 
   356 end