src/HOL/TLA/Memory/MemoryImplementation.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 6919 7985b229806c
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:        MemoryImplementation.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     RPC-Memory example: Memory implementation (ML file)
     7 
     8     The main theorem is theorem "Implementation" at the end of this file,
     9     which shows that the composition of a reliable memory, an RPC component, and
    10     a memory clerk implements an unreliable memory. The files "MIsafe.ML" and
    11     "MIlive.ML" contain lower-level lemmas for the safety and liveness parts.
    12 
    13     Steps are (roughly) numbered as in the hand proof.
    14 *)
    15 
    16 (* --------------------------- automatic prover --------------------------- *)
    17 
    18 val MI_css = (claset(), simpset());
    19 
    20 (* A more aggressive variant that tries to solve subgoals by assumption
    21    or contradiction during the simplification.
    22    THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
    23    (but it can be a lot faster than MI_css)
    24 *)
    25 val MI_fast_css =
    26   let 
    27     val (cs,ss) = MI_css
    28   in
    29     (cs addSEs [squareE], ss addSSolver (fn thms => assume_tac ORELSE' (etac notE)))
    30 end;
    31 
    32 val temp_elim = make_elim o temp_use;
    33 
    34 (****************************** The history variable ******************************)
    35 section "History variable";
    36 
    37 qed_goal "HistoryLemma" MemoryImplementation.thy
    38    "|- Init(!p. ImpInit p) & [](!p. ImpNext p)  \
    39 \      --> (EEX rmhist. Init(! p. HInit rmhist p) \
    40 \                     & [](!p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
    41    (fn _ => [Clarsimp_tac 1,
    42              rtac historyI 1, TRYALL atac, rtac MI_base 1,
    43              action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1,
    44              etac fun_cong 1,
    45              action_simp_tac (simpset() addsimps [HNext_def]) [busy_squareI] [] 1,
    46              etac fun_cong 1
    47             ]);
    48 
    49 qed_goal "History" MemoryImplementation.thy
    50    "|- Implementation --> (EEX rmhist. Hist rmhist)"
    51    (fn _ => [Clarsimp_tac 1,
    52              rtac ((temp_use HistoryLemma) RS eex_mono) 1,
    53              force_tac (MI_css 
    54                         addsimps2 [Hist_def,HistP_def,Init_def,all_box,split_box_conj]) 3,
    55              auto_tac (MI_css
    56                        addsimps2 [Implementation_def,MClkISpec_def,RPCISpec_def,IRSpec_def,
    57                                   MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
    58                                   ImpInit_def,Init_def,ImpNext_def,
    59                                   c_def,r_def,m_def,all_box,split_box_conj])
    60             ]);
    61 
    62 (******************************** The safety part *********************************)
    63 
    64 section "The safety part";
    65 
    66 (* ------------------------- Include lower-level lemmas ------------------------- *)
    67 use "MIsafe.ML";
    68 
    69 section "Correctness of predicate-action diagram";
    70 
    71 
    72 (* ========== Step 1.1 ================================================= *)
    73 (* The implementation's initial condition implies the state predicate S1 *)
    74 
    75 qed_goal "Step1_1" MemoryImplementation.thy
    76    "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
    77    (fn _ => [auto_tac (MI_fast_css
    78 		       addsimps2 [MVNROKBA_def,MClkInit_def,RPCInit_def,PInit_def,
    79 			          HInit_def,ImpInit_def,S_def,S1_def])
    80 	    ]);
    81 
    82 (* ========== Step 1.2 ================================================== *)
    83 (* Figure 16 is a predicate-action diagram for the implementation. *)
    84 
    85 qed_goal "Step1_2_1" MemoryImplementation.thy
    86    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
    87 \             & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p \
    88 \      --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
    89    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
    90                              (map temp_elim [S1ClerkUnch,S1RPCUnch,S1MemUnch,S1Hist]) 1,
    91              auto_tac (MI_fast_css addSIs2 [S1Env])
    92 	    ]);
    93 
    94 qed_goal "Step1_2_2" MemoryImplementation.thy
    95    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
    96 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p \
    97 \      --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p & unchanged (e p, r p, m p, rmhist!p)"
    98    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
    99                              (map temp_elim [S2EnvUnch,S2RPCUnch,S2MemUnch,S2Hist]) 1,
   100 	     auto_tac (MI_fast_css addSIs2 [S2Clerk,S2Forward])
   101 	    ]);
   102 
   103 qed_goal "Step1_2_3" MemoryImplementation.thy
   104    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   105 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p \
   106 \      --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) \
   107 \        | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   108    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   109 	          (map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1,
   110              action_simp_tac (simpset()) [] 
   111                   (squareE::map temp_elim [S3RPC,S3Forward,S3Fail]) 1,
   112              auto_tac (MI_css addDs2 [S3Hist])
   113 	    ]);
   114 
   115 qed_goal "Step1_2_4" MemoryImplementation.thy
   116    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   117 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) \
   118 \             & $S4 rmhist p & (!l. $(MemInv mm l))     \
   119 \      --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p)) \
   120 \        | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p)) \
   121 \        | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   122    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   123                              (map temp_elim [S4EnvUnch,S4ClerkUnch,S4RPCUnch]) 1,
   124              action_simp_tac (simpset() addsimps [RNext_def]) []
   125                              (squareE::map temp_elim [S4Read,S4Write,S4Return]) 1,
   126              auto_tac (MI_css addDs2 [S4Hist])
   127             ]);
   128 
   129 qed_goal "Step1_2_5" MemoryImplementation.thy
   130    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   131 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p \
   132 \      --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p)) \
   133 \        | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   134    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   135                              (map temp_elim [S5EnvUnch,S5ClerkUnch,S5MemUnch,S5Hist]) 1,
   136 	     action_simp_tac (simpset()) [] [squareE, temp_elim S5RPC] 1,
   137 	     auto_tac (MI_fast_css addSDs2 [S5Reply,S5Fail])
   138 	    ]);
   139 
   140 qed_goal "Step1_2_6" MemoryImplementation.thy
   141    "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p  \
   142 \             & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p \
   143 \      --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))\
   144 \        | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   145    (fn _ => [action_simp_tac (simpset() addsimps [ImpNext_def]) []
   146                              (map temp_elim [S6EnvUnch,S6RPCUnch,S6MemUnch]) 1,
   147              action_simp_tac (simpset()) []
   148                              (squareE::map temp_elim [S6Clerk,S6Retry,S6Reply]) 1,
   149              auto_tac (MI_css addDs2 [S6Hist])
   150             ]);
   151 
   152 (* --------------------------------------------------------------------------
   153    Step 1.3: S1 implies the barred initial condition.
   154 *)
   155 
   156 section "Initialization (Step 1.3)";
   157 
   158 qed_goal "Step1_3" MemoryImplementation.thy 
   159    "|- S1 rmhist p --> PInit (resbar rmhist) p"
   160    (fn _ => [action_simp_tac (simpset() addsimps [resbar_def,PInit_def,S_def,S1_def])
   161                              [] [] 1
   162             ]);
   163 
   164 (* ----------------------------------------------------------------------
   165    Step 1.4: Implementation's next-state relation simulates specification's
   166              next-state relation (with appropriate substitutions)
   167 *)
   168 
   169 section "Step simulation (Step 1.4)";
   170 
   171 qed_goal "Step1_4_1" MemoryImplementation.thy
   172    "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p) \
   173 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   174   (fn _ => [ auto_tac (MI_fast_css addsimps2 [c_def,r_def,m_def,resbar_def]) ]);
   175 
   176 qed_goal "Step1_4_2" MemoryImplementation.thy
   177    "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$  \
   178 \                & unchanged (e p, r p, m p, rmhist!p) \
   179 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   180   (fn _ => [action_simp_tac
   181                 (simpset() addsimps [MClkFwd_def, e_def, r_def, m_def, resbar_def,
   182                                      S_def, S2_def, S3_def]) [] [] 1
   183            ]);
   184 
   185 qed_goal "Step1_4_3a" MemoryImplementation.thy
   186    "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$    \
   187 \                  & unchanged (e p, c p, m p, rmhist!p) \
   188 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   189   (fn _ => [Clarsimp_tac 1,
   190             REPEAT (dresolve_tac (map temp_use [S3_excl,S4_excl]) 1),
   191             action_simp_tac 
   192                  (simpset() addsimps [e_def,c_def,m_def,resbar_def,S_def, S3_def]) [] [] 1
   193            ]);
   194 
   195 qed_goal "Step1_4_3b" MemoryImplementation.thy
   196    "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$ & unchanged (e p, c p, m p) \
   197 \      --> MemFail memCh (resbar rmhist) p"
   198   (fn _ => [Clarsimp_tac 1,
   199             dtac (temp_use S6_excl) 1,
   200             auto_tac (MI_css addsimps2 [RPCFail_def,MemFail_def,e_def,c_def,m_def,
   201 		                        resbar_def]),
   202             force_tac (MI_css addsimps2 [S3_def,S_def]) 1,
   203             auto_tac (MI_css addsimps2 [Return_def])
   204            ]);
   205 
   206 
   207 qed_goal "Step1_4_4a1" MemoryImplementation.thy
   208    "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l \
   209 \             & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l \
   210 \      --> ReadInner memCh mm (resbar rmhist) p l"
   211   (fn _ => [Clarsimp_tac 1,
   212             REPEAT (dtac (temp_use S4_excl) 1),
   213             action_simp_tac 
   214                (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def]) 
   215                [] [] 1,
   216             auto_tac (MI_css addsimps2 [resbar_def]),
   217 	    ALLGOALS (action_simp_tac 
   218                         (simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
   219 		                            S_def,S4_def,RdRequest_def,MemInv_def])
   220 		      [] [impE,MemValNotAResultE])
   221            ]);
   222 
   223 qed_goal "Step1_4_4a" MemoryImplementation.thy
   224    "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ \
   225 \           & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l)) \
   226 \      --> Read memCh mm (resbar rmhist) p"
   227   (fn _ => [ force_tac (MI_css addsimps2 [Read_def] addSEs2 [Step1_4_4a1]) 1 ]);
   228 
   229 qed_goal "Step1_4_4b1" MemoryImplementation.thy
   230    "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v   \
   231 \                   & unchanged (e p, c p, r p, rmhist!p) \
   232 \      --> WriteInner memCh mm (resbar rmhist) p l v"
   233   (fn _ => [Clarsimp_tac 1,
   234             REPEAT (dtac (temp_use S4_excl) 1),
   235             action_simp_tac 
   236                (simpset() addsimps [WriteInner_def, GoodWrite_def, BadWrite_def,
   237 			           e_def, c_def, m_def])
   238                [] [] 1,
   239 	    auto_tac (MI_css addsimps2 [resbar_def]),
   240 	    ALLGOALS (action_simp_tac
   241                         (simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def,
   242 		                            S_def,S4_def,WrRequest_def])
   243 		      [] [])
   244            ]);
   245 
   246 qed_goal "Step1_4_4b" MemoryImplementation.thy
   247    "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$   \
   248 \                 & unchanged (e p, c p, r p, rmhist!p) \
   249 \      --> Write memCh mm (resbar rmhist) p l"
   250   (fn _ => [ force_tac (MI_css addsimps2 [Write_def] addSEs2 [Step1_4_4b1]) 1 ]);
   251 
   252 qed_goal "Step1_4_4c" MemoryImplementation.thy
   253    "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$ & unchanged (e p, c p, r p) \
   254 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   255   (fn _ => [action_simp_tac
   256 	       (simpset() addsimps [e_def,c_def,r_def,resbar_def]) [] [] 1,
   257 	    REPEAT (dresolve_tac [temp_use S4_excl, temp_use S5_excl] 1),
   258 	    auto_tac (MI_fast_css addsimps2 [MemReturn_def,Return_def])
   259            ]);
   260 
   261 qed_goal "Step1_4_5a" MemoryImplementation.thy
   262    "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$ & unchanged (e p, c p, m p) \
   263 \      --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   264   (fn _ => [Clarsimp_tac 1,
   265             REPEAT (dresolve_tac [temp_use S5_excl, temp_use S6_excl] 1),
   266             auto_tac (MI_css addsimps2 [e_def,c_def,m_def, resbar_def]),
   267 	    auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def] 
   268                              addSDs2 [MVOKBAnotRF])
   269            ]);
   270 
   271 qed_goal "Step1_4_5b" MemoryImplementation.thy
   272    "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$ & unchanged (e p, c p, m p) \
   273 \      --> MemFail memCh (resbar rmhist) p"
   274   (fn _ => [Clarsimp_tac 1,
   275             dtac (temp_use S6_excl) 1,
   276             auto_tac (MI_css addsimps2 [e_def, c_def, m_def, RPCFail_def, Return_def,
   277 		 		        MemFail_def, resbar_def]),
   278 	    auto_tac (MI_css addsimps2 [S5_def,S_def])
   279            ]);
   280 
   281 qed_goal "Step1_4_6a" MemoryImplementation.thy
   282    "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$ & unchanged (e p, r p, m p) \
   283 \      --> MemReturn memCh (resbar rmhist) p"
   284   (fn _ => [Clarsimp_tac 1,
   285             dtac (temp_use S6_excl) 1,
   286             action_simp_tac
   287 	      (simpset() addsimps [e_def, r_def, m_def, MClkReply_def, MemReturn_def,
   288 				  Return_def, resbar_def]) [] [] 1,
   289 	    ALLGOALS Asm_full_simp_tac,  (* simplify if-then-else *)
   290 	    ALLGOALS (action_simp_tac
   291     	              (simpset() addsimps [MClkReplyVal_def,S6_def,S_def])
   292 		      [] [MVOKBARFnotNR])
   293            ]);
   294 
   295 qed_goal "Step1_4_6b" MemoryImplementation.thy
   296    "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$   \
   297 \                & unchanged (e p, r p, m p, rmhist!p) \
   298 \      --> MemFail memCh (resbar rmhist) p"
   299   (fn _ => [Clarsimp_tac 1,
   300             dtac (temp_use S3_excl) 1,
   301             action_simp_tac
   302 	       (simpset() addsimps [e_def, r_def, m_def, MClkRetry_def, MemFail_def, resbar_def])
   303 	       [] [] 1,
   304 	    auto_tac (MI_css addsimps2 [S6_def,S_def])
   305            ]);
   306 
   307 qed_goal "S_lemma" MemoryImplementation.thy
   308    "|- unchanged (e p, c p, r p, m p, rmhist!p) \
   309 \      --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
   310    (fn _ => [auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,caller_def,rtrner_def,
   311 					 S_def,Calling_def])
   312             ]);
   313 
   314 qed_goal "Step1_4_7H" MemoryImplementation.thy
   315    "|- unchanged (e p, c p, r p, m p, rmhist!p) \
   316 \      --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p, \
   317 \                     S4 rmhist p, S5 rmhist p, S6 rmhist p)"
   318    (fn _ => [Clarsimp_tac 1,
   319              rtac conjI 1,
   320              force_tac (MI_css addsimps2 [c_def]) 1,
   321              force_tac (MI_css addsimps2 [S1_def,S2_def,S3_def,S4_def,S5_def,S6_def]
   322                                addSIs2 [S_lemma]) 1
   323             ]);
   324 
   325 qed_goal "Step1_4_7" MemoryImplementation.thy
   326    "|- unchanged (e p, c p, r p, m p, rmhist!p) \
   327 \      --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p, S3 rmhist p, \
   328 \                     S4 rmhist p, S5 rmhist p, S6 rmhist p)"
   329   (fn _ => [rtac actionI 1,
   330             rewrite_goals_tac action_rews,
   331             rtac impI 1,
   332             forward_tac [temp_use Step1_4_7H] 1,
   333 	    auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,rtrner_def,resbar_def])
   334            ]);
   335 
   336 
   337 (* Frequently needed abbreviation: distinguish between idling and non-idling
   338    steps of the implementation, and try to solve the idling case by simplification
   339 *)
   340 fun split_idle_tac simps i = 
   341     EVERY [TRY (rtac actionI i),
   342 	   case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
   343 	   rewrite_goals_tac action_rews,
   344 	   forward_tac [temp_use Step1_4_7] i,
   345 	   asm_full_simp_tac (simpset() addsimps simps) i
   346 	  ];
   347 
   348 (* ----------------------------------------------------------------------
   349    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
   350    the specification's next-state relation.
   351 *)
   352 
   353 (* Steps that leave all variables unchanged are safe, so I may assume
   354    that some variable changes in the proof that a step is safe. *)
   355 qed_goal "unchanged_safe" MemoryImplementation.thy
   356    "|- (~unchanged (e p, c p, r p, m p, rmhist!p) \
   357 \        --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) \
   358 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   359    (fn _ => [split_idle_tac [square_def] 1,
   360              Force_tac 1
   361             ]);
   362 (* turn into (unsafe, looping!) introduction rule *)
   363 bind_thm("unchanged_safeI", impI RS (action_use unchanged_safe));
   364 
   365 qed_goal "S1safe" MemoryImplementation.thy
   366    "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   367 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   368    (fn _ => [Clarsimp_tac 1, 
   369              rtac unchanged_safeI 1,
   370              rtac idle_squareI 1,
   371 	     auto_tac (MI_css addSDs2 [Step1_2_1,Step1_4_1])
   372 	    ]);
   373 
   374 qed_goal "S2safe" MemoryImplementation.thy
   375    "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   376 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   377    (fn _ => [Clarsimp_tac 1, 
   378              rtac unchanged_safeI 1,
   379              rtac idle_squareI 1,
   380 	     auto_tac (MI_css addSDs2 [Step1_2_2,Step1_4_2])
   381 	    ]);
   382 
   383 qed_goal "S3safe" MemoryImplementation.thy
   384    "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   385 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   386    (fn _ => [Clarsimp_tac 1,
   387 	     rtac unchanged_safeI 1,
   388              auto_tac (MI_css addSDs2 [Step1_2_3]),
   389 	     auto_tac (MI_css addsimps2 [square_def,UNext_def]
   390 		              addSDs2 [Step1_4_3a,Step1_4_3b])
   391 	    ]);
   392 
   393 qed_goal "S4safe" MemoryImplementation.thy
   394    "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)  \
   395 \                   & (!l. $(MemInv mm l)) \
   396 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   397    (fn _ => [Clarsimp_tac 1,
   398 	     rtac unchanged_safeI 1,
   399              auto_tac (MI_css addSDs2 [Step1_2_4]),
   400 	     auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def]
   401                               addSDs2 [Step1_4_4a,Step1_4_4b,Step1_4_4c])
   402 	    ]);
   403 
   404 qed_goal "S5safe" MemoryImplementation.thy
   405    "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)  \
   406 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   407    (fn _ => [Clarsimp_tac 1,
   408 	     rtac unchanged_safeI 1,
   409              auto_tac (MI_css addSDs2 [Step1_2_5]),
   410 	     auto_tac (MI_css addsimps2 [square_def,UNext_def]
   411 		              addSDs2 [Step1_4_5a,Step1_4_5b])
   412 	    ]);
   413 
   414 qed_goal "S6safe" MemoryImplementation.thy
   415    "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)   \
   416 \      --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   417    (fn _ => [Clarsimp_tac 1,
   418 	     rtac unchanged_safeI 1,
   419              auto_tac (MI_css addSDs2 [Step1_2_6]),
   420 	     auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def]
   421 		              addSDs2 [Step1_4_6a,Step1_4_6b])
   422 	    ]);
   423 
   424 (* ----------------------------------------------------------------------
   425    Step 1.5: Temporal refinement proof, based on previous steps.
   426 *)
   427 
   428 section "The liveness part";
   429 
   430 use "MIlive.ML";
   431 
   432 section "Refinement proof (step 1.5)";
   433 
   434 (* Prove invariants of the implementation:
   435    a. memory invariant
   436    b. "implementation invariant": always in states S1,...,S6
   437 *)
   438 qed_goal "Step1_5_1a" MemoryImplementation.thy 
   439    "|- IPImp p --> (!l. []$MemInv mm l)"
   440    (fn _ => [auto_tac (MI_css addsimps2 [IPImp_def,box_stp_act]
   441 			      addSIs2 [MemoryInvariantAll])
   442 	    ]);
   443 
   444 qed_goal "Step1_5_1b" MemoryImplementation.thy
   445    "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p) \
   446 \      & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](!l. $MemInv mm l) \
   447 \      --> []ImpInv rmhist p"
   448    (fn _ => [inv_tac MI_css 1,
   449 	     auto_tac (MI_css addsimps2 [Init_def, ImpInv_def, box_stp_act]
   450                               addSDs2 [Step1_1]
   451 		              addDs2 [S1_successors,S2_successors,S3_successors,
   452 			              S4_successors,S5_successors,S6_successors])
   453             ]);
   454 
   455 (*** Initialization ***)
   456 qed_goal "Step1_5_2a" MemoryImplementation.thy
   457    "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"
   458    (fn _ => [auto_tac (MI_css addsimps2 [Init_def]
   459                               addSIs2 [Step1_1,Step1_3])
   460             ]);
   461 
   462 (*** step simulation ***)
   463 qed_goal "Step1_5_2b" MemoryImplementation.thy
   464    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)   \
   465 \                   & $ImpInv rmhist p & (!l. $MemInv mm l))       \
   466 \      --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   467    (fn _ => [auto_tac (MI_css 
   468                           addsimps2 [ImpInv_def] addSEs2 [STL4E]
   469                           addSDs2 [S1safe,S2safe,S3safe,S4safe,S5safe,S6safe])
   470             ]);
   471 
   472 
   473 (*** Liveness ***)
   474 qed_goal "GoodImpl" MemoryImplementation.thy
   475    "|- IPImp p & HistP rmhist p  \
   476 \      -->   Init(ImpInit p & HInit rmhist p)   \
   477 \          & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   478 \          & [](!l. $MemInv mm l) & []($ImpInv rmhist p) \
   479 \          & ImpLive p"
   480    (fn _ => [Clarsimp_tac 1,
   481 	     subgoal_tac
   482 	       "sigma |= Init(ImpInit p & HInit rmhist p) \
   483 \                        & [](ImpNext p) \
   484 \                        & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) \
   485 \                        & [](!l. $MemInv mm l)" 1,
   486 	     auto_tac (MI_css addsimps2 [split_box_conj,box_stp_act] addSDs2 [Step1_5_1b]),
   487 	     force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
   488 					  ImpLive_def,c_def,r_def,m_def]) 1,
   489 	     force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
   490 					  HistP_def,Init_def,ImpInit_def]) 1,
   491 	     force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def,
   492 					  ImpNext_def,c_def,r_def,m_def,split_box_conj]) 1,
   493 	     force_tac (MI_css addsimps2 [HistP_def]) 1,
   494              force_tac (MI_css addsimps2 [temp_use allT] addSDs2 [Step1_5_1a]) 1
   495 	    ]);
   496 
   497 (* The implementation is infinitely often in state S1... *)
   498 qed_goal "Step1_5_3a" MemoryImplementation.thy
   499    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   500 \      & [](!l. $MemInv mm l)  \
   501 \      & []($ImpInv rmhist p) & ImpLive p  \
   502 \      --> []<>S1 rmhist p"
   503    (fn _ => [clarsimp_tac (MI_css addsimps2 [ImpLive_def]) 1,
   504              rtac S1Infinite 1,
   505 	     force_tac (MI_css
   506 			  addsimps2 [split_box_conj,box_stp_act]
   507 			  addSIs2 [NotS1LeadstoS6,S2_live,S3_live,S4a_live,S4b_live,S5_live]) 1,
   508              auto_tac (MI_css addsimps2 [split_box_conj] addSIs2 [S6_live])
   509             ]);
   510 
   511 (* ... which implies that it satisfies the fairness requirements of the specification *)
   512 qed_goal "Step1_5_3b" MemoryImplementation.thy
   513    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   514 \      & [](!l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p  \
   515 \      --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   516    (fn _ => [ auto_tac (MI_css addSIs2 [RNext_fair,Step1_5_3a]) ]);
   517 
   518 qed_goal "Step1_5_3c" MemoryImplementation.thy
   519    "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   520 \      & [](!l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p  \
   521 \      --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   522    (fn _ => [ auto_tac (MI_css addSIs2 [Return_fair,Step1_5_3a]) ]);
   523 
   524 
   525 (* QED step of step 1 *)
   526 qed_goal "Step1" MemoryImplementation.thy
   527    "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
   528    (fn _ => [auto_tac
   529                (MI_css addsimps2 [UPSpec_def,split_box_conj]
   530 		       addSDs2 [GoodImpl]
   531                        addSIs2 [Step1_5_2a,Step1_5_2b,Step1_5_3b,Step1_5_3c])
   532             ]);
   533 
   534 
   535 (* ------------------------------ Step 2 ------------------------------ *)
   536 section "Step 2";
   537 
   538 qed_goal "Step2_2a" MemoryImplementation.thy
   539    "|- Write rmCh mm ires p l & ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p) \
   540 \      & $ImpInv rmhist p  \
   541 \      --> (S4 rmhist p)` & unchanged (e p, c p, r p, rmhist!p)"
   542    (fn _ => [Clarsimp_tac 1,
   543              dtac (action_use WriteS4) 1, atac 1,
   544              split_idle_tac [] 1,
   545              auto_tac (MI_css addsimps2 [ImpNext_def] 
   546                               addSDs2 [S4EnvUnch,S4ClerkUnch,S4RPCUnch]),
   547              auto_tac (MI_css addsimps2 [square_def] addDs2 [S4Write])
   548             ]);
   549 
   550 qed_goal "Step2_2" MemoryImplementation.thy
   551    "|-   (!p. ImpNext p) \
   552 \      & (!p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   553 \      & (!p. $ImpInv rmhist p) \
   554 \      & [? q. Write rmCh mm ires q l]_(mm!l) \
   555 \      --> [? q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   556    (fn _ => [auto_tac (MI_css addSIs2 [squareCI] addSEs2 [squareE]),
   557              REPEAT (ares_tac [exI, action_use Step1_4_4b] 1),
   558              force_tac (MI_css addSIs2 [WriteS4]) 1,
   559              auto_tac (MI_css addSDs2 [Step2_2a])
   560             ]);
   561 
   562 qed_goal "Step2_lemma" MemoryImplementation.thy
   563    "|-  [](  (!p. ImpNext p) \
   564 \          & (!p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \
   565 \          & (!p. $ImpInv rmhist p) \
   566 \          & [? q. Write rmCh mm ires q l]_(mm!l)) \
   567 \       --> [][? q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   568    (fn _ => [ force_tac (MI_css addSEs2 [STL4E] addSDs2 [Step2_2]) 1 ]);
   569 
   570 qed_goal "Step2" MemoryImplementation.thy
   571    "|- #l : #MemLoc & (!p. IPImp p & HistP rmhist p)  \
   572 \      --> MSpec memCh mm (resbar rmhist) l"
   573    (fn _ => [auto_tac (MI_css addsimps2 [MSpec_def]),
   574 	     force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 1,
   575 	     auto_tac (MI_css addSIs2 [Step2_lemma]
   576 		              addsimps2 [split_box_conj,all_box]),
   577 	     force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 4,
   578              auto_tac (MI_css addsimps2 [split_box_conj] addSEs2 [allE] addSDs2 [GoodImpl])
   579 	    ]);
   580 
   581 (* ----------------------------- Main theorem --------------------------------- *)
   582 section "Memory implementation";
   583 
   584 (* The combination of a legal caller, the memory clerk, the RPC component,
   585    and a reliable memory implement the unreliable memory.
   586 *)
   587 
   588 (* Implementation of internal specification by combination of implementation
   589    and history variable with explicit refinement mapping
   590 *)
   591 qed_goal "Impl_IUSpec" MemoryImplementation.thy
   592    "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"
   593    (fn _ => [auto_tac (MI_css addsimps2 [IUSpec_def,Implementation_def,IPImp_def,
   594 					 MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def]
   595 		              addSIs2 [Step1,Step2])
   596 	    ]);
   597 
   598 (* The main theorem: introduce hiding and eliminate history variable. *)
   599 qed_goal "Implementation" MemoryImplementation.thy
   600    "|- Implementation --> USpec memCh"
   601    (fn _ => [Clarsimp_tac 1,
   602              forward_tac [temp_use History] 1,
   603              auto_tac (MI_css addsimps2 [USpec_def] 
   604                               addIs2 [eexI, Impl_IUSpec, MI_base]
   605                               addSEs2 [eexE])
   606             ]);
   607 
   608