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