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