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