src/HOL/TLA/Memory/MemoryImplementation.thy
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 58249 180f1b3508ed
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
wenzelm@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@21624
   221
(* A more aggressive variant that tries to solve subgoals by assumption
wenzelm@21624
   222
   or contradiction during the simplification.
wenzelm@21624
   223
   THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
wenzelm@42771
   224
   (but it can be a lot faster than the default setup)
wenzelm@21624
   225
*)
wenzelm@21624
   226
ML {*
wenzelm@42771
   227
  val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
wenzelm@51717
   228
  val fast_solver = mk_solver "fast_solver" (fn ctxt =>
wenzelm@51717
   229
    if Config.get ctxt config_fast_solver
wenzelm@42771
   230
    then assume_tac ORELSE' (etac notE)
wenzelm@42771
   231
    else K no_tac);
wenzelm@42771
   232
*}
wenzelm@21624
   233
wenzelm@51717
   234
setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
wenzelm@42771
   235
wenzelm@54742
   236
ML {* val temp_elim = make_elim oo temp_use *}
wenzelm@21624
   237
wenzelm@21624
   238
wenzelm@21624
   239
wenzelm@21624
   240
(****************************** The history variable ******************************)
wenzelm@21624
   241
wenzelm@21624
   242
section "History variable"
wenzelm@21624
   243
wenzelm@21624
   244
lemma HistoryLemma: "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p)
wenzelm@21624
   245
         --> (EEX rmhist. Init(ALL p. HInit rmhist p)
wenzelm@21624
   246
                          & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
wenzelm@21624
   247
  apply clarsimp
wenzelm@21624
   248
  apply (rule historyI)
wenzelm@21624
   249
      apply assumption+
wenzelm@21624
   250
  apply (rule MI_base)
wenzelm@51717
   251
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm HInit_def}]) [] [] 1 *})
wenzelm@21624
   252
   apply (erule fun_cong)
wenzelm@51717
   253
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}])
wenzelm@39159
   254
    [@{thm busy_squareI}] [] 1 *})
wenzelm@21624
   255
  apply (erule fun_cong)
wenzelm@21624
   256
  done
wenzelm@21624
   257
wenzelm@21624
   258
lemma History: "|- Implementation --> (EEX rmhist. Hist rmhist)"
wenzelm@21624
   259
  apply clarsimp
wenzelm@21624
   260
  apply (rule HistoryLemma [temp_use, THEN eex_mono])
wenzelm@21624
   261
    prefer 3
wenzelm@21624
   262
    apply (force simp: Hist_def HistP_def Init_def all_box [try_rewrite]
wenzelm@21624
   263
      split_box_conj [try_rewrite])
wenzelm@21624
   264
   apply (auto simp: Implementation_def MClkISpec_def RPCISpec_def
wenzelm@21624
   265
     IRSpec_def MClkIPSpec_def RPCIPSpec_def RPSpec_def ImpInit_def
wenzelm@21624
   266
     Init_def ImpNext_def c_def r_def m_def all_box [temp_use] split_box_conj [temp_use])
wenzelm@21624
   267
  done
wenzelm@21624
   268
wenzelm@21624
   269
(******************************** The safety part *********************************)
wenzelm@21624
   270
wenzelm@21624
   271
section "The safety part"
wenzelm@21624
   272
wenzelm@21624
   273
(* ------------------------- Include lower-level lemmas ------------------------- *)
wenzelm@21624
   274
wenzelm@21624
   275
(* RPCFailure notin MemVals U {OK,BadArg} *)
wenzelm@21624
   276
wenzelm@21624
   277
lemma MVOKBAnotRF: "MVOKBA x ==> x ~= RPCFailure"
wenzelm@21624
   278
  apply (unfold MVOKBA_def)
wenzelm@21624
   279
  apply auto
wenzelm@21624
   280
  done
wenzelm@21624
   281
wenzelm@21624
   282
(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
wenzelm@21624
   283
wenzelm@21624
   284
lemma MVOKBARFnotNR: "MVOKBARF x ==> x ~= NotAResult"
wenzelm@21624
   285
  apply (unfold MVOKBARF_def)
wenzelm@21624
   286
  apply auto
wenzelm@21624
   287
  done
wenzelm@21624
   288
wenzelm@21624
   289
(* ================ Si's are mutually exclusive ================================ *)
wenzelm@21624
   290
(* Si and Sj are mutually exclusive for i # j. This helps to simplify the big
wenzelm@21624
   291
   conditional in the definition of resbar when doing the step-simulation proof.
wenzelm@21624
   292
   We prove a weaker result, which suffices for our purposes:
wenzelm@21624
   293
   Si implies (not Sj), for j<i.
wenzelm@21624
   294
*)
wenzelm@21624
   295
wenzelm@21624
   296
(* --- not used ---
wenzelm@42772
   297
lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p &
wenzelm@42772
   298
    ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
wenzelm@42772
   299
  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
wenzelm@21624
   300
*)
wenzelm@21624
   301
wenzelm@21624
   302
lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p"
wenzelm@21624
   303
  by (auto simp: S_def S1_def S2_def)
wenzelm@21624
   304
wenzelm@21624
   305
lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & ~S1 rmhist p & ~S2 rmhist p"
wenzelm@21624
   306
  by (auto simp: S_def S1_def S2_def S3_def)
wenzelm@21624
   307
wenzelm@21624
   308
lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p"
wenzelm@21624
   309
  by (auto simp: S_def S1_def S2_def S3_def S4_def)
wenzelm@21624
   310
wenzelm@21624
   311
lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & ~S1 rmhist p & ~S2 rmhist p
wenzelm@21624
   312
                         & ~S3 rmhist p & ~S4 rmhist p"
wenzelm@21624
   313
  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
wenzelm@21624
   314
wenzelm@21624
   315
lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & ~S1 rmhist p & ~S2 rmhist p
wenzelm@21624
   316
                         & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p"
wenzelm@21624
   317
  by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
wenzelm@21624
   318
wenzelm@21624
   319
wenzelm@21624
   320
(* ==================== Lemmas about the environment ============================== *)
wenzelm@21624
   321
wenzelm@21624
   322
lemma Envbusy: "|- $(Calling memCh p) --> ~ENext p"
wenzelm@21624
   323
  by (auto simp: ENext_def Call_def)
wenzelm@21624
   324
wenzelm@21624
   325
(* ==================== Lemmas about the implementation's states ==================== *)
wenzelm@21624
   326
wenzelm@21624
   327
(* The following series of lemmas are used in establishing the implementation's
wenzelm@21624
   328
   next-state relation (Step 1.2 of the proof in the paper). For each state Si, we
wenzelm@21624
   329
   determine which component actions are possible and what state they result in.
wenzelm@21624
   330
*)
wenzelm@21624
   331
wenzelm@21624
   332
(* ------------------------------ State S1 ---------------------------------------- *)
wenzelm@21624
   333
wenzelm@21624
   334
lemma S1Env: "|- ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p)
wenzelm@21624
   335
         --> (S2 rmhist p)$"
wenzelm@21624
   336
  by (force simp: ENext_def Call_def c_def r_def m_def
wenzelm@21624
   337
    caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
wenzelm@21624
   338
wenzelm@21624
   339
lemma S1ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
wenzelm@42771
   340
  using [[fast_solver]]
wenzelm@42771
   341
  by (auto elim!: squareE [temp_use] dest!: MClkidle [temp_use] simp: S_def S1_def)
wenzelm@21624
   342
wenzelm@21624
   343
lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
wenzelm@42771
   344
  using [[fast_solver]]
wenzelm@42771
   345
  by (auto elim!: squareE [temp_use] dest!: RPCidle [temp_use] simp: S_def S1_def)
wenzelm@21624
   346
wenzelm@21624
   347
lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
wenzelm@42771
   348
  using [[fast_solver]]
wenzelm@42771
   349
  by (auto elim!: squareE [temp_use] dest!: Memoryidle [temp_use] simp: S_def S1_def)
wenzelm@21624
   350
wenzelm@21624
   351
lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
wenzelm@21624
   352
         --> unchanged (rmhist!p)"
wenzelm@51717
   353
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
wenzelm@39159
   354
    @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
wenzelm@54742
   355
    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
wenzelm@21624
   356
wenzelm@21624
   357
wenzelm@21624
   358
(* ------------------------------ State S2 ---------------------------------------- *)
wenzelm@21624
   359
wenzelm@21624
   360
lemma S2EnvUnch: "|- [ENext p]_(e p) & $(S2 rmhist p) --> unchanged (e p)"
wenzelm@21624
   361
  by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
wenzelm@21624
   362
wenzelm@21624
   363
lemma S2Clerk: "|- MClkNext memCh crCh cst p & $(S2 rmhist p) --> MClkFwd memCh crCh cst p"
wenzelm@21624
   364
  by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
wenzelm@21624
   365
wenzelm@21624
   366
lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
wenzelm@21624
   367
         & unchanged (e p, r p, m p, rmhist!p)
wenzelm@21624
   368
         --> (S3 rmhist p)$"
wenzelm@51717
   369
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
wenzelm@39159
   370
    @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
wenzelm@39159
   371
    @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   372
wenzelm@21624
   373
lemma S2RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
wenzelm@21624
   374
  by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
wenzelm@21624
   375
wenzelm@21624
   376
lemma S2MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) --> unchanged (m p)"
wenzelm@21624
   377
  by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
wenzelm@21624
   378
wenzelm@21624
   379
lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
wenzelm@21624
   380
         --> unchanged (rmhist!p)"
wenzelm@42771
   381
  using [[fast_solver]]
wenzelm@42771
   382
  by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
wenzelm@42771
   383
    MClkReply_def Return_def S_def S2_def)
wenzelm@21624
   384
wenzelm@21624
   385
(* ------------------------------ State S3 ---------------------------------------- *)
wenzelm@21624
   386
wenzelm@21624
   387
lemma S3EnvUnch: "|- [ENext p]_(e p) & $(S3 rmhist p) --> unchanged (e p)"
wenzelm@21624
   388
  by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
wenzelm@21624
   389
wenzelm@21624
   390
lemma S3ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) --> unchanged (c p)"
wenzelm@21624
   391
  by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
wenzelm@21624
   392
wenzelm@21624
   393
lemma S3LegalRcvArg: "|- S3 rmhist p --> IsLegalRcvArg<arg<crCh!p>>"
wenzelm@21624
   394
  by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
wenzelm@21624
   395
wenzelm@21624
   396
lemma S3RPC: "|- RPCNext crCh rmCh rst p & $(S3 rmhist p)
wenzelm@21624
   397
         --> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
wenzelm@21624
   398
  apply clarsimp
wenzelm@21624
   399
  apply (frule S3LegalRcvArg [action_use])
wenzelm@21624
   400
  apply (auto simp: RPCNext_def RPCReject_def RPCReply_def S_def S3_def)
wenzelm@21624
   401
  done
wenzelm@21624
   402
wenzelm@21624
   403
lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
wenzelm@21624
   404
         & unchanged (e p, c p, m p)
wenzelm@21624
   405
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@51717
   406
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
wenzelm@39159
   407
    @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
wenzelm@39159
   408
    @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
wenzelm@39159
   409
    @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
wenzelm@39159
   410
    @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   411
wenzelm@21624
   412
lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
wenzelm@21624
   413
         & unchanged (e p, c p, m p)
wenzelm@21624
   414
         --> (S6 rmhist p)$"
wenzelm@51717
   415
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
wenzelm@39159
   416
    @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
wenzelm@39159
   417
    @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
wenzelm@39159
   418
    @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   419
wenzelm@21624
   420
lemma S3MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
wenzelm@21624
   421
  by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
wenzelm@21624
   422
wenzelm@21624
   423
lemma S3Hist: "|- HNext rmhist p & $(S3 rmhist p) & unchanged (r p) --> unchanged (rmhist!p)"
wenzelm@21624
   424
  by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
wenzelm@21624
   425
    Return_def r_def rtrner_def S_def S3_def Calling_def)
wenzelm@21624
   426
wenzelm@21624
   427
(* ------------------------------ State S4 ---------------------------------------- *)
wenzelm@21624
   428
wenzelm@21624
   429
lemma S4EnvUnch: "|- [ENext p]_(e p) & $(S4 rmhist p) --> unchanged (e p)"
wenzelm@21624
   430
  by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
wenzelm@21624
   431
wenzelm@21624
   432
lemma S4ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) --> unchanged (c p)"
wenzelm@21624
   433
  by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
wenzelm@21624
   434
wenzelm@21624
   435
lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
wenzelm@42771
   436
  using [[fast_solver]]
wenzelm@42771
   437
  by (auto elim!: squareE [temp_use] dest!: RPCbusy [temp_use] simp: S_def S4_def)
wenzelm@21624
   438
wenzelm@21624
   439
lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
wenzelm@21624
   440
         & HNext rmhist p & $(MemInv mm l)
wenzelm@21624
   441
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@51717
   442
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
wenzelm@39159
   443
    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
wenzelm@39159
   444
    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
wenzelm@39159
   445
    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
wenzelm@39159
   446
    @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
wenzelm@39159
   447
    @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
wenzelm@21624
   448
wenzelm@21624
   449
lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
wenzelm@21624
   450
         & HNext rmhist p & (!l. $MemInv mm l)
wenzelm@21624
   451
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@21624
   452
  by (auto simp: Read_def dest!: S4ReadInner [temp_use])
wenzelm@21624
   453
wenzelm@21624
   454
lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
wenzelm@21624
   455
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@51717
   456
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
wenzelm@39159
   457
    @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
wenzelm@39159
   458
    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
wenzelm@39159
   459
    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
wenzelm@39159
   460
    @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   461
wenzelm@21624
   462
lemma S4Write: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
wenzelm@21624
   463
         & (HNext rmhist p)
wenzelm@21624
   464
         --> (S4 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@21624
   465
  by (auto simp: Write_def dest!: S4WriteInner [temp_use])
wenzelm@21624
   466
wenzelm@21624
   467
lemma WriteS4: "|- $ImpInv rmhist p & Write rmCh mm ires p l --> $S4 rmhist p"
wenzelm@21624
   468
  by (auto simp: Write_def WriteInner_def ImpInv_def
wenzelm@21624
   469
    WrRequest_def S_def S1_def S2_def S3_def S4_def S5_def S6_def)
wenzelm@21624
   470
wenzelm@21624
   471
lemma S4Return: "|- MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
wenzelm@21624
   472
         & HNext rmhist p
wenzelm@21624
   473
         --> (S5 rmhist p)$"
wenzelm@21624
   474
  by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
wenzelm@21624
   475
    rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
wenzelm@21624
   476
wenzelm@21624
   477
lemma S4Hist: "|- HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@21624
   478
  by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
wenzelm@21624
   479
    Return_def m_def rtrner_def S_def S4_def Calling_def)
wenzelm@21624
   480
wenzelm@21624
   481
(* ------------------------------ State S5 ---------------------------------------- *)
wenzelm@21624
   482
wenzelm@21624
   483
lemma S5EnvUnch: "|- [ENext p]_(e p) & $(S5 rmhist p) --> unchanged (e p)"
wenzelm@21624
   484
  by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
wenzelm@21624
   485
wenzelm@21624
   486
lemma S5ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) --> unchanged (c p)"
wenzelm@21624
   487
  by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
wenzelm@21624
   488
wenzelm@21624
   489
lemma S5RPC: "|- RPCNext crCh rmCh rst p & $(S5 rmhist p)
wenzelm@21624
   490
         --> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
wenzelm@21624
   491
  by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
wenzelm@21624
   492
wenzelm@21624
   493
lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
wenzelm@21624
   494
       --> (S6 rmhist p)$"
wenzelm@51717
   495
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
wenzelm@39159
   496
    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
wenzelm@39159
   497
    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
wenzelm@39159
   498
    @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   499
wenzelm@21624
   500
lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
wenzelm@21624
   501
         --> (S6 rmhist p)$"
wenzelm@51717
   502
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
wenzelm@39159
   503
    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
wenzelm@39159
   504
    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
wenzelm@39159
   505
    @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   506
wenzelm@21624
   507
lemma S5MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
wenzelm@21624
   508
  by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
wenzelm@21624
   509
wenzelm@21624
   510
lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
wenzelm@21624
   511
         --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@42771
   512
  using [[fast_solver]]
wenzelm@42771
   513
  by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
wenzelm@42771
   514
    MClkReply_def Return_def S_def S5_def)
wenzelm@21624
   515
wenzelm@21624
   516
(* ------------------------------ State S6 ---------------------------------------- *)
wenzelm@21624
   517
wenzelm@21624
   518
lemma S6EnvUnch: "|- [ENext p]_(e p) & $(S6 rmhist p) --> unchanged (e p)"
wenzelm@21624
   519
  by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
wenzelm@21624
   520
wenzelm@21624
   521
lemma S6Clerk: "|- MClkNext memCh crCh cst p & $(S6 rmhist p)
wenzelm@21624
   522
         --> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
wenzelm@21624
   523
  by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
wenzelm@21624
   524
wenzelm@21624
   525
lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
wenzelm@21624
   526
         & unchanged (e p,r p,m p)
wenzelm@21624
   527
         --> (S3 rmhist p)$ & unchanged (rmhist!p)"
wenzelm@51717
   528
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
wenzelm@39159
   529
    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
wenzelm@39159
   530
    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
wenzelm@39159
   531
    @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   532
wenzelm@21624
   533
lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
wenzelm@21624
   534
         & unchanged (e p,r p,m p)
wenzelm@21624
   535
         --> (S1 rmhist p)$"
wenzelm@51717
   536
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
wenzelm@39159
   537
    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
wenzelm@39159
   538
    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
wenzelm@39159
   539
    @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
wenzelm@21624
   540
wenzelm@21624
   541
lemma S6RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
wenzelm@21624
   542
  by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
wenzelm@21624
   543
wenzelm@21624
   544
lemma S6MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) --> unchanged (m p)"
wenzelm@21624
   545
  by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
wenzelm@21624
   546
wenzelm@21624
   547
lemma S6Hist: "|- HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) --> (rmhist!p)$ = $(rmhist!p)"
wenzelm@21624
   548
  by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
wenzelm@21624
   549
wenzelm@21624
   550
wenzelm@21624
   551
section "Correctness of predicate-action diagram"
wenzelm@21624
   552
wenzelm@21624
   553
wenzelm@21624
   554
(* ========== Step 1.1 ================================================= *)
wenzelm@21624
   555
(* The implementation's initial condition implies the state predicate S1 *)
wenzelm@21624
   556
wenzelm@21624
   557
lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
wenzelm@42771
   558
  using [[fast_solver]]
wenzelm@42771
   559
  by (auto elim!: squareE [temp_use] simp: MVNROKBA_def
wenzelm@42771
   560
    MClkInit_def RPCInit_def PInit_def HInit_def ImpInit_def S_def S1_def)
wenzelm@21624
   561
wenzelm@21624
   562
(* ========== Step 1.2 ================================================== *)
wenzelm@21624
   563
(* Figure 16 is a predicate-action diagram for the implementation. *)
wenzelm@21624
   564
wenzelm@21624
   565
lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   566
         & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
wenzelm@21624
   567
         --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
wenzelm@51717
   568
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
wenzelm@54742
   569
      (map (temp_elim @{context})
wenzelm@54742
   570
        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
wenzelm@42771
   571
   using [[fast_solver]]
wenzelm@42771
   572
   apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
wenzelm@21624
   573
  done
wenzelm@21624
   574
wenzelm@21624
   575
lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   576
         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
wenzelm@21624
   577
         --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
wenzelm@21624
   578
             & unchanged (e p, r p, m p, rmhist!p)"
wenzelm@51717
   579
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
wenzelm@54742
   580
    (map (temp_elim @{context})
wenzelm@54742
   581
      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
wenzelm@42771
   582
   using [[fast_solver]]
wenzelm@42771
   583
   apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
wenzelm@21624
   584
  done
wenzelm@21624
   585
wenzelm@21624
   586
lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   587
         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
wenzelm@21624
   588
         --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
wenzelm@21624
   589
             | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
wenzelm@51717
   590
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
wenzelm@54742
   591
    (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
wenzelm@51717
   592
  apply (tactic {* action_simp_tac @{context} []
wenzelm@54742
   593
    (@{thm squareE} ::
wenzelm@54742
   594
      map (temp_elim @{context}) [@{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@51717
   604
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
wenzelm@54742
   605
    (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
wenzelm@51717
   606
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
wenzelm@54742
   607
    (@{thm squareE} ::
wenzelm@54742
   608
      map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
wenzelm@21624
   609
  apply (auto dest!: S4Hist [temp_use])
wenzelm@21624
   610
  done
wenzelm@21624
   611
wenzelm@21624
   612
lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   613
              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
wenzelm@21624
   614
         --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
wenzelm@21624
   615
             | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
wenzelm@51717
   616
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
wenzelm@54742
   617
    (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
wenzelm@54742
   618
  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
wenzelm@42771
   619
   using [[fast_solver]]
wenzelm@42771
   620
   apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
wenzelm@21624
   621
  done
wenzelm@21624
   622
wenzelm@21624
   623
lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
wenzelm@21624
   624
              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
wenzelm@21624
   625
         --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
wenzelm@21624
   626
             | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
wenzelm@51717
   627
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
wenzelm@54742
   628
    (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
wenzelm@51717
   629
  apply (tactic {* action_simp_tac @{context} []
wenzelm@54742
   630
    (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
wenzelm@21624
   631
     apply (auto dest: S6Hist [temp_use])
wenzelm@21624
   632
  done
wenzelm@21624
   633
wenzelm@21624
   634
(* --------------------------------------------------------------------------
wenzelm@21624
   635
   Step 1.3: S1 implies the barred initial condition.
wenzelm@21624
   636
*)
wenzelm@21624
   637
wenzelm@21624
   638
section "Initialization (Step 1.3)"
wenzelm@21624
   639
wenzelm@21624
   640
lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
wenzelm@51717
   641
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm resbar_def},
wenzelm@39159
   642
    @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
wenzelm@21624
   643
wenzelm@21624
   644
(* ----------------------------------------------------------------------
wenzelm@21624
   645
   Step 1.4: Implementation's next-state relation simulates specification's
wenzelm@21624
   646
             next-state relation (with appropriate substitutions)
wenzelm@21624
   647
*)
wenzelm@21624
   648
wenzelm@21624
   649
section "Step simulation (Step 1.4)"
wenzelm@21624
   650
wenzelm@21624
   651
lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
wenzelm@21624
   652
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@42771
   653
  using [[fast_solver]]
wenzelm@42771
   654
  by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def)
wenzelm@21624
   655
wenzelm@21624
   656
lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
wenzelm@21624
   657
         & unchanged (e p, r p, m p, rmhist!p)
wenzelm@21624
   658
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   659
  by (tactic {* action_simp_tac
wenzelm@51717
   660
    (@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
wenzelm@39159
   661
    @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
wenzelm@21624
   662
wenzelm@21624
   663
lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
wenzelm@21624
   664
         & unchanged (e p, c p, m p, rmhist!p)
wenzelm@21624
   665
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   666
  apply clarsimp
wenzelm@21624
   667
  apply (drule S3_excl [temp_use] S4_excl [temp_use])+
wenzelm@51717
   668
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
wenzelm@39159
   669
    @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
wenzelm@21624
   670
  done
wenzelm@21624
   671
wenzelm@21624
   672
lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
wenzelm@21624
   673
         & unchanged (e p, c p, m p)
wenzelm@21624
   674
         --> MemFail memCh (resbar rmhist) p"
wenzelm@21624
   675
  apply clarsimp
wenzelm@21624
   676
  apply (drule S6_excl [temp_use])
wenzelm@21624
   677
  apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
wenzelm@21624
   678
    apply (force simp: S3_def S_def)
wenzelm@21624
   679
   apply (auto simp: Return_def)
wenzelm@21624
   680
  done
wenzelm@21624
   681
wenzelm@21624
   682
lemma Step1_4_4a1: "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
wenzelm@21624
   683
         & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l
wenzelm@21624
   684
         --> ReadInner memCh mm (resbar rmhist) p l"
wenzelm@21624
   685
  apply clarsimp
wenzelm@21624
   686
  apply (drule S4_excl [temp_use])+
wenzelm@51717
   687
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
wenzelm@39159
   688
    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
wenzelm@21624
   689
     apply (auto simp: resbar_def)
wenzelm@21624
   690
       apply (tactic {* ALLGOALS (action_simp_tac
wenzelm@51717
   691
                (@{context} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
wenzelm@39159
   692
                  @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
wenzelm@39159
   693
                [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
wenzelm@21624
   694
  done
wenzelm@21624
   695
wenzelm@21624
   696
lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
wenzelm@21624
   697
         & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l))
wenzelm@21624
   698
         --> Read memCh mm (resbar rmhist) p"
wenzelm@21624
   699
  by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
wenzelm@21624
   700
wenzelm@21624
   701
lemma Step1_4_4b1: "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
wenzelm@21624
   702
         & unchanged (e p, c p, r p, rmhist!p)
wenzelm@21624
   703
         --> WriteInner memCh mm (resbar rmhist) p l v"
wenzelm@21624
   704
  apply clarsimp
wenzelm@21624
   705
  apply (drule S4_excl [temp_use])+
wenzelm@51717
   706
  apply (tactic {* action_simp_tac (@{context} addsimps
wenzelm@39159
   707
    [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
wenzelm@39159
   708
    @{thm c_def}, @{thm m_def}]) [] [] 1 *})
wenzelm@21624
   709
     apply (auto simp: resbar_def)
wenzelm@51717
   710
    apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
wenzelm@39159
   711
      [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
wenzelm@39159
   712
      @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
wenzelm@21624
   713
  done
wenzelm@21624
   714
wenzelm@21624
   715
lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
wenzelm@21624
   716
         & unchanged (e p, c p, r p, rmhist!p)
wenzelm@21624
   717
         --> Write memCh mm (resbar rmhist) p l"
wenzelm@21624
   718
  by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
wenzelm@21624
   719
wenzelm@21624
   720
lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
wenzelm@21624
   721
         & unchanged (e p, c p, r p)
wenzelm@21624
   722
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@51717
   723
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
wenzelm@39159
   724
    @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
wenzelm@21624
   725
  apply (drule S4_excl [temp_use] S5_excl [temp_use])+
wenzelm@42771
   726
  using [[fast_solver]]
wenzelm@42771
   727
  apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
wenzelm@21624
   728
  done
wenzelm@21624
   729
wenzelm@21624
   730
lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
wenzelm@21624
   731
         & unchanged (e p, c p, m p)
wenzelm@21624
   732
         --> unchanged (rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   733
  apply clarsimp
wenzelm@21624
   734
  apply (drule S5_excl [temp_use] S6_excl [temp_use])+
wenzelm@21624
   735
  apply (auto simp: e_def c_def m_def resbar_def)
wenzelm@21624
   736
   apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
wenzelm@21624
   737
  done
wenzelm@21624
   738
wenzelm@21624
   739
lemma Step1_4_5b: "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
wenzelm@21624
   740
         & unchanged (e p, c p, m p)
wenzelm@21624
   741
         --> MemFail memCh (resbar rmhist) p"
wenzelm@21624
   742
  apply clarsimp
wenzelm@21624
   743
  apply (drule S6_excl [temp_use])
wenzelm@21624
   744
  apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
wenzelm@21624
   745
   apply (auto simp: S5_def S_def)
wenzelm@21624
   746
  done
wenzelm@21624
   747
wenzelm@21624
   748
lemma Step1_4_6a: "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
wenzelm@21624
   749
         & unchanged (e p, r p, m p)
wenzelm@21624
   750
         --> MemReturn memCh (resbar rmhist) p"
wenzelm@21624
   751
  apply clarsimp
wenzelm@21624
   752
  apply (drule S6_excl [temp_use])+
wenzelm@51717
   753
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
wenzelm@39159
   754
    @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
wenzelm@39159
   755
    @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
wenzelm@21624
   756
    apply simp_all (* simplify if-then-else *)
wenzelm@51717
   757
    apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
wenzelm@39159
   758
      [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
wenzelm@21624
   759
  done
wenzelm@21624
   760
wenzelm@21624
   761
lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
wenzelm@21624
   762
         & unchanged (e p, r p, m p, rmhist!p)
wenzelm@21624
   763
         --> MemFail memCh (resbar rmhist) p"
wenzelm@21624
   764
  apply clarsimp
wenzelm@21624
   765
  apply (drule S3_excl [temp_use])+
wenzelm@51717
   766
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def},
wenzelm@39159
   767
    @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
wenzelm@21624
   768
   apply (auto simp: S6_def S_def)
wenzelm@21624
   769
  done
wenzelm@21624
   770
wenzelm@21624
   771
lemma S_lemma: "|- unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   772
         --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
wenzelm@21624
   773
  by (auto simp: e_def c_def r_def m_def caller_def rtrner_def S_def Calling_def)
wenzelm@21624
   774
wenzelm@21624
   775
lemma Step1_4_7H: "|- unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   776
         --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p,
wenzelm@21624
   777
                        S4 rmhist p, S5 rmhist p, S6 rmhist p)"
wenzelm@21624
   778
  apply clarsimp
wenzelm@21624
   779
  apply (rule conjI)
wenzelm@21624
   780
   apply (force simp: c_def)
wenzelm@21624
   781
  apply (force simp: S1_def S2_def S3_def S4_def S5_def S6_def intro!: S_lemma [temp_use])
wenzelm@21624
   782
  done
wenzelm@21624
   783
wenzelm@21624
   784
lemma Step1_4_7: "|- unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   785
         --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p,
wenzelm@21624
   786
                        S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)"
wenzelm@21624
   787
  apply (rule actionI)
wenzelm@21624
   788
  apply (unfold action_rews)
wenzelm@21624
   789
  apply (rule impI)
wenzelm@21624
   790
  apply (frule Step1_4_7H [temp_use])
wenzelm@21624
   791
  apply (auto simp: e_def c_def r_def m_def rtrner_def resbar_def)
wenzelm@21624
   792
  done
wenzelm@21624
   793
wenzelm@21624
   794
(* Frequently needed abbreviation: distinguish between idling and non-idling
wenzelm@21624
   795
   steps of the implementation, and try to solve the idling case by simplification
wenzelm@21624
   796
*)
wenzelm@21624
   797
ML {*
wenzelm@42786
   798
fun split_idle_tac ctxt =
wenzelm@42786
   799
  SELECT_GOAL
wenzelm@42786
   800
   (TRY (rtac @{thm actionI} 1) THEN
wenzelm@45133
   801
    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
wenzelm@54742
   802
    rewrite_goals_tac ctxt @{thms action_rews} THEN
wenzelm@54742
   803
    forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
wenzelm@51717
   804
    asm_full_simp_tac ctxt 1);
wenzelm@21624
   805
*}
wenzelm@42786
   806
wenzelm@42786
   807
method_setup split_idle = {*
wenzelm@42786
   808
  Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
wenzelm@42786
   809
    >> (K (SIMPLE_METHOD' o split_idle_tac))
wenzelm@42814
   810
*}
wenzelm@42786
   811
wenzelm@21624
   812
(* ----------------------------------------------------------------------
wenzelm@21624
   813
   Combine steps 1.2 and 1.4 to prove that the implementation satisfies
wenzelm@21624
   814
   the specification's next-state relation.
wenzelm@21624
   815
*)
wenzelm@21624
   816
wenzelm@21624
   817
(* Steps that leave all variables unchanged are safe, so I may assume
wenzelm@21624
   818
   that some variable changes in the proof that a step is safe. *)
wenzelm@21624
   819
lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
wenzelm@21624
   820
             --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
wenzelm@21624
   821
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@42786
   822
  apply (split_idle simp: square_def)
wenzelm@21624
   823
  apply force
wenzelm@21624
   824
  done
wenzelm@21624
   825
(* turn into (unsafe, looping!) introduction rule *)
wenzelm@45605
   826
lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
wenzelm@21624
   827
wenzelm@21624
   828
lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   829
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   830
  apply clarsimp
wenzelm@21624
   831
  apply (rule unchanged_safeI)
wenzelm@21624
   832
  apply (rule idle_squareI)
wenzelm@21624
   833
  apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
wenzelm@21624
   834
  done
wenzelm@21624
   835
wenzelm@21624
   836
lemma S2safe: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   837
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   838
  apply clarsimp
wenzelm@21624
   839
  apply (rule unchanged_safeI)
wenzelm@21624
   840
  apply (rule idle_squareI)
wenzelm@21624
   841
  apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
wenzelm@21624
   842
  done
wenzelm@21624
   843
wenzelm@21624
   844
lemma S3safe: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   845
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   846
  apply clarsimp
wenzelm@21624
   847
  apply (rule unchanged_safeI)
wenzelm@21624
   848
  apply (auto dest!: Step1_2_3 [temp_use])
wenzelm@21624
   849
  apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
wenzelm@21624
   850
  done
wenzelm@21624
   851
wenzelm@21624
   852
lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   853
         & (!l. $(MemInv mm l))
wenzelm@21624
   854
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   855
  apply clarsimp
wenzelm@21624
   856
  apply (rule unchanged_safeI)
wenzelm@21624
   857
  apply (auto dest!: Step1_2_4 [temp_use])
wenzelm@21624
   858
     apply (auto simp: square_def UNext_def RNext_def
wenzelm@21624
   859
       dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
wenzelm@21624
   860
  done
wenzelm@21624
   861
wenzelm@21624
   862
lemma S5safe: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   863
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   864
  apply clarsimp
wenzelm@21624
   865
  apply (rule unchanged_safeI)
wenzelm@21624
   866
  apply (auto dest!: Step1_2_5 [temp_use])
wenzelm@21624
   867
  apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
wenzelm@21624
   868
  done
wenzelm@21624
   869
wenzelm@21624
   870
lemma S6safe: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   871
         --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   872
  apply clarsimp
wenzelm@21624
   873
  apply (rule unchanged_safeI)
wenzelm@21624
   874
  apply (auto dest!: Step1_2_6 [temp_use])
wenzelm@21624
   875
    apply (auto simp: square_def UNext_def RNext_def
wenzelm@21624
   876
      dest!: Step1_4_6a [temp_use] Step1_4_6b [temp_use])
wenzelm@21624
   877
  done
wenzelm@21624
   878
wenzelm@21624
   879
(* ----------------------------------------------------------------------
wenzelm@21624
   880
   Step 1.5: Temporal refinement proof, based on previous steps.
wenzelm@21624
   881
*)
wenzelm@21624
   882
wenzelm@21624
   883
section "The liveness part"
wenzelm@21624
   884
wenzelm@21624
   885
(* Liveness assertions for the different implementation states, based on the
wenzelm@21624
   886
   fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas
wenzelm@21624
   887
   for readability. Reuse action proofs from safety part.
wenzelm@21624
   888
*)
wenzelm@21624
   889
wenzelm@21624
   890
(* ------------------------------ State S1 ------------------------------ *)
wenzelm@21624
   891
wenzelm@21624
   892
lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   893
         --> (S1 rmhist p)$ | (S2 rmhist p)$"
wenzelm@42786
   894
  apply split_idle
wenzelm@21624
   895
  apply (auto dest!: Step1_2_1 [temp_use])
wenzelm@21624
   896
  done
wenzelm@21624
   897
wenzelm@21624
   898
(* Show that the implementation can satisfy the high-level fairness requirements
wenzelm@21624
   899
   by entering the state S1 infinitely often.
wenzelm@21624
   900
*)
wenzelm@21624
   901
wenzelm@21624
   902
lemma S1_RNextdisabled: "|- S1 rmhist p -->
wenzelm@21624
   903
         ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
wenzelm@51717
   904
  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
wenzelm@54742
   905
    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
wenzelm@21624
   906
  apply force
wenzelm@21624
   907
  done
wenzelm@21624
   908
wenzelm@21624
   909
lemma S1_Returndisabled: "|- S1 rmhist p -->
wenzelm@21624
   910
         ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
wenzelm@51717
   911
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
wenzelm@39159
   912
    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
wenzelm@21624
   913
wenzelm@21624
   914
lemma RNext_fair: "|- []<>S1 rmhist p
wenzelm@21624
   915
         --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   916
  by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
wenzelm@21624
   917
    elim!: STL4E [temp_use] DmdImplE [temp_use])
wenzelm@21624
   918
wenzelm@21624
   919
lemma Return_fair: "|- []<>S1 rmhist p
wenzelm@21624
   920
         --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
   921
  by (auto simp: WF_alt [try_rewrite]
wenzelm@21624
   922
    intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
wenzelm@21624
   923
wenzelm@21624
   924
(* ------------------------------ State S2 ------------------------------ *)
wenzelm@21624
   925
wenzelm@21624
   926
lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   927
         --> (S2 rmhist p)$ | (S3 rmhist p)$"
wenzelm@42786
   928
  apply split_idle
wenzelm@21624
   929
  apply (auto dest!: Step1_2_2 [temp_use])
wenzelm@21624
   930
  done
wenzelm@21624
   931
wenzelm@21624
   932
lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   933
         & <MClkFwd memCh crCh cst p>_(c p)
wenzelm@21624
   934
         --> (S3 rmhist p)$"
wenzelm@21624
   935
  by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
wenzelm@21624
   936
wenzelm@21624
   937
lemma S2MClkFwd_enabled: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   938
         --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
wenzelm@21624
   939
  apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use])
wenzelm@21624
   940
     apply (cut_tac MI_base)
wenzelm@21624
   941
     apply (blast dest: base_pair)
wenzelm@21624
   942
    apply (simp_all add: S_def S2_def)
wenzelm@21624
   943
  done
wenzelm@21624
   944
wenzelm@21624
   945
lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   946
         & WF(MClkFwd memCh crCh cst p)_(c p)
wenzelm@21624
   947
         --> (S2 rmhist p ~> S3 rmhist p)"
wenzelm@21624
   948
  by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
wenzelm@21624
   949
wenzelm@21624
   950
(* ------------------------------ State S3 ------------------------------ *)
wenzelm@21624
   951
wenzelm@21624
   952
lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   953
         --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
wenzelm@42786
   954
  apply split_idle
wenzelm@21624
   955
  apply (auto dest!: Step1_2_3 [temp_use])
wenzelm@21624
   956
  done
wenzelm@21624
   957
wenzelm@21624
   958
lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   959
         & <RPCNext crCh rmCh rst p>_(r p)
wenzelm@21624
   960
         --> (S4 rmhist p | S6 rmhist p)$"
wenzelm@21624
   961
  apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
wenzelm@21624
   962
  done
wenzelm@21624
   963
wenzelm@21624
   964
lemma S3RPC_enabled: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   965
         --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
wenzelm@21624
   966
  apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
wenzelm@21624
   967
    apply (cut_tac MI_base)
wenzelm@21624
   968
    apply (blast dest: base_pair)
wenzelm@21624
   969
   apply (simp_all add: S_def S3_def)
wenzelm@21624
   970
  done
wenzelm@21624
   971
wenzelm@21624
   972
lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
   973
         & WF(RPCNext crCh rmCh rst p)_(r p)
wenzelm@21624
   974
         --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
wenzelm@21624
   975
  by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
wenzelm@21624
   976
wenzelm@21624
   977
(* ------------- State S4 -------------------------------------------------- *)
wenzelm@21624
   978
wenzelm@21624
   979
lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
   980
        & (ALL l. $MemInv mm l)
wenzelm@21624
   981
        --> (S4 rmhist p)$ | (S5 rmhist p)$"
wenzelm@42786
   982
  apply split_idle
wenzelm@21624
   983
  apply (auto dest!: Step1_2_4 [temp_use])
wenzelm@21624
   984
  done
wenzelm@21624
   985
wenzelm@21624
   986
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
wenzelm@21624
   987
wenzelm@21624
   988
lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult)
wenzelm@21624
   989
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
wenzelm@21624
   990
         --> (S4 rmhist p & ires!p = #NotAResult)$
wenzelm@21624
   991
             | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
wenzelm@42786
   992
  apply split_idle
wenzelm@21624
   993
  apply (auto dest!: Step1_2_4 [temp_use])
wenzelm@21624
   994
  done
wenzelm@21624
   995
wenzelm@21624
   996
lemma S4aRNext_successors: "|- ($(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
         & <RNext rmCh mm ires p>_(m p)
wenzelm@21624
   999
         --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
wenzelm@21624
  1000
  by (auto simp: angle_def
wenzelm@21624
  1001
    dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
wenzelm@21624
  1002
wenzelm@21624
  1003
lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult)
wenzelm@21624
  1004
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
wenzelm@21624
  1005
         --> $Enabled (<RNext rmCh mm ires p>_(m p))"
wenzelm@21624
  1006
  apply (auto simp: m_def intro!: RNext_enabled [temp_use])
wenzelm@21624
  1007
   apply (cut_tac MI_base)
wenzelm@21624
  1008
   apply (blast dest: base_pair)
wenzelm@21624
  1009
  apply (simp add: S_def S4_def)
wenzelm@21624
  1010
  done
wenzelm@21624
  1011
wenzelm@21624
  1012
lemma S4a_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1013
         & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
wenzelm@21624
  1014
         --> (S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1015
              ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
wenzelm@21624
  1016
  by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
wenzelm@21624
  1017
wenzelm@21624
  1018
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
wenzelm@21624
  1019
wenzelm@21624
  1020
lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
wenzelm@21624
  1021
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
wenzelm@21624
  1022
         --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
wenzelm@42786
  1023
  apply (split_idle simp: m_def)
wenzelm@21624
  1024
  apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
wenzelm@21624
  1025
  done
wenzelm@21624
  1026
wenzelm@21624
  1027
lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult)
wenzelm@21624
  1028
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1029
         & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
wenzelm@21624
  1030
         --> (S5 rmhist p)$"
wenzelm@21624
  1031
  by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
wenzelm@21624
  1032
wenzelm@21624
  1033
lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
wenzelm@21624
  1034
         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1035
         & (ALL l. $MemInv mm l)
wenzelm@21624
  1036
         --> $Enabled (<MemReturn rmCh ires p>_(m p))"
wenzelm@21624
  1037
  apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
wenzelm@21624
  1038
   apply (cut_tac MI_base)
wenzelm@21624
  1039
   apply (blast dest: base_pair)
wenzelm@21624
  1040
  apply (simp add: S_def S4_def)
wenzelm@21624
  1041
  done
wenzelm@21624
  1042
wenzelm@21624
  1043
lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))
wenzelm@21624
  1044
         & WF(MemReturn rmCh ires p)_(m p)
wenzelm@21624
  1045
         --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
wenzelm@21624
  1046
  by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
wenzelm@21624
  1047
wenzelm@21624
  1048
(* ------------------------------ State S5 ------------------------------ *)
wenzelm@21624
  1049
wenzelm@21624
  1050
lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1051
         --> (S5 rmhist p)$ | (S6 rmhist p)$"
wenzelm@42786
  1052
  apply split_idle
wenzelm@21624
  1053
  apply (auto dest!: Step1_2_5 [temp_use])
wenzelm@21624
  1054
  done
wenzelm@21624
  1055
wenzelm@21624
  1056
lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
  1057
         & <RPCNext crCh rmCh rst p>_(r p)
wenzelm@21624
  1058
         --> (S6 rmhist p)$"
wenzelm@21624
  1059
  by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
wenzelm@21624
  1060
wenzelm@21624
  1061
lemma S5RPC_enabled: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1062
         --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
wenzelm@21624
  1063
  apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
wenzelm@21624
  1064
    apply (cut_tac MI_base)
wenzelm@21624
  1065
    apply (blast dest: base_pair)
wenzelm@21624
  1066
   apply (simp_all add: S_def S5_def)
wenzelm@21624
  1067
  done
wenzelm@21624
  1068
wenzelm@21624
  1069
lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
  1070
         & WF(RPCNext crCh rmCh rst p)_(r p)
wenzelm@21624
  1071
         --> (S5 rmhist p ~> S6 rmhist p)"
wenzelm@21624
  1072
  by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
wenzelm@21624
  1073
wenzelm@21624
  1074
(* ------------------------------ State S6 ------------------------------ *)
wenzelm@21624
  1075
wenzelm@21624
  1076
lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
wenzelm@21624
  1077
         --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
wenzelm@42786
  1078
  apply split_idle
wenzelm@21624
  1079
  apply (auto dest!: Step1_2_6 [temp_use])
wenzelm@21624
  1080
  done
wenzelm@21624
  1081
wenzelm@21624
  1082
lemma S6MClkReply_successors:
wenzelm@21624
  1083
  "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
wenzelm@21624
  1084
         & <MClkReply memCh crCh cst p>_(c p)
wenzelm@21624
  1085
         --> (S1 rmhist p)$"
wenzelm@21624
  1086
  by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
wenzelm@21624
  1087
wenzelm@21624
  1088
lemma MClkReplyS6:
wenzelm@21624
  1089
  "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
wenzelm@51717
  1090
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
wenzelm@39159
  1091
    @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
wenzelm@39159
  1092
    @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
wenzelm@21624
  1093
wenzelm@21624
  1094
lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
wenzelm@21624
  1095
  apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
wenzelm@21624
  1096
     apply (cut_tac MI_base)
wenzelm@21624
  1097
     apply (blast dest: base_pair)
wenzelm@51717
  1098
    apply (tactic {* ALLGOALS (action_simp_tac (@{context}
wenzelm@39159
  1099
      addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
wenzelm@21624
  1100
  done
wenzelm@21624
  1101
wenzelm@21624
  1102
lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
wenzelm@21624
  1103
         & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)
wenzelm@21624
  1104
         --> []<>(S1 rmhist p)"
wenzelm@21624
  1105
  apply clarsimp
wenzelm@21624
  1106
  apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
wenzelm@21624
  1107
   apply (erule InfiniteEnsures)
wenzelm@21624
  1108
    apply assumption
wenzelm@51717
  1109
   apply (tactic {* action_simp_tac @{context} []
wenzelm@54742
  1110
     (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
wenzelm@21624
  1111
  apply (auto simp: SF_def)
wenzelm@21624
  1112
  apply (erule contrapos_np)
wenzelm@21624
  1113
  apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
wenzelm@21624
  1114
  done
wenzelm@21624
  1115
wenzelm@21624
  1116
(* --------------- aggregate leadsto properties----------------------------- *)
wenzelm@21624
  1117
wenzelm@21624
  1118
lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p
wenzelm@21624
  1119
      ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
wenzelm@21624
  1120
  by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
wenzelm@21624
  1121
wenzelm@21624
  1122
lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1123
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1124
      ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p
wenzelm@21624
  1125
                    ~> S6 rmhist p"
wenzelm@21624
  1126
  by (auto intro!: LatticeDisjunctionIntro [temp_use]
wenzelm@21624
  1127
    S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
wenzelm@21624
  1128
wenzelm@21624
  1129
lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1130
                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
wenzelm@21624
  1131
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1132
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1133
      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
wenzelm@21624
  1134
  apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) |
wenzelm@21624
  1135
    (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p")
wenzelm@21624
  1136
   apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
wenzelm@21624
  1137
     (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in
wenzelm@21624
  1138
     LatticeTransitivity [temp_use])
wenzelm@21624
  1139
   apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
wenzelm@21624
  1140
  apply (rule LatticeDisjunctionIntro [temp_use])
wenzelm@21624
  1141
   apply (erule LatticeTransitivity [temp_use])
wenzelm@21624
  1142
   apply (erule LatticeTriangle2 [temp_use])
wenzelm@21624
  1143
   apply assumption
wenzelm@21624
  1144
  apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
wenzelm@21624
  1145
  done
wenzelm@21624
  1146
wenzelm@21624
  1147
lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
wenzelm@21624
  1148
         sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1149
                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
wenzelm@21624
  1150
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1151
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1152
      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
wenzelm@21624
  1153
  apply (rule LatticeDisjunctionIntro [temp_use])
wenzelm@21624
  1154
   apply (erule LatticeTriangle2 [temp_use])
wenzelm@21624
  1155
   apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
wenzelm@21624
  1156
      apply (auto intro!: S4S5S6LeadstoS6 [temp_use] necT [temp_use]
wenzelm@21624
  1157
        intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
wenzelm@21624
  1158
  done
wenzelm@21624
  1159
wenzelm@21624
  1160
lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p;
wenzelm@21624
  1161
         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
wenzelm@21624
  1162
         sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1163
                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
wenzelm@21624
  1164
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1165
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1166
      ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
wenzelm@21624
  1167
                   ~> S6 rmhist p"
wenzelm@21624
  1168
  apply (rule LatticeDisjunctionIntro [temp_use])
wenzelm@21624
  1169
   apply (rule LatticeTransitivity [temp_use])
wenzelm@21624
  1170
    prefer 2 apply assumption
wenzelm@21624
  1171
   apply (rule S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
wenzelm@21624
  1172
       apply (auto intro!: S3S4S5S6LeadstoS6 [temp_use] necT [temp_use]
wenzelm@21624
  1173
         intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
wenzelm@21624
  1174
  done
wenzelm@21624
  1175
wenzelm@21624
  1176
lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p;
wenzelm@21624
  1177
         sigma |= S2 rmhist p ~> S3 rmhist p;
wenzelm@21624
  1178
         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
wenzelm@21624
  1179
         sigma |= S4 rmhist p & ires!p = #NotAResult
wenzelm@21624
  1180
                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
wenzelm@21624
  1181
         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
wenzelm@21624
  1182
         sigma |= S5 rmhist p ~> S6 rmhist p |]
wenzelm@21624
  1183
      ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
wenzelm@21624
  1184
  apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
wenzelm@21624
  1185
       apply assumption+
wenzelm@21624
  1186
  apply (erule INV_leadsto [temp_use])
wenzelm@21624
  1187
  apply (rule ImplLeadsto_gen [temp_use])
wenzelm@21624
  1188
  apply (rule necT [temp_use])
wenzelm@21624
  1189
  apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use])
wenzelm@21624
  1190
  done
wenzelm@21624
  1191
wenzelm@21624
  1192
lemma S1Infinite: "[| sigma |= ~S1 rmhist p ~> S6 rmhist p;
wenzelm@21624
  1193
         sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
wenzelm@21624
  1194
      ==> sigma |= []<>S1 rmhist p"
wenzelm@21624
  1195
  apply (rule classical)
wenzelm@51717
  1196
  apply (tactic {* asm_lr_simp_tac (@{context} addsimps
wenzelm@54742
  1197
    [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
wenzelm@21624
  1198
  apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
wenzelm@21624
  1199
  done
wenzelm@21624
  1200
wenzelm@21624
  1201
section "Refinement proof (step 1.5)"
wenzelm@21624
  1202
wenzelm@21624
  1203
(* Prove invariants of the implementation:
wenzelm@21624
  1204
   a. memory invariant
wenzelm@21624
  1205
   b. "implementation invariant": always in states S1,...,S6
wenzelm@21624
  1206
*)
wenzelm@21624
  1207
lemma Step1_5_1a: "|- IPImp p --> (ALL l. []$MemInv mm l)"
wenzelm@21624
  1208
  by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
wenzelm@21624
  1209
wenzelm@21624
  1210
lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p)
wenzelm@21624
  1211
         & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
wenzelm@21624
  1212
         --> []ImpInv rmhist p"
wenzelm@42770
  1213
  apply invariant
wenzelm@21624
  1214
   apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
wenzelm@21624
  1215
     dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
wenzelm@21624
  1216
     S3_successors [temp_use] S4_successors [temp_use] S5_successors [temp_use]
wenzelm@21624
  1217
     S6_successors [temp_use])
wenzelm@21624
  1218
  done
wenzelm@21624
  1219
wenzelm@21624
  1220
(*** Initialization ***)
wenzelm@21624
  1221
lemma Step1_5_2a: "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"
wenzelm@21624
  1222
  by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
wenzelm@21624
  1223
wenzelm@21624
  1224
(*** step simulation ***)
wenzelm@21624
  1225
lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
wenzelm@21624
  1226
         & $ImpInv rmhist p & (!l. $MemInv mm l))
wenzelm@21624
  1227
         --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
  1228
  by (auto simp: ImpInv_def elim!: STL4E [temp_use]
wenzelm@21624
  1229
    dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
wenzelm@21624
  1230
    S5safe [temp_use] S6safe [temp_use])
wenzelm@21624
  1231
wenzelm@21624
  1232
(*** Liveness ***)
wenzelm@21624
  1233
lemma GoodImpl: "|- IPImp p & HistP rmhist p
wenzelm@21624
  1234
         -->   Init(ImpInit p & HInit rmhist p)
wenzelm@21624
  1235
             & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1236
             & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p)
wenzelm@21624
  1237
             & ImpLive p"
wenzelm@21624
  1238
  apply clarsimp
wenzelm@21624
  1239
    apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & [] (ImpNext p) &
wenzelm@21624
  1240
      [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)")
wenzelm@21624
  1241
   apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
wenzelm@21624
  1242
       dest!: Step1_5_1b [temp_use])
wenzelm@21624
  1243
      apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
wenzelm@21624
  1244
        ImpLive_def c_def r_def m_def)
wenzelm@21624
  1245
      apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
wenzelm@21624
  1246
        HistP_def Init_def ImpInit_def)
wenzelm@21624
  1247
    apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
wenzelm@21624
  1248
      ImpNext_def c_def r_def m_def split_box_conj [temp_use])
wenzelm@21624
  1249
   apply (force simp: HistP_def)
wenzelm@21624
  1250
  apply (force simp: allT [temp_use] dest!: Step1_5_1a [temp_use])
wenzelm@21624
  1251
  done
wenzelm@21624
  1252
wenzelm@21624
  1253
(* The implementation is infinitely often in state S1... *)
wenzelm@21624
  1254
lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1255
         & [](ALL l. $MemInv mm l)
wenzelm@21624
  1256
         & []($ImpInv rmhist p) & ImpLive p
wenzelm@21624
  1257
         --> []<>S1 rmhist p"
wenzelm@21624
  1258
  apply (clarsimp simp: ImpLive_def)
wenzelm@21624
  1259
  apply (rule S1Infinite)
wenzelm@21624
  1260
   apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
wenzelm@21624
  1261
     intro!: NotS1LeadstoS6 [temp_use] S2_live [temp_use] S3_live [temp_use]
wenzelm@21624
  1262
     S4a_live [temp_use] S4b_live [temp_use] S5_live [temp_use])
wenzelm@21624
  1263
  apply (auto simp: split_box_conj [temp_use] intro!: S6_live [temp_use])
wenzelm@21624
  1264
  done
wenzelm@21624
  1265
wenzelm@21624
  1266
(* ... and therefore satisfies the fairness requirements of the specification *)
wenzelm@21624
  1267
lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1268
         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
wenzelm@21624
  1269
         --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
  1270
  by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
wenzelm@21624
  1271
wenzelm@21624
  1272
lemma Step1_5_3c: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1273
         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
wenzelm@21624
  1274
         --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
wenzelm@21624
  1275
  by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
wenzelm@21624
  1276
wenzelm@21624
  1277
(* QED step of step 1 *)
wenzelm@21624
  1278
lemma Step1: "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
wenzelm@21624
  1279
  by (auto simp: UPSpec_def split_box_conj [temp_use]
wenzelm@21624
  1280
    dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use]
wenzelm@21624
  1281
    Step1_5_3b [temp_use] Step1_5_3c [temp_use])
wenzelm@21624
  1282
wenzelm@21624
  1283
(* ------------------------------ Step 2 ------------------------------ *)
wenzelm@21624
  1284
section "Step 2"
wenzelm@21624
  1285
wenzelm@21624
  1286
lemma Step2_2a: "|- Write rmCh mm ires p l & ImpNext p
wenzelm@21624
  1287
         & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
wenzelm@21624
  1288
         & $ImpInv rmhist p
wenzelm@21624
  1289
         --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
wenzelm@21624
  1290
  apply clarsimp
wenzelm@21624
  1291
  apply (drule WriteS4 [action_use])
wenzelm@21624
  1292
   apply assumption
wenzelm@42786
  1293
  apply split_idle
wenzelm@21624
  1294
  apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
wenzelm@21624
  1295
    S4RPCUnch [temp_use])
wenzelm@21624
  1296
     apply (auto simp: square_def dest: S4Write [temp_use])
wenzelm@21624
  1297
  done
wenzelm@21624
  1298
wenzelm@21624
  1299
lemma Step2_2: "|-   (ALL p. ImpNext p)
wenzelm@21624
  1300
         & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1301
         & (ALL p. $ImpInv rmhist p)
wenzelm@21624
  1302
         & [EX q. Write rmCh mm ires q l]_(mm!l)
wenzelm@21624
  1303
         --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
wenzelm@21624
  1304
  apply (auto intro!: squareCI elim!: squareE)
wenzelm@21624
  1305
  apply (assumption | rule exI Step1_4_4b [action_use])+
wenzelm@21624
  1306
    apply (force intro!: WriteS4 [temp_use])
wenzelm@21624
  1307
   apply (auto dest!: Step2_2a [temp_use])
wenzelm@21624
  1308
  done
wenzelm@21624
  1309
wenzelm@21624
  1310
lemma Step2_lemma: "|- [](  (ALL p. ImpNext p)
wenzelm@21624
  1311
            & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
wenzelm@21624
  1312
            & (ALL p. $ImpInv rmhist p)
wenzelm@21624
  1313
            & [EX q. Write rmCh mm ires q l]_(mm!l))
wenzelm@21624
  1314
         --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
wenzelm@21624
  1315
  by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
wenzelm@21624
  1316
wenzelm@21624
  1317
lemma Step2: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p)
wenzelm@21624
  1318
         --> MSpec memCh mm (resbar rmhist) l"
wenzelm@21624
  1319
  apply (auto simp: MSpec_def)
wenzelm@21624
  1320
   apply (force simp: IPImp_def MSpec_def)
wenzelm@21624
  1321
  apply (auto intro!: Step2_lemma [temp_use] simp: split_box_conj [temp_use] all_box [temp_use])
wenzelm@21624
  1322
     prefer 4
wenzelm@21624
  1323
     apply (force simp: IPImp_def MSpec_def)
wenzelm@21624
  1324
    apply (auto simp: split_box_conj [temp_use] elim!: allE dest!: GoodImpl [temp_use])
wenzelm@21624
  1325
  done
wenzelm@21624
  1326
wenzelm@21624
  1327
(* ----------------------------- Main theorem --------------------------------- *)
wenzelm@21624
  1328
section "Memory implementation"
wenzelm@21624
  1329
wenzelm@21624
  1330
(* The combination of a legal caller, the memory clerk, the RPC component,
wenzelm@21624
  1331
   and a reliable memory implement the unreliable memory.
wenzelm@21624
  1332
*)
wenzelm@21624
  1333
wenzelm@21624
  1334
(* Implementation of internal specification by combination of implementation
wenzelm@21624
  1335
   and history variable with explicit refinement mapping
wenzelm@21624
  1336
*)
wenzelm@21624
  1337
lemma Impl_IUSpec: "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"
wenzelm@21624
  1338
  by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def
wenzelm@21624
  1339
    RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use])
wenzelm@21624
  1340
wenzelm@21624
  1341
(* The main theorem: introduce hiding and eliminate history variable. *)
wenzelm@21624
  1342
lemma Implementation: "|- Implementation --> USpec memCh"
wenzelm@21624
  1343
  apply clarsimp
wenzelm@21624
  1344
  apply (frule History [temp_use])
wenzelm@21624
  1345
  apply (auto simp: USpec_def intro: eexI [temp_use] Impl_IUSpec [temp_use]
wenzelm@21624
  1346
    MI_base [temp_use] elim!: eexE)
wenzelm@21624
  1347
  done
wenzelm@3807
  1348
wenzelm@3807
  1349
end