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