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