src/HOL/TLA/Memory/MemoryImplementation.thy
author wenzelm
Tue Jun 10 16:43:14 2008 +0200 (2008-06-10)
changeset 27117 97e9dae57284
parent 27100 889613625e2b
child 27208 5fe899199f85
permissions -rw-r--r--
case_split_tac (works without context);
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        MemoryImplementation.thy
wenzelm@17309
     3
    ID:          $Id$
wenzelm@3807
     4
    Author:      Stephan Merz
wenzelm@3807
     5
    Copyright:   1997 University of Munich
wenzelm@21624
     6
*)
wenzelm@3807
     7
wenzelm@21624
     8
header {* RPC-Memory example: Memory implementation *}
wenzelm@3807
     9
wenzelm@17309
    10
theory MemoryImplementation
wenzelm@17309
    11
imports Memory RPC MemClerk
wenzelm@17309
    12
begin
wenzelm@6255
    13
wenzelm@17309
    14
datatype histState = histA | histB
wenzelm@3807
    15
wenzelm@3807
    16
types
wenzelm@3807
    17
  histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
wenzelm@3807
    18
wenzelm@3807
    19
consts
wenzelm@3807
    20
  (* the specification *)
wenzelm@3807
    21
     (* channel (external) *)
wenzelm@3807
    22
  memCh         :: "memChType"
wenzelm@3807
    23
     (* internal variables *)
wenzelm@6255
    24
  mm            :: "memType"
wenzelm@17309
    25
wenzelm@3807
    26
  (* the state variables of the implementation *)
wenzelm@3807
    27
     (* channels *)
wenzelm@3807
    28
  (* same interface channel memCh *)
wenzelm@3807
    29
  crCh          :: "rpcSndChType"
wenzelm@3807
    30
  rmCh          :: "rpcRcvChType"
wenzelm@3807
    31
     (* internal variables *)
wenzelm@6255
    32
  (* identity refinement mapping for mm -- simply reused *)
wenzelm@3807
    33
  rst           :: "rpcStType"
wenzelm@3807
    34
  cst           :: "mClkStType"
wenzelm@3807
    35
  ires          :: "resType"
wenzelm@3807
    36
wenzelm@6255
    37
constdefs
wenzelm@6255
    38
  (* auxiliary predicates *)
wenzelm@6255
    39
  MVOKBARF      :: "Vals => bool"
wenzelm@6255
    40
     "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
wenzelm@6255
    41
  MVOKBA        :: "Vals => bool"
wenzelm@6255
    42
     "MVOKBA v   == (v : MemVal) | (v = OK) | (v = BadArg)"
wenzelm@6255
    43
  MVNROKBA      :: "Vals => bool"
wenzelm@6255
    44
     "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
wenzelm@6255
    45
wenzelm@6255
    46
  (* tuples of state functions changed by the various components *)
wenzelm@6255
    47
  e             :: "PrIds => (bit * memOp) stfun"
wenzelm@6255
    48
     "e p == PRED (caller memCh!p)"
wenzelm@6255
    49
  c             :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
wenzelm@6255
    50
     "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
wenzelm@6255
    51
  r             :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
wenzelm@6255
    52
     "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
wenzelm@6255
    53
  m             :: "PrIds => ((bit * Vals) * Vals) stfun"
wenzelm@6255
    54
     "m p == PRED (rtrner rmCh!p, ires!p)"
wenzelm@6255
    55
wenzelm@3807
    56
  (* the environment action *)
wenzelm@3807
    57
  ENext         :: "PrIds => action"
wenzelm@6255
    58
     "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
wenzelm@6255
    59
wenzelm@3807
    60
wenzelm@3807
    61
  (* specification of the history variable *)
wenzelm@3807
    62
  HInit         :: "histType => PrIds => stpred"
wenzelm@6255
    63
     "HInit rmhist p == PRED rmhist!p = #histA"
wenzelm@6255
    64
wenzelm@3807
    65
  HNext         :: "histType => PrIds => action"
wenzelm@6255
    66
     "HNext rmhist p == ACT (rmhist!p)$ =
wenzelm@6255
    67
                     (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
wenzelm@6255
    68
                      then #histB
wenzelm@6255
    69
                      else if (MClkReply memCh crCh cst p)
wenzelm@6255
    70
                           then #histA
wenzelm@6255
    71
                           else $(rmhist!p))"
wenzelm@6255
    72
wenzelm@3807
    73
  HistP         :: "histType => PrIds => temporal"
wenzelm@6255
    74
     "HistP rmhist p == TEMP Init HInit rmhist p
wenzelm@6255
    75
                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"
wenzelm@6255
    76
wenzelm@3807
    77
  Hist          :: "histType => temporal"
wenzelm@9517
    78
      "Hist rmhist == TEMP (ALL p. HistP rmhist p)"
wenzelm@3807
    79
wenzelm@3807
    80
  (* the implementation *)
wenzelm@6255
    81
  IPImp          :: "PrIds => temporal"
wenzelm@6255
    82
     "IPImp p == TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
wenzelm@17309
    83
                       & MClkIPSpec memCh crCh cst p
wenzelm@17309
    84
                       & RPCIPSpec crCh rmCh rst p
wenzelm@17309
    85
                       & RPSpec rmCh mm ires p
wenzelm@17309
    86
                       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"
wenzelm@6255
    87
wenzelm@3807
    88
  ImpInit        :: "PrIds => stpred"
wenzelm@6255
    89
      "ImpInit p == PRED (  ~Calling memCh p
wenzelm@6255
    90
                          & MClkInit crCh cst p
wenzelm@17309
    91
                          & RPCInit rmCh rst p
wenzelm@17309
    92
                          & PInit ires p)"
wenzelm@6255
    93
wenzelm@3807
    94
  ImpNext        :: "PrIds => action"
wenzelm@17309
    95
      "ImpNext p == ACT  [ENext p]_(e p)
wenzelm@6255
    96
                       & [MClkNext memCh crCh cst p]_(c p)
wenzelm@17309
    97
                       & [RPCNext crCh rmCh rst p]_(r p)
wenzelm@6255
    98
                       & [RNext rmCh mm ires p]_(m p)"
wenzelm@6255
    99
wenzelm@3807
   100
  ImpLive        :: "PrIds => temporal"
wenzelm@17309
   101
      "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
wenzelm@17309
   102
                        & SF(MClkReply memCh crCh cst p)_(c p)
wenzelm@17309
   103
                        & WF(RPCNext crCh rmCh rst p)_(r p)
wenzelm@17309
   104
                        & WF(RNext rmCh mm ires p)_(m p)
wenzelm@17309
   105
                        & WF(MemReturn rmCh ires p)_(m p)"
wenzelm@6255
   106
wenzelm@3807
   107
  Implementation :: "temporal"
wenzelm@9517
   108
      "Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
wenzelm@6255
   109
                               & MClkISpec memCh crCh cst
wenzelm@6255
   110
                               & RPCISpec crCh rmCh rst
wenzelm@6255
   111
                               & IRSpec rmCh mm ires)"
wenzelm@3807
   112
wenzelm@3807
   113
  (* the predicate S describes the states of the implementation.
wenzelm@6255
   114
     slight simplification: two "histState" parameters instead of a
wenzelm@6255
   115
     (one- or two-element) set.
wenzelm@6255
   116
     NB: The second conjunct of the definition in the paper is taken care of by
wenzelm@6255
   117
     the type definitions. The last conjunct is asserted separately as the memory
wenzelm@24180
   118
     invariant MemInv, proved in Memory.thy. *)
wenzelm@6255
   119
  S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
wenzelm@6255
   120
      "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
wenzelm@6255
   121
                Calling memCh p = #ecalling
wenzelm@6255
   122
              & Calling crCh p  = #ccalling
wenzelm@6255
   123
              & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
wenzelm@6255
   124
              & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
wenzelm@6255
   125
              & Calling rmCh p  = #rcalling
wenzelm@6255
   126
              & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
wenzelm@6255
   127
              & (~ #rcalling --> ires!p = #NotAResult)
wenzelm@6255
   128
              & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
wenzelm@6255
   129
              & cst!p = #cs
wenzelm@6255
   130
              & rst!p = #rs
wenzelm@6255
   131
              & (rmhist!p = #hs1 | rmhist!p = #hs2)
wenzelm@6255
   132
              & MVNROKBA<ires!p>"
wenzelm@3807
   133
wenzelm@3807
   134
  (* predicates S1 -- S6 define special instances of S *)
wenzelm@3807
   135
  S1            :: "histType => PrIds => stpred"
wenzelm@6255
   136
      "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
wenzelm@3807
   137
  S2            :: "histType => PrIds => stpred"
wenzelm@6255
   138
      "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
wenzelm@3807
   139
  S3            :: "histType => PrIds => stpred"
wenzelm@6255
   140
      "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
wenzelm@3807
   141
  S4            :: "histType => PrIds => stpred"
wenzelm@6255
   142
      "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
wenzelm@3807
   143
  S5            :: "histType => PrIds => stpred"
wenzelm@6255
   144
      "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
wenzelm@3807
   145
  S6            :: "histType => PrIds => stpred"
wenzelm@6255
   146
      "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"
wenzelm@3807
   147
wenzelm@6255
   148
  (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
wenzelm@6255
   149
  ImpInv         :: "histType => PrIds => stpred"
wenzelm@6255
   150
      "ImpInv rmhist p == PRED (  S1 rmhist p | S2 rmhist p | S3 rmhist p
wenzelm@17309
   151
                                | S4 rmhist p | S5 rmhist p | S6 rmhist p)"
wenzelm@6255
   152
wenzelm@6255
   153
  resbar        :: "histType => resType"        (* refinement mapping *)
wenzelm@17309
   154
      "resbar rmhist s p ==
wenzelm@6255
   155
                  (if (S1 rmhist p s | S2 rmhist p s)
wenzelm@6255
   156
                   then ires s p
wenzelm@6255
   157
                   else if S3 rmhist p s
wenzelm@17309
   158
                   then if rmhist s p = histA
wenzelm@6255
   159
                        then ires s p else MemFailure
wenzelm@6255
   160
                   else if S4 rmhist p s
wenzelm@6255
   161
                   then if (rmhist s p = histB & ires s p = NotAResult)
wenzelm@6255
   162
                        then MemFailure else ires s p
wenzelm@6255
   163
                   else if S5 rmhist p s
wenzelm@6255
   164
                   then res (rmCh s p)
wenzelm@6255
   165
                   else if S6 rmhist p s
wenzelm@6255
   166
                   then if res (crCh s p) = RPCFailure
wenzelm@6255
   167
                        then MemFailure else res (crCh s p)
wenzelm@6255
   168
                   else NotAResult)" (* dummy value *)
wenzelm@3807
   169
wenzelm@17309
   170
axioms
wenzelm@3807
   171
  (* the "base" variables: everything except resbar and hist (for any index) *)
wenzelm@17309
   172
  MI_base:       "basevars (caller memCh!p,
wenzelm@17309
   173
                           (rtrner memCh!p, caller crCh!p, cst!p),
wenzelm@17309
   174
                           (rtrner crCh!p, caller rmCh!p, rst!p),
wenzelm@17309
   175
                           (mm!l, rtrner rmCh!p, ires!p))"
wenzelm@17309
   176
wenzelm@21624
   177
(*
wenzelm@21624
   178
    The main theorem is theorem "Implementation" at the end of this file,
wenzelm@21624
   179
    which shows that the composition of a reliable memory, an RPC component, and
wenzelm@24180
   180
    a memory clerk implements an unreliable memory. The files "MIsafe.thy" and
wenzelm@24180
   181
    "MIlive.thy" contain lower-level lemmas for the safety and liveness parts.
wenzelm@21624
   182
wenzelm@21624
   183
    Steps are (roughly) numbered as in the hand proof.
wenzelm@21624
   184
*)
wenzelm@21624
   185
wenzelm@21624
   186
(* --------------------------- automatic prover --------------------------- *)
wenzelm@21624
   187
wenzelm@21624
   188
declare if_weak_cong [cong del]
wenzelm@21624
   189
wenzelm@24180
   190
ML {* val MI_css = (@{claset}, @{simpset}) *}
wenzelm@21624
   191
wenzelm@21624
   192
(* A more aggressive variant that tries to solve subgoals by assumption
wenzelm@21624
   193
   or contradiction during the simplification.
wenzelm@21624
   194
   THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
wenzelm@21624
   195
   (but it can be a lot faster than MI_css)
wenzelm@21624
   196
*)
wenzelm@21624
   197
wenzelm@21624
   198
ML {*
wenzelm@21624
   199
val MI_fast_css =
wenzelm@21624
   200
  let
wenzelm@21624
   201
    val (cs,ss) = MI_css
wenzelm@21624
   202
  in
wenzelm@24180
   203
    (cs addSEs [temp_use @{thm squareE}],
wenzelm@21624
   204
      ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
wenzelm@21624
   205
  end;
wenzelm@21624
   206
wenzelm@21624
   207
val temp_elim = make_elim o temp_use;
wenzelm@21624
   208
*}
wenzelm@21624
   209
wenzelm@21624
   210
wenzelm@21624
   211
wenzelm@21624
   212
(****************************** The history variable ******************************)
wenzelm@21624
   213
wenzelm@21624
   214
section "History variable"
wenzelm@21624
   215
wenzelm@21624
   216
lemma HistoryLemma: "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p)
wenzelm@21624
   217
         --> (EEX rmhist. Init(ALL p. HInit rmhist p)
wenzelm@21624
   218
                          & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
wenzelm@21624
   219
  apply clarsimp
wenzelm@21624
   220
  apply (rule historyI)
wenzelm@21624
   221
      apply assumption+
wenzelm@21624
   222
  apply (rule MI_base)
wenzelm@26342
   223
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
wenzelm@21624
   224
   apply (erule fun_cong)
wenzelm@26342
   225
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
wenzelm@21624
   226
    [thm "busy_squareI"] [] 1 *})
wenzelm@21624
   227
  apply (erule fun_cong)
wenzelm@21624
   228
  done
wenzelm@21624
   229
wenzelm@21624
   230
lemma History: "|- Implementation --> (EEX rmhist. Hist rmhist)"
wenzelm@21624
   231
  apply clarsimp
wenzelm@21624
   232
  apply (rule HistoryLemma [temp_use, THEN eex_mono])
wenzelm@21624
   233
    prefer 3
wenzelm@21624
   234
    apply (force simp: Hist_def HistP_def Init_def all_box [try_rewrite]
wenzelm@21624
   235
      split_box_conj [try_rewrite])
wenzelm@21624
   236
   apply (auto simp: Implementation_def MClkISpec_def RPCISpec_def
wenzelm@21624
   237
     IRSpec_def MClkIPSpec_def RPCIPSpec_def RPSpec_def ImpInit_def
wenzelm@21624
   238
     Init_def ImpNext_def c_def r_def m_def all_box [temp_use] split_box_conj [temp_use])
wenzelm@21624
   239
  done
wenzelm@21624
   240
wenzelm@21624
   241
(******************************** The safety part *********************************)
wenzelm@21624
   242
wenzelm@21624
   243
section "The safety part"
wenzelm@21624
   244
wenzelm@21624
   245
(* ------------------------- Include lower-level lemmas ------------------------- *)
wenzelm@21624
   246
wenzelm@21624
   247
(* RPCFailure notin MemVals U {OK,BadArg} *)
wenzelm@21624
   248
wenzelm@21624
   249
lemma MVOKBAnotRF: "MVOKBA x ==> x ~= RPCFailure"
wenzelm@21624
   250
  apply (unfold MVOKBA_def)
wenzelm@21624
   251
  apply auto
wenzelm@21624
   252
  done
wenzelm@21624
   253
wenzelm@21624
   254
(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
wenzelm@21624
   255
wenzelm@21624
   256
lemma MVOKBARFnotNR: "MVOKBARF x ==> x ~= NotAResult"
wenzelm@21624
   257
  apply (unfold MVOKBARF_def)
wenzelm@21624
   258
  apply auto
wenzelm@21624
   259
  done
wenzelm@21624
   260
wenzelm@21624
   261
(* ================ Si's are mutually exclusive ================================ *)
wenzelm@21624
   262
(* Si and Sj are mutually exclusive for i # j. This helps to simplify the big
wenzelm@21624
   263
   conditional in the definition of resbar when doing the step-simulation proof.
wenzelm@21624
   264
   We prove a weaker result, which suffices for our purposes:
wenzelm@21624
   265
   Si implies (not Sj), for j<i.
wenzelm@21624
   266
*)
wenzelm@21624
   267
wenzelm@21624
   268
(* --- not used ---
wenzelm@21624
   269
Goal "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p &
wenzelm@21624
   270
                         ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
wenzelm@21624
   271
by (auto_tac (MI_css addsimps2 [S_def, S1_def, S2_def,
wenzelm@21624
   272
                                S3_def, S4_def, S5_def, S6_def]));
wenzelm@21624
   273
qed "S1_excl";
wenzelm@21624
   274
*)
wenzelm@21624
   275
wenzelm@21624
   276
lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p"
wenzelm@21624
   277
  by (auto simp: S_def S1_def S2_def)
wenzelm@21624
   278
wenzelm@21624
   279
lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & ~S1 rmhist p & ~S2 rmhist p"
wenzelm@21624
   280
  by (auto simp: S_def S1_def S2_def S3_def)
wenzelm@21624
   281
wenzelm@21624
   282
lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p"
wenzelm@21624
   283
  by (auto simp: S_def S1_def S2_def S3_def S4_def)
wenzelm@21624
   284
wenzelm@21624
   285
lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & ~S1 rmhist p & ~S2 rmhist p
wenzelm@21624
   286
                         & ~S3 rmhist p & ~S4 rmhist p"
wenzelm@21624
   287
  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
wenzelm@21624
   288
wenzelm@21624
   289
lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & ~S1 rmhist p & ~S2 rmhist p
wenzelm@21624
   290
                         & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p"
wenzelm@21624
   291
  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
wenzelm@21624
   292
wenzelm@21624
   293
wenzelm@21624
   294
(* ==================== Lemmas about the environment ============================== *)
wenzelm@21624
   295
wenzelm@21624
   296
lemma Envbusy: "|- $(Calling memCh p) --> ~ENext p"
wenzelm@21624
   297
  by (auto simp: ENext_def Call_def)
wenzelm@21624
   298
wenzelm@21624
   299
(* ==================== Lemmas about the implementation's states ==================== *)
wenzelm@21624
   300
wenzelm@21624
   301
(* The following series of lemmas are used in establishing the implementation's
wenzelm@21624
   302
   next-state relation (Step 1.2 of the proof in the paper). For each state Si, we
wenzelm@21624
   303
   determine which component actions are possible and what state they result in.
wenzelm@21624
   304
*)
wenzelm@21624
   305
wenzelm@21624
   306
(* ------------------------------ State S1 ---------------------------------------- *)
wenzelm@21624
   307
wenzelm@21624
   308
lemma S1Env: "|- ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p)
wenzelm@21624
   309
         --> (S2 rmhist p)$"
wenzelm@21624
   310
  by (force simp: ENext_def Call_def c_def r_def m_def
wenzelm@21624
   311
    caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
wenzelm@21624
   312
wenzelm@21624
   313
lemma S1ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
wenzelm@21624
   314
  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "MClkidle")]
wenzelm@21624
   315
    addsimps2 [thm "S_def", thm "S1_def"]) *})
wenzelm@21624
   316
wenzelm@21624
   317
lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
wenzelm@21624
   318
  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "RPCidle")]
wenzelm@21624
   319
    addsimps2 [thm "S_def", thm "S1_def"]) *})
wenzelm@21624
   320
wenzelm@21624
   321
lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
wenzelm@21624
   322
  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "Memoryidle")]
wenzelm@21624
   323
    addsimps2 [thm "S_def", thm "S1_def"]) *})
wenzelm@21624
   324
wenzelm@21624
   325
lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
wenzelm@21624
   326
         --> unchanged (rmhist!p)"
wenzelm@26342
   327
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
wenzelm@21624
   328
    thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
wenzelm@21624
   329
    thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
wenzelm@21624
   330
wenzelm@21624
   331
wenzelm@21624
   332
(* ------------------------------ State S2 ---------------------------------------- *)
wenzelm@21624
   333
wenzelm@21624
   334
lemma S2EnvUnch: "|- [ENext p]_(e p) & $(S2 rmhist p) --> unchanged (e p)"
wenzelm@21624
   335
  by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
wenzelm@21624
   336
wenzelm@21624
   337
lemma S2Clerk: "|- MClkNext memCh crCh cst p & $(S2 rmhist p) --> MClkFwd memCh crCh cst p"
wenzelm@21624
   338
  by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
wenzelm@21624
   339
wenzelm@21624
   340
lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
wenzelm@21624
   341
         & unchanged (e p, r p, m p, rmhist!p)
wenzelm@21624
   342
         --> (S3 rmhist p)$"
wenzelm@26342
   343
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
wenzelm@21624
   344
    thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
wenzelm@21624
   345
    thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   346
wenzelm@21624
   347
lemma S2RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
wenzelm@21624
   348
  by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
wenzelm@21624
   349
wenzelm@21624
   350
lemma S2MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) --> unchanged (m p)"
wenzelm@21624
   351
  by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
wenzelm@21624
   352
wenzelm@21624
   353
lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
wenzelm@21624
   354
         --> unchanged (rmhist!p)"
wenzelm@21624
   355
  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", thm "MemReturn_def",
wenzelm@21624
   356
    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "S_def", thm "S2_def"]) *})
wenzelm@21624
   357
wenzelm@21624
   358
(* ------------------------------ State S3 ---------------------------------------- *)
wenzelm@21624
   359
wenzelm@21624
   360
lemma S3EnvUnch: "|- [ENext p]_(e p) & $(S3 rmhist p) --> unchanged (e p)"
wenzelm@21624
   361
  by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
wenzelm@21624
   362
wenzelm@21624
   363
lemma S3ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) --> unchanged (c p)"
wenzelm@21624
   364
  by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
wenzelm@21624
   365
wenzelm@21624
   366
lemma S3LegalRcvArg: "|- S3 rmhist p --> IsLegalRcvArg<arg<crCh!p>>"
wenzelm@21624
   367
  by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
wenzelm@21624
   368
wenzelm@21624
   369
lemma S3RPC: "|- RPCNext crCh rmCh rst p & $(S3 rmhist p)
wenzelm@21624
   370
         --> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
wenzelm@21624
   371
  apply clarsimp
wenzelm@21624
   372
  apply (frule S3LegalRcvArg [action_use])
wenzelm@21624
   373
  apply (auto simp: RPCNext_def RPCReject_def RPCReply_def S_def S3_def)
wenzelm@21624
   374
  done
wenzelm@21624
   375
wenzelm@21624
   376
lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
wenzelm@21624
   377
         & unchanged (e p, c p, m p)
wenzelm@21624
   378
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@26342
   379
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
wenzelm@21624
   380
    thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
wenzelm@21624
   381
    thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
wenzelm@21624
   382
    thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
wenzelm@21624
   383
    thm "S3_def", thm "S4_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   384
wenzelm@21624
   385
lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
wenzelm@21624
   386
         & unchanged (e p, c p, m p)
wenzelm@21624
   387
         --> (S6 rmhist p)$"
wenzelm@26342
   388
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
wenzelm@21624
   389
    thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
wenzelm@21624
   390
    thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
wenzelm@21624
   391
    thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   392
wenzelm@21624
   393
lemma S3MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
wenzelm@21624
   394
  by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
wenzelm@21624
   395
wenzelm@21624
   396
lemma S3Hist: "|- HNext rmhist p & $(S3 rmhist p) & unchanged (r p) --> unchanged (rmhist!p)"
wenzelm@21624
   397
  by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
wenzelm@21624
   398
    Return_def r_def rtrner_def S_def S3_def Calling_def)
wenzelm@21624
   399
wenzelm@21624
   400
(* ------------------------------ State S4 ---------------------------------------- *)
wenzelm@21624
   401
wenzelm@21624
   402
lemma S4EnvUnch: "|- [ENext p]_(e p) & $(S4 rmhist p) --> unchanged (e p)"
wenzelm@21624
   403
  by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
wenzelm@21624
   404
wenzelm@21624
   405
lemma S4ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) --> unchanged (c p)"
wenzelm@21624
   406
  by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
wenzelm@21624
   407
wenzelm@21624
   408
lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
wenzelm@21624
   409
  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "S_def", thm "S4_def"]
wenzelm@21624
   410
    addSDs2 [temp_use (thm "RPCbusy")]) *})
wenzelm@21624
   411
wenzelm@21624
   412
lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
wenzelm@21624
   413
         & HNext rmhist p & $(MemInv mm l)
wenzelm@21624
   414
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@26342
   415
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
wenzelm@21624
   416
    thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
wenzelm@21624
   417
    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
wenzelm@21624
   418
    thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
wenzelm@21624
   419
    thm "MVNROKBA_def", thm "S_def", thm "S4_def", thm "RdRequest_def",
wenzelm@21624
   420
    thm "Calling_def", thm "MemInv_def"]) [] [] 1 *})
wenzelm@21624
   421
wenzelm@21624
   422
lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
wenzelm@21624
   423
         & HNext rmhist p & (!l. $MemInv mm l)
wenzelm@21624
   424
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@21624
   425
  by (auto simp: Read_def dest!: S4ReadInner [temp_use])
wenzelm@21624
   426
wenzelm@21624
   427
lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
wenzelm@21624
   428
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@26342
   429
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
wenzelm@21624
   430
    thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
wenzelm@21624
   431
    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
wenzelm@21624
   432
    thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
wenzelm@21624
   433
    thm "S_def", thm "S4_def", thm "WrRequest_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   434
wenzelm@21624
   435
lemma S4Write: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
wenzelm@21624
   436
         & (HNext rmhist p)
wenzelm@21624
   437
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@21624
   438
  by (auto simp: Write_def dest!: S4WriteInner [temp_use])
wenzelm@21624
   439
wenzelm@21624
   440
lemma WriteS4: "|- $ImpInv rmhist p & Write rmCh mm ires p l --> $S4 rmhist p"
wenzelm@21624
   441
  by (auto simp: Write_def WriteInner_def ImpInv_def
wenzelm@21624
   442
    WrRequest_def S_def S1_def S2_def S3_def S4_def S5_def S6_def)
wenzelm@21624
   443
wenzelm@21624
   444
lemma S4Return: "|- MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
wenzelm@21624
   445
         & HNext rmhist p
wenzelm@21624
   446
         --> (S5 rmhist p)$"
wenzelm@21624
   447
  by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
wenzelm@21624
   448
    rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
wenzelm@21624
   449
wenzelm@21624
   450
lemma S4Hist: "|- HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@21624
   451
  by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
wenzelm@21624
   452
    Return_def m_def rtrner_def S_def S4_def Calling_def)
wenzelm@21624
   453
wenzelm@21624
   454
(* ------------------------------ State S5 ---------------------------------------- *)
wenzelm@21624
   455
wenzelm@21624
   456
lemma S5EnvUnch: "|- [ENext p]_(e p) & $(S5 rmhist p) --> unchanged (e p)"
wenzelm@21624
   457
  by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
wenzelm@21624
   458
wenzelm@21624
   459
lemma S5ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) --> unchanged (c p)"
wenzelm@21624
   460
  by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
wenzelm@21624
   461
wenzelm@21624
   462
lemma S5RPC: "|- RPCNext crCh rmCh rst p & $(S5 rmhist p)
wenzelm@21624
   463
         --> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
wenzelm@21624
   464
  by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
wenzelm@21624
   465
wenzelm@21624
   466
lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
wenzelm@21624
   467
       --> (S6 rmhist p)$"
wenzelm@26342
   468
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
wenzelm@21624
   469
    thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
wenzelm@21624
   470
    thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
wenzelm@21624
   471
    thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   472
wenzelm@21624
   473
lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
wenzelm@21624
   474
         --> (S6 rmhist p)$"
wenzelm@26342
   475
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
wenzelm@21624
   476
    thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
wenzelm@21624
   477
    thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
wenzelm@21624
   478
    thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   479
wenzelm@21624
   480
lemma S5MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
wenzelm@21624
   481
  by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
wenzelm@21624
   482
wenzelm@21624
   483
lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
wenzelm@21624
   484
         --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@21624
   485
  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def",
wenzelm@21624
   486
    thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", thm "Return_def",
wenzelm@21624
   487
    thm "S_def", thm "S5_def"]) *})
wenzelm@21624
   488
wenzelm@21624
   489
(* ------------------------------ State S6 ---------------------------------------- *)
wenzelm@21624
   490
wenzelm@21624
   491
lemma S6EnvUnch: "|- [ENext p]_(e p) & $(S6 rmhist p) --> unchanged (e p)"
wenzelm@21624
   492
  by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
wenzelm@21624
   493
wenzelm@21624
   494
lemma S6Clerk: "|- MClkNext memCh crCh cst p & $(S6 rmhist p)
wenzelm@21624
   495
         --> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
wenzelm@21624
   496
  by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
wenzelm@21624
   497
wenzelm@21624
   498
lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
wenzelm@21624
   499
         & unchanged (e p,r p,m p)
wenzelm@21624
   500
         --> (S3 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@26342
   501
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
wenzelm@21624
   502
    thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
wenzelm@21624
   503
    thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
wenzelm@21624
   504
    thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   505
wenzelm@21624
   506
lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
wenzelm@21624
   507
         & unchanged (e p,r p,m p)
wenzelm@21624
   508
         --> (S1 rmhist p)$"
wenzelm@26342
   509
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
wenzelm@21624
   510
    thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
wenzelm@21624
   511
    thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
wenzelm@21624
   512
    thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
wenzelm@21624
   513
wenzelm@21624
   514
lemma S6RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
wenzelm@21624
   515
  by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
wenzelm@21624
   516
wenzelm@21624
   517
lemma S6MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) --> unchanged (m p)"
wenzelm@21624
   518
  by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
wenzelm@21624
   519
wenzelm@21624
   520
lemma S6Hist: "|- HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@21624
   521
  by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
wenzelm@21624
   522
wenzelm@21624
   523
wenzelm@21624
   524
section "Correctness of predicate-action diagram"
wenzelm@21624
   525
wenzelm@21624
   526
wenzelm@21624
   527
(* ========== Step 1.1 ================================================= *)
wenzelm@21624
   528
(* The implementation's initial condition implies the state predicate S1 *)
wenzelm@21624
   529
wenzelm@21624
   530
lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
wenzelm@21624
   531
  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MVNROKBA_def",
wenzelm@21624
   532
    thm "MClkInit_def", thm "RPCInit_def", thm "PInit_def", thm "HInit_def",
wenzelm@21624
   533
    thm "ImpInit_def", thm "S_def", thm "S1_def"]) *})
wenzelm@21624
   534
wenzelm@21624
   535
(* ========== Step 1.2 ================================================== *)
wenzelm@21624
   536
(* Figure 16 is a predicate-action diagram for the implementation. *)
wenzelm@21624
   537
wenzelm@21624
   538
lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   539
         & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
wenzelm@21624
   540
         --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
wenzelm@26342
   541
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
wenzelm@21624
   542
      (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
wenzelm@21624
   543
   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
wenzelm@21624
   544
  done
wenzelm@21624
   545
wenzelm@21624
   546
lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   547
         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
wenzelm@21624
   548
         --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
wenzelm@21624
   549
             & unchanged (e p, r p, m p, rmhist!p)"
wenzelm@26342
   550
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
wenzelm@21624
   551
    (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
wenzelm@21624
   552
   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
wenzelm@21624
   553
     temp_use (thm "S2Forward")]) *})
wenzelm@21624
   554
  done
wenzelm@21624
   555
wenzelm@21624
   556
lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   557
         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
wenzelm@21624
   558
         --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
wenzelm@21624
   559
             | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
wenzelm@26342
   560
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
wenzelm@21624
   561
    (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
wenzelm@26342
   562
  apply (tactic {* action_simp_tac @{simpset} []
wenzelm@21624
   563
    (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
wenzelm@21624
   564
   apply (auto dest!: S3Hist [temp_use])
wenzelm@21624
   565
  done
wenzelm@21624
   566
wenzelm@21624
   567
lemma Step1_2_4: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   568
              & ~unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   569
              & $S4 rmhist p & (!l. $(MemInv mm l))
wenzelm@21624
   570
         --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
wenzelm@21624
   571
             | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
wenzelm@21624
   572
             | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
wenzelm@26342
   573
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
wenzelm@21624
   574
    (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
wenzelm@26342
   575
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
wenzelm@21624
   576
    (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
wenzelm@21624
   577
  apply (auto dest!: S4Hist [temp_use])
wenzelm@21624
   578
  done
wenzelm@21624
   579
wenzelm@21624
   580
lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   581
              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
wenzelm@21624
   582
         --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
wenzelm@21624
   583
             | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
wenzelm@26342
   584
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
wenzelm@21624
   585
    (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
wenzelm@26342
   586
  apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
wenzelm@21624
   587
   apply (tactic {* auto_tac (MI_fast_css addSDs2
wenzelm@21624
   588
     [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
wenzelm@21624
   589
  done
wenzelm@21624
   590
wenzelm@21624
   591
lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   592
              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
wenzelm@21624
   593
         --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
wenzelm@21624
   594
             | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
wenzelm@26342
   595
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
wenzelm@21624
   596
    (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
wenzelm@26342
   597
  apply (tactic {* action_simp_tac @{simpset} []
wenzelm@21624
   598
    (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
wenzelm@21624
   599
     apply (auto dest: S6Hist [temp_use])
wenzelm@21624
   600
  done
wenzelm@21624
   601
wenzelm@21624
   602
(* --------------------------------------------------------------------------
wenzelm@21624
   603
   Step 1.3: S1 implies the barred initial condition.
wenzelm@21624
   604
*)
wenzelm@21624
   605
wenzelm@21624
   606
section "Initialization (Step 1.3)"
wenzelm@21624
   607
wenzelm@21624
   608
lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
wenzelm@26342
   609
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
wenzelm@21624
   610
    thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
wenzelm@21624
   611
wenzelm@21624
   612
(* ----------------------------------------------------------------------
wenzelm@21624
   613
   Step 1.4: Implementation's next-state relation simulates specification's
wenzelm@21624
   614
             next-state relation (with appropriate substitutions)
wenzelm@21624
   615
*)
wenzelm@21624
   616
wenzelm@21624
   617
section "Step simulation (Step 1.4)"
wenzelm@21624
   618
wenzelm@21624
   619
lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
wenzelm@21624
   620
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   621
  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "c_def", thm "r_def",
wenzelm@21624
   622
    thm "m_def", thm "resbar_def"]) *})
wenzelm@21624
   623
wenzelm@21624
   624
lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
wenzelm@21624
   625
         & unchanged (e p, r p, m p, rmhist!p)
wenzelm@21624
   626
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   627
  by (tactic {* action_simp_tac
wenzelm@26342
   628
    (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
wenzelm@21624
   629
    thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
wenzelm@21624
   630
wenzelm@21624
   631
lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
wenzelm@21624
   632
         & unchanged (e p, c p, m p, rmhist!p)
wenzelm@21624
   633
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   634
  apply clarsimp
wenzelm@21624
   635
  apply (drule S3_excl [temp_use] S4_excl [temp_use])+
wenzelm@26342
   636
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
wenzelm@21624
   637
    thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
wenzelm@21624
   638
  done
wenzelm@21624
   639
wenzelm@21624
   640
lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
wenzelm@21624
   641
         & unchanged (e p, c p, m p)
wenzelm@21624
   642
         --> MemFail memCh (resbar rmhist) p"
wenzelm@21624
   643
  apply clarsimp
wenzelm@21624
   644
  apply (drule S6_excl [temp_use])
wenzelm@21624
   645
  apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
wenzelm@21624
   646
    apply (force simp: S3_def S_def)
wenzelm@21624
   647
   apply (auto simp: Return_def)
wenzelm@21624
   648
  done
wenzelm@21624
   649
wenzelm@21624
   650
lemma Step1_4_4a1: "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
wenzelm@21624
   651
         & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l
wenzelm@21624
   652
         --> ReadInner memCh mm (resbar rmhist) p l"
wenzelm@21624
   653
  apply clarsimp
wenzelm@21624
   654
  apply (drule S4_excl [temp_use])+
wenzelm@26342
   655
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
wenzelm@21624
   656
    thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
wenzelm@21624
   657
     apply (auto simp: resbar_def)
wenzelm@21624
   658
       apply (tactic {* ALLGOALS (action_simp_tac
wenzelm@26342
   659
                (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
wenzelm@21624
   660
                  thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
wenzelm@21624
   661
                [] [thm "impE", thm "MemValNotAResultE"]) *})
wenzelm@21624
   662
  done
wenzelm@21624
   663
wenzelm@21624
   664
lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
wenzelm@21624
   665
         & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l))
wenzelm@21624
   666
         --> Read memCh mm (resbar rmhist) p"
wenzelm@21624
   667
  by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
wenzelm@21624
   668
wenzelm@21624
   669
lemma Step1_4_4b1: "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
wenzelm@21624
   670
         & unchanged (e p, c p, r p, rmhist!p)
wenzelm@21624
   671
         --> WriteInner memCh mm (resbar rmhist) p l v"
wenzelm@21624
   672
  apply clarsimp
wenzelm@21624
   673
  apply (drule S4_excl [temp_use])+
wenzelm@26342
   674
  apply (tactic {* action_simp_tac (@{simpset} addsimps
wenzelm@21624
   675
    [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
wenzelm@21624
   676
    thm "c_def", thm "m_def"]) [] [] 1 *})
wenzelm@21624
   677
     apply (auto simp: resbar_def)
wenzelm@26342
   678
    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
wenzelm@21624
   679
      [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
wenzelm@21624
   680
      thm "S4_def", thm "WrRequest_def"]) [] []) *})
wenzelm@21624
   681
  done
wenzelm@21624
   682
wenzelm@21624
   683
lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
wenzelm@21624
   684
         & unchanged (e p, c p, r p, rmhist!p)
wenzelm@21624
   685
         --> Write memCh mm (resbar rmhist) p l"
wenzelm@21624
   686
  by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
wenzelm@21624
   687
wenzelm@21624
   688
lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
wenzelm@21624
   689
         & unchanged (e p, c p, r p)
wenzelm@21624
   690
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@26342
   691
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
wenzelm@21624
   692
    thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
wenzelm@21624
   693
  apply (drule S4_excl [temp_use] S5_excl [temp_use])+
wenzelm@21624
   694
  apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
wenzelm@21624
   695
  done
wenzelm@21624
   696
wenzelm@21624
   697
lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
wenzelm@21624
   698
         & unchanged (e p, c p, m p)
wenzelm@21624
   699
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   700
  apply clarsimp
wenzelm@21624
   701
  apply (drule S5_excl [temp_use] S6_excl [temp_use])+
wenzelm@21624
   702
  apply (auto simp: e_def c_def m_def resbar_def)
wenzelm@21624
   703
   apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
wenzelm@21624
   704
  done
wenzelm@21624
   705
wenzelm@21624
   706
lemma Step1_4_5b: "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
wenzelm@21624
   707
         & unchanged (e p, c p, m p)
wenzelm@21624
   708
         --> MemFail memCh (resbar rmhist) p"
wenzelm@21624
   709
  apply clarsimp
wenzelm@21624
   710
  apply (drule S6_excl [temp_use])
wenzelm@21624
   711
  apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
wenzelm@21624
   712
   apply (auto simp: S5_def S_def)
wenzelm@21624
   713
  done
wenzelm@21624
   714
wenzelm@21624
   715
lemma Step1_4_6a: "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
wenzelm@21624
   716
         & unchanged (e p, r p, m p)
wenzelm@21624
   717
         --> MemReturn memCh (resbar rmhist) p"
wenzelm@21624
   718
  apply clarsimp
wenzelm@21624
   719
  apply (drule S6_excl [temp_use])+
wenzelm@26342
   720
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
wenzelm@21624
   721
    thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
wenzelm@21624
   722
    thm "Return_def", thm "resbar_def"]) [] [] 1 *})
wenzelm@21624
   723
    apply simp_all (* simplify if-then-else *)
wenzelm@26342
   724
    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
wenzelm@21624
   725
      [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
wenzelm@21624
   726
  done
wenzelm@21624
   727
wenzelm@21624
   728
lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
wenzelm@21624
   729
         & unchanged (e p, r p, m p, rmhist!p)
wenzelm@21624
   730
         --> MemFail memCh (resbar rmhist) p"
wenzelm@21624
   731
  apply clarsimp
wenzelm@21624
   732
  apply (drule S3_excl [temp_use])+
wenzelm@26342
   733
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
wenzelm@21624
   734
    thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
wenzelm@21624
   735
   apply (auto simp: S6_def S_def)
wenzelm@21624
   736
  done
wenzelm@21624
   737
wenzelm@21624
   738
lemma S_lemma: "|- unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   739
         --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
wenzelm@21624
   740
  by (auto simp: e_def c_def r_def m_def caller_def rtrner_def S_def Calling_def)
wenzelm@21624
   741
wenzelm@21624
   742
lemma Step1_4_7H: "|- unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   743
         --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p,
wenzelm@21624
   744
                        S4 rmhist p, S5 rmhist p, S6 rmhist p)"
wenzelm@21624
   745
  apply clarsimp
wenzelm@21624
   746
  apply (rule conjI)
wenzelm@21624
   747
   apply (force simp: c_def)
wenzelm@21624
   748
  apply (force simp: S1_def S2_def S3_def S4_def S5_def S6_def intro!: S_lemma [temp_use])
wenzelm@21624
   749
  done
wenzelm@21624
   750
wenzelm@21624
   751
lemma Step1_4_7: "|- unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   752
         --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p,
wenzelm@21624
   753
                        S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)"
wenzelm@21624
   754
  apply (rule actionI)
wenzelm@21624
   755
  apply (unfold action_rews)
wenzelm@21624
   756
  apply (rule impI)
wenzelm@21624
   757
  apply (frule Step1_4_7H [temp_use])
wenzelm@21624
   758
  apply (auto simp: e_def c_def r_def m_def rtrner_def resbar_def)
wenzelm@21624
   759
  done
wenzelm@21624
   760
wenzelm@21624
   761
(* Frequently needed abbreviation: distinguish between idling and non-idling
wenzelm@21624
   762
   steps of the implementation, and try to solve the idling case by simplification
wenzelm@21624
   763
*)
wenzelm@21624
   764
ML {*
wenzelm@24180
   765
fun split_idle_tac ss simps i =
wenzelm@27117
   766
  TRY (rtac @{thm actionI} i) THEN
wenzelm@27117
   767
  case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
wenzelm@27117
   768
  rewrite_goals_tac @{thms action_rews} THEN
wenzelm@27117
   769
  forward_tac [temp_use @{thm Step1_4_7}] i THEN
wenzelm@27117
   770
  asm_full_simp_tac (ss addsimps simps) i
wenzelm@21624
   771
*}
wenzelm@21624
   772
(* ----------------------------------------------------------------------
wenzelm@21624
   773
   Combine steps 1.2 and 1.4 to prove that the implementation satisfies
wenzelm@21624
   774
   the specification's next-state relation.
wenzelm@21624
   775
*)
wenzelm@21624
   776
wenzelm@21624
   777
(* Steps that leave all variables unchanged are safe, so I may assume
wenzelm@21624
   778
   that some variable changes in the proof that a step is safe. *)
wenzelm@21624
   779
lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   780
             --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
wenzelm@21624
   781
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@24180
   782
  apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *})
wenzelm@21624
   783
  apply force
wenzelm@21624
   784
  done
wenzelm@21624
   785
(* turn into (unsafe, looping!) introduction rule *)
wenzelm@21624
   786
lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard]
wenzelm@21624
   787
wenzelm@21624
   788
lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   789
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   790
  apply clarsimp
wenzelm@21624
   791
  apply (rule unchanged_safeI)
wenzelm@21624
   792
  apply (rule idle_squareI)
wenzelm@21624
   793
  apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
wenzelm@21624
   794
  done
wenzelm@21624
   795
wenzelm@21624
   796
lemma S2safe: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   797
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   798
  apply clarsimp
wenzelm@21624
   799
  apply (rule unchanged_safeI)
wenzelm@21624
   800
  apply (rule idle_squareI)
wenzelm@21624
   801
  apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
wenzelm@21624
   802
  done
wenzelm@21624
   803
wenzelm@21624
   804
lemma S3safe: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   805
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   806
  apply clarsimp
wenzelm@21624
   807
  apply (rule unchanged_safeI)
wenzelm@21624
   808
  apply (auto dest!: Step1_2_3 [temp_use])
wenzelm@21624
   809
  apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
wenzelm@21624
   810
  done
wenzelm@21624
   811
wenzelm@21624
   812
lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   813
         & (!l. $(MemInv mm l))
wenzelm@21624
   814
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   815
  apply clarsimp
wenzelm@21624
   816
  apply (rule unchanged_safeI)
wenzelm@21624
   817
  apply (auto dest!: Step1_2_4 [temp_use])
wenzelm@21624
   818
     apply (auto simp: square_def UNext_def RNext_def
wenzelm@21624
   819
       dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
wenzelm@21624
   820
  done
wenzelm@21624
   821
wenzelm@21624
   822
lemma S5safe: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   823
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   824
  apply clarsimp
wenzelm@21624
   825
  apply (rule unchanged_safeI)
wenzelm@21624
   826
  apply (auto dest!: Step1_2_5 [temp_use])
wenzelm@21624
   827
  apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
wenzelm@21624
   828
  done
wenzelm@21624
   829
wenzelm@21624
   830
lemma S6safe: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   831
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   832
  apply clarsimp
wenzelm@21624
   833
  apply (rule unchanged_safeI)
wenzelm@21624
   834
  apply (auto dest!: Step1_2_6 [temp_use])
wenzelm@21624
   835
    apply (auto simp: square_def UNext_def RNext_def
wenzelm@21624
   836
      dest!: Step1_4_6a [temp_use] Step1_4_6b [temp_use])
wenzelm@21624
   837
  done
wenzelm@21624
   838
wenzelm@21624
   839
(* ----------------------------------------------------------------------
wenzelm@21624
   840
   Step 1.5: Temporal refinement proof, based on previous steps.
wenzelm@21624
   841
*)
wenzelm@21624
   842
wenzelm@21624
   843
section "The liveness part"
wenzelm@21624
   844
wenzelm@21624
   845
(* Liveness assertions for the different implementation states, based on the
wenzelm@21624
   846
   fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas
wenzelm@21624
   847
   for readability. Reuse action proofs from safety part.
wenzelm@21624
   848
*)
wenzelm@21624
   849
wenzelm@21624
   850
(* ------------------------------ State S1 ------------------------------ *)
wenzelm@21624
   851
wenzelm@21624
   852
lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   853
         --> (S1 rmhist p)$ | (S2 rmhist p)$"
wenzelm@24180
   854
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
   855
  apply (auto dest!: Step1_2_1 [temp_use])
wenzelm@21624
   856
  done
wenzelm@21624
   857
wenzelm@21624
   858
(* Show that the implementation can satisfy the high-level fairness requirements
wenzelm@21624
   859
   by entering the state S1 infinitely often.
wenzelm@21624
   860
*)
wenzelm@21624
   861
wenzelm@21624
   862
lemma S1_RNextdisabled: "|- S1 rmhist p -->
wenzelm@21624
   863
         ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
wenzelm@26342
   864
  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
wenzelm@21624
   865
    thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
wenzelm@21624
   866
  apply force
wenzelm@21624
   867
  done
wenzelm@21624
   868
wenzelm@21624
   869
lemma S1_Returndisabled: "|- S1 rmhist p -->
wenzelm@21624
   870
         ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
wenzelm@26342
   871
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
wenzelm@21624
   872
    thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
wenzelm@21624
   873
wenzelm@21624
   874
lemma RNext_fair: "|- []<>S1 rmhist p
wenzelm@21624
   875
         --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   876
  by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
wenzelm@21624
   877
    elim!: STL4E [temp_use] DmdImplE [temp_use])
wenzelm@21624
   878
wenzelm@21624
   879
lemma Return_fair: "|- []<>S1 rmhist p
wenzelm@21624
   880
         --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   881
  by (auto simp: WF_alt [try_rewrite]
wenzelm@21624
   882
    intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
wenzelm@21624
   883
wenzelm@21624
   884
(* ------------------------------ State S2 ------------------------------ *)
wenzelm@21624
   885
wenzelm@21624
   886
lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   887
         --> (S2 rmhist p)$ | (S3 rmhist p)$"
wenzelm@24180
   888
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
   889
  apply (auto dest!: Step1_2_2 [temp_use])
wenzelm@21624
   890
  done
wenzelm@21624
   891
wenzelm@21624
   892
lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   893
         & <MClkFwd memCh crCh cst p>_(c p)
wenzelm@21624
   894
         --> (S3 rmhist p)$"
wenzelm@21624
   895
  by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
wenzelm@21624
   896
wenzelm@21624
   897
lemma S2MClkFwd_enabled: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   898
         --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
wenzelm@21624
   899
  apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use])
wenzelm@21624
   900
     apply (cut_tac MI_base)
wenzelm@21624
   901
     apply (blast dest: base_pair)
wenzelm@21624
   902
    apply (simp_all add: S_def S2_def)
wenzelm@21624
   903
  done
wenzelm@21624
   904
wenzelm@21624
   905
lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   906
         & WF(MClkFwd memCh crCh cst p)_(c p)
wenzelm@21624
   907
         --> (S2 rmhist p ~> S3 rmhist p)"
wenzelm@21624
   908
  by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
wenzelm@21624
   909
wenzelm@21624
   910
(* ------------------------------ State S3 ------------------------------ *)
wenzelm@21624
   911
wenzelm@21624
   912
lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   913
         --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
wenzelm@24180
   914
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
   915
  apply (auto dest!: Step1_2_3 [temp_use])
wenzelm@21624
   916
  done
wenzelm@21624
   917
wenzelm@21624
   918
lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   919
         & <RPCNext crCh rmCh rst p>_(r p)
wenzelm@21624
   920
         --> (S4 rmhist p | S6 rmhist p)$"
wenzelm@21624
   921
  apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
wenzelm@21624
   922
  done
wenzelm@21624
   923
wenzelm@21624
   924
lemma S3RPC_enabled: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   925
         --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
wenzelm@21624
   926
  apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
wenzelm@21624
   927
    apply (cut_tac MI_base)
wenzelm@21624
   928
    apply (blast dest: base_pair)
wenzelm@21624
   929
   apply (simp_all add: S_def S3_def)
wenzelm@21624
   930
  done
wenzelm@21624
   931
wenzelm@21624
   932
lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   933
         & WF(RPCNext crCh rmCh rst p)_(r p)
wenzelm@21624
   934
         --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
wenzelm@21624
   935
  by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
wenzelm@21624
   936
wenzelm@21624
   937
(* ------------- State S4 -------------------------------------------------- *)
wenzelm@21624
   938
wenzelm@21624
   939
lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   940
        & (ALL l. $MemInv mm l)
wenzelm@21624
   941
        --> (S4 rmhist p)$ | (S5 rmhist p)$"
wenzelm@24180
   942
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
   943
  apply (auto dest!: Step1_2_4 [temp_use])
wenzelm@21624
   944
  done
wenzelm@21624
   945
wenzelm@21624
   946
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
wenzelm@21624
   947
wenzelm@21624
   948
lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult)
wenzelm@21624
   949
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
wenzelm@21624
   950
         --> (S4 rmhist p & ires!p = #NotAResult)$
wenzelm@21624
   951
             | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
wenzelm@24180
   952
  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
wenzelm@21624
   953
  apply (auto dest!: Step1_2_4 [temp_use])
wenzelm@21624
   954
  done
wenzelm@21624
   955
wenzelm@21624
   956
lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult)
wenzelm@21624
   957
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l))
wenzelm@21624
   958
         & <RNext rmCh mm ires p>_(m p)
wenzelm@21624
   959
         --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
wenzelm@21624
   960
  by (auto simp: angle_def
wenzelm@21624
   961
    dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
wenzelm@21624
   962
wenzelm@21624
   963
lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult)
wenzelm@21624
   964
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
wenzelm@21624
   965
         --> $Enabled (<RNext rmCh mm ires p>_(m p))"
wenzelm@21624
   966
  apply (auto simp: m_def intro!: RNext_enabled [temp_use])
wenzelm@21624
   967
   apply (cut_tac MI_base)
wenzelm@21624
   968
   apply (blast dest: base_pair)
wenzelm@21624
   969
  apply (simp add: S_def S4_def)
wenzelm@21624
   970
  done
wenzelm@21624
   971
wenzelm@21624
   972
lemma S4a_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   973
         & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
wenzelm@21624
   974
         --> (S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
   975
              ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
wenzelm@21624
   976
  by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
wenzelm@21624
   977
wenzelm@21624
   978
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
wenzelm@21624
   979
wenzelm@21624
   980
lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
wenzelm@21624
   981
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
wenzelm@21624
   982
         --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
wenzelm@24180
   983
  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
wenzelm@21624
   984
  apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
wenzelm@21624
   985
  done
wenzelm@21624
   986
wenzelm@21624
   987
lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult)
wenzelm@21624
   988
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   989
         & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
wenzelm@21624
   990
         --> (S5 rmhist p)$"
wenzelm@21624
   991
  by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
wenzelm@21624
   992
wenzelm@21624
   993
lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
wenzelm@21624
   994
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   995
         & (ALL l. $MemInv mm l)
wenzelm@21624
   996
         --> $Enabled (<MemReturn rmCh ires p>_(m p))"
wenzelm@21624
   997
  apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
wenzelm@21624
   998
   apply (cut_tac MI_base)
wenzelm@21624
   999
   apply (blast dest: base_pair)
wenzelm@21624
  1000
  apply (simp add: S_def S4_def)
wenzelm@21624
  1001
  done
wenzelm@21624
  1002
wenzelm@21624
  1003
lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))
wenzelm@21624
  1004
         & WF(MemReturn rmCh ires p)_(m p)
wenzelm@21624
  1005
         --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
wenzelm@21624
  1006
  by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
wenzelm@21624
  1007
wenzelm@21624
  1008
(* ------------------------------ State S5 ------------------------------ *)
wenzelm@21624
  1009
wenzelm@21624
  1010
lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1011
         --> (S5 rmhist p)$ | (S6 rmhist p)$"
wenzelm@24180
  1012
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
  1013
  apply (auto dest!: Step1_2_5 [temp_use])
wenzelm@21624
  1014
  done
wenzelm@21624
  1015
wenzelm@21624
  1016
lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
  1017
         & <RPCNext crCh rmCh rst p>_(r p)
wenzelm@21624
  1018
         --> (S6 rmhist p)$"
wenzelm@21624
  1019
  by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
wenzelm@21624
  1020
wenzelm@21624
  1021
lemma S5RPC_enabled: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1022
         --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
wenzelm@21624
  1023
  apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
wenzelm@21624
  1024
    apply (cut_tac MI_base)
wenzelm@21624
  1025
    apply (blast dest: base_pair)
wenzelm@21624
  1026
   apply (simp_all add: S_def S5_def)
wenzelm@21624
  1027
  done
wenzelm@21624
  1028
wenzelm@21624
  1029
lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
  1030
         & WF(RPCNext crCh rmCh rst p)_(r p)
wenzelm@21624
  1031
         --> (S5 rmhist p ~> S6 rmhist p)"
wenzelm@21624
  1032
  by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
wenzelm@21624
  1033
wenzelm@21624
  1034
(* ------------------------------ State S6 ------------------------------ *)
wenzelm@21624
  1035
wenzelm@21624
  1036
lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1037
         --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
wenzelm@24180
  1038
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
  1039
  apply (auto dest!: Step1_2_6 [temp_use])
wenzelm@21624
  1040
  done
wenzelm@21624
  1041
wenzelm@21624
  1042
lemma S6MClkReply_successors:
wenzelm@21624
  1043
  "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
  1044
         & <MClkReply memCh crCh cst p>_(c p)
wenzelm@21624
  1045
         --> (S1 rmhist p)$"
wenzelm@21624
  1046
  by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
wenzelm@21624
  1047
wenzelm@21624
  1048
lemma MClkReplyS6:
wenzelm@21624
  1049
  "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
wenzelm@26342
  1050
  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
wenzelm@21624
  1051
    thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
wenzelm@21624
  1052
    thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
wenzelm@21624
  1053
wenzelm@21624
  1054
lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
wenzelm@21624
  1055
  apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
wenzelm@21624
  1056
     apply (cut_tac MI_base)
wenzelm@21624
  1057
     apply (blast dest: base_pair)
wenzelm@26342
  1058
    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
wenzelm@21624
  1059
      addsimps [thm "S_def", thm "S6_def"]) [] []) *})
wenzelm@21624
  1060
  done
wenzelm@21624
  1061
wenzelm@21624
  1062
lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
wenzelm@21624
  1063
         & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)
wenzelm@21624
  1064
         --> []<>(S1 rmhist p)"
wenzelm@21624
  1065
  apply clarsimp
wenzelm@21624
  1066
  apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
wenzelm@21624
  1067
   apply (erule InfiniteEnsures)
wenzelm@21624
  1068
    apply assumption
wenzelm@26342
  1069
   apply (tactic {* action_simp_tac @{simpset} []
wenzelm@21624
  1070
     (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
wenzelm@21624
  1071
  apply (auto simp: SF_def)
wenzelm@21624
  1072
  apply (erule contrapos_np)
wenzelm@21624
  1073
  apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
wenzelm@21624
  1074
  done
wenzelm@21624
  1075
wenzelm@21624
  1076
(* --------------- aggregate leadsto properties----------------------------- *)
wenzelm@21624
  1077
wenzelm@21624
  1078
lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p
wenzelm@21624
  1079
      ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
wenzelm@21624
  1080
  by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
wenzelm@21624
  1081
wenzelm@21624
  1082
lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1083
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1084
      ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p
wenzelm@21624
  1085
                    ~> S6 rmhist p"
wenzelm@21624
  1086
  by (auto intro!: LatticeDisjunctionIntro [temp_use]
wenzelm@21624
  1087
    S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
wenzelm@21624
  1088
wenzelm@21624
  1089
lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1090
                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
wenzelm@21624
  1091
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1092
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1093
      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
wenzelm@21624
  1094
  apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) |
wenzelm@21624
  1095
    (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p")
wenzelm@21624
  1096
   apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
wenzelm@21624
  1097
     (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in
wenzelm@21624
  1098
     LatticeTransitivity [temp_use])
wenzelm@21624
  1099
   apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
wenzelm@21624
  1100
  apply (rule LatticeDisjunctionIntro [temp_use])
wenzelm@21624
  1101
   apply (erule LatticeTransitivity [temp_use])
wenzelm@21624
  1102
   apply (erule LatticeTriangle2 [temp_use])
wenzelm@21624
  1103
   apply assumption
wenzelm@21624
  1104
  apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
wenzelm@21624
  1105
  done
wenzelm@21624
  1106
wenzelm@21624
  1107
lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
wenzelm@21624
  1108
         sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1109
                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
wenzelm@21624
  1110
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1111
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1112
      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
wenzelm@21624
  1113
  apply (rule LatticeDisjunctionIntro [temp_use])
wenzelm@21624
  1114
   apply (erule LatticeTriangle2 [temp_use])
wenzelm@21624
  1115
   apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
wenzelm@21624
  1116
      apply (auto intro!: S4S5S6LeadstoS6 [temp_use] necT [temp_use]
wenzelm@21624
  1117
        intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
wenzelm@21624
  1118
  done
wenzelm@21624
  1119
wenzelm@21624
  1120
lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p;
wenzelm@21624
  1121
         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
wenzelm@21624
  1122
         sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1123
                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
wenzelm@21624
  1124
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1125
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1126
      ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
wenzelm@21624
  1127
                   ~> S6 rmhist p"
wenzelm@21624
  1128
  apply (rule LatticeDisjunctionIntro [temp_use])
wenzelm@21624
  1129
   apply (rule LatticeTransitivity [temp_use])
wenzelm@21624
  1130
    prefer 2 apply assumption
wenzelm@21624
  1131
   apply (rule S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
wenzelm@21624
  1132
       apply (auto intro!: S3S4S5S6LeadstoS6 [temp_use] necT [temp_use]
wenzelm@21624
  1133
         intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
wenzelm@21624
  1134
  done
wenzelm@21624
  1135
wenzelm@21624
  1136
lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p;
wenzelm@21624
  1137
         sigma |= S2 rmhist p ~> S3 rmhist p;
wenzelm@21624
  1138
         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
wenzelm@21624
  1139
         sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1140
                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
wenzelm@21624
  1141
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1142
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1143
      ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
wenzelm@21624
  1144
  apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
wenzelm@21624
  1145
       apply assumption+
wenzelm@21624
  1146
  apply (erule INV_leadsto [temp_use])
wenzelm@21624
  1147
  apply (rule ImplLeadsto_gen [temp_use])
wenzelm@21624
  1148
  apply (rule necT [temp_use])
wenzelm@21624
  1149
  apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use])
wenzelm@21624
  1150
  done
wenzelm@21624
  1151
wenzelm@21624
  1152
lemma S1Infinite: "[| sigma |= ~S1 rmhist p ~> S6 rmhist p;
wenzelm@21624
  1153
         sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
wenzelm@21624
  1154
      ==> sigma |= []<>S1 rmhist p"
wenzelm@21624
  1155
  apply (rule classical)
wenzelm@26342
  1156
  apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
wenzelm@21624
  1157
    [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
wenzelm@21624
  1158
  apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
wenzelm@21624
  1159
  done
wenzelm@21624
  1160
wenzelm@21624
  1161
section "Refinement proof (step 1.5)"
wenzelm@21624
  1162
wenzelm@21624
  1163
(* Prove invariants of the implementation:
wenzelm@21624
  1164
   a. memory invariant
wenzelm@21624
  1165
   b. "implementation invariant": always in states S1,...,S6
wenzelm@21624
  1166
*)
wenzelm@21624
  1167
lemma Step1_5_1a: "|- IPImp p --> (ALL l. []$MemInv mm l)"
wenzelm@21624
  1168
  by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
wenzelm@21624
  1169
wenzelm@21624
  1170
lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p)
wenzelm@21624
  1171
         & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
wenzelm@21624
  1172
         --> []ImpInv rmhist p"
wenzelm@21624
  1173
  apply (tactic "inv_tac MI_css 1")
wenzelm@21624
  1174
   apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
wenzelm@21624
  1175
     dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
wenzelm@21624
  1176
     S3_successors [temp_use] S4_successors [temp_use] S5_successors [temp_use]
wenzelm@21624
  1177
     S6_successors [temp_use])
wenzelm@21624
  1178
  done
wenzelm@21624
  1179
wenzelm@21624
  1180
(*** Initialization ***)
wenzelm@21624
  1181
lemma Step1_5_2a: "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"
wenzelm@21624
  1182
  by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
wenzelm@21624
  1183
wenzelm@21624
  1184
(*** step simulation ***)
wenzelm@21624
  1185
lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
wenzelm@21624
  1186
         & $ImpInv rmhist p & (!l. $MemInv mm l))
wenzelm@21624
  1187
         --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
  1188
  by (auto simp: ImpInv_def elim!: STL4E [temp_use]
wenzelm@21624
  1189
    dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
wenzelm@21624
  1190
    S5safe [temp_use] S6safe [temp_use])
wenzelm@21624
  1191
wenzelm@21624
  1192
(*** Liveness ***)
wenzelm@21624
  1193
lemma GoodImpl: "|- IPImp p & HistP rmhist p
wenzelm@21624
  1194
         -->   Init(ImpInit p & HInit rmhist p)
wenzelm@21624
  1195
             & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1196
             & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p)
wenzelm@21624
  1197
             & ImpLive p"
wenzelm@21624
  1198
  apply clarsimp
wenzelm@21624
  1199
    apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & [] (ImpNext p) &
wenzelm@21624
  1200
      [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)")
wenzelm@21624
  1201
   apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
wenzelm@21624
  1202
       dest!: Step1_5_1b [temp_use])
wenzelm@21624
  1203
      apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
wenzelm@21624
  1204
        ImpLive_def c_def r_def m_def)
wenzelm@21624
  1205
      apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
wenzelm@21624
  1206
        HistP_def Init_def ImpInit_def)
wenzelm@21624
  1207
    apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
wenzelm@21624
  1208
      ImpNext_def c_def r_def m_def split_box_conj [temp_use])
wenzelm@21624
  1209
   apply (force simp: HistP_def)
wenzelm@21624
  1210
  apply (force simp: allT [temp_use] dest!: Step1_5_1a [temp_use])
wenzelm@21624
  1211
  done
wenzelm@21624
  1212
wenzelm@21624
  1213
(* The implementation is infinitely often in state S1... *)
wenzelm@21624
  1214
lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1215
         & [](ALL l. $MemInv mm l)
wenzelm@21624
  1216
         & []($ImpInv rmhist p) & ImpLive p
wenzelm@21624
  1217
         --> []<>S1 rmhist p"
wenzelm@21624
  1218
  apply (clarsimp simp: ImpLive_def)
wenzelm@21624
  1219
  apply (rule S1Infinite)
wenzelm@21624
  1220
   apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
wenzelm@21624
  1221
     intro!: NotS1LeadstoS6 [temp_use] S2_live [temp_use] S3_live [temp_use]
wenzelm@21624
  1222
     S4a_live [temp_use] S4b_live [temp_use] S5_live [temp_use])
wenzelm@21624
  1223
  apply (auto simp: split_box_conj [temp_use] intro!: S6_live [temp_use])
wenzelm@21624
  1224
  done
wenzelm@21624
  1225
wenzelm@21624
  1226
(* ... and therefore satisfies the fairness requirements of the specification *)
wenzelm@21624
  1227
lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1228
         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
wenzelm@21624
  1229
         --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
  1230
  by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
wenzelm@21624
  1231
wenzelm@21624
  1232
lemma Step1_5_3c: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1233
         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
wenzelm@21624
  1234
         --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
  1235
  by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
wenzelm@21624
  1236
wenzelm@21624
  1237
(* QED step of step 1 *)
wenzelm@21624
  1238
lemma Step1: "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
wenzelm@21624
  1239
  by (auto simp: UPSpec_def split_box_conj [temp_use]
wenzelm@21624
  1240
    dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use]
wenzelm@21624
  1241
    Step1_5_3b [temp_use] Step1_5_3c [temp_use])
wenzelm@21624
  1242
wenzelm@21624
  1243
(* ------------------------------ Step 2 ------------------------------ *)
wenzelm@21624
  1244
section "Step 2"
wenzelm@21624
  1245
wenzelm@21624
  1246
lemma Step2_2a: "|- Write rmCh mm ires p l & ImpNext p
wenzelm@21624
  1247
         & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
wenzelm@21624
  1248
         & $ImpInv rmhist p
wenzelm@21624
  1249
         --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
wenzelm@21624
  1250
  apply clarsimp
wenzelm@21624
  1251
  apply (drule WriteS4 [action_use])
wenzelm@21624
  1252
   apply assumption
wenzelm@24180
  1253
  apply (tactic "split_idle_tac @{simpset} [] 1")
wenzelm@21624
  1254
  apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
wenzelm@21624
  1255
    S4RPCUnch [temp_use])
wenzelm@21624
  1256
     apply (auto simp: square_def dest: S4Write [temp_use])
wenzelm@21624
  1257
  done
wenzelm@21624
  1258
wenzelm@21624
  1259
lemma Step2_2: "|-   (ALL p. ImpNext p)
wenzelm@21624
  1260
         & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1261
         & (ALL p. $ImpInv rmhist p)
wenzelm@21624
  1262
         & [EX q. Write rmCh mm ires q l]_(mm!l)
wenzelm@21624
  1263
         --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
wenzelm@21624
  1264
  apply (auto intro!: squareCI elim!: squareE)
wenzelm@21624
  1265
  apply (assumption | rule exI Step1_4_4b [action_use])+
wenzelm@21624
  1266
    apply (force intro!: WriteS4 [temp_use])
wenzelm@21624
  1267
   apply (auto dest!: Step2_2a [temp_use])
wenzelm@21624
  1268
  done
wenzelm@21624
  1269
wenzelm@21624
  1270
lemma Step2_lemma: "|- [](  (ALL p. ImpNext p)
wenzelm@21624
  1271
            & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1272
            & (ALL p. $ImpInv rmhist p)
wenzelm@21624
  1273
            & [EX q. Write rmCh mm ires q l]_(mm!l))
wenzelm@21624
  1274
         --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
wenzelm@21624
  1275
  by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
wenzelm@21624
  1276
wenzelm@21624
  1277
lemma Step2: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p)
wenzelm@21624
  1278
         --> MSpec memCh mm (resbar rmhist) l"
wenzelm@21624
  1279
  apply (auto simp: MSpec_def)
wenzelm@21624
  1280
   apply (force simp: IPImp_def MSpec_def)
wenzelm@21624
  1281
  apply (auto intro!: Step2_lemma [temp_use] simp: split_box_conj [temp_use] all_box [temp_use])
wenzelm@21624
  1282
     prefer 4
wenzelm@21624
  1283
     apply (force simp: IPImp_def MSpec_def)
wenzelm@21624
  1284
    apply (auto simp: split_box_conj [temp_use] elim!: allE dest!: GoodImpl [temp_use])
wenzelm@21624
  1285
  done
wenzelm@21624
  1286
wenzelm@21624
  1287
(* ----------------------------- Main theorem --------------------------------- *)
wenzelm@21624
  1288
section "Memory implementation"
wenzelm@21624
  1289
wenzelm@21624
  1290
(* The combination of a legal caller, the memory clerk, the RPC component,
wenzelm@21624
  1291
   and a reliable memory implement the unreliable memory.
wenzelm@21624
  1292
*)
wenzelm@21624
  1293
wenzelm@21624
  1294
(* Implementation of internal specification by combination of implementation
wenzelm@21624
  1295
   and history variable with explicit refinement mapping
wenzelm@21624
  1296
*)
wenzelm@21624
  1297
lemma Impl_IUSpec: "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"
wenzelm@21624
  1298
  by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def
wenzelm@21624
  1299
    RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use])
wenzelm@21624
  1300
wenzelm@21624
  1301
(* The main theorem: introduce hiding and eliminate history variable. *)
wenzelm@21624
  1302
lemma Implementation: "|- Implementation --> USpec memCh"
wenzelm@21624
  1303
  apply clarsimp
wenzelm@21624
  1304
  apply (frule History [temp_use])
wenzelm@21624
  1305
  apply (auto simp: USpec_def intro: eexI [temp_use] Impl_IUSpec [temp_use]
wenzelm@21624
  1306
    MI_base [temp_use] elim!: eexE)
wenzelm@21624
  1307
  done
wenzelm@3807
  1308
wenzelm@3807
  1309
end