src/HOL/TLA/Memory/MemoryImplementation.thy
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 58249 180f1b3508ed
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
     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 ctxt =>
   229     if Config.get ctxt config_fast_solver
   230     then assume_tac ORELSE' (etac notE)
   231     else K no_tac);
   232 *}
   233 
   234 setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
   235 
   236 ML {* val temp_elim = make_elim oo 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 (@{context} addsimps [@{thm HInit_def}]) [] [] 1 *})
   252    apply (erule fun_cong)
   253   apply (tactic {* action_simp_tac (@{context} 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 (@{context} 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 @{context} @{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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} 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 (@{context} addsimps [@{thm ImpNext_def}]) []
   569       (map (temp_elim @{context})
   570         [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
   571    using [[fast_solver]]
   572    apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
   573   done
   574 
   575 lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   576          & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
   577          --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
   578              & unchanged (e p, r p, m p, rmhist!p)"
   579   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   580     (map (temp_elim @{context})
   581       [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
   582    using [[fast_solver]]
   583    apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
   584   done
   585 
   586 lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   587          & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
   588          --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
   589              | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   590   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   591     (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   592   apply (tactic {* action_simp_tac @{context} []
   593     (@{thm squareE} ::
   594       map (temp_elim @{context}) [@{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 (@{context} addsimps [@{thm ImpNext_def}]) []
   605     (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   606   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
   607     (@{thm squareE} ::
   608       map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
   609   apply (auto dest!: S4Hist [temp_use])
   610   done
   611 
   612 lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   613               & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
   614          --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
   615              | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   616   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   617     (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
   618   apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
   619    using [[fast_solver]]
   620    apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
   621   done
   622 
   623 lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   624               & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
   625          --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
   626              | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   627   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   628     (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   629   apply (tactic {* action_simp_tac @{context} []
   630     (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
   631      apply (auto dest: S6Hist [temp_use])
   632   done
   633 
   634 (* --------------------------------------------------------------------------
   635    Step 1.3: S1 implies the barred initial condition.
   636 *)
   637 
   638 section "Initialization (Step 1.3)"
   639 
   640 lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
   641   by (tactic {* action_simp_tac (@{context} addsimps [@{thm resbar_def},
   642     @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
   643 
   644 (* ----------------------------------------------------------------------
   645    Step 1.4: Implementation's next-state relation simulates specification's
   646              next-state relation (with appropriate substitutions)
   647 *)
   648 
   649 section "Step simulation (Step 1.4)"
   650 
   651 lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
   652          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   653   using [[fast_solver]]
   654   by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def)
   655 
   656 lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
   657          & unchanged (e p, r p, m p, rmhist!p)
   658          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   659   by (tactic {* action_simp_tac
   660     (@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
   661     @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
   662 
   663 lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
   664          & unchanged (e p, c p, m p, rmhist!p)
   665          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   666   apply clarsimp
   667   apply (drule S3_excl [temp_use] S4_excl [temp_use])+
   668   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
   669     @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
   670   done
   671 
   672 lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
   673          & unchanged (e p, c p, m p)
   674          --> MemFail memCh (resbar rmhist) p"
   675   apply clarsimp
   676   apply (drule S6_excl [temp_use])
   677   apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
   678     apply (force simp: S3_def S_def)
   679    apply (auto simp: Return_def)
   680   done
   681 
   682 lemma Step1_4_4a1: "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
   683          & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l
   684          --> ReadInner memCh mm (resbar rmhist) p l"
   685   apply clarsimp
   686   apply (drule S4_excl [temp_use])+
   687   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
   688     @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
   689      apply (auto simp: resbar_def)
   690        apply (tactic {* ALLGOALS (action_simp_tac
   691                 (@{context} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
   692                   @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
   693                 [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
   694   done
   695 
   696 lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
   697          & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l))
   698          --> Read memCh mm (resbar rmhist) p"
   699   by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
   700 
   701 lemma Step1_4_4b1: "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
   702          & unchanged (e p, c p, r p, rmhist!p)
   703          --> WriteInner memCh mm (resbar rmhist) p l v"
   704   apply clarsimp
   705   apply (drule S4_excl [temp_use])+
   706   apply (tactic {* action_simp_tac (@{context} addsimps
   707     [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
   708     @{thm c_def}, @{thm m_def}]) [] [] 1 *})
   709      apply (auto simp: resbar_def)
   710     apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
   711       [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
   712       @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
   713   done
   714 
   715 lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
   716          & unchanged (e p, c p, r p, rmhist!p)
   717          --> Write memCh mm (resbar rmhist) p l"
   718   by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
   719 
   720 lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
   721          & unchanged (e p, c p, r p)
   722          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   723   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
   724     @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
   725   apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   726   using [[fast_solver]]
   727   apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
   728   done
   729 
   730 lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
   731          & unchanged (e p, c p, m p)
   732          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   733   apply clarsimp
   734   apply (drule S5_excl [temp_use] S6_excl [temp_use])+
   735   apply (auto simp: e_def c_def m_def resbar_def)
   736    apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
   737   done
   738 
   739 lemma Step1_4_5b: "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
   740          & unchanged (e p, c p, m p)
   741          --> MemFail memCh (resbar rmhist) p"
   742   apply clarsimp
   743   apply (drule S6_excl [temp_use])
   744   apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
   745    apply (auto simp: S5_def S_def)
   746   done
   747 
   748 lemma Step1_4_6a: "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
   749          & unchanged (e p, r p, m p)
   750          --> MemReturn memCh (resbar rmhist) p"
   751   apply clarsimp
   752   apply (drule S6_excl [temp_use])+
   753   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
   754     @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
   755     @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
   756     apply simp_all (* simplify if-then-else *)
   757     apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
   758       [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
   759   done
   760 
   761 lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
   762          & unchanged (e p, r p, m p, rmhist!p)
   763          --> MemFail memCh (resbar rmhist) p"
   764   apply clarsimp
   765   apply (drule S3_excl [temp_use])+
   766   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def},
   767     @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
   768    apply (auto simp: S6_def S_def)
   769   done
   770 
   771 lemma S_lemma: "|- unchanged (e p, c p, r p, m p, rmhist!p)
   772          --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
   773   by (auto simp: e_def c_def r_def m_def caller_def rtrner_def S_def Calling_def)
   774 
   775 lemma Step1_4_7H: "|- unchanged (e p, c p, r p, m p, rmhist!p)
   776          --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p,
   777                         S4 rmhist p, S5 rmhist p, S6 rmhist p)"
   778   apply clarsimp
   779   apply (rule conjI)
   780    apply (force simp: c_def)
   781   apply (force simp: S1_def S2_def S3_def S4_def S5_def S6_def intro!: S_lemma [temp_use])
   782   done
   783 
   784 lemma Step1_4_7: "|- unchanged (e p, c p, r p, m p, rmhist!p)
   785          --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p,
   786                         S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)"
   787   apply (rule actionI)
   788   apply (unfold action_rews)
   789   apply (rule impI)
   790   apply (frule Step1_4_7H [temp_use])
   791   apply (auto simp: e_def c_def r_def m_def rtrner_def resbar_def)
   792   done
   793 
   794 (* Frequently needed abbreviation: distinguish between idling and non-idling
   795    steps of the implementation, and try to solve the idling case by simplification
   796 *)
   797 ML {*
   798 fun split_idle_tac ctxt =
   799   SELECT_GOAL
   800    (TRY (rtac @{thm actionI} 1) THEN
   801     Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
   802     rewrite_goals_tac ctxt @{thms action_rews} THEN
   803     forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
   804     asm_full_simp_tac ctxt 1);
   805 *}
   806 
   807 method_setup split_idle = {*
   808   Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
   809     >> (K (SIMPLE_METHOD' o split_idle_tac))
   810 *}
   811 
   812 (* ----------------------------------------------------------------------
   813    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
   814    the specification's next-state relation.
   815 *)
   816 
   817 (* Steps that leave all variables unchanged are safe, so I may assume
   818    that some variable changes in the proof that a step is safe. *)
   819 lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
   820              --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
   821          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   822   apply (split_idle simp: square_def)
   823   apply force
   824   done
   825 (* turn into (unsafe, looping!) introduction rule *)
   826 lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
   827 
   828 lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   829          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   830   apply clarsimp
   831   apply (rule unchanged_safeI)
   832   apply (rule idle_squareI)
   833   apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
   834   done
   835 
   836 lemma S2safe: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   837          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   838   apply clarsimp
   839   apply (rule unchanged_safeI)
   840   apply (rule idle_squareI)
   841   apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
   842   done
   843 
   844 lemma S3safe: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   845          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   846   apply clarsimp
   847   apply (rule unchanged_safeI)
   848   apply (auto dest!: Step1_2_3 [temp_use])
   849   apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
   850   done
   851 
   852 lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   853          & (!l. $(MemInv mm l))
   854          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   855   apply clarsimp
   856   apply (rule unchanged_safeI)
   857   apply (auto dest!: Step1_2_4 [temp_use])
   858      apply (auto simp: square_def UNext_def RNext_def
   859        dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
   860   done
   861 
   862 lemma S5safe: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   863          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   864   apply clarsimp
   865   apply (rule unchanged_safeI)
   866   apply (auto dest!: Step1_2_5 [temp_use])
   867   apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
   868   done
   869 
   870 lemma S6safe: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   871          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   872   apply clarsimp
   873   apply (rule unchanged_safeI)
   874   apply (auto dest!: Step1_2_6 [temp_use])
   875     apply (auto simp: square_def UNext_def RNext_def
   876       dest!: Step1_4_6a [temp_use] Step1_4_6b [temp_use])
   877   done
   878 
   879 (* ----------------------------------------------------------------------
   880    Step 1.5: Temporal refinement proof, based on previous steps.
   881 *)
   882 
   883 section "The liveness part"
   884 
   885 (* Liveness assertions for the different implementation states, based on the
   886    fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas
   887    for readability. Reuse action proofs from safety part.
   888 *)
   889 
   890 (* ------------------------------ State S1 ------------------------------ *)
   891 
   892 lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   893          --> (S1 rmhist p)$ | (S2 rmhist p)$"
   894   apply split_idle
   895   apply (auto dest!: Step1_2_1 [temp_use])
   896   done
   897 
   898 (* Show that the implementation can satisfy the high-level fairness requirements
   899    by entering the state S1 infinitely often.
   900 *)
   901 
   902 lemma S1_RNextdisabled: "|- S1 rmhist p -->
   903          ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   904   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
   905     @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
   906   apply force
   907   done
   908 
   909 lemma S1_Returndisabled: "|- S1 rmhist p -->
   910          ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   911   by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
   912     @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
   913 
   914 lemma RNext_fair: "|- []<>S1 rmhist p
   915          --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   916   by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
   917     elim!: STL4E [temp_use] DmdImplE [temp_use])
   918 
   919 lemma Return_fair: "|- []<>S1 rmhist p
   920          --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   921   by (auto simp: WF_alt [try_rewrite]
   922     intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
   923 
   924 (* ------------------------------ State S2 ------------------------------ *)
   925 
   926 lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   927          --> (S2 rmhist p)$ | (S3 rmhist p)$"
   928   apply split_idle
   929   apply (auto dest!: Step1_2_2 [temp_use])
   930   done
   931 
   932 lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   933          & <MClkFwd memCh crCh cst p>_(c p)
   934          --> (S3 rmhist p)$"
   935   by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
   936 
   937 lemma S2MClkFwd_enabled: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   938          --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
   939   apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use])
   940      apply (cut_tac MI_base)
   941      apply (blast dest: base_pair)
   942     apply (simp_all add: S_def S2_def)
   943   done
   944 
   945 lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   946          & WF(MClkFwd memCh crCh cst p)_(c p)
   947          --> (S2 rmhist p ~> S3 rmhist p)"
   948   by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
   949 
   950 (* ------------------------------ State S3 ------------------------------ *)
   951 
   952 lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   953          --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
   954   apply split_idle
   955   apply (auto dest!: Step1_2_3 [temp_use])
   956   done
   957 
   958 lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   959          & <RPCNext crCh rmCh rst p>_(r p)
   960          --> (S4 rmhist p | S6 rmhist p)$"
   961   apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
   962   done
   963 
   964 lemma S3RPC_enabled: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   965          --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
   966   apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
   967     apply (cut_tac MI_base)
   968     apply (blast dest: base_pair)
   969    apply (simp_all add: S_def S3_def)
   970   done
   971 
   972 lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
   973          & WF(RPCNext crCh rmCh rst p)_(r p)
   974          --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
   975   by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
   976 
   977 (* ------------- State S4 -------------------------------------------------- *)
   978 
   979 lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   980         & (ALL l. $MemInv mm l)
   981         --> (S4 rmhist p)$ | (S5 rmhist p)$"
   982   apply split_idle
   983   apply (auto dest!: Step1_2_4 [temp_use])
   984   done
   985 
   986 (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
   987 
   988 lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult)
   989          & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
   990          --> (S4 rmhist p & ires!p = #NotAResult)$
   991              | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
   992   apply split_idle
   993   apply (auto dest!: Step1_2_4 [temp_use])
   994   done
   995 
   996 lemma S4aRNext_successors: "|- ($(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          & <RNext rmCh mm ires p>_(m p)
   999          --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
  1000   by (auto simp: angle_def
  1001     dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
  1002 
  1003 lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult)
  1004          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
  1005          --> $Enabled (<RNext rmCh mm ires p>_(m p))"
  1006   apply (auto simp: m_def intro!: RNext_enabled [temp_use])
  1007    apply (cut_tac MI_base)
  1008    apply (blast dest: base_pair)
  1009   apply (simp add: S_def S4_def)
  1010   done
  1011 
  1012 lemma S4a_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
  1013          & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
  1014          --> (S4 rmhist p & ires!p = #NotAResult
  1015               ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
  1016   by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
  1017 
  1018 (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
  1019 
  1020 lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
  1021          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
  1022          --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
  1023   apply (split_idle simp: m_def)
  1024   apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
  1025   done
  1026 
  1027 lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult)
  1028          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
  1029          & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
  1030          --> (S5 rmhist p)$"
  1031   by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
  1032 
  1033 lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
  1034          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
  1035          & (ALL l. $MemInv mm l)
  1036          --> $Enabled (<MemReturn rmCh ires p>_(m p))"
  1037   apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
  1038    apply (cut_tac MI_base)
  1039    apply (blast dest: base_pair)
  1040   apply (simp add: S_def S4_def)
  1041   done
  1042 
  1043 lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))
  1044          & WF(MemReturn rmCh ires p)_(m p)
  1045          --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
  1046   by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
  1047 
  1048 (* ------------------------------ State S5 ------------------------------ *)
  1049 
  1050 lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
  1051          --> (S5 rmhist p)$ | (S6 rmhist p)$"
  1052   apply split_idle
  1053   apply (auto dest!: Step1_2_5 [temp_use])
  1054   done
  1055 
  1056 lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
  1057          & <RPCNext crCh rmCh rst p>_(r p)
  1058          --> (S6 rmhist p)$"
  1059   by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
  1060 
  1061 lemma S5RPC_enabled: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
  1062          --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
  1063   apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
  1064     apply (cut_tac MI_base)
  1065     apply (blast dest: base_pair)
  1066    apply (simp_all add: S_def S5_def)
  1067   done
  1068 
  1069 lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
  1070          & WF(RPCNext crCh rmCh rst p)_(r p)
  1071          --> (S5 rmhist p ~> S6 rmhist p)"
  1072   by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
  1073 
  1074 (* ------------------------------ State S6 ------------------------------ *)
  1075 
  1076 lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
  1077          --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
  1078   apply split_idle
  1079   apply (auto dest!: Step1_2_6 [temp_use])
  1080   done
  1081 
  1082 lemma S6MClkReply_successors:
  1083   "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
  1084          & <MClkReply memCh crCh cst p>_(c p)
  1085          --> (S1 rmhist p)$"
  1086   by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
  1087 
  1088 lemma MClkReplyS6:
  1089   "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
  1090   by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
  1091     @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
  1092     @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
  1093 
  1094 lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
  1095   apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
  1096      apply (cut_tac MI_base)
  1097      apply (blast dest: base_pair)
  1098     apply (tactic {* ALLGOALS (action_simp_tac (@{context}
  1099       addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
  1100   done
  1101 
  1102 lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
  1103          & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)
  1104          --> []<>(S1 rmhist p)"
  1105   apply clarsimp
  1106   apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
  1107    apply (erule InfiniteEnsures)
  1108     apply assumption
  1109    apply (tactic {* action_simp_tac @{context} []
  1110      (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
  1111   apply (auto simp: SF_def)
  1112   apply (erule contrapos_np)
  1113   apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
  1114   done
  1115 
  1116 (* --------------- aggregate leadsto properties----------------------------- *)
  1117 
  1118 lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p
  1119       ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
  1120   by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
  1121 
  1122 lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
  1123          sigma |= S5 rmhist p ~> S6 rmhist p |]
  1124       ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p
  1125                     ~> S6 rmhist p"
  1126   by (auto intro!: LatticeDisjunctionIntro [temp_use]
  1127     S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
  1128 
  1129 lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult
  1130                   ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
  1131          sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
  1132          sigma |= S5 rmhist p ~> S6 rmhist p |]
  1133       ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
  1134   apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) |
  1135     (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p")
  1136    apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
  1137      (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in
  1138      LatticeTransitivity [temp_use])
  1139    apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
  1140   apply (rule LatticeDisjunctionIntro [temp_use])
  1141    apply (erule LatticeTransitivity [temp_use])
  1142    apply (erule LatticeTriangle2 [temp_use])
  1143    apply assumption
  1144   apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
  1145   done
  1146 
  1147 lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
  1148          sigma |= S4 rmhist p & ires!p = #NotAResult
  1149                   ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
  1150          sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
  1151          sigma |= S5 rmhist p ~> S6 rmhist p |]
  1152       ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
  1153   apply (rule LatticeDisjunctionIntro [temp_use])
  1154    apply (erule LatticeTriangle2 [temp_use])
  1155    apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
  1156       apply (auto intro!: S4S5S6LeadstoS6 [temp_use] necT [temp_use]
  1157         intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
  1158   done
  1159 
  1160 lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p;
  1161          sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
  1162          sigma |= S4 rmhist p & ires!p = #NotAResult
  1163                   ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
  1164          sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
  1165          sigma |= S5 rmhist p ~> S6 rmhist p |]
  1166       ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
  1167                    ~> S6 rmhist p"
  1168   apply (rule LatticeDisjunctionIntro [temp_use])
  1169    apply (rule LatticeTransitivity [temp_use])
  1170     prefer 2 apply assumption
  1171    apply (rule S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
  1172        apply (auto intro!: S3S4S5S6LeadstoS6 [temp_use] necT [temp_use]
  1173          intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
  1174   done
  1175 
  1176 lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p;
  1177          sigma |= S2 rmhist p ~> S3 rmhist p;
  1178          sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
  1179          sigma |= S4 rmhist p & ires!p = #NotAResult
  1180                   ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
  1181          sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
  1182          sigma |= S5 rmhist p ~> S6 rmhist p |]
  1183       ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
  1184   apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
  1185        apply assumption+
  1186   apply (erule INV_leadsto [temp_use])
  1187   apply (rule ImplLeadsto_gen [temp_use])
  1188   apply (rule necT [temp_use])
  1189   apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use])
  1190   done
  1191 
  1192 lemma S1Infinite: "[| sigma |= ~S1 rmhist p ~> S6 rmhist p;
  1193          sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
  1194       ==> sigma |= []<>S1 rmhist p"
  1195   apply (rule classical)
  1196   apply (tactic {* asm_lr_simp_tac (@{context} addsimps
  1197     [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
  1198   apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
  1199   done
  1200 
  1201 section "Refinement proof (step 1.5)"
  1202 
  1203 (* Prove invariants of the implementation:
  1204    a. memory invariant
  1205    b. "implementation invariant": always in states S1,...,S6
  1206 *)
  1207 lemma Step1_5_1a: "|- IPImp p --> (ALL l. []$MemInv mm l)"
  1208   by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
  1209 
  1210 lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p)
  1211          & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
  1212          --> []ImpInv rmhist p"
  1213   apply invariant
  1214    apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
  1215      dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
  1216      S3_successors [temp_use] S4_successors [temp_use] S5_successors [temp_use]
  1217      S6_successors [temp_use])
  1218   done
  1219 
  1220 (*** Initialization ***)
  1221 lemma Step1_5_2a: "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"
  1222   by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
  1223 
  1224 (*** step simulation ***)
  1225 lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
  1226          & $ImpInv rmhist p & (!l. $MemInv mm l))
  1227          --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
  1228   by (auto simp: ImpInv_def elim!: STL4E [temp_use]
  1229     dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
  1230     S5safe [temp_use] S6safe [temp_use])
  1231 
  1232 (*** Liveness ***)
  1233 lemma GoodImpl: "|- IPImp p & HistP rmhist p
  1234          -->   Init(ImpInit p & HInit rmhist p)
  1235              & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
  1236              & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p)
  1237              & ImpLive p"
  1238   apply clarsimp
  1239     apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & [] (ImpNext p) &
  1240       [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)")
  1241    apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
  1242        dest!: Step1_5_1b [temp_use])
  1243       apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
  1244         ImpLive_def c_def r_def m_def)
  1245       apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
  1246         HistP_def Init_def ImpInit_def)
  1247     apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
  1248       ImpNext_def c_def r_def m_def split_box_conj [temp_use])
  1249    apply (force simp: HistP_def)
  1250   apply (force simp: allT [temp_use] dest!: Step1_5_1a [temp_use])
  1251   done
  1252 
  1253 (* The implementation is infinitely often in state S1... *)
  1254 lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
  1255          & [](ALL l. $MemInv mm l)
  1256          & []($ImpInv rmhist p) & ImpLive p
  1257          --> []<>S1 rmhist p"
  1258   apply (clarsimp simp: ImpLive_def)
  1259   apply (rule S1Infinite)
  1260    apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
  1261      intro!: NotS1LeadstoS6 [temp_use] S2_live [temp_use] S3_live [temp_use]
  1262      S4a_live [temp_use] S4b_live [temp_use] S5_live [temp_use])
  1263   apply (auto simp: split_box_conj [temp_use] intro!: S6_live [temp_use])
  1264   done
  1265 
  1266 (* ... and therefore satisfies the fairness requirements of the specification *)
  1267 lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
  1268          & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
  1269          --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
  1270   by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
  1271 
  1272 lemma Step1_5_3c: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
  1273          & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
  1274          --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
  1275   by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
  1276 
  1277 (* QED step of step 1 *)
  1278 lemma Step1: "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
  1279   by (auto simp: UPSpec_def split_box_conj [temp_use]
  1280     dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use]
  1281     Step1_5_3b [temp_use] Step1_5_3c [temp_use])
  1282 
  1283 (* ------------------------------ Step 2 ------------------------------ *)
  1284 section "Step 2"
  1285 
  1286 lemma Step2_2a: "|- Write rmCh mm ires p l & ImpNext p
  1287          & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
  1288          & $ImpInv rmhist p
  1289          --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
  1290   apply clarsimp
  1291   apply (drule WriteS4 [action_use])
  1292    apply assumption
  1293   apply split_idle
  1294   apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
  1295     S4RPCUnch [temp_use])
  1296      apply (auto simp: square_def dest: S4Write [temp_use])
  1297   done
  1298 
  1299 lemma Step2_2: "|-   (ALL p. ImpNext p)
  1300          & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
  1301          & (ALL p. $ImpInv rmhist p)
  1302          & [EX q. Write rmCh mm ires q l]_(mm!l)
  1303          --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
  1304   apply (auto intro!: squareCI elim!: squareE)
  1305   apply (assumption | rule exI Step1_4_4b [action_use])+
  1306     apply (force intro!: WriteS4 [temp_use])
  1307    apply (auto dest!: Step2_2a [temp_use])
  1308   done
  1309 
  1310 lemma Step2_lemma: "|- [](  (ALL p. ImpNext p)
  1311             & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
  1312             & (ALL p. $ImpInv rmhist p)
  1313             & [EX q. Write rmCh mm ires q l]_(mm!l))
  1314          --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
  1315   by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
  1316 
  1317 lemma Step2: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p)
  1318          --> MSpec memCh mm (resbar rmhist) l"
  1319   apply (auto simp: MSpec_def)
  1320    apply (force simp: IPImp_def MSpec_def)
  1321   apply (auto intro!: Step2_lemma [temp_use] simp: split_box_conj [temp_use] all_box [temp_use])
  1322      prefer 4
  1323      apply (force simp: IPImp_def MSpec_def)
  1324     apply (auto simp: split_box_conj [temp_use] elim!: allE dest!: GoodImpl [temp_use])
  1325   done
  1326 
  1327 (* ----------------------------- Main theorem --------------------------------- *)
  1328 section "Memory implementation"
  1329 
  1330 (* The combination of a legal caller, the memory clerk, the RPC component,
  1331    and a reliable memory implement the unreliable memory.
  1332 *)
  1333 
  1334 (* Implementation of internal specification by combination of implementation
  1335    and history variable with explicit refinement mapping
  1336 *)
  1337 lemma Impl_IUSpec: "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"
  1338   by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def
  1339     RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use])
  1340 
  1341 (* The main theorem: introduce hiding and eliminate history variable. *)
  1342 lemma Implementation: "|- Implementation --> USpec memCh"
  1343   apply clarsimp
  1344   apply (frule History [temp_use])
  1345   apply (auto simp: USpec_def intro: eexI [temp_use] Impl_IUSpec [temp_use]
  1346     MI_base [temp_use] elim!: eexE)
  1347   done
  1348 
  1349 end