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